Commit ab739e49 authored by Andrei Paskevich's avatar Andrei Paskevich

update sessions

parent fb4f4a25
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="foveoos2011/duplets/why3session.xml">
<prover
......@@ -36,10 +36,10 @@
locfile="foveoos2011/duplets/../duplets.mlw"
loclnum="43" loccnumb="6" loccnume="12"
expl="parameter duplet"
sum="be962a5577c9db0d565e6d563eba464e"
sum="62e462537298fecdf521150553ebd251"
proved="true"
expanded="true"
shape="Lamk arrayV0V2ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FNALagetV2V7iCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =aTuple2V18V19aTuple2V7V17Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2Aainfix &gt;c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0FFF">
shape="Lamk arrayV0V2ais_dupletV3V4V5NICV1aNonefaSomeVainfix =V6agetV2V4NIainfix &lt;V5V0Aainfix &lt;V4V5Aainfix &lt;V4ainfix +ainfix -V0c2c1Aainfix &lt;=c0V4FNALagetV2V7iCV1aNonefaSomeVainfix =V9V8ais_dupletV3V10V11NICV1aNonefaSomeVainfix =V12agetV2V10NIainfix &lt;V11V0Aainfix &lt;V10V11Aainfix &lt;V10ainfix +V7c1Aainfix &lt;=c0V10Fais_dupletV3V13V14NICV1aNonefaSomeVainfix =V15agetV2V13NIainfix &lt;V14V0Aainfix &lt;V13V14Aainfix &lt;V13ainfix +V7c1Aainfix &lt;=c0V13FIais_dupletV3V7V16NIainfix &lt;V16ainfix +ainfix -V0c1c1Aainfix &lt;V7V16FAiainfix =agetV2V17V8CV1aNonefaSomeVainfix =V20agetV2V18NAais_dupletV3V18V19Iainfix =V19V17Aainfix =V18V7Fais_dupletV3V7V21NIainfix &lt;V21ainfix +V17c1Aainfix &lt;V7V21FAainfix &lt;V17V0Aainfix &lt;=c0V17Iais_dupletV3V7V22NIainfix &lt;V22V17Aainfix &lt;V7V22FIainfix &lt;=V17ainfix -V0c1Aainfix &lt;=ainfix +V7c1V17FAais_dupletV3V7V23NIainfix &lt;V23ainfix +V7c1Aainfix &lt;V7V23FIainfix &lt;=ainfix +V7c1ainfix -V0c1Aais_dupletV3V24V25NICV1aNonefaSomeVainfix =V26agetV2V24NIainfix &lt;V25V0Aainfix &lt;V24V25Aainfix &lt;V24ainfix +V7c1Aainfix &lt;=c0V24FIainfix &gt;ainfix +V7c1ainfix -V0c1Aainfix &lt;V7V0Aainfix &lt;=c0V7Iais_dupletV3V27V28NICV1aNonefaSomeVainfix =V29agetV2V27NIainfix &lt;V28V0Aainfix &lt;V27V28Aainfix &lt;V27V7Aainfix &lt;=c0V27FIainfix &lt;=V7ainfix -V0c2Aainfix &lt;=c0V7FAais_dupletV3V30V31NICV1aNonefaSomeVainfix =V32agetV2V30NIainfix &lt;V31V0Aainfix &lt;V30V31Aainfix &lt;V30c0Aainfix &lt;=c0V30FIainfix &lt;=c0ainfix -V0c2Aainfix &gt;c0ainfix -V0c2NICV1aNonefaSomeVainfix =V35agetV2V33NAais_dupletV3V33V34EAainfix &lt;=c2V0FFF">
<label
name="expl:parameter duplet"/>
<proof
......@@ -48,7 +48,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.05"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="1"
......@@ -56,7 +56,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.05"/>
</proof>
</goal>
<goal
......@@ -76,7 +76,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
<proof
prover="1"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="add_list/why3session.xml">
name="programs/add_list/why3session.xml">
<prover
id="0"
name="Alt-Ergo"
......@@ -20,23 +20,23 @@
expanded="true">
<theory
name="SumList"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="2" loccnumb="7" loccnume="14"
verified="true"
expanded="false">
</theory>
<theory
name="WP AddListRec"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="29" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="33" loccnumb="8" loccnume="11"
expl="parameter sum"
sum="864122fc1850685da889e50a016bf139"
sum="e8f428f8ff2f8c4c809829b72ccf847b"
proved="true"
expanded="true"
shape="CV0aNilainfix =c0.0aadd_realV0Aainfix =c0aadd_intV0aConsVVCV1aIntegerVainfix =V4aadd_realV0Aainfix =ainfix +V5V3aadd_intV0aRealVainfix =ainfix +.V6V4aadd_realV0Aainfix =V3aadd_intV0Iainfix =V4aadd_realV2Aainfix =V3aadd_intV2FF">
......@@ -56,7 +56,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.00"/>
</proof>
<proof
prover="2"
......@@ -64,15 +64,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter main"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="46" loccnumb="4" loccnume="8"
expl="parameter main"
sum="70fc66f484fe4f2dacec8be731a0e282"
sum="840b6a07c4fa0fa9cbf47eb732cef621"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
......@@ -84,7 +84,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -92,22 +92,22 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
<theory
name="WP AddListImp"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="58" loccnumb="7" loccnume="17"
verified="true"
expanded="true">
<goal
name="WP_parameter sum"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="65" loccnumb="4" loccnume="7"
expl="parameter sum"
sum="8c2e6fba3d93a8246e6ea9886fb15437"
sum="a1e9fc3e91b972d21b1df21784b15a5f"
proved="true"
expanded="true"
shape="CV1aNilainfix =V2aadd_realV0Aainfix =V3aadd_intV0aConsaIntegerVVainfix =ainfix +.V2aadd_realV7aadd_realV0Aainfix =ainfix +V6aadd_intV7aadd_intV0Iainfix =V7V5FIainfix =V6ainfix +V3V4FaConsaRealVVainfix =ainfix +.V10aadd_realV11aadd_realV0Aainfix =ainfix +V3aadd_intV11aadd_intV0Iainfix =V11V9FIainfix =V10ainfix +.V2V8FIainfix =ainfix +.V2aadd_realV1aadd_realV0Aainfix =ainfix +V3aadd_intV1aadd_intV0FFFAainfix =ainfix +.c0.0aadd_realV0aadd_realV0Aainfix =ainfix +c0aadd_intV0aadd_intV0F">
......@@ -119,7 +119,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -127,15 +127,15 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
name="WP_parameter main"
locfile="add_list/../add_list.mlw"
locfile="programs/add_list/../add_list.mlw"
loclnum="89" loccnumb="4" loccnume="8"
expl="parameter main"
sum="319b8c9fa71c762cd764adb846386504"
sum="3325916e5f9c20203b1f3dc9799e7d53"
proved="true"
expanded="true"
shape="ainfix =V1c4.7Aainfix =V0c22Iainfix =V1aadd_realaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilAainfix =V0aadd_intaConsaIntegerc5aConsaRealc3.3aConsaIntegerc8aConsaRealc1.4aConsaIntegerc9aNilF">
......@@ -147,7 +147,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
<proof
prover="2"
......@@ -155,7 +155,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</theory>
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/max_matrix/why3session.xml">
<prover
......@@ -58,7 +58,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="6.06"/>
<result status="valid" time="4.89"/>
</proof>
</goal>
<goal
......@@ -260,7 +260,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.03"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -302,7 +302,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -352,7 +352,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.50"/>
<result status="valid" time="0.42"/>
</proof>
</goal>
</transf>
......@@ -376,7 +376,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -411,7 +411,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.46"/>
<result status="valid" time="0.41"/>
</proof>
</goal>
</transf>
......@@ -433,7 +433,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal
......@@ -453,7 +453,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.13"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
</transf>
......@@ -490,7 +490,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.03"/>
</proof>
</goal>
</transf>
......@@ -542,7 +542,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.14"/>
<result status="valid" time="0.13"/>
</proof>
</goal>
</transf>
......@@ -576,10 +576,10 @@
locfile="programs/max_matrix/../max_matrix.mlw"
loclnum="181" loccnumb="7" loccnume="11"
expl="parameter memo"
sum="a8c50c1fd2930336f2779e51c58e10ce"
sum="e3cabf56a2f7ad217c29043312c90853"
proved="true"
expanded="false"
shape="Lamk tV2LaTuple2V5V6ainvamk tV8AapostaTuple2V0V1V7ILaTuple2V9V10ainfix =agetV8V11agetV4V11Iainfix =V11aTuple2V0V1NFAainfix =agetV8aTuple2V0V1aSomeV7FIainvamk tV4AapostaTuple2V0V1V7FFAainvV3AapreaTuple2V0V1Aainfix &lt;ainfix -ainfix *c2anainfix *c2V0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Iainfix =agetV2aTuple2V0V1aNoneALaTuple2V12V13ainvV3AapostaTuple2V0V1V14Iainfix =agetV2aTuple2V0V1aSomeV14FIainvV3AapreaTuple2V0V1FFF">
shape="Lamk tV2LaTuple2V5V6ainvamk tV8AapostaTuple2V0V1V7ILaTuple2V9V10ainfix =agetV8V11agetV4V11Iainfix =V1V10Aainfix =V0V9NFAainfix =agetV8aTuple2V0V1aSomeV7FIainvamk tV4AapostaTuple2V0V1V7FFAainvV3AapreaTuple2V0V1Aainfix &lt;ainfix -ainfix *c2anainfix *c2V0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Iainfix =agetV2aTuple2V0V1aNoneALaTuple2V12V13ainvV3AapostaTuple2V0V1V14Iainfix =agetV2aTuple2V0V1aSomeV14FIainvV3AapreaTuple2V0V1FFF">
<label
name="expl:parameter memo"/>
<transf
......@@ -618,7 +618,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.00"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -638,7 +638,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.00"/>
</proof>
</goal>
</transf>
......@@ -660,7 +660,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal
......@@ -668,10 +668,10 @@
locfile="programs/max_matrix/../max_matrix.mlw"
loclnum="181" loccnumb="7" loccnume="11"
expl="normal postcondition"
sum="315f364c8de9507cfb1cc7bb8f53ba7e"
sum="00f771552f674482924cfd76b757f58f"
proved="true"
expanded="false"
shape="Lamk tV2LaTuple2V5V6ainvamk tV8AapostaTuple2V0V1V7ILaTuple2V9V10ainfix =agetV8V11agetV4V11Iainfix =V11aTuple2V0V1NFAainfix =agetV8aTuple2V0V1aSomeV7FIainvamk tV4AapostaTuple2V0V1V7FFIainvV3AapreaTuple2V0V1Aainfix &lt;ainfix -ainfix *c2anainfix *c2V0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Iainfix =agetV2aTuple2V0V1aNoneILaTuple2V12V13ainvV3AapostaTuple2V0V1V14Iainfix =agetV2aTuple2V0V1aSomeV14FIainvV3AapreaTuple2V0V1FFF">
shape="Lamk tV2LaTuple2V5V6ainvamk tV8AapostaTuple2V0V1V7ILaTuple2V9V10ainfix =agetV8V11agetV4V11Iainfix =V1V10Aainfix =V0V9NFAainfix =agetV8aTuple2V0V1aSomeV7FIainvamk tV4AapostaTuple2V0V1V7FFIainvV3AapreaTuple2V0V1Aainfix &lt;ainfix -ainfix *c2anainfix *c2V0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix -ainfix *c2anainfix *c2V0c1Iainfix =agetV2aTuple2V0V1aNoneILaTuple2V12V13ainvV3AapostaTuple2V0V1V14Iainfix =agetV2aTuple2V0V1aSomeV14FIainvV3AapreaTuple2V0V1FFF">
<label
name="expl:parameter memo"/>
<proof
......@@ -680,7 +680,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
</transf>
......@@ -732,7 +732,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.01"/>
</proof>
</goal>
</transf>
......@@ -923,7 +923,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -958,7 +958,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.11"/>
<result status="valid" time="0.10"/>
</proof>
</goal>
</transf>
......
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/andrei/prj/why-git/share/why3session.dtd">
<why3session
name="programs/vstte10_aqueue/why3session.xml">
<prover
......@@ -41,10 +41,10 @@
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="28" loccnumb="6" loccnume="10"
expl="parameter head"
sum="5916ef6a02b8590c0eaa0b9b05831a82"
sum="cbebae5e195b4dc416bc94a63ac89a2b"
proved="true"
expanded="false"
shape="CV0aNilfaConsVwainfix =Cainfix ++V0areverseV2aNilaNoneaConsVwaSomeV5aSomeV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNilfaConsVwCainfix ++V0areverseV2aNilfaConsVwainfix =V4V5Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
<label
name="expl:parameter head"/>
<proof
......@@ -53,7 +53,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
<result status="valid" time="0.12"/>
</proof>
</goal>
<goal
......@@ -73,7 +73,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.22"/>
<result status="valid" time="0.20"/>
</proof>
</goal>
<goal
......@@ -81,10 +81,10 @@
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="45" loccnumb="6" loccnume="10"
expl="parameter tail"
sum="87a45c9f0f21880bdfd308b156e1d7ea"
sum="74bbdd7fad01a67ecf6a0125c034bd37"
proved="true"
expanded="false"
shape="CV0aNilfaConswVLamk queueV5V6V7V8ainfix =Cainfix ++V0areverseV2aNilaNoneaConswVaSomeV10aSomeainfix ++V5areverseV7AainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2AainvV9FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNilfaConswVLamk queueV5V6V7V8Cainfix ++V0areverseV2aNilfaConswVainfix =ainfix ++V5areverseV7V10AainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2AainvV9FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
<label
name="expl:parameter tail"/>
<transf
......@@ -136,10 +136,10 @@
locfile="programs/vstte10_aqueue/../vstte10_aqueue.mlw"
loclnum="45" loccnumb="6" loccnume="10"
expl="parameter tail"
sum="dbcb916d4f7f9cd290fe34fd649677cb"
sum="38e87156f257039a78985e2a5eb9110b"
proved="true"
expanded="false"
shape="CV0aNiltaConswVLamk queueV5V6V7V8ainfix =Cainfix ++V0areverseV2aNilaNoneaConswVaSomeV10aSomeainfix ++V5areverseV7AainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2AainvV9FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
shape="CV0aNiltaConswVLamk queueV5V6V7V8Cainfix ++V0areverseV2aNilfaConswVainfix =ainfix ++V5areverseV7V10AainvV9Iainfix =ainfix ++V5areverseV7ainfix ++V4areverseV2AainvV9FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV4Iainfix =ainfix ++V0areverseV2aNilNAainvamk queueV0V1V2V3F">
<label
name="expl:parameter tail"/>
<proof
......@@ -148,7 +148,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.48"/>
<result status="valid" time="0.25"/>
</proof>
</goal>
</transf>
......
......@@ -2,18 +2,27 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Require int.Int.
Parameter mark : Type.
(* Why3 assumption *)
Definition unit := unit.
Parameter at1: forall (a:Type), a -> mark -> a.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
......@@ -22,11 +31,12 @@ Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| Cons _ r => (1%Z + (length r))%Z
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
......@@ -34,8 +44,9 @@ Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil:(list a))).
((length l) = 0%Z) <-> (l = (Nil :(list a))).
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
......@@ -45,56 +56,70 @@ Unset Contextual Implicit.
Implicit Arguments Some.
Parameter nth: forall (a:Type), Z -> (list a) -> (option a).
Implicit Arguments nth.
Axiom nth_def : forall (a:Type), forall (n:Z) (l:(list a)),
match l with
| Nil => ((nth n l) = (None:(option a)))
| Cons x r => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
| Nil => ((nth n l) = (None :(option a)))
| (Cons x r) => ((n = 0%Z) -> ((nth n l) = (Some x))) /\ ((~ (n = 0%Z)) ->
((nth n l) = (nth (n - 1%Z)%Z r)))
end.
(* Why3 assumption *)
Definition zero_at(l:(list Z)) (i:Z): Prop := ((nth i l) = (Some 0%Z)) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z)).
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Definition no_zero(l:(list Z)): Prop := forall (j:Z), ((0%Z <= j)%Z /\
(j < (length l))%Z) -> ~ ((nth j l) = (Some 0%Z)).
(j < (length l))%Z) -> ~ ((nth j l) = (Some 0%Z)).
(* Why3 assumption *)
Inductive ref (a:Type) :=
| mk_ref : a -> ref a.
Implicit Arguments mk_ref.
Definition contents (a:Type)(u:(ref a)): a :=
match u with
| mk_ref contents1 => contents1
(* Why3 assumption *)
Definition contents (a:Type)(v:(ref a)): a :=
match v with
| (mk_ref x) => x
end.
Implicit Arguments contents.
(* Why3 assumption *)
Definition hd (a:Type)(l:(list a)): (option a) :=
match l with
| Nil => (None:(option a))
| Cons h _ => (Some h)
| Nil => (None :(option a))
| (Cons h _) => (Some h)
end.
Implicit Arguments hd.
(* Why3 assumption *)
Definition tl (a:Type)(l:(list a)): (option (list a)) :=
match l with
| Nil => (None:(option (list a)))
| Cons _ t => (Some t)
| Nil => (None :(option (list a)))
| (Cons _ t) => (Some t)
end.
Implicit Arguments tl.
(* YOU MAY EDIT THE CONTEXT BELOW *)
(* DO NOT EDIT BELOW *)
Theorem WP_parameter_search_loop : True.
(* Why3 goal *)
Theorem WP_parameter_search_loop : forall (l:(list Z)), forall (s:(list Z)),
forall (i:Z), ((0%Z <= i)%Z /\ (((i + (length s))%Z = (length l)) /\
((forall (j:Z), (0%Z <= j)%Z -> ((nth j s) = (nth (i + j)%Z l))) /\
forall (j:Z), ((0%Z <= j)%Z /\ (j < i)%Z) -> ~ ((nth j
l) = (Some 0%Z))))) -> ((~ (s = (Nil :(list Z)))) -> ((~ (s = (Nil :(list
Z)))) -> forall (result:Z),
match s with
| Nil => False
| (Cons h _) => (result = h)
end -> ((result = 0%Z) -> ((((0%Z <= i)%Z /\ (i < (length l))%Z) /\
(zero_at l i)) \/ ((i = (length l)) /\ (no_zero l)))))).
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.
destruct s.
discriminate H4.
injection H4; intros; subst; clear H4.
destruct H4.
subst; subst.
clear H0 H1.
left.
split.
......@@ -110,6 +135,5 @@ intuition.
rewrite H4 in H1.
auto.
Qed.
(* DO NOT EDIT BELOW *)
......@@ -2,18 +2,27 @@
(* Beware! Only edit allowed sections below *)
Require Import ZArith.
Require Import Rbase.
Definition unit := unit.
Require int.Int.
Parameter mark : Type.
(* Why3 assumption *)
Definition unit := unit.
Parameter at1: forall (a:Type), a -> mark -> a.
Parameter qtmark : Type.
Parameter at1: forall (a:Type), a -> qtmark -> a.
Implicit Arguments at1.
Parameter old: forall (a:Type), a -> a.
Parameter old: forall (a:Type), a -> a.
Implicit Arguments old.
(* Why3 assumption *)
Definition implb(x:bool) (y:bool): bool := match (x,
y) with
| (true, false) => false
| (_, _) => true
end.
(* Why3 assumption *)
Inductive list (a:Type) :=
| Nil : list a
| Cons : a -> (list a) -> list a.
......@@ -22,11 +31,12 @@ Implicit Arguments Nil.
Unset Contextual Implicit.
Implicit Arguments Cons.
(* Why3 assumption *)
Set Implicit Arguments.
Fixpoint length (a:Type)(l:(list a)) {struct l}: Z :=
match l with
| Nil => 0%Z
| Cons _ r => (1%Z + (length r))%Z
| Nil => 0%Z
| (Cons _ r) => (1%Z + (length r))%Z
end.
Unset Implicit Arguments.
......@@ -34,8 +44,9 @@ Axiom Length_nonnegative : forall (a:Type), forall (l:(list a)),
(0%Z <= (length l))%Z.
Axiom Length_nil : forall (a:Type), forall (l:(list a)),
((length l) = 0%Z) <-> (l = (Nil:(list a))).
((length l) = 0%Z) <-> (l = (Nil :(list a))).
(* Why3 assumption *)
Inductive option (a:Type) :=
| None : option a
| Some : a -> option a.
......@@ -44,78 +55,83 @@ Implicit Arguments None.
Unset Contextual Implicit.
Implicit