updated proof sessions

examples/programs/algo64/why3session.xml

 <?xml version="1.0" encoding="UTF-8"?>
-<!DOCTYPE why3session SYSTEM "/home/jc/why3/share/why3session.dtd">
+<!DOCTYPE why3session SYSTEM "/home/jcf/why3/share/why3session.dtd">
 <why3session
  name="examples/programs/algo64/why3session.xml" shape_version="2">
  <prover
@@ -25,10 +25,10 @@
     locfile="examples/programs/algo64/../algo64.mlw"
     loclnum="37" loccnumb="10" loccnume="19"
     expl="parameter quicksort"
-    sum="3533c0ea980cde0949f11d81f0039f7d"
+    sum="8a1f2b902fdeeefdde002420e440667a"
     proved="true"
     expanded="true"
-    shape="iainfix &lt;V1V2asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Aapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FAainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Aapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FAainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FAainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1asorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+    shape="iainfix &lt;V2V3asorted_subV8V2ainfix +V3c1Aapermut_subV1V8V2ainfix +V3c1Aapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1FAainfix &lt;V3V0Aainfix &lt;=V5V3Aainfix &lt;=c0V5Aainfix &lt;ainfix -V3V5ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Aapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FAainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V3Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FAainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2asorted_subV1V2ainfix +V3c1Aapermut_subV1V1V2ainfix +V3c1Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
     <label
      name="expl:parameter quicksort"/>
     <transf
@@ -40,10 +40,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="precondition"
-      sum="1937b51a248d0b81e263cfda90830a31"
+      sum="cb7d833fa021079e7387b5a29f2e9f92"
       proved="true"
       expanded="false"
-      shape="ainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="ainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -52,7 +52,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.02"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
      <goal
@@ -60,10 +60,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="variant decreases"
-      sum="194b5831756da65b29d0a1aea48225f1"
+      sum="955f0e4ead25821bcf767a1e84d4e18c"
       proved="true"
       expanded="false"
-      shape="ainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V8V7Iainfix &lt;=V8V2Aainfix &lt;=V5V8FAainfix =agetV6V9V7Iainfix &lt;V9V5Aainfix &lt;V4V9FAainfix &lt;=agetV6V10V7Iainfix &lt;=V10V4Aainfix &lt;=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="ainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V8V7Iainfix &lt;=V8V3Aainfix &lt;=V5V8FAainfix =agetV6V9V7Iainfix &lt;V9V5Aainfix &lt;V4V9FAainfix &lt;=agetV6V10V7Iainfix &lt;=V10V4Aainfix &lt;=V2V10FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -72,7 +72,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.00"/>
       </proof>
      </goal>
      <goal
@@ -80,10 +80,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="precondition"
-      sum="034928eff8a6ffb4a2a09d9cef39ca33"
+      sum="a2c1f0d51466ad9ac8d51ca2b56d892f"
       proved="true"
       expanded="false"
-      shape="ainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Iainfix &gt;=agetV6V8V7Iainfix &lt;=V8V2Aainfix &lt;=V5V8FAainfix =agetV6V9V7Iainfix &lt;V9V5Aainfix &lt;V4V9FAainfix &lt;=agetV6V10V7Iainfix &lt;=V10V4Aainfix &lt;=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="ainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Iainfix &gt;=agetV6V8V7Iainfix &lt;=V8V3Aainfix &lt;=V5V8FAainfix =agetV6V9V7Iainfix &lt;V9V5Aainfix &lt;V4V9FAainfix &lt;=agetV6V10V7Iainfix &lt;=V10V4Aainfix &lt;=V2V10FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -92,7 +92,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.00"/>
       </proof>
      </goal>
      <goal
@@ -100,10 +100,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="assertion"
-      sum="c02cf84424f0d3f80a18bbd62f4f9d7f"
+      sum="5538048324f60bc28ab3a89ad6bb1a0a"
       proved="true"
       expanded="false"
-      shape="apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="apermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V3Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V2V11FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -112,7 +112,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.04"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
      <goal
@@ -120,10 +120,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="variant decreases"
-      sum="2acdc20b13b77e830b11f6b0ff7915bc"
+      sum="76f9de2e9851d43da8e0c1d0a9a909c2"
       proved="true"
       expanded="false"
-      shape="ainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="ainfix &lt;ainfix -V3V5ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V3Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V2V11FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -132,7 +132,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
      <goal
@@ -140,10 +140,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="precondition"
-      sum="2e6be7b6dba972c3888cf2d815f92588"
+      sum="e354ccfbacbd8537ee3b299ceb577a2a"
       proved="true"
       expanded="false"
-      shape="ainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V2Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="ainfix &lt;V3V0Aainfix &lt;=V5V3Aainfix &lt;=c0V5Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V9V8Iainfix &lt;=V9V3Aainfix &lt;=V5V9FAainfix =agetV6V10V8Iainfix &lt;V10V5Aainfix &lt;V4V10FAainfix &lt;=agetV6V11V8Iainfix &lt;=V11V4Aainfix &lt;=V2V11FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -152,7 +152,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.03"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
      <goal
@@ -160,10 +160,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="assertion"
-      sum="4cb0e10c07f7d1266dcbca3b21e61000"
+      sum="a7b20e810f99eaf58093b1da07c72c7f"
       proved="true"
       expanded="false"
-      shape="apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="apermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1FIainfix &lt;V3V0Aainfix &lt;=V5V3Aainfix &lt;=c0V5Aainfix &lt;ainfix -V3V5ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V3Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -172,7 +172,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.04"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
      <goal
@@ -180,10 +180,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="normal postcondition"
-      sum="73b08ee7a978f24b740f747e96186b06"
+      sum="671e204156a481acc2c24e60fd72520c"
       proved="true"
       expanded="true"
-      shape="asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="asorted_subV8V2ainfix +V3c1Aapermut_subV1V8V2ainfix +V3c1Iapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1FIainfix &lt;V3V0Aainfix &lt;=V5V3Aainfix &lt;=c0V5Aainfix &lt;ainfix -V3V5ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V3Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <transf
@@ -195,10 +195,10 @@
         locfile="examples/programs/algo64/../algo64.mlw"
         loclnum="37" loccnumb="10" loccnume="19"
         expl="parameter quicksort"
-        sum="ad5ce69bb20a3c62372c864f4a9a6cdc"
+        sum="c857efe3d1922bae632c30e069abfef7"
         proved="true"
         expanded="false"
-        shape="apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+        shape="apermut_subV1V8V2ainfix +V3c1Iapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1FIainfix &lt;V3V0Aainfix &lt;=V5V3Aainfix &lt;=c0V5Aainfix &lt;ainfix -V3V5ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V3Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
         <label
          name="expl:parameter quicksort"/>
         <proof
@@ -207,7 +207,7 @@
          memlimit="1000"
          obsolete="false"
          archived="false">
-         <result status="valid" time="0.10"/>
+         <result status="valid" time="0.03"/>
         </proof>
        </goal>
        <goal
@@ -215,19 +215,19 @@
         locfile="examples/programs/algo64/../algo64.mlw"
         loclnum="37" loccnumb="10" loccnume="19"
         expl="parameter quicksort"
-        sum="af0bb134c03b7b81b0ec6db2673c6e7c"
+        sum="a319e14a4cac7b86e8881c095cd603ec"
         proved="true"
         expanded="true"
-        shape="asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1FIainfix &lt;V2V0Aainfix &lt;=V5V2Aainfix &lt;=c0V5Aainfix &lt;ainfix -V2V5ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V1V4Aainfix &lt;=c0V1Aainfix &lt;ainfix -V4V1ainfix -V2V1Aainfix &lt;=c0ainfix -V2V1Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V2Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix &lt;=V5V2Aainfix &lt;V4V5Aainfix &lt;=V1V4FIainfix &lt;V2V0Aainfix &lt;V1V2Aainfix &lt;=c0V1Iainfix &lt;V1V2Iainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+        shape="asorted_subV8V2ainfix +V3c1Iapermut_subV7V8V2ainfix +V3c1Iasorted_subV8V5ainfix +V3c1Aapermut_subV7V8V5ainfix +V3c1FIainfix &lt;V3V0Aainfix &lt;=V5V3Aainfix &lt;=c0V5Aainfix &lt;ainfix -V3V5ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iapermut_subV6V7V2ainfix +V3c1Iasorted_subV7V2ainfix +V4c1Aapermut_subV6V7V2ainfix +V4c1FIainfix &lt;V4V0Aainfix &lt;=V2V4Aainfix &lt;=c0V2Aainfix &lt;ainfix -V4V2ainfix -V3V2Aainfix &lt;=c0ainfix -V3V2Iainfix &gt;=agetV6V10V9Iainfix &lt;=V10V3Aainfix &lt;=V5V10FAainfix =agetV6V11V9Iainfix &lt;V11V5Aainfix &lt;V4V11FAainfix &lt;=agetV6V12V9Iainfix &lt;=V12V4Aainfix &lt;=V2V12FEAapermut_subV1V6V2ainfix +V3c1Aainfix &lt;=V5V3Aainfix &lt;V4V5Aainfix &lt;=V2V4FIainfix &lt;V3V0Aainfix &lt;V2V3Aainfix &lt;=c0V2Iainfix &lt;V2V3Iainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
         <label
          name="expl:parameter quicksort"/>
         <proof
          prover="1"
-         timelimit="19"
+         timelimit="30"
          memlimit="1000"
          obsolete="false"
          archived="false">
-         <result status="valid" time="14.69"/>
+         <result status="valid" time="4.11"/>
         </proof>
        </goal>
       </transf>
@@ -237,10 +237,10 @@
       locfile="examples/programs/algo64/../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="normal postcondition"
-      sum="07812c408c2ef8ba959a4c34a2b3e06e"
+      sum="6940adf4c5a2be18549747c0a1d12871"
       proved="true"
       expanded="false"
-      shape="asorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1Iainfix &lt;V1V2NIainfix &lt;V2V0Aainfix &lt;=V1V2Aainfix &lt;=c0V1FF">
+      shape="asorted_subV1V2ainfix +V3c1Aapermut_subV1V1V2ainfix +V3c1Iainfix &lt;V2V3NIainfix &lt;V3V0Aainfix &lt;=V2V3Aainfix &lt;=c0V2F">
       <label
        name="expl:parameter quicksort"/>
       <proof
@@ -249,7 +249,7 @@
        memlimit="1000"
        obsolete="false"
        archived="false">
-       <result status="valid" time="0.04"/>
+       <result status="valid" time="0.01"/>
       </proof>
      </goal>
     </transf>