Commit d625cbbd authored by MARCHE Claude's avatar MARCHE Claude

updated sessions for lagrange, cauchy-schwarz and triangle inequalities

parent 2e93c184
......@@ -20,7 +20,7 @@
<prover
id="4"
name="Coq"
version="8.3pl4"/>
version="8.4"/>
<prover
id="5"
name="Z3"
......@@ -38,14 +38,14 @@
locfile="../lagrange_inequality.why"
loclnum="3" loccnumb="7" loccnume="25"
verified="true"
expanded="false">
expanded="true">
<goal
name="norm2_pos"
locfile="../lagrange_inequality.why"
loclnum="24" loccnumb="8" loccnume="17"
sum="c6713b13328556e5aa44d719637857fd"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anorm2V0V1c0.0F">
<proof
prover="5"
......@@ -70,7 +70,7 @@
loclnum="28" loccnumb="8" loccnume="16"
sum="1a74668a6a15dfafb66a489f26ce72c0"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =ainfix *anorm2V0V1anorm2V2V3ainfix +asqradotV0V1V2V3asqrainfix -ainfix *V0V3ainfix *V1V2F">
<proof
prover="5"
......@@ -102,7 +102,7 @@
loclnum="42" loccnumb="8" loccnume="25"
sum="8ba764166645697844f18c787d612735"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=asqradotV0V1V2V3ainfix *anorm2V0V1anorm2V2V3F">
<proof
prover="2"
......@@ -127,7 +127,7 @@
loclnum="50" loccnumb="8" loccnume="16"
sum="bae896604a117b9697d08353f3ed6435"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anormV0V1c0.0F">
<proof
prover="0"
......@@ -184,7 +184,7 @@
loclnum="54" loccnumb="8" loccnume="19"
sum="ce3b326b0d6887f18e3115dd235b6a7a"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=V0asqrtV1Iainfix &lt;=asqrV0V1F">
<proof
prover="4"
......@@ -193,7 +193,7 @@
edited="lagrange_inequality_CauchySchwarzInequality_sqr_le_sqrt_1.v"
obsolete="false"
archived="false">
<result status="valid" time="1.12"/>
<result status="valid" time="1.61"/>
</proof>
</goal>
<goal
......@@ -202,7 +202,7 @@
loclnum="57" loccnumb="8" loccnume="21"
sum="3027e8050a1b1b1fae27eaacfc79e36c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=adotV0V1V2V3ainfix *anormV0V1anormV2V3F">
<proof
prover="0"
......@@ -219,7 +219,7 @@
edited="lagrange_inequality_CauchySchwarzInequality_CauchySchwarz_1.v"
obsolete="false"
archived="false">
<result status="valid" time="0.85"/>
<result status="valid" time="1.41"/>
</proof>
</goal>
</theory>
......@@ -235,7 +235,7 @@
loclnum="77" loccnumb="8" loccnume="20"
sum="0d3d97f95fe13be3df20f19761742f49"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=anorm2ainfix +V0V2ainfix +V1V3asqrainfix +anormV0V1anormV2V3F">
<proof
prover="5"
......@@ -260,7 +260,7 @@
loclnum="82" loccnumb="8" loccnume="19"
sum="4592f000abc47d88953aaf6cc810981c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=asqrtV0V1Iainfix &lt;=V0asqrV1Aainfix &lt;=c0.0V0Aainfix &lt;=c0.0V1F">
<proof
prover="0"
......@@ -301,7 +301,7 @@
loclnum="85" loccnumb="8" loccnume="16"
sum="c312a44ce3003ac500885e4899b0f591"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=anormainfix +V0V2ainfix +V1V3ainfix +anormV0V1anormV2V3F">
<proof
prover="0"
......
......@@ -8,7 +8,7 @@
<prover
id="1"
name="Alt-Ergo"
version="0.95"/>
version="0.95.1"/>
<prover
id="2"
name="CVC3"
......@@ -41,7 +41,7 @@
loclnum="30" loccnumb="8" loccnume="17"
sum="c6713b13328556e5aa44d719637857fd"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anorm2V0V1c0.0F">
<proof
prover="4"
......@@ -66,7 +66,7 @@
loclnum="43" loccnumb="8" loccnume="14"
sum="4bf0d64706cccba6fae9418c1f312b1e"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =apV0V1V2V3V4anorm2ainfix +V0ainfix *V4V2ainfix +V1ainfix *V4V3F">
<proof
prover="2"
......@@ -188,21 +188,13 @@
proved="true"
expanded="true"
shape="ainfix =ainfix +ainfix +anorm2V0V1ainfix *ainfix *c2.0aprefix -ainfix /adotV0V1V2V3anorm2V2V3adotV0V1V2V3ainfix *asqraprefix -ainfix /adotV0V1V2V3anorm2V2V3anorm2V2V3ainfix +anorm2V0V1aprefix -ainfix /asqradotV0V1V2V3anorm2V2V3Iainfix &lt;c0.0anorm2V2V3F">
<proof
prover="0"
timelimit="30"
memlimit="4000"
obsolete="false"
archived="false">
<result status="valid" time="0.33"/>
</proof>
<proof
prover="1"
timelimit="30"
memlimit="4000"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.63"/>
<result status="valid" time="0.43"/>
</proof>
</goal>
</transf>
......@@ -213,7 +205,7 @@
loclnum="59" loccnumb="8" loccnume="22"
sum="85bc73eb1e3dcd9e39d84419a6e3cd1b"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=ainfix -anorm2V0V1ainfix /asqradotV0V1V2V3anorm2V2V3c0.0Iainfix &gt;anorm2V2V3c0.0F">
<proof
prover="0"
......@@ -229,7 +221,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.23"/>
<result status="valid" time="0.02"/>
</proof>
</goal>
<goal
......@@ -238,7 +230,7 @@
loclnum="64" loccnumb="8" loccnume="26"
sum="6dafe957c05d4d4481fbcdae0f95cf60"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=ainfix *anorm2V2V3apV0V1V2V3ainfix /aprefix -adotV0V1V2V3anorm2V2V3c0.0Iainfix &gt;anorm2V2V3c0.0F">
<proof
prover="0"
......@@ -263,7 +255,7 @@
loclnum="69" loccnumb="8" loccnume="34"
sum="0efbf4657fbbb30ead5ffc3323d2d94c"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=asqradotV0V1V2V3ainfix *anorm2V0V1anorm2V2V3Iainfix &gt;anorm2V2V3c0.0F">
<proof
prover="0"
......@@ -279,7 +271,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.90"/>
<result status="timeout" time="29.94"/>
</proof>
</goal>
<goal
......@@ -288,7 +280,7 @@
loclnum="74" loccnumb="8" loccnume="17"
sum="7e3a265b12669732a872b760314d15c6"
proved="true"
expanded="false"
expanded="true"
shape="ainfix =V1c0.0Oainfix =V0c0.0Iainfix =anorm2V0V1c0.0F">
<proof
prover="0"
......@@ -313,7 +305,7 @@
loclnum="78" loccnumb="8" loccnume="30"
sum="d92ffa92c844a0e219a5c060906924ce"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=asqradotV0V1V2V3ainfix *anorm2V0V1anorm2V2V3Iainfix =anorm2V2V3c0.0F">
<proof
prover="0"
......@@ -370,7 +362,7 @@
loclnum="83" loccnumb="8" loccnume="25"
sum="f503826c0855b489c83cd9b2d32a2476"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=asqradotV0V1V2V3ainfix *anorm2V0V1anorm2V2V3F">
<proof
prover="0"
......@@ -419,7 +411,7 @@
loclnum="91" loccnumb="8" loccnume="16"
sum="c871e0a08e431eca5ac7303db17208de"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &gt;=anormV0V1c0.0F">
<proof
prover="0"
......@@ -476,7 +468,7 @@
loclnum="95" loccnumb="8" loccnume="19"
sum="110ea3076bceb5ffe4e2a9d8d28e19e8"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=V0asqrtV1Iainfix &lt;=asqrV0V1Aainfix &lt;=c0.0asqrV0Aainfix &lt;=c0.0V0F">
<proof
prover="0"
......@@ -501,7 +493,7 @@
loclnum="99" loccnumb="8" loccnume="21"
sum="d1d9abeb8d1e95a154667e2755e33e42"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=adotV0V1V2V3ainfix *anormV0V1anormV2V3F">
<proof
prover="0"
......@@ -517,7 +509,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.32"/>
<result status="timeout" time="2.99"/>
</proof>
</goal>
</theory>
......@@ -533,7 +525,7 @@
loclnum="118" loccnumb="8" loccnume="20"
sum="184aec3bef26362dc011f2281c2f365e"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=anorm2ainfix +V0V2ainfix +V1V3asqrainfix +anormV0V1anormV2V3F">
<proof
prover="4"
......@@ -550,7 +542,7 @@
loclnum="123" loccnumb="8" loccnume="19"
sum="402ac12c4d8ec94ad412037107baaca3"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=asqrtV0V1Iainfix &lt;=V0asqrV1Aainfix &lt;=c0.0V0Aainfix &lt;=c0.0V1F">
<proof
prover="0"
......@@ -591,7 +583,7 @@
loclnum="126" loccnumb="8" loccnume="16"
sum="f960411051796024f2c2d99e8223d6cd"
proved="true"
expanded="false"
expanded="true"
shape="ainfix &lt;=anormainfix +V0V2ainfix +V1V3ainfix +anormV0V1anormV2V3F">
<proof
prover="0"
......@@ -607,7 +599,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.09"/>
<result status="timeout" time="3.00"/>
</proof>
</goal>
</theory>
......
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