Require Export lemmas.
Require Export tacdef.
Theorem div_goal2 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(rz : Z)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\(`q = 0`\/`q = 1`)
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\(`q = 1`
->`(I m (plus np (mult (S (S O)) l)) h)
< (I m (plus sp l) h)`)
/\`(pow beta h) <= 2*(I m (plus sp l) h)`)
(resultb : bool)
(Test_2 : `q <> 0`)
(rb0 : bool)
(m0 : (array bound modZ))
(result : unit)
(Post_3 : `(I m0 (plus np (mult (S (S O)) l)) h)
= (Zmultbool rb0 (pow beta h))+
(I m (plus np (mult (S (S O)) l)) h)-
(I m (plus sp l) h)`
/\((p:nat)
`0 <= p < bound`
->(lt p (plus np (mult (2) l)))
\/(le (plus (plus np (mult (2) l)) h) p)
->(access m0 p)=(access m p)))
`(I m (plus np (mult (S (S O)) l)) h)+q*(pow beta h)-q*
(I m (plus sp l) h) = (I m0 (plus np (mult (S (S O)) l)) h)`
/\((p:nat)
`0 <= p < bound`
->~((le (plus np (mult (2) l)) p)
/\(lt p (plus np (plus (mult (2) l) h))))
->(access m0 p)=(access m p))
.