Commit b8edf02b authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft

Finish Toom22 proof

parent 1683cd5d
......@@ -8,8 +8,9 @@ module Toom
use import mach.int.UInt64GMP as Limb
use import int.Int
use import int.Power
use import valuation.Valuation
use import mp2.N
use import int.EuclideanDivision
use import int.ComputerDivision
let constant toom22_threshold : int32 = 20
......@@ -280,7 +281,8 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
+ hv0 + m * lvinf - m * cy2 - m * m * !cy
\/ !cy = radix - 1
/\ value v0n (n+n) = a1 * b1 + a0 * b0 - (a0 - a1)*(b0 - b1)
+ hv0 + m * lvinf - m * cy2 + m * m }
+ hv0 + m * lvinf - m * cy2 + m * m
/\ !cy at AddSub = 0 }
assert { !vm1_neg /\ value scratch (n+n) = - (a0-a1)*(b0-b1)
\/ not !vm1_neg /\ value scratch (n+n) = (a0-a1)*(b0-b1)
by value scratch (n+n) = asm1_abs * bsm1_abs
......@@ -317,7 +319,7 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
\/ !cy = radix - 1 /\ !cy at AddSub = 0 /\ b = 1
by [@case_split]
((!cy at AddSub = 0 /\ b = 1
so !cy = mod (-1) radix = radix - 1)
so !cy = EuclideanDivision.mod (-1) radix = radix - 1)
\/
(1 <= !cy at AddSub \/ b = 0
so 0 <= !cy at AddSub - b < radix
......@@ -358,7 +360,7 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
assert { value r n = value rj n = lv0 };
value_concat r n (Int32.( *) 3 n);
value_sub_frame (pelts r) (pelts v0nj) (offset r + p2i n)
(offset r + 3 * p2i n);
(offset r + 3 * p2i n);
assert { value r (3*n) = value r n + m * value (v0n at Join) (n+n)
by offset v0nj = offset r + n
so offset v0nj + (n + n) = offset r + 3 * n
......@@ -461,16 +463,112 @@ let rec toom22_mul (r x y scratch: ptr limb) (sx sy:int32) (ghost k: int) : unit
begin ensures { value r (sx + sy) + m * m * cy2 < m * m * m * m' }
ensures { value x sx * value y sy < m * m * m * m' }
assert { power radix (s+t) = m * m' };
assert { !cy = radix - 1 -> hvinf <= m' - 2
(* TODO v0n (n+n) < m * m -> lvinf=0 (by value v0n (n+n) < m*m)
-> a1*b1=m*hvinf
-> a1=b^k*a1', b1= b^l*b1', k+l = n
-> a1*b1 < m * (m' - 1) *) };
value_sub_upper_bound (pelts r) (offset r) (offset r + int32'int n);
value_sub_upper_bound (pelts v0nj) (offset v0nj)
(offset v0nj + int32'int n + int32'int n);
value_sub_upper_bound (pelts x) (offset x) (offset x + int32'int sx);
value_sub_upper_bound (pelts y) (offset y) (offset y + int32'int sy);
assert { !cy = radix - 1 -> hvinf <= m' - 2
by value v0nj (n+n) < power radix (n+n) = m * m
so value v0nj (n+n) = a1 * b1 + a0 * b0 - (a0 - a1)*(b0 - b1)
+ hv0 + m * lvinf - m * cy2 + m * m
= a0 * b1 + a1 * b0 + hv0 + m * lvinf - m * cy2 + m * m
so (0 <= a0 * b1 by 0 <= a0 /\ 0 <= b1)
so (0 <= a1 * b0 by 0 <= a1 /\ 0 <= b0)
so hv0 >= 0
so value v0nj (n+n) >= m * lvinf - m * cy2 + m * m
so m * lvinf - m * cy2 + m * m < m * m
so m * (lvinf - cy2) = m * lvinf - m * cy2 < 0
so lvinf - cy2 < 0
so (cy2 <= 1 by !cy at AddSub = 0 so !cy at Add3 = 0)
so (lvinf = 0 by 0 <= lvinf)
so a1 * b1 = m * hvinf
so if a1*b1 <= 0
then (hvinf <= m' - 2
by m*hvinf=0 so 0 <> m so hvinf = 0
so 1 <= s+t-n
so radix = power radix 1 <= power radix (s+t-n)
so m' > 2
so hvinf <= m' - 2)
else hvinf <= m'-2 by
(forall s. 0 <= s -> power radix s = power 2 (64*s)
by radix = power 2 64)
so (m = power 2 (64 * n)
by m = power radix n)
so m >= 1
so (hvinf >= 1 by m*hvinf > 0)
so valuation m 2 = 64*n
so 64*n <= valuation (a1*b1) 2 = valuation a1 2 + valuation b1 2
so if 64*n < valuation (a1*b1) 2
then hvinf <= m'-2
by valuation (m*hvinf) 2 > 64*n
so valuation m 2 = 64*n
so if valuation hvinf 2 = 0
then false by valuation (m*hvinf) 2 = valuation m 2
else hvinf <= m'-2
by even hvinf
so (odd (m'-1)
by m' = power radix (s+t-n)
= power 2 (64*(s+t-n))
= 2 * power 2 (64*(s+t-n) - 1)
so even m')
so hvinf <> m'-1
so (hvinf < m'
by hvinf = value vinfnj (s+t-n)
< power radix ((offset vinfnj +(s+t-n))
- offset vinfnj)
= power radix (s+t-n))
so hvinf < m'-1
else hvinf <= m'-2
by power radix s = power 2 (64*s)
so power radix t = power 2 (64*t)
so m' = power radix (s+t-n) = power 2 (64*(s+t-n))
so let k = valuation a1 2 in
let l = valuation b1 2 in
let a1' = div a1 (power 2 k) in
let b1' = div b1 (power 2 l) in
a1 = (power 2 k) * a1'
so b1 = (power 2 l) * b1'
so 64*n = k + l
so 1 <= a1 /\ 1 <= b1
so 0 <= k /\ 0 <= l
so 1 <= a1' /\ 1 <= b1'
so (k <= 64*s by power 2 k <= a1 < power 2 (64*s)
so power 2 k < power 2 (64*s)
so not 64*s < k)
so (l <= 64*t by power 2 l <= b1 < power 2 (64*t)
so power 2 l < power 2 (64*t)
so not 64*t < l)
so (forall a b c m:int. 0 <= a -> 0 <= b -> 0 < c -> 0 < m
-> a * c < m -> b * c >= m -> a < b)
so a1' < power 2 (64*s - k)
(*(by a1' * (power 2 k) = a1 < power radix s = power 2 (64*s)
so a1' * power 2 k < power 2 (64*s)
so power 2 (64*s-k) * power 2 k = power 2 (64*s))*)
so a1' <= power 2 (64*s - k) - 1
so b1' < power 2 (64*t - l)
so b1' <= power 2 (64*t - l) - 1
so a1' * b1'
<= (power 2 (64*s - k) - 1) * b1'
<= (power 2 (64*s - k) - 1) * (power 2 (64*t - l) - 1)
= (power 2 (64*s-k))*(power 2 (64*t -l))
- power 2 (64*s-k)
- power 2 (64*t-l)
+ 1
<= (power 2 (64*s-k))*(power 2 (64*t -l)) - 2
= power 2 (64*(s+t) - (k+l)) - 2
= power 2 (64*(s+t) - 64*n) - 2
= power 2 (64*(s+t-n)) - 2
= power radix (s+t-n) - 2
= m' - 2
so a1 * b1 = (power 2 k) * a1' * (power 2 l) * b1'
= power 2 k * power 2 l * a1' * b1'
= (power 2 (k+l)) * a1' * b1'
= power 2 (64*n) * a1' * b1'
= power radix n * a1' * b1'
= m * (a1' * b1')
so a1 * b1 = m * hvinf = m * (a1' * b1')
so hvinf = a1' * b1' <= m' - 2 };
assert { value x sx * value y sy < m * m * m * m'
by (m * m * m * m' = power radix (n+n+s+t)
by m * m * m * m'
......
This source diff could not be displayed because it is too large. You can view the blob instead.
module Valuation
use import int.Int
use import int.Power
use import int.ComputerDivision
use export number.Divisibility
use import number.Prime
use import number.Coprime
use export number.Parity
let rec function valuation (n p: int)
requires { 1 < p }
requires { 1 <= n }
variant { n }
ensures { 0 <= result }
ensures { divides (power p result) n }
= if mod n p = 0
then
let d = div n p in
let r = valuation d p in
r+1
else 0
lemma valuation_mul: forall n p. 1 <= n -> 1 < p
-> valuation (n*p) p = 1 + valuation n p
by mod (n*p) p = 0 so div (n*p) p = n
lemma power_ge_1: forall b e. 1 <= b -> 0 <= e -> 1 <= power b e
let rec lemma valuation_times_pow (n p k:int)
requires { 1 <= n /\ 1 < p /\ 0 <= k }
ensures { valuation (n * power p k) p = k + valuation n p }
variant { k }
=
if k > 0
then begin
valuation_times_pow n p (k-1);
assert { valuation (n * power p k) p
= 1 + valuation (n * power p (k-1)) p
by valuation (n * power p k) p
= valuation (n * power p (k-1) * p) p
= 1 + valuation (n * power p (k-1)) p }
end
let lemma valuation_lower_bound (n p v:int)
requires { 1 <= n /\ 1 < p /\ 0 <= v }
requires { divides (power p v) n }
ensures { v <= valuation n p }
=
let q = div n (power p v) in
assert { n = q * power p v };
valuation_times_pow q p v
lemma valuation_pow: forall p k. 1 < p /\ 0 <= k -> valuation (power p k) p = k
let rec lemma valuation_monotonous (n c p:int)
requires { 1 <= n /\ 1 <= c /\ 1 < p }
ensures { valuation n p <= valuation (n*c) p }
variant { n }
= if mod n p = 0
then begin
let q = div n p in
assert { n = p * q };
valuation_monotonous q c p;
assert { valuation n p = 1 + valuation q p };
let m = q * c in
assert { valuation (n * c) p = 1 + valuation m p
by n * c = m * p
so valuation (n*c) p = valuation (m*p) p
= 1 + valuation m p };
end
lemma valuation_nondiv: forall n p. 1 <= n -> 1 < p ->
valuation n p = 0 <-> not (divides p n)
lemma valuation_zero_prod: forall c1 c2 p. 1 <= c1 -> 1 <= c2 -> prime p ->
valuation c1 p = 0 -> valuation c2 p = 0 -> valuation (c1 * c2) p = 0
lemma valuation_split: forall n p. 1 <= n -> prime p ->
let v = valuation n p in
valuation (div n (power p v)) p = 0 (* only altergo proves this? *)
let rec lemma valuation_times_nondiv (n c p:int)
requires { 1 <= n /\ 1 <= c }
requires { prime p }
requires { valuation c p = 0 }
ensures { valuation (n*c) p = valuation n p }
variant { n }
= if mod n p = 0
then let d = div n p in
valuation_times_nondiv d c p;
assert { valuation (n*c) p
= valuation (d*c*p) p
= 1 + valuation (d*c) p
= 1 + valuation d p = valuation n p }
else ()
lemma valuation_prod: forall n1 n2 p. 1 <= n1 -> 1 <= n2 -> prime p
-> valuation (n1 * n2) p = valuation n1 p + valuation n2 p
by let v1 = valuation n1 p in
let v2 = valuation n2 p in
let c1 = div n1 (power p v1) in
let c2 = div n2 (power p v2) in
n1 = power p v1 * c1
so n2 = power p v2 * c2
so valuation c1 p = 0
so valuation c2 p = 0
so valuation (c1 * c2) p = 0
so n1 * n2 = power p v1 * power p v2 * (c1 * c2)
= power p (v1+v2) * (c1 * c2)
so let pow = power p (v1+v2) in
let c = c1 * c2 in
1 <= c1 so 1 <= c2 so 1 <= c
so valuation (n1*n2) p = valuation (pow * c) p = valuation pow p = v1 + v2
lemma valuation_mod: forall n p. 1 <= n -> 1 < p -> (mod n p = 0 <-> valuation n p > 0)
lemma valuation_decomp: forall n p. 1 <= n -> 1 < p ->
n = (power p (valuation n p)) * (div n (power p (valuation n p)))
by divides (power p (valuation n p)) n
end
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="2000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../valuation.mlw" proved="true">
<theory name="Valuation" proved="true">
<goal name="VC valuation" expl="VC for valuation" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC valuation.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation.2" expl="variant decrease" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="VC valuation.2.0" expl="variant decrease" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation.2.0.0" expl="VC for valuation" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation.2.0.1" expl="VC for valuation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<transf name="remove" proved="true" arg1="real,bool,tuple0,unit,zero,one,(-),(+),(-),div1,mod1,power,even,odd,divides,gcd,prime,coprime,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc2,Mul_distr_l,Mul_distr_r,Comm2,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Div_mod,Mod_bound,Div_unique,Mod_1,Div_1,Div_inf,Div_inf_neg,Mod_0,Div_1_left,Div_minus1_left,Mod_1_left,Mod_minus1_left,Div_mult,Mod_mult,Div_mod1,Div_bound1,Mod_bound1,Div_sign_pos,Div_sign_neg,Mod_sign_pos,Mod_sign_neg,Div_11,Mod_11,Div_inf1,Mod_inf,Div_mult1,Mod_mult1,Power_0,Power_s,Power_s_alt,Power_1,Power_sum,Power_mult,Power_comm1,Power_comm2,Power_non_neg,Power_monotonic,even_or_odd,even_not_odd,odd_not_even,even_odd,odd_even,even_even,odd_odd,even_2k,odd_2k1,even_mod2,divides_spec,divides_refl,divides_1_n,divides_0,divides_left,divides_right,divides_oppr,divides_oppl,divides_oppr_rev,divides_oppl_rev,divides_plusr,divides_minusr,divides_multl,divides_multr,divides_factorl,divides_factorr,divides_n_1,divides_antisym,divides_trans,divides_bounds,mod_divides_euclidean,divides_mod_euclidean,mod_divides_computer,divides_mod_computer,even_divides,odd_divides,gcd_nonneg,gcd_def1,gcd_def2,gcd_def3,gcd_unique,Assoc,Comm,gcd_0_pos,gcd_0_neg,gcd_opp,gcd_euclid,Gcd_computer_mod,Gcd_euclidean_mod,gcd_mult,not_prime_1,prime_2,prime_3,prime_divisors,small_divisors,even_prime,odd_prime,prime_coprime,Gauss,Euclid,gcd_coprime,H">
<goal name="VC valuation.2.0.1.0" expl="VC for valuation" proved="true">
<proof prover="1" timelimit="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC valuation.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC valuation.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC valuation.5" expl="postcondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation.6" expl="postcondition" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation.6.0" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="2.24"/></proof>
</goal>
<goal name="VC valuation.6.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="19"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="valuation_mul" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="valuation_mul.0" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="valuation_mul.1" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="35"/></proof>
</goal>
<goal name="valuation_mul.2" proved="true">
<proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
</goal>
</transf>
</goal>
<goal name="power_ge_1" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
<transf name="introduce_premises" proved="true" >
<goal name="power_ge_1.0" proved="true">
<transf name="induction" proved="true" arg1="e">
<goal name="power_ge_1.0.0" expl="base case" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="power_ge_1.0.1" expl="recursive case" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC valuation_times_pow" expl="VC for valuation_times_pow" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_times_pow.0" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_pow.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_pow.2" expl="assertion" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_times_pow.2.0" expl="VC for valuation_times_pow" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC valuation_times_pow.2.1" expl="VC for valuation_times_pow" proved="true">
<proof prover="3"><result status="valid" time="0.13" steps="44"/></proof>
</goal>
<goal name="VC valuation_times_pow.2.2" expl="VC for valuation_times_pow" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC valuation_times_pow.3" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
</transf>
</goal>
<goal name="VC valuation_lower_bound" expl="VC for valuation_lower_bound" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_lower_bound.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC valuation_lower_bound.1" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="VC valuation_lower_bound.2" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="VC valuation_lower_bound.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.06" steps="41"/></proof>
</goal>
</transf>
</goal>
<goal name="valuation_pow" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="valuation_pow.0" proved="true">
<transf name="induction" proved="true" arg1="k">
<goal name="valuation_pow.0.0" expl="base case" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="valuation_pow.0.1" expl="recursive case" proved="true">
<proof prover="4"><result status="valid" time="0.90"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC valuation_monotonous" expl="VC for valuation_monotonous" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_monotonous.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_monotonous.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_monotonous.2" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_monotonous.3" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC valuation_monotonous.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_monotonous.5" expl="assertion" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_monotonous.6" expl="assertion" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_monotonous.6.0" expl="VC for valuation_monotonous" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="11"/></proof>
</goal>
<goal name="VC valuation_monotonous.6.1" expl="VC for valuation_monotonous" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_monotonous.6.2" expl="VC for valuation_monotonous" proved="true">
<proof prover="3"><result status="valid" time="0.12" steps="100"/></proof>
</goal>
<goal name="VC valuation_monotonous.6.3" expl="VC for valuation_monotonous" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
<goal name="VC valuation_monotonous.7" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="22"/></proof>
</goal>
</transf>
</goal>
<goal name="valuation_nondiv" proved="true">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="valid" time="0.13" steps="97"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="valuation_zero_prod" proved="true">
<proof prover="3"><result status="valid" time="0.13" steps="73"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="valuation_split" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="valuation_split.0" proved="true">
<proof prover="3"><result status="valid" time="0.45" steps="85"/></proof>
<transf name="remove" proved="true" arg1="real,bool,tuple0,unit">
<goal name="valuation_split.0.0" proved="true">
<proof prover="3"><result status="valid" time="0.32" steps="85"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC valuation_times_nondiv" expl="VC for valuation_times_nondiv" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_times_nondiv.0" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.1" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.2" expl="variant decrease" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.3" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.4" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.5" expl="precondition" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6" expl="assertion" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="VC valuation_times_nondiv.6.0" expl="VC for valuation_times_nondiv" proved="true">
<proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6.1" expl="VC for valuation_times_nondiv" proved="true">
<transf name="apply" proved="true" arg1="valuation_mul">
<goal name="VC valuation_times_nondiv.6.1.0" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6.1.1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6.1.2" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="32"/></proof>
</goal>
</transf>
</goal>
<goal name="VC valuation_times_nondiv.6.2" expl="VC for valuation_times_nondiv" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6.3" expl="VC for valuation_times_nondiv" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="VC valuation_times_nondiv.7" expl="postcondition" proved="true">
<proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
<proof prover="3"><result status="valid" time="0.02" steps="25"/></proof>
<proof prover="4" obsolete="true"><result status="timeout" time="1.00"/></proof>
</goal>
</transf>
</goal>
<goal name="valuation_prod" proved="true">
<transf name="split_intros_goal_wp" proved="true" >
<goal name="valuation_prod.0" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="34"/></proof>
</goal>
<goal name="valuation_prod.1" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="37"/></proof>
</goal>
<goal name="valuation_prod.2" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="valuation_prod.3" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="valuation_prod.4" proved="true">
<transf name="apply" proved="true" arg1="valuation_zero_prod">
<goal name="valuation_prod.4.0" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="valuation_prod.4.1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="valuation_prod.4.2" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="valuation_prod.4.3" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
<goal name="valuation_prod.4.4" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="19"/></proof>
</goal>
</transf>
</goal>
<goal name="valuation_prod.5" proved="true">
<proof prover="3"><result status="valid" time="0.02" steps="12"/></proof>
</goal>
<goal name="valuation_prod.6" proved="true">
<transf name="rewrite" proved="true" arg1="&lt;-" arg2="Power_sum">
<goal name="valuation_prod.6.0" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="valuation_prod.6.1" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="valuation_prod.6.2" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
<goal name="valuation_prod.7" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="32"/></proof>
</goal>
<goal name="valuation_prod.8" proved="true">
<proof prover="3"><result status="valid" time="0.04" steps="33"/></proof>