vstte12_tree_reconstruction: updated proof on moloch

examples/vstte12_tree_reconstruction/why3session.xml

@@ -8,7 +8,7 @@
 <prover id="5" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="8" name="Z3" version="4.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
-<file name="../vstte12_tree_reconstruction.mlw">
+<file name="../vstte12_tree_reconstruction.mlw" proved="true">
 <theory name="Tree" proved="true">
  <goal name="VC depths" expl="VC for depths" proved="true">
  <transf name="split_goal_right" proved="true" >
@@ -94,7 +94,7 @@
  <proof prover="4" timelimit="1"><result status="valid" time="0.56"/></proof>
  </goal>
 </theory>
-<theory name="ZipperBased">
+<theory name="ZipperBased" proved="true">
  <goal name="forest_depths_append" proved="true">
  <proof prover="5" timelimit="10" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_forest_depths_append_1.v"><result status="valid" time="0.30"/></proof>
  </goal>
@@ -127,10 +127,10 @@
  </transf>
  </goal>
  <goal name="key_lemma" proved="true">
- <proof prover="1" edited="vstte12_tree_reconstruction_ZipperBased_key_lemma_2.v"><result status="valid" time="2.27"/></proof>
+ <proof prover="5" edited="vstte12_tree_reconstruction_ZipperBased_key_lemma_2.v"><result status="valid" time="2.27"/></proof>
  </goal>
- <goal name="right_nil">
- <proof prover="5" timelimit="29" memlimit="0" obsolete="true" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="3.14"/></proof>
+ <goal name="right_nil" proved="true">
+ <proof prover="5" timelimit="29" memlimit="0" edited="vstte12_tree_reconstruction_WP_ZipperBased_right_nil_1.v"><result status="valid" time="1.54"/></proof>
  </goal>
  <goal name="main_lemma" proved="true">
  <proof prover="4" timelimit="1"><result status="valid" time="0.07"/></proof>