Require Export lemmas.
Require Export tacdef.
Require Export memory.
Theorem auxiliary_for_sqrt_goals1 :
(sp : nat)
(np : nat)
(nn : nat)
(m : (array bound modZ))
(rb : bool)
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(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))
(rb1 : bool)
(m1 : (array bound modZ))
(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`))
(q1 : Z)
(m2 : (array bound modZ))
(c0 : Z)
(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)))`))
`q1*(pow beta (div2' nn0))+(I m2 sp0 (div2' nn0))
<= (pow beta (div2' nn0))`
.
Theorem sqrt_goal6 :
(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`)
(lt (1) nn0)
/\(div2' nn0)=(div2' nn0)
/\(minus nn0 (div2' nn0))=(minus nn0 (div2' nn0))
/\`np0+2*nn0 <= bound`
/\`sp0+nn0 <= bound`
/\(`np0+2*nn0 <= sp0`\/`sp0+nn0 <= np0`)
/\`q1*(pow beta (div2' nn0))+(I m2 sp0 (div2' nn0))
<= (pow beta (div2' nn0))`/\`0 <= q1 <= 1`
.
Theorem sqrt_goal7 :
(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)))
`(plus sp0 (div2' nn0))+(minus nn0 (div2' nn0)) <= bound`
/\`(plus sp0 (div2' nn0))+(minus nn0 (div2' nn0)) <= bound`
/\`0 <= q1 < beta`
/\(no_overlap (plus sp0 (div2' nn0)) (plus sp0 (div2' nn0))
(minus nn0 (div2' nn0)) (minus nn0 (div2' nn0)))
.
Theorem sqrt_goal8 :
(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)))
(lt (1) nn0)
/\(div2' nn0)=(div2' nn0)
/\(minus nn0 (div2' nn0))=(minus nn0 (div2' nn0))
/\`np0+2*nn0 <= bound`
/\`sp0+nn0 <= bound`
/\(`np0+2*nn0 <= sp0`\/`sp0+nn0 <= np0`)
/\`(bool2Z rb4)*(pow beta nn0)+(I m4 sp0 nn0)
<= (pow beta nn0)`
/\`0 < (bool2Z rb4)*(pow beta nn0)+(I m4 sp0 nn0)`
.