Skip to content

Commit

Permalink
Update proofs
Browse files Browse the repository at this point in the history
  • Loading branch information
@benozol
benozol committed Feb 18, 2020
1 parent b5ce9fd commit 5293d89
Show file tree
Hide file tree
Showing 10 changed files with 2,085 additions and 2,449 deletions.
40 changes: 13 additions & 27 deletions src/concrete/auxiliaries/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,81 +1,67 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="2.2.0" timelimit="1" steplimit="0" memlimit="1000"/>
<why3session shape_version="6">
<prover id="0" name="CVC4" version="1.6" timelimit="5" steplimit="0" memlimit="1000"/>
<prover id="2" name="Alt-Ergo" version="2.3.0" timelimit="1" steplimit="0" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="auxiliaries.mlw"/>
<theory name="TakeDrop" proved="true">
<goal name="drop0" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="4974"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="4975"/></proof>
</goal>
<goal name="drop_all" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="drop_all.0" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="48"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="47"/></proof>
</goal>
</transf>
</goal>
<goal name="nth_drop" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="nth_drop.0" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="10461"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="128"/></proof>
</goal>
</transf>
</goal>
<goal name="take_0" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="7533"/></proof>
<proof prover="2"><result status="valid" time="0.00" steps="2"/></proof>
</goal>
<goal name="take_all" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="take_all.0" proved="true">
<proof prover="0"><result status="valid" time="0.33" steps="57402"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="57"/></proof>
</goal>
</transf>
</goal>
<goal name="take_drop" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="take_drop.0" proved="true">
<proof prover="0"><result status="valid" time="0.50" steps="74924"/></proof>
<proof prover="2"><result status="valid" time="0.02" steps="120"/></proof>
</goal>
</transf>
</goal>
<goal name="take_nth_drop" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="9693"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="6"/></proof>
</goal>
<goal name="take_nth" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="take_nth.0" proved="true">
<transf name="split_vc" proved="true" >
<goal name="take_nth.0.0" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="9531"/></proof>
</goal>
<goal name="take_nth.0.1" proved="true">
<proof prover="0"><result status="valid" time="0.04" steps="15406"/></proof>
</goal>
</transf>
<proof prover="2"><result status="valid" time="0.04" steps="307"/></proof>
</goal>
</transf>
</goal>
<goal name="some_nth" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="some_nth.0" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="13355"/></proof>
<proof prover="2"><result status="valid" time="0.01" steps="96"/></proof>
</goal>
</transf>
</goal>
<goal name="nth_nth" proved="true">
<transf name="induction_ty_lex" proved="true" >
<goal name="nth_nth.0" proved="true">
<transf name="split_vc" proved="true" >
<goal name="nth_nth.0.0" proved="true">
<proof prover="1"><result status="valid" time="0.00" steps="18"/></proof>
</goal>
<goal name="nth_nth.0.1" proved="true">
<proof prover="1"><result status="valid" time="0.01" steps="55"/></proof>
</goal>
</transf>
<proof prover="2"><result status="valid" time="0.01" steps="74"/></proof>
</goal>
</transf>
</goal>
Expand Down
Binary file modified src/concrete/auxiliaries/why3shapes.gz
View file
Binary file not shown.
1,013 changes: 481 additions & 532 deletions src/concrete/interpreter/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified src/concrete/interpreter/why3shapes.gz
View file
Binary file not shown.
266 changes: 105 additions & 161 deletions src/concrete/semantics/why3session.xml
View file

Large diffs are not rendered by default.

Binary file modified src/concrete/semantics/why3shapes.gz
View file
Binary file not shown.
12 changes: 6 additions & 6 deletions src/symbolic/collection/why3session.xml
View file
Original file line number Diff line number Diff line change
@@ -1,8 +1,8 @@
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="8">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="0" memlimit="1000"/>
<why3session shape_version="6">
<prover id="0" name="CVC4" version="1.6" timelimit="1" steplimit="17445" memlimit="1000"/>
<file format="whyml" proved="true">
<path name=".."/><path name="collection.mlw"/>
<theory name="Collection" proved="true">
Expand All @@ -11,7 +11,7 @@
<goal name="union_empty_left.0" proved="true">
<transf name="apply" proved="true" arg1="extensionality">
<goal name="union_empty_left.0.0" expl="apply premises" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="17309"/></proof>
<proof prover="0" steplimit="17309"><result status="valid" time="0.03" steps="17310"/></proof>
</goal>
</transf>
</goal>
Expand All @@ -22,17 +22,17 @@
<goal name="union_empty_right.0" proved="true">
<transf name="apply" proved="true" arg1="extensionality">
<goal name="union_empty_right.0.0" expl="apply premises" proved="true">
<proof prover="0"><result status="valid" time="0.05" steps="17445"/></proof>
<proof prover="0"><result status="valid" time="0.05" steps="17446"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal name="union_left" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="19354"/></proof>
<proof prover="0" steplimit="19354"><result status="valid" time="0.06" steps="19355"/></proof>
</goal>
<goal name="union_right" proved="true">
<proof prover="0"><result status="valid" time="0.06" steps="19502"/></proof>
<proof prover="0" steplimit="19502"><result status="valid" time="0.06" steps="19503"/></proof>
</goal>
</theory>
</file>
Expand Down
Binary file modified src/symbolic/collection/why3shapes.gz
View file
Binary file not shown.
Loading

0 comments on commit 5293d89

Please sign in to comment.