Commit e12d156e authored by MARCHE Claude's avatar MARCHE Claude

update provers in sessions

parent c1f8c976
......@@ -2,67 +2,67 @@
<!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.7.1" 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">
<goal name="ident_eq_dec" expl="">
<file name="../imp_n.why" proved="true">
<theory name="Imp" proved="true" sum="3ef09115e35536df0c4a509815956237">
<goal name="ident_eq_dec" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="check_skip" expl="">
<goal name="check_skip" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="Test13" expl="">
<goal name="Test13" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Test42" expl="">
<goal name="Test42" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="Test55" expl="">
<goal name="Test55" proved="true">
<proof prover="4"><result status="valid" time="0.00" steps="16"/></proof>
</goal>
<goal name="Ass42" expl="">
<goal name="Ass42" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="91"/></proof>
</goal>
<goal name="If42" expl="">
<goal name="If42" proved="true">
<proof prover="4"><result status="valid" time="0.13" steps="485"/></proof>
</goal>
<goal name="progress" expl="">
<proof prover="2" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
<goal name="progress" proved="true">
<proof prover="0" edited="imp_n_Imp_progress_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="steps_non_neg" expl="">
<proof prover="2" edited="imp_n_Imp_steps_non_neg_1.v"><result status="valid" time="0.29"/></proof>
<goal name="steps_non_neg" proved="true">
<proof prover="0" 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="2" edited="imp_n_Imp_many_steps_seq_1.v"><result status="valid" time="0.36"/></proof>
<goal name="many_steps_seq" proved="true">
<proof prover="0" 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">
<goal name="eval_subst_expr.1" expl="">
<goal name="eval_subst_expr" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="eval_subst_expr.0" proved="true">
<proof prover="4"><result status="valid" time="0.02" steps="107"/></proof>
</goal>
</transf>
</goal>
<goal name="eval_subst" expl="">
<proof prover="2" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.33"/></proof>
<goal name="eval_subst" proved="true">
<proof prover="0" edited="imp_n_Imp_eval_subst_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="skip_rule" expl="">
<goal name="skip_rule" proved="true">
<proof prover="4"><result status="valid" time="0.04" steps="146"/></proof>
</goal>
<goal name="assign_rule" expl="">
<goal name="assign_rule" proved="true">
<proof prover="4"><result status="valid" time="0.99" steps="1831"/></proof>
</goal>
<goal name="seq_rule" expl="">
<proof prover="4"><result status="valid" time="2.20" steps="6927"/></proof>
<goal name="seq_rule" proved="true">
<proof prover="4"><result status="valid" time="2.20" steps="6935"/></proof>
</goal>
<goal name="if_rule" expl="">
<proof prover="2" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
<goal name="if_rule" proved="true">
<proof prover="0" edited="imp_n_Imp_if_rule_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="while_rule" expl="">
<proof prover="2" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.39"/></proof>
<goal name="while_rule" proved="true">
<proof prover="0" edited="imp_n_Imp_while_rule_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="consequence_rule" expl="">
<goal name="consequence_rule" proved="true">
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
</theory>
......
......@@ -4,38 +4,38 @@
<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.7.1" 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">
<file name="../double.why" proved="true">
<theory name="BV_double" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="TestDouble" sum="4120bd89e05ca08e761d40884b9d0621" expanded="true">
<goal name="nth_one1" expl="" expanded="true">
<theory name="TestDouble" proved="true" sum="4120bd89e05ca08e761d40884b9d0621">
<goal name="nth_one1" proved="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.05" steps="77"/></proof>
</goal>
<goal name="nth_one2" expl="" expanded="true">
<goal name="nth_one2" proved="true">
<proof prover="0" timelimit="3"><result status="valid" time="0.04" steps="77"/></proof>
</goal>
<goal name="nth_one3" expl="">
<goal name="nth_one3" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="77"/></proof>
</goal>
<goal name="sign_one" expl="">
<goal name="sign_one" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="76"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="5"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="exp_one" expl="" expanded="true">
<goal name="exp_one" proved="true">
<proof prover="0" timelimit="30"><result status="valid" time="2.21" steps="668"/></proof>
<proof prover="2" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
<proof prover="4" edited="double_TestDouble_exp_one_1.v"><result status="valid" time="0.52"/></proof>
</goal>
<goal name="mantissa_one" expl="">
<goal name="mantissa_one" proved="true">
<proof prover="0"><result status="valid" time="0.09" steps="87"/></proof>
<proof prover="3"><result status="valid" time="0.84"/></proof>
<proof prover="5" timelimit="11"><result status="valid" time="2.72"/></proof>
</goal>
<goal name="double_value_of_1" expl="">
<goal name="double_value_of_1" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="94"/></proof>
<proof prover="1"><result status="valid" time="0.03"/></proof>
</goal>
......
This diff is collapsed.
......@@ -2,14 +2,14 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Coq" version="8.7.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="1" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
<file name="../bresenham.mlw" proved="true">
<theory name="M" proved="true" sum="7f17c0a603b1cea677dd6eb91a67437a">
<goal name="closest" proved="true">
<proof prover="0" edited="bresenham_M_closest_1.v"><result status="valid" time="0.54"/></proof>
</goal>
<goal name="VC bresenham" expl="VC for bresenham" expanded="true">
<goal name="VC bresenham" expl="VC for bresenham" proved="true">
<proof prover="2"><result status="valid" time="0.12" steps="70"/></proof>
</goal>
</theory>
......
......@@ -2,16 +2,16 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="0" name="Coq" version="8.7.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"/>
<prover id="9" name="Gappa" version="1.3.0" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="12" name="Alt-Ergo" version="0.99.1" timelimit="3" steplimit="0" memlimit="0"/>
<prover id="14" name="Z3" version="4.3.2" timelimit="3" steplimit="0" memlimit="0"/>
<file name="../real.why" expanded="true">
<theory name="Test" sum="fa766792600f8b59ffb54deaecae5fd5" expanded="true">
<goal name="G1" expl="" expanded="true">
<file name="../real.why" proved="true">
<theory name="Test" proved="true" sum="fa766792600f8b59ffb54deaecae5fd5">
<goal name="G1" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
......@@ -19,129 +19,129 @@
<proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G2" expl="" expanded="true">
<goal name="G2" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="G3" expl="" expanded="true">
<goal name="G3" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="TestInfix" sum="f9e4b7c6b90d06ca8e54ccb21378b7c3" expanded="true">
<goal name="Add" expl="" expanded="true">
<theory name="TestInfix" proved="true" sum="f9e4b7c6b90d06ca8e54ccb21378b7c3">
<goal name="Add" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Sub" expl="" expanded="true">
<goal name="Sub" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Neg" expl="" expanded="true">
<goal name="Neg" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Mul" expl="" expanded="true">
<goal name="Mul" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Div" expl="" expanded="true">
<goal name="Div" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.00" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="Inv" expl="" expanded="true">
<goal name="Inv" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="0"/></proof>
<proof prover="14"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="SquareTest" sum="f5ea8549d8b1f79c2129c56632f38b01" expanded="true">
<goal name="Sqrt_zero" expl="" expanded="true">
<theory name="SquareTest" proved="true" sum="f5ea8549d8b1f79c2129c56632f38b01">
<goal name="Sqrt_zero" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="8" timelimit="60" memlimit="1000"><result status="valid" time="0.02"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="14" timelimit="60" memlimit="1000"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Sqrt_one" expl="" expanded="true">
<goal name="Sqrt_one" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="Sqrt_four" expl="" expanded="true">
<goal name="Sqrt_four" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8" timelimit="67" memlimit="1000"><result status="valid" time="22.59"/></proof>
<proof prover="9"><result status="valid" time="0.00"/></proof>
<proof prover="12" timelimit="5" memlimit="1000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
</theory>
<theory name="ExpLogTest" sum="cd1e6835a7a21f47ea5fa0d7580d1c27" expanded="true">
<goal name="Log_e" expl="" expanded="true">
<theory name="ExpLogTest" proved="true" sum="cd1e6835a7a21f47ea5fa0d7580d1c27">
<goal name="Log_e" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerIntTest" sum="1e54cdf0224cce818e1516659037b62e" expanded="true">
<goal name="Pow_2_2" expl="" expanded="true">
<theory name="PowerIntTest" proved="true" sum="1e54cdf0224cce818e1516659037b62e">
<goal name="Pow_2_2" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="12" timelimit="60" memlimit="1000"><result status="valid" time="0.02" steps="4"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="PowerRealTest" sum="180a4360503699539283c0e3683511ef" expanded="true">
<goal name="Pow_2_2" expl="" expanded="true">
<theory name="PowerRealTest" proved="true" sum="180a4360503699539283c0e3683511ef">
<goal name="Pow_2_2" proved="true">
<proof prover="8"><result status="valid" time="0.01"/></proof>
<proof prover="12"><result status="valid" time="0.01" steps="6"/></proof>
<proof prover="14"><result status="valid" time="0.01"/></proof>
</goal>
</theory>
<theory name="TrigonometryTest" sum="d294ff286e37b3974b0eafb6adbbf485" expanded="true">
<goal name="Cos_2_pi" expl="" expanded="true">
<theory name="TrigonometryTest" proved="true" sum="d294ff286e37b3974b0eafb6adbbf485">
<goal name="Cos_2_pi" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="8"><result status="valid" time="0.09"/></proof>
<proof prover="12"><result status="valid" time="0.12" steps="37"/></proof>
<proof prover="14"><result status="valid" time="0.11"/></proof>
</goal>
<goal name="Sin_2_pi" expl="" expanded="true">
<goal name="Sin_2_pi" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="8"><result status="valid" time="0.12"/></proof>
<proof prover="12" timelimit="60" memlimit="1000"><result status="valid" time="0.10" steps="87"/></proof>
<proof prover="14"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Tan_pi_4" expl="" expanded="true">
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
<goal name="Tan_pi_4" proved="true">
<proof prover="0" 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="1" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
<goal name="Tan_pi_3" proved="true">
<proof prover="0" 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="1" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
<goal name="Atan_1" proved="true">
<proof prover="0" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
</file>
......
......@@ -2,53 +2,53 @@
<!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.7.1" 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="">
<file name="../dfa_example.mlw" proved="true">
<theory name="DfaExample" proved="true" sum="8b182d4c6b2d88551595aee1ff3eae1c">
<goal name="nil_notin_r1" proved="true">
<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">
<goal name="VC all_in_r0" expl="VC for all_in_r0" proved="true">
<proof prover="2"><result status="valid" time="0.03" steps="222"/></proof>
</goal>
<goal name="words_in_r1_end_with_one" expl="">
<goal name="words_in_r1_end_with_one" proved="true">
<proof prover="8"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC words_in_r1_suffix_in_r1" expl="VC for words_in_r1_suffix_in_r1" expanded="true">
<goal name="VC words_in_r1_suffix_in_r1" expl="VC for words_in_r1_suffix_in_r1" proved="true">
<proof prover="1"><result status="valid" time="3.06"/></proof>
</goal>
<goal name="VC zero_w_in_r1" expl="VC for zero_w_in_r1" expanded="true">
<transf name="split_goal_wp" expanded="true">
<goal name="VC zero_w_in_r1.1" expl="assertion">
<goal name="VC zero_w_in_r1" expl="VC for zero_w_in_r1" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="VC zero_w_in_r1.0" expl="assertion" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="42"/></proof>
</goal>
<goal name="VC zero_w_in_r1.2" expl="postcondition">
<goal name="VC zero_w_in_r1.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.50"/></proof>
</goal>
</transf>
</goal>
<goal name="VC one_w_in_r1" expl="VC for one_w_in_r1" expanded="true">
<proof prover="2"><result status="valid" time="2.22" steps="6899"/></proof>
<goal name="VC one_w_in_r1" expl="VC for one_w_in_r1" proved="true">
<proof prover="2"><result status="valid" time="2.22" steps="6829"/></proof>
</goal>
<goal name="zero_w_in_r2" expl="">
<goal name="zero_w_in_r2" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="48"/></proof>
</goal>
<goal name="one_w_in_r2" expl="">
<goal name="one_w_in_r2" proved="true">
<proof prover="2"><result status="valid" time="0.01" steps="50"/></proof>
</goal>
<goal name="VC astate1" expl="VC for astate1" expanded="true">
<goal name="VC astate1" expl="VC for astate1" proved="true">
<proof prover="2"><result status="valid" time="0.59" steps="3042"/></proof>
</goal>
<goal name="VC astate2" expl="VC for astate2" expanded="true">
<proof prover="2"><result status="valid" time="0.75" steps="3708"/></proof>
<goal name="VC astate2" expl="VC for astate2" proved="true">
<proof prover="2"><result status="valid" time="0.75" steps="3925"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,7 +4,7 @@
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="5" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.7.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="10" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="11" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../edit_distance.mlw" proved="true">
......@@ -20,7 +20,7 @@
<proof prover="11"><result status="valid" time="0.12"/></proof>
</goal>
<goal name="key_lemma_right" proved="true">
<proof prover="5" edited="edit_distance_Word_key_lemma_right_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="2" edited="edit_distance_Word_key_lemma_right_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="dist_symetry" proved="true">
<transf name="induction_pr" proved="true" >
......@@ -28,10 +28,10 @@
<proof prover="11"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="dist_symetry.1" proved="true">
<proof prover="11"><result status="valid" time="0.20"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="dist_symetry.2" proved="true">
<proof prover="11"><result status="valid" time="0.16"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="dist_symetry.3" proved="true">
<proof prover="11"><result status="valid" time="0.02"/></proof>
......@@ -79,7 +79,7 @@
</transf>
</goal>
<goal name="min_dist_diff" proved="true">
<proof prover="5" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.33"/></proof>
<proof prover="2" edited="edit_distance_Word_min_dist_diff_1.v"><result status="valid" time="0.33"/></proof>
</goal>
<goal name="min_dist_eps" proved="true">
<transf name="inline_goal" proved="true" >
......@@ -94,7 +94,7 @@
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="min_dist_eps.0.1.1" proved="true">
<proof prover="11"><result status="valid" time="0.56"/></proof>
<proof prover="11"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="min_dist_eps.0.1.2" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......@@ -125,7 +125,7 @@
</theory>
<theory name="EditDistance" proved="true" sum="321168524f7331d73d4b86da8584816c">
<goal name="suffix_length" proved="true">
<proof prover="5" timelimit="5" memlimit="1000" edited="edit_distance_WP_EditDistance_suffix_length_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="2" 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" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -145,10 +145,10 @@
<proof prover="10"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC distance.5" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
<proof prover="11"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC distance.6" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.02"/></proof>
<proof prover="11"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC distance.7" expl="index in array bounds" proved="true">
<proof prover="11"><result status="valid" time="0.03"/></proof>
......
......@@ -2,126 +2,126 @@
<!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.7.1" 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="2" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="0.34"/></proof>
<file name="../euler001.mlw" proved="true">
<theory name="DivModHints" proved="true" sum="4684d234b6fd5ff14ff22c5fd979de0f">
<goal name="mod_div_unique" proved="true">
<proof prover="0" edited="euler001_DivModHints_mod_div_unique_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="mod_succ_1" expl="">
<proof prover="2" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="0.38"/></proof>
<goal name="mod_succ_1" proved="true">
<proof prover="0" edited="euler001_DivModHints_mod_succ_1_1.v"><result status="valid" time="0.38"/></proof>
</goal>
<goal name="mod_succ_2" expl="">
<proof prover="2" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.34"/></proof>
<goal name="mod_succ_2" proved="true">
<proof prover="0" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.34"/></proof>
</goal>
<goal name="div_succ_1" expl="">
<goal name="div_succ_1" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="div_succ_2" expl="">
<goal name="div_succ_2" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.10"/></proof>
<proof prover="4" timelimit="30"><result status="valid" time="0.17" steps="52"/></proof>
</goal>
<goal name="mod2_mul2" expl="">
<goal name="mod2_mul2" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.05" steps="10"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="mod2_mul2_aux" expl="">
<goal name="mod2_mul2_aux" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.02" steps="12"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="mod2_mul2_aux2" expl="">
<goal name="mod2_mul2_aux2" proved="true">
<proof prover="1" timelimit="35"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.03" steps="15"/></proof>
<proof prover="5"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="div2_mul2" expl="">
<goal name="div2_mul2" proved="true">
<proof prover="1"><result status="valid" time="0.06"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="3"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="div2_mul2_aux" expl="">
<goal name="div2_mul2_aux" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="div2_add" expl="">
<goal name="div2_add" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="div2_sub" expl="">
<goal name="div2_sub" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="5" timelimit="5"><result status="valid" time="0.02"/></proof>
</goal>
</theory>
<theory name="TriangularNumbers" sum="1dd8270afe1631351bdfba598382f6b3">
<goal name="tr_mod_2" expl="">
<proof prover="2" memlimit="1000" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.31"/></proof>
<theory name="TriangularNumbers" proved="true" sum="1dd8270afe1631351bdfba598382f6b3">
<goal name="tr_mod_2" proved="true">
<proof prover="0" memlimit="1000" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="tr_repr" expl="">
<goal name="tr_repr" proved="true">
<proof prover="4"><result status="valid" time="0.01" steps="7"/></proof>
</goal>
<goal name="tr_succ" expl="">
<goal name="tr_succ" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="5"/></proof>
</goal>
</theory>
<theory name="SumMultiple" sum="d140aaf24b66c137cc24a25cb64b9e35">
<goal name="mod_15" expl="">
<theory name="SumMultiple" proved="true" sum="d140aaf24b66c137cc24a25cb64b9e35">
<goal name="mod_15" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.13"/></proof>
<proof prover="4"><result status="valid" time="0.17" steps="76"/></proof>
</goal>
<goal name="Closed_formula_0" expl="">
<goal name="Closed_formula_0" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.06" steps="85"/></proof>
</goal>
<goal name="Closed_formula_n" expl="">
<goal name="Closed_formula_n" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="1.46"/></proof>
<proof prover="4" timelimit="10"><result status="valid" time="0.35" steps="55"/></proof>
</goal>
<goal name="Closed_formula_n_3" expl="">
<goal name="Closed_formula_n_3" proved="true">
<proof prover="1" timelimit="10"><result status="valid" time="2.35"/></proof>
</goal>
<goal name="Closed_formula_n_5" expl="">
<goal name="Closed_formula_n_5" proved="true">
<proof prover="1"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="Closed_formula_n_15" expl="">
<goal name="Closed_formula_n_15" proved="true">
<proof prover="1"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="Closed_formula_ind" expl="">
<goal name="Closed_formula_ind" proved="true">
<proof prover="1"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="div_15" expl="">
<goal name="div_15" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="div_5" expl="">
<goal name="div_5" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.01"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="div_3" expl="">
<goal name="div_3" proved="true">
<proof prover="1" timelimit="30"><result status="valid" time="0.02"/></proof>
<proof prover="4"><result status="valid" time="0.01" steps="8"/></proof>
<proof prover="5"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Closed_Formula" expl="">
<proof prover="2" timelimit="30" memlimit="1000" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="0.32"/></proof>
<goal name="Closed_Formula" proved="true">
<proof prover="0" timelimit="30" memlimit="1000" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="0.32"/></proof>
</goal>
</theory>
<theory name="Euler001" sum="4e3f4b4595e4f016609346dd30c13287">
<goal name="VC solve" expl="VC for solve">
<theory name="Euler001" proved="true" sum="4e3f4b4595e4f016609346dd30c13287">
<goal name="VC solve" expl="VC for solve" proved="true">
<proof prover="4"><result status="valid" time="2.18" steps="522"/></proof>