Require Export sqrt_prog.
Require Export sub_goals.
Require Export sub_goals2.
Correctness square_s_and_sub
fun (np : nat)(sp : nat)(nn:nat) (l: nat ref)(h:nat ref)
(q : Z ref)(c:Z ref) (b:Z ref) ->
{(lt (S O) 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 l) + (I m sp l) <= (pow beta l)` /\ `0 <= q <= 1`}
begin
(mpn_sqr_n (plus np nn) sp !l);
(mpn_sub_n np np (plus np nn) (mult (S (S O)) !l));
b := !q + (bool2Z !rb);
if (nat_eq_bool !l !h) then
c := !c - !b
else
begin
(mpn_sub_1 (plus np (mult (S (S O)) !l))
(plus np (mult (S (S O)) !l))
(S O) !b);
c := !c - (bool2Z !rb)
end
end
{`(I m np nn)=(c@-c) * (pow beta nn) +
(I m@ np nn) - (q@ * (pow beta l) + (I m@ sp l))*
(q@ * (pow beta l) + (I m@ sp l))` /\
(p:nat)`0<=p<bound`->~((le np p)/\(lt p (plus np (mult (S (S O)) nn)))) ->
(access m p)=(access m@ p)}.
Apply sub_goal1 with
np := np sp := sp nn := nn h:= h l := l m := m q:=q;Assumption.
Apply sub_goal2 with
np := np sp := sp nn := nn h:= h l := l m := m q:=q
m0 := m0;Assumption.
Apply sub_goal3 with
np := np sp := sp nn := nn h:= h l := l m := m q:=q
m0 := m0 rb0 := rb0 m1 := m1;Assumption.
Apply sub_goal4 with
np := np sp := sp nn := nn h:= h l := l m := m q:=q
m0 := m0 rb0 := rb0 m1 := m1;Assumption.
Apply sub_goal5 with
np := np sp := sp nn := nn h:= h l := l m := m q:=q
m0 := m0 rb0 := rb0 m1 := m1 rb1 := rb1 m2 := m2;Assumption.
Defined.