Require Export lemmas.
Require Export memory.
Theorem sub_goal1 :
(np : nat)
(sp : nat)
(nn : nat)
(b : Z)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta l)+(I m sp l) <= (pow beta l)`
/\`0 <= q <= 1`)
`sp+l <= bound`
/\`(plus np nn)+2*l <= bound`
/\(`(plus np nn)+2*l <= sp`\/`sp+l <= (plus np nn)`)
.
Theorem sub_goal2 :
(np : nat)
(sp : nat)
(nn : nat)
(b : Z)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta l)+(I m sp l) <= (pow beta l)`
/\`0 <= q <= 1`)
(m0 : (array bound modZ))
(result : unit)
(Post_2 : `(Zsquare (I m sp l))
= (I m0 (plus np nn) (mult (S (S O)) l))`
/\((p:nat)
`0 <= p < bound`
->(lt p (plus np nn))
\/(le (plus (plus np nn) (mult (2) l)) p)
->(access m0 p)=(access m p)))
`np+(mult (S (S O)) l) <= bound`
/\`(plus np nn)+(mult (S (S O)) l) <= bound`
/\`np+(mult (S (S O)) l) <= bound`
/\(no_overlap np np (mult (2) l) (mult (2) l))
/\(no_overlap np (plus np nn) (mult (2) l) (mult (2) l))
/\(no_overlap np (plus np nn) (mult (2) l) (mult (2) l))
.
Theorem sub_goal3 :
(np : nat)
(sp : nat)
(nn : nat)
(b : Z)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta l)+(I m sp l) <= (pow beta l)`
/\`0 <= q <= 1`)
(m0 : (array bound modZ))
(result : unit)
(Post_3 : `(Zsquare (I m sp l))
= (I m0 (plus np nn) (mult (S (S O)) l))`
/\((p:nat)
`0 <= p < bound`
->(lt p (plus np nn))
\/(le (plus (plus np nn) (mult (2) l)) p)
->(access m0 p)=(access m p)))
(rb0 : bool)
(m1 : (array bound modZ))
(result0 : unit)
(Post_4 : `(I m1 np (mult (S (S O)) l))
= (Zmultbool rb0 (pow beta (mult (S (S O)) l)))+
(I m0 np (mult (S (S O)) l))-
(I m0 (plus np nn) (mult (S (S O)) l))`
/\((p:nat)
`0 <= p < bound`
->(lt p np)\/(le (plus np (mult (2) l)) p)
->(access m1 p)=(access m0 p)))
(resultb : bool)
(Test_2 : l=h)
`(I m1 np nn) = (c-(c-(q+(bool2Z rb0))))*(pow beta nn)+(I m np nn)-
(q*(pow beta l)+(I m sp l))*(q*(pow beta l)+(I m sp l))`
/\((p:nat)
`0 <= p < bound`
->~((le np p)/\(lt p (plus np (mult (2) nn))))
->(access m1 p)=(access m p))
.
Theorem sub_goal4 :
(np : nat)
(sp : nat)
(nn : nat)
(b : Z)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta l)+(I m sp l) <= (pow beta l)`
/\`0 <= q <= 1`)
(m0 : (array bound modZ))
(result : unit)
(Post_3 : `(Zsquare (I m sp l))
= (I m0 (plus np nn) (mult (S (S O)) l))`
/\((p:nat)
`0 <= p < bound`
->(lt p (plus np nn))
\/(le (plus (plus np nn) (mult (2) l)) p)
->(access m0 p)=(access m p)))
(rb0 : bool)
(m1 : (array bound modZ))
(result0 : unit)
(Post_4 : `(I m1 np (mult (S (S O)) l))
= (Zmultbool rb0 (pow beta (mult (S (S O)) l)))+
(I m0 np (mult (S (S O)) l))-
(I m0 (plus np nn) (mult (S (S O)) l))`
/\((p:nat)
`0 <= p < bound`
->(lt p np)\/(le (plus np (mult (2) l)) p)
->(access m1 p)=(access m0 p)))
(resultb : bool)
(Test_2 : ~l=h)
`(plus np (mult (S (S O)) l))+(S O) <= bound`
/\`(plus np (mult (S (S O)) l))+(S O) <= bound`
/\`0 <= q+(bool2Z rb0) < beta`
/\(no_overlap (plus np (mult (2) l)) (plus np (mult (2) l)) (1)
(1))
.