Require Export lemmas.
Require Export memory.
Theorem sub_goal5 :
(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)
(rb1 : bool)
(m2 : (array bound modZ))
(result1 : unit)
(Post_5 : `(I m2 (plus np (mult (S (S O)) l)) (S O))
= (Zmultbool rb1 (pow beta (S O)))+
(I m1 (plus np (mult (S (S O)) l)) (S O))-(q+(bool2Z rb0))`
/\((p:nat)
`0 <= p < bound`
->(lt p (plus np (mult (2) l)))
\/(le (plus (plus np (mult (2) l)) (1)) p)
->(access m2 p)=(access m1 p)))
`(I m2 np nn) = (c-(c-(bool2Z rb1)))*(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 m2 p)=(access m p))
.