new implementation of the pairing algorithm, updated proof sessions

examples/add_list/why3session.xml

@@ -35,7 +35,7 @@
     locfile="../add_list.mlw"
     loclnum="32" loccnumb="8" loccnume="11"
     expl="VC for sum"
-    sum="3a88e37519a95048cc50ef9138956651"
+    sum="b655fa25e271e649aca23e9cc43dddcd"
     proved="true"
     expanded="true"
     shape="CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF">
@@ -71,7 +71,7 @@
     locfile="../add_list.mlw"
     loclnum="44" loccnumb="4" loccnume="8"
     expl="VC for main"
-    sum="df005abc0acb54725806339e698597f8"
+    sum="47f3e40b493f519ebf1c4be2f438d08a"
     proved="true"
     expanded="true"
     shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
@@ -106,7 +106,7 @@
     locfile="../add_list.mlw"
     loclnum="63" loccnumb="4" loccnume="7"
     expl="VC for sum"
-    sum="ba225088321d5a1a8cae0184cb19113d"
+    sum="c41dd4b709a78980ecafa56e520f250b"
     proved="true"
     expanded="true"
     shape="itCV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FfIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
@@ -134,7 +134,7 @@
     locfile="../add_list.mlw"
     loclnum="86" loccnumb="4" loccnume="8"
     expl="VC for main"
-    sum="1cf88d24902cc9a993f7d1ddf27c27bf"
+    sum="d6d5b03ee7f7b7855cd1135a9c87ab0e"
     proved="true"
     expanded="true"
     shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">

examples/algo64/why3session.xml

@@ -28,7 +28,7 @@
     locfile="../algo64.mlw"
     loclnum="37" loccnumb="10" loccnume="19"
     expl="VC for quicksort"
-    sum="b40455eea6fa8f5f8be3ae873ef4b885"
+    sum="5bad16d0f07bc4f66c98b988f2fd73a7"
     proved="true"
     expanded="true"
     shape="iainfix <V1V2asorted_subV8V1ainfix +V2c1Aapermut_subV3V8V1ainfix +V2c1Aapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FAainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Aainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Aapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FAainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Aainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FAainfix <V2V0Aainfix <V1V2Aainfix <=c0V1asorted_subV3V1ainfix +V2c1Aapermut_subV3V3V1ainfix +V2c1Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -43,7 +43,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="1. precondition"
-      sum="a45b02e8c4d56b83dd0ba0d355ebd5d3"
+      sum="78ff0ba8a03ecb4552b6894224928cf3"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -63,7 +63,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="2. variant decrease"
-      sum="0bf365deaa3a34ff3134bfbd740b2574"
+      sum="1a2d41703fab4faaeb527dbf69806fdc"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V4V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -83,7 +83,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="3. precondition"
-      sum="185085aaf34ff7553db76e027b7b6ba4"
+      sum="5c4469adf46d4939a3813d207849f75d"
       proved="true"
       expanded="true"
       shape="ainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V8V7Iainfix <=V8V2Aainfix <=V5V8FAainfix =agetV6V9V7Iainfix <V9V5Aainfix <V4V9FAainfix <=agetV6V10V7Iainfix <=V10V4Aainfix <=V1V10FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -103,7 +103,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="4. assertion"
-      sum="b21840d6e68ef9ac3f747096b12f348d"
+      sum="235590bf66c96bcffc40647251ca8e7a"
       proved="true"
       expanded="true"
       shape="apermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -123,7 +123,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="5. variant decrease"
-      sum="810c5db5caf74579f3183df10554cfb4"
+      sum="ac836f8d3f086054674e4c60090520a9"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V2V5ainfix -V2V1Aainfix <=c0ainfix -V2V1Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -143,7 +143,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="6. precondition"
-      sum="97247797257b81988b838ad9002f4cf7"
+      sum="6546b46be7267386af528de814800fc2"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V9V8Iainfix <=V9V2Aainfix <=V5V9FAainfix =agetV6V10V8Iainfix <V10V5Aainfix <V4V10FAainfix <=agetV6V11V8Iainfix <=V11V4Aainfix <=V1V11FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -163,7 +163,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="7. assertion"
-      sum="d410783d8fe90fe9ec9bae2f09528720"
+      sum="75c69e76e7f0c4a831886e9b503d9edd"
       proved="true"
       expanded="true"
       shape="apermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -183,7 +183,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="8. postcondition"
-      sum="d7b340f2383cfa547f1ddddda332d682"
+      sum="be21a4eeb36482399f92dac7cbe0c767"
       proved="true"
       expanded="true"
       shape="apermut_subV3V8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -203,7 +203,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="9. postcondition"
-      sum="cc4da29a7cb4a6c9c850b3d63fa33ee2"
+      sum="706b3fda811fd7a432ec6d58ceb01363"
       proved="true"
       expanded="true"
       shape="asorted_subV8V1ainfix +V2c1Iapermut_subV7V8V1ainfix +V2c1Iasorted_subV8V5ainfix +V2c1Aapermut_subV7V8V5ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V5V2Aainfix <=c0V5Iapermut_subV6V7V1ainfix +V2c1Iasorted_subV7V1ainfix +V4c1Aapermut_subV6V7V1ainfix +V4c1Aainfix <=c0V0FIainfix <V4V0Aainfix <=V1V4Aainfix <=c0V1Iainfix >=agetV6V10V9Iainfix <=V10V2Aainfix <=V5V10FAainfix =agetV6V11V9Iainfix <V11V5Aainfix <V4V11FAainfix <=agetV6V12V9Iainfix <=V12V4Aainfix <=V1V12FEAapermut_subV3V6V1ainfix +V2c1Aainfix <=V5V2Aainfix <V4V5Aainfix <=V1V4Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -231,7 +231,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="10. postcondition"
-      sum="6c0018c482239ff70d1707887727abac"
+      sum="3b9cbe2d79bcac592f3dffca66734852"
       proved="true"
       expanded="true"
       shape="apermut_subV3V3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -251,7 +251,7 @@
       locfile="../algo64.mlw"
       loclnum="37" loccnumb="10" loccnume="19"
       expl="11. postcondition"
-      sum="2b9e560b9c4d73531e3e483336932d92"
+      sum="3b968c1dc9bf57ac80fd52b1a6edcfd7"
       proved="true"
       expanded="true"
       shape="asorted_subV3V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V1V2Aainfix <=c0V1Aainfix <=c0V0FF">

examples/algo65/why3session.xml

@@ -24,7 +24,7 @@
     locfile="../algo65.mlw"
     loclnum="36" loccnumb="10" loccnume="14"
     expl="VC for find"
-    sum="a963c19dcbf0a1dcd8d82dc82681fb7b"
+    sum="35a54557b0d1a316767159e0358443d4"
     proved="true"
     expanded="true"
     shape="iainfix <V1V2iainfix <=V3V5iainfix <=V6V3ainfix <=agetV9V3agetV9V10Iainfix <=V10V2Aainfix <=V3V10FAainfix <=agetV9V11agetV9V3Iainfix <=V11V3Aainfix <=V1V11FAapermut_subV4V9V1ainfix +V2c1Iainfix <=agetV9V3agetV9V12Iainfix <=V12V2Aainfix <=V3V12FAainfix <=agetV9V13agetV9V3Iainfix <=V13V3Aainfix <=V6V13FAapermut_subV8V9V6ainfix +V2c1Aainfix <=c0V0FAainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V2V6ainfix -V2V1Aainfix <=c0ainfix -V2V1ainfix <=agetV8V3agetV8V14Iainfix <=V14V2Aainfix <=V3V14FAainfix <=agetV8V15agetV8V3Iainfix <=V15V3Aainfix <=V1V15FAapermut_subV4V8V1ainfix +V2c1Aapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V16Iainfix <=V16V5Aainfix <=V3V16FAainfix <=agetV8V17agetV8V3Iainfix <=V17V3Aainfix <=V1V17FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FAainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Aainfix <ainfix -V5V1ainfix -V2V1Aainfix <=c0ainfix -V2V1iainfix <=V6V3ainfix <=agetV18V3agetV18V19Iainfix <=V19V2Aainfix <=V3V19FAainfix <=agetV18V20agetV18V3Iainfix <=V20V3Aainfix <=V1V20FAapermut_subV4V18V1ainfix +V2c1Iainfix <=agetV18V3agetV18V21Iainfix <=V21V2Aainfix <=V3V21FAainfix <=agetV18V22agetV18V3Iainfix <=V22V3Aainfix <=V6V22FAapermut_subV7V18V6ainfix +V2c1Aainfix <=c0V0FAainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Aainfix <ainfix -V2V6ainfix -V2V1Aainfix <=c0ainfix -V2V1ainfix <=agetV7V3agetV7V23Iainfix <=V23V2Aainfix <=V3V23FAainfix <=agetV7V24agetV7V3Iainfix <=V24V3Aainfix <=V1V24FAapermut_subV4V7V1ainfix +V2c1Aapermut_subV7V7V1ainfix +V2c1Aapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V26V25Iainfix <=V26V2Aainfix <=V6V26FAainfix =agetV7V27V25Iainfix <V27V6Aainfix <V5V27FAainfix <=agetV7V28V25Iainfix <=V28V5Aainfix <=V1V28FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FAainfix <V2V0Aainfix <V1V2Aainfix <=c0V1ainfix <=agetV4V3agetV4V29Iainfix <=V29V2Aainfix <=V3V29FAainfix <=agetV4V30agetV4V3Iainfix <=V30V3Aainfix <=V1V30FAapermut_subV4V4V1ainfix +V2c1Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -39,7 +39,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="1. precondition"
-      sum="2540ad5605614898e93315c677977895"
+      sum="83d3c5ab5be7d9d7921554c6cd3d1741"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -59,7 +59,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="2. assertion"
-      sum="328c717fe4045b552b08f4357125f8cd"
+      sum="aa51013e2f55b177202a1a039525b164"
       proved="true"
       expanded="true"
       shape="apermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -79,7 +79,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="3. variant decrease"
-      sum="d28925d644e5d8088b209951ac66c280"
+      sum="4e72fdb6df7687687a870dc48b1594aa"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V5V1ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -99,7 +99,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="4. precondition"
-      sum="ef119c12013d882b9d200cedc83bb3b2"
+      sum="e480e8389447090db987cb314ef77952"
       proved="true"
       expanded="true"
       shape="ainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -119,7 +119,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="5. assertion"
-      sum="daea93c1adfc7e8afa21d78b2a6d9dce"
+      sum="a242ac10fbdd0fc53de03986f0853096"
       proved="true"
       expanded="true"
       shape="apermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V9Iainfix <=V9V5Aainfix <=V3V9FAainfix <=agetV8V10agetV8V3Iainfix <=V10V3Aainfix <=V1V10FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V12V11Iainfix <=V12V2Aainfix <=V6V12FAainfix =agetV7V13V11Iainfix <V13V6Aainfix <V5V13FAainfix <=agetV7V14V11Iainfix <=V14V5Aainfix <=V1V14FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -139,7 +139,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="6. variant decrease"
-      sum="6c8f28b36fb9ebb94025f4c12b6358a1"
+      sum="79dab20ad0e70c0bc6acaca74add38be"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V2V6ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix <=V6V3Iapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V9Iainfix <=V9V5Aainfix <=V3V9FAainfix <=agetV8V10agetV8V3Iainfix <=V10V3Aainfix <=V1V10FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V12V11Iainfix <=V12V2Aainfix <=V6V12FAainfix =agetV7V13V11Iainfix <V13V6Aainfix <V5V13FAainfix <=agetV7V14V11Iainfix <=V14V5Aainfix <=V1V14FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -159,7 +159,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="7. precondition"
-      sum="101168400c75b1695d737cab32f1190b"
+      sum="71b921456246a3608dc75e9b1caf8866"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V9Iainfix <=V9V5Aainfix <=V3V9FAainfix <=agetV8V10agetV8V3Iainfix <=V10V3Aainfix <=V1V10FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V12V11Iainfix <=V12V2Aainfix <=V6V12FAainfix =agetV7V13V11Iainfix <V13V6Aainfix <V5V13FAainfix <=agetV7V14V11Iainfix <=V14V5Aainfix <=V1V14FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -179,7 +179,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="8. postcondition"
-      sum="8b5867596ac6df09c32d04f5bab7976d"
+      sum="4c1e71c0775d1e62424e060e82fab17f"
       proved="true"
       expanded="true"
       shape="apermut_subV4V9V1ainfix +V2c1Iainfix <=agetV9V3agetV9V10Iainfix <=V10V2Aainfix <=V3V10FAainfix <=agetV9V11agetV9V3Iainfix <=V11V3Aainfix <=V6V11FAapermut_subV8V9V6ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V12Iainfix <=V12V5Aainfix <=V3V12FAainfix <=agetV8V13agetV8V3Iainfix <=V13V3Aainfix <=V1V13FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V15V14Iainfix <=V15V2Aainfix <=V6V15FAainfix =agetV7V16V14Iainfix <V16V6Aainfix <V5V16FAainfix <=agetV7V17V14Iainfix <=V17V5Aainfix <=V1V17FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -199,7 +199,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="9. postcondition"
-      sum="602640f45d546590dc0cdd8ed8146fa0"
+      sum="d5e8ce64f2363c16b46d47c4aab7f451"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV9V10agetV9V3Iainfix <=V10V3Aainfix <=V1V10FIainfix <=agetV9V3agetV9V11Iainfix <=V11V2Aainfix <=V3V11FAainfix <=agetV9V12agetV9V3Iainfix <=V12V3Aainfix <=V6V12FAapermut_subV8V9V6ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V13Iainfix <=V13V5Aainfix <=V3V13FAainfix <=agetV8V14agetV8V3Iainfix <=V14V3Aainfix <=V1V14FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V16V15Iainfix <=V16V2Aainfix <=V6V16FAainfix =agetV7V17V15Iainfix <V17V6Aainfix <V5V17FAainfix <=agetV7V18V15Iainfix <=V18V5Aainfix <=V1V18FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -219,7 +219,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="10. postcondition"
-      sum="39532632a9f028fd6e907f5a1bc1ebca"
+      sum="5f93c21976e903c761ce68f340808248"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV9V3agetV9V10Iainfix <=V10V2Aainfix <=V3V10FIainfix <=agetV9V3agetV9V11Iainfix <=V11V2Aainfix <=V3V11FAainfix <=agetV9V12agetV9V3Iainfix <=V12V3Aainfix <=V6V12FAapermut_subV8V9V6ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V13Iainfix <=V13V5Aainfix <=V3V13FAainfix <=agetV8V14agetV8V3Iainfix <=V14V3Aainfix <=V1V14FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V16V15Iainfix <=V16V2Aainfix <=V6V16FAainfix =agetV7V17V15Iainfix <V17V6Aainfix <V5V17FAainfix <=agetV7V18V15Iainfix <=V18V5Aainfix <=V1V18FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -239,7 +239,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="11. postcondition"
-      sum="656a34012b7706844b8364436bdce063"
+      sum="c1e6c431b021e1c1b6b52424b34c9d03"
       proved="true"
       expanded="true"
       shape="apermut_subV4V8V1ainfix +V2c1Iainfix <=V6V3NIapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V9Iainfix <=V9V5Aainfix <=V3V9FAainfix <=agetV8V10agetV8V3Iainfix <=V10V3Aainfix <=V1V10FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V12V11Iainfix <=V12V2Aainfix <=V6V12FAainfix =agetV7V13V11Iainfix <V13V6Aainfix <V5V13FAainfix <=agetV7V14V11Iainfix <=V14V5Aainfix <=V1V14FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -259,7 +259,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="12. postcondition"
-      sum="260201c2853663e9dead522d06430525"
+      sum="61a6417670454d51e23e84a571dd6c35"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV8V9agetV8V3Iainfix <=V9V3Aainfix <=V1V9FIainfix <=V6V3NIapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V10Iainfix <=V10V5Aainfix <=V3V10FAainfix <=agetV8V11agetV8V3Iainfix <=V11V3Aainfix <=V1V11FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V13V12Iainfix <=V13V2Aainfix <=V6V13FAainfix =agetV7V14V12Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15V12Iainfix <=V15V5Aainfix <=V1V15FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -279,7 +279,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="13. postcondition"
-      sum="86c0aedae6b1b6a16ab631fca9ba3132"
+      sum="3746cbd5dc33a4f41655c8fa41952d97"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV8V3agetV8V9Iainfix <=V9V2Aainfix <=V3V9FIainfix <=V6V3NIapermut_subV7V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V10Iainfix <=V10V5Aainfix <=V3V10FAainfix <=agetV8V11agetV8V3Iainfix <=V11V3Aainfix <=V1V11FAapermut_subV7V8V1ainfix +V5c1Aainfix <=c0V0FIainfix <V5V0Aainfix <=V3V5Aainfix <=V1V3Aainfix <=c0V1Iainfix <=V3V5Iapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V13V12Iainfix <=V13V2Aainfix <=V6V13FAainfix =agetV7V14V12Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15V12Iainfix <=V15V5Aainfix <=V1V15FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -299,7 +299,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="14. assertion"
-      sum="1667828901f64ef93bae8a04d4de4d60"
+      sum="d2b5abc979679ac82fddbe5a961859db"
       proved="true"
       expanded="true"
       shape="apermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -319,7 +319,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="15. variant decrease"
-      sum="806bc4764c90ca45592a2b35a36fd1a8"
+      sum="6004ff547223819aaac81bd3522f780a"
       proved="true"
       expanded="true"
       shape="ainfix <ainfix -V2V6ainfix -V2V1Aainfix <=c0ainfix -V2V1Iainfix <=V6V3Iapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -339,7 +339,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="16. precondition"
-      sum="b8df43a5149564f8fb589dc8d27bbf83"
+      sum="a55cce504ac9e31e45bf086d7e996876"
       proved="true"
       expanded="true"
       shape="ainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -359,7 +359,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="17. postcondition"
-      sum="6cd59df6e5963a877457f9b4157d285b"
+      sum="05343008fe6426418b99f978e7b49f50"
       proved="true"
       expanded="true"
       shape="apermut_subV4V8V1ainfix +V2c1Iainfix <=agetV8V3agetV8V9Iainfix <=V9V2Aainfix <=V3V9FAainfix <=agetV8V10agetV8V3Iainfix <=V10V3Aainfix <=V6V10FAapermut_subV7V8V6ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V12V11Iainfix <=V12V2Aainfix <=V6V12FAainfix =agetV7V13V11Iainfix <V13V6Aainfix <V5V13FAainfix <=agetV7V14V11Iainfix <=V14V5Aainfix <=V1V14FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -379,7 +379,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="18. postcondition"
-      sum="d798f3e949eb3f26ce7d64cb5e91d966"
+      sum="47cdf9cbebbe05cdbdb051bc3c8f59a9"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV8V9agetV8V3Iainfix <=V9V3Aainfix <=V1V9FIainfix <=agetV8V3agetV8V10Iainfix <=V10V2Aainfix <=V3V10FAainfix <=agetV8V11agetV8V3Iainfix <=V11V3Aainfix <=V6V11FAapermut_subV7V8V6ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V13V12Iainfix <=V13V2Aainfix <=V6V13FAainfix =agetV7V14V12Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15V12Iainfix <=V15V5Aainfix <=V1V15FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -399,7 +399,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="19. postcondition"
-      sum="59c03df7580fb2e84e63f97bdf941cc1"
+      sum="b589ae5aa4ea29ea4fca8938936cfe38"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV8V3agetV8V9Iainfix <=V9V2Aainfix <=V3V9FIainfix <=agetV8V3agetV8V10Iainfix <=V10V2Aainfix <=V3V10FAainfix <=agetV8V11agetV8V3Iainfix <=V11V3Aainfix <=V6V11FAapermut_subV7V8V6ainfix +V2c1Aainfix <=c0V0FIainfix <V2V0Aainfix <=V3V2Aainfix <=V6V3Aainfix <=c0V6Iainfix <=V6V3Iapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V13V12Iainfix <=V13V2Aainfix <=V6V13FAainfix =agetV7V14V12Iainfix <V14V6Aainfix <V5V14FAainfix <=agetV7V15V12Iainfix <=V15V5Aainfix <=V1V15FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -419,7 +419,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="20. postcondition"
-      sum="fa9172da91c8947dac3bd83f238b5620"
+      sum="3c154afac20fe058f7060c03b3fd9f55"
       proved="true"
       expanded="true"
       shape="apermut_subV4V7V1ainfix +V2c1Iainfix <=V6V3NIapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V9V8Iainfix <=V9V2Aainfix <=V6V9FAainfix =agetV7V10V8Iainfix <V10V6Aainfix <V5V10FAainfix <=agetV7V11V8Iainfix <=V11V5Aainfix <=V1V11FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -439,7 +439,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="21. postcondition"
-      sum="f5dda22c0b96bb54186f8e2271dbe148"
+      sum="488a76dd8841c1e39578de1eff33a792"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV7V8agetV7V3Iainfix <=V8V3Aainfix <=V1V8FIainfix <=V6V3NIapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V10V9Iainfix <=V10V2Aainfix <=V6V10FAainfix =agetV7V11V9Iainfix <V11V6Aainfix <V5V11FAainfix <=agetV7V12V9Iainfix <=V12V5Aainfix <=V1V12FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -459,7 +459,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="22. postcondition"
-      sum="d207808bc06460e685e43add520a41f2"
+      sum="c5c68420c26e089fa63501f340d042d3"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV7V3agetV7V8Iainfix <=V8V2Aainfix <=V3V8FIainfix <=V6V3NIapermut_subV7V7V1ainfix +V2c1Iainfix <=V3V5NIapermut_subV4V7V1ainfix +V2c1Iainfix >=agetV7V10V9Iainfix <=V10V2Aainfix <=V6V10FAainfix =agetV7V11V9Iainfix <V11V6Aainfix <V5V11FAainfix <=agetV7V12V9Iainfix <=V12V5Aainfix <=V1V12FEAapermut_subV4V7V1ainfix +V2c1Aainfix <=V6V2Aainfix <V5V6Aainfix <=V1V5Aainfix <=c0V0FIainfix <V2V0Aainfix <V1V2Aainfix <=c0V1Iainfix <V1V2Iainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -479,7 +479,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="23. postcondition"
-      sum="f39cbc770922932941b03ee859c68f72"
+      sum="1c1a4e153e07f2fd8fcb266c3a430808"
       proved="true"
       expanded="true"
       shape="apermut_subV4V4V1ainfix +V2c1Iainfix <V1V2NIainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -499,7 +499,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="24. postcondition"
-      sum="148df9f04176b7bda62b976da36402f1"
+      sum="f5a76a376659622a6765696492fcd6d3"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV4V5agetV4V3Iainfix <=V5V3Aainfix <=V1V5FIainfix <V1V2NIainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">
@@ -519,7 +519,7 @@
       locfile="../algo65.mlw"
       loclnum="36" loccnumb="10" loccnume="14"
       expl="25. postcondition"
-      sum="bc142b10ca0df104cf3bff4d61ec200b"
+      sum="817675da3963fe91243d68be0f51de0b"
       proved="true"
       expanded="true"
       shape="ainfix <=agetV4V3agetV4V5Iainfix <=V5V2Aainfix <=V3V5FIainfix <V1V2NIainfix <V2V0Aainfix <=V3V2Aainfix <=V1V3Aainfix <=c0V1Aainfix <=c0V0FF">

examples/alphaBeta/why3session.xml

@@ -51,7 +51,7 @@
     name="Test"
     locfile="../alphaBeta.mlw"
     loclnum="76" loccnumb="7" loccnume="11"
-    sum="af3ffdef718c759d4773bd79f43e7e30"
+    sum="1aa960b887d5af278444d89cef166c30"
     proved="true"
     expanded="false"
     shape="ainfix <=aprefix -aposition_valueado_moveV0V1aminmaxV0c1IamemV1V2Lalegal_movesV0F">
@@ -85,7 +85,7 @@
     name="minmax_bound"
     locfile="../alphaBeta.mlw"
     loclnum="82" loccnumb="8" loccnume="20"
-    sum="1bcd8a36394df0992b33bb260e348c88"
+    sum="a3fe8ad5d354c07f77310e49bed57baa"
     proved="true"
     expanded="false"
     shape="ainfix <aminmaxV0V1ainfinityAainfix <aprefix -ainfinityaminmaxV0V1Iainfix >=V1c0F">
@@ -103,7 +103,7 @@
     name="minmax_nomove"
     locfile="../alphaBeta.mlw"
     loclnum="86" loccnumb="8" loccnume="21"
-    sum="0b0addfda9118de4bafbe1a65e672cf1"
+    sum="37f686764a137ef6323e22e3c1c89384"
     proved="true"
     expanded="false"
     shape="ainfix =aminmaxV0V1aposition_valueV0Iainfix =alegal_movesV0aNilAainfix >=V1c0F">
@@ -184,7 +184,7 @@
     locfile="../alphaBeta.mlw"
     loclnum="109" loccnumb="10" loccnume="31"
     expl="VC for move_value_alpha_beta"
-    sum="5eeda3672d8d2f2cd58191ef8c15dc40"
+    sum="e4c492a0ec689b1462b839b1b894fc8c"
     proved="true"
     expanded="false"
     shape="iainfix <V6aprefix -V0Aainfix <aprefix -V1V6ainfix =aprefix -V5aprefix -V6iainfix <=V6aprefix -V1ainfix >=aprefix -V5V1ainfix <=aprefix -V5V0Laminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FAainfix >=ainfix -V3c1c0Iainfix >=V3c1F">
@@ -199,7 +199,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="109" loccnumb="10" loccnume="31"
       expl="1. precondition"
-      sum="a1808fdc345936478c7d217e8986f457"
+      sum="53a92003b802c519c4f3df9e61415222"
       proved="true"
       expanded="false"
       shape="ainfix >=ainfix -V3c1c0Iainfix >=V3c1F">
@@ -275,7 +275,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="109" loccnumb="10" loccnume="31"
       expl="2. postcondition"
-      sum="8140eb9ce7909fb01a2e15bf334a8873"
+      sum="1b451dfd562ff0261baabe943dd22f7c"
       proved="true"
       expanded="false"
       shape="iainfix <V6aprefix -V0Aainfix <aprefix -V1V6ainfix =aprefix -V5aprefix -V6iainfix <=V6aprefix -V1ainfix >=aprefix -V5V1ainfix <=aprefix -V5V0Laminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F">
@@ -290,7 +290,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="109" loccnumb="10" loccnume="31"
         expl="1. postcondition"
-        sum="4991642b458035aa4a6c7ff40583df8f"
+        sum="c652eed1e2f439d45f47ef23627c75ae"
         proved="true"
         expanded="false"
         shape="ainfix =aprefix -V5aprefix -V6Iainfix <V6aprefix -V0Aainfix <aprefix -V1V6Laminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F">
@@ -310,7 +310,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="109" loccnumb="10" loccnume="31"
         expl="2. postcondition"
-        sum="2b8b8d3be5e8e6d388c3cbecd15a9cf9"
+        sum="84638a48ccdaf2d8b6340da57fb5434c"
         proved="true"
         expanded="false"
         shape="ainfix >=aprefix -V5V1Iainfix <=V6aprefix -V1Iainfix <V6aprefix -V0Aainfix <aprefix -V1V6NLaminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F">
@@ -330,7 +330,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="109" loccnumb="10" loccnume="31"
         expl="3. postcondition"
-        sum="d98fbd0104c113af965c1a0969f25348"
+        sum="83052a9bb2fb4c57bd268f4c476f41d2"
         proved="true"
         expanded="false"
         shape="ainfix <=aprefix -V5V0Iainfix <=V6aprefix -V1NIainfix <V6aprefix -V0Aainfix <aprefix -V1V6NLaminmaxado_moveV2V4ainfix -V3c1Iiainfix <aminmaxado_moveV2V4ainfix -V3c1aprefix -V0Aainfix <aprefix -V1aminmaxado_moveV2V4ainfix -V3c1ainfix =V5aminmaxado_moveV2V4ainfix -V3c1iainfix <=aminmaxado_moveV2V4ainfix -V3c1aprefix -V1ainfix <=V5aprefix -V1ainfix >=V5aprefix -V0FIainfix >=ainfix -V3c1c0Iainfix >=V3c1F">
@@ -354,7 +354,7 @@
     locfile="../alphaBeta.mlw"
     loclnum="121" loccnumb="7" loccnume="15"
     expl="VC for negabeta"
-    sum="e275db87e7bafa137960c3e485470254"
+    sum="9d7bfdbcc42fc5c7cec3abfcab211367"
     proved="false"
     expanded="true"
     shape="iainfix =V3c0iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1Calegal_movesV2aNiliainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1aConsVViainfix >=V6V1iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V6aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V6V0ainfix >=V6V1iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V7aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V7V0ainfix >=V7V1Iiais_emptyV8ainfix =V7V6iainfix <V9V1Aainfix <amaxV6V0V9ainfix =V7V9iainfix <=V9amaxV6V0ainfix <=V7amaxV6V0ainfix >=V7V1LaminaTuple2V2V3V8LaelementsV5FAainfix >=V3c1Iiainfix <V10aprefix -V0Aainfix <aprefix -V1V10ainfix =V6aprefix -V10iainfix <=V10aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FAainfix >=V3c1Iainfix >=V3c0F">
@@ -369,7 +369,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="121" loccnumb="7" loccnume="15"
       expl="1. postcondition"
-      sum="7cea8c16f45481393c7ed19323c9cf00"
+      sum="ab8681aaf4912bba2f99a0ed984911d9"
       proved="true"
       expanded="false"
       shape="iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1Iainfix =V3c0Iainfix >=V3c0F">
@@ -392,7 +392,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="121" loccnumb="7" loccnume="15"
         expl="1. postcondition"
-        sum="e50fe264528ad54603548406e9bb093e"
+        sum="bd104fc8c08908b07ef8a9484e57a399"
         proved="true"
         expanded="false"
         shape="ainfix =aposition_valueV2aminmaxV2V3Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3Iainfix =V3c0Iainfix >=V3c0F">
@@ -420,7 +420,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="121" loccnumb="7" loccnume="15"
         expl="2. postcondition"
-        sum="a1e8321b9aa07cb6bd62c0dcf17267a6"
+        sum="25e934a301b56793018f8f5a6c1fcbb0"
         proved="true"
         expanded="false"
         shape="ainfix <=aposition_valueV2V0Iainfix <=aminmaxV2V3V0Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NIainfix =V3c0Iainfix >=V3c0F">
@@ -448,7 +448,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="121" loccnumb="7" loccnume="15"
         expl="3. postcondition"
-        sum="3fe502381e5d642864ff4479130f67c4"
+        sum="712a396952c0862e9b49f34fbb2490a4"
         proved="true"
         expanded="false"
         shape="ainfix >=aposition_valueV2V1Iainfix <=aminmaxV2V3V0NIainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NIainfix =V3c0Iainfix >=V3c0F">
@@ -478,7 +478,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="121" loccnumb="7" loccnume="15"
       expl="2. postcondition"
-      sum="b0f71411555bf6f6a49319b10547e75d"
+      sum="848484923f90fda7b54b0309d43d9ed9"
       proved="true"
       expanded="false"
       shape="Calegal_movesV2aNiliainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =aposition_valueV2aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=aposition_valueV2V0ainfix >=aposition_valueV2V1aConsVVtIainfix =V3c0NIainfix >=V3c0F">
@@ -493,7 +493,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="121" loccnumb="7" loccnume="15"
         expl="1. postcondition"
-        sum="bb8226faf0bc93acf933bd2038b98e23"
+        sum="85912351fe83419299848e3f5c1982cf"
         proved="true"
         expanded="false"
         shape="Calegal_movesV2aNilainfix =aposition_valueV2aminmaxV2V3Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3aConsVVtIainfix =V3c0NIainfix >=V3c0F">
@@ -529,7 +529,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="121" loccnumb="7" loccnume="15"
         expl="2. postcondition"
-        sum="d180dc50e81f6bdf8edff0ae68aa5e86"
+        sum="cc20ae36074a4fe51b188d4927f81fae"
         proved="true"
         expanded="false"
         shape="Calegal_movesV2aNilainfix <=aposition_valueV2V0Iainfix <=aminmaxV2V3V0Iainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NaConsVVtIainfix =V3c0NIainfix >=V3c0F">
@@ -565,7 +565,7 @@
         locfile="../alphaBeta.mlw"
         loclnum="121" loccnumb="7" loccnume="15"
         expl="3. postcondition"
-        sum="c82d56a4ac016e8839dce0de84018fb8"
+        sum="506cd4fc7abe3051f3451cd813ebd7e5"
         proved="true"
         expanded="false"
         shape="Calegal_movesV2aNilainfix >=aposition_valueV2V1Iainfix <=aminmaxV2V3V0NIainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3NaConsVVtIainfix =V3c0NIainfix >=V3c0F">
@@ -603,7 +603,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="121" loccnumb="7" loccnume="15"
       expl="3. precondition"
-      sum="6045211f56a53ac4515749f51e289919"
+      sum="92416b4cea2ff50735cc4e2e7ab09e11"
       proved="true"
       expanded="false"
       shape="Calegal_movesV2aNiltaConsVVainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F">
@@ -639,7 +639,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="121" loccnumb="7" loccnume="15"
       expl="4. postcondition"
-      sum="640ab76cb472655ce8eaf23073fad568"
+      sum="9914171d51b71c9ca355479fee156ddf"
       proved="false"
       expanded="true"
       shape="Calegal_movesV2aNiltaConsVViainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V6aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V6V0ainfix >=V6V1Iainfix >=V6V1Iiainfix <V7aprefix -V0Aainfix <aprefix -V1V7ainfix =V6aprefix -V7iainfix <=V7aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F">
@@ -651,7 +651,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="121" loccnumb="7" loccnume="15"
       expl="5. precondition"
-      sum="1e74940031cdea274b38b37a1ddbefa6"
+      sum="acc7d49d1d594b413ff8ad925ef65895"
       proved="true"
       expanded="false"
       shape="Calegal_movesV2aNiltaConsVVainfix >=V3c1Iainfix >=V6V1NIiainfix <V7aprefix -V0Aainfix <aprefix -V1V7ainfix =V6aprefix -V7iainfix <=V7aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F">
@@ -687,7 +687,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="121" loccnumb="7" loccnume="15"
       expl="6. postcondition"
-      sum="404e57d028647bc1a7aafe2ad331a326"
+      sum="600958f14f18d4b436f4e24e405f4c0a"
       proved="false"
       expanded="true"
       shape="Calegal_movesV2aNiltaConsVViainfix <aminmaxV2V3V1Aainfix <V0aminmaxV2V3ainfix =V7aminmaxV2V3iainfix <=aminmaxV2V3V0ainfix <=V7V0ainfix >=V7V1Iiais_emptyV8ainfix =V7V6iainfix <V9V1Aainfix <amaxV6V0V9ainfix =V7V9iainfix <=V9amaxV6V0ainfix <=V7amaxV6V0ainfix >=V7V1LaminaTuple2V2V3V8LaelementsV5FIainfix >=V3c1Iainfix >=V6V1NIiainfix <V10aprefix -V0Aainfix <aprefix -V1V10ainfix =V6aprefix -V10iainfix <=V10aprefix -V1ainfix >=V6V1ainfix <=V6V0Laminmaxado_moveV2V4ainfix -V3c1FIainfix >=V3c1Iainfix =V3c0NIainfix >=V3c0F">
@@ -701,7 +701,7 @@
     locfile="../alphaBeta.mlw"
     loclnum="139" loccnumb="7" loccnume="19"
     expl="VC for negabeta_rec"
-    sum="2134e39bfcf18e9393a818ff694e669f"
+    sum="012d67bc12d6e7a273a74e9f2812db42"
     proved="false"
     expanded="true"
     shape="CV5aNiliainfix <V7V1Aainfix <V0V7ainfix =V4V7iainfix <=V7V0ainfix <=V4V0ainfix >=V4V1LaminaTuple2V2V3V6Iais_emptyV6NLaelementsV5aConsVViainfix >=amaxV10V4V1iais_emptyV11ainfix =amaxV10V4V4iainfix <V12V1Aainfix <V0V12ainfix =amaxV10V4V12iainfix <=V12V0ainfix <=amaxV10V4V0ainfix >=amaxV10V4V1LaminaTuple2V2V3V11LaelementsV5iais_emptyV14ainfix =V13V4iainfix <V15V1Aainfix <V0V15ainfix =V13V15iainfix <=V15V0ainfix <=V13V0ainfix >=V13V1LaminaTuple2V2V3V14LaelementsV5Iiais_emptyV16ainfix =V13amaxV10V4iainfix <V17V1Aainfix <amaxamaxV10V4V0V17ainfix =V13V17iainfix <=V17amaxamaxV10V4V0ainfix <=V13amaxamaxV10V4V0ainfix >=V13V1LaminaTuple2V2V3V16LaelementsV9FAainfix >=V3c1Iiainfix <V18aprefix -V0Aainfix <aprefix -V1V18ainfix =V10aprefix -V18iainfix <=V18aprefix -V1ainfix >=V10V1ainfix <=V10V0Laminmaxado_moveV2V8ainfix -V3c1FAainfix >=V3c1Iainfix >=V3c1F">
@@ -716,7 +716,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="139" loccnumb="7" loccnume="19"
       expl="1. postcondition"
-      sum="1eb81ae3bdca869ea154b51098b87a86"
+      sum="5f601b642bda04bb8d27914557493751"
       proved="true"
       expanded="false"
       shape="CV5aNiliainfix <V7V1Aainfix <V0V7ainfix =V4V7iainfix <=V7V0ainfix <=V4V0ainfix >=V4V1LaminaTuple2V2V3V6Iais_emptyV6NLaelementsV5aConsVVtIainfix >=V3c1F">
@@ -736,7 +736,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="139" loccnumb="7" loccnume="19"
       expl="2. precondition"
-      sum="9938059d21c1e699233305535f043a80"
+      sum="cbe226da784c47693bb2e350a1bdde29"
       proved="true"
       expanded="false"
       shape="CV5aNiltaConsVVainfix >=V3c1Iainfix >=V3c1F">
@@ -756,7 +756,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="139" loccnumb="7" loccnume="19"
       expl="3. postcondition"
-      sum="5832ed2d4a603fa5e5e810fc8685468f"
+      sum="113b98cf818e0719b63f98f415cdaf65"
       proved="false"
       expanded="true"
       shape="CV5aNiltaConsVViais_emptyV9ainfix =amaxV8V4V4iainfix <V10V1Aainfix <V0V10ainfix =amaxV8V4V10iainfix <=V10V0ainfix <=amaxV8V4V0ainfix >=amaxV8V4V1LaminaTuple2V2V3V9LaelementsV5Iainfix >=amaxV8V4V1Iiainfix <V11aprefix -V0Aainfix <aprefix -V1V11ainfix =V8aprefix -V11iainfix <=V11aprefix -V1ainfix >=V8V1ainfix <=V8V0Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1Iainfix >=V3c1F">
@@ -768,7 +768,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="139" loccnumb="7" loccnume="19"
       expl="4. precondition"
-      sum="9eece8d8b9b26a3e2f91ba9a256d056e"
+      sum="7186098d5475577625401728ddb97ad7"
       proved="true"
       expanded="false"
       shape="CV5aNiltaConsVVainfix >=V3c1Iainfix >=amaxV8V4V1NIiainfix <V9aprefix -V0Aainfix <aprefix -V1V9ainfix =V8aprefix -V9iainfix <=V9aprefix -V1ainfix >=V8V1ainfix <=V8V0Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1Iainfix >=V3c1F">
@@ -788,7 +788,7 @@
       locfile="../alphaBeta.mlw"
       loclnum="139" loccnumb="7" loccnume="19"
       expl="5. postcondition"
-      sum="67ad47c1bd49b82b563963e6cb5fa964"
+      sum="d931e1fc4b18ce57bbfd25c024d85e14"
       proved="false"
       expanded="true"
       shape="CV5aNiltaConsVViais_emptyV10ainfix =V9V4iainfix <V11V1Aainfix <V0V11ainfix =V9V11iainfix <=V11V0ainfix <=V9V0ainfix >=V9V1LaminaTuple2V2V3V10LaelementsV5Iiais_emptyV12ainfix =V9amaxV8V4iainfix <V13V1Aainfix <amaxamaxV8V4V0V13ainfix =V9V13iainfix <=V13amaxamaxV8V4V0ainfix <=V9amaxamaxV8V4V0ainfix >=V9V1LaminaTuple2V2V3V12LaelementsV7FIainfix >=V3c1Iainfix >=amaxV8V4V1NIiainfix <V14aprefix -V0Aainfix <aprefix -V1V14ainfix =V8aprefix -V14iainfix <=V14aprefix -V1ainfix >=V8V1ainfix <=V8V0Laminmaxado_moveV2V6ainfix -V3c1FIainfix >=V3c1Iainfix >=V3c1F">
@@ -802,7 +802,7 @@
     locfile="../alphaBeta.mlw"
     loclnum="161" loccnumb="4" loccnume="14"
     expl="VC for alpha_beta"
-    sum="aefc65a0c9efa1dfbe91c46d1eb0a7e0"
+    sum="d7c3376ec359790570f411ad399a7c17"
     proved="true"
     expanded="false"
     shape="ainfix =V2aminmaxV0V1Iiainfix <aminmaxV0V1ainfinityAainfix <aprefix -ainfinityaminmaxV0V1ainfix =V2aminmaxV0V1iainfix <=aminmaxV0V1aprefix -ainfinityainfix <=V2aprefix -ainfinityainfix >=V2ainfinityFAainfix >=V1c0Iainfix >=V1c0F">

examples/arm/why3session.xml

@@ -24,7 +24,7 @@
     locfile="../arm.mlw"
     loclnum="16" loccnumb="6" loccnume="20"
     expl="VC for insertion_sort"
-    sum="3ce68aec817c9861b3b7cb459122b9e9"
+    sum="6152c465572f116cb4cbdb54cec6b773"
     proved="false"
     expanded="false"
     shape="iainfix <=V5c10iainfix <agetV13V11agetV13ainfix -V11c1ainfix <V18V11Aainfix <=c0V11Aainfix <=ainfix *c2V15ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V18Aainvamk arrayV0V17Aainfix <=V18V5Aainfix <=c1V18Iainfix =V18ainfix -V11c1FIainfix =V17asetV16ainfix -V11c1agetV13V11Aainfix <=c0V0FAainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Iainfix =V16asetV13V11agetV13ainfix -V11c1Aainfix <=c0V0FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <V11V0Aainfix <=c0V11Iainfix =V15ainfix +V12c1Fainfix <ainfix -c10V19ainfix -c10V5Aainfix <=c0ainfix -c10V5Aainfix <=ainfix *c2V12ainfix *ainfix -V19c2ainfix -V19c1Aainfix =V10ainfix -V19c2AainvV14Aainfix <=V19c11Aainfix <=c2V19Iainfix =V19ainfix +V5c1FAainfix <V11V0Aainfix <=c0V11Aainfix <ainfix -V11c1V0Aainfix <=c0ainfix -V11c1Aainfix <=c0V0Iainfix <=ainfix *c2V12ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V11AainvV14Aainfix <=V11V5Aainfix <=c1V11Lamk arrayV0V13FAainfix <=ainfix *c2V6ainfix +ainfix *ainfix -V5c2ainfix -V5c1ainfix *c2ainfix -V5V5AainvV9Aainfix <=V5V5Aainfix <=c1V5Iainfix =V10ainfix +V7c1Fainfix <=V6c45Aainfix =V7c9Aainfix <=c0V0Iainfix <=ainfix *c2V6ainfix *ainfix -V5c2ainfix -V5c1Aainfix =V7ainfix -V5c2AainvV9Aainfix <=V5c11Aainfix <=c2V5Lamk arrayV0V8FAainfix <=ainfix *c2V1ainfix *ainfix -c2c2ainfix -c2c1Aainfix =V2ainfix -c2c2AainvV4Aainfix <=c2c11Aainfix <=c2c2Iainfix =V1c0Aainfix =V2c0AainvV4Aainfix <=c0V0Lamk arrayV0V3FF">
@@ -50,7 +50,7 @@
     locfile="../arm.mlw"
     loclnum="120" loccnumb="6" loccnume="18"
     expl="VC for path_init_l2"
-    sum="38759903d66d93a0badff4ab76c129e6"
+    sum="492d92d7d4a40e7717e9736c55995716"
     proved="true"
     expanded="true"
     shape="ainv_l2V5V0V2Iainfix =V5amixfix [<-]V1ainfix -V0c16V4FIainfix =V4c2FIainfix =V3c0FIainfix =V2c0FIainvV1AaseparationV0F">
@@ -78,7 +78,7 @@
     locfile="../arm.mlw"
     loclnum="127" loccnumb="6" loccnume="18"
     expl="VC for path_l2_exit"
-    sum="548a1717c3f91ea68d3cbefc909a77e8"
+    sum="60875edac419a47f205013458f0c3aaa"
     proved="true"
     expanded="true"
     shape="ainfix =V0c9Iainfix =V4aFalseIainfix <=V3c10qainfix =V4aTrueFIainfix =V3amixfix []V2ainfix -V1c16FIainv_l2V2V1V0AaseparationV1F">