Update sessions and add forgotten function to util

examples/in_progress/multiprecision/valuation.mlw

@@ -42,6 +42,10 @@ module Valuation
                = 1 + valuation (n * power p (k-1)) p }
     end
 
+  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 lemma valuation_lower_bound (n p v:int)
     requires {  1 <= n /\ 1 < p /\ 0 <= v }
     requires { divides (power p v) n }
@@ -76,10 +80,6 @@ module Valuation
   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 }

examples/in_progress/multiprecision/valuation/valuation-Valuation-valuation_split_1.why

+(* this is the prelude for Alt-Ergo, version >= 0.95.2 *)
+(* this is a prelude for Alt-Ergo integer arithmetic *)
+logic comp_div: int, int -> int
+axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y
+logic comp_mod: int, int -> int
+axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y
+logic match_bool : bool, 'a, 'a -> 'a
+
+axiom match_bool_True :
+  (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))
+
+axiom match_bool_False :
+  (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))
+
+axiom CompatOrderMult :
+  (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) ->
+  ((x * z) <= (y * z)))))
+
+logic power : int, int -> int
+
+axiom Power_0 : (forall x:int. (power(x, 0) = 1))
+
+axiom Power_s :
+  (forall x:int. forall n:int. ((0 <= n) -> (power(x,
+  (n + 1)) = (x * power(x, n)))))
+
+axiom Power_s_alt :
+  (forall x:int. forall n:int. ((0 <  n) -> (power(x, n) = (x * power(x,
+  (n - 1))))))
+
+axiom Power_1 : (forall x:int. (power(x, 1) = x))
+
+axiom Power_sum :
+  (forall x:int. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) ->
+  (power(x, (n + m)) = (power(x, n) * power(x, m))))))
+
+axiom Power_mult :
+  (forall x:int. forall n:int. forall m:int. ((0 <= n) -> ((0 <= m) ->
+  (power(x, (n * m)) = power(power(x, n), m)))))
+
+axiom Power_comm1 :
+  (forall x:int. forall y:int. (((x * y) = (y * x)) ->
+  (forall n:int. ((0 <= n) -> ((power(x, n) * y) = (y * power(x, n)))))))
+
+axiom Power_comm2 :
+  (forall x:int. forall y:int. (((x * y) = (y * x)) ->
+  (forall n:int. ((0 <= n) -> (power((x * y), n) = (power(x, n) * power(y,
+  n)))))))
+
+axiom Power_non_neg :
+  (forall x:int. forall y:int. (((0 <= x) and (0 <= y)) -> (0 <= power(x,
+  y))))
+
+axiom Power_monotonic :
+  (forall x:int. forall n:int. forall m:int. (((0 <  x) and ((0 <= n) and
+  (n <= m))) -> (power(x, n) <= power(x, m))))
+
+logic abs : int -> int
+
+axiom abs_def : (forall x:int. ((0 <= x) -> (abs(x) = x)))
+
+axiom abs_def1 : (forall x:int. ((not (0 <= x)) -> (abs(x) = (-x))))
+
+axiom Abs_le : (forall x:int. forall y:int. ((abs(x) <= y) -> ((-y) <= x)))
+
+axiom Abs_le1 : (forall x:int. forall y:int. ((abs(x) <= y) -> (x <= y)))
+
+axiom Abs_le2 :
+  (forall x:int. forall y:int. ((((-y) <= x) and (x <= y)) -> (abs(x) <= y)))
+
+axiom Abs_pos : (forall x:int. (0 <= abs(x)))
+
+axiom Div_mod :
+  (forall x:int. forall y:int. ((not (y = 0)) ->
+  (x = ((y * comp_div(x,y)) + comp_mod(x,y)))))
+
+axiom Div_bound :
+  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
+  (0 <= comp_div(x,y))))
+
+axiom Div_bound1 :
+  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
+  (comp_div(x,y) <= x)))
+
+axiom Mod_bound :
+  (forall x:int. forall y:int. ((not (y = 0)) ->
+  ((-abs(y)) <  comp_mod(x,y))))
+
+axiom Mod_bound1 :
+  (forall x:int. forall y:int. ((not (y = 0)) -> (comp_mod(x,y) <  abs(y))))
+
+axiom Div_sign_pos :
+  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) ->
+  (0 <= comp_div(x,y))))
+
+axiom Div_sign_neg :
+  (forall x:int. forall y:int. (((x <= 0) and (0 <  y)) ->
+  (comp_div(x,y) <= 0)))
+
+axiom Mod_sign_pos :
+  (forall x:int. forall y:int. (((0 <= x) and (not (y = 0))) ->
+  (0 <= comp_mod(x,y))))
+
+axiom Mod_sign_neg :
+  (forall x:int. forall y:int. (((x <= 0) and (not (y = 0))) ->
+  (comp_mod(x,y) <= 0)))
+
+axiom Rounds_toward_zero :
+  (forall x:int. forall y:int. ((not (y = 0)) ->
+  (abs((comp_div(x,y) * y)) <= abs(x))))
+
+axiom Div_1 : (forall x:int. (comp_div(x,1) = x))
+
+axiom Mod_1 : (forall x:int. (comp_mod(x,1) = 0))
+
+axiom Div_inf :
+  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
+  (comp_div(x,y) = 0)))
+
+axiom Mod_inf :
+  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) ->
+  (comp_mod(x,y) = x)))
+
+axiom Div_mult :
+  (forall x:int. forall y:int. forall z:int [comp_div(((x * y) + z),x)].
+  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
+  (comp_div(((x * y) + z),x) = (y + comp_div(z,x)))))
+
+axiom Mod_mult :
+  (forall x:int. forall y:int. forall z:int [comp_mod(((x * y) + z),x)].
+  (((0 <  x) and ((0 <= y) and (0 <= z))) ->
+  (comp_mod(((x * y) + z),x) = comp_mod(z,x))))
+
+predicate divides(d: int, n: int) = (((d = 0) -> (n = 0)) and
+  ((not (d = 0)) -> (comp_mod(n,d) = 0)))
+
+axiom divides_spec :
+  (forall d:int. forall n:int. (divides(d, n) ->
+  (exists q:int. (n = (q * d)))))
+
+axiom divides_spec1 :
+  (forall d:int. forall n:int. ((exists q:int. (n = (q * d))) -> divides(d,
+  n)))
+
+axiom divides_refl : (forall n:int. divides(n, n))
+
+axiom divides_1_n : (forall n:int. divides(1, n))
+
+axiom divides_0 : (forall n:int. divides(n, 0))
+
+axiom divides_left :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) ->
+  divides((c * a), (c * b))))
+
+axiom divides_right :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) ->
+  divides((a * c), (b * c))))
+
+axiom divides_oppr :
+  (forall a:int. forall b:int. (divides(a, b) -> divides(a, (-b))))
+
+axiom divides_oppl :
+  (forall a:int. forall b:int. (divides(a, b) -> divides((-a), b)))
+
+axiom divides_oppr_rev :
+  (forall a:int. forall b:int. (divides((-a), b) -> divides(a, b)))
+
+axiom divides_oppl_rev :
+  (forall a:int. forall b:int. (divides(a, (-b)) -> divides(a, b)))
+
+axiom divides_plusr :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(a,
+  c) -> divides(a, (b + c)))))
+
+axiom divides_minusr :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(a,
+  c) -> divides(a, (b - c)))))
+
+axiom divides_multl :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides(a,
+  (c * b))))
+
+axiom divides_multr :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) -> divides(a,
+  (b * c))))
+
+axiom divides_factorl : (forall a:int. forall b:int. divides(a, (b * a)))
+
+axiom divides_factorr : (forall a:int. forall b:int. divides(a, (a * b)))
+
+axiom divides_n_1 :
+  (forall n:int. (divides(n, 1) -> ((n = 1) or (n = (- 1)))))
+
+axiom divides_antisym :
+  (forall a:int. forall b:int. (divides(a, b) -> (divides(b, a) ->
+  ((a = b) or (a = (-b))))))
+
+axiom divides_trans :
+  (forall a:int. forall b:int. forall c:int. (divides(a, b) -> (divides(b,
+  c) -> divides(a, c))))
+
+axiom divides_bounds :
+  (forall a:int. forall b:int. (divides(a, b) -> ((not (b = 0)) ->
+  (abs(a) <= abs(b)))))
+
+axiom Div_mod1 :
+  (forall x:int. forall y:int. ((not (y = 0)) ->
+  (x = ((y * (x / y)) + (x % y)))))
+
+axiom Mod_bound2 :
+  (forall x:int. forall y:int. ((not (y = 0)) -> (0 <= (x % y))))
+
+axiom Mod_bound3 :
+  (forall x:int. forall y:int. ((not (y = 0)) -> ((x % y) <  abs(y))))
+
+axiom Div_unique :
+  (forall x:int. forall y:int. forall q:int. ((0 <  y) ->
+  ((((q * y) <= x) and (x <  ((q * y) + y))) -> ((x / y) = q))))
+
+axiom Div_bound2 :
+  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) -> (0 <= (x / y))))
+
+axiom Div_bound3 :
+  (forall x:int. forall y:int. (((0 <= x) and (0 <  y)) -> ((x / y) <= x)))
+
+axiom Mod_11 : (forall x:int. ((x % 1) = 0))
+
+axiom Div_11 : (forall x:int. ((x / 1) = x))
+
+axiom Div_inf1 :
+  (forall x:int. forall y:int. (((0 <= x) and (x <  y)) -> ((x / y) = 0)))
+
+axiom Div_inf_neg :
+  (forall x:int. forall y:int. (((0 <  x) and (x <= y)) ->
+  (((-x) / y) = (- 1))))
+
+axiom Mod_0 : (forall y:int. ((not (y = 0)) -> ((0 % y) = 0)))
+
+axiom Div_1_left : (forall y:int. ((1 <  y) -> ((1 / y) = 0)))
+
+axiom Div_minus1_left : (forall y:int. ((1 <  y) -> (((- 1) / y) = (- 1))))
+
+axiom Mod_1_left : (forall y:int. ((1 <  y) -> ((1 % y) = 1)))
+
+axiom Mod_minus1_left : (forall y:int. ((1 <  y) -> (((- 1) % y) = (y - 1))))
+
+axiom Div_mult1 :
+  (forall x:int. forall y:int. forall z:int [(((x * y) + z) / x)].
+  ((0 <  x) -> ((((x * y) + z) / x) = (y + (z / x)))))
+
+axiom Mod_mult1 :
+  (forall x:int. forall y:int. forall z:int [(((x * y) + z) % x)].
+  ((0 <  x) -> ((((x * y) + z) % x) = (z % x))))
+
+axiom mod_divides_euclidean :
+  (forall a:int. forall b:int. ((not (b = 0)) -> (((a % b) = 0) -> divides(b,
+  a))))
+
+axiom divides_mod_euclidean :
+  (forall a:int. forall b:int. ((not (b = 0)) -> (divides(b, a) ->
+  ((a % b) = 0))))
+
+axiom mod_divides_computer :
+  (forall a:int. forall b:int. ((not (b = 0)) -> ((comp_mod(a,b) = 0) ->
+  divides(b, a))))
+
+axiom divides_mod_computer :
+  (forall a:int. forall b:int. ((not (b = 0)) -> (divides(b, a) ->
+  (comp_mod(a,b) = 0))))
+
+predicate even(n: int) = (exists k:int. (n = (2 * k)))
+
+predicate odd(n: int) = (exists k:int. (n = ((2 * k) + 1)))
+
+axiom even_or_odd : (forall n:int. (even(n) or odd(n)))
+
+axiom even_not_odd : (forall n:int. (even(n) -> (not odd(n))))
+
+axiom odd_not_even : (forall n:int. (odd(n) -> (not even(n))))
+
+axiom even_odd : (forall n:int. (even(n) -> odd((n + 1))))
+
+axiom odd_even : (forall n:int. (odd(n) -> even((n + 1))))
+
+axiom even_even : (forall n:int. (even(n) -> even((n + 2))))
+
+axiom odd_odd : (forall n:int. (odd(n) -> odd((n + 2))))
+
+axiom even_2k : (forall k:int. even((2 * k)))
+
+axiom odd_2k1 : (forall k:int. odd(((2 * k) + 1)))
+
+axiom even_mod2 : (forall n:int. (even(n) -> (comp_mod(n,2) = 0)))
+
+axiom even_mod21 : (forall n:int. ((comp_mod(n,2) = 0) -> even(n)))
+
+axiom even_divides : (forall a:int. (even(a) -> divides(2, a)))
+
+axiom even_divides1 : (forall a:int. (divides(2, a) -> even(a)))
+
+axiom odd_divides : (forall a:int. (odd(a) -> (not divides(2, a))))
+
+axiom odd_divides1 : (forall a:int. ((not divides(2, a)) -> odd(a)))
+
+predicate prime(p: int) = ((2 <= p) and
+  (forall n:int. (((1 <  n) and (n <  p)) -> (not divides(n, p)))))
+
+axiom not_prime_1 : (not prime(1))
+
+axiom prime_2 : prime(2)
+
+axiom prime_3 : prime(3)
+
+axiom prime_divisors :
+  (forall p:int. (prime(p) ->
+  (forall d:int. (divides(d, p) -> ((d = 1) or ((d = (- 1)) or ((d = p) or
+  (d = (-p)))))))))
+
+axiom small_divisors :
+  (forall p:int. ((2 <= p) ->
+  ((forall d:int. ((2 <= d) -> (prime(d) -> (((1 <  (d * d)) and
+   ((d * d) <= p)) -> (not divides(d, p)))))) ->
+  prime(p))))
+
+axiom even_prime : (forall p:int. (prime(p) -> (even(p) -> (p = 2))))
+
+axiom odd_prime : (forall p:int. (prime(p) -> ((3 <= p) -> odd(p))))
+
+logic ac gcd : int, int -> int
+
+axiom gcd_nonneg : (forall a:int. forall b:int. (0 <= gcd(a, b)))
+
+axiom gcd_def1 : (forall a:int. forall b:int. divides(gcd(a, b), a))
+
+axiom gcd_def2 : (forall a:int. forall b:int. divides(gcd(a, b), b))
+
+axiom gcd_def3 :
+  (forall a:int. forall b:int. forall x:int. (divides(x, a) -> (divides(x,
+  b) -> divides(x, gcd(a, b)))))
+
+axiom gcd_unique :
+  (forall a:int. forall b:int. forall d:int. ((0 <= d) -> (divides(d, a) ->
+  (divides(d, b) ->
+  ((forall x:int. (divides(x, a) -> (divides(x, b) -> divides(x, d)))) ->
+  (d = gcd(a, b)))))))
+
+axiom gcd_0_pos : (forall a:int. ((0 <= a) -> (gcd(a, 0) = a)))
+
+axiom gcd_0_neg : (forall a:int. ((a <  0) -> (gcd(a, 0) = (-a))))
+
+axiom gcd_opp : (forall a:int. forall b:int. (gcd(a, b) = gcd((-a), b)))
+
+axiom gcd_euclid :
+  (forall a:int. forall b:int. forall q:int. (gcd(a, b) = gcd(a,
+  (b - (q * a)))))
+
+axiom Gcd_computer_mod :
+  (forall a:int. forall b:int [gcd(b, comp_mod(a,b))]. ((not (b = 0)) ->
+  (gcd(b, comp_mod(a,b)) = gcd(a, b))))
+
+axiom Gcd_euclidean_mod :
+  (forall a:int. forall b:int [gcd(b, (a % b))]. ((not (b = 0)) -> (gcd(b,
+  (a % b)) = gcd(a, b))))
+
+axiom gcd_mult :
+  (forall a:int. forall b:int. forall c:int. ((0 <= c) -> (gcd((c * a),
+  (c * b)) = (c * gcd(a, b)))))
+
+predicate coprime(a: int, b: int) = (gcd(a, b) = 1)
+
+axiom prime_coprime : (forall p:int. (prime(p) -> (2 <= p)))
+
+axiom prime_coprime1 :
+  (forall p:int. (prime(p) ->
+  (forall n:int. (((1 <= n) and (n <  p)) -> coprime(n, p)))))
+
+axiom prime_coprime2 :
+  (forall p:int. (((2 <= p) and
+  (forall n:int. (((1 <= n) and (n <  p)) -> coprime(n, p)))) -> prime(p)))
+
+axiom Gauss :
+  (forall a:int. forall b:int. forall c:int. ((divides(a, (b * c)) and
+  coprime(a, b)) -> divides(a, c)))
+
+axiom Euclid :
+  (forall p:int. forall a:int. forall b:int. ((prime(p) and divides(p,
+  (a * b))) -> (divides(p, a) or divides(p, b))))
+
+axiom gcd_coprime :
+  (forall a:int. forall b:int. forall c:int. (coprime(a, b) -> (gcd(a,
+  (b * c)) = gcd(a, c))))
+
+logic valuation : int, int -> int
+
+axiom valuation_def :
+  (forall n:int. forall p:int. ((1 <  p) -> ((1 <= n) ->
+  ((comp_mod(n,p) = 0) -> (valuation(n, p) = (valuation(comp_div(n,p),
+  p) + 1))))))
+
+axiom valuation_def1 :
+  (forall n:int. forall p:int. ((1 <  p) -> ((1 <= n) ->
+  ((not (comp_mod(n,p) = 0)) -> (valuation(n, p) = 0)))))
+
+axiom valuation_spec :
+  (forall n:int. forall p:int. ((1 <  p) -> ((1 <= n) -> (0 <= valuation(n,
+  p)))))
+
+axiom valuation_spec1 :
+  (forall n:int. forall p:int. ((1 <  p) -> ((1 <= n) -> divides(power(p,
+  valuation(n, p)), n))))
+
+axiom valuation_mul :
+  (forall n:int. forall p:int. ((1 <= n) -> ((1 <  p) -> (valuation((n * p),
+  p) = (1 + valuation(n, p))))))
+
+axiom power_ge_1 :
+  (forall b:int. forall e:int. ((1 <= b) -> ((0 <= e) -> (1 <= power(b,
+  e)))))
+
+axiom valuation_times_pow :
+  (forall n:int. forall p:int. forall k:int. (((1 <= n) and ((1 <  p) and
+  (0 <= k))) -> (valuation((n * power(p, k)), p) = (k + valuation(n, p)))))
+
+goal valuation_split :
+  (forall n:int. forall p:int. ((1 <= n) -> (prime(p) ->
+  (valuation(comp_div(n,power(p, valuation(n, p))), p) = 0))))

examples/in_progress/multiprecision/valuation/why3session.xml

@@ -5,8 +5,8 @@
 <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"/>
+<prover id="5" name="Alt-Ergo" version="2.0.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">
@@ -26,12 +26,6 @@
     </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>
@@ -52,8 +46,8 @@
    <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>
+   <proof prover="5"><result status="valid" time="0.01" steps="21"/></proof>
    </goal>
   </transf>
   </goal>
@@ -62,13 +56,13 @@
  <goal name="valuation_mul" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="valuation_mul.0" proved="true">
-  <proof prover="3"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="5"><result status="valid" time="0.01" steps="17"/></proof>
   </goal>
   <goal name="valuation_mul.1" proved="true">
-  <proof prover="3"><result status="valid" time="0.01" steps="35"/></proof>
+  <proof prover="5"><result status="valid" time="0.01" steps="37"/></proof>
   </goal>
   <goal name="valuation_mul.2" proved="true">
-  <proof prover="3"><result status="valid" time="0.00" steps="13"/></proof>
+  <proof prover="5"><result status="valid" time="0.00" steps="15"/></proof>
   </goal>
  </transf>
  </goal>
@@ -98,10 +92,10 @@
   <goal name="VC valuation_times_pow.2" expl="assertion" proved="true">
   <transf name="split_vc" 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>
+   <proof prover="5"><result status="valid" time="0.01" steps="18"/></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>
+   <proof prover="5"><result status="valid" time="0.13" steps="47"/></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>
@@ -113,19 +107,23 @@
   </goal>
  </transf>
  </goal>
+ <goal name="valuation_split" proved="true">
+ <proof prover="4"><result status="timeout" time="1.00"/></proof>
+ <proof prover="5"><result status="valid" time="0.48" steps="164"/></proof>
+ </goal>
  <goal name="VC valuation_lower_bound" expl="VC for valuation_lower_bound" proved="true">
  <transf name="split_vc" 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>
+  <proof prover="5"><result status="valid" time="0.01" steps="17"/></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>
+  <proof prover="5"><result status="valid" time="0.02" steps="40"/></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>
+  <proof prover="5"><result status="valid" time="0.06" steps="43"/></proof>
   </goal>
  </transf>
  </goal>
@@ -134,7 +132,7 @@
   <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>
+   <proof prover="5"><result status="valid" time="0.02" steps="25"/></proof>
    </goal>
    <goal name="valuation_pow.0.1" expl="recursive case" proved="true">
    <proof prover="4"><result status="valid" time="0.90"/></proof>
@@ -146,10 +144,10 @@
  <goal name="VC valuation_monotonous" expl="VC for valuation_monotonous" proved="true">
  <transf name="split_vc" proved="true" >
   <goal name="VC valuation_monotonous.0" expl="precondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.02"/></proof>
+  <proof prover="4"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC valuation_monotonous.1" expl="precondition" proved="true">
-  <proof prover="4"><result status="valid" time="0.01"/></proof>
+  <proof prover="4"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC valuation_monotonous.2" expl="assertion" proved="true">
   <proof prover="4"><result status="valid" time="0.02"/></proof>
@@ -166,13 +164,13 @@
   <goal name="VC valuation_monotonous.6" expl="assertion" proved="true">
   <transf name="split_vc" 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>
+   <proof prover="5"><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>
+   <proof prover="5"><result status="valid" time="0.12" steps="110"/></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>
@@ -180,39 +178,23 @@
   </transf>
   </goal>
   <goal name="VC valuation_monotonous.7" expl="postcondition" proved="true">
-  <proof prover="3"><result status="valid" time="0.01" steps="22"/></proof>
+  <proof prover="5"><result status="valid" time="0.01" steps="24"/></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>
+ <proof prover="5"><result status="valid" time="0.13" steps="98"/></proof>