Commit a1c5709c authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

same fringe example: simpler termination argument

parent d9732c3c
......@@ -38,7 +38,7 @@ module SameFringe
(* the enum of a tree [t], prepended to a given enum [e] *)
let rec enum t e variant { length (elements t) }
let rec enum t e variant { t }
ensures { enum_elements result = elements t ++ enum_elements e }
= match t with
| Empty -> e
......
......@@ -24,10 +24,10 @@
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
expl="VC for enum"
sum="baafae9ecfd9b0dab57698949053c88f"
sum="1a8be7972b22f1230da0b2838f3e739c"
proved="true"
expanded="true"
shape="CV0aEmptyainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aNodeVVVainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FAainfix <alengthaelementsV2alengthaelementsV0Aainfix <=c0alengthaelementsV0F">
shape="Cainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aEmptyainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FACfaEmptyainfix =V7V2Oainfix =V6V2aNodeVwVV0aNodeVVVV0F">
<label
name="expl:VC for enum"/>
<transf
......@@ -42,7 +42,7 @@
sum="beb2f0007d1c94eff394e1c707fe0604"
proved="true"
expanded="true"
shape="CV0aEmptyainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aNodeVVVtF">
shape="postconditionCainfix =aenum_elementsV1ainfix ++aelementsV0aenum_elementsV1aEmptytaNodeVVVV0F">
<label
name="expl:VC for enum"/>
<proof
......@@ -59,10 +59,10 @@
locfile="../same_fringe.mlw"
loclnum="41" loccnumb="10" loccnume="14"
expl="2. variant decrease"
sum="f6bc551b65e6d386fe8abeb3cf1abc41"
sum="02b6e4c6c7ee0c7cd5d7e4f8f06d0229"
proved="true"
expanded="true"
shape="CV0aEmptytaNodeVVVainfix &lt;alengthaelementsV2alengthaelementsV0Aainfix &lt;=c0alengthaelementsV0F">
shape="variant decreaseCtaEmptyCfaEmptyainfix =V6V2Oainfix =V5V2aNodeVwVV0aNodeVVVV0F">
<label
name="expl:VC for enum"/>
<proof
......@@ -82,7 +82,7 @@
sum="1b239bd1fbbbf378fce0d04f1b444a27"
proved="true"
expanded="true"
shape="CV0aEmptytaNodeVVVainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FF">
shape="postconditionCtaEmptyainfix =aenum_elementsV5ainfix ++aelementsV0aenum_elementsV1Iainfix =aenum_elementsV5ainfix ++aelementsV2aenum_elementsaNextV3V4V1FaNodeVVVV0F">
<label
name="expl:VC for enum"/>
<proof
......@@ -104,7 +104,7 @@
sum="ec562dea41cb51c7a73addc6ea779761"
proved="true"
expanded="true"
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">
shape="CCiNainfix =aenum_elementsV0aenum_elementsV1ainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFAainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4Fainfix =V5V2aNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
<transf
......@@ -119,7 +119,7 @@
sum="6e39f74ab276bf4e82c48ce96319d1c3"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2wtaDonetF">
shape="variant decreaseCCainfix &lt;alengthaenum_elementsV9alengthaenum_elementsV0Aainfix &lt;=c0alengthaenum_elementsV0Iainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -147,7 +147,7 @@
sum="0ca3e70f3dd4a563e25dfe755e04e7f6"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFIainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2wtaDonetF">
shape="postconditionCCainfix =aenum_elementsV0aenum_elementsV1qainfix =V10aTrueIainfix =aenum_elementsV9aenum_elementsV8qainfix =V10aTrueFIainfix =aenum_elementsV9ainfix ++aelementsV6aenum_elementsV7FIainfix =aenum_elementsV8ainfix ++aelementsV3aenum_elementsV4FIainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -167,7 +167,7 @@
sum="2e2fdc6f60e4b1dc04dddb458957bfc4"
proved="true"
expanded="false"
shape="CV1aNextVVVCV0aNextVVVainfix =aenum_elementsV0aenum_elementsV1NIainfix =V5V2NwtaDonetF">
shape="postconditionCCNainfix =aenum_elementsV0aenum_elementsV1INainfix =V5V2aNextVVVtwV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -187,7 +187,7 @@
sum="f928c51aa703ee5accb2189f529d32d2"
proved="true"
expanded="true"
shape="CV1aNextVVVCV0aNextVVVtwainfix =aenum_elementsV0aenum_elementsV1NaDonetF">
shape="postconditionCCtaNextVVVNainfix =aenum_elementsV0aenum_elementsV1wV0aNextVVVtaDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -207,7 +207,7 @@
sum="9625235d246c1c6acb7ee6635ea3f868"
proved="true"
expanded="true"
shape="CV1aNextVVVtaDoneCV0aDoneainfix =aenum_elementsV0aenum_elementsV1wtF">
shape="postconditionCtaNextVVVCainfix =aenum_elementsV0aenum_elementsV1aDonetwV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......@@ -227,7 +227,7 @@
sum="63d7a3c44e709bf4fa95f03d644d80aa"
proved="true"
expanded="true"
shape="CV1aNextVVVtaDoneCV0aDonetwainfix =aenum_elementsV0aenum_elementsV1NF">
shape="postconditionCtaNextVVVCtaDoneNainfix =aenum_elementsV0aenum_elementsV1wV0aDoneV1F">
<label
name="expl:VC for eq_enum"/>
<proof
......
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