factorize uses of "instantiate"

examples/WP_revisited/blocking_semantics5/why3session.xml

@@ -6,6 +6,7 @@
 <prover id="1" name="Coq" version="8.7.1" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Alt-Ergo" version="2.0.0" timelimit="10" steplimit="0" memlimit="4000"/>
 <prover id="3" name="CVC3" version="2.4.1" timelimit="5" steplimit="0" memlimit="1000"/>
+<prover id="4" name="Eprover" version="2.0" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="5" name="Eprover" version="1.8-001" timelimit="5" steplimit="0" memlimit="1000"/>
 <prover id="7" name="CVC4" version="1.5" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="10" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
@@ -565,17 +566,9 @@
      <proof prover="7"><result status="valid" time="0.13"/></proof>
      </goal>
      <goal name="distrib_conj.0.2.0.1" proved="true">
-     <transf name="instantiate" proved="true" arg1="monotonicity" arg2="x1">
+     <transf name="instantiate" proved="true" arg1="monotonicity" arg2="x1,(Fand (wp x p) (wp x q)),(wp x (Fand p q))">
       <goal name="distrib_conj.0.2.0.1.0" proved="true">
-      <transf name="instantiate" proved="true" arg1="Hinst" arg2="(Fand (wp x p) (wp x q))">
-       <goal name="distrib_conj.0.2.0.1.0.0" proved="true">
-       <transf name="instantiate" proved="true" arg1="Hinst" arg2="(wp x (Fand p q))">
-        <goal name="distrib_conj.0.2.0.1.0.0.0" proved="true">
-        <proof prover="5"><result status="valid" time="0.15"/></proof>
-        </goal>
-       </transf>
-       </goal>
-      </transf>
+      <proof prover="4"><result status="valid" time="0.35"/></proof>
       </goal>
      </transf>
      </goal>
@@ -650,25 +643,9 @@
       <goal name="progress.0.2.0.1.1" expl="false case" proved="true">
       <transf name="introduce_premises" proved="true" >
        <goal name="progress.0.2.0.1.1.0" expl="false case" proved="true">
-       <transf name="instantiate" proved="true" arg1="H8" arg2="sigma1">
+       <transf name="instantiate" proved="true" arg1="H8" arg2="sigma1,pi1,sigmat,pit,(wp s2 q)">
         <goal name="progress.0.2.0.1.1.0.0" expl="false case" proved="true">
-        <transf name="instantiate" proved="true" arg1="Hinst" arg2="pi1">
-         <goal name="progress.0.2.0.1.1.0.0.0" expl="false case" proved="true">
-         <transf name="instantiate" proved="true" arg1="Hinst" arg2="sigmat">
-          <goal name="progress.0.2.0.1.1.0.0.0.0" expl="false case" proved="true">
-          <transf name="instantiate" proved="true" arg1="Hinst" arg2="pit">
-           <goal name="progress.0.2.0.1.1.0.0.0.0.0" expl="false case" proved="true">
-           <transf name="instantiate" proved="true" arg1="Hinst" arg2="(wp s2 q)">
-            <goal name="progress.0.2.0.1.1.0.0.0.0.0.0" expl="false case" proved="true">
-            <proof prover="5" timelimit="1"><result status="valid" time="0.30"/></proof>
-            </goal>
-           </transf>
-           </goal>
-          </transf>
-          </goal>
-         </transf>
-         </goal>
-        </transf>
+        <proof prover="4"><result status="valid" time="1.63"/></proof>
         </goal>
        </transf>
        </goal>