Commit bd6d67ef authored by Andrei Paskevich's avatar Andrei Paskevich

update session files

parent 48c29c43
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw" locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum="13" loccnumb="6" loccnume="9" loclnum="13" loccnumb="6" loccnume="9"
expl="parameter sum" expl="parameter sum"
sum="ab6ece0ccf048de22ee253bbefd81b26" sum="2aa5aa37364097fffd4757203fa00fcc"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF"> shape="iainfix <=V4V1ainfix <ainfix -V1V6ainfix -V1V4Aainfix <=c0ainfix -V1V4Aainfix =V5asumV2c1V6Aainfix <=V6ainfix +V1c1Aainfix <=c1V6Iainfix =V6ainfix +V4c1FIainfix =V5ainfix +V3agetV2V4FAainfix <V4V0Aainfix <=c0V4ainfix =V3asumV2c1ainfix +V1c1Iainfix =V3asumV2c1V4Aainfix <=V4ainfix +V1c1Aainfix <=c1V4FFAainfix =c0asumV2c1c1Aainfix <=c1ainfix +V1c1Aainfix <=c1c1Iainfix <V1V0Aainfix <=c0V1FFF">
...@@ -52,7 +52,7 @@ ...@@ -52,7 +52,7 @@
locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw" locfile="programs/assigning_meanings_to_programs/../assigning_meanings_to_programs.mlw"
loclnum="39" loccnumb="6" loccnume="14" loclnum="39" loccnumb="6" loccnume="14"
expl="parameter division" expl="parameter division"
sum="4ae56abf35642f92abc882dea8823761" sum="3e2f94bf7a9ca10dd00db606c0735125"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF"> shape="iainfix >=V2V1ainfix <V4V2Aainfix <=c0V2Aainfix =V0ainfix +ainfix *V5V1V4Aainfix <=c0V4Iainfix =V5ainfix +V3c1FIainfix =V4ainfix -V2V1Fainfix =V0ainfix +ainfix *V3V1V2Aainfix <V2V1Aainfix <=c0V2Iainfix =V0ainfix +ainfix *V3V1V2Aainfix <=c0V2FFAainfix =V0ainfix +ainfix *c0V1V0Aainfix <=c0V0Iainfix <c0V1Aainfix <=c0V0FF">
......
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
locfile="programs/binary_search/../binary_search.mlw" locfile="programs/binary_search/../binary_search.mlw"
loclnum="17" loccnumb="6" loccnume="19" loclnum="17" loccnumb="6" loccnume="19"
expl="parameter binary_search" expl="parameter binary_search"
sum="01f4f15024cb46b8dde333e7be87903b" sum="f8c12c2ff9cb894549acb66daf7b4619"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF"> shape="iainfix <=V4V3iainfix <agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V3V5ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V6V3Aainfix <=V5V6Iainfix =agetV2V6V1Iainfix <V6V0Aainfix <=c0V6FAainfix <V3V0Aainfix <=c0V5Iainfix =V5ainfix +ainfix +V4adivainfix -V3V4c2c1Fiainfix >agetV2ainfix +V4adivainfix -V3V4c2V1ainfix <ainfix -V7V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V7Aainfix <=V4V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V7V0Aainfix <=c0V4Iainfix =V7ainfix -ainfix +V4adivainfix -V3V4c2c1Fainfix =agetV2ainfix +V4adivainfix -V3V4c2V1Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <ainfix +V4adivainfix -V3V4c2V0Aainfix <=c0ainfix +V4adivainfix -V3V4c2Aainfix <=ainfix +V4adivainfix -V3V4c2V3Aainfix <=V4ainfix +V4adivainfix -V3V4c2ainfix =agetV2V9V1NIainfix <V9V0Aainfix <=c0V9FIainfix <=V10V3Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V11ainfix -V0c1Aainfix <=c0V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V12agetV2V13Iainfix <V13V0Aainfix <=V12V13Aainfix <=c0V12FFFF">
...@@ -59,7 +59,7 @@ ...@@ -59,7 +59,7 @@
locfile="programs/binary_search/../binary_search.mlw" locfile="programs/binary_search/../binary_search.mlw"
loclnum="59" loccnumb="6" loccnume="19" loclnum="59" loccnumb="6" loccnume="19"
expl="parameter binary_search" expl="parameter binary_search"
sum="4d2d8b250c84dcb1cca8870c974bbcd1" sum="e5e36982c9bb33a11e966b564dfa8b9b"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <=V4V3iainfix <agetV2V5V1ainfix <ainfix -V3V6ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V7V3Aainfix <=V6V7Iainfix =agetV2V7V1Iainfix <V7V0Aainfix <=c0V7FAainfix <V3V0Aainfix <=c0V6Iainfix =V6ainfix +V5c1Fiainfix >agetV2V5V1ainfix <ainfix -V8V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V9V8Aainfix <=V4V9Iainfix =agetV2V9V1Iainfix <V9V0Aainfix <=c0V9FAainfix <V8V0Aainfix <=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Iainfix <=V5V3Aainfix <=V4V5FAainfix <=V4V3ainfix =agetV2V10V1NIainfix <V10V0Aainfix <=c0V10FIainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FFFF"> shape="iainfix <=V4V3iainfix <agetV2V5V1ainfix <ainfix -V3V6ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V7V3Aainfix <=V6V7Iainfix =agetV2V7V1Iainfix <V7V0Aainfix <=c0V7FAainfix <V3V0Aainfix <=c0V6Iainfix =V6ainfix +V5c1Fiainfix >agetV2V5V1ainfix <ainfix -V8V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V9V8Aainfix <=V4V9Iainfix =agetV2V9V1Iainfix <V9V0Aainfix <=c0V9FAainfix <V8V0Aainfix <=c0V4Iainfix =V8ainfix -V5c1Fainfix =agetV2V5V1Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Aainfix <V5V0Aainfix <=c0V5Iainfix <=V5V3Aainfix <=V4V5FAainfix <=V4V3ainfix =agetV2V10V1NIainfix <V10V0Aainfix <=c0V10FIainfix <=V11V3Aainfix <=V4V11Iainfix =agetV2V11V1Iainfix <V11V0Aainfix <=c0V11FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V12ainfix -V0c1Aainfix <=c0V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <ainfix -V0c1V0Aainfix <=c0c0Iainfix <=agetV2V13agetV2V14Iainfix <V14V0Aainfix <=V13V14Aainfix <=c0V13FFFF">
...@@ -86,7 +86,7 @@ ...@@ -86,7 +86,7 @@
locfile="programs/binary_search/../binary_search.mlw" locfile="programs/binary_search/../binary_search.mlw"
loclnum="99" loccnumb="6" loccnume="19" loclnum="99" loccnumb="6" loccnume="19"
expl="parameter binary_search" expl="parameter binary_search"
sum="c426f5bceb7394f61477135985a213e4" sum="673c686736f86d8bd075c49720af3e5d"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <=V4V3Lainfix -V3V4Lainfix +V4adivV5c2iainfix <agetV2V6V1ainfix <ainfix -V3V7ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V3Aainfix <=V7V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V7Iainfix =V7ainfix +V6c1FAainfix <=ainfix +V6c1amax_intAainfix <=amin_intainfix +V6c1iainfix >agetV2V6V1ainfix <ainfix -V9V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V9Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V9V0Aainfix <=c0V4Iainfix =V9ainfix -V6c1FAainfix <=ainfix -V6c1amax_intAainfix <=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <=V6V3Aainfix <=V4V6Aainfix <=ainfix +V4adivV5c2amax_intAainfix <=amin_intainfix +V4adivV5c2Aainfix <=ainfix -V3V4amax_intAainfix <=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix <V11V0Aainfix <=c0V11FIainfix <=V12V3Aainfix <=V4V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V13ainfix -V0c1Aainfix <=c0V13Iainfix =agetV2V13V1Iainfix <V13V0Aainfix <=c0V13FAainfix <ainfix -V0c1V0Aainfix <=c0c0Aainfix <=ainfix -V0c1amax_intAainfix <=amin_intainfix -V0c1Iainfix <=agetV2V14agetV2V15Iainfix <V15V0Aainfix <=V14V15Aainfix <=c0V14FAainfix <=V0amax_intAainfix <=c0V0FFF"> shape="iainfix <=V4V3Lainfix -V3V4Lainfix +V4adivV5c2iainfix <agetV2V6V1ainfix <ainfix -V3V7ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V8V3Aainfix <=V7V8Iainfix =agetV2V8V1Iainfix <V8V0Aainfix <=c0V8FAainfix <V3V0Aainfix <=c0V7Iainfix =V7ainfix +V6c1FAainfix <=ainfix +V6c1amax_intAainfix <=amin_intainfix +V6c1iainfix >agetV2V6V1ainfix <ainfix -V9V4ainfix -V3V4Aainfix <=c0ainfix -V3V4Aainfix <=V10V9Aainfix <=V4V10Iainfix =agetV2V10V1Iainfix <V10V0Aainfix <=c0V10FAainfix <V9V0Aainfix <=c0V4Iainfix =V9ainfix -V6c1FAainfix <=ainfix -V6c1amax_intAainfix <=amin_intainfix -V6c1ainfix =agetV2V6V1Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <V6V0Aainfix <=c0V6Aainfix <=V6V3Aainfix <=V4V6Aainfix <=ainfix +V4adivV5c2amax_intAainfix <=amin_intainfix +V4adivV5c2Aainfix <=ainfix -V3V4amax_intAainfix <=amin_intainfix -V3V4ainfix =agetV2V11V1NIainfix <V11V0Aainfix <=c0V11FIainfix <=V12V3Aainfix <=V4V12Iainfix =agetV2V12V1Iainfix <V12V0Aainfix <=c0V12FAainfix <V3V0Aainfix <=c0V4FFAainfix <=V13ainfix -V0c1Aainfix <=c0V13Iainfix =agetV2V13V1Iainfix <V13V0Aainfix <=c0V13FAainfix <ainfix -V0c1V0Aainfix <=c0c0Aainfix <=ainfix -V0c1amax_intAainfix <=amin_intainfix -V0c1Iainfix <=agetV2V14agetV2V15Iainfix <V15V0Aainfix <=V14V15Aainfix <=c0V14FAainfix <=V0amax_intAainfix <=c0V0FFF">
...@@ -98,7 +98,7 @@ ...@@ -98,7 +98,7 @@
timelimit="5" timelimit="5"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.14"/> <result status="valid" time="0.15"/>
</proof> </proof>
</goal> </goal>
</theory> </theory>
......
...@@ -32,7 +32,7 @@ ...@@ -32,7 +32,7 @@
name="invariant_is_ok" name="invariant_is_ok"
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="35" loccnumb="8" loccnume="23" loclnum="35" loccnumb="8" loccnume="23"
sum="beff13e8611b37422ec4e085840b924a" sum="efb912c30d9e16a8d30a0911aab80d9d"
proved="true" proved="true"
expanded="true" expanded="true"
shape="abestV0V1Iainvariant_V0V1V2F"> shape="abestV0V1Iainvariant_V0V1V2F">
...@@ -42,7 +42,7 @@ ...@@ -42,7 +42,7 @@
edited="bresenham_WP_M_invariant_is_ok_1.v" edited="bresenham_WP_M_invariant_is_ok_1.v"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="1.23"/> <result status="valid" time="1.26"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -50,7 +50,7 @@ ...@@ -50,7 +50,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="parameter bresenham" expl="parameter bresenham"
sum="bcba2edf5dd35515e1700353a55dd929" sum="ec58d7f3477f9d697ce5bc3ec2d0ce0b"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0"> shape="iainfix <V0c0ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2Fainfix <ainfix -ainfix +ax2c1V7ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Aainvariant_V7V5V6Aainfix <=V7ainfix +ax2c1Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V6ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V5ainfix +V1c1FAabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFFAainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
...@@ -66,7 +66,7 @@ ...@@ -66,7 +66,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="loop invariant init" expl="loop invariant init"
sum="f83e0e8a8cfce051a259c6cf27b5820d" sum="e867126400d30cca57667f4a386beefe"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0"> shape="ainvariant_c0c0ainfix -ainfix *c2ay2ax2Aainfix <=c0ainfix +ax2c1Aainfix <=c0c0">
...@@ -100,7 +100,7 @@ ...@@ -100,7 +100,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="assertion" expl="assertion"
sum="2950c4b04670596cf7d332f5768f61ad" sum="ebd8d765087c46d4c451499df5884eb7"
proved="true" proved="true"
expanded="true" expanded="true"
shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"> shape="abestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
...@@ -127,7 +127,7 @@ ...@@ -127,7 +127,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="loop invariant preservation" expl="loop invariant preservation"
sum="9cd6a0795c9927aec161ff90632a079e" sum="5f0f31c42ee4d9c677117b01c806bbc3"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"> shape="ainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
...@@ -146,7 +146,7 @@ ...@@ -146,7 +146,7 @@
timelimit="10" timelimit="10"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.01"/> <result status="valid" time="0.00"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -154,7 +154,7 @@ ...@@ -154,7 +154,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="loop variant decreases" expl="loop variant decreases"
sum="8f8807827d192fee3af94a9f86612c8e" sum="f2e94c2030c552b8f3163cd22ddf0dd4"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"> shape="ainfix <ainfix -ainfix +ax2c1V4ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V4V1V3Aainfix <=V4ainfix +ax2c1Aainfix <=c0V4Iainfix =V4ainfix +V2c1FIainfix =V3ainfix +V0ainfix *c2ay2FIainfix <V0c0IabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
...@@ -188,7 +188,7 @@ ...@@ -188,7 +188,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="loop invariant preservation" expl="loop invariant preservation"
sum="48406b48feb2d0d50220609b923257fd" sum="fe0d08f0dc86b35d8d29b27a5d6e6e25"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"> shape="ainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
...@@ -215,7 +215,7 @@ ...@@ -215,7 +215,7 @@
locfile="programs/bresenham/../bresenham.mlw" locfile="programs/bresenham/../bresenham.mlw"
loclnum="37" loccnumb="6" loccnume="15" loclnum="37" loccnumb="6" loccnume="15"
expl="loop variant decreases" expl="loop variant decreases"
sum="71f61a751cf75317ec9b98cbc852ce43" sum="a55a100c6d28b8b08514c9f2fc389a08"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF"> shape="ainfix <ainfix -ainfix +ax2c1V5ainfix -ainfix +ax2c1V2Aainfix <=c0ainfix -ainfix +ax2c1V2Iainvariant_V5V3V4Aainfix <=V5ainfix +ax2c1Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix =V4ainfix +V0ainfix *c2ainfix -ay2ax2FIainfix =V3ainfix +V1c1FIainfix <V0c0NIabestV2V1Iainfix <=V2ax2Iainvariant_V2V1V0Aainfix <=V2ainfix +ax2c1Aainfix <=c0V2FFF">
...@@ -234,7 +234,7 @@ ...@@ -234,7 +234,7 @@
timelimit="10" timelimit="10"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.01"/>
</proof> </proof>
<proof <proof
prover="0" prover="0"
......
...@@ -25,7 +25,7 @@ ...@@ -25,7 +25,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="parameter routine" expl="parameter routine"
sum="3bf53e6f38348a8fdfffc6473f681188" sum="291741da10e028832fd0d84557fb52f1"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <V2V0iainfix <=V3V2ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1Fainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV7Aainfix <=V7V0Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix =V1afactV0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F"> shape="iainfix <V2V0iainfix <=V3V2ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Aainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1Fainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =V4afactV7Aainfix <=V7V0Aainfix <=c0V7Iainfix =V7ainfix +V2c1FIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFAainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1ainfix =V1afactV0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFAainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
...@@ -41,7 +41,7 @@ ...@@ -41,7 +41,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="loop invariant init" expl="loop invariant init"
sum="496d4e9dc9d08ddfdcd951cf9579dd08" sum="dd94a8debb18c08dfb22964ea561eb85"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F"> shape="ainfix =c1afactc0Aainfix <=c0V0Aainfix <=c0c0Iainfix >=V0c0F">
...@@ -61,7 +61,7 @@ ...@@ -61,7 +61,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="loop invariant init" expl="loop invariant init"
sum="4b41a40f971c37b7d3a545063e77d98a" sum="7ecbf54a0f3b0b3380a4941b2ab3bc24"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"> shape="ainfix =V1ainfix *c1afactV2Aainfix <=c1ainfix +V2c1Aainfix <=c1c1Iainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
...@@ -81,7 +81,7 @@ ...@@ -81,7 +81,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="loop invariant preservation" expl="loop invariant preservation"
sum="a9aa19c076fdf7448f828ea2e8a96dc9" sum="6b99142cc6dab407500b962a73a00f32"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"> shape="ainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
...@@ -101,7 +101,7 @@ ...@@ -101,7 +101,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="loop variant decreases" expl="loop variant decreases"
sum="c4417face0d7e00423a2c5db7f7c29d2" sum="b776c57b3a50d4bbd1d169ea7254033b"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"> shape="ainfix <ainfix -V2V6ainfix -V2V3Aainfix <=c0ainfix -V2V3Iainfix =V5ainfix *V6afactV2Aainfix <=V6ainfix +V2c1Aainfix <=c1V6Iainfix =V6ainfix +V3c1FIainfix =V5ainfix +V4V1FIainfix <=V3V2Iainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
...@@ -121,7 +121,7 @@ ...@@ -121,7 +121,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="loop invariant preservation" expl="loop invariant preservation"
sum="b196a86eadd3e167f070cd667cdb9cd0" sum="1f2030cc417fe008d71b90b7147f8152"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"> shape="ainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
...@@ -133,7 +133,7 @@ ...@@ -133,7 +133,7 @@
timelimit="10" timelimit="10"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.00"/> <result status="valid" time="0.01"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -141,7 +141,7 @@ ...@@ -141,7 +141,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="loop variant decreases" expl="loop variant decreases"
sum="27d4461c1f444047a13219624ec0fb12" sum="0f2a68a43370710a5a10b17c321b9b0b"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"> shape="ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =V4afactV5Aainfix <=V5V0Aainfix <=c0V5Iainfix =V5ainfix +V2c1FIainfix <=V3V2NIainfix =V4ainfix *V3afactV2Aainfix <=V3ainfix +V2c1Aainfix <=c1V3FFIainfix <V2V0Iainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
...@@ -161,7 +161,7 @@ ...@@ -161,7 +161,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="13" loccnumb="6" loccnume="13" loclnum="13" loccnumb="6" loccnume="13"
expl="normal postcondition" expl="normal postcondition"
sum="3b7319c898f84f53e057504fbb75799d" sum="72fa7e7e9aa7ff066f2b9119bf0a0868"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V1afactV0Iainfix <V2V0NIainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F"> shape="ainfix =V1afactV0Iainfix <V2V0NIainfix =V1afactV2Aainfix <=V2V0Aainfix <=c0V2FFIainfix >=V0c0F">
...@@ -183,7 +183,7 @@ ...@@ -183,7 +183,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="34" loccnumb="6" loccnume="14" loclnum="34" loccnumb="6" loccnume="14"
expl="parameter routine2" expl="parameter routine2"
sum="19c613019a4c45b829e84d9095a008ce" sum="0da4e019fa76bf569aa23267a670b659"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1Aainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFAainfix =c1afactc0Iainfix <=c0ainfix -V0c1Aainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F"> shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1Aainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFAainfix =c1afactc0Iainfix <=c0ainfix -V0c1Aainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F">
...@@ -199,7 +199,7 @@ ...@@ -199,7 +199,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="34" loccnumb="6" loccnume="14" loclnum="34" loccnumb="6" loccnume="14"
expl="normal postcondition" expl="normal postcondition"
sum="48b27d3e4b5e9d2fba88970f72a5a0de" sum="83496f7885f21e2b5d1fa1789ac571be"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F"> shape="ainfix =c1afactV0Iainfix >c0ainfix -V0c1Iainfix >=V0c0F">
...@@ -219,7 +219,7 @@ ...@@ -219,7 +219,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="34" loccnumb="6" loccnume="14" loclnum="34" loccnumb="6" loccnume="14"
expl="for loop initialization" expl="for loop initialization"
sum="32b38dfb9a33bfe592b8b970fce3d924" sum="6795593e5e428f68351a6f3b3f2e73de"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =c1afactc0Iainfix <=c0ainfix -V0c1Iainfix >=V0c0F"> shape="ainfix =c1afactc0Iainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
...@@ -239,7 +239,7 @@ ...@@ -239,7 +239,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="34" loccnumb="6" loccnume="14" loclnum="34" loccnumb="6" loccnume="14"
expl="for loop preservation" expl="for loop preservation"
sum="51b1ac0ea0c96e90b9450667444ebc35" sum="e220952b89311d868a301c4d8e7330fc"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"> shape="ainfix =V3afactainfix +V2c1Iainfix =V3ainfix *ainfix +V2c1afactV2Aainfix =V5ainfix *ainfix +V4c1afactV2Iainfix =V5ainfix +V3V1FIainfix =V3ainfix *V4afactV2Iainfix <=V4V2Aainfix <=c1V4FFAainfix =V1ainfix *c1afactV2Iainfix <=c1V2Aainfix =V1afactainfix +V2c1Iainfix >c1V2Iainfix =V1afactV2Iainfix <=V2ainfix -V0c1Aainfix <=c0V2FFIainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
...@@ -251,7 +251,7 @@ ...@@ -251,7 +251,7 @@
timelimit="10" timelimit="10"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.01"/> <result status="valid" time="0.02"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -259,7 +259,7 @@ ...@@ -259,7 +259,7 @@
locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw" locfile="programs/checking_a_large_routine/../checking_a_large_routine.mlw"
loclnum="34" loccnumb="6" loccnume="14" loclnum="34" loccnumb="6" loccnume="14"
expl="normal postcondition" expl="normal postcondition"
sum="4f1bfc1d3b1c252f14bed06c8c61d7ad" sum="550dc6f829ce2485a14ba4a27c49216f"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1FIainfix <=c0ainfix -V0c1Iainfix >=V0c0F"> shape="ainfix =V1afactV0Iainfix =V1afactainfix +ainfix -V0c1c1FIainfix <=c0ainfix -V0c1Iainfix >=V0c0F">
......
...@@ -40,7 +40,7 @@ ...@@ -40,7 +40,7 @@
name="decrease1_induction" name="decrease1_induction"
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="17" loccnumb="8" loccnume="27" loclnum="17" loccnumb="8" loccnume="27"
sum="e4ed02982122ea650ffced258963beee" sum="b3ac1578e588f434e668cb2609763397"
proved="true" proved="true"
expanded="true" expanded="true"
shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F"> shape="ainfix >=amixfix []V0V2ainfix -ainfix +amixfix []V0V1V1V2Iainfix <V2alengthV0Aainfix <=V1V2Aainfix <=c0V1FIadecrease1V0F">
...@@ -50,7 +50,7 @@ ...@@ -50,7 +50,7 @@
edited="decrease1_Decrease1_decrease1_induction_2.v" edited="decrease1_Decrease1_decrease1_induction_2.v"
obsolete="false" obsolete="false"
archived="false"> archived="false">
<result status="valid" time="0.59"/> <result status="valid" time="0.60"/>
</proof> </proof>
</goal> </goal>
<goal <goal
...@@ -58,7 +58,7 @@ ...@@ -58,7 +58,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="parameter search" expl="parameter search"
sum="a5a5d63ce42315e11e304e326f930813" sum="8cc82d81ea36a7d743bad8916aa747a0"
proved="true" proved="true"
expanded="true" expanded="true"
shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF"> shape="iainfix <V2V0iainfix =agetV1V2c0ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1iainfix >agetV1V2c0ainfix <ainfix -V0V5ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V6c0NIainfix <V6V0Iainfix <V6V5Aainfix <=c0V6FAainfix <=c0V5Iainfix =V5ainfix +V2agetV1V2FAainfix <V2V0Aainfix <=c0V2ainfix <ainfix -V0V7ainfix -V0V2Aainfix <=c0ainfix -V0V2Aainfix =agetV1V8c0NIainfix <V8V0Iainfix <V8V7Aainfix <=c0V8FAainfix <=c0V7Iainfix =V7ainfix +V2c1FAainfix <V2V0Aainfix <=c0V2Aainfix <V2V0Aainfix <=c0V2ainfix =agetV1V9c0NIainfix <V9aprefix -c1Aainfix <=c0V9FAainfix =agetV1aprefix -c1c0Aainfix <aprefix -c1V0Aainfix <=c0aprefix -c1Oainfix =agetV1V10c0NIainfix <V10V0Aainfix <=c0V10FAainfix =aprefix -c1aprefix -c1Iainfix =agetV1V11c0NIainfix <V11V0Iainfix <V11V2Aainfix <=c0V11FAainfix <=c0V2FAainfix =agetV1V12c0NIainfix <V12V0Iainfix <V12c0Aainfix <=c0V12FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
...@@ -74,7 +74,7 @@ ...@@ -74,7 +74,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="loop invariant init" expl="loop invariant init"
sum="229e741d6a04e810f151948d11a9913a" sum="8a77b342994cdee6d6b433924d7ccd9e"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF"> shape="ainfix =agetV1V2c0NIainfix <V2V0Iainfix <V2c0Aainfix <=c0V2FAainfix <=c0c0Iadecrease1amk arrayV0V1FF">
...@@ -108,7 +108,7 @@ ...@@ -108,7 +108,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="precondition" expl="precondition"
sum="d9637785255666d718b6d41e0c20c3a7" sum="b3bc505747f92be9cf67ab6650c941b5"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -142,7 +142,7 @@ ...@@ -142,7 +142,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="normal postcondition" expl="normal postcondition"
sum="45ba1432c8fa59623a113ebde9768be7" sum="f8de58a58ec3dc331e05f722abdd9e5f"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix =agetV1V3c0NIainfix <V3V2Aainfix <=c0V3FAainfix =agetV1V2c0Aainfix <V2V0Aainfix <=c0V2Oainfix =agetV1V4c0NIainfix <V4V0Aainfix <=c0V4FAainfix =V2aprefix -c1Iainfix =agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -176,7 +176,7 @@ ...@@ -176,7 +176,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="precondition" expl="precondition"
sum="b7b57323c0f68bfde0aec3fd12975221" sum="9c84addb584c0cb2c7ca597445e8128b"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -210,7 +210,7 @@ ...@@ -210,7 +210,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="precondition" expl="precondition"
sum="b33ec8f71fafc258f3c6289f0e2e51f1" sum="a156dd2f60e96f4cd2bebf2214888c11"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V3c0NIainfix <V3V0Iainfix <V3V2Aainfix <=c0V3FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -244,7 +244,7 @@ ...@@ -244,7 +244,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="loop invariant preservation" expl="loop invariant preservation"
sum="1f7a7f98dd7824bd83ec31755d352c2f" sum="3493e2078ee1d58972d0d4548296285e"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -260,7 +260,7 @@ ...@@ -260,7 +260,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="parameter search" expl="parameter search"
sum="14718f6dd8f059fc81e67ff2c3918e0d" sum="69d48b498e9787d69037810f0ef088a8"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V2Aainfix <=c0V4FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V2Aainfix <=c0V4FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -308,7 +308,7 @@ ...@@ -308,7 +308,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="parameter search" expl="parameter search"
sum="2216c6145d760ab315956294b9e74041" sum="8afbfddf9caa1618af955cc06c8dfa79"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FIainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FIainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -330,7 +330,7 @@ ...@@ -330,7 +330,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="loop variant decreases" expl="loop variant decreases"
sum="5904617529f1a62b64786640b085f507" sum="c51f0c7769364b23739e6fdbe8acfaa3"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix <ainfix -V0V3ainfix -V0V2Aainfix <=c0ainfix -V0V2Iainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2agetV1V2FIainfix <V2V0Aainfix <=c0V2Iainfix >agetV1V2c0Iainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -364,7 +364,7 @@ ...@@ -364,7 +364,7 @@
locfile="programs/decrease1/../decrease1.mlw" locfile="programs/decrease1/../decrease1.mlw"
loclnum="23" loccnumb="6" loccnume="12" loclnum="23" loccnumb="6" loccnume="12"
expl="loop invariant preservation" expl="loop invariant preservation"
sum="31cc04f25872159425cbc8c7edbb8a74" sum="bd516d3d3e46f318b1fd5ddeb5fb5402"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF"> shape="ainfix =agetV1V4c0NIainfix <V4V0Iainfix <V4V3Aainfix <=c0V4FAainfix <=c0V3Iainfix =V3ainfix +V2c1FIainfix >agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix =agetV1V2c0NIainfix <V2V0Aainfix <=c0V2Iainfix <V2V0Iainfix =agetV1V5c0NIainfix <V5V0Iainfix <V5V2Aainfix <=c0V5FAainfix <=c0V2FIadecrease1amk arrayV0V1FF">
...@@ -383,7 +383,7 @@ ...@@ -383,7 +383,7 @@
timelimit="10" timelimit="10"
obsolete="false" obsolete="false"
archived="false">