Commit c7bd3398 authored by MARCHE Claude's avatar MARCHE Claude

update sessions to Coq 8.6.1

parent 9c4127a8
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../imp_n.why" expanded="true">
<theory name="Imp" sum="393416a5d93852e1dde31286bcba2c8e" expanded="true">
......@@ -29,13 +29,13 @@
<proof prover="4"><result status="valid" time="0.13" steps="485"/></proof>
</goal>
<goal name="progress" expl="">
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="2" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="0" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.29"/></proof>
<proof prover="2" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="many_steps_seq" expl="">
<proof prover="0" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
<proof prover="2" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="eval_subst_expr" expl="">
<transf name="induction_ty_lex">
......@@ -45,7 +45,7 @@
</transf>
</goal>
<goal name="eval_subst" expl="">
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="2" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="skip_rule" expl="">
<proof prover="4"><result status="valid" time="0.04" steps="146"/></proof>
......@@ -57,10 +57,10 @@
<proof prover="4"><result status="valid" time="2.20" steps="6927"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="2" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="2" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="consequence_rule" expl="">
<proof prover="1"><result status="valid" time="0.05"/></proof>
......
......@@ -2,8 +2,8 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="6" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Eprover" version="1.8-001" timelimit="30" steplimit="0" memlimit="4000"/>
<prover id="10" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
......@@ -40,7 +40,7 @@
<proof prover="10"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="eval_change_free" expl="">
<proof prover="0" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="2" timelimit="5" edited="wp2_Imp_eval_change_free_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="check_skip" expl="">
<proof prover="6"><result status="valid" time="0.01" steps="2"/></proof>
......@@ -56,7 +56,7 @@
</transf>
</goal>
<goal name="many_steps_seq" expl="">
<proof prover="0" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="2" edited="wp2_Imp_many_steps_seq_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
<theory name="TestSemantics" sum="41aa0312c3a7229313465ec4249007d8">
......@@ -126,7 +126,7 @@
<proof prover="6"><result status="valid" time="0.14" steps="487"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.49"/></proof>
<proof prover="2" edited="wp2_HoareLogic_if_rule_1.v"><result status="valid" time="0.49"/></proof>
</goal>
<goal name="assert_rule" expl="">
<proof prover="6"><result status="valid" time="0.22" steps="631"/></proof>
......@@ -135,10 +135,10 @@
<proof prover="6"><result status="valid" time="0.31" steps="1397"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="0" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.70"/></proof>
<proof prover="2" edited="wp2_HoareLogic_while_rule_1.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="while_rule_ext" expl="">
<proof prover="0" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
<proof prover="2" edited="wp2_HoareLogic_while_rule_ext_1.v"><result status="valid" time="0.54"/></proof>
</goal>
</theory>
<theory name="WP" sum="658fad42eb6dd30941a57184e5c43ba4">
......@@ -186,7 +186,7 @@
<proof prover="6" timelimit="1"><result status="valid" time="0.07" steps="283"/></proof>
</goal>
<goal name="VC compute_writes.6.5" expl="postcondition">
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_WP_VC_compute_writes_1.v"><result status="valid" time="0.45"/></proof>
<proof prover="2" timelimit="5" memlimit="1000" edited="wp2_WP_VC_compute_writes_1.v"><result status="valid" time="0.45"/></proof>
</goal>
<goal name="VC compute_writes.6.6" expl="postcondition">
<proof prover="10"><result status="valid" time="0.32"/></proof>
......@@ -230,7 +230,7 @@
<proof prover="6"><result status="valid" time="0.02" steps="18"/></proof>
</goal>
<goal name="VC wp.6.6" expl="postcondition">
<proof prover="0" timelimit="5" memlimit="1000" edited="wp2_WP_VC_wp_2.v"><result status="valid" time="0.44"/></proof>
<proof prover="2" timelimit="5" memlimit="1000" edited="wp2_WP_VC_wp_2.v"><result status="valid" time="0.44"/></proof>
</goal>
</transf>
</goal>
......
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="10" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -32,16 +32,16 @@
<proof prover="6"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="to_nat_of_zero2" expl="">
<proof prover="1" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="4" edited="bitvector_BitVector_to_nat_of_zero2_1.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="to_nat_of_zero" expl="">
<proof prover="1" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
<proof prover="4" timelimit="30" edited="bitvector_BitVector_to_nat_of_zero_1.v"><result status="valid" time="1.01"/></proof>
</goal>
<goal name="to_nat_of_one" expl="">
<proof prover="1" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="0.96"/></proof>
<proof prover="4" edited="bitvector_BitVector_to_nat_of_one_1.v"><result status="valid" time="0.96"/></proof>
</goal>
<goal name="to_nat_sub_footprint" expl="">
<proof prover="1" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="1.40"/></proof>
<proof prover="4" timelimit="7" edited="bitvector_BitVector_to_nat_sub_footprint_1.v"><result status="valid" time="1.40"/></proof>
</goal>
<goal name="nth_from_int_low_even" expl="">
<proof prover="2"><result status="valid" time="0.02" steps="68"/></proof>
......@@ -73,8 +73,8 @@
<proof prover="3"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="nth_from_int2c_plus_pow2" expl="">
<proof prover="1" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.69"/></proof>
<proof prover="2"><result status="valid" time="0.33" steps="94"/></proof>
<proof prover="4" timelimit="10" edited="bitvector_BitVector_nth_from_int2c_plus_pow2_1.v"><result status="valid" time="0.49"/></proof>
</goal>
</theory>
<theory name="BV32" sum="34ed4e77796acb2611bcf8f00bf21d7d" expanded="true">
......@@ -139,16 +139,16 @@
<proof prover="10"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="to_nat_0x00000001" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="71.82"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="85.20"/></proof>
</goal>
<goal name="to_nat_0x00000003" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="74.14"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="64.88"/></proof>
</goal>
<goal name="to_nat_0x00000007" expl="">
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="61.79"/></proof>
<proof prover="6" timelimit="60" memlimit="4000"><result status="valid" time="54.54"/></proof>
</goal>
<goal name="to_nat_0x0000000F" expl="">
<proof prover="6" timelimit="120"><result status="valid" time="45.53"/></proof>
<proof prover="6" timelimit="120"><result status="valid" time="53.60"/></proof>
</goal>
<goal name="to_nat_0x0000001F" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="37.94"/></proof>
......@@ -157,13 +157,13 @@
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="31.43"/></proof>
</goal>
<goal name="to_nat_0x0000007F" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="30.37"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="26.21"/></proof>
</goal>
<goal name="to_nat_0x000000FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="21.03"/></proof>
</goal>
<goal name="to_nat_0x000001FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="17.00"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="18.93"/></proof>
</goal>
<goal name="to_nat_0x000003FF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="13.72"/></proof>
......@@ -175,10 +175,10 @@
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="8.76"/></proof>
</goal>
<goal name="to_nat_0x00001FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="6.86"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="7.74"/></proof>
</goal>
<goal name="to_nat_0x00003FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.95"/></proof>
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="5.75"/></proof>
</goal>
<goal name="to_nat_0x00007FFF" expl="">
<proof prover="6" timelimit="30" memlimit="4000"><result status="valid" time="4.44"/></proof>
......
......@@ -4,8 +4,8 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.6" timelimit="30" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double.why" expanded="true">
<theory name="BV_double" sum="d41d8cd98f00b204e9800998ecf8427e">
......@@ -28,7 +28,7 @@
</goal>
<goal name="exp_one" expl="" expanded="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.21" steps="668"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="2" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="mantissa_one" expl="">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
......
......@@ -5,8 +5,8 @@
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.6" timelimit="60" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../double_of_int.why" expanded="true">
......@@ -86,7 +86,7 @@
<proof prover="8"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="exp_const" expl="">
<proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
<proof prover="3" timelimit="30" edited="double_of_int_DoubleOfInt_exp_const_1.v"><result status="valid" time="0.80"/></proof>
</goal>
<goal name="to_nat_mantissa_1" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="91"/></proof>
......@@ -162,10 +162,10 @@
<proof prover="8"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_pos" expl="">
<proof prover="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="3" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_pos_1.v"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="lemma1_pos" expl="">
<proof prover="5" timelimit="6" edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"><result status="valid" time="1.44"/></proof>
<proof prover="3" timelimit="6" edited="double_of_int_DoubleOfInt_lemma1_pos_1.v"><result status="valid" time="1.44"/></proof>
</goal>
<goal name="jpxorx_neg" expl="">
<proof prover="2"><result status="valid" time="0.07"/></proof>
......@@ -174,10 +174,10 @@
<proof prover="8"><result status="valid" time="0.19"/></proof>
</goal>
<goal name="from_int2c_to_nat_sub_neg" expl="">
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.06"/></proof>
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_from_int2c_to_nat_sub_neg_1.v"><result status="valid" time="2.06"/></proof>
</goal>
<goal name="lemma1_neg" expl="">
<proof prover="5" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="3" timelimit="10" edited="double_of_int_DoubleOfInt_lemma1_neg_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="lemma1" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="95"/></proof>
......@@ -190,7 +190,7 @@
<proof prover="4" timelimit="10"><result status="valid" time="1.96"/></proof>
</goal>
<goal name="to_nat_bv32_bv64_aux" expl="">
<proof prover="5" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="2.08"/></proof>
<proof prover="3" timelimit="5" edited="double_of_int_DoubleOfInt_to_nat_bv32_bv64_aux_1.v"><result status="valid" time="2.08"/></proof>
</goal>
<goal name="to_nat_bv32_bv64" expl="">
<proof prover="1"><result status="valid" time="0.06" steps="90"/></proof>
......@@ -213,7 +213,7 @@
<proof prover="8"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="lemma2" expl="">
<proof prover="5" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="22.36"/></proof>
<proof prover="3" edited="double_of_int_DoubleOfInt_lemma2_1.v"><result status="valid" time="22.36"/></proof>
</goal>
<goal name="nth_var4" expl="">
<proof prover="1"><result status="valid" time="1.44" steps="148"/></proof>
......@@ -267,7 +267,7 @@
<proof prover="8"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="var_value0" expl="">
<proof prover="5" timelimit="30" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.19"/></proof>
<proof prover="3" timelimit="30" edited="double_of_int_DoubleOfInt_var_value0_1.v"><result status="valid" time="3.19"/></proof>
</goal>
<goal name="from_int_sum" expl="">
<proof prover="1"><result status="valid" time="0.05" steps="92"/></proof>
......
......@@ -3,9 +3,9 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="9" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -18,10 +18,10 @@
<proof prover="10"><result status="valid" time="0.00" steps="3"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="4" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.46"/></proof>
<proof prover="1" edited="power2_Pow2int_Power_sum_1.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="pow2pos" expl="">
<proof prover="4" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.43"/></proof>
<proof prover="1" edited="power2_Pow2int_pow2pos_1.v"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="pow2_0" expl="">
<proof prover="0"><result status="valid" time="0.00"/></proof>
......@@ -316,13 +316,13 @@
<goal name="pow2_48" expl="">
<proof prover="2"><result status="valid" time="0.04"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.60"/></proof>
<proof prover="9"><result status="valid" time="1.82"/></proof>
<proof prover="9"><result status="valid" time="1.50"/></proof>
<proof prover="10"><result status="valid" time="0.03" steps="51"/></proof>
</goal>
<goal name="pow2_49" expl="">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="6" timelimit="6"><result status="valid" time="1.68"/></proof>
<proof prover="9"><result status="valid" time="1.89"/></proof>
<proof prover="9"><result status="valid" time="1.60"/></proof>
<proof prover="10"><result status="valid" time="0.02" steps="52"/></proof>
</goal>
<goal name="pow2_50" expl="">
......@@ -431,7 +431,7 @@
<proof prover="10"><result status="valid" time="0.24" steps="99"/></proof>
</goal>
<goal name="Mod_pow2_gen" expl="">
<proof prover="4" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
<proof prover="1" edited="power2_Pow2int_Mod_pow2_gen_1.v"><result status="valid" time="0.86"/></proof>
</goal>
</theory>
<theory name="Pow2real" sum="e31a44730ea8985818a40fb1e9374bf0" expanded="true">
......@@ -467,25 +467,25 @@
<proof prover="10"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="Power_non_null_aux" expl="">
<proof prover="4" edited="power2_Pow2real_Power_non_null_aux_1.v"><result status="valid" time="0.65"/></proof>
<proof prover="1" edited="power2_Pow2real_Power_non_null_aux_1.v"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="Power_neg_aux" expl="">
<proof prover="4" edited="power2_Pow2real_Power_neg_aux_1.v"><result status="valid" time="0.85"/></proof>
<proof prover="1" edited="power2_Pow2real_Power_neg_aux_1.v"><result status="valid" time="0.85"/></proof>
</goal>
<goal name="Power_non_null" expl="">
<proof prover="4" edited="power2_Pow2real_Power_non_null_1.v"><result status="valid" time="0.84"/></proof>
<proof prover="1" edited="power2_Pow2real_Power_non_null_1.v"><result status="valid" time="0.84"/></proof>
</goal>
<goal name="Power_neg" expl="">
<proof prover="10"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="Power_sum_aux" expl="">
<proof prover="4" edited="power2_Pow2real_Power_sum_aux_1.v"><result status="valid" time="0.82"/></proof>
<proof prover="1" edited="power2_Pow2real_Power_sum_aux_1.v"><result status="valid" time="0.82"/></proof>
</goal>
<goal name="Power_sum" expl="">
<proof prover="4" edited="power2_Pow2real_Power_sum_1.v"><result status="valid" time="0.62"/></proof>
<proof prover="1" edited="power2_Pow2real_Power_sum_1.v"><result status="valid" time="0.62"/></proof>
</goal>
<goal name="Pow2_int_real" expl="">
<proof prover="4" edited="power2_Pow2real_Pow2_int_real_1.v"><result status="valid" time="0.51"/></proof>
<proof prover="1" edited="power2_Pow2real_Pow2_int_real_1.v"><result status="valid" time="0.51"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,12 +2,12 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../bresenham.mlw" expanded="true">
<theory name="M" sum="7f17c0a603b1cea677dd6eb91a67437a" expanded="true">
<goal name="closest" expl="" expanded="true">
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
<proof prover="1" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC bresenham" expl="VC for bresenham" expanded="true">
<proof prover="2"><result status="valid" time="0.12" steps="70"/></proof>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../12934.why" expanded="true">
<theory name="BTS12934" sum="a1c52743c237f96f62b5a441ad065efb" expanded="true">
<goal name="t" expanded="true">
<proof prover="0" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
<goal name="t" expl="" expanded="true">
<proof prover="1" edited="12934_BTS12934_t_1.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<file name="../13849.why" expanded="true">
<theory name="T" sum="9002cd307075906fccf3007350013be9" expanded="true">
<goal name="x" expanded="true">
<proof prover="0" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13849_T_x_2.v"><result status="valid" time="0.29"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="0"/>
<file name="../13854.why">
<theory name="T" sum="b5806ff59fa2827b1dd2b7113af851bc" expanded="true">
<goal name="g" expanded="true">
<proof prover="0" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
<goal name="g" expl="" expanded="true">
<proof prover="1" edited="13854_T_g_1.v"><result status="valid" time="0.29"/></proof>
</goal>
<goal name="x" expanded="true">
<proof prover="0" edited="13854_T_x_1.v"><result status="valid" time="0.30"/></proof>
<goal name="x" expl="" expanded="true">
<proof prover="1" edited="13854_T_x_1.v"><result status="valid" time="0.30"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,7 +2,7 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Yices" version="1.0.38" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="8" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="0"/>
......@@ -135,13 +135,13 @@
<proof prover="14"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Tan_pi_4" expl="" expanded="true">
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="Tan_pi_3" expl="" expanded="true">
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="Atan_1" expl="" expanded="true">
<proof prover="0" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="1" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,18 +2,18 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="1" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="5" name="Coq" version="8.6.1" timelimit="8" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="8" name="Z3" version="4.4.0" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../dfa_example.mlw" expanded="true">
<theory name="DfaExample" sum="dd8fae77d607d67a93d10a5e7b2617f8" expanded="true">
<goal name="nil_notin_r1" expl="">
<proof prover="0" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.26"/></proof>
<proof prover="4"><result status="valid" time="0.10"/></proof>
<proof prover="5" edited="dfa_example_DfaExample_nil_notin_r1_1.v"><result status="valid" time="0.26"/></proof>
<proof prover="7"><result status="valid" time="0.08" steps="140"/></proof>
</goal>
<goal name="VC all_in_r0" expl="VC for all_in_r0" expanded="true">
......
......@@ -2,11 +2,11 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="2.19" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Z3" version="4.3.1" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="7" name="Alt-Ergo" version="0.95.2" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="8" name="CVC4" version="1.3" timelimit="6" steplimit="0" memlimit="1000"/>
......@@ -21,10 +21,10 @@
</transf>
</goal>
<goal name="first_last" expl="">
<proof prover="0" edited="edit_distance_Word_first_last_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="5" edited="edit_distance_Word_first_last_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="key_lemma_right" expl="">
<proof prover="0" edited="edit_distance_Word_key_lemma_right_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="5" edited="edit_distance_Word_key_lemma_right_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="dist_symetry" expl="">
<transf name="induction_pr">
......@@ -76,7 +76,7 @@
<proof prover="8"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="min_dist_equal.1.2.2" expl="">
<proof prover="8"><result status="valid" time="1.16"/></proof>
<proof prover="8"><result status="valid" time="1.39"/></proof>
</goal>
<goal name="min_dist_equal.1.2.3" expl="">
<proof prover="8"><result status="valid" time="1.03"/></proof>
......@@ -93,7 +93,7 @@
</transf>
</goal>
<goal name="min_dist_diff" expl="">
<proof prover="0" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="5" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="min_dist_eps" expl="">
<transf name="inline_goal">
......@@ -139,7 +139,7 @@
</theory>
<theory name="EditDistance" sum="31e3d97050737973b223fb837f3ddb4c" expanded="true">
<goal name="suffix_length" expl="" expanded="true">
<proof prover="0" timelimit="5" memlimit="1000" edited="edit_distance_WP_EditDistance_suffix_length_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="5" timelimit="5" memlimit="1000" edited="edit_distance_WP_EditDistance_suffix_length_1.v"><result status="valid" time="0.41"/></proof>
</goal>
<goal name="VC distance" expl="VC for distance">
<transf name="split_goal_wp">
......@@ -159,13 +159,13 @@
<proof prover="1"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="VC distance.6" expl="index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
</goal>
<goal name="VC distance.7" expl="index in array bounds">
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC distance.8" expl="index in array bounds">
<proof prover="1"><result status="valid" time="0.00" steps="10"/></proof>
<proof prover="1"><result status="valid" time="0.01" steps="10"/></proof>
</goal>
<goal name="VC distance.9" expl="loop invariant init">
<proof prover="1"><result status="valid" time="0.08" steps="232"/></proof>
......
......@@ -2,20 +2,20 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Coq" version="8.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.4.1" timelimit="30" steplimit="0" memlimit="1000"/>
<file name="../euler001.mlw">
<theory name="DivModHints" sum="4684d234b6fd5ff14ff22c5fd979de0f">
<goal name="mod_div_unique" expl="">
<proof prover="0" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="2" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="mod_succ_1" expl="">
<proof prover="0" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="0.38"/></proof>
<proof prover="2" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="mod_succ_2" expl="">
<proof prover="0" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="2" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="div_succ_1" expl="">
<proof prover="1" timelimit="30"><result status="valid" time="0.04"/></proof>
......@@ -60,7 +60,7 @@
</theory>
<theory name="TriangularNumbers" sum="1dd8270afe1631351bdfba598382f6b3">
<goal name="tr_mod_2" expl="">
<proof prover="0" memlimit="1000" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="2" memlimit="1000" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.31"/></proof>