Require Export lemmas.
Require Export tacdef.
Require Export memory.
Require Export build_aux_thms.
Theorem sqrt_goal9 :
(sp : nat)
(np : nat)
(nn : nat)
(m : (array bound modZ))
(rb : bool)
(rz : Z)
(rphi1 : nat)
(mpn_dq_sqrtrem : (phi:nat)
(lt phi rphi1)
->(sp0,np0,nn0:nat; m0:(array bound modZ))
bool
->Z
->phi=nn0
->`sp0+nn0 <= bound`
/\`np0+2*nn0 <= bound`
/\`0 < (I m0 np0 (mult (S (S O)) nn0))`
/\(`np0+2*nn0 <= sp0`\/`sp0+nn0 <= np0`)
/\(IsNormalized
(I m0 np0 (mult (2) nn0))
(pow beta (mult (2) nn0)))
/\(lt (0) nn0)
->(sig_4 Z bool (array bound modZ) unit
[_:Z;
rb':bool;
m':(array bound modZ);
_:unit]
(SqrtremProp (I m0 np0 (mult (2) nn0))
(I m' sp0 nn0)
`(I m' np0 nn0)+
(Zmultbool rb' (pow beta nn0))`)
/\((p:nat)
`0 <= p < bound`
->~((le np0 p)
/\(lt p (plus np0 (mult (2) nn0)))
\/(le sp0 p)
/\(lt p (plus sp0 nn0)))
->(access m0 p)=(access m' p))))
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(Variant1 : rphi1=nn0)
(Pre_1 : `sp0+nn0 <= bound`
/\`np0+2*nn0 <= bound`
/\`0 < (I m0 np0 (mult (S (S O)) nn0))`
/\(`np0+2*nn0 <= sp0`\/`sp0+nn0 <= np0`)
/\(IsNormalized (I m0 np0 (mult (2) nn0))
(pow beta (mult (2) nn0)))/\(lt (0) nn0))
(resultb : bool)
(Test_4 : ~nn0=(1))
(rz1 : Z)
(rb1 : bool)
(m1 : (array bound modZ))
(result : unit)
(Post_5 : (SqrtremProp
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))
`(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))+
(Zmultbool rb1 (pow beta (minus nn0 (div2' nn0))))`)
/\((p:nat)
`0 <= p < bound`
->~((le (plus np0 (mult (2) (div2' nn0))) p)
/\(lt p
(plus (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0)))))
\/(le (plus sp0 (div2' nn0)) p)
/\(lt p
(plus (plus sp0 (div2' nn0))
(minus nn0 (div2' nn0)))))
->(access m0 p)=(access m1 p)))
(Pre_2 : (SqrtremProp
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))
`(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))+(bool2Z rb1)*
(pow beta (minus nn0 (div2' nn0)))`)
/\((p:nat)
`0 <= p < bound`
->~((le (plus np0 (mult (2) (div2' nn0))) p)
/\(lt p (plus np0 (mult (2) nn0)))
\/(le (plus sp0 (div2' nn0)) p)
/\(lt p (plus sp0 nn0)))
->(access m0 p)=(access m1 p))
/\(`(bool2Z rb1) = 0`\/`(bool2Z rb1) = 1`))
(rz2 : Z)
(rb2 : bool)
(q1 : Z)
(m2 : (array bound modZ))
(c0 : Z)
(result0 : unit)
(Post_6 : (Zdivprop'
`(bool2Z rb1)*(pow beta nn0)+
(I m1 (plus np0 (div2' nn0)) nn0)`
`2*(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))`
`q1*(pow beta (div2' nn0))+(I m2 sp0 (div2' nn0))`
`c0*(pow beta (minus nn0 (div2' nn0)))+
(I m2 (plus np0 (div2' nn0)) (minus nn0 (div2' nn0)))`)
/\((p:nat)
`0 <= p < bound`
->~((le sp0 p)/\(lt p (plus sp0 (div2' nn0)))
\/(le (plus np0 (div2' nn0)) p)
/\(lt p
(plus np0
(plus (plus (div2' nn0) (div2' nn0))
(minus nn0 (div2' nn0))))))
->(access m2 p)=(access m1 p))/\`0 <= q1 <= 1`)
(Pre_3 : (Zdivprop'
`(bool2Z rb1)*(pow beta nn0)+
(I m1 (plus np0 (div2' nn0)) nn0)`
`2*(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))`
`q1*(pow beta (div2' nn0))+(I m2 sp0 (div2' nn0))`
`c0*(pow beta (minus nn0 (div2' nn0)))+
(I m2 (plus np0 (div2' nn0)) (minus nn0 (div2' nn0)))`)
/\((p:nat)
`0 <= p < bound`
->~((le sp0 p)/\(lt p (plus sp0 (div2' nn0)))
\/(le (plus np0 (div2' nn0)) p)
/\(lt p
(plus np0
(plus (plus (div2' nn0) (div2' nn0))
(minus nn0 (div2' nn0))))))
->(access m2 p)=(access m1 p))/\`0 <= q1 <= 1`)
(rb3 : bool)
(m3 : (array bound modZ))
(c1 : Z)
(b0 : Z)
(result1 : unit)
(Post_7 : `(I m3 np0 nn0) = (c0-c1)*(pow beta nn0)+(I m2 np0 nn0)-
(q1*(pow beta (div2' nn0))+(I m2 sp0 (div2' nn0)))*(q1*
(pow beta (div2' nn0))+(I m2 sp0 (div2' nn0)))`
/\((p:nat)
`0 <= p < bound`
->~((le np0 p)/\(lt p (plus np0 (mult (2) nn0))))
->(access m3 p)=(access m2 p)))
(rb4 : bool)
(m4 : (array bound modZ))
(result2 : unit)
(Post_8 : `(Zmultbool rb4 (pow beta (minus nn0 (div2' nn0))))+
(I m4 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))
= (I m3 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0)))+q1`
/\((p:nat)
`0 <= p < bound`
->(lt p (plus sp0 (div2' nn0)))
\/(le
(plus (plus sp0 (div2' nn0))
(minus nn0 (div2' nn0))) p)
->(access m4 p)=(access m3 p)))
(rb5 : bool)
(q3 : Z)
(m5 : (array bound modZ))
(c2 : Z)
(result3 : unit)
(Post_9 : (`0 <= c1`->m5=m4/\`c2 = c1`)
/\(`c1 < 0`
->`(I m5 sp0 nn0)
= (Zminus ((bool2Z rb4)*(pow beta nn0)+(I m4 sp0 nn0))
1)`
/\`c2*(pow beta nn0)+(I m5 np0 nn0)
= (Zminus (c1*(pow beta nn0)+(I m4 np0 nn0)+2*
(bool2Z rb4)*(pow beta nn0)+2*(I m4 sp0 nn0)) 1)`
/\((p:nat)
`0 <= p < bound`
->~((le sp0 p)/\(lt p (plus sp0 nn0))
\/(le np0 p)
/\(lt p (plus np0 (mult (2) nn0))))
->(access m5 p)=(access m4 p))))
(SqrtremProp (I m0 np0 (mult (2) nn0)) (I m5 sp0 nn0)
`(I m5 np0 nn0)+(Zmultbool (Z2bool c2) (pow beta nn0))`)
/\((p:nat)
`0 <= p < bound`
->~((le np0 p)/\(lt p (plus np0 (mult (2) nn0)))
\/(le sp0 p)/\(lt p (plus sp0 nn0)))
->(access m0 p)=(access m5 p))
.