Require Export lemmas.
Require Export tacdef.
Require Export memory.
Require Export Decidable.
Theorem div_goal12 :
(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)`)
(rb0 : bool)
(m0 : (array bound modZ))
(result : unit)
(Post_4 : `(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)))
(rb1 : bool)
(m1 : (array bound modZ))
(result0 : unit)
(Post_5 : `(I m0 (plus np l) nn)
= ((Zmultbool rb1 (pow beta (minus nn h)))+
(I m1 sp (minus nn h)))*(I m0 (plus sp l) h)+
(I m1 (plus np l) h)`
/\`(I m1 (plus np l) h) < (I m0 (plus sp l) h)`
/\((p:nat)
`0 <= p < bound`
->((lt p sp)\/(le (plus sp (minus nn h)) p))
/\((lt p (plus np l))\/(le (plus (plus np l) h) p))
->(access m1 p)=(access m0 p)))
(rz0 : Z)
(result1 : unit)
(Post_6 : `rz0 = (modZtoZ (isEvenOrOdd m1 sp))`)
(m2 : (array bound modZ))
(result2 : unit)
(Post_7 : `(I m1 sp l) = 2*(I m2 sp l)+(modZtoZ (isEvenOrOdd m1 sp))`
/\((p:nat)
`0 <= p < bound`
->(lt p sp)\/(le (plus sp l) p)
->(access m2 p)=(access m1 p)))
(Pre_2 : `0 <= (plus sp (pred l)) < bound`)
(m3 : (array bound modZ))
(result3 : unit)
(Post_8 : `(modZtoZ (access m3 (plus sp (pred l))))
= (modZtoZ (access m2 (plus sp (pred l))))+
(aux_shift_1 (q+(bool2Z rb1)))`
/\((p:nat)
`0 <= p < bound`/\`p <> (plus sp (pred l))`
->(access m3 p)=(access m2 p)))
(resultb : bool)
(Test_3 : `rz0 = 0`)
(Zdivprop' `q*(pow beta nn)+(I m (plus np l) nn)`
`2*(I m (plus sp l) h)`
`(shift_2 (q+(bool2Z rb1)))*(pow beta l)+(I m3 sp l)`
`rz0*(pow beta h)+(I m3 (plus np l) h)`)
/\((p:nat)
`0 <= p < bound`
->~((le sp p)/\(lt p (plus sp l))
\/(le (plus np l) p)/\(lt p (plus np (plus (plus l l) h))))
->(access m3 p)=(access m p))
/\`0 <= (shift_2 (q+(bool2Z rb1))) <= 1`
.