Commit b8b42d57 authored by MARCHE Claude's avatar MARCHE Claude

add missing proof in examples/stdlib

parent 4baede19
......@@ -3,6 +3,7 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.99.1" timelimit="5" memlimit="1000"/>
<file name="../../../theories/bintree.why" expanded="true">
<theory name="Tree" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......@@ -31,8 +32,13 @@
</transf>
</goal>
</theory>
<theory name="Height" sum="dfe6f2e0201e3e30f92c12e8d2d8b3ee" expanded="true">
<theory name="Height" sum="94f804e09f4fba3f0004208e1a3017a5" expanded="true">
<goal name="height_nonneg" expanded="true">
<transf name="induction_ty_lex" expanded="true">
<goal name="height_nonneg.1" expl="1.">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
</transf>
</goal>
</theory>
<theory name="Inorder" 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