Require Export lemmas.
Require Export tacdef.
Require Export memory.
Theorem correct_goal1 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `c < 0`)
`sp+nn <= bound`
/\`np+nn <= bound`
/\`0 <= (S (S O)) < beta`/\(no_overlap np sp nn nn)
.
Theorem correct_goal2 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `c < 0`)
(m0 : (array bound modZ))
(x0 : Z)
(Post_3 : (Post_mpn_addmul_1 m0 m np sp nn (2) x0))
(Post_mpn_addmul_1 m0 m np sp nn (2) (Zminus `x0+2*q` `2*q`))
.
Theorem correct_goal3 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `c < 0`)
(m0 : (array bound modZ))
(x0 : Z)
(Post_3 : (Post_mpn_addmul_1 m0 m np sp nn (2) (Zminus x0 `2*q`)))
(Post_mpn_addmul_1 m0 m np sp nn (2)
(Zminus (Zminus `x0+c` `2*q`) c))
.
Theorem correct_goal4 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `c < 0`)
(m0 : (array bound modZ))
(c0 : Z)
(result : unit)
(Post_3 : (Post_mpn_addmul_1 m0 m np sp nn (2)
(Zminus (Zminus c0 `2*q`) c)))
`np+nn <= bound`
/\`np+nn <= bound`/\`0 <= (S O) < beta`/\(no_overlap np np nn nn)
.
Theorem correct_goal5 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `c < 0`)
(m0 : (array bound modZ))
(c0 : Z)
(result : unit)
(Post_3 : (Post_mpn_addmul_1 m0 m np sp nn (2)
(Zminus (Zminus c0 `2*q`) c)))
(rb0 : bool)
(m1 : (array bound modZ))
(result0 : unit)
(Post_4 : `(I m1 np nn) = (Zmultbool rb0 (pow beta nn))+(I m0 np nn)-
(S O)`
/\((p:nat)
`0 <= p < bound`
->(lt p np)\/(le (plus np nn) p)
->(access m1 p)=(access m0 p)))
`sp+nn <= bound`
/\`sp+nn <= bound`/\`0 <= (S O) < beta`/\(no_overlap sp sp nn nn)
.
Theorem correct_goal6 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `c < 0`)
(m0 : (array bound modZ))
(c0 : Z)
(result : unit)
(Post_3 : (Post_mpn_addmul_1 m0 m np sp nn (2)
(Zminus (Zminus c0 `2*q`) c)))
(rb0 : bool)
(m1 : (array bound modZ))
(result0 : unit)
(Post_4 : `(I m1 np nn) = (Zmultbool rb0 (pow beta nn))+(I m0 np nn)-
(S O)`
/\((p:nat)
`0 <= p < bound`
->(lt p np)\/(le (plus np nn) p)
->(access m1 p)=(access m0 p)))
(rb1 : bool)
(m2 : (array bound modZ))
(result1 : unit)
(Post_5 : `(I m2 sp nn) = (Zmultbool rb1 (pow beta nn))+(I m1 sp nn)-
(S O)`
/\((p:nat)
`0 <= p < bound`
->(lt p sp)\/(le (plus sp nn) p)
->(access m2 p)=(access m1 p)))
(`0 <= c`->m2=m/\`(Zminus c0 (bool2Z rb0)) = c`)
/\(`c < 0`
->`(I m2 sp nn) = (Zminus (q*(pow beta nn)+(I m sp nn)) 1)`
/\`(Zminus c0 (bool2Z rb0))*(pow beta nn)+(I m2 np nn)
= (Zminus (c*(pow beta nn)+(I m np nn)+2*q*(pow beta nn)+2*
(I m sp nn)) 1)`
/\((p:nat)
`0 <= p < bound`
->~((le sp p)/\(lt p (plus sp nn))
\/(le np p)/\(lt p (plus np (mult (2) nn))))
->(access m2 p)=(access m p)))
.
Theorem correct_goal7 :
(np : nat)
(sp : nat)
(nn : nat)
(c : Z)
(h : nat)
(l : nat)
(m : (array bound modZ))
(q : Z)
(rb : bool)
(Pre_1 : (lt (1) nn)
/\l=(div2' nn)
/\h=(minus nn (div2' nn))
/\`np+2*nn <= bound`
/\`sp+nn <= bound`
/\(`np+2*nn <= sp`\/`sp+nn <= np`)
/\`q*(pow beta nn)+(I m sp nn) <= (pow beta nn)`
/\`0 < q*(pow beta nn)+(I m sp nn)`)
(resultb : bool)
(Test_2 : `0 <= c`)
(`0 <= c`->m=m/\`c = c`)
/\(`c < 0`
->`(I m sp nn) = (Zminus (q*(pow beta nn)+(I m sp nn)) 1)`
/\`c*(pow beta nn)+(I m np nn)
= (Zminus (c*(pow beta nn)+(I m np nn)+2*q*(pow beta nn)+2*
(I m sp nn)) 1)`
/\((p:nat)
`0 <= p < bound`
->~((le sp p)/\(lt p (plus sp nn))
\/(le np p)/\(lt p (plus np (mult (2) nn))))
->(access m p)=(access m p)))
.