Commit 78c4e12c authored by MARCHE Claude's avatar MARCHE Claude

update proofs to Coq 8.7.1

parent 53b8fd13
......@@ -2,7 +2,7 @@
<!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"/>
......@@ -135,13 +135,13 @@
<proof prover="14"><result status="valid" time="0.17"/></proof>
</goal>
<goal name="Tan_pi_4" proved="true">
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_4_1.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="Tan_pi_3" proved="true">
<proof prover="1" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
<proof prover="0" edited="real_TrigonometryTest_Tan_pi_3_1.v"><result status="valid" time="0.43"/></proof>
</goal>
<goal name="Atan_1" proved="true">
<proof prover="1" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
<proof prover="0" edited="real_TrigonometryTest_Atan_1_1.v"><result status="valid" time="0.41"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,10 +4,10 @@
<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="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../compiler.mlw" proved="true">
<theory name="Compile_aexpr" proved="true" sum="407d77668df70f8af94774aee7f39cf3">
<goal name="WP_parameter compile_aexpr" expl="VC for compile_aexpr" proved="true">
......@@ -1005,7 +1005,7 @@
<proof prover="0"><result status="valid" time="0.12" steps="40"/></proof>
</goal>
<goal name="WP_parameter compile_com.46" expl="precondition" proved="true">
<proof prover="2" edited="compiler_Compile_com_WP_parameter_compile_com_1.v"><result status="valid" time="2.27"/></proof>
<proof prover="6" edited="compiler_Compile_com_WP_parameter_compile_com_1.v"><result status="valid" time="1.69"/></proof>
</goal>
<goal name="WP_parameter compile_com.47" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.14" steps="40"/></proof>
......
......@@ -3,13 +3,13 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="30" steplimit="0" memlimit="1500"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="1" steplimit="0" memlimit="0"/>
<prover id="2" name="Eprover" version="2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="3" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1500"/>
<prover id="4" name="Z3" version="3.2" timelimit="30" steplimit="0" memlimit="1500"/>
<prover id="5" name="Z3" version="4.5.0" timelimit="5" steplimit="0" memlimit="1500"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="Coq" version="8.7.1" timelimit="1" steplimit="0" memlimit="0"/>
<file name="../euler001.mlw" proved="true">
<theory name="DivModHints" proved="true" sum="6f77cd46f4f6ca514a80124063f6a33c">
<goal name="mod_div_unique" proved="true">
......@@ -79,7 +79,7 @@
<goal name="mod_succ_1.0.1.1.0.0.0.0.1" expl="false case" proved="true">
<transf name="assert" proved="true" arg1="(x = y * q + (r-1))">
<goal name="mod_succ_1.0.1.1.0.0.0.0.1.0" proved="true">
<proof prover="7" timelimit="1"><result status="valid" time="0.01"/></proof>
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="mod_succ_1.0.1.1.0.0.0.0.1.1" expl="false case" proved="true">
<proof prover="3" memlimit="2000"><result status="valid" time="2.19" steps="53"/></proof>
......@@ -103,7 +103,7 @@
</transf>
</goal>
<goal name="mod_succ_2" proved="true">
<proof prover="1" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.37"/></proof>
<proof prover="8" edited="euler001_DivModHints_mod_succ_2_1.v"><result status="valid" time="0.37"/></proof>
</goal>
<goal name="div_succ_1" proved="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
......@@ -149,7 +149,7 @@
</theory>
<theory name="TriangularNumbers" proved="true" sum="5dd3402674ce736b7bf98870de3440c5">
<goal name="tr_mod_2" proved="true">
<proof prover="1" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.31"/></proof>
<proof prover="8" edited="euler001_TriangularNumbers_tr_mod_2_1.v"><result status="valid" time="0.31"/></proof>
</goal>
<goal name="tr_repr" proved="true">
<proof prover="3"><result status="valid" time="0.01" steps="7"/></proof>
......@@ -203,7 +203,7 @@
<proof prover="4"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="Closed_Formula" proved="true">
<proof prover="1" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="0.36"/></proof>
<proof prover="8" edited="euler001_SumMultiple_Closed_Formula_1.v"><result status="valid" time="0.36"/></proof>
</goal>
</theory>
<theory name="Euler001" proved="true" sum="ac5e739bc4723e5c8ba7bae0a1b7655c">
......
......@@ -2,9 +2,9 @@
<!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="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="5" steplimit="0" memlimit="4000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="4" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="7" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="8" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="1000"/>
......@@ -455,12 +455,12 @@
<proof prover="1"><result status="valid" time="0.00" steps="5"/></proof>
</goal>
<goal name="WP_parameter logfib.3" expl="postcondition" proved="true">
<proof prover="3" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="0.47"/></proof>
<proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_WP_parameter_logfib_1.v"><result status="valid" time="0.47"/></proof>
</goal>
</transf>
</goal>
<goal name="fib_m" proved="true">
<proof prover="3" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="0" edited="fibonacci_WP_FibonacciLogarithmic_fib_m_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="WP_parameter fibo" expl="VC for fibo" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="6"/></proof>
......
......@@ -4,12 +4,12 @@
<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="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../hashtbl_impl.mlw" proved="true">
<theory name="HashtblImpl" proved="true" sum="30f5106c44030a9cdf3c12f15983519e">
<theory name="HashtblImpl" proved="true" sum="331f1b2d1a0952e60733252f44b4585b">
<goal name="bucket_bounds" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="16"/></proof>
</goal>
......@@ -150,7 +150,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="17"/></proof>
</goal>
<goal name="WP_parameter find.1" expl="postcondition" proved="true">
<proof prover="2" edited="hashtbl_impl_HashtblImpl_WP_parameter_find_1.v"><result status="valid" time="0.34"/></proof>
<proof prover="6" edited="hashtbl_impl_HashtblImpl_WP_parameter_find_1.v"><result status="valid" time="0.34"/></proof>
</goal>
</transf>
</goal>
......@@ -181,7 +181,7 @@
<proof prover="4"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter remove.1" expl="postcondition" proved="true">
<proof prover="2" edited="hashtbl_impl_HashtblImpl_WP_parameter_remove_2.v"><result status="valid" time="0.35"/></proof>
<proof prover="6" edited="hashtbl_impl_HashtblImpl_WP_parameter_remove_2.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="WP_parameter remove.2" expl="index in array bounds" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="5"/></proof>
......@@ -237,7 +237,7 @@
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter add.3" expl="type invariant" proved="true">
<proof prover="2" edited="hashtbl_impl_HashtblImpl_WP_parameter_add_1.v"><result status="valid" time="2.74"/></proof>
<proof prover="6" edited="hashtbl_impl_HashtblImpl_WP_parameter_add_1.v"><result status="valid" time="2.74"/></proof>
</goal>
<goal name="WP_parameter add.4" expl="type invariant" proved="true">
<transf name="inline_all" proved="true" >
......
......@@ -5,7 +5,6 @@
<prover id="0" name="CVC4" version="1.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="4000"/>
<prover id="2" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.01" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="2.19" timelimit="10" steplimit="0" memlimit="0"/>
......@@ -14,10 +13,11 @@
<prover id="9" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="10" name="Alt-Ergo" version="0.95.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="11" name="Z3" version="4.3.2" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="12" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../knuth_prime_numbers.mlw" proved="true">
<theory name="PrimeNumbers" proved="true" sum="6550cbedc0c19c9611f6cb6986837c1e">
<goal name="exists_prime" proved="true">
<proof prover="3" timelimit="10" memlimit="0" edited="knuth_prime_numbers_WP_PrimeNumbers_exists_prime_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="12" timelimit="10" memlimit="0" edited="knuth_prime_numbers_WP_PrimeNumbers_exists_prime_1.v"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="WP_parameter prime_numbers" expl="VC for prime_numbers" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -58,7 +58,7 @@
<proof prover="1" memlimit="1000"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.10" expl="assertion" proved="true">
<proof prover="3" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_2.v"><result status="valid" time="0.65"/></proof>
<proof prover="12" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_2.v"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.11" expl="variant decrease" proved="true">
<proof prover="1"><result status="valid" time="0.02" steps="33"/></proof>
......@@ -79,7 +79,7 @@
<proof prover="1" memlimit="1000"><result status="valid" time="0.02" steps="33"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.14.1" expl="VC for prime_numbers" proved="true">
<proof prover="3" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_3.v"><result status="valid" time="0.42"/></proof>
<proof prover="12" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_3.v"><result status="valid" time="0.42"/></proof>
</goal>
</transf>
</goal>
......@@ -115,7 +115,7 @@
<proof prover="5"><result status="valid" time="0.01" steps="32"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.22.1" expl="VC for prime_numbers" proved="true">
<proof prover="3" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_5.v"><result status="valid" time="0.48"/></proof>
<proof prover="12" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_5.v"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
</goal>
......@@ -138,7 +138,7 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.29" expl="assertion" proved="true">
<proof prover="3" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_4.v"><result status="valid" time="1.12"/></proof>
<proof prover="12" edited="knuth_prime_numbers_PrimeNumbers_WP_parameter_prime_numbers_4.v"><result status="valid" time="1.12"/></proof>
</goal>
<goal name="WP_parameter prime_numbers.30" expl="postcondition" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="33"/></proof>
......
......@@ -3,15 +3,15 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC3" version="2.4.1" timelimit="36" steplimit="0" memlimit="1000"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="4.4.1" alternative="noBV" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="36" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="8" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../koda_ruskey.mlw" proved="true">
<theory name="KodaRuskey_Spec" proved="true" sum="5610b955c7ce4dfe99ceff63113fcab2">
<theory name="KodaRuskey_Spec" proved="true" sum="dddd314edb7b7b360dbf8fce57a65e85">
<goal name="size_forest_nonneg" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="size_forest_nonneg.0" proved="true">
......@@ -27,7 +27,7 @@
</transf>
</goal>
</theory>
<theory name="Lemmas" proved="true" sum="54b6ee224ed5345958f7ba5b41a86f21">
<theory name="Lemmas" proved="true" sum="6c8a523509a689028db8d82c3be6ed4d">
<goal name="mem_app" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="mem_app.0" proved="true">
......@@ -501,7 +501,7 @@
<proof prover="4" timelimit="11"><result status="valid" time="0.01" steps="13"/></proof>
</goal>
<goal name="WP_parameter sub_valid_coloring_white.9" expl="postcondition" proved="true">
<proof prover="1" edited="koda_ruskey_KodaRuskey_Spec_WP_parameter_sub_valid_coloring_white_1.v"><result status="valid" time="2.37"/></proof>
<proof prover="8" edited="koda_ruskey_KodaRuskey_Spec_WP_parameter_sub_valid_coloring_white_1.v"><result status="valid" time="2.37"/></proof>
</goal>
</transf>
</goal>
......@@ -575,7 +575,7 @@
</transf>
</goal>
</theory>
<theory name="KodaRuskey" proved="true" sum="13b8895a9dd806dbd900fdf73e535dd2">
<theory name="KodaRuskey" proved="true" sum="ca57d555c54836e62b2126156102821e">
<goal name="WP_parameter enum" expl="VC for enum" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter enum.0" expl="unreachable point" proved="true">
......
......@@ -4,14 +4,14 @@
<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="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="MetiTarski" version="2.4" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Z3" version="3.2" timelimit="3" steplimit="0" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../triangle_inequality.why" proved="true">
<theory name="CauchySchwarzInequality" proved="true" sum="028eeb3c0da238696d03921fac93ef00">
<theory name="CauchySchwarzInequality" proved="true" sum="ee5bf3c314caefca0d3c63fad9d0ed76">
<goal name="norm2_pos" proved="true">
<proof prover="4"><result status="valid" time="0.04"/></proof>
<proof prover="6"><result status="valid" time="0.01"/></proof>
......@@ -62,8 +62,8 @@
<proof prover="4"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="CauchySchwarz_aux_non_null" proved="true">
<proof prover="2" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.42"/></proof>
<proof prover="4"><result status="valid" time="0.03"/></proof>
<proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_aux_non_null_1.v"><result status="valid" time="0.42"/></proof>
</goal>
<goal name="norm_null" proved="true">
<proof prover="4"><result status="valid" time="0.06"/></proof>
......@@ -94,7 +94,7 @@
<proof prover="4"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="CauchySchwarz" proved="true">
<proof prover="2" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.48"/></proof>
<proof prover="8" edited="triangle_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"><result status="valid" time="0.48"/></proof>
</goal>
</theory>
<theory name="TriangleInequality" proved="true" sum="c81c1e0efd1ec340bc35ab1ce72e8bb8">
......@@ -107,7 +107,7 @@
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="triangle" proved="true">
<proof prover="2" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.40"/></proof>
<proof prover="8" edited="triangle_inequality_TriangleInequality_triangle_1.v"><result status="valid" time="0.40"/></proof>
</goal>
</theory>
</file>
......
......@@ -3,15 +3,15 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" 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="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Z3" version="3.2" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="5" name="Z3" version="4.3.2" timelimit="10" steplimit="0" memlimit="1000"/>
<prover id="6" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../maximum_subarray.mlw" proved="true">
<theory name="Spec" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Algo1" proved="true" sum="a89d18ca40dcc22fa9868a59c354857f">
<theory name="Algo1" proved="true" sum="a81e0a8022fa5f4d1f1f107f8cedc54a">
<goal name="WP_parameter maximum_subarray" expl="VC for maximum_subarray" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter maximum_subarray.0" expl="postcondition" proved="true">
......@@ -162,7 +162,7 @@
</transf>
</goal>
</theory>
<theory name="Algo2" proved="true" sum="0b49164cba75630b08a8bc1e7da63fdb">
<theory name="Algo2" proved="true" sum="a7e2211418f00a111bd43b8aa5d27c39">
<goal name="WP_parameter maximum_subarray" expl="VC for maximum_subarray" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter maximum_subarray.0" expl="postcondition" proved="true">
......@@ -240,7 +240,7 @@
</transf>
</goal>
</theory>
<theory name="Algo3" proved="true" sum="4454f683cfdd6f475d2948e91cb5b69d">
<theory name="Algo3" proved="true" sum="0f330de659703291ef1cd8786666a8e8">
<goal name="WP_parameter maximum_subarray_rec" expl="VC for maximum_subarray_rec" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter maximum_subarray_rec.0" expl="postcondition" proved="true">
......@@ -476,7 +476,7 @@
<proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
</goal>
<goal name="WP_parameter maximum_subarray_rec.76" expl="loop invariant preservation" proved="true">
<proof prover="1" edited="maximum_subarray_Algo3_WP_parameter_maximum_subarray_rec_1.v"><result status="valid" time="0.48"/></proof>
<proof prover="6" edited="maximum_subarray_Algo3_WP_parameter_maximum_subarray_rec_1.v"><result status="valid" time="0.48"/></proof>
</goal>
<goal name="WP_parameter maximum_subarray_rec.77" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -485,7 +485,7 @@
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="WP_parameter maximum_subarray_rec.79" expl="loop invariant preservation" proved="true">
<proof prover="1" edited="maximum_subarray_Algo3_WP_parameter_maximum_subarray_rec_3.v"><result status="valid" time="0.46"/></proof>
<proof prover="6" edited="maximum_subarray_Algo3_WP_parameter_maximum_subarray_rec_3.v"><result status="valid" time="0.46"/></proof>
</goal>
<goal name="WP_parameter maximum_subarray_rec.80" expl="loop invariant preservation" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
......@@ -548,7 +548,7 @@
</transf>
</goal>
</theory>
<theory name="Algo4" proved="true" sum="034b628d7824d5af3d43df821ebda33e">
<theory name="Algo4" proved="true" sum="355a377a2fc13afbe47e9470e692961b">
<goal name="WP_parameter maximum_subarray" expl="VC for maximum_subarray" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter maximum_subarray.0" expl="postcondition" proved="true">
......@@ -648,7 +648,7 @@
</transf>
</goal>
</theory>
<theory name="Algo5" proved="true" sum="168ca956ed7ab79235ebc43d52e0f472">
<theory name="Algo5" proved="true" sum="afe0499b30cc61a8fedc416adfa99157">
<goal name="WP_parameter maximum_subarray" expl="VC for maximum_subarray" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter maximum_subarray.0" expl="postcondition" proved="true">
......
......@@ -5,11 +5,11 @@
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Coq" version="8.6.1" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Alt-Ergo" version="1.01" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="6" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="7" name="Z3" version="4.3.2" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="8" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../residual.mlw" proved="true">
<theory name="Residuals" proved="true" sum="751887864908ee3d56cf65a325b5bea0">
<goal name="WP_parameter accepts_epsilon" expl="VC for accepts_epsilon" proved="true">
......@@ -61,7 +61,7 @@
</transf>
</goal>
<goal name="inversion_mem_star_gen" proved="true">
<proof prover="3" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.28"/></proof>
<proof prover="8" edited="residual_Residuals_inversion_mem_star_gen_1.v"><result status="valid" time="0.28"/></proof>
<transf name="induction_arg_pr" proved="true" arg1="H2">
<goal name="inversion_mem_star_gen.0" proved="true">
<proof prover="5"><result status="valid" time="0.02"/></proof>
......@@ -155,7 +155,7 @@
<proof prover="7"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="WP_parameter residual.8" expl="postcondition" proved="true">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="0.35"/></proof>
<proof prover="8" edited="residual_Residuals_WP_parameter_residual_1.v"><result status="valid" time="0.35"/></proof>
</goal>
<goal name="WP_parameter residual.9" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="54"/></proof>
......@@ -164,7 +164,7 @@
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.10" expl="postcondition" proved="true">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.39"/></proof>
<proof prover="8" edited="residual_Residuals_WP_parameter_residual_3.v"><result status="valid" time="0.39"/></proof>
</goal>
<goal name="WP_parameter residual.11" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="52"/></proof>
......@@ -173,7 +173,7 @@
<proof prover="7"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="WP_parameter residual.12" expl="postcondition" proved="true">
<proof prover="3" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.34"/></proof>
<proof prover="8" edited="residual_Residuals_WP_parameter_residual_2.v"><result status="valid" time="0.34"/></proof>
</goal>
</transf>
</goal>
......
......@@ -3,12 +3,12 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="2250"/>
<prover id="1" name="Coq" version="8.6.1" timelimit="2" steplimit="0" memlimit="0"/>
<prover id="2" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="2250"/>
<prover id="3" name="CVC4" version="1.4" timelimit="5" steplimit="0" memlimit="2250"/>
<prover id="4" name="Alt-Ergo" version="1.30" timelimit="5" steplimit="0" memlimit="2250"/>
<prover id="5" name="Z3" version="4.4.0" timelimit="6" steplimit="0" memlimit="2250"/>
<file name="../../../modules/array.mlw">
<prover id="6" name="Coq" version="8.7.1" timelimit="2" steplimit="0" memlimit="0"/>
<file name="../../../modules/array.mlw" proved="true">
<theory name="Array" proved="true" sum="a4386c74c7fc0ab46ab3dd9d9d5cae40">
<goal name="WP_parameter defensive_get" expl="VC for defensive_get" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
......@@ -34,12 +34,12 @@
</theory>
<theory name="ArrayExchange" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="ArrayPermut" sum="4df642c6a5d352ea5ec0e76c805c8f49">
<goal name="exchange_permut_sub">
<proof prover="1" timelimit="4" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="1.53"/></proof>
<theory name="ArrayPermut" proved="true" sum="4df642c6a5d352ea5ec0e76c805c8f49">
<goal name="exchange_permut_sub" proved="true">
<proof prover="6" timelimit="4" edited="array_ArrayPermut_exchange_permut_sub_1.v"><result status="valid" time="1.53"/></proof>
</goal>
<goal name="permut_sub_weakening" proved="true">
<proof prover="1" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="0.50"/></proof>
<proof prover="6" edited="array_ArrayPermut_permut_sub_weakening_2.v"><result status="valid" time="0.50"/></proof>
</goal>
<goal name="exchange_permut_all" proved="true">
<proof prover="3"><result status="valid" time="0.06"/></proof>
......@@ -62,7 +62,7 @@
<proof prover="4"><result status="valid" time="0.01" steps="34"/></proof>
</goal>
</theory>
<theory name="ToSeq" proved="true" sum="16189e2571a1238f4124921c02a79c14">
<theory name="ToSeq" proved="true" sum="094a325952a512c87b367dbc9505daa4">
<goal name="WP_parameter to_seq_length" expl="VC for to_seq_length" proved="true">
<transf name="split_goal_wp" proved="true" >
<goal name="WP_parameter to_seq_length.0" expl="variant decrease" proved="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="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"/>
<file name="../coq-interval.why" proved="true">
<theory name="P" proved="true" sum="1e4fe85b7d4e5d74721c865ee586cec8">
<goal name="pow_eps2_max_int" proved="true">
<proof prover="1" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="0.83"/></proof>
<proof prover="0" edited="coqmninterval_P_pow_eps2_max_int_1.v"><result status="valid" time="0.83"/></proof>
</goal>
</theory>
</file>
......
......@@ -4,14 +4,14 @@
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.99.1" timelimit="5" steplimit="0" memlimit="0"/>
<prover id="1" name="CVC3" version="2.4.1" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="2" name="Coq" version="8.6.1" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="3" name="Spass" version="3.7" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="4" name="Z3" version="3.2" timelimit="10" steplimit="0" memlimit="0"/>
<prover id="5" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="6" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="7" name="Vampire" version="0.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="8" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../vstte12_combinators.mlw" proved="true">
<theory name="Combinators" proved="true" sum="4f97418a18367ae189310c09e6f5f92b">
<theory name="Combinators" proved="true" sum="6bf4759b565894459404caff601a463c">
<goal name="red_left" proved="true">
<proof prover="4"><result status="valid" time="3.80"/></proof>
</goal>
......@@ -19,10 +19,10 @@
<proof prover="4"><result status="valid" time="3.82"/></proof>
</goal>
<goal name="red_star_left" proved="true">
<proof prover="2" timelimit="10" memlimit="0" edited="vstte12_combinators_WP_Combinators_red_star_left_1.v"><result status="valid" time="0.27"/></proof>
<proof prover="8" timelimit="10" memlimit="0" edited="vstte12_combinators_WP_Combinators_red_star_left_1.v"><result status="valid" time="0.27"/></proof>
</goal>
<goal name="red_star_right" proved="true">
<proof prover="2" timelimit="10" memlimit="0" edited="vstte12_combinators_WP_Combinators_red_star_right_1.v"><result status="valid" time="0.28"/></proof>
<proof prover="8" timelimit="10" memlimit="0" edited="vstte12_combinators_WP_Combinators_red_star_right_1.v"><result status="valid" time="0.28"/></proof>
</goal>
<goal name="WP_parameter reduction" expl="VC for reduction" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -96,16 +96,16 @@
<proof prover="0" memlimit="1000"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="reducible_or_value" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_reducible_or_value_1.v"><result status="valid" time="0.69"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_reducible_or_value_1.v"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="irreducible_is_value" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_irreducible_is_value_1.v"><result status="valid" time="1.76"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_irreducible_is_value_1.v"><result status="valid" time="1.76"/></proof>
</goal>
<goal name="only_K_reduces" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_only_K_reduces_1.v"><result status="valid" time="0.69"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_only_K_reduces_1.v"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="size_nonneg" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_size_nonneg_1.v"><result status="valid" time="0.36"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_size_nonneg_1.v"><result status="valid" time="0.36"/></proof>
</goal>
<goal name="WP_parameter reduction2" expl="VC for reduction2" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -194,13 +194,13 @@
<proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
</goal>
<goal name="only_K_ks" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_only_K_ks_1.v"><result status="valid" time="0.30"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_only_K_ks_1.v"><result status="valid" time="0.30"/></proof>
</goal>
<goal name="ks_inversion" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
</goal>
<goal name="ks_injective" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_ks_injective_1.v"><result status="valid" time="0.71"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_ks_injective_1.v"><result status="valid" time="0.71"/></proof>
</goal>
<goal name="WP_parameter reduction3" expl="VC for reduction3" proved="true">
<transf name="split_goal_wp" proved="true" >
......@@ -231,10 +231,10 @@
<proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
</goal>
<goal name="WP_parameter reduction3.4.1" expl="VC for reduction3" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_3.v"><result status="valid" time="1.50"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_3.v"><result status="valid" time="1.50"/></proof>
</goal>
<goal name="WP_parameter reduction3.4.2" expl="VC for reduction3" proved="true">
<proof prover="2" memlimit="4000" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_4.v"><result status="valid" time="0.78"/></proof>
<proof prover="8" memlimit="4000" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_4.v"><result status="valid" time="0.78"/></proof>
</goal>
</transf>
</goal>
......@@ -242,7 +242,7 @@
<proof prover="1"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="WP_parameter reduction3.6" expl="postcondition" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_6.v"><result status="valid" time="1.07"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_6.v"><result status="valid" time="1.07"/></proof>
</goal>
<goal name="WP_parameter reduction3.7" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.09"/></proof>
......@@ -255,7 +255,7 @@
<proof prover="4"><result status="valid" time="0.13"/></proof>
</goal>
<goal name="WP_parameter reduction3.8.1" expl="VC for reduction3" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_5.v"><result status="valid" time="0.68"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_5.v"><result status="valid" time="0.68"/></proof>
</goal>
<goal name="WP_parameter reduction3.8.2" expl="VC for reduction3" proved="true">
<proof prover="0"><result status="valid" time="0.10" steps="142"/></proof>
......@@ -266,16 +266,16 @@
<proof prover="1"><result status="valid" time="0.07"/></proof>
</goal>
<goal name="WP_parameter reduction3.10" expl="postcondition" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_9.v"><result status="valid" time="1.86"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_9.v"><result status="valid" time="1.86"/></proof>
</goal>
<goal name="WP_parameter reduction3.11" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="WP_parameter reduction3.12" expl="precondition" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_7.v"><result status="valid" time="0.68"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_7.v"><result status="valid" time="0.94"/></proof>
</goal>
<goal name="WP_parameter reduction3.13" expl="postcondition" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_8.v"><result status="valid" time="0.88"/></proof>
<proof prover="8" edited="vstte12_combinators_WP_Combinators_WP_parameter_reduction3_8.v"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="WP_parameter reduction3.14" expl="unreachable point" proved="true">
<proof prover="0"><result status="valid" time="0.08" steps="114"/></proof>
......@@ -285,10 +285,10 @@
</transf>
</goal>
<goal name="ks_value" proved="true">
<proof prover="2" edited="vstte12_combinators_WP_Combinators_ks_value_1.v"><result status="valid" time="0.34"/></proof>