Commit 41363e32 authored by Andrei Paskevich's avatar Andrei Paskevich

update sessions

parent 401e4625
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="bts/fsetint/why3session.xml" shape_version="2">
name="examples/bts/fsetint/why3session.xml" shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -32,36 +32,36 @@
expanded="true">
<theory
name="Th1"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="2" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="l_false"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="5" loccnumb="9" loccnume="16"
sum="d7f2aebfd2edd578b1a93cf604aec178"
sum="c947d53d28f83e6855846af79dd2fd23"
proved="false"
expanded="true"
shape="f">
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -69,7 +69,7 @@
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -77,7 +77,7 @@
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -96,20 +96,20 @@
</theory>
<theory
name="Th2"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="9" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="mem_integer"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="13" loccnumb="8" loccnume="19"
sum="242bf143cc8b33512505c233039239e5"
sum="7955f9947fe99d987021ad54e5134999"
proved="false"
expanded="true"
shape="amemV0aintegerF">
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -117,7 +117,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -125,28 +125,28 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
<result status="timeout" time="3.02"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.02"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
......@@ -159,14 +159,14 @@
</goal>
<goal
name="foo"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="15" loccnumb="7" loccnume="10"
sum="80ba20b39cf0e3e682e5c0d84d596f36"
sum="1b9f1948f208c84cec8e9d3afbc69215"
proved="false"
expanded="true"
shape="f">
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -174,7 +174,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -182,7 +182,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -190,20 +190,20 @@
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.01"/>
<result status="timeout" time="3.11"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="3.11"/>
<result status="timeout" time="3.01"/>
</proof>
<proof
prover="5"
......@@ -217,20 +217,20 @@
</theory>
<theory
name="Th3"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="20" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<goal
name="foo"
locfile="bts/fsetint/../fsetint.why"
locfile="examples/bts/fsetint/../fsetint.why"
loclnum="30" loccnumb="7" loccnume="10"
sum="ee9eb17e39034c473cffb6f065106935"
proved="false"
expanded="true"
shape="f">
<proof
prover="1"
prover="0"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -238,7 +238,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -246,7 +246,7 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="3"
prover="2"
timelimit="3"
memlimit="1000"
obsolete="false"
......@@ -254,20 +254,20 @@
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="4"
prover="3"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="2"
prover="4"
timelimit="3"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="5"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="foveoos2011/tree_max/why3session.xml" shape_version="2">
<prover
......@@ -50,10 +50,10 @@
locfile="foveoos2011/tree_max/../tree_max.mlw"
loclnum="58" loccnumb="10" loccnume="17"
expl="parameter max_aux"
sum="9fc59bad6ad8d5848304ed16ba8aba48"
sum="ff881f65aef0140a6dfc905eb5fda89a"
proved="true"
expanded="true"
shape="CV0aNullainfix &gt;=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix &gt;=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V3FIamemV5V4Oainfix =V5amaxV2V1Aainfix &gt;=V5amaxV2V1Aage_treeV5V4FF">
shape="CV0aNullainfix &gt;=V1V1Aage_treeV1V0aTreeVVVamemV6V0Oainfix =V6V1Aainfix &gt;=V6V1Aage_treeV6V0IamemV6V3Oainfix =V6V5Aainfix &gt;=V6V5Aage_treeV6V3FACV0aNullfaTreewVVainfix =V8V3Oainfix =V7V3IamemV5V4Oainfix =V5amaxV2V1Aainfix &gt;=V5amaxV2V1Aage_treeV5V4FACV0aNullfaTreewVVainfix =V10V4Oainfix =V9V4F">
<label
name="expl:parameter max_aux"/>
<proof
......@@ -68,8 +68,8 @@
<goal
name="WP_parameter max"
locfile="foveoos2011/tree_max/../tree_max.mlw"
loclnum="68" loccnumb="6" loccnume="9"
expl="parameter max"
loclnum="67" loccnumb="6" loccnume="9"
expl="postcondition"
sum="28e5d856901e66fadb02844681ad3b11"
proved="true"
expanded="true"
......
This diff is collapsed.
......@@ -28,11 +28,11 @@
name="WP_parameter insert"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="normal postcondition"
sum="50d27999e9260510364622fcfe7de7bc"
expl="parameter insert"
sum="8c949dfa217f9bcbbeab182e92a6bbe4"
proved="true"
expanded="true"
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix &lt;=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3Aainfix &lt;alengthV3alengthV1Aainfix &lt;=c0alengthV1IasortedV1F">
shape="CV1aNilapermutaConsV0V1aConsV0aNilAasortedaConsV0aNilaConsVViainfix &lt;=V0V2apermutaConsV0V1aConsV0V1AasortedaConsV0V1apermutaConsV0V1aConsV2V4AasortedaConsV2V4IapermutaConsV0V3V4AasortedV4FAasortedV3ACV1aNilfaConswVainfix =V5V3IasortedV1F">
<label
name="expl:parameter insert"/>
<transf
......@@ -43,7 +43,7 @@
name="WP_parameter insert.1"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="normal postcondition"
expl="postcondition"
sum="3c3f20287b2598f197dffcab0c1b4e01"
proved="true"
expanded="true"
......@@ -63,7 +63,7 @@
name="WP_parameter insert.2"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="normal postcondition"
expl="postcondition"
sum="bef425ce04e590572c7731091c1e1f5a"
proved="true"
expanded="true"
......@@ -83,11 +83,11 @@
name="WP_parameter insert.3"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="variant decreases"
sum="305f79d325fe748a40f4ef3ca8fe537b"
expl="variant decrease"
sum="07c671597521e1e3e21b3cfacd432576"
proved="true"
expanded="true"
shape="CV1aNiltaConsVVainfix &lt;alengthV3alengthV1Aainfix &lt;=c0alengthV1Iainfix &lt;=V0V2NIasortedV1F">
shape="CV1aNiltaConsVVCV1aNilfaConswVainfix =V4V3Iainfix &lt;=V0V2NIasortedV1F">
<label
name="expl:parameter insert"/>
<proof
......@@ -131,7 +131,7 @@
name="WP_parameter insert.5"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="11" loccnumb="10" loccnume="16"
expl="normal postcondition"
expl="postcondition"
sum="bfe71c11e2fd453b82fffaa40b2f8661"
proved="true"
expanded="true"
......@@ -153,11 +153,11 @@
name="WP_parameter insertion_sort"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="normal postcondition"
sum="91e7a417bbda5e6e7a25fbb0ce7c9d75"
expl="parameter insertion_sort"
sum="d8acc8a2d5e27f9daac8d71bd50a82bc"
proved="true"
expanded="true"
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FAainfix &lt;alengthV2alengthV0Aainfix &lt;=c0alengthV0F">
shape="CV0aNilapermutV0aNilAasortedaNilaConsVVapermutV0V4AasortedV4IapermutaConsV1V3V4AasortedV4FAasortedV3IapermutV2V3AasortedV3FACV0aNilfaConswVainfix =V5V2F">
<label
name="expl:parameter insertion_sort"/>
<transf
......@@ -168,7 +168,7 @@
name="WP_parameter insertion_sort.1"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="normal postcondition"
expl="postcondition"
sum="10fffeed3eae8b2ec39b461fcad338e3"
proved="true"
expanded="true"
......@@ -188,28 +188,28 @@
name="WP_parameter insertion_sort.2"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="variant decreases"
sum="585ace7cdfac142a9315ac496ca56dcd"
expl="variant decrease"
sum="be1acf2d059d38b4f026fcf1e9e940ef"
proved="true"
expanded="true"
shape="CV0aNiltaConsVVainfix &lt;alengthV2alengthV0Aainfix &lt;=c0alengthV0F">
shape="CV0aNiltaConsVVCV0aNilfaConswVainfix =V3V2F">
<label
name="expl:parameter insertion_sort"/>
<proof
prover="1"
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -224,7 +224,7 @@
<label
name="expl:parameter insertion_sort"/>
<proof
prover="1"
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -232,7 +232,7 @@
<result status="valid" time="0.01"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
......@@ -244,7 +244,7 @@
name="WP_parameter insertion_sort.4"
locfile="programs/insertion_sort_list/../insertion_sort_list.mlw"
loclnum="19" loccnumb="10" loccnume="24"
expl="normal postcondition"
expl="postcondition"
sum="51cc212a15945c2aec5b681db1cbf378"
proved="true"
expanded="true"
......@@ -252,20 +252,20 @@
<label
name="expl:parameter insertion_sort"/>
<proof
prover="1"
prover="0"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.07"/>
<result status="valid" time="0.10"/>
</proof>
<proof
prover="0"
prover="1"
timelimit="10"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.10"/>
<result status="valid" time="0.07"/>
</proof>
</goal>
</transf>
......
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
This diff is collapsed.
......@@ -175,6 +175,7 @@ module Harness
let s = snapshot t in
let it = iterator s in
while hasNext it do
invariant { bst t.tree }
variant { length (elements it) }
let x = next it in
let _ = add t (x * 3) in
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/users/demons/melquion/src/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/vstte10_aqueue/why3session.xml" shape_version="2">
<prover
......@@ -19,12 +19,12 @@
<goal
name="WP_parameter empty"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="23" loccnumb="6" loccnume="11"
expl="normal postcondition"
sum="498d84262c30a9b2934c3bb7bcc44d5a"
loclnum="21" loccnumb="6" loccnume="11"
expl="parameter empty"
sum="e7190a3f05a3e5728d5182b6f3ff1850"
proved="true"
expanded="false"
shape="ainfix =ainfix ++aNilareverseaNilaNilAainvamk queueaNilc0aNilc0">
shape="ainfix =alengthV0c0Aainfix &gt;=c0alengthV0Aainfix =alengthaNilc0LaNilAainfix =ainfix ++aNilareverseaNilaNil">
<label
name="expl:parameter empty"/>
<proof
......@@ -39,12 +39,12 @@
<goal
name="WP_parameter head"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="28" loccnumb="6" loccnume="10"
expl="parameter head"
sum="64983e0baac48d883c036004ba40e21e"
loclnum="24" loccnumb="6" loccnume="10"
expl="postcondition"
sum="731d618ab885e13a385f070505c96178"
proved="true"
expanded="false"
shape="CV0aNilfaConsVwCainfix ++V0areverseV2aNilfaConsVwainfix =V4V5Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNilfaConsVwCainfix ++V0areverseV2aNilfaConsVwainfix =V4V5Iainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1Aainfix =ainfix ++V0areverseV2aNilNF">
<label
name="expl:parameter head"/>
<proof
......@@ -59,12 +59,12 @@
<goal
name="WP_parameter create"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="36" loccnumb="6" loccnume="12"
loclnum="32" loccnumb="6" loccnume="12"
expl="parameter create"
sum="a165a71d9f58b13dbc4acbd82b56df31"
sum="e4493530dbb94b33806eb2a0070fdeca"
proved="true"
expanded="false"
shape="iainfix &gt;=V1V3ainfix =ainfix ++V0areverseV2ainfix ++V0areverseV2Aainvamk queueV0V1V2V3ainfix =ainfix ++ainfix ++V0areverseV2areverseaNilainfix ++V0areverseV2Aainvamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0Iainfix =V3alengthV2Aainfix =V1alengthV0F">
shape="iainfix &gt;=V1V3ainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1Aainfix =ainfix ++V0areverseV2ainfix ++V0areverseV2ainfix =alengthV5c0Aainfix &gt;=V4alengthV5Aainfix =alengthainfix ++V0areverseV2V4LaNilLainfix +V1V3Aainfix =ainfix ++ainfix ++V0areverseV2areverseaNilainfix ++V0areverseV2Iainfix =V3alengthV2Aainfix =V1alengthV0F">
<label
name="expl:parameter create"/>
<proof
......@@ -73,18 +73,18 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
<result status="valid" time="0.06"/>
</proof>
</goal>
<goal
name="WP_parameter tail"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="45" loccnumb="6" loccnume="10"
loclnum="41" loccnumb="6" loccnume="10"
expl="parameter tail"
sum="f3431d96040089e759a45554b314a269"
sum="a6440f8070a3a8534544700cdd6e4204"
proved="true"
expanded="false"
shape="CV0aNilfaConswVCainfix ++V0areverseV2aNilfaConswVainfix =ainfix ++V5areverseV7V10AainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2AainvV9Lamk queueV5V6V7V8FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNilfaConswVCainfix ++V0areverseV2aNilfaConswVainfix =ainfix ++V5areverseV7V9Iainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6Aainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1Aainfix =ainfix ++V0areverseV2aNilNF">
<label
name="expl:parameter tail"/>
<transf
......@@ -94,12 +94,12 @@
<goal
name="WP_parameter tail.1"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="45" loccnumb="6" loccnume="10"
loclnum="41" loccnumb="6" loccnume="10"
expl="parameter tail"
sum="4888cb9fe8cfdc43be348ddd8f842f70"
sum="010e43c61197c54d2ae7e9eaaeebe781"
proved="true"
expanded="false"
shape="CV0aNilfaConswVtIainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNilfaConswVtIainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1Aainfix =ainfix ++V0areverseV2aNilNF">
<label
name="expl:parameter tail"/>
<proof
......@@ -114,12 +114,12 @@
<goal
name="WP_parameter tail.2"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="45" loccnumb="6" loccnume="10"
expl="parameter tail"
sum="68931e7ee369bfa166975119600e3b21"
loclnum="41" loccnumb="6" loccnume="10"
expl="precondition"
sum="a193f4ad19553331fdb67d308fbb399e"
proved="true"
expanded="false"
shape="CV0aNiltaConswVainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNiltaConswVainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1Aainfix =ainfix ++V0areverseV2aNilNF">
<label
name="expl:parameter tail"/>
<proof
......@@ -134,12 +134,12 @@
<goal
name="WP_parameter tail.3"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="45" loccnumb="6" loccnume="10"
expl="parameter tail"
sum="e3cd38003adee97315e3cf49b49723ab"
loclnum="41" loccnumb="6" loccnume="10"
expl="postcondition"
sum="f1c01d477137a0eeb89dd49b58ab0d01"
proved="true"
expanded="false"
shape="CV0aNiltaConswVCainfix ++V0areverseV2aNilfaConswVainfix =ainfix ++V5areverseV7V10AainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2AainvV9Lamk queueV5V6V7V8FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNiltaConswVCainfix ++V0areverseV2aNilfaConswVainfix =ainfix ++V5areverseV7V9Iainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6Aainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1Aainfix =ainfix ++V0areverseV2aNilNF">
<label
name="expl:parameter tail"/>
<proof
......@@ -148,7 +148,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.26"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
</transf>
......@@ -156,12 +156,12 @@
<goal
name="WP_parameter enqueue"
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="53" loccnumb="6" loccnume="13"
loclnum="49" loccnumb="6" loccnume="13"
expl="parameter enqueue"
sum="75784486f186bfc210e481f8526ecff3"
sum="a5041cec8b908b9416f27b032df60668"
proved="true"
expanded="false"
shape="ainfix =ainfix ++V5areverseV7ainfix ++ainfix ++V1areverseV3aConsV0aNilAainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V1areverseaConsV0V3AainvV9Lamk queueV5V6V7V8FAainfix =ainfix +V4c1alengthaConsV0V3Aainfix =V2alengthV1Iainvamk queueV1V2V3V4F">
shape="ainfix =ainfix ++V5areverseV7ainfix ++ainfix ++V1areverseV3aConsV0aNilIainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6Aainfix =ainfix ++V5areverseV7ainfix ++V1areverseaConsV0V3FAainfix =ainfix +V4c1alengthaConsV0V3Aainfix =V2alengthV1Iainfix =alengthV3V4Aainfix &gt;=V2alengthV3Aainfix =alengthV1V2F">
<label
name="expl:parameter enqueue"/>
<proof
......
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Require Import BuiltIn.
Require BuiltIn.
(* Why3 assumption *)
Definition unit := unit.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a