Require Export lemmas.
Require Export tacdef.
Require Export memory.
Theorem sqrt_goal10 :
(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_2 : ~nn0=(1))
(rz1 : Z)
(rb1 : bool)
(m1 : (array bound modZ))
(result : unit)
(Post_3 : (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)))
(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`)
.