list.RevAppend exported in list.ListRich

parent 22a41280
...@@ -14,13 +14,13 @@ ...@@ -14,13 +14,13 @@
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="9" loccnumb="7" loccnume="21" loclnum="9" loccnumb="7" loccnume="21"
verified="true" verified="true"
expanded="true"> expanded="false">
<goal <goal
name="WP_parameter empty" name="WP_parameter empty"
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="21" loccnumb="6" loccnume="11" loclnum="21" loccnumb="6" loccnume="11"
expl="VC for empty" expl="VC for empty"
sum="8d4f555fd4a663723217f745b47ac262" sum="cfcee1a68a863ac6f33e18a5da6055fd"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =ainfix ++aNilareverseaNilaNilAainfix =alengthaNilc0Aainfix &gt;=c0alengthaNilAainfix =alengthaNilc0"> shape="ainfix =ainfix ++aNilareverseaNilaNilAainfix =alengthaNilc0Aainfix &gt;=c0alengthaNilAainfix =alengthaNilc0">
...@@ -39,11 +39,11 @@ ...@@ -39,11 +39,11 @@
name="WP_parameter head" name="WP_parameter head"
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="24" loccnumb="6" loccnume="10" loclnum="24" loccnumb="6" loccnume="10"
expl="unreachable point" expl="VC for head"
sum="713a72568da13755e82810a050290fa8" sum="91a3b23cd199d113c247dea656eb2aca"
proved="true" proved="true"
expanded="false" expanded="false"
shape="unreachable pointCfaNilCfaNilainfix =V4V5aConsVwainfix ++V0areverseV2aConsVwV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F"> shape="CfaNilCfaNilainfix =V4V5aConsVwainfix ++V0areverseV2aConsVwV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F">
<label <label
name="expl:VC for head"/> name="expl:VC for head"/>
<proof <proof
...@@ -60,7 +60,7 @@ ...@@ -60,7 +60,7 @@
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="32" loccnumb="6" loccnume="12" loclnum="32" loccnumb="6" loccnume="12"
expl="VC for create" expl="VC for create"
sum="4f448b9d9fb30dcd705811da5452b4a7" sum="ce7c4cd8b58bcbc84feb7eb5c123566c"
proved="true" proved="true"
expanded="false" expanded="false"
shape="iainfix =ainfix ++ainfix ++V0areverseV2areverseaNilainfix ++V0areverseV2Aainfix =alengthaNilc0Aainfix &gt;=ainfix +V1V3alengthaNilAainfix =alengthainfix ++V0areverseV2ainfix +V1V3ainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1ainfix &gt;=V1V3Iainfix =V3alengthV2Aainfix =V1alengthV0F"> shape="iainfix =ainfix ++ainfix ++V0areverseV2areverseaNilainfix ++V0areverseV2Aainfix =alengthaNilc0Aainfix &gt;=ainfix +V1V3alengthaNilAainfix =alengthainfix ++V0areverseV2ainfix +V1V3ainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1ainfix &gt;=V1V3Iainfix =V3alengthV2Aainfix =V1alengthV0F">
...@@ -80,7 +80,7 @@ ...@@ -80,7 +80,7 @@
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="41" loccnumb="6" loccnume="10" loclnum="41" loccnumb="6" loccnume="10"
expl="VC for tail" expl="VC for tail"
sum="670ad4e02fae8ac914dc725bf6d7d712" sum="58c273de1c7ad2b92ce76190f6853b83"
proved="true" proved="true"
expanded="false" expanded="false"
shape="CfaNilCfaNilainfix =ainfix ++V5areverseV7V9aConswVainfix ++V0areverseV2Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2Aainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4aConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F"> shape="CfaNilCfaNilainfix =ainfix ++V5areverseV7V9aConswVainfix ++V0areverseV2Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2Aainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4aConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F">
...@@ -89,13 +89,13 @@ ...@@ -89,13 +89,13 @@
<transf <transf
name="split_goal" name="split_goal"
proved="true" proved="true"
expanded="true"> expanded="false">
<goal <goal
name="WP_parameter tail.1" name="WP_parameter tail.1"
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="41" loccnumb="6" loccnume="10" loclnum="41" loccnumb="6" loccnume="10"
expl="1. unreachable point" expl="1. unreachable point"
sum="4c5cdcd7ca4965d0a0513fc8d518383f" sum="4399b8ef7dfaed7cb70dce233662273d"
proved="true" proved="true"
expanded="false" expanded="false"
shape="unreachable pointCfaNiltaConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F"> shape="unreachable pointCfaNiltaConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F">
...@@ -115,7 +115,7 @@ ...@@ -115,7 +115,7 @@
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="41" loccnumb="6" loccnume="10" loclnum="41" loccnumb="6" loccnume="10"
expl="2. precondition" expl="2. precondition"
sum="d34c553c1c01ec82fb187da4cb0fbebb" sum="de81eca023e9e6d1ffb8443593dfb8b2"
proved="true" proved="true"
expanded="false" expanded="false"
shape="preconditionCtaNilainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4aConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F"> shape="preconditionCtaNilainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4aConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F">
...@@ -135,7 +135,7 @@ ...@@ -135,7 +135,7 @@
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="41" loccnumb="6" loccnume="10" loclnum="41" loccnumb="6" loccnume="10"
expl="3. postcondition" expl="3. postcondition"
sum="ec20461ce141ba17adc677f84dbccce0" sum="3cdf608a4c646633a86e5db82692dcda"
proved="true" proved="true"
expanded="false" expanded="false"
shape="postconditionCtaNilCfaNilainfix =ainfix ++V5areverseV7V9aConswVainfix ++V0areverseV2Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2Aainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4aConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F"> shape="postconditionCtaNilCfaNilainfix =ainfix ++V5areverseV7V9aConswVainfix ++V0areverseV2Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2Aainfix =alengthV7V8Aainfix &gt;=V6alengthV7Aainfix =alengthV5V6FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4aConswVV0INainfix =ainfix ++V0areverseV2aNilAainfix =alengthV2V3Aainfix &gt;=V1alengthV2Aainfix =alengthV0V1F">
...@@ -157,7 +157,7 @@ ...@@ -157,7 +157,7 @@
locfile="../vstte10_aqueue.mlw" locfile="../vstte10_aqueue.mlw"
loclnum="49" loccnumb="6" loccnume="13" loclnum="49" loccnumb="6" loccnume="13"
expl="VC for enqueue" expl="VC for enqueue"
sum="2d12fa3ae5c5a402f1d856d285dd9da7" sum="d14f5de8feb6efa126f36ea6fe84bdbc"
proved="true" proved="true"
expanded="false" expanded="false"
shape="ainfix =ainfix ++V6areverseV8ainfix ++ainfix ++V1areverseV3aConsV0aNilIainfix =ainfix ++V6areverseV8ainfix ++V1areverseV5Aainfix =alengthV8V9Aainfix &gt;=V7alengthV8Aainfix =alengthV6V7FAainfix =ainfix +V4c1alengthV5Aainfix =V2alengthV1LaConsV0V3Iainfix =alengthV3V4Aainfix &gt;=V2alengthV3Aainfix =alengthV1V2F"> shape="ainfix =ainfix ++V6areverseV8ainfix ++ainfix ++V1areverseV3aConsV0aNilIainfix =ainfix ++V6areverseV8ainfix ++V1areverseV5Aainfix =alengthV8V9Aainfix &gt;=V7alengthV8Aainfix =alengthV6V7FAainfix =ainfix +V4c1alengthV5Aainfix =V2alengthV1LaConsV0V3Iainfix =alengthV3V4Aainfix &gt;=V2alengthV3Aainfix =alengthV1V2F">
......
...@@ -548,6 +548,7 @@ theory ListRich ...@@ -548,6 +548,7 @@ theory ListRich
use export NthHdTl use export NthHdTl
use export Append use export Append
use export Reverse use export Reverse
use export RevAppend
use export Sorted use export Sorted
use export NumOcc use export NumOcc
use export Permut use export Permut
......
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