Commit 1a38eac5 authored by MARCHE Claude's avatar MARCHE Claude

session updated

parent cb488374
......@@ -2,8 +2,9 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="2" steplimit="0" memlimit="1000"/>
<prover id="0" name="Alt-Ergo" version="1.30" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="2" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
<file name="../demo-itp.mlw">
<theory name="M" proved="true" sum="d41d8cd98f00b204e9800998ecf8427e">
</theory>
......@@ -41,31 +42,42 @@
<goal name="g2">
</goal>
</theory>
<theory name="Power" sum="1d85f0040f747fee402221dbf53ac9a8">
<theory name="Power" sum="53cae56d1419c17b838380453eb24720">
<goal name="power_1" proved="true">
<proof prover="1"><result status="valid" time="0.17"/></proof>
<transf name="replace" proved="true" arg1="1" arg2="0+1" arg3="power_1">
<goal name="power_1.0" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="power_1.1" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
</goal>
<goal name="sqrt4_256" proved="true">
<transf name="exists" proved="true" arg1="4">
<goal name="sqrt4_256.0" proved="true">
<proof prover="1"><result status="valid" time="0.04"/></proof>
<proof prover="2"><result status="unknown" time="1.00"/></proof>
</goal>
</transf>
</goal>
<goal name="sqrt4_256">
</goal>
<goal name="power_sum" proved="true">
<transf name="induction" proved="true" arg1="n" arg2="0">
<transf name="induction" proved="true" arg1="n">
<goal name="power_sum.0" proved="true">
<proof prover="1"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="unknown" time="1.00"/></proof>
</goal>
<goal name="power_sum.1" proved="true">
<proof prover="0" timelimit="1"><result status="valid" time="0.87" steps="15"/></proof>
<proof prover="0"><result status="valid" time="0.87" steps="15"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="1.01"/></proof>
</goal>
</transf>
</goal>
<goal name="power_0_left">
<goal name="power_0_left" proved="true">
<transf name="replace" proved="true" arg1="n" arg2="(n-1+1)">
<goal name="power_0_left.0" proved="true">
<proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="1"><result status="timeout" time="1.00"/></proof>
<proof prover="2"><result status="unknown" time="0.98"/></proof>
</goal>
<goal name="power_0_left.1" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
<goal name="little_fermat_3">
</goal>
......
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