Commit 00b674fa authored by Sylvain Dailler's avatar Sylvain Dailler

Update shapes and sessions

parent f2886c41
......@@ -561,7 +561,7 @@
<transf name="introduce_premises" proved="true" >
<goal name="distrib_conj.0.2.0" proved="true">
<transf name="assert" proved="true" arg1="(valid_fmla (Fimplies (Fand (wp x p) (wp x q)) (wp x (Fand p q))))">
<goal name="distrib_conj.0.2.0.0" proved="true">
<goal name="distrib_conj.0.2.0.0" expl="asserted formula" proved="true">
<proof prover="7"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="distrib_conj.0.2.0.1" proved="true">
......
......@@ -315,12 +315,12 @@
</goal>
</transf>
</goal>
<goal name="var_value0.0.0.0.1" proved="true">
<goal name="var_value0.0.0.0.1" expl="rewrite premises" proved="true">
<proof prover="11"><result status="valid" time="0.06"/></proof>
</goal>
</transf>
</goal>
<goal name="var_value0.0.0.1" proved="true">
<goal name="var_value0.0.0.1" expl="rewrite premises" proved="true">
<proof prover="11"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
......
......@@ -34,7 +34,7 @@
</goal>
</transf>
</goal>
<goal name="Power_sum.0.1.1" proved="true">
<goal name="Power_sum.0.1.1" expl="equality hypothesis" proved="true">
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
......@@ -55,7 +55,7 @@
<goal name="pow2pos.0.1.0" expl="recursive case" proved="true">
<proof prover="7" timelimit="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="pow2pos.0.1.1" proved="true">
<goal name="pow2pos.0.1.1" expl="equality hypothesis" proved="true">
<proof prover="5"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
......@@ -482,17 +482,17 @@
<goal name="Mod_pow2_gen.0.0.0.0" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Mod_pow2_gen.0.0.0.1" proved="true">
<goal name="Mod_pow2_gen.0.0.0.1" expl="equality hypothesis" proved="true">
<proof prover="5"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="Mod_pow2_gen.0.0.1" proved="true">
<goal name="Mod_pow2_gen.0.0.1" expl="rewrite premises" proved="true">
<proof prover="5"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
</goal>
<goal name="Mod_pow2_gen.0.1" proved="true">
<goal name="Mod_pow2_gen.0.1" expl="equality hypothesis" proved="true">
<proof prover="5"><result status="valid" time="0.07"/></proof>
</goal>
</transf>
......@@ -595,7 +595,7 @@
<goal name="Pow2_int_real.0.1.0" expl="recursive case" proved="true">
<proof prover="7" timelimit="1"><result status="valid" time="0.12" steps="135"/></proof>
</goal>
<goal name="Pow2_int_real.0.1.1" proved="true">
<goal name="Pow2_int_real.0.1.1" expl="equality hypothesis" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......
......@@ -192,7 +192,7 @@
<goal name="VC shortest_path_code.17.0.0" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC shortest_path_code.17.0.1" proved="true">
<goal name="VC shortest_path_code.17.0.1" expl="asserted formula" proved="true">
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......
......@@ -56,7 +56,7 @@
<transf name="introduce_premises" proved="true" >
<goal name="VC two_equal_elements.14.0.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(forall i1 j:int. 0 &lt;= i1 /\ i1 &lt; (i + 1) /\ 0 &lt;= j /\ j &lt; (i + 1) /\ i1 &lt;&gt; j -&gt; a[i1] &lt;&gt; v \/ a[j] &lt;&gt; v)">
<goal name="VC two_equal_elements.14.0.0.0" proved="true">
<goal name="VC two_equal_elements.14.0.0.0" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC two_equal_elements.14.0.0.1" expl="loop invariant preservation" proved="true">
......@@ -111,7 +111,7 @@
<transf name="introduce_premises" proved="true" >
<goal name="VC two_equal_elements.26.0.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(forall i1 j:int. 0 &lt;= i1 /\ i1 &lt; (i + 1) /\ 0 &lt;= j /\ j &lt; (i + 1) /\ i1 &lt;&gt; j -&gt; a[i1] &lt;&gt; v \/ a[j] &lt;&gt; v)">
<goal name="VC two_equal_elements.26.0.0.0" proved="true">
<goal name="VC two_equal_elements.26.0.0.0" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC two_equal_elements.26.0.0.1" expl="loop invariant preservation" proved="true">
......@@ -144,7 +144,7 @@
<transf name="introduce_premises" proved="true" >
<goal name="VC two_equal_elements.32.0.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(forall i1 j:int. 0 &lt;= i1 /\ i1 &lt; (i + 1) /\ 0 &lt;= j /\ j &lt; (i + 1) /\ i1 &lt;&gt; j -&gt; a[i1] &lt;&gt; v \/ a[j] &lt;&gt; v)">
<goal name="VC two_equal_elements.32.0.0.0" proved="true">
<goal name="VC two_equal_elements.32.0.0.0" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="VC two_equal_elements.32.0.0.1" expl="loop invariant preservation" proved="true">
......
......@@ -56,7 +56,7 @@
</goal>
<goal name="VC unique.11.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(mem x a (i+1) &lt;-&gt; mem x a i)">
<goal name="VC unique.11.1.0" proved="true">
<goal name="VC unique.11.1.0" expl="asserted formula" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.11.1.1" expl="false case (loop invariant preservation)" proved="true">
......@@ -73,7 +73,7 @@
</goal>
<goal name="VC unique.12.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(not (mem a[i1] a i1))">
<goal name="VC unique.12.1.0" proved="true">
<goal name="VC unique.12.1.0" expl="asserted formula" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC unique.12.1.1" expl="false case (loop invariant preservation)" proved="true">
......@@ -96,7 +96,7 @@
</goal>
<goal name="VC unique.15.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(mem x a (i+1) &lt;-&gt; mem x a i)">
<goal name="VC unique.15.1.0" proved="true">
<goal name="VC unique.15.1.0" expl="asserted formula" proved="true">
<proof prover="0"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC unique.15.1.1" expl="false case (loop invariant preservation)" proved="true">
......
This diff is collapsed.
......@@ -306,17 +306,17 @@
<transf name="destruct" proved="true" arg1="H">
<goal name="VC list_seg_sublistl.6.0.0" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(l1 = empty)">
<goal name="VC list_seg_sublistl.6.0.0.0" proved="true">
<goal name="VC list_seg_sublistl.6.0.0.0" expl="asserted formula" proved="true">
<proof prover="0"><result status="valid" time="2.07"/></proof>
</goal>
<goal name="VC list_seg_sublistl.6.0.0.1" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(forall l:seq &#39;a. empty ++ l = l)">
<goal name="VC list_seg_sublistl.6.0.0.1.0" proved="true">
<goal name="VC list_seg_sublistl.6.0.0.1.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(forall l:seq &#39;a. empty ++ l == l)">
<goal name="VC list_seg_sublistl.6.0.0.1.0.0" proved="true">
<goal name="VC list_seg_sublistl.6.0.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
<goal name="VC list_seg_sublistl.6.0.0.1.0.1" proved="true">
<goal name="VC list_seg_sublistl.6.0.0.1.0.1" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
......
......@@ -193,12 +193,12 @@
</goal>
<goal name="VC mex.28" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(mem x a)">
<goal name="VC mex.28.0" proved="true">
<goal name="VC mex.28.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(a[x] = x)">
<goal name="VC mex.28.0.0" proved="true">
<goal name="VC mex.28.0.0" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC mex.28.0.1" proved="true">
<goal name="VC mex.28.0.1" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -219,12 +219,12 @@
</goal>
<goal name="VC mex.32" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="(mem x a)">
<goal name="VC mex.32.0" proved="true">
<goal name="VC mex.32.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(a[x] = x)">
<goal name="VC mex.32.0.0" proved="true">
<goal name="VC mex.32.0.0" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC mex.32.0.1" proved="true">
<goal name="VC mex.32.0.1" expl="asserted formula" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
......
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
......@@ -75,13 +75,13 @@
<proof prover="1"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC wmpn_copyi.22" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="213"/></proof>
<proof prover="0"><result status="valid" time="0.06" steps="204"/></proof>
</goal>
<goal name="VC wmpn_copyi.23" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_copyi.24" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="101"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="97"/></proof>
</goal>
<goal name="VC wmpn_copyi.25" expl="loop invariant preservation" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......@@ -102,7 +102,7 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_copyi.31" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="108"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="105"/></proof>
</goal>
<goal name="VC wmpn_copyi.32" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -133,10 +133,10 @@
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC wmpn_zero_p.6" expl="assertion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="VC wmpn_zero_p.7" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC wmpn_zero_p.8" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
......@@ -151,7 +151,7 @@
<proof prover="1"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC wmpn_zero_p.12" expl="postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="84"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="80"/></proof>
</goal>
<goal name="VC wmpn_zero_p.13" expl="assertion" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
......@@ -212,10 +212,10 @@
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC wmpn_zero.11" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="110"/></proof>
<proof prover="0"><result status="valid" time="0.10" steps="105"/></proof>
</goal>
<goal name="VC wmpn_zero.12" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="51"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="50"/></proof>
</goal>
<goal name="VC wmpn_zero.13" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.03"/></proof>
......
......@@ -214,13 +214,13 @@
</goal>
<goal name="VC valuation_times_nondiv.6.1" expl="assertion" proved="true">
<transf name="apply" proved="true" arg1="valuation_mul">
<goal name="VC valuation_times_nondiv.6.1.0" proved="true">
<goal name="VC valuation_times_nondiv.6.1.0" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6.1.1" proved="true">
<goal name="VC valuation_times_nondiv.6.1.1" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC valuation_times_nondiv.6.1.2" proved="true">
<goal name="VC valuation_times_nondiv.6.1.2" expl="apply premises" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
</transf>
......@@ -254,19 +254,19 @@
</goal>
<goal name="valuation_prod.4" proved="true">
<transf name="apply" proved="true" arg1="valuation_zero_prod">
<goal name="valuation_prod.4.0" proved="true">
<goal name="valuation_prod.4.0" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="valuation_prod.4.1" proved="true">
<goal name="valuation_prod.4.1" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="valuation_prod.4.2" proved="true">
<goal name="valuation_prod.4.2" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="valuation_prod.4.3" proved="true">
<goal name="valuation_prod.4.3" expl="apply premises" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
<goal name="valuation_prod.4.4" proved="true">
<goal name="valuation_prod.4.4" expl="apply premises" proved="true">
<proof prover="5"><result status="valid" time="0.02" steps="22"/></proof>
</goal>
</transf>
......@@ -279,10 +279,10 @@
<goal name="valuation_prod.6.0" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="valuation_prod.6.1" proved="true">
<goal name="valuation_prod.6.1" expl="rewrite premises" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="valuation_prod.6.2" proved="true">
<goal name="valuation_prod.6.2" expl="rewrite premises" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -301,18 +301,18 @@
</goal>
<goal name="valuation_prod.11" proved="true">
<transf name="apply" proved="true" arg1="valuation_times_nondiv">
<goal name="valuation_prod.11.0" proved="true">
<goal name="valuation_prod.11.0" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="valuation_prod.11.1" proved="true">
<goal name="valuation_prod.11.1" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="valuation_prod.11.2" proved="true">
<goal name="valuation_prod.11.2" expl="apply premises" proved="true">
<transf name="split_vc" proved="true" >
<goal name="valuation_prod.11.2.0" proved="true">
<goal name="valuation_prod.11.2.0" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="valuation_prod.11.2.1" proved="true">
<goal name="valuation_prod.11.2.1" expl="apply premises" proved="true">
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......
......@@ -432,19 +432,19 @@
<transf name="unfold" proved="true" arg1="permut" arg2="in" arg3="H">
<goal name="Permut_length.0.1.0" proved="true">
<transf name="assert" proved="true" arg1="(num_occ x1 l1 &gt;= 1)">
<goal name="Permut_length.0.1.0.0" proved="true">
<goal name="Permut_length.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Permut_length.0.1.0.1" proved="true">
<transf name="assert" proved="true" arg1="(mem x1 l2)">
<goal name="Permut_length.0.1.0.1.0" proved="true">
<goal name="Permut_length.0.1.0.1.0" expl="asserted formula" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Permut_length.0.1.0.1.1" proved="true">
<transf name="instantiate" proved="true" arg1="mem_decomp" arg2="x1,l2">
<goal name="Permut_length.0.1.0.1.1.0" proved="true">
<transf name="destruct" proved="true" arg1="Hinst">
<goal name="Permut_length.0.1.0.1.1.0.0" proved="true">
<goal name="Permut_length.0.1.0.1.1.0.0" expl="destruct premise" proved="true">
<proof prover="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Permut_length.0.1.0.1.1.0.1" proved="true">
......@@ -453,7 +453,7 @@
<transf name="destruct" proved="true" arg1="Hinst">
<goal name="Permut_length.0.1.0.1.1.0.1.0.0" proved="true">
<transf name="assert" proved="true" arg1="(permut x (l1 ++ l2))">
<goal name="Permut_length.0.1.0.1.1.0.1.0.0.0" proved="true">
<goal name="Permut_length.0.1.0.1.1.0.1.0.0.0" expl="asserted formula" proved="true">
<proof prover="5"><result status="valid" time="0.22"/></proof>
</goal>
<goal name="Permut_length.0.1.0.1.1.0.1.0.0.1" proved="true">
......
......@@ -75,7 +75,7 @@
</goal>
<goal name="pigeon_0.0.0.1" proved="true">
<transf name="assert" proved="true" arg1="(mem x1 empty)">
<goal name="pigeon_0.0.0.1.0" proved="true">
<goal name="pigeon_0.0.0.1.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="pigeon_0.0.0.1.1" proved="true">
......
......@@ -14,16 +14,16 @@
<transf name="introduce_premises" proved="true" >
<goal name="sum_right.0" proved="true">
<transf name="assert" proved="true" arg1="(forall x. 0 &lt; x &lt; j -&gt; sum a (j-x) j = sum a (j-x) (j-1) + a[j-1])">
<goal name="sum_right.0.0" proved="true">
<goal name="sum_right.0.0" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="sum_right.0.0.0" proved="true">
<goal name="sum_right.0.0.0" expl="asserted formula" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_right.0.0.0.0" expl="base case" proved="true">
<goal name="sum_right.0.0.0.0" expl="base case (asserted formula)" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="sum_right.0.0.0.1" expl="recursive case" proved="true">
<goal name="sum_right.0.0.0.1" expl="recursive case (asserted formula)" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_right.0.0.0.1.0" expl="recursive case" proved="true">
<goal name="sum_right.0.0.0.1.0" expl="recursive case (asserted formula)" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -88,16 +88,16 @@
<transf name="introduce_premises" proved="true" >
<goal name="sum_frame.0" proved="true">
<transf name="assert" proved="true" arg1="(forall x. 0 &lt;= x &lt;= j-i -&gt; sum a1 (j-x) j = sum a2 (j-x) j)">
<goal name="sum_frame.0.0" proved="true">
<goal name="sum_frame.0.0" expl="asserted formula" proved="true">
<transf name="introduce_premises" proved="true" >
<goal name="sum_frame.0.0.0" proved="true">
<goal name="sum_frame.0.0.0" expl="asserted formula" proved="true">
<transf name="induction" proved="true" arg1="x">
<goal name="sum_frame.0.0.0.0" expl="base case" proved="true">
<goal name="sum_frame.0.0.0.0" expl="base case (asserted formula)" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="sum_frame.0.0.0.1" expl="recursive case" proved="true">
<goal name="sum_frame.0.0.0.1" expl="recursive case (asserted formula)" proved="true">
<transf name="instantiate" proved="true" arg1="Hrec" arg2="(x - 1)">
<goal name="sum_frame.0.0.0.1.0" expl="recursive case" proved="true">
<goal name="sum_frame.0.0.0.1.0" expl="recursive case (asserted formula)" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......
......@@ -82,7 +82,7 @@
</goal>
<goal name="VC equality.6" expl="precondition" proved="true">
<transf name="assert" proved="true" arg1="((k-1)*lambda &gt;= 0)">
<goal name="VC equality.6.0" proved="true">
<goal name="VC equality.6.0" expl="asserted formula" proved="true">
<proof prover="7"><result status="valid" time="2.45"/></proof>
</goal>
<goal name="VC equality.6.1" expl="precondition" proved="true">
......@@ -139,7 +139,7 @@
</goal>
<goal name="VC equality.20.2" expl="postcondition" proved="true">
<transf name="assert" proved="true" arg1="((k-1) * lambda &gt;= 0)">
<goal name="VC equality.20.2.0" proved="true">
<goal name="VC equality.20.2.0" expl="asserted formula" proved="true">
<proof prover="7"><result status="valid" time="4.35"/></proof>
</goal>
<goal name="VC equality.20.2.1" expl="postcondition" proved="true">
......@@ -214,7 +214,7 @@
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.10.0.1" proved="true">
<goal name="VC tortoise_and_hare.10.0.1" expl="equality hypothesis" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
</transf>
......@@ -247,31 +247,31 @@
</goal>
<goal name="VC tortoise_and_hare.19" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(lam1 = 0)">
<goal name="VC tortoise_and_hare.19.0" proved="true">
<goal name="VC tortoise_and_hare.19.0" expl="asserted formula" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(x (n + i1) = x n)">
<goal name="VC tortoise_and_hare.19.1.0" proved="true">
<goal name="VC tortoise_and_hare.19.1.0" expl="asserted formula" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1" expl="loop invariant preservation" proved="true">
<transf name="instantiate" proved="true" arg1="H24" arg2="(n+i1),n">
<goal name="VC tortoise_and_hare.19.1.1.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(exists k. k &gt;= 1 /\ i1 = k * lambda)">
<goal name="VC tortoise_and_hare.19.1.1.0.0" proved="true">
<goal name="VC tortoise_and_hare.19.1.1.0.0" expl="asserted formula" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1" expl="loop invariant preservation" proved="true">
<transf name="destruct" proved="true" arg1="h">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="((k-1) * lambda &gt;= 0)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.0" proved="true">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="7"><result status="valid" time="9.59"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1" expl="loop invariant preservation" proved="true">
<transf name="assert" proved="true" arg1="(i1 &gt;= lambda)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.0" proved="true">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.0" expl="asserted formula" proved="true">
<proof prover="6"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1" expl="loop invariant preservation" proved="true">
......@@ -281,12 +281,12 @@
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1" expl="false case (loop invariant preservation)" proved="true">
<transf name="assert" proved="true" arg1="(x (n + lambda) &lt;&gt; x n)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0" proved="true">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0" expl="asserted formula" proved="true">
<transf name="assert" proved="true" arg1="(lambda &lt; i1)">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.0" proved="true">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.80" steps="276"/></proof>
</goal>
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.1" proved="true">
<goal name="VC tortoise_and_hare.19.1.1.0.1.0.1.1.1.0.1" expl="asserted formula" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
......@@ -316,7 +316,7 @@
<transf name="case" proved="true" arg1="(i = mu+1)">
<goal name="VC tortoise_and_hare.20.0" expl="true case (loop variant decrease)" proved="true">
<transf name="assert" proved="true" arg1="(x mu = x (mu + n))">
<goal name="VC tortoise_and_hare.20.0.0" proved="true">
<goal name="VC tortoise_and_hare.20.0.0" expl="asserted formula" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="VC tortoise_and_hare.20.0.1" expl="true case (loop variant decrease)" proved="true">
......@@ -334,7 +334,7 @@
<goal name="VC tortoise_and_hare.21.0" expl="loop invariant preservation" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="39"/></proof>
</goal>
<goal name="VC tortoise_and_hare.21.1" proved="true">
<goal name="VC tortoise_and_hare.21.1" expl="equality hypothesis" proved="true">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -366,30 +366,30 @@
<transf name="case" proved="true" arg1="(lam = 0)">
<goal name="VC tortoise_and_hare.26.0" expl="true case (assertion)" proved="true">
<transf name="assert" proved="true" arg1="(lambda &gt;= mu)">
<goal name="VC tortoise_and_hare.26.0.0" proved="true">
<goal name="VC tortoise_and_hare.26.0.0" expl="asserted formula" proved="true">
<transf name="case" proved="true" arg1="(lambda &lt; mu)">
<goal name="VC tortoise_and_hare.26.0.0.0" expl="true case" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.0" expl="true case (asserted formula)" proved="true">
<transf name="assert" proved="true" arg1="(x (n + lambda) &lt;&gt; x n)">
<goal name="VC tortoise_and_hare.26.0.0.0.0" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.0.0" expl="asserted formula" proved="true">
<proof prover="5"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC tortoise_and_hare.26.0.0.0.1" expl="true case" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.0.1" expl="true case (asserted formula)" proved="true">
<transf name="assert" proved="true" arg1="(x (n + lambda) = x n)">
<goal name="VC tortoise_and_hare.26.0.0.0.1.0" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.0.1.0" expl="asserted formula" proved="true">
<transf name="instantiate" proved="true" arg1="H18" arg2="(n+lambda),n">
<goal name="VC tortoise_and_hare.26.0.0.0.1.0.0" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="6"><result status="valid" time="0.05"/></proof>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26.0.0.0.1.1" expl="true case" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.0.1.1" expl="true case (asserted formula)" proved="true">
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="VC tortoise_and_hare.26.0.0.1" expl="false case" proved="true">
<goal name="VC tortoise_and_hare.26.0.0.1" expl="false case (asserted formula)" proved="true">
<proof prover="6"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -398,7 +398,7 @@
<transf name="destruct" proved="true" arg1="H10">
<goal name="VC tortoise_and_hare.26.0.1.0" expl="true case (assertion)" proved="true">
<transf name="assert" proved="true" arg1="(n = lambda \/ n = 2*lambda)">
<goal name="VC tortoise_and_hare.26.0.1.0.0" proved="true">
<goal name="VC tortoise_and_hare.26.0.1.0.0" expl="asserted formula" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="36"/></proof>
</goal>
<goal name="VC tortoise_and_hare.26.0.1.0.1" expl="true case (assertion)" proved="true">
......
......@@ -73,12 +73,12 @@
<transf name="case" proved="true" arg1="hi=lo+1">
<goal name="VC tree_of_array_aux.6.3.1.0" expl="false case (true case)" proved="true">
<transf name="assert" proved="true" arg1="left=Empty">
<goal name="VC tree_of_array_aux.6.3.1.0.0" proved="true">
<goal name="VC tree_of_array_aux.6.3.1.0.0" expl="asserted formula" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC tree_of_array_aux.6.3.1.0.1" expl="false case (true case)" proved="true">
<transf name="assert" proved="true" arg1="right=Empty">
<goal name="VC tree_of_array_aux.6.3.1.0.1.0" proved="true">
<goal name="VC tree_of_array_aux.6.3.1.0.1.0" expl="asserted formula" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC tree_of_array_aux.6.3.1.0.1.1" expl="false case (true case)" proved="true">
......
......@@ -21,7 +21,7 @@
<transf name="subst" proved="true" arg1="a">
<goal name="VC fetch_and_add.0.0.0" expl="assertion" proved="true">
<transf name="apply" proved="true" arg1="Div_mod">
<goal name="VC fetch_and_add.0.0.0.0" proved="true">
<goal name="VC fetch_and_add.0.0.0.0" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -228,16 +228,16 @@
</goal>
<goal name="VC main.25" expl="liveness" proved="true">
<transf name="right" proved="true" >
<goal name="VC main.25.0" expl="VC for main" proved="true">
<goal name="VC main.25.0" expl="right case" proved="true">
<transf name="split_vc" proved="true" >
<goal name="VC main.25.0.0" expl="VC for main" proved="true">
<goal name="VC main.25.0.0" expl="right case" proved="true">
<transf name="exists" proved="true" arg1="0">
<goal name="VC main.25.0.0.0" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="27"/></proof>
</goal>
</transf>
</goal>
<goal name="VC main.25.0.1" expl="VC for main" proved="true">
<goal name="VC main.25.0.1" expl="right case" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
......@@ -468,10 +468,10 @@
<transf name="rewrite" proved="true" arg1="H">
<goal name="VC main.57.1.0" expl="assertion" proved="true">
<transf name="apply" proved="true" arg1="consecutive_last_push">
<goal name="VC main.57.1.0.0" proved="true">
<goal name="VC main.57.1.0.0" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC main.57.1.0.1" proved="true">
<goal name="VC main.57.1.0.1" expl="apply premises" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
......@@ -587,7 +587,7 @@
</goal>
<goal name="VC main.63.1.0.3" expl="VC for main" proved="true">
<transf name="assert" proved="true" arg1="( x1 &lt;&gt; th )">
<goal name="VC main.63.1.0.3.0" proved="true">
<goal name="VC main.63.1.0.3.0" expl="asserted formula" proved="true">
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC main.63.