Require Export lemmas.
Require Export tacdef.
Require Export memory.
Lemma sqrt_goals9_1' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(H : `0
<= (R1 (pow beta (div2' nn0)) (I m0 np0 (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)))))`)
`0 <= c1`
.
Lemma sqrt_goals9_2' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(HdivN : (Zdivprop' (I m0 np0 (mult (2) nn0))
(pow beta (mult (2) (div2' nn0)))
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(I m0 np0 (mult (2) (div2' nn0)))))
(HdivN'' : (Zdivprop' (I m0 np0 (mult (2) (div2' nn0)))
(pow beta (div2' nn0))
(I m0 (plus np0 (div2' nn0)) (div2' nn0))
(I m0 np0 (div2' nn0))))
(HdivR'N1 : (Zdivprop'
`((bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0))))*(pow beta (div2' nn0))+
(I m0 (plus np0 (div2' nn0)) (div2' 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)))`))
(Hnorm : (IsNormalized (I m0 np0 (mult (2) nn0))
(Zsquare
`(pow beta (minus nn0 (div2' nn0)))*
(pow beta (div2' nn0))`)))
(HR1_neg_c1_neg : `(R1 (pow beta (div2' nn0))
(I m0 np0 (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))))) < 0`
->`c1 < 0`)
(HsS' : (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)))
`(bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))`))
(Hs2 : (SqrtremProp2 (I m0 np0 (mult (2) nn0)) (I m5 sp0 nn0)
`(I m5 np0 nn0)+c2*(pow beta nn0)`))
(H : `(R1 (pow beta (div2' nn0)) (I m0 np0 (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))))) < 0`)
`(I m5 np0 nn0)+(Zmultbool (Z2bool c2) (pow beta nn0))
= (R1 (pow beta (div2' nn0)) (I m0 np0 (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)))))+(2*
(S1 (pow beta (div2' nn0)) (q1*(pow beta (div2' nn0))+
(I m2 sp0 (div2' nn0)))
(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0))))-1)`.
Lemma sqrt_goals9_3' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(Hs2 : (SqrtremProp2 (I m0 np0 (mult (2) nn0)) (I m5 sp0 nn0)
`(I m5 np0 nn0)+c2*(pow beta nn0)`))
(H : `0
<= (R1 (pow beta (div2' nn0)) (I m0 np0 (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)))))`)
`(I m5 np0 nn0)+(Zmultbool (Z2bool c2) (pow beta nn0))
= (R1 (pow beta (div2' nn0)) (I m0 np0 (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)))))`
.
Lemma sqrt_goals9_4' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(HdivN : (Zdivprop' (I m0 np0 (mult (2) nn0))
(pow beta (mult (2) (div2' nn0)))
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(I m0 np0 (mult (2) (div2' nn0)))))
(HdivN'' : (Zdivprop' (I m0 np0 (mult (2) (div2' nn0)))
(pow beta (div2' nn0))
(I m0 (plus np0 (div2' nn0)) (div2' nn0))
(I m0 np0 (div2' nn0))))
(HdivR'N1 : (Zdivprop'
`((bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0))))*(pow beta (div2' nn0))+
(I m0 (plus np0 (div2' nn0)) (div2' 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)))`))
(Hnorm : (IsNormalized (I m0 np0 (mult (2) nn0))
(Zsquare
`(pow beta (minus nn0 (div2' nn0)))*
(pow beta (div2' nn0))`)))
(HR1_neg_c1_neg : `(R1 (pow beta (div2' nn0))
(I m0 np0 (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))))) < 0`
->`c1 < 0`)
(HsS' : (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)))
`(bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))`))
(Hs2 : (SqrtremProp2 (I m0 np0 (mult (2) nn0)) (I m5 sp0 nn0)
`(I m5 np0 nn0)+c2*(pow beta nn0)`))
(S2eq : `0
<= (R1 (pow beta (div2' nn0)) (I m0 np0 (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)))))`
->`(I m5 sp0 nn0)
= (S1 (pow beta (div2' nn0)) (q1*(pow beta (div2' nn0))+
(I m2 sp0 (div2' nn0)))
(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0))))`)
(H : `(R1 (pow beta (div2' nn0)) (I m0 np0 (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))))) < 0`)
`(I m5 sp0 nn0)
= (S1 (pow beta (div2' nn0)) (q1*(pow beta (div2' nn0))+
(I m2 sp0 (div2' nn0)))
(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0))))-1`
.
Lemma sqrt_goals9_5' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(HdivN : (Zdivprop' (I m0 np0 (mult (2) nn0))
(pow beta (mult (2) (div2' nn0)))
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(I m0 np0 (mult (2) (div2' nn0)))))
(HdivN'' : (Zdivprop' (I m0 np0 (mult (2) (div2' nn0)))
(pow beta (div2' nn0))
(I m0 (plus np0 (div2' nn0)) (div2' nn0))
(I m0 np0 (div2' nn0))))
(HdivR'N1 : (Zdivprop'
`((bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0))))*(pow beta (div2' nn0))+
(I m0 (plus np0 (div2' nn0)) (div2' 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)))`))
(Hnorm : (IsNormalized (I m0 np0 (mult (2) nn0))
(Zsquare
`(pow beta (minus nn0 (div2' nn0)))*
(pow beta (div2' nn0))`)))
(HR1_neg_c1_neg : `(R1 (pow beta (div2' nn0))
(I m0 np0 (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))))) < 0`
->`c1 < 0`)
(HsS' : (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)))
`(bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))`))
(Hs2 : (SqrtremProp2 (I m0 np0 (mult (2) nn0)) (I m5 sp0 nn0)
`(I m5 np0 nn0)+c2*(pow beta nn0)`))
(H : `0
<= (R1 (pow beta (div2' nn0)) (I m0 np0 (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)))))`)
`(I m5 sp0 nn0)
= (S1 (pow beta (div2' nn0)) (q1*(pow beta (div2' nn0))+
(I m2 sp0 (div2' nn0)))
(I m1 (plus sp0 (div2' nn0)) (minus nn0 (div2' nn0))))`
.
Lemma sqrt_goals9_6' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(HdivN : (Zdivprop' (I m0 np0 (mult (2) nn0))
(pow beta (mult (2) (div2' nn0)))
(I m0 (plus np0 (mult (2) (div2' nn0)))
(mult (2) (minus nn0 (div2' nn0))))
(I m0 np0 (mult (2) (div2' nn0)))))
(HdivN'' : (Zdivprop' (I m0 np0 (mult (2) (div2' nn0)))
(pow beta (div2' nn0))
(I m0 (plus np0 (div2' nn0)) (div2' nn0))
(I m0 np0 (div2' nn0))))
(HdivR'N1 : (Zdivprop'
`((bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0))))*(pow beta (div2' nn0))+
(I m0 (plus np0 (div2' nn0)) (div2' 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)))`))
(Hnorm : (IsNormalized (I m0 np0 (mult (2) nn0))
(Zsquare
`(pow beta (minus nn0 (div2' nn0)))*
(pow beta (div2' nn0))`)))
(HR1_neg_c1_neg : `(R1 (pow beta (div2' nn0))
(I m0 np0 (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))))) < 0`
->`c1 < 0`)
(HsS' : (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)))
`(bool2Z rb1)*(pow beta (minus nn0 (div2' nn0)))+
(I m1 (plus np0 (mult (S (S O)) (div2' nn0)))
(minus nn0 (div2' nn0)))`))
(SqrtremProp2 (I m0 np0 (mult (2) nn0)) (I m5 sp0 nn0)
`(I m5 np0 nn0)+c2*(pow beta nn0)`)
.
Lemma sqrt_goals9_7' :
(sp0 : nat)
(np0 : nat)
(nn0 : nat)
(m0 : (array bound modZ))
(rb0 : bool)
(rz0 : Z)
(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) = (bool2Z rb4)*(pow beta nn0)+
(I m4 sp0 nn0)-1`
/\`c2*(pow beta nn0)+(I m5 np0 nn0) = 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))))
(H : `(R1 (pow beta (div2' nn0)) (I m0 np0 (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))))) < 0`)
`c1 < 0`.