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

updated proof session

parent 00009264
......@@ -548,18 +548,10 @@
expl="parameter t3"
sum="5f20971638b30640d32e2a10cb0d6572"
proved="true"
expanded="false"
expanded="true"
shape="ainfix <=c0amixfix []V13V15Iainfix <V15V14Aainfix <=c0V15FIainfix =V14ainfix +V11c1FIainfix =V13asetV12V11amin_eltV8FIamemV16V8NFNIainfix =amixfix []V4V17amixfix []V10V17Iainfix <V17V3Aainfix <=c0V17FAainfix =amixfix []V6V18amixfix []V12V18Iainfix <V18V11Aainfix <=c0V18FAaeq_prefixV19amixfix []V10V20anAainfix <V20V9Aainfix =V3V20Oainfix <V3V20Eqamemamixfix []V19V11adiffadiffadiffV0V1V2V8Aainfix =amixfix []V12V21amixfix []V19V21Iainfix <V21V11Aainfix <=c0V21FAapartial_solutionanV19FAainfix <V22V23IamemV23V8IamemV22adiffadiffadiffV0V1V2V8FAalt_solamixfix []V10V24amixfix []V10V25Iainfix <V25V9Aainfix <V24V25Aainfix <=V3V24FAainfix =ainfix -amixfix []V12V26amixfix []V12V27ainfix -V27V26NAainfix =ainfix -amixfix []V12V26amixfix []V12V27ainfix -V26V27NAainfix =amixfix []V12V26amixfix []V12V27NIainfix <V27V26Aainfix <=c0V27FAainfix <amixfix []V12V26anAainfix <=c0amixfix []V12V26Iainfix <V26V11Aainfix <=c0V26FAamemV28adiffadiffV0V1V2IamemV28V8FAainfix =V11V5Aainfix <=c0ainfix -V9V3Aainfix =V7ainfix +V9aprefix -V3FFFFFFIamemV29V0NFNIainfix =ainfix -amixfix []V6V30amixfix []V6V31ainfix -V31V30NAainfix =ainfix -amixfix []V6V30amixfix []V6V31ainfix -V30V31NAainfix =amixfix []V6V30amixfix []V6V31NIainfix <V31V30Aainfix <=c0V31FAainfix <amixfix []V6V30anAainfix <=c0amixfix []V6V30Iainfix <V30V5Aainfix <=c0V30FAainfix =agetV6V33ainfix +ainfix +V32V5aprefix -V33NIainfix <V33V5Aainfix =c0V33Oainfix <c0V33FqamemV32V2NIainfix <=c0V32FAainfix =agetV6V35ainfix +ainfix +V34V35aprefix -V5NIainfix <V35V5Aainfix =c0V35Oainfix <c0V35FqamemV34V1NIainfix <=c0V34FAainfix =agetV6V37V36NIainfix <V37V5Aainfix =c0V37Oainfix <c0V37FAainfix <V36anAainfix =c0V36Oainfix <c0V36qamemV36V0FAainfix <=c0V3Aainfix =ainfix +V5acardinalV0anAainfix =c0V5Oainfix <c0V5FFFFFFF">
<label
name="expl:parameter t3"/>
<proof
prover="1"
timelimit="30"
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="11.34"/>
</proof>
<proof
prover="0"
timelimit="30"
......@@ -649,7 +641,7 @@
expl="parameter t3"
sum="a12f0e3d40ba55fa67f3077ef01432c0"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =ainfix -amixfix []V13V15amixfix []V13V16ainfix -V15V16NIainfix &lt;V16V15Aainfix &lt;=c0V16FIainfix &lt;V15V14Aainfix &lt;=c0V15FIainfix =V14ainfix +V11c1FIainfix =V13asetV12V11amin_eltV8FIamemV17V8NFNIainfix =amixfix []V4V18amixfix []V10V18Iainfix &lt;V18V3Aainfix &lt;=c0V18FAainfix =amixfix []V6V19amixfix []V12V19Iainfix &lt;V19V11Aainfix &lt;=c0V19FAaeq_prefixV20amixfix []V10V21anAainfix &lt;V21V9Aainfix =V3V21Oainfix &lt;V3V21Eqamemamixfix []V20V11adiffadiffadiffV0V1V2V8Aainfix =amixfix []V12V22amixfix []V20V22Iainfix &lt;V22V11Aainfix &lt;=c0V22FAapartial_solutionanV20FAainfix &lt;V23V24IamemV24V8IamemV23adiffadiffadiffV0V1V2V8FAalt_solamixfix []V10V25amixfix []V10V26Iainfix &lt;V26V9Aainfix &lt;V25V26Aainfix &lt;=V3V25FAainfix =ainfix -amixfix []V12V27amixfix []V12V28ainfix -V28V27NAainfix =ainfix -amixfix []V12V27amixfix []V12V28ainfix -V27V28NAainfix =amixfix []V12V27amixfix []V12V28NIainfix &lt;V28V27Aainfix &lt;=c0V28FAainfix &lt;amixfix []V12V27anAainfix &lt;=c0amixfix []V12V27Iainfix &lt;V27V11Aainfix &lt;=c0V27FAamemV29adiffadiffV0V1V2IamemV29V8FAainfix =V11V5Aainfix &lt;=c0ainfix -V9V3Aainfix =V7ainfix +V9aprefix -V3FFFFFFIamemV30V0NFNIainfix =ainfix -amixfix []V6V31amixfix []V6V32ainfix -V32V31NAainfix =ainfix -amixfix []V6V31amixfix []V6V32ainfix -V31V32NAainfix =amixfix []V6V31amixfix []V6V32NIainfix &lt;V32V31Aainfix &lt;=c0V32FAainfix &lt;amixfix []V6V31anAainfix &lt;=c0amixfix []V6V31Iainfix &lt;V31V5Aainfix &lt;=c0V31FAainfix =agetV6V34ainfix +ainfix +V33V5aprefix -V34NIainfix &lt;V34V5Aainfix =c0V34Oainfix &lt;c0V34FqamemV33V2NIainfix &lt;=c0V33FAainfix =agetV6V36ainfix +ainfix +V35V36aprefix -V5NIainfix &lt;V36V5Aainfix =c0V36Oainfix &lt;c0V36FqamemV35V1NIainfix &lt;=c0V35FAainfix =agetV6V38V37NIainfix &lt;V38V5Aainfix =c0V38Oainfix &lt;c0V38FAainfix &lt;V37anAainfix =c0V37Oainfix &lt;c0V37qamemV37V0FAainfix &lt;=c0V3Aainfix =ainfix +V5acardinalV0anAainfix =c0V5Oainfix &lt;c0V5FFFFFFF">
<label
name="expl:parameter t3"/>
......
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