Commit ca7f4394 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

euler002: proofs with Coq 8.3pl4

parent 897a183c
...@@ -28,7 +28,7 @@ ...@@ -28,7 +28,7 @@
<prover <prover
id="6" id="6"
name="Coq" name="Coq"
version="8.4"/> version="8.3pl4"/>
<prover <prover
id="7" id="7"
name="Z3" name="Z3"
...@@ -68,14 +68,14 @@ ...@@ -68,14 +68,14 @@
locfile="../euler002.mlw" locfile="../euler002.mlw"
loclnum="94" loccnumb="7" loccnume="18" loclnum="94" loccnumb="7" loccnume="18"
verified="true" verified="true"
expanded="false"> expanded="true">
<goal <goal
name="fib_even" name="fib_even"
locfile="../euler002.mlw" locfile="../euler002.mlw"
loclnum="100" loccnumb="8" loccnume="16" loclnum="100" loccnumb="8" loccnume="16"
sum="d486dc78b6862c9ad860b8f66867d892" sum="d486dc78b6862c9ad860b8f66867d892"
proved="true" proved="true"
expanded="false" expanded="true"
shape="ainfix =amodV0c3c1qainfix =amodafibV0c2c0Iainfix &gt;=V0c0F"> shape="ainfix =amodV0c3c1qainfix =amodafibV0c2c0Iainfix &gt;=V0c0F">
<proof <proof
prover="6" prover="6"
...@@ -84,7 +84,7 @@ ...@@ -84,7 +84,7 @@
edited="euler002_FibOnlyEven_fib_even_1.v" edited="euler002_FibOnlyEven_fib_even_1.v"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="1.95"/> <result status="valid" time="1.61"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -93,7 +93,7 @@ ...@@ -93,7 +93,7 @@
loclnum="114" loccnumb="8" loccnume="24" loclnum="114" loccnumb="8" loccnume="24"
sum="3a38e9bb92fcd974a8d29c247220a669" sum="3a38e9bb92fcd974a8d29c247220a669"
proved="true" proved="true"
expanded="false" expanded="true"
shape="ainfix =afib_evenV0afibainfix +ainfix *c3V0c1Iainfix &gt;=V0c0F"> shape="ainfix =afib_evenV0afibainfix +ainfix *c3V0c1Iainfix &gt;=V0c0F">
<proof <proof
prover="6" prover="6"
...@@ -102,7 +102,7 @@ ...@@ -102,7 +102,7 @@
edited="euler002_FibOnlyEven_fib_even_correct_1.v" edited="euler002_FibOnlyEven_fib_even_correct_1.v"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="1.32"/> <result status="valid" time="0.89"/>
</proof> </proof>
</goal> </goal>
</theory> </theory>
...@@ -111,7 +111,7 @@ ...@@ -111,7 +111,7 @@
locfile="../euler002.mlw" locfile="../euler002.mlw"
loclnum="119" loccnumb="7" loccnume="12" loclnum="119" loccnumb="7" loccnume="12"
verified="true" verified="true"
expanded="false"> expanded="true">
<goal <goal
name="WP_parameter f" name="WP_parameter f"
locfile="../euler002.mlw" locfile="../euler002.mlw"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment