blocking semantic: expressions

24f5f244 · atafat · bf311cc1 · 24f5f244 · 24f5f244 · 24f5f244
Commit 24f5f244 authored Sep 25, 2012 by atafat
4 changed files
--- a/examples/hoare_logic/blocking_semantics2.mlw
+++ b/examples/hoare_logic/blocking_semantics2.mlw
@@ -152,7 +152,7 @@ inductive type_expr type_env type_stack expr datatype =
 	type_expr sigma pi e2 ty2 ->
 	type_operator op ty1 ty2 ty -> type_expr sigma pi (Ebin e1 op e2) ty
  | Type_eseq :
-      forall sigma: type_env, pi:type_stack, e1 e2:expr, op:operator, ty:datatype.
+      forall sigma: type_env, pi:type_stack, e1 e2:expr, ty:datatypew.
        type_expr sigma pi e1 TYunit ->
 	type_expr sigma pi e2 ty ->
 	type_expr sigma pi (Eseq e1 e2) ty

--- a/examples/hoare_logic/blocking_semantics3/why3session.xml
+++ b/examples/hoare_logic/blocking_semantics3/why3session.xml
@@ -2649,7 +2649,7 @@
    name="assigns_refl"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="653" loccnumb="6" loccnume="18"
-    sum="f90eef52da71cd7bf67770d0b0f63b8b"
+    sum="37f4fc83faa6f8aefbd36ccee2337a5a"
    proved="true"
    expanded="false"
    shape="aassignsV0V1V0F">
@@ -2659,7 +2659,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.06"/>
    </proof>
    <proof
     prover="11"
@@ -2667,14 +2667,14 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.15"/>
    </proof>
   </goal>
   <goal
    name="assigns_trans"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="656" loccnumb="6" loccnume="19"
-    sum="f49e740118dc96156f6389814566c428"
+    sum="64298c6b39fa607f3ea9f1149c7f83bf"
    proved="true"
    expanded="false"
    shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F">
@@ -2692,14 +2692,14 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.15"/>
    </proof>
   </goal>
   <goal
    name="assigns_union_left"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="661" loccnumb="6" loccnume="24"
-    sum="72a07d9a65ceb4a77559d18852260b0a"
+    sum="fdfc38afecfc34e0b9a5f900b349ace0"
    proved="true"
    expanded="false"
    shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F">
@@ -2709,7 +2709,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.04"/>
+     <result status="valid" time="0.05"/>
    </proof>
    <proof
     prover="11"
@@ -2717,14 +2717,14 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.10"/>
+     <result status="valid" time="0.15"/>
    </proof>
   </goal>
   <goal
    name="assigns_union_right"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="665" loccnumb="6" loccnume="25"
-    sum="ebf45489286020ac11e1cb3b195150ee"
+    sum="05dc4d3614bc725c1619cf3b4c4d9f90"
    proved="true"
    expanded="false"
    shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F">
@@ -2734,7 +2734,7 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.06"/>
    </proof>
    <proof
     prover="11"
@@ -2742,14 +2742,14 @@
     memlimit="1000"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.11"/>
+     <result status="valid" time="0.15"/>
    </proof>
   </goal>
   <goal
    name="monotonicity"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="733" loccnumb="8" loccnume="20"
-    sum="47e15c538359092133991525add37a01"
+    sum="b012764e95073fe6abf1d1a83af59e4d"
    proved="true"
    expanded="false"
    shape="avalid_fmlaaFimpliesawpV0V1awpV0V2Iavalid_fmlaaFimpliesV1V2F">
@@ -2761,7 +2761,7 @@
      name="monotonicity.1"
      locfile="blocking_semantics3/../blocking_semantics3.mlw"
      loclnum="733" loccnumb="8" loccnume="20"
-      sum="1780621b5826d52e9e0f42681e6c8d29"
+      sum="6364117bb46156c7766dd5b1e3e99c59"
      proved="true"
      expanded="false"
      shape="CV0aSskipavalid_fmlaaFimpliesawpV0V1awpV0V2Iavalid_fmlaaFimpliesV1V2FaSassignVVavalid_fmlaaFimpliesawpV0V5awpV0V6Iavalid_fmlaaFimpliesV5V6FaSseqVVavalid_fmlaaFimpliesawpV0V9awpV0V10Iavalid_fmlaaFimpliesV9V10FIavalid_fmlaaFimpliesawpV7V11awpV7V12Iavalid_fmlaaFimpliesV11V12FIavalid_fmlaaFimpliesawpV8V13awpV8V14Iavalid_fmlaaFimpliesV13V14FaSifVVVavalid_fmlaaFimpliesawpV0V18awpV0V19Iavalid_fmlaaFimpliesV18V19FIavalid_fmlaaFimpliesawpV16V20awpV16V21Iavalid_fmlaaFimpliesV20V21FIavalid_fmlaaFimpliesawpV17V22awpV17V23Iavalid_fmlaaFimpliesV22V23FaSassertVavalid_fmlaaFimpliesawpV0V25awpV0V26Iavalid_fmlaaFimpliesV25V26FaSwhileVVVavalid_fmlaaFimpliesawpV0V30awpV0V31Iavalid_fmlaaFimpliesV30V31FIavalid_fmlaaFimpliesawpV29V32awpV29V33Iavalid_fmlaaFimpliesV32V33FF">
@@ -2773,7 +2773,7 @@
        name="monotonicity.1.1"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="733" loccnumb="8" loccnume="20"
-        sum="8221e5bc9a4c673a65a18a8d8da78191"
+        sum="f6b566b5fb717c4254291a4c01f834e3"
        proved="true"
        expanded="false"
        shape="CV0aSskipavalid_fmlaaFimpliesawpV0V1awpV0V2Iavalid_fmlaaFimpliesV1V2FaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
@@ -2783,14 +2783,14 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.05"/>
+         <result status="valid" time="0.06"/>
        </proof>
       </goal>
       <goal
        name="monotonicity.1.2"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="733" loccnumb="8" loccnume="20"
-        sum="a1e5ec843129757142663a1b9d150ff3"
+        sum="eb44d50a00e17d04f774ebbd00a629b6"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVavalid_fmlaaFimpliesawpV0V3awpV0V4Iavalid_fmlaaFimpliesV3V4FaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
@@ -2801,14 +2801,14 @@
         edited="blocking_semantics3_WP_monotonicity_5.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.70"/>
+         <result status="valid" time="1.01"/>
        </proof>
       </goal>
       <goal
        name="monotonicity.1.3"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="733" loccnumb="8" loccnume="20"
-        sum="4582ae6dd3e06288d864d77937574cbf"
+        sum="767eb3874908196e2a1171f132d2fea6"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVavalid_fmlaaFimpliesawpV0V5awpV0V6Iavalid_fmlaaFimpliesV5V6FIavalid_fmlaaFimpliesawpV3V7awpV3V8Iavalid_fmlaaFimpliesV7V8FIavalid_fmlaaFimpliesawpV4V9awpV4V10Iavalid_fmlaaFimpliesV9V10FaSifVVVtaSassertVtaSwhileVVVtF">
@@ -2818,14 +2818,14 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.06"/>
+         <result status="valid" time="0.08"/>
        </proof>
       </goal>
       <goal
        name="monotonicity.1.4"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="733" loccnumb="8" loccnume="20"
-        sum="307fb4e3add630d0704c9b1872e3d6f4"
+        sum="d771305878be5d6572d1e4ee300adb05"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVavalid_fmlaaFimpliesawpV0V8awpV0V9Iavalid_fmlaaFimpliesV8V9FIavalid_fmlaaFimpliesawpV6V10awpV6V11Iavalid_fmlaaFimpliesV10V11FIavalid_fmlaaFimpliesawpV7V12awpV7V13Iavalid_fmlaaFimpliesV12V13FaSassertVtaSwhileVVVtF">
@@ -2836,14 +2836,14 @@
         edited="blocking_semantics3_WP_monotonicity_3.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.68"/>
+         <result status="valid" time="1.01"/>
        </proof>
       </goal>
       <goal
        name="monotonicity.1.5"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="733" loccnumb="8" loccnume="20"
-        sum="5aa55dde8511da6e82f99fdb6810f2fd"
+        sum="07d021db552b1542fefbc49f77689031"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVavalid_fmlaaFimpliesawpV0V9awpV0V10Iavalid_fmlaaFimpliesV9V10FaSwhileVVVtF">
@@ -2854,14 +2854,14 @@
         edited="blocking_semantics3_WP_monotonicity_2.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.65"/>
+         <result status="valid" time="1.00"/>
        </proof>
       </goal>
       <goal
        name="monotonicity.1.6"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="733" loccnumb="8" loccnume="20"
-        sum="a11eddfccf4d58bb53e692cd5b42afc5"
+        sum="b2a0aff95c47b767da2814a4dbd70bd0"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVavalid_fmlaaFimpliesawpV0V12awpV0V13Iavalid_fmlaaFimpliesV12V13FIavalid_fmlaaFimpliesawpV11V14awpV11V15Iavalid_fmlaaFimpliesV14V15FF">
@@ -2872,7 +2872,7 @@
         edited="blocking_semantics3_WP_monotonicity_4.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.66"/>
+         <result status="valid" time="1.03"/>
        </proof>
       </goal>
      </transf>
@@ -2883,7 +2883,7 @@
    name="distrib_conj"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="738" loccnumb="8" loccnume="20"
-    sum="531940b71e309c4491a7b79af90d58e5"
+    sum="1b3808ef065f50e5fbc8f0d32a23a891"
    proved="true"
    expanded="false"
    shape="aeval_fmlaV1V2awpV0aFandV3V4Iaeval_fmlaV1V2awpV0V4Aaeval_fmlaV1V2awpV0V3F">
@@ -2895,7 +2895,7 @@
      name="distrib_conj.1"
      locfile="blocking_semantics3/../blocking_semantics3.mlw"
      loclnum="738" loccnumb="8" loccnume="20"
-      sum="ac0478078d133fcf3880e13b59e5aa71"
+      sum="9778ae383afe5c170cfa3cef53c3b358"
      proved="true"
      expanded="false"
      shape="CV0aSskipaeval_fmlaV1V2awpV0aFandV3V4Iaeval_fmlaV1V2awpV0V4Aaeval_fmlaV1V2awpV0V3FaSassignVVaeval_fmlaV7V8awpV0aFandV9V10Iaeval_fmlaV7V8awpV0V10Aaeval_fmlaV7V8awpV0V9FaSseqVVaeval_fmlaV13V14awpV0aFandV15V16Iaeval_fmlaV13V14awpV0V16Aaeval_fmlaV13V14awpV0V15FIaeval_fmlaV17V18awpV11aFandV19V20Iaeval_fmlaV17V18awpV11V20Aaeval_fmlaV17V18awpV11V19FIaeval_fmlaV21V22awpV12aFandV23V24Iaeval_fmlaV21V22awpV12V24Aaeval_fmlaV21V22awpV12V23FaSifVVVaeval_fmlaV28V29awpV0aFandV30V31Iaeval_fmlaV28V29awpV0V31Aaeval_fmlaV28V29awpV0V30FIaeval_fmlaV32V33awpV26aFandV34V35Iaeval_fmlaV32V33awpV26V35Aaeval_fmlaV32V33awpV26V34FIaeval_fmlaV36V37awpV27aFandV38V39Iaeval_fmlaV36V37awpV27V39Aaeval_fmlaV36V37awpV27V38FaSassertVaeval_fmlaV41V42awpV0aFandV43V44Iaeval_fmlaV41V42awpV0V44Aaeval_fmlaV41V42awpV0V43FaSwhileVVVaeval_fmlaV48V49awpV0aFandV50V51Iaeval_fmlaV48V49awpV0V51Aaeval_fmlaV48V49awpV0V50FIaeval_fmlaV52V53awpV47aFandV54V55Iaeval_fmlaV52V53awpV47V55Aaeval_fmlaV52V53awpV47V54FF">
@@ -2907,7 +2907,7 @@
        name="distrib_conj.1.1"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="738" loccnumb="8" loccnume="20"
-        sum="8fcb2022e3de8e4fca0a2538c4c710dc"
+        sum="68be63d56bab67a9491a658adb1b4266"
        proved="true"
        expanded="false"
        shape="CV0aSskipaeval_fmlaV1V2awpV0aFandV3V4Iaeval_fmlaV1V2awpV0V4Aaeval_fmlaV1V2awpV0V3FaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
@@ -2917,13 +2917,13 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.05"/>
+         <result status="valid" time="0.07"/>
        </proof>
        <proof
         prover="2"
         timelimit="5"
         memlimit="1000"
-         obsolete="false"
+         obsolete="true"
         archived="false">
         <result status="valid" time="0.04"/>
        </proof>
@@ -2932,7 +2932,7 @@
        name="distrib_conj.1.2"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="738" loccnumb="8" loccnume="20"
-        sum="384cbc980801410aeee753698e2630b1"
+        sum="0f073174f10f7755a9a8753bc8e131ed"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVaeval_fmlaV3V4awpV0aFandV5V6Iaeval_fmlaV3V4awpV0V6Aaeval_fmlaV3V4awpV0V5FaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
@@ -2943,14 +2943,14 @@
         edited="blocking_semantics3_WP_distrib_conj_5.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.72"/>
+         <result status="valid" time="1.05"/>
        </proof>
       </goal>
       <goal
        name="distrib_conj.1.3"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="738" loccnumb="8" loccnume="20"
-        sum="55abcf20e6bd911a1d61e7c8825cd7b6"
+        sum="ae18f796d680c6c3dd92fb5d6a4006f5"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVaeval_fmlaV5V6awpV0aFandV7V8Iaeval_fmlaV5V6awpV0V8Aaeval_fmlaV5V6awpV0V7FIaeval_fmlaV9V10awpV3aFandV11V12Iaeval_fmlaV9V10awpV3V12Aaeval_fmlaV9V10awpV3V11FIaeval_fmlaV13V14awpV4aFandV15V16Iaeval_fmlaV13V14awpV4V16Aaeval_fmlaV13V14awpV4V15FaSifVVVtaSassertVtaSwhileVVVtF">
@@ -2961,14 +2961,14 @@
         edited="blocking_semantics3_WP_distrib_conj_3.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.65"/>
+         <result status="valid" time="1.01"/>
        </proof>
       </goal>
       <goal
        name="distrib_conj.1.4"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="738" loccnumb="8" loccnume="20"
-        sum="c5638c4b1d98e56d784123ba730592b5"
+        sum="88e85d6a4931f848e44be722633bd5bd"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVaeval_fmlaV8V9awpV0aFandV10V11Iaeval_fmlaV8V9awpV0V11Aaeval_fmlaV8V9awpV0V10FIaeval_fmlaV12V13awpV6aFandV14V15Iaeval_fmlaV12V13awpV6V15Aaeval_fmlaV12V13awpV6V14FIaeval_fmlaV16V17awpV7aFandV18V19Iaeval_fmlaV16V17awpV7V19Aaeval_fmlaV16V17awpV7V18FaSassertVtaSwhileVVVtF">
@@ -2978,13 +2978,13 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.18"/>
+         <result status="valid" time="0.24"/>
        </proof>
        <proof
         prover="2"
         timelimit="5"
         memlimit="1000"
-         obsolete="false"
+         obsolete="true"
         archived="false">
         <result status="valid" time="0.17"/>
        </proof>
@@ -2993,7 +2993,7 @@
        name="distrib_conj.1.5"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="738" loccnumb="8" loccnume="20"
-        sum="024c86d557c6ecea3bc003778aa23e3c"
+        sum="eda88eef8b881d9ef567b1e4be249164"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVaeval_fmlaV9V10awpV0aFandV11V12Iaeval_fmlaV9V10awpV0V12Aaeval_fmlaV9V10awpV0V11FaSwhileVVVtF">
@@ -3003,13 +3003,13 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.09"/>
+         <result status="valid" time="0.13"/>
        </proof>
        <proof
         prover="2"
         timelimit="5"
         memlimit="1000"
-         obsolete="false"
+         obsolete="true"
         archived="false">
         <result status="valid" time="0.10"/>
        </proof>
@@ -3018,7 +3018,7 @@
        name="distrib_conj.1.6"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="738" loccnumb="8" loccnume="20"
-        sum="2b045c2e0d8e3ab4f59fde6c2e477303"
+        sum="2b9fdb5788b02dd5f6940ce489c416ee"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVaeval_fmlaV12V13awpV0aFandV14V15Iaeval_fmlaV12V13awpV0V15Aaeval_fmlaV12V13awpV0V14FIaeval_fmlaV16V17awpV11aFandV18V19Iaeval_fmlaV16V17awpV11V19Aaeval_fmlaV16V17awpV11V18FF">
@@ -3029,7 +3029,7 @@
         edited="blocking_semantics3_WP_distrib_conj_4.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.67"/>
+         <result status="valid" time="1.06"/>
        </proof>
       </goal>
      </transf>
@@ -3040,7 +3040,7 @@
    name="wp_reduction"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="744" loccnumb="8" loccnume="20"
-    sum="e17b18b12076413bd443685209a02cbb"
+    sum="4fe361b10701083e53743e68bdf034fa"
    proved="true"
    expanded="false"
    shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F">
@@ -3051,14 +3051,14 @@
     edited="blocking_semantics3_WP_wp_reduction_1.v"
     obsolete="false"
     archived="false">
-     <result status="valid" time="0.71"/>
+     <result status="valid" time="1.06"/>
    </proof>
   </goal>
   <goal
    name="progress"
    locfile="blocking_semantics3/../blocking_semantics3.mlw"
    loclnum="751" loccnumb="8" loccnume="16"
-    sum="6b555ab70b645da284643700dcdaacd0"
+    sum="07e830e0f0dda34b460b90e664fdce12"
    proved="true"
    expanded="false"
    shape="aone_stepV1V2V0V6V7V8EIainfix =V0aSskipNIaeval_fmlaV1V2awpV0V5Iatype_stmtV3V4V0F">
@@ -3070,7 +3070,7 @@
      name="progress.1"
      locfile="blocking_semantics3/../blocking_semantics3.mlw"
      loclnum="751" loccnumb="8" loccnume="16"
-      sum="a4039a01c3d6439a8d73955711048f02"
+      sum="2e294fa72d58123519a68c4ef511b729"
      proved="true"
      expanded="false"
      shape="CV0aSskipaone_stepV1V2V0V6V7V8EIainfix =V0aSskipNIaeval_fmlaV1V2awpV0V5Iatype_stmtV3V4V0FaSassignVVaone_stepV11V12V0V16V17V18EIainfix =V0aSskipNIaeval_fmlaV11V12awpV0V15Iatype_stmtV13V14V0FaSseqVVaone_stepV21V22V0V26V27V28EIainfix =V0aSskipNIaeval_fmlaV21V22awpV0V25Iatype_stmtV23V24V0FIaone_stepV29V30V19V34V35V36EIainfix =V19aSskipNIaeval_fmlaV29V30awpV19V33Iatype_stmtV31V32V19FIaone_stepV37V38V20V42V43V44EIainfix =V20aSskipNIaeval_fmlaV37V38awpV20V41Iatype_stmtV39V40V20FaSifVVVaone_stepV48V49V0V53V54V55EIainfix =V0aSskipNIaeval_fmlaV48V49awpV0V52Iatype_stmtV50V51V0FIaone_stepV56V57V46V61V62V63EIainfix =V46aSskipNIaeval_fmlaV56V57awpV46V60Iatype_stmtV58V59V46FIaone_stepV64V65V47V69V70V71EIainfix =V47aSskipNIaeval_fmlaV64V65awpV47V68Iatype_stmtV66V67V47FaSassertVaone_stepV73V74V0V78V79V80EIainfix =V0aSskipNIaeval_fmlaV73V74awpV0V77Iatype_stmtV75V76V0FaSwhileVVVaone_stepV84V85V0V89V90V91EIainfix =V0aSskipNIaeval_fmlaV84V85awpV0V88Iatype_stmtV86V87V0FIaone_stepV92V93V83V97V98V99EIainfix =V83aSskipNIaeval_fmlaV92V93awpV83V96Iatype_stmtV94V95V83FF">
@@ -3082,7 +3082,7 @@
        name="progress.1.1"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="751" loccnumb="8" loccnume="16"
-        sum="ca914e40dae77b0e4ff3cf36f7ee6437"
+        sum="a44e1f9d2ac69b6b3a317669640496dc"
        proved="true"
        expanded="false"
        shape="CV0aSskipaone_stepV1V2V0V6V7V8EIainfix =V0aSskipNIaeval_fmlaV1V2awpV0V5Iatype_stmtV3V4V0FaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
@@ -3092,7 +3092,7 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.04"/>
+         <result status="valid" time="0.05"/>
        </proof>
        <proof
         prover="11"
@@ -3100,14 +3100,14 @@
         memlimit="1000"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.00"/>
+         <result status="valid" time="0.03"/>
        </proof>
       </goal>
       <goal
        name="progress.1.2"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="751" loccnumb="8" loccnume="16"
-        sum="0ae384af6f78c6df6f25c04666e15fd7"
+        sum="b285cdf4191274841821c5ee4a160575"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVaone_stepV3V4V0V8V9V10EIainfix =V0aSskipNIaeval_fmlaV3V4awpV0V7Iatype_stmtV5V6V0FaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
@@ -3118,14 +3118,14 @@
         edited="blocking_semantics3_WP_progress_1.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.68"/>
+         <result status="valid" time="1.06"/>
        </proof>
       </goal>
       <goal
        name="progress.1.3"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="751" loccnumb="8" loccnume="16"
-        sum="e8c371c0f5f8e808e1345696e12de934"
+        sum="7e14f7c522b7b89a477d80438e7a73a2"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVaone_stepV5V6V0V10V11V12EIainfix =V0aSskipNIaeval_fmlaV5V6awpV0V9Iatype_stmtV7V8V0FIaone_stepV13V14V3V18V19V20EIainfix =V3aSskipNIaeval_fmlaV13V14awpV3V17Iatype_stmtV15V16V3FIaone_stepV21V22V4V26V27V28EIainfix =V4aSskipNIaeval_fmlaV21V22awpV4V25Iatype_stmtV23V24V4FaSifVVVtaSassertVtaSwhileVVVtF">
@@ -3136,14 +3136,14 @@
         edited="blocking_semantics3_WP_progress_2.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.71"/>
+         <result status="valid" time="1.09"/>
        </proof>
       </goal>
       <goal
        name="progress.1.4"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="751" loccnumb="8" loccnume="16"
-        sum="cf10a73ddecfea49a6efa21c2829c537"
+        sum="56d6c20293bb5ad0bf19a207d6f76cec"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVaone_stepV8V9V0V13V14V15EIainfix =V0aSskipNIaeval_fmlaV8V9awpV0V12Iatype_stmtV10V11V0FIaone_stepV16V17V6V21V22V23EIainfix =V6aSskipNIaeval_fmlaV16V17awpV6V20Iatype_stmtV18V19V6FIaone_stepV24V25V7V29V30V31EIainfix =V7aSskipNIaeval_fmlaV24V25awpV7V28Iatype_stmtV26V27V7FaSassertVtaSwhileVVVtF">
@@ -3154,14 +3154,14 @@
         edited="blocking_semantics3_WP_progress_3.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.71"/>
+         <result status="valid" time="1.09"/>
        </proof>
       </goal>
       <goal
        name="progress.1.5"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="751" loccnumb="8" loccnume="16"
-        sum="ddf7d3eaa14dec42fc4be26f2a2fbdb7"
+        sum="46f6b598587231c76c3ba325eadb0244"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVaone_stepV9V10V0V14V15V16EIainfix =V0aSskipNIaeval_fmlaV9V10awpV0V13Iatype_stmtV11V12V0FaSwhileVVVtF">
@@ -3172,14 +3172,14 @@
         edited="blocking_semantics3_WP_progress_5.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.64"/>
+         <result status="valid" time="1.01"/>
        </proof>
       </goal>
       <goal
        name="progress.1.6"
        locfile="blocking_semantics3/../blocking_semantics3.mlw"
        loclnum="751" loccnumb="8" loccnume="16"
-        sum="c4e43655dc52b8f61727a6eedee9e36d"
+        sum="ce249f707903dfceecc11f3292050cf5"
        proved="true"
        expanded="false"
        shape="CV0aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVaone_stepV12V13V0V17V18V19EIainfix =V0aSskipNIaeval_fmlaV12V13awpV0V16Iatype_stmtV14V15V0FIaone_stepV20V21V11V25V26V27EIainfix =V11aSskipNIaeval_fmlaV20V21awpV11V24Iatype_stmtV22V23V11FF">
@@ -3190,7 +3190,7 @@
         edited="blocking_semantics3_WP_progress_4.v"
         obsolete="false"
         archived="false">
-         <result status="valid" time="0.68"/>
+         <result status="valid" time="1.04"/>
        </proof>
       </goal>
      </transf>

--- a/examples/hoare_logic/blocking_semantics4.mlw
+++ b/examples/hoare_logic/blocking_semantics4.mlw
@@ -9,6 +9,7 @@ use import int.Int
 use import int.MinMax
 use import bool.Bool
 use export list.List
+use export list.Append
 use map.Map as IdMap

 (** types and values *)
@@ -23,60 +24,48 @@ type operator = Oplus | Ominus | Omult | Ole
 (** ident for mutable variables *)
 type mident

+
 axiom mident_decide :
  forall m1 m2: mident. m1 = m2 \/ m1 <> m2

 (** ident for immutable variables *)
 type ident = {| ident_index : int |}
+ 
+constant result : ident
+
+axiom ident_decide :
+  forall m1 m2: ident. m1 = m2 \/ m1 <> m2

 (** Terms *)
-type term_node =
+type term =
  | Tvalue value
  | Tvar ident
  | Tderef mident
  | Tbin term operator term

-with term = {| term_node : term_node;
-               term_maxvar : int;
-             |}

 predicate var_occurs_in_term (x:ident) (t:term) =
  match t with
-  | {| term_node = Tvalue _ |} -> false
-  | {| term_node = Tvar i |} -> x=i
-  | {| term_node = Tderef _ |} -> false
-  | {| term_node = Tbin t1 _ t2 |} -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
+  | Tvalue _  -> false
+  |  Tvar i  -> x=i
+  |  Tderef _  -> false
+  |  Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
  end

-predicate term_inv (t:term) =
-  forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar
+(* predicate term_inv (t:term) = *)
+(*   forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar *)

 function mk_tvalue (v:value) : term =
-   {| term_node = Tvalue v; term_maxvar = -1 |}
-
-lemma mk_tvalue_inv :
-   forall v:value. term_inv (mk_tvalue v)
+   Tvalue v

 function mk_tvar (i:ident) : term =
-   {| term_node = Tvar i; term_maxvar = i.ident_index |}
-
-lemma mk_tvar_inv :
-   forall i:ident. term_inv (mk_tvar i)
+   Tvar i

 function mk_tderef (r:mident) : term =
-   {| term_node = Tderef r; term_maxvar = -1 |}
-
-lemma mk_tderef_inv :
-   forall r:mident. term_inv (mk_tderef r)
+   Tderef r

 function mk_tbin (t1:term) (o:operator) (t2:term) : term =
-   {| term_node = Tbin t1 o t2;
-      term_maxvar = max t1.term_maxvar t2.term_maxvar |}
-
-lemma mk_tbin_inv :
-   forall t1 t2:term, o:operator. term_inv t1 /\ term_inv t2 ->
-     term_inv (mk_tbin t1 o t2)
-
+    Tbin t1 o t2

 (** Formulas *)
 type fmla =
@@ -87,17 +76,33 @@ type fmla =
  | Flet ident term fmla         (* let id = term in fmla *)
  | Fforall ident datatype fmla  (* forall id : ty, fmla *)

-(** Statements *)
-type stmt =
-  | Sskip
-  | Sassign mident term
-  | Sseq stmt stmt
-  | Sif term stmt stmt
-  | Sassert fmla
-  | Swhile term fmla stmt  (* while cond invariant inv body *)
+(** Expressions *)
+type expr =
+  | Evalue value
+  | Ebin expr operator expr
+  | Evar ident
+  | Ederef mident
+  | Eassign mident expr
+  | Eseq expr expr
+  | Elet ident expr expr
+  | Eif expr expr expr
+  | Eassert fmla
+  | Ewhile expr fmla expr  (* while cond invariant inv body *)
+
+function mk_evalue (v:value) : expr =
+   Evalue v

-lemma decide_is_skip:
-  forall s:stmt. s = Sskip \/ s <> Sskip
+function mk_evar (i:ident) : expr =
+   Evar i
+
+function mk_ederef (r:mident) : expr =
+   Ederef r
+
+function mk_ebin (e1:expr) (o:operator) (e2:expr) : expr =
+    Ebin e1 o e2
+
+(* lemma decide_is_skip: *)
+(*   forall s:stmt. s = Sskip \/ s <> Sskip *)

 (** Typing *)

@@ -121,28 +126,29 @@ function get_vartype (i:ident) (pi:type_stack) : datatype =
  | Cons (x,ty) r -> if x=i then ty else get_vartype i r
  end

+    
 type type_env = IdMap.map mident datatype  (* map global mutable variables to their type *)
 function get_reftype (i:mident) (e:type_env) : datatype = IdMap.get e i

 inductive type_term type_env type_stack term datatype =
  | Type_value :
-      forall sigma: type_env, pi:type_stack, v:value, m:int.
-	type_term sigma pi {| term_node = Tvalue v; term_maxvar = m |} (type_value v)
+      forall sigma: type_env, pi:type_stack, v:value.
+	type_term sigma pi  (Tvalue v) (type_value v)
  | Type_var :
-      forall sigma: type_env, pi:type_stack, v: ident, m:int, ty:datatype.
+      forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
        (get_vartype v pi = ty) ->
-        type_term sigma pi {| term_node = Tvar v ; term_maxvar = m |} ty
+        type_term sigma pi (Tvar v) ty
  | Type_deref :
-      forall sigma: type_env, pi:type_stack, v: mident, m:int, ty:datatype.
+      forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
        (get_reftype v sigma = ty) ->
-        type_term sigma pi {| term_node = Tderef v; term_maxvar = m |} ty
+        type_term sigma pi (Tderef v) ty
  | Type_bin :
      forall sigma: type_env, pi:type_stack, t1 t2 : term, op:operator,
-        m:int, ty1 ty2 ty:datatype.
+        ty1 ty2 ty:datatype.
        type_term sigma pi t1 ty1 ->
 	type_term sigma pi t2 ty2 ->
 	type_operator op ty1 ty2 ty ->
-        type_term sigma pi {| term_node = Tbin t1 op t2; term_maxvar = m |} ty
+        type_term sigma pi (Tbin t1 op t2) ty

 inductive type_fmla type_env type_stack fmla =
  | Type_term :
@@ -181,36 +187,52 @@ inductive type_fmla type_env type_stack fmla =
        type_fmla sigma (Cons (x,TYunit) pi) f ->
  	type_fmla sigma pi (Fforall x TYunit f)

-inductive type_stmt type_env type_stack stmt =
-  | Type_skip :
-      forall sigma: type_env, pi:type_stack.
-	type_stmt sigma pi Sskip
+inductive type_expr type_env type_stack expr datatype =
+  | Type_Evalue :
+      forall sigma: type_env, pi:type_stack, v:value.
+	type_expr sigma pi (Evalue v) (type_value v)
+  | Type_Evar :
+      forall sigma: type_env, pi:type_stack, v: ident, ty:datatype.
+        (get_vartype v pi = ty) -> type_expr sigma pi (Evar v) ty
+  | Type_Ederef :
+      forall sigma: type_env, pi:type_stack, v: mident, ty:datatype.
+        (get_reftype v sigma = ty) -> type_expr sigma pi (Ederef v) ty
+  | Type_Ebinop :
+      forall sigma: type_env, pi:type_stack, e1 e2 : expr, op:operator, ty1 ty2 ty:datatype.
+        type_expr sigma pi e1 ty1 ->
+        type_expr sigma pi e2 ty2 ->
+        type_operator op ty1 ty2 ty -> type_expr sigma pi (Ebin e1 op e2) ty