Commit 38628bc5 authored by MARCHE Claude's avatar MARCHE Claude

change proof of wp preservation

parent e9c6e1ae
......@@ -879,7 +879,7 @@
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="406" loccnumb="7" loccnume="21"
verified="true"
expanded="true">
expanded="false">
<goal
name="eval_msubst_term"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
......@@ -2867,31 +2867,31 @@
loclnum="480" loccnumb="6" loccnume="27"
sum="e94d482d6342c70ef6b05771254ae33d"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =aeval_termV1aConsaTuple2V3V4V2V0aeval_termV1V2V0Iafresh_in_termV3V0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="eval_term_change_free.1"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="480" loccnumb="6" loccnume="27"
sum="1a78284cadf2c1c0c66e79b70067e55e"
proved="true"
expanded="true"
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"
expanded="true">
expanded="false">
<goal
name="eval_term_change_free.1.1"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="480" loccnumb="6" loccnume="27"
sum="3b8e622f232e3f4dd6381e14e60a04ec"
proved="true"
expanded="true"
expanded="false"
shape="CV0aTvalueVainfix =aeval_termV2aConsaTuple2V4V5V3V0aeval_termV2V3V0Iafresh_in_termV4V0FaTvarVtaTderefVtaTbinVVVtF">
<proof
prover="1"
......@@ -2948,7 +2948,7 @@
loclnum="480" loccnumb="6" loccnume="27"
sum="5e70cf8106f3a360b2f866bfff4acf4b"
proved="true"
expanded="true"
expanded="false"
shape="CV0aTvalueVtaTvarVainfix =aeval_termV3aConsaTuple2V5V6V4V0aeval_termV3V4V0Iafresh_in_termV5V0FaTderefVtaTbinVVVtF">
<proof
prover="1"
......@@ -3005,7 +3005,7 @@
loclnum="480" loccnumb="6" loccnume="27"
sum="906eea10d79fb9d659502082efc6a8fb"
proved="true"
expanded="true"
expanded="false"
shape="CV0aTvalueVtaTvarVtaTderefVainfix =aeval_termV4aConsaTuple2V6V7V5V0aeval_termV4V5V0Iafresh_in_termV6V0FaTbinVVVtF">
<proof
prover="1"
......@@ -3062,7 +3062,7 @@
loclnum="480" loccnumb="6" loccnume="27"
sum="e1ac81d1824d1b01625bbd24dfb327be"
proved="true"
expanded="true"
expanded="false"
shape="CV0aTvalueVtaTvarVtaTderefVtaTbinVVVainfix =aeval_termV7aConsaTuple2V9V10V8V0aeval_termV7V8V0Iafresh_in_termV9V0FIainfix =aeval_termV11aConsaTuple2V13V14V12V4aeval_termV11V12V4Iafresh_in_termV13V4FIainfix =aeval_termV15aConsaTuple2V17V18V16V6aeval_termV15V16V6Iafresh_in_termV17V6FF">
<proof
prover="1"
......@@ -3123,24 +3123,24 @@
loclnum="486" loccnumb="6" loccnume="22"
sum="9a591815b28d479aa9112764a1da0eaf"
proved="true"
expanded="true"
expanded="false"
shape="aeval_fmlaV1V2V0qaeval_fmlaV1aConsaTuple2V3V4V2V0Iafresh_in_fmlaV3V0F">
<transf
name="induction_ty_lex"
proved="true"
expanded="true">
expanded="false">
<goal
name="eval_change_free.1"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="486" loccnumb="6" loccnume="22"
sum="c5cd871dd0d4a59c996215921b07d9a3"
proved="true"
expanded="true"
expanded="false"
shape="CV0aFtermVaeval_fmlaV2V3V0qaeval_fmlaV2aConsaTuple2V4V5V3V0Iafresh_in_fmlaV4V0FaFandVVaeval_fmlaV8V9V0qaeval_fmlaV8aConsaTuple2V10V11V9V0Iafresh_in_fmlaV10V0FIaeval_fmlaV12V13V6qaeval_fmlaV12aConsaTuple2V14V15V13V6Iafresh_in_fmlaV14V6FIaeval_fmlaV16V17V7qaeval_fmlaV16aConsaTuple2V18V19V17V7Iafresh_in_fmlaV18V7FaFnotVaeval_fmlaV21V22V0qaeval_fmlaV21aConsaTuple2V23V24V22V0Iafresh_in_fmlaV23V0FIaeval_fmlaV25V26V20qaeval_fmlaV25aConsaTuple2V27V28V26V20Iafresh_in_fmlaV27V20FaFimpliesVVaeval_fmlaV31V32V0qaeval_fmlaV31aConsaTuple2V33V34V32V0Iafresh_in_fmlaV33V0FIaeval_fmlaV35V36V29qaeval_fmlaV35aConsaTuple2V37V38V36V29Iafresh_in_fmlaV37V29FIaeval_fmlaV39V40V30qaeval_fmlaV39aConsaTuple2V41V42V40V30Iafresh_in_fmlaV41V30FaFletVVVaeval_fmlaV46V47V0qaeval_fmlaV46aConsaTuple2V48V49V47V0Iafresh_in_fmlaV48V0FIaeval_fmlaV50V51V45qaeval_fmlaV50aConsaTuple2V52V53V51V45Iafresh_in_fmlaV52V45FaFforallVVVaeval_fmlaV57V58V0qaeval_fmlaV57aConsaTuple2V59V60V58V0Iafresh_in_fmlaV59V0FIaeval_fmlaV61V62V56qaeval_fmlaV61aConsaTuple2V63V64V62V56Iafresh_in_fmlaV63V56FF">
<transf
name="split_goal_wp"
proved="true"
expanded="true">
expanded="false">
<goal
name="eval_change_free.1.1"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
......@@ -3603,7 +3603,7 @@
loclnum="486" loccnumb="6" loccnume="22"
sum="5ad5870b9ebfd5198cae075473953562"
proved="true"
expanded="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVaeval_fmlaV10V11V0Iaeval_fmlaV10aConsaTuple2V12V13V11V0Iafresh_in_fmlaV12V0FIaeval_fmlaV14V15V9qaeval_fmlaV14aConsaTuple2V16V17V15V9Iafresh_in_fmlaV16V9FaFforallVVVtF">
<proof
prover="1"
......@@ -3669,7 +3669,7 @@
loclnum="486" loccnumb="6" loccnume="22"
sum="b8230b2ea8a4a80f33e7afe9cc6f0bb1"
proved="true"
expanded="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVaeval_fmlaV10aConsaTuple2V12V13V11V0Iaeval_fmlaV10V11V0Iafresh_in_fmlaV12V0FIaeval_fmlaV14V15V9qaeval_fmlaV14aConsaTuple2V16V17V15V9Iafresh_in_fmlaV16V9FaFforallVVVtF">
<proof
prover="1"
......@@ -3735,7 +3735,7 @@
loclnum="486" loccnumb="6" loccnume="22"
sum="c21693a82bc418647be9de0023c336c8"
proved="true"
expanded="true"
expanded="false"
shape="CV0aFtermVtaFandVVtaFnotVtaFimpliesVVtaFletVVVtaFforallVVVaeval_fmlaV13V14V0Iaeval_fmlaV13aConsaTuple2V15V16V14V0Iafresh_in_fmlaV15V0FIaeval_fmlaV17V18V12qaeval_fmlaV17aConsaTuple2V19V20V18V12Iafresh_in_fmlaV19V12FF">
<proof
prover="1"
......@@ -4881,394 +4881,15 @@
proved="true"
expanded="false"
shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F">
<transf
name="induction_ty_lex"
proved="true"
expanded="false">
<goal
name="wp_preserved_by_reduction.1"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="2c3eb9e03056d7dd7e77025450a7dc7f"
proved="true"
expanded="false"
shape="CV4aSskipaeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5FaSassignVVaeval_fmlaV1V3awpV9V10Iaeval_fmlaV0V2awpV4V10FIaone_stepV0V2V4V1V3V9FaSseqVVaeval_fmlaV1V3awpV13V14Iaeval_fmlaV0V2awpV4V14FIaone_stepV0V2V4V1V3V13FIaeval_fmlaV1V3awpV15V16Iaeval_fmlaV0V2awpV11V16FIaone_stepV0V2V11V1V3V15FIaeval_fmlaV1V3awpV17V18Iaeval_fmlaV0V2awpV12V18FIaone_stepV0V2V12V1V3V17FaSifVVVaeval_fmlaV1V3awpV22V23Iaeval_fmlaV0V2awpV4V23FIaone_stepV0V2V4V1V3V22FIaeval_fmlaV1V3awpV24V25Iaeval_fmlaV0V2awpV20V25FIaone_stepV0V2V20V1V3V24FIaeval_fmlaV1V3awpV26V27Iaeval_fmlaV0V2awpV21V27FIaone_stepV0V2V21V1V3V26FaSassertVaeval_fmlaV1V3awpV29V30Iaeval_fmlaV0V2awpV4V30FIaone_stepV0V2V4V1V3V29FaSwhileVVVaeval_fmlaV1V3awpV34V35Iaeval_fmlaV0V2awpV4V35FIaone_stepV0V2V4V1V3V34FIaeval_fmlaV1V3awpV36V37Iaeval_fmlaV0V2awpV33V37FIaone_stepV0V2V33V1V3V36FF">
<transf
name="split_goal_wp"
proved="true"
expanded="false">
<goal
name="wp_preserved_by_reduction.1.1"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="8ddeea390a07fde75ee6eee7c0a69f99"
proved="true"
expanded="false"
shape="CV4aSskipaeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5FaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.32"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.19"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.39"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.14"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.09"/>
</proof>
</goal>
<goal
name="wp_preserved_by_reduction.1.2"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="12acada10a801ad628647b25dae645c0"
proved="true"
expanded="false"
shape="CV4aSskiptaSassignVVaeval_fmlaV1V3awpV7V8Iaeval_fmlaV0V2awpV4V8FIaone_stepV0V2V4V1V3V7FaSseqVVtaSifVVVtaSassertVtaSwhileVVVtF">
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.04"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.06"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.02"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.04"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.13"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.11"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="1000"
edited="blocking_semantics5_WP_wp_preserved_by_reduction_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.94"/>
</proof>
</goal>
<goal
name="wp_preserved_by_reduction.1.3"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="89fea236b68e19d1290baf9e87cea08e"
proved="true"
expanded="false"
shape="CV4aSskiptaSassignVVtaSseqVVaeval_fmlaV1V3awpV9V10Iaeval_fmlaV0V2awpV4V10FIaone_stepV0V2V4V1V3V9FIaeval_fmlaV1V3awpV11V12Iaeval_fmlaV0V2awpV7V12FIaone_stepV0V2V7V1V3V11FIaeval_fmlaV1V3awpV13V14Iaeval_fmlaV0V2awpV8V14FIaone_stepV0V2V8V1V3V13FaSifVVVtaSassertVtaSwhileVVVtF">
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.05"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="17.95"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.02"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="21.92"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.07"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.09"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="1000"
edited="blocking_semantics5_WP_wp_preserved_by_reduction_2.v"
obsolete="false"
archived="false">
<result status="valid" time="1.11"/>
</proof>
</goal>
<goal
name="wp_preserved_by_reduction.1.4"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="e3376fca7aeb65d4ed7265c151a5136f"
proved="true"
expanded="false"
shape="CV4aSskiptaSassignVVtaSseqVVtaSifVVVaeval_fmlaV1V3awpV12V13Iaeval_fmlaV0V2awpV4V13FIaone_stepV0V2V4V1V3V12FIaeval_fmlaV1V3awpV14V15Iaeval_fmlaV0V2awpV10V15FIaone_stepV0V2V10V1V3V14FIaeval_fmlaV1V3awpV16V17Iaeval_fmlaV0V2awpV11V17FIaone_stepV0V2V11V1V3V16FaSassertVtaSwhileVVVtF">
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="4.02"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.08"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="15.40"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.12"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.14"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.08"/>
</proof>
</goal>
<goal
name="wp_preserved_by_reduction.1.5"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="3719944ccda6ed455967502e408d738a"
proved="true"
expanded="false"
shape="CV4aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVaeval_fmlaV1V3awpV13V14Iaeval_fmlaV0V2awpV4V14FIaone_stepV0V2V4V1V3V13FaSwhileVVVtF">
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.18"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.14"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.18"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="outofmemory" time="25.82"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.07"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.13"/>
</proof>
</goal>
<goal
name="wp_preserved_by_reduction.1.6"
locfile="blocking_semantics5/../blocking_semantics5.mlw"
loclnum="696" loccnumb="8" loccnume="33"
sum="85e8dba3b85659d5c8105992d3ce3698"
proved="true"
expanded="false"
shape="CV4aSskiptaSassignVVtaSseqVVtaSifVVVtaSassertVtaSwhileVVVaeval_fmlaV1V3awpV16V17Iaeval_fmlaV0V2awpV4V17FIaone_stepV0V2V4V1V3V16FIaeval_fmlaV1V3awpV18V19Iaeval_fmlaV0V2awpV15V19FIaone_stepV0V2V15V1V3V18FF">
<proof
prover="1"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="outofmemory" time="20.31"/>
</proof>
<proof
prover="3"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.03"/>
</proof>
<proof
prover="0"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.02"/>
</proof>
<proof
prover="4"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.06"/>
</proof>
<proof
prover="7"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.13"/>
</proof>
<proof
prover="6"
timelimit="30"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="30.12"/>
</proof>
<proof
prover="5"
timelimit="30"
memlimit="1000"
edited="blocking_semantics5_WP_wp_preserved_by_reduction_3.v"
obsolete="false"
archived="false">
<result status="valid" time="1.21"/>
</proof>
</goal>
</transf>
</goal>
</transf>
<proof
prover="5"
timelimit="5"
memlimit="4000"
edited="blocking_semantics5_WP_wp_preserved_by_reduction_4.v"
obsolete="false"
archived="false">
<result status="valid" time="6.78"/>
</proof>
</goal>
<goal
name="progress"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment