Require Export lemmas.
Require Export tacdef.
Remark Zmultbool_beta_pos : (b:bool)`0<=(Zmultbool b beta)`.
Hints Resolve Zmultbool_beta_pos.
Remark pow_beta_pos : (n:nat)`0<(pow beta n)`.
Hints Resolve pow_beta_pos.
Remark Zmultbool_pow_beta_pos : (b:bool)(n:nat)`0<=(Zmultbool b (pow beta n))`.
Hints Resolve Zmultbool_pow_beta_pos.
Theorem zlt_zero_beta :(Zlt ZERO beta).
Hints Resolve zlt_zero_beta.
Theorem sqrt_goal1 :
(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))
`np0+2 <= bound`
/\`sp0+1 <= bound`
/\`np0+1 <= bound`
/\(no_overlap np0 sp0 (1) (1))
/\(IsNormalized (I m0 np0 (2)) (pow beta (2)))
.
Theorem sqrt_goal2 :
(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))
(rb1 : bool)
(m1 : (array bound modZ))
(result : unit)
(Post_3 : `(I m0 np0 (S (S O))) = (I m1 sp0 (S O))*(I m1 sp0 (S O))+
((I m1 np0 (S O))+(Zmultbool rb1 beta))`
/\`(I m1 np0 (S O))+(Zmultbool rb1 beta) <= 2*
(I m1 sp0 (S O))`
/\((p:nat)
`0 <= p < bound`
->(lt p np0)\/(le (plus np0 (2)) p)
->(access m1 p)=(access m0 p)))
(SqrtremProp (I m0 np0 (mult (2) nn0)) (I m1 sp0 nn0)
`(I m1 np0 nn0)+(Zmultbool rb1 (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 m1 p))
.
Theorem sqrt_goal3 :
(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))
(lt (minus nn0 (div2' nn0)) nn0)
.
Theorem sqrt_goal4 :
(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))
`(plus sp0 (div2' nn0))+(minus nn0 (div2' nn0)) <= bound`
/\`(plus np0 (mult (S (S O)) (div2' nn0)))+2*(minus nn0 (div2' nn0))
<= bound`
/\`0
< (I m0 (plus np0 (mult (S (S O)) (div2' nn0)))
(mult (S (S O)) (minus nn0 (div2' nn0))))`
/\(`(plus np0 (mult (S (S O)) (div2' nn0)))+2*
(minus nn0 (div2' nn0)) <= (plus sp0 (div2' nn0))`
\/`(plus sp0 (div2' nn0))+(minus nn0 (div2' nn0))
<= (plus np0 (mult (S (S O)) (div2' nn0)))`)
/\(IsNormalized
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(pow beta (mult (2) (minus nn0 (div2' nn0)))))
/\(lt (0) (minus nn0 (div2' nn0)))
.
Theorem sqrt_goal5 :
(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_3 : ~nn0=(1))
(rz1 : Z)
(rb1 : bool)
(m1 : (array bound modZ))
(result : unit)
(Post_4 : (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`))
(lt (1) nn0)
/\(div2' nn0)=(div2' nn0)
/\(minus nn0 (div2' nn0))=(minus nn0 (div2' nn0))
/\(`(bool2Z rb1) = 0`\/`(bool2Z rb1) = 1`)
/\`np0+2*nn0 <= bound`
/\`sp0+nn0 <= bound`
/\(`np0+2*nn0 <= sp0`\/`sp0+nn0 <= np0`)
/\(`(bool2Z rb1) = 1`
->`(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))
< (I m1 (plus sp0 (div2' nn0))
(minus nn0 (div2' nn0)))`)
/\`(pow beta (minus nn0 (div2' nn0))) <= 2*
(I m1 (plus sp0 (div2' nn0))
(minus nn0 (div2' nn0)))`
.