updated proof

parent 9bbbcb61
......@@ -7,12 +7,16 @@
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<file
name="../same_fringe.mlw"
verified="true"
expanded="false">
expanded="true">
<theory
name="SameFringe"
locfile="../same_fringe.mlw"
......@@ -24,7 +28,7 @@
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
expl="VC for enum"
sum="bac40cccc22ed75ba7eef3c4a5a0af2a"
sum="7dff3fa5c1413287a3468bc32e6ab807"
proved="true"
expanded="true"
shape="CV0aEmptyainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aNodeVVVainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FAainfix &lt;alengthaelementsV2alengthaelementsV0Aainfix &lt;=c0alengthaelementsV0F">
......@@ -39,7 +43,7 @@
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
expl="1. postcondition"
sum="21fe9b1bcb70c32e377266edee64b50e"
sum="7218904307e865eb69cc519a9d7e4db5"
proved="true"
expanded="true"
shape="CV0aEmptyainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aNodeVVVtF">
......@@ -59,7 +63,7 @@
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
expl="2. variant decrease"
sum="5c362974e3e66efddbe35b1ef2acdeff"
sum="4a60f331193ad3c45b9968f62d0fdf98"
proved="true"
expanded="true"
shape="CV0aEmptytaNodeVVVainfix &lt;alengthaelementsV2alengthaelementsV0Aainfix &lt;=c0alengthaelementsV0F">
......@@ -79,7 +83,7 @@
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
expl="3. postcondition"
sum="899561acb862d9fcb7633681ede19024"
sum="faeacd4d5e3fb432239aeafe7aa41c9b"
proved="true"
expanded="true"
shape="CV0aEmptytaNodeVVVainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FF">
......@@ -101,10 +105,10 @@
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="VC for eq_enum"
sum="17387998d624297720d94c7ea4f4ffe3"
sum="079da6d4fa1b02402a49e314bf8f3a1a"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueAainfix =V5V2Iainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFAainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4Fwainfix =aenum_elementsV0aenum_elementsV1NaDoneCV0aDoneainfix =aenum_elementsV0aenum_elementsV1wainfix =aenum_elementsV0aenum_elementsV1NF">
shape="CV1aNextVVVCV0aNextVVViainfix =V5V2ainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFAainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4Fainfix =aenum_elementsV0aenum_elementsV1Nwainfix =aenum_elementsV0aenum_elementsV1NaDoneCV0aDoneainfix =aenum_elementsV0aenum_elementsV1wainfix =aenum_elementsV0aenum_elementsV1NF">
<label
name="expl:VC for eq_enum"/>
<transf
......@@ -116,10 +120,10 @@
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="1. variant decrease"
sum="1e1a01398f54e6fb5496fdea8d6c9f01"
sum="107c6b8106a173dbd801060d3475add8"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FwtaDonetF">
shape="CV1aNextVVVCV0aNextVVVainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2wtaDonetF">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -131,7 +135,7 @@
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -144,10 +148,10 @@
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="2. postcondition"
sum="4c78ad0d6c5101fd6448da9520cc20bc"
sum="98c3bed21b432ee674b7b3570d8c5189"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueAainfix =V5V2Iainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFIainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FwtaDonetF">
shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFIainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2wtaDonetF">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -164,7 +168,27 @@
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="3. postcondition"
sum="bdaec892866bbbde9a5705fa0756c4c9"
sum="b98a2a3da51a5b19e0dc2dcb5355ee44"
proved="true"
expanded="false"
shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1NIainfix =V5V2NwtaDonetF">
<label
name="expl:VC for eq_enum"/>
<proof
prover="1"
timelimit="10"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
name="WP_parameter eq_enum.4"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="4. postcondition"
sum="a88b53fd0b760e6104de8cd246e982f4"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVtwainfix =aenum_elementsV0aenum_elementsV1NaDonetF">
......@@ -180,11 +204,11 @@
</proof>
</goal>
<goal
name="WP_parameter eq_enum.4"
name="WP_parameter eq_enum.5"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="4. postcondition"
sum="6d45465cf50f326baba1e1702f9f155c"
expl="5. postcondition"
sum="0dabfe76e7db8d01d0f96d8dd8be704e"
proved="true"
expanded="true"
shape="CV1aNextVVVtaDoneCV0aDoneainfix =aenum_elementsV0aenum_elementsV1wtF">
......@@ -200,11 +224,11 @@
</proof>
</goal>
<goal
name="WP_parameter eq_enum.5"
name="WP_parameter eq_enum.6"
locfile="../same_fringe.mlw"
loclnum="48" loccnumb="10" loccnume="17"
expl="5. postcondition"
sum="592204cd012136f778811fdbb0844d1d"
expl="6. postcondition"
sum="d6076076174b95ff54f6ddb8d3e783f9"
proved="true"
expanded="true"
shape="CV1aNextVVVtaDoneCV0aDonetwainfix =aenum_elementsV0aenum_elementsV1NF">
......@@ -226,7 +250,7 @@
locfile="../same_fringe.mlw"
loclnum="59" loccnumb="6" loccnume="17"
expl="VC for same_fringe"
sum="83c0f2fffee77a0707df98739479164e"
sum="f98d3647758a24cb6221a5fb9a058726"
proved="true"
expanded="true"
shape="ainfix =aelementsV0aelementsV1qainfix =V4aTrueIainfix =aenum_elementsV3aenum_elementsV2qainfix =V4aTrueFIainfix =aenum_elementsV3ainfix ++aelementsV0aenum_elementsaDoneFIainfix =aenum_elementsV2ainfix ++aelementsV1aenum_elementsaDoneFF">
......
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