stdlib/list: updated proof session

parent 2f2fdd0a
......@@ -7,8 +7,9 @@
<prover id="2" name="CVC4" version="1.4" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="3" name="Spass" version="3.7" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="4" name="Eprover" version="1.8-001" timelimit="5" steplimit="1" memlimit="1000"/>
<prover id="5" name="Alt-Ergo" version="1.01" timelimit="6" steplimit="0" memlimit="1000"/>
<prover id="6" name="Coq" version="8.4pl6" timelimit="5" steplimit="1" memlimit="4000"/>
<file name="../../../theories/list.why" expanded="true">
<file name="../../../theories/list.why">
<theory name="List" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Length" sum="05caecc0d3ea8074e1ba80a75530a754">
......@@ -33,10 +34,13 @@
</theory>
<theory name="Mem" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
<theory name="Elements" sum="9cccc6673c270c379e44a00d296242c8">
<goal name="elements_Nil">
<proof prover="3"><result status="valid" time="0.51"/></proof>
<proof prover="4"><result status="valid" time="0.02"/></proof>
<theory name="Elements" sum="26b8d407081a0df014fdec443dd1bbf1">
<goal name="elements_mem">
<transf name="induction_ty_lex">
<goal name="elements_mem.1" expl="1.">
<proof prover="5"><result status="valid" time="0.00" steps="57"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Nth" sum="d41d8cd98f00b204e9800998ecf8427e">
......
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