Commit c57ffaa6 authored by Asma Tafat's avatar Asma Tafat
Browse files

eval_swap

parent ec3b98a2
......@@ -391,7 +391,7 @@ lemma eval_swap:
(eval_fmla sigma (l++(Cons (id1,v1) (Cons (id2,v2) pi))) f <->
eval_fmla sigma (l++(Cons (id2,v2) (Cons (id1,v1) pi))) f)
lemma eval_swap:
lemma eval_swap_2:
forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
......
......@@ -820,7 +820,7 @@
proved="true"
expanded="false">
<goal
name="eval_swap_term.0"
name="eval_swap_term.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="376" loccnumb="6" loccnume="20"
sum="05d6d800c66d93b4cc193957064c4b51"
......@@ -832,7 +832,7 @@
proved="true"
expanded="false">
<goal
name="eval_swap_term.0.0"
name="eval_swap_term.1.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="376" loccnumb="6" loccnume="20"
sum="8c612f8b937d3df7647158f70fd24edd"
......@@ -849,7 +849,7 @@
</proof>
</goal>
<goal
name="eval_swap_term.0.1"
name="eval_swap_term.1.2"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="376" loccnumb="6" loccnume="20"
sum="c2a5a503bdd0a949b064d13f4af29c4a"
......@@ -867,7 +867,7 @@
</proof>
</goal>
<goal
name="eval_swap_term.0.2"
name="eval_swap_term.1.3"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="376" loccnumb="6" loccnume="20"
sum="94a70c7ca4534008833289008cb504e6"
......@@ -884,7 +884,7 @@
</proof>
</goal>
<goal
name="eval_swap_term.0.3"
name="eval_swap_term.1.4"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="376" loccnumb="6" loccnume="20"
sum="3563d543613e459fd90c47ce74c9af1c"
......@@ -917,7 +917,7 @@
proved="true"
expanded="false">
<goal
name="eval_swap.0"
name="eval_swap.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="81bd146411010485181a0e2d2629738d"
......@@ -929,7 +929,7 @@
proved="true"
expanded="false">
<goal
name="eval_swap.0.0"
name="eval_swap.1.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="4a23865ecd32ef2e23618a7d95803884"
......@@ -946,7 +946,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.1"
name="eval_swap.1.2"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="37a0bb1862789acb214292390cf40ea4"
......@@ -963,7 +963,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.2"
name="eval_swap.1.3"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="f335b0a57133b45d102e6ed60be20448"
......@@ -980,7 +980,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.3"
name="eval_swap.1.4"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="92e9aaf208482910ec49e5d46e5c3503"
......@@ -997,7 +997,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.4"
name="eval_swap.1.5"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="c50923a9289054f1f8f49a16a6f33e29"
......@@ -1014,7 +1014,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.5"
name="eval_swap.1.6"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="275e654609557a4b6908e8c0d472c568"
......@@ -1031,7 +1031,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.6"
name="eval_swap.1.7"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="0380ad284c5294c4a089971f5696dbff"
......@@ -1048,7 +1048,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.7"
name="eval_swap.1.8"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="f7ee32104aac2645a1c5b5e29d069624"
......@@ -1065,7 +1065,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.8"
name="eval_swap.1.9"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="c017dc8975a88863de2311977fe31b3a"
......@@ -1082,7 +1082,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.9"
name="eval_swap.1.10"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="c9d18367352127085ed40f0214c23e31"
......@@ -1099,7 +1099,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.10"
name="eval_swap.1.11"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="ec1fcd5fdb78d3e6ca538cd62ca655ec"
......@@ -1117,7 +1117,7 @@
</proof>
</goal>
<goal
name="eval_swap.0.11"
name="eval_swap.1.12"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="388" loccnumb="6" loccnume="15"
sum="5a5df8ff96e2e761bc70722f67627be2"
......@@ -1138,43 +1138,379 @@
</goal>
</transf>
</goal>
<goal
name="eval_swap_2"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="b117e6c3c7f7d4eee741e1eed36f99cc"
proved="false"
expanded="true"
shape="aeval_fmlaV1aConsaTuple2V4V6aConsaTuple2V3V5V2V0qaeval_fmlaV1aConsaTuple2V3V5aConsaTuple2V4V6V2V0Iainfix =V3V4NF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.91"/>
</proof>
<transf
name="induction_ty_lex"
proved="false"
expanded="true">
<goal
name="eval_swap_2.0"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="9986b503b081aedd1aa7ba3ed69ec490"
proved="false"
expanded="true"
shape="CV0aFtermVaeval_fmlaV2aConsaTuple2V5V7aConsaTuple2V4V6V3V0qaeval_fmlaV2aConsaTuple2V4V6aConsaTuple2V5V7V3V0Iainfix =V4V5NFaFandVVaeval_fmlaV10aConsaTuple2V13V15aConsaTuple2V12V14V11V0qaeval_fmlaV10aConsaTuple2V12V14aConsaTuple2V13V15V11V0Iainfix =V12V13NFIaeval_fmlaV16aConsaTuple2V19V21aConsaTuple2V18V20V17V8qaeval_fmlaV16aConsaTuple2V18V20aConsaTuple2V19V21V17V8Iainfix =V18V19NFIaeval_fmlaV22aConsaTuple2V25V27aConsaTuple2V24V26V23V9qaeval_fmlaV22aConsaTuple2V24V26aConsaTuple2V25V27V23V9Iainfix =V24V25NFaFnotVaeval_fmlaV29aConsaTuple2V32V34aConsaTuple2V31V33V30V0qaeval_fmlaV29aConsaTuple2V31V33aConsaTuple2V32V34V30V0Iainfix =V31V32NFIaeval_fmlaV35aConsaTuple2V38V40aConsaTuple2V37V39V36V28qaeval_fmlaV35aConsaTuple2V37V39aConsaTuple2V38V40V36V28Iainfix =V37V38NFaFimpliesVVaeval_fmlaV43aConsaTuple2V46V48aConsaTuple2V45V47V44V0qaeval_fmlaV43aConsaTuple2V45V47aConsaTuple2V46V48V44V0Iainfix =V45V46NFIaeval_fmlaV49aConsaTuple2V52V54aConsaTuple2V51V53V50V41qaeval_fmlaV49aConsaTuple2V51V53aConsaTuple2V52V54V50V41Iainfix =V51V52NFIaeval_fmlaV55aConsaTuple2V58V60aConsaTuple2V57V59V56V42qaeval_fmlaV55aConsaTuple2V57V59aConsaTuple2V58V60V56V42Iainfix =V57V58NFaFletVVVaeval_fmlaV64aConsaTuple2V67V69aConsaTuple2V66V68V65V0qaeval_fmlaV64aConsaTuple2V66V68aConsaTuple2V67V69V65V0Iainfix =V66V67NFIaeval_fmlaV70aConsaTuple2V73V75aConsaTuple2V72V74V71V63qaeval_fmlaV70aConsaTuple2V72V74aConsaTuple2V73V75V71V63Iainfix =V72V73NFaFforallVVVaeval_fmlaV79aConsaTuple2V82V84aConsaTuple2V81V83V80V0qaeval_fmlaV79aConsaTuple2V81V83aConsaTuple2V82V84V80V0Iainfix =V81V82NFIaeval_fmlaV85aConsaTuple2V88V90aConsaTuple2V87V89V86V78qaeval_fmlaV85aConsaTuple2V87V89aConsaTuple2V88V90V86V78Iainfix =V87V88NFF">
<transf
name="split_goal_wp"
proved="false"
expanded="true">
<goal
name="eval_swap_2.0.0"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="4230e2aa10a4d772dfd1f3f0dd601ad8"
proved="false"
expanded="false"
shape="CV0aFtermVaeval_fmlaV2aConsaTuple2V5V7aConsaTuple2V4V6V3V0Iaeval_fmlaV2aConsaTuple2V4V6aConsaTuple2V5V7V3V0Iainfix =V4V5NFaFandVVtaFnotVtaFimpliesVVtaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="8.56"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="6.56"/>
</proof>
</goal>
<goal
name="eval_swap_2.0.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="d268e92430217f61baf29a651dbde7f2"
proved="false"
expanded="false"
shape="CV0aFtermVaeval_fmlaV2aConsaTuple2V4V6aConsaTuple2V5V7V3V0Iaeval_fmlaV2aConsaTuple2V5V7aConsaTuple2V4V6V3V0Iainfix =V4V5NFaFandVVtaFnotVtaFimpliesVVtaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="8.86"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="8.12"/>
</proof>
</goal>
<goal
name="eval_swap_2.0.2"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="067a90514fea82a3a98919ae4b1a017b"
proved="true"
expanded="false"
shape="CV0aFtermVtaFandVVaeval_fmlaV4aConsaTuple2V7V9aConsaTuple2V6V8V5V0Iaeval_fmlaV4aConsaTuple2V6V8aConsaTuple2V7V9V5V0Iainfix =V6V7NFIaeval_fmlaV10aConsaTuple2V13V15aConsaTuple2V12V14V11V2qaeval_fmlaV10aConsaTuple2V12V14aConsaTuple2V13V15V11V2Iainfix =V12V13NFIaeval_fmlaV16aConsaTuple2V19V21aConsaTuple2V18V20V17V3qaeval_fmlaV16aConsaTuple2V18V20aConsaTuple2V19V21V17V3Iainfix =V18V19NFaFnotVtaFimpliesVVtaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.25"/>
</proof>
</goal>
<goal
name="eval_swap_2.0.3"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="027437ee3caea9f80baa63f2885547d3"
proved="true"
expanded="false"
shape="CV0aFtermVtaFandVVaeval_fmlaV4aConsaTuple2V6V8aConsaTuple2V7V9V5V0Iaeval_fmlaV4aConsaTuple2V7V9aConsaTuple2V6V8V5V0Iainfix =V6V7NFIaeval_fmlaV10aConsaTuple2V13V15aConsaTuple2V12V14V11V2qaeval_fmlaV10aConsaTuple2V12V14aConsaTuple2V13V15V11V2Iainfix =V12V13NFIaeval_fmlaV16aConsaTuple2V19V21aConsaTuple2V18V20V17V3qaeval_fmlaV16aConsaTuple2V18V20aConsaTuple2V19V21V17V3Iainfix =V18V19NFaFnotVtaFimpliesVVtaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.30"/>
</proof>
</goal>
<goal
name="eval_swap_2.0.4"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="92f54013479e9a613c9d3bc3f7de06f5"
proved="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVaeval_fmlaV5aConsaTuple2V8V10aConsaTuple2V7V9V6V0Iaeval_fmlaV5aConsaTuple2V7V9aConsaTuple2V8V10V6V0Iainfix =V7V8NFIaeval_fmlaV11aConsaTuple2V14V16aConsaTuple2V13V15V12V4qaeval_fmlaV11aConsaTuple2V13V15aConsaTuple2V14V16V12V4Iainfix =V13V14NFaFimpliesVVtaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.98"/>
</proof>
</goal>
<goal
name="eval_swap_2.0.5"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="e51e23197496bf28f106b309f253eb83"
proved="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVaeval_fmlaV5aConsaTuple2V7V9aConsaTuple2V8V10V6V0Iaeval_fmlaV5aConsaTuple2V8V10aConsaTuple2V7V9V6V0Iainfix =V7V8NFIaeval_fmlaV11aConsaTuple2V14V16aConsaTuple2V13V15V12V4qaeval_fmlaV11aConsaTuple2V13V15aConsaTuple2V14V16V12V4Iainfix =V13V14NFaFimpliesVVtaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.00"/>
</proof>
</goal>
<goal
name="eval_swap_2.0.6"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="07ee81210a6d50aa4fc5c1400edf4fee"
proved="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVaeval_fmlaV7aConsaTuple2V10V12aConsaTuple2V9V11V8V0Iaeval_fmlaV7aConsaTuple2V9V11aConsaTuple2V10V12V8V0Iainfix =V9V10NFIaeval_fmlaV13aConsaTuple2V16V18aConsaTuple2V15V17V14V5qaeval_fmlaV13aConsaTuple2V15V17aConsaTuple2V16V18V14V5Iainfix =V15V16NFIaeval_fmlaV19aConsaTuple2V22V24aConsaTuple2V21V23V20V6qaeval_fmlaV19aConsaTuple2V21V23aConsaTuple2V22V24V20V6Iainfix =V21V22NFaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false"><undone/>
</proof>
</goal>
<goal
name="eval_swap_2.0.7"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="0e08574c41225481325381c51ded3e60"
proved="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVaeval_fmlaV7aConsaTuple2V9V11aConsaTuple2V10V12V8V0Iaeval_fmlaV7aConsaTuple2V10V12aConsaTuple2V9V11V8V0Iainfix =V9V10NFIaeval_fmlaV13aConsaTuple2V16V18aConsaTuple2V15V17V14V5qaeval_fmlaV13aConsaTuple2V15V17aConsaTuple2V16V18V14V5Iainfix =V15V16NFIaeval_fmlaV19aConsaTuple2V22V24aConsaTuple2V21V23V20V6qaeval_fmlaV19aConsaTuple2V21V23aConsaTuple2V22V24V20V6Iainfix =V21V22NFaFletVVVtaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false"><undone/>
</proof>
</goal>
<goal
name="eval_swap_2.0.8"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="a4b30e7dff1d38db7e6a7a613e1a4bad"
proved="false"
expanded="true"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVaeval_fmlaV10aConsaTuple2V13V15aConsaTuple2V12V14V11V0Iaeval_fmlaV10aConsaTuple2V12V14aConsaTuple2V13V15V11V0Iainfix =V12V13NFIaeval_fmlaV16aConsaTuple2V19V21aConsaTuple2V18V20V17V9qaeval_fmlaV16aConsaTuple2V18V20aConsaTuple2V19V21V17V9Iainfix =V18V19NFaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="7.10"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false"><undone/>
</proof>
</goal>
<goal
name="eval_swap_2.0.9"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="4013ee4dc75814d687277db047363ba0"
proved="false"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVaeval_fmlaV10aConsaTuple2V12V14aConsaTuple2V13V15V11V0Iaeval_fmlaV10aConsaTuple2V13V15aConsaTuple2V12V14V11V0Iainfix =V12V13NFIaeval_fmlaV16aConsaTuple2V19V21aConsaTuple2V18V20V17V9qaeval_fmlaV16aConsaTuple2V18V20aConsaTuple2V19V21V17V9Iainfix =V18V19NFaFforallVVVtF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="8.02"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false"><undone/>
</proof>
</goal>
<goal
name="eval_swap_2.0.10"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="27f830df381663c8700c1d377807468b"
proved="false"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVtaFforallVVVaeval_fmlaV13aConsaTuple2V16V18aConsaTuple2V15V17V14V0Iaeval_fmlaV13aConsaTuple2V15V17aConsaTuple2V16V18V14V0Iainfix =V15V16NFIaeval_fmlaV19aConsaTuple2V22V24aConsaTuple2V21V23V20V12qaeval_fmlaV19aConsaTuple2V21V23aConsaTuple2V22V24V20V12Iainfix =V21V22NFF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="6.18"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false"><undone/>
</proof>
</goal>
<goal
name="eval_swap_2.0.11"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="394" loccnumb="6" loccnume="17"
sum="a882f7693a991b95bd19735a2902d13f"
proved="false"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVtaFforallVVVaeval_fmlaV13aConsaTuple2V15V17aConsaTuple2V16V18V14V0Iaeval_fmlaV13aConsaTuple2V16V18aConsaTuple2V15V17V14V0Iainfix =V15V16NFIaeval_fmlaV19aConsaTuple2V22V24aConsaTuple2V21V23V20V12qaeval_fmlaV19aConsaTuple2V21V23aConsaTuple2V22V24V20V12Iainfix =V21V22NFF">
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="8.48"/>
</proof>
<proof
prover="9"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false"><undone/>
</proof>
</goal>
</transf>
</goal>
</transf>
</goal>
<goal
name="eval_term_change_free"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="400" loccnumb="6" loccnume="27"
sum="daf52c9f99b05cf1bcdd52fb4cb4bd8a"
proved="true"
sum="b68ee8ac05844e79152cfbf336a7e24c"
proved="false"
expanded="false"
shape="ainfix =aeval_termV1aConsaTuple2V3V4V2V0aeval_termV1V2V0Iafresh_in_termV3V0F">
<transf
name="induction_ty_lex"
proved="true"
proved="false"
expanded="false">
<goal
name="eval_term_change_free.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="400" loccnumb="6" loccnume="27"
sum="98fed2c79072dbd7351a1535f2474e12"
proved="true"
sum="83b0082074dea0c52343338842db1cd0"
proved="false"
expanded="false"
shape="CV0aTvalueVainfix =aeval_termV2aConsaTuple2V4V5V3V0aeval_termV2V3V0Iafresh_in_termV4V0FaTvarVainfix =aeval_termV7aConsaTuple2V9V10V8V0aeval_termV7V8V0Iafresh_in_termV9V0FaTderefVainfix =aeval_termV12aConsaTuple2V14V15V13V0aeval_termV12V13V0Iafresh_in_termV14V0FaTbinVVVainfix =aeval_termV19aConsaTuple2V21V22V20V0aeval_termV19V20V0Iafresh_in_termV21V0FIainfix =aeval_termV23aConsaTuple2V25V26V24V16aeval_termV23V24V16Iafresh_in_termV25V16FIainfix =aeval_termV27aConsaTuple2V29V30V28V18aeval_termV27V28V18Iafresh_in_termV29V18FF">
<transf
name="split_goal_wp"
proved="true"
proved="false"
expanded="false">
<goal
name="eval_term_change_free.1.1"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="400" loccnumb="6" loccnume="27"
sum="53430cbf0ce3f97a039307ba10671bad"
proved="true"
sum="2fd946145fe6108332d3359c5409364a"
proved="false"
expanded="false"
shape="CV0aTvalueVainfix =aeval_termV2aConsaTuple2V4V5V3V0aeval_termV2V3V0Iafresh_in_termV4V0FaTvarVtaTderefVtaTbinVVVtF">
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.04"/>
</proof>
......@@ -1182,7 +1518,7 @@
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.02"/>
</proof>
......@@ -1190,7 +1526,7 @@
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.05"/>
</proof>
......@@ -1198,7 +1534,7 @@
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.06"/>
</proof>
......@@ -1206,7 +1542,7 @@
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.06"/>
</proof>
......@@ -1214,7 +1550,7 @@
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.03"/>
</proof>
......@@ -1223,15 +1559,15 @@
name="eval_term_change_free.1.2"
locfile="blocking_semantics3/../blocking_semantics3.mlw"
loclnum="400" loccnumb="6" loccnume="27"
sum="15e9b9a9cc7305be2d1dee6fa931fa97"
proved="true"
sum="b5a4d0f3bc98a208e290553b21bb72b7"
proved="false"
expanded="false"
shape="CV0aTvalueVtaTvarVainfix =aeval_termV3aConsaTuple2V5V6V4V0aeval_termV3V4V0Iafresh_in_termV5V0FaTderefVtaTbinVVVtF">
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
obsolete="true"
archived="false">
<result status="valid" time="0.10"/>