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

lcp: proofs with Coq 8.3pl4

parent e3bc6d2e
......@@ -28,7 +28,7 @@
<prover
id="6"
name="Coq"
version="8.4"/>
version="8.3pl4"/>
<prover
id="7"
name="Eprover"
......@@ -58,14 +58,14 @@
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="89" loccnumb="7" loccnume="10"
verified="true"
expanded="true">
expanded="false">
<goal
name="not_common_prefix_if_last_char_are_different"
locfile="../verifythis_fm2012_lcp.mlw"
loclnum="104" loccnumb="6" loccnume="50"
sum="d031ecf9b2e0645dc74ea7af771bc99c"
proved="true"
expanded="true"
expanded="false"
shape="ais_common_prefixV0V1V2ainfix +V3c1NIainfix =amixfix []V0ainfix +V1V3amixfix []V0ainfix +V2V3NAainfix &lt;ainfix +V2V3alengthV0Aainfix &lt;ainfix +V1V3alengthV0Aainfix &lt;=c0V3F">
<proof
prover="0"
......@@ -7496,8 +7496,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.09"/>
......@@ -7596,8 +7596,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.40"/>
......@@ -7696,8 +7696,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.38"/>
......@@ -7796,8 +7796,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.08"/>
......@@ -7896,8 +7896,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -7996,8 +7996,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -8096,8 +8096,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -8196,8 +8196,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -8296,8 +8296,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -8396,8 +8396,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.08"/>
......@@ -8496,8 +8496,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.00"/>
......@@ -8596,8 +8596,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -8696,8 +8696,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.03"/>
......@@ -8796,8 +8796,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.00"/>
......@@ -8896,8 +8896,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.02"/>
......@@ -8996,8 +8996,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.07"/>
......@@ -9096,8 +9096,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -9196,8 +9196,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -9296,8 +9296,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -9396,8 +9396,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -9496,8 +9496,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.08"/>
......@@ -9596,8 +9596,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.84"/>
......@@ -9696,8 +9696,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.09"/>
......@@ -9796,8 +9796,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.03"/>
......@@ -9896,8 +9896,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.08"/>
......@@ -9996,8 +9996,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.08"/>
......@@ -10096,8 +10096,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.03"/>
......@@ -10196,8 +10196,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.27"/>
......@@ -10296,8 +10296,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -10396,8 +10396,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="unknown" time="10.00"/>
......@@ -10496,8 +10496,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -10596,8 +10596,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -10696,8 +10696,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -10796,8 +10796,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
......@@ -10896,8 +10896,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -10996,8 +10996,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
......@@ -11096,8 +11096,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.12"/>
......@@ -11196,8 +11196,8 @@
</proof>
<proof
prover="8"
timelimit="10"
memlimit="1000"
timelimit="5"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
......@@ -11399,7 +11399,7 @@
edited="verifythis_fm2012_lcp_SuffixArray_permut_permutation_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.72"/>
<result status="valid" time="1.22"/>
</proof>
<proof
prover="7"
......@@ -16162,7 +16162,7 @@
edited="verifythis_fm2012_lcp_LRS_WP_parameter_lrs_10.v"
obsolete="false"
archived="false">
<result status="valid" time="1.39"/>
<result status="valid" time="0.88"/>
</proof>
<proof
prover="7"
......@@ -16571,7 +16571,7 @@
edited="verifythis_fm2012_lcp_LRS_WP_parameter_lrs_12.v"
obsolete="false"
archived="false">
<result status="valid" time="1.21"/>
<result status="valid" time="0.73"/>
</proof>
<proof
prover="7"
......
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