Skip to content

GitLab

Commit 8051c0eb authored by MARCHE Claude's avatar MARCHE Claude
Browse files

updated proof sessions

parent 7b11724d
Hide whitespace changes
Inline Side-by-side
examples/programs/power/why3session.xml
View file @ 8051c0eb
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/power/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../power.mlw" verified="true" expanded="true">
<theory name="Power" verified="true" expanded="true">
<goal name="Power_1" sum="35b3c1cecd4cc836e84c041c8c553841" proved="true" expanded="true" shape="ainfix =apowerV0c1V0F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<why3session
name="programs/power/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../power.mlw"
verified="true"
expanded="true">
<theory
name="Power"
verified="true"
expanded="true">
<goal
name="Power_1"
sum="35b3c1cecd4cc836e84c041c8c553841"
proved="true"
expanded="true"
shape="ainfix =apowerV0c1V0F">
<proof
prover="cvc3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<proof
prover="z3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="Power_sum" sum="1ea1f98419e27d558db9442efa814db5" proved="true" expanded="true" shape="ainfix =apowerV0ainfix +V1V2ainfix *apowerV0V1apowerV0V2Iainfix <=c0V2Iainfix <=c0V1F">
<proof prover="coq" timelimit="2" edited="power_Power_Power_sum_1.v" obsolete="false">
<result status="valid" time="0.68"/>
<goal
name="Power_sum"
sum="1ea1f98419e27d558db9442efa814db5"
proved="true"
expanded="true"
shape="ainfix =apowerV0ainfix +V1V2ainfix *apowerV0V1apowerV0V2Iainfix <=c0V2Iainfix <=c0V1F">
<proof
prover="coq"
timelimit="2"
edited="power_Power_Power_sum_1.v"
obsolete="false">
<result status="valid" time="0.53"/>
</proof>
</goal>
<goal name="Power_mult" sum="a4251b66eb0d3675f94cbb81ae01186b" proved="true" expanded="true" shape="ainfix =apowerV0ainfix *V1V2apowerapowerV0V1V2Iainfix <=c0V2Iainfix <=c0V1F">
<proof prover="coq" timelimit="2" edited="power_Power_Power_mult_1.v" obsolete="false">
<result status="valid" time="0.81"/>
<goal
name="Power_mult"
sum="a4251b66eb0d3675f94cbb81ae01186b"
proved="true"
expanded="true"
shape="ainfix =apowerV0ainfix *V1V2apowerapowerV0V1V2Iainfix <=c0V2Iainfix <=c0V1F">
<proof
prover="coq"
timelimit="2"
edited="power_Power_Power_mult_1.v"
obsolete="false">
<result status="valid" time="0.55"/>
</proof>
</goal>
<goal name="Power_mult2" sum="bb045f291ad34df7ae867374d62c84e2" proved="true" expanded="true" shape="ainfix =apowerainfix *V0V1V2ainfix *apowerV0V2apowerV1V2Iainfix <=c0V2F">
<proof prover="coq" timelimit="5" edited="power_Power_Power_mult2_1.v" obsolete="false">
<result status="valid" time="0.70"/>
<goal
name="Power_mult2"
sum="bb045f291ad34df7ae867374d62c84e2"
proved="true"
expanded="true"
shape="ainfix =apowerainfix *V0V1V2ainfix *apowerV0V2apowerV1V2Iainfix <=c0V2F">
<proof
prover="coq"
timelimit="5"
edited="power_Power_Power_mult2_1.v"
obsolete="false">
<result status="valid" time="0.50"/>
</proof>
</goal>
</theory>
<theory name="WP M" verified="true" expanded="true">
<goal name="WP_parameter fast_exp" expl="parameter fast_exp" sum="f6e26076d5377c35b12cf996db10a73c" proved="true" expanded="true" shape="iainfix =V1c0ainfix =c1apowerV0V1LapowerV0adivV1c2ainfix =iainfix =iainfix =amodV1c2c0aTrueaFalseaTrueainfix *V2V2ainfix *ainfix *V2V2V0apowerV0V1Aainfix <=c0adivV1c2Aainfix <adivV1c2V1Aainfix <=c0V1Iainfix <=c0V1FF">
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="1.68"/>
<theory
name="WP M"
verified="true"
expanded="true">
<goal
name="WP_parameter fast_exp"
expl="parameter fast_exp"
sum="b636521503048b6a8c7a0f58662f09f5"
proved="true"
expanded="true"
shape="iainfix =V1c0ainfix =c1apowerV0V1LapowerV0adivV1c2ainfix =iainfix =amodV1c2c0ainfix *V2V2ainfix *ainfix *V2V2V0apowerV0V1Aainfix <=c0adivV1c2Aainfix <adivV1c2V1Aainfix <=c0V1Iainfix <=c0V1FF">
<proof
prover="alt-ergo"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="1.02"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative" expl="parameter fast_exp_imperative" sum="d3f84a4dd8380326b827e22dd0be5aa4" proved="true" expanded="true" shape="iainfix >V2c0iainfix =amodV2c2c1ainfix <V7V2Aainfix <=c0V2Aainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix <=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3Fainfix <V9V2Aainfix <=c0V2Aainfix =ainfix *V4apowerV8V9apowerV0V1Aainfix <=c0V9Iainfix =V9adivV2c2FIainfix =V8ainfix *V3V3Fainfix =V4apowerV0V1Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFAainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix <=c0V1Iainfix <=c0V1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter fast_exp_imperative.1" expl="loop invariant init" sum="bf0f389b38ed69a2beff47c1bb10a940" proved="true" expanded="true" shape="ainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix <=c0V1Iainfix <=c0V1FF">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<goal
name="WP_parameter fast_exp_imperative"
expl="parameter fast_exp_imperative"
sum="d3f84a4dd8380326b827e22dd0be5aa4"
proved="true"
expanded="true"
shape="iainfix >V2c0iainfix =amodV2c2c1ainfix <V7V2Aainfix <=c0V2Aainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix <=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3Fainfix <V9V2Aainfix <=c0V2Aainfix =ainfix *V4apowerV8V9apowerV0V1Aainfix <=c0V9Iainfix =V9adivV2c2FIainfix =V8ainfix *V3V3Fainfix =V4apowerV0V1Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFAainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix <=c0V1Iainfix <=c0V1FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter fast_exp_imperative.1"
expl="loop invariant init"
sum="bf0f389b38ed69a2beff47c1bb10a940"
proved="true"
expanded="true"
shape="ainfix =ainfix *c1apowerV0V1apowerV0V1Aainfix <=c0V1Iainfix <=c0V1FF">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="cvc3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<proof
prover="cvc3"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="z3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.01"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.2" expl="loop invariant preservation" sum="090f1fa2d9526c6a93902ed56477a27a" proved="true" expanded="true" shape="ainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix <=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.12"/>
<goal
name="WP_parameter fast_exp_imperative.2"
expl="loop invariant preservation"
sum="090f1fa2d9526c6a93902ed56477a27a"
proved="true"
expanded="true"
shape="ainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix <=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.06"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.84"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.42"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.3" expl="loop variant decreases" sum="50b3ebd224c35da27eb97a3326e280a7" proved="true" expanded="true" shape="ainfix <V7V2Aainfix <=c0V2Iainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix <=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<goal
name="WP_parameter fast_exp_imperative.3"
expl="loop variant decreases"
sum="50b3ebd224c35da27eb97a3326e280a7"
proved="true"
expanded="true"
shape="ainfix <V7V2Aainfix <=c0V2Iainfix =ainfix *V5apowerV6V7apowerV0V1Aainfix <=c0V7Iainfix =V7adivV2c2FIainfix =V6ainfix *V3V3FIainfix =V5ainfix *V4V3FIainfix =amodV2c2c1Iainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.23"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.10"/>
</proof>
<proof prover="z3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4" expl="loop invariant preservation" sum="720be8e9b9f81e3f859b16bcc46f6f30" proved="true" expanded="true" shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Aainfix <=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter fast_exp_imperative.4.1" expl="parameter fast_exp_imperative" sum="63ffb2e47776120b9d96ac711018ec9a" proved="true" expanded="true" shape="ainfix <=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<goal
name="WP_parameter fast_exp_imperative.4"
expl="loop invariant preservation"
sum="720be8e9b9f81e3f859b16bcc46f6f30"
proved="true"
expanded="true"
shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Aainfix <=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter fast_exp_imperative.4.1"
expl="parameter fast_exp_imperative"
sum="63ffb2e47776120b9d96ac711018ec9a"
proved="true"
expanded="true"
shape="ainfix <=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
<proof prover="z3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.4.2" expl="parameter fast_exp_imperative" sum="d9ddf441b5ac0c79579e09a303cdc52b" proved="true" expanded="true" shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof prover="coq" timelimit="5" edited="power_WP_M_WP_parameter_fast_exp_imperative_3.v" obsolete="false">
<result status="valid" time="0.74"/>
<goal
name="WP_parameter fast_exp_imperative.4.2"
expl="parameter fast_exp_imperative"
sum="d9ddf441b5ac0c79579e09a303cdc52b"
proved="true"
expanded="true"
shape="ainfix =ainfix *V4apowerV5V6apowerV0V1Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof
prover="coq"
timelimit="5"
edited="power_WP_M_WP_parameter_fast_exp_imperative_3.v"
obsolete="false">
<result status="valid" time="0.63"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter fast_exp_imperative.5" expl="loop variant decreases" sum="59a7cd42627dbfdbc77899ee0de3b3a4" proved="true" expanded="true" shape="ainfix <V6V2Aainfix <=c0V2Iainfix =ainfix *V4apowerV5V6apowerV0V1Aainfix <=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<goal
name="WP_parameter fast_exp_imperative.5"
expl="loop variant decreases"
sum="59a7cd42627dbfdbc77899ee0de3b3a4"
proved="true"
expanded="true"
shape="ainfix <V6V2Aainfix <=c0V2Iainfix =ainfix *V4apowerV5V6apowerV0V1Aainfix <=c0V6Iainfix =V6adivV2c2FIainfix =V5ainfix *V3V3FIainfix =amodV2c2c1NIainfix >V2c0Iainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
<proof prover="alt-ergo" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.10"/>
<proof
prover="alt-ergo"
timelimit="10"
edited=""
obsolete="false">
<result status="valid" time="0.05"/>
</proof>
<proof prover="z3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.01"/>
</proof>
</goal>
<goal name="WP_parameter fast_exp_imperative.6" expl="normal postcondition" sum="0e5707d10bc270abb7a299e973704522" proved="true" expanded="true" shape="ainfix =V4apowerV0V1Iainfix >V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<transf name="split_goal" proved="true" expanded="true">
<goal name="WP_parameter fast_exp_imperative.6.1" expl="normal postcondition" sum="0e5707d10bc270abb7a299e973704522" proved="true" expanded="true" shape="ainfix =V4apowerV0V1Iainfix >V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.02"/>
<goal
name="WP_parameter fast_exp_imperative.6"
expl="normal postcondition"
sum="0e5707d10bc270abb7a299e973704522"
proved="true"
expanded="true"
shape="ainfix =V4apowerV0V1Iainfix >V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<transf
name="split_goal"
proved="true"
expanded="true">
<goal
name="WP_parameter fast_exp_imperative.6.1"
expl="normal postcondition"
sum="0e5707d10bc270abb7a299e973704522"
proved="true"
expanded="true"
shape="ainfix =V4apowerV0V1Iainfix >V2c0NIainfix =ainfix *V4apowerV3V2apowerV0V1Aainfix <=c0V2FFFIainfix <=c0V1FF">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
......
examples/programs/vstte10_aqueue/why3session.xml
View file @ 8051c0eb
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/vstte10_aqueue/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../vstte10_aqueue.mlw" verified="true" expanded="true">
<theory name="WP AmortizedQueue" verified="true" expanded="true">
<goal name="WP_parameter empty" expl="normal postcondition" sum="56199579334bc0c09dfc265f9a083361" proved="true" expanded="false" shape="ainfix =asequenceamk queueaNilc0aNilc0aNilAainvamk queueaNilc0aNilc0">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<why3session
name="programs/vstte10_aqueue/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.3pl2"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="gappa"
name="Gappa"
version="0.15.0"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../vstte10_aqueue.mlw"
verified="true"
expanded="true">
<theory
name="WP AmortizedQueue"
verified="true"
expanded="true">
<goal
name="WP_parameter empty"
expl="normal postcondition"
sum="230f294d32073949569b6813fdd40338"
proved="true"
expanded="false"
shape="ainfix =asequenceamk queueaNilc0aNilc0aNilAainvamk queueaNilc0aNilc0">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter head" expl="parameter head" sum="19a1eda8e90f4479d688665d97f387af" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNilfaConsVwainfix =CasequenceV4aNilaNoneaConsVwaSomeV6aSomeV5Iainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.06"/>
<goal
name="WP_parameter head"
expl="parameter head"
sum="5d971bd8dc2798166e5f557be97bc250"
proved="true"
expanded="false"
shape="Lamk queueV0V1V2V3CV0aNilfaConsVwainfix =CasequenceV4aNilaNoneaConsVwaSomeV6aSomeV5Iainfix =asequenceV4aNilNAainvV4F">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal name="WP_parameter create" expl="parameter create" sum="3dfcc4b3b2a01618a67bab2d1e2834a0" proved="true" expanded="false" shape="LalengthV2iainfix >=V1V3ainfix =asequenceamk queueV0V1V2V3ainfix ++V0areverseV2Aainvamk queueV0V1V2V3ainfix =asequenceamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0ainfix ++V0areverseV2Aainvamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0Iainfix =V1alengthV0FFF">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.55"/>
<goal
name="WP_parameter create"
expl="parameter create"
sum="9f62cd1a4911914c0718f32d6ee320db"
proved="true"
expanded="false"
shape="LalengthV2iainfix >=V1V3ainfix =asequenceamk queueV0V1V2V3ainfix ++V0areverseV2Aainvamk queueV0V1V2V3ainfix =asequenceamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0ainfix ++V0areverseV2Aainvamk queueainfix ++V0areverseV2ainfix +V1V3aNilc0Iainfix =V1alengthV0FFF">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.36"/>
</proof>
</goal>
<goal name="WP_parameter tail" expl="parameter tail" sum="eae68069fc0e15b3357b1ded3a01e7f3" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNilfaConswVLamk queueV6V7V8V9ainfix =CasequenceV4aNilaNoneaConswVaSomeV11aSomeasequenceV10AainvV10Iainfix =asequenceV10ainfix ++V5areverseV2AainvV10FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<transf name="split_goal" proved="true" expanded="false">
<goal name="WP_parameter tail.1" expl="parameter tail" sum="71bd2802efe3cfe29e3169ef3daf1f1d" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNilfaConswVtIainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<goal
name="WP_parameter tail"
expl="parameter tail"
sum="e27fbf04990d6cb6cea41882773bbc2d"
proved="true"
expanded="false"
shape="Lamk queueV0V1V2V3CV0aNilfaConswVLamk queueV6V7V8V9ainfix =CasequenceV4aNilaNoneaConswVaSomeV11aSomeasequenceV10AainvV10Iainfix =asequenceV10ainfix ++V5areverseV2AainvV10FAainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<transf
name="split_goal"
proved="true"
expanded="false">
<goal
name="WP_parameter tail.1"
expl="parameter tail"
sum="386d61acc6104cd83432d31effdf2903"
proved="true"
expanded="false"
shape="Lamk queueV0V1V2V3CV0aNilfaConswVtIainfix =asequenceV4aNilNAainvV4F">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal name="WP_parameter tail.2" expl="parameter tail" sum="ef1133c6110aaf6c8ae111b4bd3d1c16" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNiltaConswVainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.05"/>
<goal
name="WP_parameter tail.2"
expl="parameter tail"
sum="e947312d041b790683bec575aea37c1b"
proved="true"
expanded="false"
shape="Lamk queueV0V1V2V3CV0aNiltaConswVainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.03"/>
</proof>
</goal>
<goal name="WP_parameter tail.3" expl="parameter tail" sum="4dd78769b1a8286913ecd7d7979c8591" proved="true" expanded="false" shape="Lamk queueV0V1V2V3CV0aNiltaConswVLamk queueV6V7V8V9ainfix =CasequenceV4aNilaNoneaConswVaSomeV11aSomeasequenceV10AainvV10Iainfix =asequenceV10ainfix ++V5areverseV2AainvV10FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.26"/>
<goal
name="WP_parameter tail.3"
expl="parameter tail"
sum="82715c8aecd7f67c840f13f1bad05863"
proved="true"
expanded="false"
shape="Lamk queueV0V1V2V3CV0aNiltaConswVLamk queueV6V7V8V9ainfix =CasequenceV4aNilaNoneaConswVaSomeV11aSomeasequenceV10AainvV10Iainfix =asequenceV10ainfix ++V5areverseV2AainvV10FIainfix =V3alengthV2Aainfix =ainfix -V1c1alengthV5Iainfix =asequenceV4aNilNAainvV4F">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.14"/>
</proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter enqueue" expl="parameter enqueue" sum="84ebb382d72476b4bca544c3f5435117" proved="true" expanded="false" shape="Lamk queueV1V2V3V4Lamk queueV6V7V8V9ainfix =asequenceV10ainfix ++asequenceV5aConsV0aNilAainvV10Iainfix =asequenceV10ainfix ++V1areverseaConsV0V3AainvV10FAainfix =ainfix +V4c1alengthaConsV0V3Aainfix =V2alengthV1IainvV5FF">
<proof prover="alt-ergo" timelimit="20" edited="" obsolete="false">
<result status="valid" time="0.19"/>
<goal
name="WP_parameter enqueue"
expl="parameter enqueue"
sum="73a156b122d8f82a5ab0969ef9ebf079"
proved="true"
expanded="false"
shape="Lamk queueV1V2V3V4Lamk queueV6V7V8V9ainfix =asequenceV10ainfix ++asequenceV5aConsV0aNilAainvV10Iainfix =asequenceV10ainfix ++V1areverseaConsV0V3AainvV10FAainfix =ainfix +V4c1alengthaConsV0V3Aainfix =V2alengthV1IainvV5FF">
<proof
prover="alt-ergo"
timelimit="20"
edited=""
obsolete="false">
<result status="valid" time="0.09"/>