...
  View open merge request
Commits (1)
(* This module implements constructive reals (exact real numbers),
following the algorithms given in Valérie Ménissier-Morain's
thesis: "conception, algorithmique et performances d'une
implémentation informatique en précision arbitraire".
The division algorithm is different from the one presented in the thesis.
*)
module Z
use mach.int.Int
use real.RealInfix
use int.Power
use int.EuclideanDivision as ED
let rec power2 (l:int)
requires { 0 <= l }
ensures { result = power 2 l }
variant { l }
=
if l = 0 then 1 else 2 * power2 (l-1)
let shift_left (z: int) (l:int) : int
requires { 0 <= l }
ensures { result = z * (power 2 l) } =
z * (power2 l)
let lemma euclid_uniq (x y q : int) : unit
requires { y > 0 }
requires { q * y <= x < q * y + y }
ensures { ED.div x y = q } =
()
let ediv_mod (x:int) (y:int) : (int, int)
requires { 0 < y }
ensures { let d,r = result in
d = ED.div x y /\ r = ED.mod x y } =
let rec aux (x q r:int) : (int, int)
requires { x = q * y + r }
requires { 0 <= r }
ensures { let q,_ = result in ED.div x y = q }
ensures { let _,r = result in ED.mod x y = r }
variant { r }
=
if r < y then q,r
else aux x (q+1) (r-y)
in
if 0 <= x then
aux x 0 x
else
let q,r = aux (-x) 0 (-x) in
if 0 = r then begin euclid_uniq x y (-q); (-q,0) end
else begin euclid_uniq x y (-q-1); (-q-1,y - r) end
let shift_right (z: int) (l:int) : int
requires { 0 <= l }
ensures { result = ED.div z (power 2 l) } =
let d,_ = ediv_mod z (power2 l) in
d
use real.Square
use real.FromInt
use real.Truncate
let function isqrt (n:int) : int
requires { 0 <= n }
ensures { result = floor (sqrt (from_int n)) } =
let rec aux (res sum:int) : int
requires { 0 <= res }
requires { from_int n >=. sqr (from_int res) }
requires { from_int sum = sqr (from_int (res + 1)) }
ensures { result = floor (sqrt (from_int n)) }
variant { n - sum } =
if n < sum then begin
assert { from_int res <=. (sqrt (from_int n))
by sqrt (sqr (from_int res)) <=. (sqrt (from_int n))
};
assert { (sqrt (from_int n)) <. (from_int res) +. 1. };
res
end
else begin
aux (res + 1) (sum + (2 * res) + 3)
end
in
aux 0 1
end
module RealArith
use Z
use mach.int.Int
use real.RealInfix
use real.FromInt
use real.Truncate
use int.EuclideanDivision as ED
use int.Power
lemma mul_str_ordr: forall x y z. 0. <. z -> x <. y -> x *. z <. y *. z
lemma mul_str_ordl: forall x y z. 0. <. z -> x <. y -> z *. x <. z *. y
lemma mul_ordr: forall x y z. 0. <=. z -> x <=. y -> x *. z <=. y *. z
lemma mul_ordl: forall x y z. 0. <=. z -> x <=. y -> z *. x <=. z *. y
lemma mul_ord_zero: forall x z. 0. <=. z -> 0. <=. x -> 0. <=. z *. x
lemma mul_mul_div_mul_mul: forall x y z t. 0. <> z -> 0. <> t -> (x *. y) /. (z *. t) = (x /. z) *. (y /. t)
let lemma invord (a b: real) : unit
requires { 0. <. a <. b }
ensures { 0. <. 1./.b <. 1. /. a } =
assert { a *. inv a <=. b *. inv a };
assert { inv b <=. inv a };
()
use real.ExpLog
lemma log2_pos: 0. <. log 2.
lemma compatorderlog : forall x y :real. 0. <. x <. y -> log2 x <. log2 y
let lemma invlog (x :real)
requires { 0. <. x }
ensures { log (inv x) = -. log x } =
assert { log (x *. inv x) = log 1. }
lemma invlog2 : forall x :real. 0. <. x -> log2 (inv x) = -. log2 x
let lemma div_mult (a b y:int) : unit
requires { 0 < b <= y }
requires { 0 <= a }
ensures { ED.div (a*b) y <= a } =
assert { a * b = ED.div (a*b) y * y + ED.mod (a*b) y };
assert { a * b >= ED.div (a*b) y * y };
assert { ED.div (a*b) y >= 0 };
assert { ED.div (a*b) y * y >= ED.div (a*b) y * b };
assert { a * b >= ED.div (a*b) y * b };
let rec lemma mult_ord (a b c:int) : unit
requires { b > 0 }
requires { a >= 0 }
requires { c >= 0 }
requires { a * b >= c * b }
ensures { a >= c }
variant { c } =
if c = 0 then ()
else
mult_ord a b (c-1)
in
mult_ord a b (ED.div (a*b) y);
assert { a >= ED.div (a*b) y };
()
let lemma euclid_uniq (x y q : int) : unit
requires { y > 0 }
requires { q * y <= x < q * y + y }
ensures { ED.div x y = q } =
()
let lemma floor_div_is_ed_div (a b : int) : unit
requires { 0 < a }
requires { 0 < b }
ensures { ED.div a b = floor ((from_int a) /. (from_int b)) } =
let q = floor ((from_int a) /. (from_int b)) in
assert { q * b <= a
by from_int q <=. ((from_int a) /. (from_int b))
so from_int q *. (from_int b) <=. ((from_int a) /. (from_int b)) *. (from_int b) = from_int a };
assert { q * b + b > a
by from_int q *. (from_int b) +. (from_int b) >. (((from_int a) /. (from_int b)) -. 1.) *. from_int b +. from_int b = from_int a
so from_int (q * b + b) >. from_int a };
()
let lemma big_den_at_least_one_for_succ (a b : int) : unit
requires { 0 < a }
requires { 0 < b }
requires { ED.div a b < b }
ensures { ED.div a (b+1) = (if ED.mod a b < ED.div a b
then (ED.div a b) - 1
else (ED.div a b)) } =
if ED.mod a b < ED.div a b then
let q = (ED.div a b) - 1 in
assert { q * (b+1) = ED.div a b * b + ED.div a b - b - 1 = a - ED.mod a b + ED.div a b - b - 1 <= a };
assert { q * (b+1) + (b+1) = ED.div a b * b + ED.div a b = a - ED.mod a b + ED.div a b > a };
euclid_uniq a (b+1) q
else
let q = (ED.div a b) in
assert { q * (b+1) = ED.div a b * b + ED.div a b = a - ED.mod a b + ED.div a b <= a };
assert { q * (b+1) + (b+1) = ED.div a b * b + ED.div a b + b + 1 = a - ED.mod a b + ED.div a b + b + 1 > a };
euclid_uniq a (b+1) q
let lemma big_den_at_least_one_for_pred (a b : int) : unit
requires { 0 < a }
requires { 1 < b }
requires { ED.div a b < b - 1 }
ensures { ED.div a (b-1) = (if ED.mod a b + ED.div a b < b - 1
then (ED.div a b)
else (ED.div a b) + 1) } =
if ED.mod a b + ED.div a b < b - 1 then
let q = (ED.div a b) in
assert { q * (b-1) = ED.div a b * b - ED.div a b = a - ED.mod a b - ED.div a b <= a };
assert { q * (b-1) + (b-1) = ED.div a b * b - ED.div a b + b - 1 = a - ED.mod a b - ED.div a b + b - 1 > a };
euclid_uniq a (b-1) q
else
let q = (ED.div a b) + 1 in
assert { q * (b-1) = ED.div a b * b - ED.div a b + b - 1 = a - ED.mod a b - ED.div a b + b - 1 <= a };
assert { q * (b-1) + (b-1) = ED.div a b * b - ED.div a b + 2*b - 2 = a - ED.mod a b - ED.div a b + 2*b - 2 >= a };
euclid_uniq a (b-1) q
end
module Power
use Z
use mach.int.Int
use real.RealInfix
use real.FromInt
use real.Truncate
use RealArith
use int.EuclideanDivision as ED
use int.Power
use real.Square
use real.PowerReal
constant b : real = 4.
function _B (n:int) : real = pow b (from_int n)
let lemma _B_pos (n: int)
ensures { 0. <. _B n } = ()
let lemma _B_add (n:int) (m:int)
ensures { _B n *. _B m = _B (n+m) } =
()
let lemma _B_neg (n:int)
ensures { _B n *. _B (-n) = 1. } =
_B_add n (-n)
let lemma _B_sqrt (a:real) (n:int)
requires { 0. <=. a }
ensures { sqrt (a *. _B (-2*n)) = sqrt a *. _B (-n) }
=
assert { sqrt (a *. _B (-2*n)) = sqrt a *. sqrt (_B (-2*n)) };
assert { sqrt (_B (-2*n)) = pow (_B (-2*n)) 0.5 };
assert { sqrt (_B (-2*n)) = pow 4. (from_int (-2*n)*.0.5) };
assert { sqrt (_B (-2*n)) = pow 4. (from_int (-n)) };
()
let rec lemma power_2_4 (y:int)
requires { 0 <= y }
ensures { power 2 (2 * y) = power 4 y }
variant { y } =
if y = 0 then ()
else begin
power_2_4 (y-1);
()
end
let lemma power_int_is_power_on_int_pos (x:int) (y:int)
requires { 0 <= y }
ensures { from_int (power 4 y) = _B y }
=
assert { _B y = pow (from_int 4) (from_int y) }
let lemma power_int_is_power_on_int_neg (x:int) (y:int)
requires { y < 0 }
ensures { inv (from_int (power 4 (-y))) = _B y }
=
power_int_is_power_on_int_pos x (-y)
end
module CReal
use mach.int.Int
use real.RealInfix
use real.FromInt
use real.Truncate
use real.Abs
use RealArith
use Power
use Z
use int.Power
predicate framing (x:real) (p:int) (n:int) =
(from_int p -. 1.) *. (_B (-n)) <. x <. (from_int p +. 1.) *. (_B (-n))
let round_z_over_4 (z : int)
ensures { ((from_int z) -. 2.) *. (_B (-1)) <. from_int result <=. ((from_int z) +. 2.) *. (_B (-1)) }
=
let r = shift_right (z + 2) 2 in
assert { 4 = power 2 2 };
assert { _B 1 = from_int 4 };
assert { z + 2 = 4 * r + ED.mod (z + 2) 4};
assert { ED.mod (z + 2) 4 = - 4 * r + z + 2 };
assert { 0 <= - 4 * r + z + 2 < 4 };
assert { -4 < 4 * r - z - 2 <= 0 };
assert { z - 2 < 4 * r <= z + 2 };
assert { z - 2 < r * 4 <= z + 2 };
assert { (from_int z) -. 2. <. from_int r *. 4. <=. (from_int z) +. 2. };
r
let compute_round (n:int) (ghost z : real) (zp: int)
requires { (from_int zp -. 2.) *. _B (-(n+1)) <. z <=. (from_int zp +. 2.) *. _B (-(n+1)) }
ensures { framing z result n } =
let p = round_z_over_4 zp in
assert { _B (-1) = 0.25 };
assert { ((from_int p) -. 1.) *. _B (-n) <=. ((((from_int zp) +. 2.) *. (_B (-1)) ) -. 1. ) *. _B (-n) };
_B_add (-1) (-n);
_B_pos (-n);
assert { ((from_int p) -. 1.) *. _B (-n) <=. ((from_int zp) -. 2.) *. _B (-(n+1)) };
assert { ((from_int p) -. 1.) *. _B (-n) <. z };
assert { ((from_int p) +. 1.) *. _B (-n) >. ((((from_int zp) -. 2.) *. (_B (-1)) ) +. 1. ) *. _B (-n) };
assert { ((from_int p) +. 1.) *. _B (-n) >. ((from_int zp) +. 2.) *. _B (-(n+1)) };
assert { ((from_int p) +. 1.) *. _B (-n) >. z };
p
let compute_add (n: int) (ghost x : real) (xp : int) (ghost y : real) (yp : int)
requires { framing x xp (n+1) }
requires { framing y yp (n+1) }
ensures { framing (x+.y) result n } =
let ghost z = x +. y in
let zp = xp + yp in
assert { (from_int zp) = (from_int xp) +. (from_int yp) };
assert { ((from_int zp) -. 2.) *. _B (-(n+1)) = ((from_int xp) -. 1.) *. _B (-(n+1)) +.
((from_int yp) -. 1.) *. _B (-(n+1)) };
assert { ((from_int zp) +. 2.) *. _B (-(n+1)) = ((from_int xp) +. 1.) *. _B (-(n+1)) +.
((from_int yp) +. 1.) *. _B (-(n+1)) };
let p = compute_round n z zp in
p
let compute_neg (n: int) (ghost x : real) (xp : int)
requires { framing x xp n }
ensures { framing (-. x) result n } =
- xp
let compute_sub (n: int) (ghost x : real) (xp : int) (ghost y : real) (yp : int)
requires { framing x xp (n+1) }
requires { framing y yp (n+1) }
ensures { framing (x-.y) result n } =
compute_add n x xp (-. y) (compute_neg (n+1) y yp)
let compute_cst (n: int) (x : int) : int
ensures { framing (from_int x) result n } =
if n = 0 then begin
x
end else if n < 0 then begin
assert { (from_int (power 2 (2 * (-n)))) = _B (-n) };
let r = shift_right x (2*(-n)) in
assert { r = ED.div x (power 2 (2*(-n))) };
assert { x = r * (power 2 (2*(-n))) + ED.mod x (power 2 (2*(-n))) };
assert { x - r * (power 2 (2*(-n))) = ED.mod x (power 2 (2*(-n))) };
assert { 0 <= x - r * (power 2 (2*(-n))) < (power 2 (2*(-n))) };
assert { 0. <=. from_int x -. from_int r *. _B (-n) <. _B (-n) };
assert { from_int r *. _B (-n) <=. from_int x <. (from_int r +. 1.) *. _B (-n) };
r
end else begin
assert { from_int (power 2 (2 * n)) = _B n };
let r = shift_left x (2*n) in
assert { r = x * (power 2 (2 * n)) };
assert { from_int r = (from_int x) *. _B n };
assert { from_int r *. _B (-n) = (from_int x) };
r
end
use real.Square
type term =
| Cst int
| Add term term
| Neg term
| Sub term term
| Inv term
| Sqrt term
function interp (t:term) : real =
match t with
| Cst i -> from_int i
| Add t1 t2 -> (interp t1) +. (interp t2)
| Neg t1 -> -. (interp t1)
| Sub t1 t2 -> (interp t1) -. (interp t2)
| Inv t -> inv (interp t)
| Sqrt t -> sqrt (interp t)
end
predicate wf_term (t:term) =
match t with
| Cst _ -> true
| Neg t1 -> wf_term t1
| Add t1 t2 | Sub t1 t2 -> wf_term t1 /\ wf_term t2
| Inv t1 -> wf_term t1 /\ interp t1 <> 0.
| Sqrt t1 -> wf_term t1 /\ 0. <=. interp t1
end
use int.EuclideanDivision as ED
use real.ExpLog
let inv_simple_simple (ghost x:real) (p:int) (n:int)
requires { framing x p (n+1) }
requires { 0 <= n }
requires { 1. <=. x }
ensures { framing (inv x) result n } =
let k = n + 1 in
let ghost p' = from_int p in
assert { 4 = power 2 (2*1) <= power 2 (2*k) <= p
by x <. ( p' +. 1. ) *. _B (- k)
so 1. <. ( p' +. 1. ) *. _B (- k)
so _B k <. ( p' +. 1. )
so _B k -. 1. <. p'
(* so from_int 1 = 1. *)
so from_int (power 2 (2*k)) -. from_int 1 <. from_int p
so from_int (power 2 (2*k) - 1) <. from_int p
so power 2 (2*k) - 1 < p
};
let d,r = ediv_mod (power2 (2*(n+k))) p in
let ghost b ()
ensures { 1. /. (_B (-k)) = _B (n+k) *. _B (-n) }
=
_B_add n (-n);
_B_add (n+k) (-n);
()
in
b();
assert { (power 2 (2*(n+k))) = power 2 (2*n) * power 2 (2*k) };
assert { 0 <= d <= power 2 (2*n) };
assert { 0. <. (p' -. 1.) *. _B (-k) <. x <. (p' +. 1.) *. _B (-k) };
invord ((p' -. 1.) *. _B (-k)) x;
invord x ((p' +. 1.) *. _B (-k));
assert { from_int (floor (_B (n + k) /. (p' +. 1.))) *. _B (-n) <. 1. /. x <. from_int (floor (_B (n + k) /. (p' -. 1.)) + 1) *. _B (-n)
by 1. /. ((p' +. 1.) *. _B (-k)) <. 1. /. x <. 1. /. ((p' -. 1.) *. _B (-k))
so (1. *. 1.) /. ((p' +. 1.) *. _B (-k)) <. 1. /. x <. (1. *. 1.) /. ((p' -. 1.) *. _B (-k))
so (1. /. (p' +. 1.)) *. (1. /. _B (-k)) <. 1. /. x <. (1. /. (p' -. 1.)) *. (1. /. _B (-k))
so (1. /. (p' +. 1.)) *. _B (n + k) *. _B (-n) <. 1. /. x <. (1. /. (p' -. 1.)) *. _B (n + k) *. _B (-n)
so (_B (n + k) /. (p' +. 1.)) *. _B (-n) <. 1. /. x <. (_B (n + k) /. (p' -. 1.)) *. _B (-n)
so from_int (floor (_B (n + k) /. (p' +. 1.))) *. _B (-n) <. 1. /. x <. from_int (ceil (_B (n + k) /. (p' -. 1.))) *. _B (-n)
};
let ghost num = (power 2 (2*(n+k))) in
floor_div_is_ed_div num (p + 1);
floor_div_is_ed_div num (p - 1);
power_int_is_power_on_int_pos 4 (n+k);
power_2_4 (n+k);
assert { from_int (ED.div num (p + 1)) *. _B (-n) <. 1. /. x <. from_int (ED.div num (p - 1) + 1) *. _B (-n) };
let d' = if 2*r <= p then d else d+1 in
big_den_at_least_one_for_succ num p;
big_den_at_least_one_for_pred num p;
d'
let lemma smaller (x:real) (n:int)
requires { 0. <. abs x <. 2. *. _B (-n) }
requires { 0 <= n }
ensures { floor (log2 (abs x)) < 1 - (n*2) } =
assert { log2 2. = 1. };
assert { log2 (abs x) <. log2 (2. *. _B (-n)) };
assert { log2 (abs x) <. log2 2. +. log2 (_B (-n)) };
assert { log2 (abs x) <. 1. +. log2 (exp ((from_int (-n)) *. log 4.)) };
assert { log 4. = 2. *. log 2. };
assert { log2 (exp ((from_int (-n)) *. log 4.)) = ((from_int (-n)) *. log 4.) /. log 2. };
assert { log2 (abs x) <. 1. -. 2. *. from_int (n) };
assert { floor (log2 (abs x)) < 1 - (n*2) }
use int.MinMax
let function isqr (n:int) : int = n*n
let lemma sqr_is_isqr (n:int)
ensures { sqr (from_int n) = from_int (isqr n) } =
()
let lemma sqrt_pred (n:int)
requires { 1 <= n }
ensures { isqrt n - 1 <= isqrt (n - 1) } =
assert { isqrt (n-1) = floor (sqrt (from_int (n-1))) };
let c = isqrt (n - 1) + 1 in
assert { from_int (isqrt (n - 1)) <=. sqrt (from_int (n-1)) <. from_int c };
assert { sqr (sqrt (from_int (n-1))) <. sqr (from_int c) };
assert { sqr (sqrt (from_int (n-1))) <. sqr (from_int c) };
assert { from_int (n-1) <. from_int (isqr c) };
assert { (n-1) < (isqr c) };
assert { (n-1) < n <= (isqr c) };
assert { from_int n <=. from_int (isqr c) };
assert { from_int n <=. sqr (from_int c) };
assert { sqrt (from_int n) <=. sqrt (sqr (from_int c)) };
assert { from_int (isqrt n) <=. from_int c };
()
let lemma sqrt_succ (n:int)
requires { 0 <= n }
ensures { ceil (sqrt (from_int (n + 1))) - 1 <= isqrt n } =
let c = ceil (sqrt (from_int (n + 1))) - 1 in
assert { from_int (c) <. sqrt (from_int (n+1)) };
assert { sqr (from_int c) <. from_int (n+1) };
assert { isqr c < n+1 };
assert { isqr c <= n < n+1 };
assert { sqr (from_int c) <=. from_int n };
assert { from_int c <=. sqrt (from_int (n)) };
assert { from_int c <=. from_int (floor (sqrt (from_int (n)))) };
()
let compute_sqrt (n: int) (ghost x : real) (xp : int)
requires { 0. <=. x }
requires { framing x xp (2*n) }
ensures { framing (sqrt x) result n } =
if xp <= 0 then begin
assert { 0. <=. x <. _B (-2*n) };
_B_sqrt 1. n;
assert { 0. <=. sqrt x <. sqrt (_B (-2*n)) = _B (-n) };
0
end
else
let r = isqrt xp in
let ghost xp' = from_int xp in
assert { sqrt ((xp' -. 1.) *. _B (-2*n)) <. sqrt x <. sqrt ((xp' +. 1.) *. _B (-2*n)) };
assert { sqrt (xp' -. 1.) *. _B (-n) <. sqrt x <. sqrt (xp' +. 1.) *. _B (-n) };
assert { from_int (floor (sqrt (xp' -. 1.))) *. _B (-n) <. sqrt x <. from_int (ceil (sqrt (xp' +. 1.))) *. _B (-n) };
sqrt_pred xp;
sqrt_succ xp;
assert { from_int (floor (sqrt (from_int (xp - 1)))) *. _B (-n) <. sqrt x <. from_int (ceil (sqrt (from_int (xp + 1)))) *. _B (-n) };
r
let inv_simple (ghost x) p m n
requires { 0 <= m }
requires { 0 <= n }
requires { _B (-m) <. x }
requires { framing x p (n+1+2*m) }
ensures { framing (inv x) result n }
=
assert { 1. <=. x *. _B m
by _B (-m) *. _B m <. x *. _B m };
assert { _B (-(n+1+2*m)) = _B (-(n+1+m)) *. _B (-m) };
assert { _B (-(n+1+m)) *. _B (-m) *. _B m = _B (-(n+1+m)) };
assert { from_int (p - 1) *. _B (-(n+1+2*m)) <. x <. from_int (p + 1) *. _B (-(n+1+2*m)) };
assert { from_int (p - 1) *. _B (-(n+1+m)) *. _B (-m) <. x <. from_int (p + 1) *. _B (-(n+1+m)) *. _B (-m) };
assert { from_int (p - 1) *. _B (-(n+1+m)) *. _B (-m) *. _B m <. x *. _B m <. from_int (p + 1) *. _B (-(n+1+m)) *. _B (-m) *. _B m};
assert { from_int (p - 1) *. _B (-(n+1+m)) <. x *. _B m <. from_int (p + 1) *. _B (-(n+1+m)) };
let r = inv_simple_simple (x *. _B m) p (n+m) in
assert { from_int (r - 1) *. _B ((-n)+(-m)) = from_int (r - 1) *. (_B (-n) *. _B (-m)) };
assert { inv (x *. _B m) = inv x *. inv (_B m)};
assert { from_int (r + 1) *. _B ((-n)+(-m)) = from_int (r + 1) *. (_B (-n) *. _B(-m)) };
assert { from_int (r - 1) *. (_B (-n) *. _B (-m)) *. _B m <. inv x *. inv (_B m) *. _B m <. from_int (r + 1) *. (_B (-n) *. _B(-m)) *. _B m };
assert { from_int (r - 1) *. _B (-n) *. (_B (-m) *. _B m) <. inv x *. (inv (_B m) *. _B m) <. from_int (r + 1) *. _B (-n) *. (_B(-m) *. _B m) };
_B_add (-m) m;
assert { (_B (-m) *. _B m) = 1. };
r
let rec compute (t:term) (n:int) : int
requires { wf_term t }
requires { 0 <= n }
ensures { framing (interp t) result n }
variant { t, 1 - floor (log2 (abs (interp t))) - n }
=
match t with
| Cst i -> compute_cst n i
| Add t1 t2 -> compute_add n (interp t1) (compute t1 (n+1)) (interp t2) (compute t2 (n+1))
| Neg t1 -> compute_neg n (interp t1) (compute t1 n)
| Sub t1 t2 -> compute_sub n (interp t1) (compute t1 (n+1)) (interp t2) (compute t2 (n+1))
| Sqrt t1 -> compute_sqrt n (interp t1) (compute t1 (2*n))
| Inv t ->
let m,sgn = msd t 0 (compute t 0) in
let ghost x = interp t in
let p = compute t (n+1+2*m) in
if sgn
then inv_simple x p m n
else begin
let r = inv_simple (-. x) (-p) m n in
assert { inv (-. x) = -. inv x };
assert { from_int (r - 1) *. _B (-n) <. -. inv x <. from_int (r + 1) *. _B (-n) };
assert { -. (from_int (r + 1) *. _B (-n)) <. -. (-. inv x) <. -. (from_int (r - 1) *. _B (-n)) };
assert { from_int (- r - 1) *. _B (-n) <. inv x <. from_int (- r + 1) *. _B (-n) };
- r
end
end
with msd (t:term) (n:int) (c:int) : (int, bool)
requires { 0 <= n }
requires { wf_term t }
requires { interp t <> 0. }
requires { framing (interp t) c n }
ensures { let m,sgn = result in
0 <= m /\
if sgn then _B (-m) <. interp t else interp t <. -. _B (-m) }
variant { t, 1 - floor (log2 (abs (interp t))) - n } =
assert { from_int 0 = 0. };
if c = 0 || c = 1 || c = -1 then begin
smaller (interp t) n;
let c = compute t (n+1) in
msd t (n+1) c
end
else begin
assert { from_int 1 = 1. };
if 1 < c then begin
assert { 1 <= c - 1 };
assert { 0. <=. 1. <=. from_int c -. 1. };
assert { _B (-n) <=. (from_int c -. 1.) *. _B (-n) <. interp t };
n, true
end
else begin
assert { c + 1 <= -1 };
assert { (from_int c +. 1.) <=. -1. <=. 0. };
assert { interp t <. (from_int c +. 1.) *. _B (-n) <=. -. 1. *. _B (-n) };
n, false
end
end
let exec0 () : int =
compute (Cst 2) 4
let exec1 () : int =
compute (Add (Cst 2) (Cst 4)) 4
let exec2 () : int =
compute (Inv (Cst 2)) 4
let exec3 () : int =
compute (Sqrt (Cst 2)) 4
end
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Z3" version="4.4.1" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="2.0.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.6.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file proved="true">
<path name=".."/><path name="creal.mlw"/>
<theory name="Z" proved="true">
<goal name="VC power2" expl="VC for power2" proved="true">
<proof prover="4"><result status="valid" time="0.07" steps="7202"/></proof>
</goal>
<goal name="VC shift_left" expl="VC for shift_left" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="5541"/></proof>
</goal>
<goal name="VC euclid_uniq" expl="VC for euclid_uniq" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="5852"/></proof>
</goal>
<goal name="VC ediv_mod" expl="VC for ediv_mod" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC ediv_mod.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="6100"/></proof>
</goal>
<goal name="VC ediv_mod.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="6112"/></proof>
</goal>
<goal name="VC ediv_mod.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6123"/></proof>
</goal>
<goal name="VC ediv_mod.3" expl="postcondition" proved="true">
<proof prover="6" timelimit="5"><result status="valid" time="0.02" steps="19157"/></proof>
</goal>
<goal name="VC ediv_mod.4" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13185"/></proof>
</goal>
<goal name="VC ediv_mod.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6030"/></proof>
</goal>
<goal name="VC ediv_mod.6" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6034"/></proof>
</goal>
<goal name="VC ediv_mod.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6040"/></proof>
</goal>
<goal name="VC ediv_mod.8" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="6230"/></proof>
</goal>
<goal name="VC ediv_mod.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6109"/></proof>
</goal>
<goal name="VC ediv_mod.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.15" steps="12373"/></proof>
</goal>
<goal name="VC ediv_mod.11" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6113"/></proof>
</goal>
<goal name="VC ediv_mod.12" expl="precondition" proved="true">
<proof prover="6" timelimit="5"><result status="valid" time="3.37" steps="27202884"/></proof>
</goal>
<goal name="VC ediv_mod.13" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
</transf>
</goal>
<goal name="VC shift_right" expl="VC for shift_right" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6872"/></proof>
</goal>
<goal name="VC isqrt" expl="VC for isqrt" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC isqrt.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC isqrt.0.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC isqrt.0.1" expl="VC for isqrt" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="214"/></proof>
</goal>
</transf>
</goal>
<goal name="VC isqrt.1" expl="assertion" proved="true">
<proof prover="6"><result status="valid" time="0.61" steps="2093869"/></proof>
</goal>
<goal name="VC isqrt.2" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="6948"/></proof>
</goal>
<goal name="VC isqrt.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6889"/></proof>
</goal>
<goal name="VC isqrt.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6941"/></proof>
</goal>
<goal name="VC isqrt.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="7343"/></proof>
</goal>
<goal name="VC isqrt.6" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC isqrt.6.0" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="7374"/></proof>
</goal>
<goal name="VC isqrt.6.1" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6739"/></proof>
</goal>
</transf>
</goal>
<goal name="VC isqrt.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6573"/></proof>
</goal>
<goal name="VC isqrt.8" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="7046"/></proof>
</goal>
<goal name="VC isqrt.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="7076"/></proof>
</goal>
<goal name="VC isqrt.10" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="6564"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="RealArith" proved="true">
<goal name="mul_str_ordr" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="mul_str_ordl" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="7312"/></proof>
</goal>
<goal name="mul_ordr" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="7444"/></proof>
</goal>
<goal name="mul_ordl" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="7576"/></proof>
</goal>
<goal name="mul_ord_zero" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="mul_mul_div_mul_mul" proved="true">
<proof prover="3"><result status="valid" time="0.75" steps="988"/></proof>
</goal>
<goal name="VC invord" expl="VC for invord" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC invord.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.18"/></proof>
</goal>
<goal name="VC invord.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="15072"/></proof>
</goal>
<goal name="VC invord.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
</transf>
</goal>
<goal name="log2_pos" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="9612"/></proof>
</goal>
<goal name="compatorderlog" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC invlog" expl="VC for invlog" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="invlog2" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="21"/></proof>
</goal>
<goal name="VC div_mult" expl="VC for div_mult" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC div_mult.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC div_mult.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="12197"/></proof>
</goal>
<goal name="VC div_mult.2" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="VC div_mult.3" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="VC div_mult.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="12367"/></proof>
</goal>
<goal name="VC div_mult.5" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="11698"/></proof>
</goal>
<goal name="VC div_mult.6" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="11672"/></proof>
</goal>
<goal name="VC div_mult.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="11679"/></proof>
</goal>
<goal name="VC div_mult.8" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="12706"/></proof>
</goal>
<goal name="VC div_mult.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="12763"/></proof>
</goal>
<goal name="VC div_mult.10" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="11805"/></proof>
</goal>
<goal name="VC div_mult.11" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="19"/></proof>
</goal>
<goal name="VC div_mult.12" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="12026"/></proof>
</goal>
<goal name="VC div_mult.13" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="11737"/></proof>
</goal>
<goal name="VC div_mult.14" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="11744"/></proof>
</goal>
<goal name="VC div_mult.15" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="11751"/></proof>
</goal>
<goal name="VC div_mult.16" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="11758"/></proof>
</goal>
<goal name="VC div_mult.17" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="11749"/></proof>
</goal>
<goal name="VC div_mult.18" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="11756"/></proof>
</goal>
</transf>
</goal>
<goal name="VC euclid_uniq" expl="VC for euclid_uniq" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="9450"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div" expl="VC for floor_div_is_ed_div" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC floor_div_is_ed_div.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="11810"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.1" expl="assertion" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC floor_div_is_ed_div.1.0" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="11885"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.1.1" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.1.2" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.1.3" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="3"><result status="valid" time="0.07" steps="108"/></proof>
</goal>
</transf>
</goal>
<goal name="VC floor_div_is_ed_div.2" expl="assertion" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC floor_div_is_ed_div.2.0" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="3"><result status="valid" time="0.62" steps="439"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.2.1" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.2.2" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC floor_div_is_ed_div.2.3" expl="VC for floor_div_is_ed_div" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="37"/></proof>
</goal>
</transf>
</goal>
<goal name="VC floor_div_is_ed_div.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
</transf>
</goal>
<goal name="VC big_den_at_least_one_for_succ" expl="VC for big_den_at_least_one_for_succ" proved="true">
<proof prover="3" timelimit="10"><result status="valid" time="2.36" steps="917"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred" expl="VC for big_den_at_least_one_for_pred" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC big_den_at_least_one_for_pred.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="12434"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="12434"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="12540"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.3" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="13298"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="12576"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.6" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="13463"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="12540"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.8" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.9" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="13373"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="12620"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.11" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13554"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.12" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="12731"/></proof>
</goal>
<goal name="VC big_den_at_least_one_for_pred.13" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="12794"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Power" proved="true">
<goal name="VC _B_pos" expl="VC for _B_pos" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC _B_add" expl="VC for _B_add" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC _B_add.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
</transf>
</goal>
<goal name="VC _B_neg" expl="VC for _B_neg" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="58"/></proof>
</goal>
<goal name="VC _B_sqrt" expl="VC for _B_sqrt" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC _B_sqrt.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC _B_sqrt.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="16875"/></proof>
</goal>
<goal name="VC _B_sqrt.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="22161"/></proof>
</goal>
<goal name="VC _B_sqrt.3" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="13634"/></proof>
</goal>
<goal name="VC _B_sqrt.4" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
</transf>
</goal>
<goal name="VC power_2_4" expl="VC for power_2_4" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC power_2_4.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13675"/></proof>
</goal>
<goal name="VC power_2_4.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="14034"/></proof>
</goal>
<goal name="VC power_2_4.2" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="14874"/></proof>
</goal>
<goal name="VC power_2_4.3" expl="postcondition" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
</transf>
</goal>
<goal name="VC power_int_is_power_on_int_pos" expl="VC for power_int_is_power_on_int_pos" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC power_int_is_power_on_int_pos.0" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14881"/></proof>
</goal>
<goal name="VC power_int_is_power_on_int_pos.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
</transf>
</goal>
<goal name="VC power_int_is_power_on_int_neg" expl="VC for power_int_is_power_on_int_neg" proved="true">
<proof prover="3"><result status="valid" time="0.05" steps="69"/></proof>
</goal>
</theory>
<theory name="CReal" proved="true">
<goal name="VC round_z_over_4" expl="VC for round_z_over_4" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC round_z_over_4.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="14343"/></proof>
</goal>
<goal name="VC round_z_over_4.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="20604"/></proof>
</goal>
<goal name="VC round_z_over_4.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="17768"/></proof>
</goal>
<goal name="VC round_z_over_4.3" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="15300"/></proof>
</goal>
<goal name="VC round_z_over_4.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="14521"/></proof>
</goal>
<goal name="VC round_z_over_4.5" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="15378"/></proof>
</goal>
<goal name="VC round_z_over_4.6" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="15446"/></proof>
</goal>
<goal name="VC round_z_over_4.7" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="15483"/></proof>
</goal>
<goal name="VC round_z_over_4.8" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="15520"/></proof>
</goal>
<goal name="VC round_z_over_4.9" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC round_z_over_4.10" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC round_z_over_4.10.0" expl="VC for round_z_over_4" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="0.08" steps="89"/></proof>
</goal>
<goal name="VC round_z_over_4.10.1" expl="VC for round_z_over_4" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="0.07" steps="86"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC compute_round" expl="VC for compute_round" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute_round.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.43" steps="287"/></proof>
</goal>
<goal name="VC compute_round.1" expl="assertion" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="VC compute_round.2" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="14"/></proof>
</goal>
<goal name="VC compute_round.3" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.10" steps="15833"/></proof>
</goal>
<goal name="VC compute_round.4" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC compute_round.5" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="VC compute_round.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC compute_round.7" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.13" steps="19357"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compute_add" expl="VC for compute_add" proved="true">
<proof prover="3"><result status="valid" time="0.09" steps="48"/></proof>
</goal>
<goal name="VC compute_neg" expl="VC for compute_neg" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="38"/></proof>
</goal>
<goal name="VC compute_sub" expl="VC for compute_sub" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="12224"/></proof>
</goal>
<goal name="VC compute_cst" expl="VC for compute_cst" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute_cst.0" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.16" steps="21973"/></proof>
</goal>
<goal name="VC compute_cst.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="14899"/></proof>
</goal>
<goal name="VC compute_cst.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="14439"/></proof>
</goal>
<goal name="VC compute_cst.3" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC compute_cst.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="14538"/></proof>
</goal>
<goal name="VC compute_cst.5" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="18664"/></proof>
</goal>
<goal name="VC compute_cst.6" expl="assertion" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute_cst.6.0" expl="VC for compute_cst" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="75"/></proof>
</goal>
<goal name="VC compute_cst.6.1" expl="VC for compute_cst" proved="true">
<proof prover="3"><result status="valid" time="0.17" steps="82"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compute_cst.7" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="15687"/></proof>
</goal>
<goal name="VC compute_cst.8" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.17" steps="21953"/></proof>
</goal>
<goal name="VC compute_cst.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="14431"/></proof>
</goal>
<goal name="VC compute_cst.10" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="14428"/></proof>
</goal>
<goal name="VC compute_cst.11" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC compute_cst.12" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC compute_cst.13" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="50"/></proof>
</goal>
<goal name="VC compute_cst.14" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="20"/></proof>
</goal>
<goal name="VC compute_cst.15" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="53"/></proof>
</goal>
</transf>
</goal>
<goal name="VC inv_simple_simple" expl="VC for inv_simple_simple" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC inv_simple_simple.0" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC inv_simple_simple.0.0" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="17077"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.1" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14830"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.2" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="48"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.3" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13797"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.4" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="22632"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.5" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="13873"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.6" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13890"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.7" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="22461"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.8" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="17551"/></proof>
</goal>
<goal name="VC inv_simple_simple.0.9" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13901"/></proof>
</goal>
</transf>
</goal>
<goal name="VC inv_simple_simple.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="13804"/></proof>
</goal>
<goal name="VC inv_simple_simple.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="14884"/></proof>
</goal>
<goal name="VC inv_simple_simple.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="161"/></proof>
</goal>
<goal name="VC inv_simple_simple.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.12" steps="26934"/></proof>
</goal>
<goal name="VC inv_simple_simple.5" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.22" steps="167"/></proof>
</goal>
<goal name="VC inv_simple_simple.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="41"/></proof>
</goal>
<goal name="VC inv_simple_simple.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14098"/></proof>
</goal>
<goal name="VC inv_simple_simple.8" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="15994"/></proof>
</goal>
<goal name="VC inv_simple_simple.9" expl="assertion" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC inv_simple_simple.9.0" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14258"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14258"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.2" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14305"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.3" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14305"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.4" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.5" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="33"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.6" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="29"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.7" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="29"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.8" expl="VC for inv_simple_simple" proved="true">
<proof prover="6"><result status="valid" time="0.05" steps="132854"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.9" expl="VC for inv_simple_simple" proved="true">
<proof prover="6"><result status="valid" time="0.05" steps="133054"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.10" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.28" steps="122"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.11" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.32" steps="122"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.12" expl="VC for inv_simple_simple" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14625"/></proof>
</goal>
<goal name="VC inv_simple_simple.9.13" expl="VC for inv_simple_simple" proved="true">
<proof prover="3"><result status="valid" time="0.44" steps="142"/></proof>
</goal>
</transf>
</goal>
<goal name="VC inv_simple_simple.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.07" steps="20210"/></proof>
</goal>
<goal name="VC inv_simple_simple.11" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="16714"/></proof>
</goal>
<goal name="VC inv_simple_simple.12" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="20595"/></proof>
</goal>
<goal name="VC inv_simple_simple.13" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="17096"/></proof>
</goal>
<goal name="VC inv_simple_simple.14" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14483"/></proof>
</goal>
<goal name="VC inv_simple_simple.15" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="14503"/></proof>
</goal>
<goal name="VC inv_simple_simple.16" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.92" steps="221"/></proof>
</goal>
<goal name="VC inv_simple_simple.17" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="21805"/></proof>
</goal>
<goal name="VC inv_simple_simple.18" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="17997"/></proof>
</goal>
<goal name="VC inv_simple_simple.19" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="21961"/></proof>
</goal>
<goal name="VC inv_simple_simple.20" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="22005"/></proof>
</goal>
<goal name="VC inv_simple_simple.21" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="18147"/></proof>
</goal>
<goal name="VC inv_simple_simple.22" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="22116"/></proof>
</goal>
<goal name="VC inv_simple_simple.23" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC inv_simple_simple.23.0" expl="postcondition" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.16" steps="432"/></proof>
</goal>
<goal name="VC inv_simple_simple.23.1" expl="postcondition" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="1.20" steps="441"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC smaller" expl="VC for smaller" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC smaller.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC smaller.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.12" steps="33216"/></proof>
</goal>
<goal name="VC smaller.2" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.05" steps="109"/></proof>
</goal>
<goal name="VC smaller.3" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.10" steps="27061"/></proof>
</goal>
<goal name="VC smaller.4" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.09" steps="21846"/></proof>
</goal>
<goal name="VC smaller.5" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="20"/></proof>
</goal>
<goal name="VC smaller.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="77"/></proof>
</goal>
<goal name="VC smaller.7" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC smaller.8" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="16653"/></proof>
</goal>
</transf>
</goal>
<goal name="VC sqr_is_isqr" expl="VC for sqr_is_isqr" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="27"/></proof>
</goal>
<goal name="VC sqrt_pred" expl="VC for sqrt_pred" proved="true">
<proof prover="3"><result status="valid" time="1.69" steps="963"/></proof>
</goal>
<goal name="VC sqrt_succ" expl="VC for sqrt_succ" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC sqrt_succ.0" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="17439"/></proof>
</goal>
<goal name="VC sqrt_succ.1" expl="assertion" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="0.33" steps="432"/></proof>
</goal>
<goal name="VC sqrt_succ.2" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC sqrt_succ.3" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="17460"/></proof>
</goal>
<goal name="VC sqrt_succ.4" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC sqrt_succ.5" expl="assertion" proved="true">
<proof prover="3" timelimit="10" memlimit="4000"><result status="valid" time="6.43" steps="1848"/></proof>
</goal>
<goal name="VC sqrt_succ.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.08" steps="99"/></proof>
</goal>
<goal name="VC sqrt_succ.7" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compute_sqrt" expl="VC for compute_sqrt" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute_sqrt.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="47"/></proof>
</goal>
<goal name="VC compute_sqrt.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="17598"/></proof>
</goal>
<goal name="VC compute_sqrt.2" expl="assertion" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute_sqrt.2.0" expl="VC for compute_sqrt" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="22281"/></proof>
</goal>
<goal name="VC compute_sqrt.2.1" expl="VC for compute_sqrt" proved="true">
<proof prover="4"><result status="valid" time="0.17" steps="44569"/></proof>
</goal>
<goal name="VC compute_sqrt.2.2" expl="VC for compute_sqrt" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="52"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compute_sqrt.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="18266"/></proof>
</goal>
<goal name="VC compute_sqrt.4" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.17" steps="137"/></proof>
</goal>
<goal name="VC compute_sqrt.5" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="124"/></proof>
</goal>
<goal name="VC compute_sqrt.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.24" steps="189"/></proof>
</goal>
<goal name="VC compute_sqrt.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="17816"/></proof>
</goal>
<goal name="VC compute_sqrt.8" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="19379"/></proof>
</goal>
<goal name="VC compute_sqrt.9" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC compute_sqrt.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03" steps="18"/></proof>
</goal>
<goal name="VC compute_sqrt.11" expl="postcondition" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC compute_sqrt.11.0" expl="postcondition" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC compute_sqrt.11.0.0" expl="postcondition" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute_sqrt.11.0.0.0" expl="VC for compute_sqrt" proved="true">
<proof prover="3"><result status="valid" time="0.34" steps="275"/></proof>
</goal>
<goal name="VC compute_sqrt.11.0.0.1" expl="VC for compute_sqrt" proved="true">
<proof prover="3"><result status="valid" time="0.31" steps="207"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC inv_simple" expl="VC for inv_simple" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC inv_simple.0" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.83" steps="648"/></proof>
</goal>
<goal name="VC inv_simple.1" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.19" steps="27764"/></proof>
</goal>
<goal name="VC inv_simple.2" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="VC inv_simple.3" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC inv_simple.4" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC inv_simple.5" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="103"/></proof>
</goal>
<goal name="VC inv_simple.6" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="VC inv_simple.7" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC inv_simple.8" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="19262"/></proof>
</goal>
<goal name="VC inv_simple.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="17937"/></proof>
</goal>
<goal name="VC inv_simple.10" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="31"/></proof>
</goal>
<goal name="VC inv_simple.11" expl="assertion" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="0.04" steps="36"/></proof>
</goal>
<goal name="VC inv_simple.12" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="62"/></proof>
</goal>
<goal name="VC inv_simple.13" expl="assertion" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC inv_simple.13.0" expl="VC for inv_simple" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC inv_simple.13.0.0" expl="VC for inv_simple" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC inv_simple.13.0.0.0" expl="VC for inv_simple" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.52" steps="112"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC inv_simple.13.1" expl="VC for inv_simple" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC inv_simple.13.1.0" expl="VC for inv_simple" proved="true">
<transf name="inline_goal" proved="true" >
<goal name="VC inv_simple.13.1.0.0" expl="VC for inv_simple" proved="true">
<proof prover="3" timelimit="5"><result status="valid" time="0.52" steps="112"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC inv_simple.14" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="20331"/></proof>
</goal>
<goal name="VC inv_simple.15" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.07" steps="24948"/></proof>
</goal>
<goal name="VC inv_simple.16" expl="postcondition" proved="true">
<proof prover="3" timelimit="5" memlimit="2000"><result status="valid" time="2.60" steps="243"/></proof>
</goal>
</transf>
</goal>
<goal name="VC compute" expl="VC for compute" proved="true">
<transf name="split_all_full" proved="true" >
<goal name="VC compute.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="24354"/></proof>
</goal>
<goal name="VC compute.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="19584"/></proof>
</goal>
<goal name="VC compute.2" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="18404"/></proof>
</goal>
<goal name="VC compute.3" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.08" steps="24709"/></proof>
</goal>
<goal name="VC compute.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="19718"/></proof>
</goal>
<goal name="VC compute.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="18510"/></proof>
</goal>
<goal name="VC compute.6" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="17631"/></proof>
</goal>
<goal name="VC compute.7" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="17674"/></proof>
</goal>
<goal name="VC compute.8" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.07" steps="24312"/></proof>
</goal>
<goal name="VC compute.9" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="19564"/></proof>
</goal>
<goal name="VC compute.10" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03" steps="17597"/></proof>
</goal>
<goal name="VC compute.11" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.05" steps="17586"/></proof>
</goal>
<goal name="VC compute.12" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.17" steps="24391"/></proof>
</goal>
<goal name="VC compute.13" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="19584"/></proof>
</goal>
<goal name="VC compute.14" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="18404"/></proof>
</goal>
<goal name="VC compute.15" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.06" steps="24746"/></proof>
</goal>
<goal name="VC compute.16" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.07" steps="19718"/></proof>
</goal>
<goal name="VC compute.17" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="18510"/></proof>
</goal>
<goal name="VC compute.18" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="17631"/></proof>
</goal>
<goal name="VC compute.19" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="17674"/></proof>