From 636f400d3c048670b96b8d8d1c60f091e22bca8e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Mon, 3 Oct 2022 16:12:32 +0200
Subject: [PATCH] Simplify the proof of floating point propagation
But the approach seems not scalable
---
common/float_interval.mlw | 63 +-
common/float_interval/why3session.xml | 1117 ++++++++++---------------
2 files changed, 518 insertions(+), 662 deletions(-)
diff --git a/common/float_interval.mlw b/common/float_interval.mlw
index 37f1ac629..de3e0bb7e 100644
--- a/common/float_interval.mlw
+++ b/common/float_interval.mlw
@@ -44,7 +44,7 @@ module GenericFloat
axiom round_to_float: forall r m. is_float (round m r)
axiom round_float: forall r m. is_float r -> round m r = r
- axiom max_real_not_zero: max_real <> 0.
+ axiom max_real_not_zero: 0. <. max_real
axiom max_real_round: is_float max_real
type finite = abstract {
@@ -315,7 +315,8 @@ module GenericFloat
axiom minus_max_real_round : forall m. round m (-. max_real) = -. max_real
- axiom zero_round : forall m. round m 0. = 0.
+ axiom zero_is_float : is_float 0.
+ lemma zero_round : forall m. round m 0. = 0.
goal is_finite: forall x:t. is_finite x <-> in_range (to_real x)
@@ -330,6 +331,12 @@ module GenericFloat
axiom Round_monotonic :
forall m:mode, x y:real. x <=. y -> round m x <=. round m y
+ lemma Round_monotonic_gen :
+ forall m:mode, x y:real. is_float x -> if x <=. y then x <=. round m y else round m y <=. x
+
+ lemma Round_monotonic_zero :
+ forall m:mode, x : real. if 0. <=. x then 0. <=. round m x else round m x <=. 0.
+
axiom Round_idempotent :
forall m1 m2:mode, x:real. round m1 (round m2 x) = round m2 x
@@ -1121,6 +1128,7 @@ module Float_interval
F.(andb (F.is_plus_infinity h2) (F.is_minus_infinity l1)))
end
*)
+
let cadd3 (m : F.mode) (i1 i2: t) : t
requires { valid i1 }
requires { valid i2 }
@@ -1135,7 +1143,7 @@ module Float_interval
| True, True -> add_nan m l1 l2; add_nan m h1 h2; Inan
| True, False -> add_nan m l1 l2; Intv (F.Infinity false) (F.Infinity false) true
| False, True -> add_nan m h1 h2; Intv (F.Infinity true) (F.Infinity true) true
- | False, False ->begin
+ | False, False -> begin
add_not_nan m l1 l2;
add_not_nan m h1 h2;
let r =
@@ -1165,5 +1173,54 @@ module Float_interval
end
end
+(*
+ let cmul3 (m : F.mode) (i1 i2: t) : t
+ requires { valid i1 }
+ requires { valid i2 }
+ ensures { forall f1 f2. mem f1 i1 -> mem f2 i2 -> mem F.(mul m f1 f2) result }
+ ensures { valid result } =
+ match i1, i2 with
+ | Inan, _ | _, Inan -> Inan
+ | Intv l1 h1 b1, Intv l2 h2 b2 ->
+ let m1 = F.mul m l1 l2 in
+ let m2 = F.mul m h1 h2 in
+ let m3 = F.mul m l1 h2 in
+ let m4 = F.mul m l2 h1 in
+
+
+ match F.is_nan sum1, F.is_nan sum2, F.is_nan sum3, F.is_nan with
+ | True, True -> add_nan m l1 l2; add_nan m h1 h2; Inan
+ | True, False -> add_nan m l1 l2; Intv (F.Infinity false) (F.Infinity false) true
+ | False, True -> add_nan m h1 h2; Intv (F.Infinity true) (F.Infinity true) true
+ | False, False -> begin
+ add_not_nan m l1 l2;
+ add_not_nan m h1 h2;
+ let r =
+ Intv sum1 sum2 (orb (orb (orb b1 b2)
+ F.(andb (F.is_plus_infinity h1) (F.is_minus_infinity l2)))
+ F.(andb (F.is_plus_infinity h2) (F.is_minus_infinity l1)))
+ in
+ let lemma mem (f1:F.t) (f2:F.t) =
+ requires { mem f1 i1 }
+ requires { mem f2 i2 }
+ ensures { mem (F.add m f1 f2) r }
+ if F.is_nan (F.add m f1 f2) then
+ if F.is_nan f1 then assert { b1 }
+ else if F.is_nan f2 then assert { b2 }
+ else add_nan m f1 f2
+ else begin
+ monotone_add3 m l1 l2 f1 f2;
+ monotone_add3 m f1 f2 h1 h2;
+ end
+ in
+ let lemma valid () =
+ ensures { valid r }
+ monotone_add3 m l1 l2 h1 h2;
+ in
+ r
+ end
+ end
+ end
+*)
end
diff --git a/common/float_interval/why3session.xml b/common/float_interval/why3session.xml
index a5d5080a9..decc07a72 100644
--- a/common/float_interval/why3session.xml
+++ b/common/float_interval/why3session.xml
@@ -8,22 +8,40 @@
<path name=".."/><path name="float_interval.mlw"/>
<theory name="GenericFloat">
<goal name="finite'vc" expl="VC for finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="zero_round" proved="true">
<proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
- <goal name="is_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
- </goal>
- <goal name="round_sign">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.07"/></proof>
- <proof prover="1" obsolete="true"><result status="unknown" time="0.15" steps="41497"/></proof>
- <transf name="introduce_premises" >
- <goal name="round_sign.0">
- <transf name="instantiate" arg1="Round_monotonic" arg2="m,0.,x">
- <goal name="round_sign.0.0">
- <transf name="instantiate" arg1="Round_monotonic" arg2="m,x,0.">
- <goal name="round_sign.0.0.0">
- <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
- <proof prover="1" obsolete="true"><result status="valid" time="0.03" steps="12145"/></proof>
+ <goal name="is_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="Round_monotonic_gen" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="Round_monotonic_gen.0" proved="true">
+ <transf name="cut" proved="true" arg1="(round m x = x)">
+ <goal name="Round_monotonic_gen.0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="Round_monotonic_gen.0.1" expl="asserted formula" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="Round_monotonic_zero" proved="true">
+ <proof prover="0"><result status="valid" time="0.10"/></proof>
+ </goal>
+ <goal name="round_sign" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="round_sign.0" proved="true">
+ <transf name="instantiate" proved="true" arg1="Round_monotonic" arg2="m,0.,x">
+ <goal name="round_sign.0.0" proved="true">
+ <transf name="instantiate" proved="true" arg1="Round_monotonic" arg2="m,x,0.">
+ <goal name="round_sign.0.0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
+ <proof prover="1"><result status="valid" time="0.03" steps="12151"/></proof>
</goal>
</transf>
</goal>
@@ -31,96 +49,94 @@
</goal>
</transf>
</goal>
- <goal name="feq_eq">
- <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
+ <goal name="feq_eq" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
- <goal name="eq_feq">
- <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_feq" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
- <goal name="eq_refl">
- <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_refl" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
- <goal name="eq_sym">
- <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
+ <goal name="eq_sym" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
- <goal name="eq_trans">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="eq_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="eq_zero">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="eq_zero" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="eq_to_real_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.16"/></proof>
+ <goal name="eq_to_real_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.16"/></proof>
</goal>
- <goal name="eq_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
+ <goal name="eq_special" proved="true">
+ <proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
- <goal name="lt_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
+ <goal name="lt_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
- <goal name="le_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ <goal name="le_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
- <goal name="le_trans">
- <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
+ <goal name="le_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
- <goal name="le_lt_trans">
- <proof prover="0" obsolete="true"><path name="float_interval-GenericFloat-le_lt_trans_2.psmt2"/><result status="failure" time="0.00"/></proof>
- <transf name="introduce_premises" >
- <goal name="le_lt_trans.0">
- <proof prover="0" obsolete="true"><path name="float_interval-GenericFloat-le_lt_trans_1.psmt2"/><result status="unknown" time="0.00" steps="0"/></proof>
- <transf name="destruct_term" arg1="x">
- <goal name="le_lt_trans.0.0">
- <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+ <goal name="le_lt_trans" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="le_lt_trans.0" proved="true">
+ <transf name="destruct_term" proved="true" arg1="x">
+ <goal name="le_lt_trans.0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
</goal>
- <goal name="le_lt_trans.0.1">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="le_lt_trans.0.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="le_lt_trans.0.2">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="le_lt_trans.0.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="le_lt_trans.0.3">
- <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+ <goal name="le_lt_trans.0.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="lt_le_trans">
- <proof prover="0" obsolete="true"><result status="valid" time="0.27"/></proof>
+ <goal name="lt_le_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.27"/></proof>
</goal>
- <goal name="le_ge_asym">
- <proof prover="0" obsolete="true"><result status="valid" time="0.15"/></proof>
+ <goal name="le_ge_asym" proved="true">
+ <proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="not_lt_ge">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
</goal>
- <goal name="not_gt_le">
- <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+ <goal name="not_gt_le" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
</goal>
- <goal name="le_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
+ <goal name="le_special" proved="true">
+ <proof prover="0"><result status="valid" time="0.18"/></proof>
</goal>
- <goal name="lt_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.19"/></proof>
+ <goal name="lt_special" proved="true">
+ <proof prover="0"><result status="valid" time="0.19"/></proof>
</goal>
- <goal name="lt_lt_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="lt_lt_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="positive_to_real">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="positive_to_real" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="to_real_positive">
- <proof prover="0" obsolete="true"><result status="valid" time="0.07"/></proof>
+ <goal name="to_real_positive" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
</goal>
- <goal name="negative_to_real">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="negative_to_real" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="to_real_negative">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="to_real_negative" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="diff_sign_trans">
- <proof prover="0" obsolete="true"><result status="valid" time="0.12"/></proof>
+ <goal name="diff_sign_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="diff_sign_product">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
@@ -128,32 +144,32 @@
<goal name="same_sign_product">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="add_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
+ <goal name="add_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.13"/></proof>
</goal>
- <goal name="add_finite_rev">
- <proof prover="0" obsolete="true"><result status="valid" time="0.20"/></proof>
+ <goal name="add_finite_rev" proved="true">
+ <proof prover="0"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="add_finite_rev_n">
- <proof prover="0" obsolete="true"><result status="valid" time="0.42"/></proof>
+ <goal name="add_finite_rev_n" proved="true">
+ <proof prover="0"><result status="valid" time="0.42"/></proof>
</goal>
- <goal name="sub_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.24"/></proof>
+ <goal name="sub_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.24"/></proof>
</goal>
- <goal name="sub_finite_rev">
- <proof prover="0" obsolete="true"><result status="valid" time="0.17"/></proof>
+ <goal name="sub_finite_rev" proved="true">
+ <proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
- <goal name="sub_finite_rev_n">
- <proof prover="0" obsolete="true"><result status="valid" time="0.55"/></proof>
+ <goal name="sub_finite_rev_n" proved="true">
+ <proof prover="0"><result status="valid" time="0.55"/></proof>
</goal>
- <goal name="mul_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.19"/></proof>
+ <goal name="mul_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.19"/></proof>
</goal>
- <goal name="mul_finite_rev">
- <proof prover="0" obsolete="true"><result status="valid" time="0.14"/></proof>
+ <goal name="mul_finite_rev" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
- <goal name="mul_finite_rev_n">
- <proof prover="0" obsolete="true"><result status="valid" time="0.39"/></proof>
+ <goal name="mul_finite_rev_n" proved="true">
+ <proof prover="0"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="div_finite">
<proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
@@ -162,13 +178,13 @@
<proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
</goal>
<goal name="div_finite_rev_n">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
+ <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="neg_finite">
- <proof prover="0" obsolete="true"><result status="valid" time="0.12"/></proof>
+ <goal name="neg_finite" proved="true">
+ <proof prover="0"><result status="valid" time="0.12"/></proof>
</goal>
- <goal name="neg_finite_rev">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="neg_finite_rev" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
<goal name="abs_finite_rev">
<proof prover="0" obsolete="true"><result status="unknown" time="0.12"/></proof>
@@ -191,223 +207,172 @@
<goal name="sqrt_finite_rev">
<proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
</goal>
- <goal name="add_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.45"/></proof>
- <proof prover="1" obsolete="true"><result status="unknown" time="0.24" steps="64795"/></proof>
+ <goal name="add_special" proved="true">
+ <proof prover="0"><result status="valid" time="1.15"/></proof>
</goal>
- <goal name="sub_special">
- <transf name="split_vc" >
- <goal name="sub_special.0">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="sub_special" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="sub_special.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="sub_special.1">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="sub_special.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="sub_special.2">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="sub_special.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="sub_special.3">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="sub_special.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="sub_special.4">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="sub_special.4" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="sub_special.5">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="sub_special.5" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="sub_special.6">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="sub_special.6" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="sub_special.7">
- <proof prover="0" obsolete="true"><result status="valid" time="0.08"/></proof>
+ <goal name="sub_special.7" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
</goal>
- <goal name="sub_special.8">
- <proof prover="0" obsolete="true"><result status="valid" time="0.61"/></proof>
+ <goal name="sub_special.8" proved="true">
+ <proof prover="0"><result status="valid" time="0.84"/></proof>
</goal>
- <goal name="sub_special.9">
- <proof prover="0" obsolete="true"><result status="valid" time="1.16"/></proof>
+ <goal name="sub_special.9" proved="true">
+ <proof prover="0"><result status="valid" time="0.79"/></proof>
</goal>
- <goal name="sub_special.10">
- <proof prover="0" obsolete="true"><result status="valid" time="0.22"/></proof>
+ <goal name="sub_special.10" proved="true">
+ <proof prover="0"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="sub_special.11">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.19"/></proof>
+ <goal name="sub_special.11" proved="true">
+ <proof prover="0"><result status="valid" time="1.43"/></proof>
</goal>
</transf>
</goal>
- <goal name="mul_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.40"/></proof>
+ <goal name="mul_special" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mul_special.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="mul_special.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="mul_special.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
+ </goal>
+ <goal name="mul_special.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="mul_special.4" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="mul_special.5" proved="true">
+ <proof prover="0"><result status="valid" time="0.07"/></proof>
+ </goal>
+ <goal name="mul_special.6" proved="true">
+ <proof prover="0"><result status="valid" time="0.38"/></proof>
+ </goal>
+ <goal name="mul_special.7" proved="true">
+ <transf name="inline_goal" proved="true" >
+ <goal name="mul_special.7.0" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="mul_special.7.0.0" proved="true">
+ <transf name="destruct_term" proved="true" arg1="x">
+ <goal name="mul_special.7.0.0.0" proved="true">
+ <transf name="destruct_term" proved="true" arg1="y">
+ <goal name="mul_special.7.0.0.0.0" proved="true">
+ <transf name="case" proved="true" arg1="(0.0 <. x1)">
+ <goal name="mul_special.7.0.0.0.0.0" expl="true case" proved="true">
+ <proof prover="0"><result status="valid" time="0.58"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.0.0.0.1" expl="false case" proved="true">
+ <proof prover="0"><result status="valid" time="0.57"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mul_special.7.0.0.0.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.0.0.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.0.0.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mul_special.7.0.0.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.0.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.15"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.0.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mul_special.7.0.1" proved="true">
+ <transf name="destruct_term" proved="true" arg1="x">
+ <goal name="mul_special.7.0.1.0" proved="true">
+ <transf name="destruct_term" proved="true" arg1="y">
+ <goal name="mul_special.7.0.1.0.0" proved="true">
+ <transf name="case" proved="true" arg1="(0.0 <. x1)">
+ <goal name="mul_special.7.0.1.0.0.0" expl="true case" proved="true">
+ <proof prover="0"><result status="valid" time="0.39"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.1.0.0.1" expl="false case" proved="true">
+ <transf name="case" proved="true" arg1="(0.0 <. x)">
+ <goal name="mul_special.7.0.1.0.0.1.0" expl="false case (true case)" proved="true">
+ <proof prover="0"><result status="valid" time="0.39"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.1.0.0.1.1" expl="false case" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mul_special.7.0.1.0.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.1.0.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.1.0.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="mul_special.7.0.1.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.12"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.1.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.18"/></proof>
+ </goal>
+ <goal name="mul_special.7.0.1.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.20"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
<goal name="div_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.16"/></proof>
+ <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
</goal>
- <goal name="neg_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.14"/></proof>
+ <goal name="neg_special" proved="true">
+ <proof prover="0"><result status="valid" time="0.14"/></proof>
</goal>
<goal name="abs_special">
<proof prover="0" obsolete="true"><result status="unknown" time="0.14"/></proof>
</goal>
<goal name="fma_special">
- <proof prover="0" obsolete="true"><result status="valid" time="0.23"/></proof>
- <transf name="remove" arg1="zero1,one1,(-'),(>'),(<='),(>='),zero,one,(>),(<=),(>=),(-),(/),(/.),inv,(>=.),(<.),(>.),abs1,sqr,andb,orb,notb,xorb,implb,to_nearest,zeroF,neg,(.-_),(./),sign,classify,le,lt,eq,ge,gt,(.<=),(.<),(.>=),(.>),(.=),is_normal,is_subnormal,is_zero,is_nan,is_finite,is_plus_infinity,is_minus_infinity,is_plus_zero,is_minus_zero,emax,in_int_range,no_overflow,in_safe_int_range,same_sign,product_sign,overflow_value,sign_zero_result,is_RTN,add,(.+),sub,(.-),mul,(.* ),same_sign_real,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Abs_le,Abs_pos,Abs_sum,Abs_prod,triangular_inequality,Zero1,One,Add,Sub,Mul,Neg,Injective,Monotonic,Truncate_int,Truncate_down_pos,Truncate_up_neg,Truncate_monotonic,Truncate_monotonic_int1,Floor_int,Ceil_int,Floor_down,Ceil_up,Floor_monotonic,Ceil_monotonic,Sqrt_positive,Sqrt_square,Square_sqrt,Sqrt_mul,Sqrt_le,Power_0,Power_s,Power_1,Power_sum,pow2pos,pow2_0,pow2_1,pow2_2,pow2_3,pow2_4,pow2_5,pow2_6,pow2_7,pow2_8,pow2_9,pow2_10,pow2_11,pow2_12,pow2_13,pow2_14,pow2_15,pow2_16,pow2_17,pow2_18,pow2_19,pow2_20,pow2_21,pow2_22,pow2_23,pow2_24,pow2_25,pow2_26,pow2_27,pow2_28,pow2_29,pow2_30,pow2_31,pow2_32,pow2_33,pow2_34,pow2_35,pow2_36,pow2_37,pow2_38,pow2_39,pow2_40,pow2_41,pow2_42,pow2_43,pow2_44,pow2_45,pow2_46,pow2_47,pow2_48,pow2_49,pow2_50,pow2_51,pow2_52,pow2_53,pow2_54,pow2_55,pow2_56,pow2_57,pow2_58,pow2_59,pow2_60,pow2_61,pow2_62,pow2_63,pow2_64,eb_gt_1,sb_gt_1,round_to_float,round_float,max_real_not_zero,max_real_round,mk_finite_def,mk_finite_fed,zeroF_is_positive,zeroF_is_zero,zero_to_real,zero_of_int,max_real_bound,max_int,minus_max_real_round,zero_round,Bounded_real_no_overflow,Round_monotonic,Round_idempotent,Round_to_real,Round_down_le,Round_up_ge,Round_down_neg,Round_up_neg,round_sign,pow2sb,Exact_rounding_for_integers,le_trans,abs_finite">
- <goal name="fma_special.0">
- <proof prover="0" timelimit="1" obsolete="true"><path name="float_interval-GenericFloat-fma_special_1.psmt2"/><result status="valid" time="0.09"/></proof>
- <transf name="split_vc" >
- <goal name="fma_special.0.0">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.1">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="fma_special.0.2">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.3">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.03"/></proof>
- </goal>
- <goal name="fma_special.0.4">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.5">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="fma_special.0.6">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.7">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="fma_special.0.8">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.9">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.10">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.11">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="fma_special.0.12">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="fma_special.0.13">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.14">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.15">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.16">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.17">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.18">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.19">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.02"/></proof>
- </goal>
- <goal name="fma_special.0.20">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.06"/></proof>
- </goal>
- <goal name="fma_special.0.21">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.07"/></proof>
- </goal>
- <goal name="fma_special.0.22">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
- </goal>
- <goal name="fma_special.0.23">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.0.24">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.06"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- <transf name="split_vc" >
- <goal name="fma_special.0">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
- </goal>
- <goal name="fma_special.1">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
- </goal>
- <goal name="fma_special.2">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.3">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.4">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
- </goal>
- <goal name="fma_special.5">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.6">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
- </goal>
- <goal name="fma_special.7">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
- </goal>
- <goal name="fma_special.8">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.9">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
- </goal>
- <goal name="fma_special.10">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.11">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.12">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.11"/></proof>
- </goal>
- <goal name="fma_special.13">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.14">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.15">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
- </goal>
- <goal name="fma_special.16">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.17">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
- </goal>
- <goal name="fma_special.18">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.19">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.08"/></proof>
- </goal>
- <goal name="fma_special.20">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="fma_special.21">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- </goal>
- <goal name="fma_special.22">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- <goal name="fma_special.23">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.10"/></proof>
- </goal>
- <goal name="fma_special.24">
- <proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
- </goal>
- </transf>
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.25"/></proof>
</goal>
<goal name="sqrt_special">
<proof prover="0" obsolete="true"><result status="unknown" time="0.09"/></proof>
@@ -434,49 +399,31 @@
<proof prover="0" obsolete="true"><result status="unknown" time="0.14"/></proof>
</goal>
</theory>
-<theory name="Float_interval">
- <goal name="Test2">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
- <transf name="split_vc" >
- <goal name="Test2.0">
- <transf name="instantiate" arg1="is_not_finite" arg2="f1">
- <goal name="Test2.0.0">
- <proof prover="0"><result status="valid" time="0.05"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="Test">
- <proof prover="0" obsolete="true"><result status="valid" time="0.17"/></proof>
- <transf name="split_vc" >
- <goal name="Test.0">
- <transf name="instantiate" arg1="add_special" arg2="m, f1, f2">
- <goal name="Test.0.0">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- </goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="G1">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
- <transf name="split_vc" >
- <goal name="G1.0">
- <transf name="unfold" arg1="is_plus_infinity" arg2="in" arg3="H">
- <goal name="G1.0.0">
- <transf name="destruct_term" arg1="f">
- <goal name="G1.0.0.0">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+<theory name="Float_interval" proved="true">
+ <goal name="Test2" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="Test" proved="true">
+ <proof prover="0"><result status="valid" time="0.17"/></proof>
+ </goal>
+ <goal name="G1" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="G1.0" proved="true">
+ <transf name="unfold" proved="true" arg1="is_plus_infinity" arg2="in" arg3="H">
+ <goal name="G1.0.0" proved="true">
+ <transf name="destruct_term" proved="true" arg1="f">
+ <goal name="G1.0.0.0" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="G1.0.0.1">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+ <goal name="G1.0.0.1" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="G1.0.0.2">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="G1.0.0.2" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="G1.0.0.3">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="G1.0.0.3" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
@@ -484,413 +431,265 @@
</goal>
</transf>
</goal>
- <goal name="monotone_add'vc" expl="VC for monotone_add">
- <proof prover="0" obsolete="true"><result status="valid" time="3.16"/></proof>
- <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="529404"/></proof>
- </goal>
- <goal name="monotone_add2'vc" expl="VC for monotone_add2">
- <proof prover="0" obsolete="true"><result status="valid" time="3.05"/></proof>
- <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="619003"/></proof>
- <transf name="remove" arg1="zero,one,(-),(>),(<=),(>=),zero1,one1,(>'),(<='),(>='),(-'),(/),(>=.),(<.),(>.),abs1,sqr,andb,orb,notb,xorb,implb,to_nearest,zeroF,in_int_range,in_safe_int_range,same_sign,product_sign,overflow_value,sign_zero_result,is_RTN,add,(.+),same_sign_real,valid,mem,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Abs_le,Abs_pos,Abs_sum,Abs_prod,triangular_inequality,Zero1,One,Add,Sub,Mul,Neg,Injective,Monotonic,Truncate_int,Truncate_down_pos,Truncate_up_neg,Real_of_truncate,Truncate_monotonic,Truncate_monotonic_int1,Truncate_monotonic_int2,Floor_int,Ceil_int,Floor_down,Ceil_up,Ceil_monotonic,Sqrt_positive,Sqrt_square,Square_sqrt,Sqrt_mul,Sqrt_le,Power_0,Power_s,Power_1,Power_sum,pow2pos,pow2_0,pow2_1,pow2_2,pow2_3,pow2_4,pow2_5,pow2_6,pow2_7,pow2_8,pow2_9,pow2_10,pow2_11,pow2_12,pow2_13,pow2_14,pow2_15,pow2_16,pow2_17,pow2_18,pow2_19,pow2_20,pow2_21,pow2_22,pow2_23,pow2_24,pow2_25,pow2_26,pow2_27,pow2_28,pow2_29,pow2_30,pow2_31,pow2_32,pow2_33,pow2_34,pow2_35,pow2_36,pow2_37,pow2_38,pow2_39,pow2_40,pow2_41,pow2_42,pow2_43,pow2_44,pow2_45,pow2_46,pow2_47,pow2_48,pow2_49,pow2_50,pow2_51,pow2_52,pow2_53,pow2_54,pow2_55,pow2_56,pow2_57,pow2_58,pow2_59,pow2_60,pow2_61,pow2_62,pow2_63,pow2_64,eb_gt_1,sb_gt_1,round_to_float,round_float,max_real_not_zero,max_real_round,finite'invariant,mk_finite_def,mk_finite_fed,Round_idempotent,Round_to_real,Round_down_le,Round_up_ge,Round_down_neg,Round_up_neg,round_sign,pow2sb,Exact_rounding_for_integers,le_trans,sub_finite,mul_finite,div_finite,neg_finite,abs_finite,abs_universal,fma_finite,sqrt_finite,sub_special,mul_special,div_special,neg_special,abs_special,fma_special,sqrt_special,of_int_add_exact,of_int_sub_exact,of_int_mul_exact,zeroF_is_int,of_int_is_int,big_float_is_int,roundToIntegral_is_int,eq_is_int,add_int,sub_int,mul_int,fma_int,neg_int,abs_int,is_int_of_int,is_int_to_int,is_int_is_finite,int_to_real,truncate_int,truncate_neg,truncate_pos,ceil_le,ceil_lest,ceil_to_int,floor_le,floor_lest,floor_to_int,RNA_down,RNA_up,RNA_down_tie,RNA_up_tie,to_int_roundToIntegral,to_int_monotonic,to_int_of_int,eq_to_int,neg_to_int,roundToIntegral_is_finite,Test2,Test">
- <goal name="monotone_add2'vc.0" expl="VC for monotone_add2">
- <proof prover="0" timelimit="1" obsolete="true"><path name="float_interval-Float_interval-monotone_add2qtvc_1.psmt2"/><undone/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="le_trans'vc" expl="VC for le_trans">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="monotone_add3'vc" expl="VC for monotone_add3">
- <proof prover="0" timelimit="100" obsolete="true"><result status="valid" time="5.72"/></proof>
- <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="555896"/></proof>
- <transf name="remove" arg1="zero,one,(-),(>),(<=),(>=),zero1,one1,(>'),(<='),(>='),(-'),(/),(+.),(/.),(-._),abs1,andb,orb,notb,xorb,implb,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Abs_le,Abs_pos,Abs_sum,Abs_prod,triangular_inequality,Zero1,One,Add,Sub,Mul,Neg,Injective,Monotonic,Truncate_int,Truncate_down_pos,Truncate_up_neg,Truncate_monotonic_int2,Floor_int,Power_1,pow2_19,pow2_20,pow2_21,pow2_22,pow2_23,pow2_24,pow2_25,pow2_26,pow2_27,pow2_28,pow2_29,pow2_30,pow2_31,pow2_32,pow2_33,pow2_34,pow2_35,pow2_36,pow2_37,pow2_38,pow2_39,pow2_40,pow2_41,pow2_42,pow2_43,pow2_44,pow2_45,pow2_46,pow2_47,pow2_48,pow2_49,pow2_50,pow2_51,pow2_52,pow2_53,pow2_54,pow2_55,pow2_56,pow2_57,pow2_58,pow2_59,pow2_60,pow2_61,pow2_62,pow2_63,pow2_64">
- <goal name="monotone_add3'vc.0" expl="VC for monotone_add3">
- <proof prover="0" timelimit="19" obsolete="true"><undone/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="cadd'vc" expl="VC for cadd">
- <transf name="split_vc" >
- <goal name="cadd'vc.0" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.68"/></proof>
- </goal>
- <goal name="cadd'vc.1" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="3.30"/></proof>
- </goal>
- <goal name="cadd'vc.2" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="1.98"/></proof>
- </goal>
- <goal name="cadd'vc.3" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
- </goal>
- <goal name="cadd'vc.4" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.68"/></proof>
- </goal>
- <goal name="cadd'vc.5" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.18"/></proof>
- </goal>
- <goal name="cadd'vc.6" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.42"/></proof>
- </goal>
- <goal name="cadd'vc.7" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="cadd'vc.8" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.74"/></proof>
- </goal>
- <goal name="cadd'vc.9" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.61"/></proof>
- </goal>
- <goal name="cadd'vc.10" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.20"/></proof>
- </goal>
- <goal name="cadd'vc.11" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
- </goal>
- <goal name="cadd'vc.12" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.46"/></proof>
- </goal>
- <goal name="cadd'vc.13" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="0.68"/></proof>
- </goal>
- <goal name="cadd'vc.14" expl="assertion">
- <proof prover="0" obsolete="true"><result status="valid" time="2.28"/></proof>
- </goal>
- <goal name="cadd'vc.15" expl="postcondition">
- <transf name="split_vc" >
- <goal name="cadd'vc.15.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
+ <goal name="monotone_add'vc" expl="VC for monotone_add" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="monotone_add'vc.0" expl="VC for monotone_add" proved="true">
+ <transf name="destruct_term" proved="true" arg1="f1">
+ <goal name="monotone_add'vc.0.0" expl="VC for monotone_add" proved="true">
+ <proof prover="0" timelimit="20"><result status="valid" time="10.40"/></proof>
</goal>
- <goal name="cadd'vc.15.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ <goal name="monotone_add'vc.0.1" expl="VC for monotone_add" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
</goal>
- <goal name="cadd'vc.15.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="monotone_add'vc.0.2" expl="VC for monotone_add" proved="true">
+ <proof prover="0"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="cadd'vc.15.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd'vc.15.3.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.33"/></proof>
+ <goal name="monotone_add'vc.0.3" expl="VC for monotone_add" proved="true">
+ <proof prover="0"><result status="valid" time="0.85"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="le_trans'vc" expl="VC for le_trans" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc" expl="VC for monotone_add3" proved="true">
+ <transf name="introduce_premises" proved="true" >
+ <goal name="monotone_add3'vc.0" expl="VC for monotone_add3" proved="true">
+ <transf name="destruct_term" proved="true" arg1="l1">
+ <goal name="monotone_add3'vc.0.0" expl="VC for monotone_add3" proved="true">
+ <transf name="destruct_term" proved="true" arg1="l2">
+ <goal name="monotone_add3'vc.0.0.0" expl="VC for monotone_add3" proved="true">
+ <transf name="destruct_term" proved="true" arg1="h1">
+ <goal name="monotone_add3'vc.0.0.0.0" expl="VC for monotone_add3" proved="true">
+ <transf name="destruct_term" proved="true" arg1="h2">
+ <goal name="monotone_add3'vc.0.0.0.0.0" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="2.99"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.0.0.0.1" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.0.0.0.2" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.0.0.0.3" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="1.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="monotone_add3'vc.0.0.0.1" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.0.0.2" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.19"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.0.0.3" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="2.67"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="cadd'vc.15.3.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="1.60"/></proof>
+ <goal name="monotone_add3'vc.0.0.1" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
- <goal name="cadd'vc.15.3.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <proof prover="1" obsolete="true"><result status="timeout" time="5.00" steps="525585"/></proof>
+ <goal name="monotone_add3'vc.0.0.2" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.17"/></proof>
</goal>
- <goal name="cadd'vc.15.3.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <goal name="monotone_add3'vc.0.0.3" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.76"/></proof>
</goal>
</transf>
</goal>
+ <goal name="monotone_add3'vc.0.1" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.13"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.2" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="0.41"/></proof>
+ </goal>
+ <goal name="monotone_add3'vc.0.3" expl="VC for monotone_add3" proved="true">
+ <proof prover="0"><result status="valid" time="3.13"/></proof>
+ </goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="add_nan'vc" expl="VC for add_nan">
- <proof prover="0" obsolete="true"><result status="valid" time="0.11"/></proof>
+ <goal name="add_nan'vc" expl="VC for add_nan" proved="true">
+ <proof prover="0"><result status="valid" time="0.11"/></proof>
</goal>
- <goal name="add_not_nan'vc" expl="VC for add_not_nan">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ <goal name="add_not_nan'vc" expl="VC for add_not_nan" proved="true">
+ <proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
- <goal name="add_not_nan">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
+ <goal name="add_not_nan" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
- <goal name="cadd2'vc" expl="VC for cadd2">
- <proof prover="0" timelimit="100" obsolete="true"><result status="timeout" time="177.00"/></proof>
- <transf name="remove" arg1="zero,one,(-),(>),(<=),(>=),zero1,one1,(>'),(<='),(>='),(-'),(/),( *.),(<=.),andb,orb,notb,xorb,implb,Assoc1,Unit_def_l,Unit_def_r,Inv_def_l,Inv_def_r,Comm1,Assoc,Mul_distr_l,Mul_distr_r,Comm,Unitary,NonTrivialRing,Refl,Trans,Antisymm,Total,ZeroLessOne,CompatOrderAdd,CompatOrderMult,Assoc3,Unit_def_l1,Unit_def_r1,Inv_def_l1,Inv_def_r1,Comm3,Assoc2,Mul_distr_l1,Mul_distr_r1,Comm2,Unitary1,NonTrivialRing1,Inverse,add_div,sub_div,neg_div,assoc_mul_div,assoc_div_mul,assoc_div_div,Refl1,Trans1,Antisymm1,Total1,ZeroLessOne1,CompatOrderAdd1,CompatOrderMult1,Power_0,Power_s,Power_1,Power_sum,pow2_0,pow2_2,pow2_4,pow2_5,pow2_6">
- <goal name="cadd2'vc.0" expl="VC for cadd2">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
+ <goal name="cadd3'vc" expl="VC for cadd3" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.0" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- </transf>
- <transf name="split_vc" >
- <goal name="cadd2'vc.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd2'vc.0.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.13"/></proof>
- </goal>
- <goal name="cadd2'vc.0.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
- </goal>
- <goal name="cadd2'vc.0.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
- </goal>
- <goal name="cadd2'vc.0.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="cadd2'vc.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd2'vc.1.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="cadd2'vc.1.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="cadd2'vc.1.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="cadd2'vc.1.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- </goal>
- </transf>
+ <goal name="cadd3'vc.1" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- </transf>
- </goal>
- <goal name="cadd3'vc" expl="VC for cadd3">
- <proof prover="0" timelimit="100" obsolete="true"><result status="timeout" time="100.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.0" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+ <goal name="cadd3'vc.2" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.1" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+ <goal name="cadd3'vc.3" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.2" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.4" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.3" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.5" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="cadd3'vc.4" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.6" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="cadd3'vc.5" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+ <goal name="cadd3'vc.7" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.6" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+ <goal name="cadd3'vc.8" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
- <goal name="cadd3'vc.7" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.9" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.8" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
+ <goal name="cadd3'vc.10" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.9" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.11" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
- <goal name="cadd3'vc.10" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.12" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.11" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
+ <goal name="cadd3'vc.13" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.12" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.14" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="cadd3'vc.13" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.15" expl="assertion" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.14" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.66"/></proof>
+ <goal name="cadd3'vc.16" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="cadd3'vc.15" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.58"/></proof>
+ <goal name="cadd3'vc.17" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="cadd3'vc.16" expl="precondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.16.0" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.18" expl="precondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.18.0" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
- <goal name="cadd3'vc.17" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.19" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.18" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.04"/></proof>
+ <goal name="cadd3'vc.20" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
- <goal name="cadd3'vc.19" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.19"/></proof>
+ <goal name="cadd3'vc.21" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.19"/></proof>
</goal>
- <goal name="cadd3'vc.20" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.17"/></proof>
+ <goal name="cadd3'vc.22" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.29"/></proof>
</goal>
- <goal name="cadd3'vc.21" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.23" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.22" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.24" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.23" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.32"/></proof>
+ <goal name="cadd3'vc.25" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.32"/></proof>
</goal>
- <goal name="cadd3'vc.24" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.27"/></proof>
+ <goal name="cadd3'vc.26" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.27"/></proof>
</goal>
- <goal name="cadd3'vc.25" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="instantiate" arg1="le_trans" arg2="(add m x2 x5)">
- <goal name="cadd3'vc.25.0" expl="postcondition">
- <transf name="instantiate" arg1="Hinst" arg2="(add m x2 f2)">
- <goal name="cadd3'vc.25.0.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.53"/></proof>
+ <goal name="cadd3'vc.27" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="le_trans" arg2="(add m x2 x5)">
+ <goal name="cadd3'vc.27.0" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Hinst" arg2="(add m x2 f2)">
+ <goal name="cadd3'vc.27.0.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.53"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="cadd3'vc.26" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.28" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.27" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.29" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.28" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.30" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.29" expl="precondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.31" expl="precondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.30" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.06"/></proof>
+ <goal name="cadd3'vc.32" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.06"/></proof>
</goal>
- <goal name="cadd3'vc.31" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="10.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.31.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ <goal name="cadd3'vc.33" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.33.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
- <goal name="cadd3'vc.31.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.31.1.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.09"/></proof>
- </goal>
- <goal name="cadd3'vc.31.3.0" expl="postcondition">
- <proof prover="0"><result status="valid" time="2.73"/></proof>
- </goal>
- <goal name="cadd3'vc.31.3.1" expl="postcondition">
- <proof prover="0"><result status="valid" time="4.04"/></proof>
- </goal>
- <goal name="cadd3'vc.31.3.2" expl="postcondition">
- <proof prover="0"><result status="timeout" time="5.00"/></proof>
+ <goal name="cadd3'vc.33.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.33.1.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.09"/></proof>
</goal>
</transf>
</goal>
- <goal name="cadd3'vc.31.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.05"/></proof>
+ <goal name="cadd3'vc.33.2" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="cadd3'vc.31.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.31.3.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.35"/></proof>
+ <goal name="cadd3'vc.33.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.33.3.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.35"/></proof>
</goal>
- <goal name="cadd3'vc.31.3.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.56"/></proof>
+ <goal name="cadd3'vc.33.3.1" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.56"/></proof>
</goal>
- <goal name="cadd3'vc.31.3.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="2.37"/></proof>
+ <goal name="cadd3'vc.33.3.2" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="3.19"/></proof>
</goal>
- <goal name="cadd3'vc.31.3.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.10"/></proof>
+ <goal name="cadd3'vc.33.3.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.10"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="cadd3'vc.32" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.32.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.34" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.34.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.32.1" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.32.1.0" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
- </goal>
- <goal name="cadd3'vc.32.3.2" expl="postcondition">
- <proof prover="0"><result status="valid" time="0.08"/></proof>
- </goal>
- <goal name="cadd3'vc.32.3.0" expl="postcondition">
- <proof prover="0"><result status="valid" time="0.04"/></proof>
- </goal>
- <goal name="cadd3'vc.32.3.1" expl="postcondition">
- <proof prover="0"><result status="valid" time="0.19"/></proof>
+ <goal name="cadd3'vc.34.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="cadd3'vc.34.1.0" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
- <goal name="cadd3'vc.32.2" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.03"/></proof>
+ <goal name="cadd3'vc.34.2" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="cadd3'vc.32.3" expl="postcondition">
- <proof prover="0" obsolete="true"><result status="valid" time="0.15"/></proof>
+ <goal name="cadd3'vc.34.3" expl="postcondition" proved="true">
+ <proof prover="0"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
- <goal name="cadd3'vc.25" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.39" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.22" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.41" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.33" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.35" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.42" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.18" expl="precondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.18.0" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.19.1" expl="postcondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.19.2" expl="postcondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.19.3" expl="postcondition">
- <proof prover="0"><undone/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="cadd3'vc.26" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.24" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.32" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- <goal name="cadd3'vc.30" expl="precondition">
- <proof prover="0" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="cadd3'vc.30.0" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="cadd3'vc.17" expl="precondition">
- <proof prover="0"><undone/></proof>
- </goal>
</transf>
</goal>
- <goal name="G2">
- <proof prover="0"><undone/></proof>
- </goal>
</theory>
</file>
</why3session>
--
GitLab