Require Export sqrt_prog.
Require Export div_goals.
Require Export div_goals2.
Require Export div_goals3.
Require Export div_goals4.
Require Export div_goals5.
Require Export div_goals6.
Require Export div_goals7.
Require Export div_goals8.
Require Export div_goals9.
Require Export div_goals10.
Require Export div_goals11.
Require Export div_goals12.
Require Export div_goals13.
Correctness division_step
fun (np:nat)(sp:nat)(nn:nat)(l:nat ref)(h:nat ref)(c: Z ref)(q:Z ref) ->
{(lt (S O) nn)
/\(l=(div2' nn))/\(h=(minus nn (div2' nn)))/\((q=ZERO)\/(q=`1`))
/\ (`np+2*nn<=bound`)/\(`sp+nn<=bound`)
/\ (`np +2*nn <= sp`\/`sp+nn <= np`)
/\ (`q=1` -> `(I m (plus np (mult (S (S O)) l)) h) < (I m (plus sp l) h)`)
/\ `(pow beta h) <= 2*(I m (plus sp l) h)`}
begin
(if (Z_noteq_bool !q ZERO)
then
(mpn_sub_n (plus np (mult (S (S O)) !l))
(plus np (mult (S (S O)) !l))
(plus sp !l)
!h)
else tt)
{`(I m@ (plus np (mult (S (S O)) l)) h) + (q*(pow beta h))
-(q*(I m@ (plus sp l) h))=
(I m (plus np (mult (S (S O)) l)) h)` /\
((p:nat)`0<=p<bound`->~(((le (plus np (mult (2) l)) p)/\
(lt p (plus np (plus (mult (2) l) h)))))->
(access m p)=(access m@ p))};
(mpn_divrem sp
(plus np !l)
nn
(plus sp !l)
!h);
q:= (Zplus !q (bool2Z !rb));
(single_and_1 sp);
c:= !rz;
(mpn_rshift2 sp sp !l);
label avant_affectation;
(m[(plus sp (pred !l))] :=
(I_or (plus sp (pred !l)) (shift_1 !q))
{`(modZtoZ result) =
(modZtoZ (access m@avant_affectation (plus sp (pred l)))) + (aux_shift_1 q)`})
{`(modZtoZ (access m (plus sp (pred l)))) =
(modZtoZ (access m@ (plus sp (pred l)))) + (aux_shift_1 q)`/\
((p:nat)((`0<=p<bound`/\~`p=(plus sp (pred l))`)->(access m p)=(access m@ p)))};
q := (shift_2 !q);
if (Z_noteq_bool !c ZERO)
then
begin
(mpn_add_n (plus np !l)
(plus np !l)
(plus sp !l)
!h);
c := (bool2Z !rb)
end
end
{(Zdivprop' `q@ *(pow beta nn) +
(I m@
(plus np l) nn)`
`2 *(I m@
(plus sp l) h)`
`q * (pow beta l) + (I m sp l)`
`c * (pow beta h) + (I m (plus np l) h)`)
/\
((p:nat)`0<=p<bound`->~((le sp p)/\ (lt p (plus sp l))\/
(le (plus np l) p)/\ (lt p (plus np (plus (plus l l) h))))->
(access m p)=(access m@ p))/\`0<=q<=1`}.
Apply div_goal1
with nn := nn
q := q
m := m ; Assumption.
Apply div_goal2
with nn := nn
q := q
rb0 := rb0
; Assumption.
Apply div_goal3
with nn := nn
q := q
; Assumption.
Apply div_goal4
with nn := nn
q := q
m := m; Assumption.
Apply div_goal5
with np := np
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1; Assumption.
Apply div_goal6
with np := np
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
rz0 := rz0; Assumption.
Apply div_goal7
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
rz0 := rz0; Assumption.
Apply div_goal8
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
rz0 := rz0
y0 := y0; Assumption.
Apply div_goal9
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
rz0 := rz0 ; Assumption.
Apply div_goal10
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
m3 := m3
rz0 := rz0 ; Assumption.
Apply div_goal11
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
m3 := m3
rz0 := rz0 ; Assumption.
Apply div_goal12
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
m3 := m3
rz0 := rz0 ; Assumption.
Apply div_goal13
with np := np
sp := sp
l := l
h := h
nn := nn
q := q
m := m
m0 := m0
rb1 := rb1
m1 := m1
m2 := m2
rz0 := rz0 ; Assumption.
Defined.