Commit 05e8681c authored by MARCHE Claude's avatar MARCHE Claude

Updated sessions for nightly bench

parent 27f632fd
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<why3session
shape_version="2">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
......@@ -9,7 +8,7 @@
<prover
id="1"
name="Coq"
version="8.3pl3"/>
version="8.3pl4"/>
<prover
id="2"
name="Simplify"
......@@ -94,7 +93,7 @@
edited="hello_proof_HelloProof_G2_1.v"
obsolete="false"
archived="false">
<result status="unknown" time="0.76"/>
<result status="unknown" time="0.43"/>
</proof>
<proof
prover="2"
......
......@@ -38,7 +38,7 @@
locfile="../blocking_semantics2.mlw"
loclnum="6" loccnumb="7" loccnume="14"
verified="false"
expanded="false">
expanded="true">
<goal
name="get_stack_eq"
locfile="../blocking_semantics2.mlw"
......@@ -473,7 +473,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.98"/>
<result status="valid" time="0.18"/>
</proof>
<proof
prover="2"
......@@ -728,7 +728,7 @@
locfile="../blocking_semantics2.mlw"
loclnum="533" loccnumb="7" loccnume="20"
verified="false"
expanded="false">
expanded="true">
<goal
name="Test13"
locfile="../blocking_semantics2.mlw"
......@@ -905,7 +905,7 @@
locfile="../blocking_semantics2.mlw"
loclnum="586" loccnumb="7" loccnume="17"
verified="false"
expanded="false">
expanded="true">
<goal
name="consequence_rule"
locfile="../blocking_semantics2.mlw"
......@@ -1055,14 +1055,14 @@
locfile="../blocking_semantics2.mlw"
loclnum="665" loccnumb="7" loccnume="9"
verified="false"
expanded="true">
expanded="false">
<goal
name="assigns_refl"
locfile="../blocking_semantics2.mlw"
loclnum="679" loccnumb="6" loccnume="18"
sum="691b4a950d4fb69698e595e7d6e67155"
proved="true"
expanded="true"
expanded="false"
shape="aassignsV0V1V0F">
<proof
prover="0"
......@@ -1079,7 +1079,7 @@
loclnum="682" loccnumb="6" loccnume="19"
sum="e72c9bac070e4888eae25bacd28230c0"
proved="true"
expanded="true"
expanded="false"
shape="aassignsV0V3V2IaassignsV1V3V2AaassignsV0V3V1F">
<proof
prover="0"
......@@ -1096,7 +1096,7 @@
loclnum="687" loccnumb="6" loccnume="24"
sum="4de0e7cd3678845163fea4ddae002b99"
proved="true"
expanded="true"
expanded="false"
shape="aassignsV0aunionV2V3V1IaassignsV0V2V1F">
<proof
prover="0"
......@@ -1113,7 +1113,7 @@
loclnum="691" loccnumb="6" loccnume="25"
sum="2c35eb4b97f2d4c289e1acc6ec516a09"
proved="true"
expanded="true"
expanded="false"
shape="aassignsV0aunionV2V3V1IaassignsV0V3V1F">
<proof
prover="0"
......@@ -1130,7 +1130,7 @@
loclnum="759" loccnumb="8" loccnume="33"
sum="be47737172e5671c7aaa55f7a7fd37cf"
proved="false"
expanded="true"
expanded="false"
shape="afresh_in_fmlaaresultawpV0V1F">
<proof
prover="4"
......@@ -1157,7 +1157,7 @@
loclnum="773" loccnumb="8" loccnume="20"
sum="8303f19fb131736c0ca9a12b89496224"
proved="false"
expanded="true"
expanded="false"
shape="avalid_fmlaaFimpliesawpV0V1awpV0V2Iavalid_fmlaaFimpliesV1V2F">
<proof
prover="4"
......@@ -1175,7 +1175,7 @@
loclnum="778" loccnumb="8" loccnume="20"
sum="1d12416ea3c79d39a42fed5efcc89076"
proved="true"
expanded="true"
expanded="false"
shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F">
<proof
prover="4"
......@@ -1193,7 +1193,7 @@
loclnum="791" loccnumb="8" loccnume="20"
sum="9338f5886af84236ed351d30918db37a"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0aEvalueV1EOais_valueV0NF">
<proof
prover="2"
......@@ -1218,7 +1218,7 @@
loclnum="794" loccnumb="8" loccnume="18"
sum="677b063d1ca65cae1de5582db67cc56b"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0aVboolaTrueOainfix =V0aVboolaFalseIatype_exprV1V2aEvalueV0aTYboolF">
<proof
prover="4"
......@@ -1236,7 +1236,7 @@
loclnum="799" loccnumb="8" loccnume="18"
sum="864eed57b4cc97dd3656758f67a8014e"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =V0aVvoidIatype_exprV1V2aEvalueV0aTYunitF">
<proof
prover="2"
......@@ -1253,7 +1253,7 @@
loclnum="803" loccnumb="8" loccnume="16"
sum="22825d9d05f5b2b5efaa0fd2b4ec7d0b"
proved="true"
expanded="true"
expanded="false"
shape="aone_stepV1V2V0V7V8V9EIais_valueV0NIaeval_fmlaV1V2awpV0V6Iatype_fmlaV3aConsaTuple2aresultV5V4V6Iatype_exprV3V4V0V5F">
<proof
prover="4"
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "/usr/local/share/why3/why3session.dtd">
<!DOCTYPE why3session SYSTEM "/home/marche/why3/share/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
......@@ -415,7 +415,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="parameter wp"
sum="917c9fa392280fcd2eec55d072558486"
sum="ca36efc8b3606fb37e394c56407b804c"
proved="false"
expanded="true"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVavalid_tripleasubstV1V6V7V0V1aSifVVVavalid_tripleaFandaFimpliesaFtermV8V12aFimpliesaFnotaFtermV8V11V0V1Iavalid_tripleV12V9V1FIavalid_tripleV11V10V1FaSassertVavalid_tripleaFimpliesV13V1V0V1aSwhileVVVavalid_tripleaFandV15aFandaFimpliesaFandaFtermV14V15V17aFimpliesaFandaFnotaFtermV14V15V1V0V1Iavalid_tripleV17V16V15FF">
......@@ -439,7 +439,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="9790cc1fd417477f9e71930a1c81388e"
sum="d6cc82e1eaea36ec027025bacc29124d"
proved="true"
expanded="false"
shape="CV0aSskipavalid_tripleV1V0V1aSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
......@@ -459,7 +459,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="04f0b357e67561b63482717b70b66b65"
sum="76687642530d6b2b926881d6a1b65459"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVavalid_tripleV5V0V1Iavalid_tripleV5V2V4FIavalid_tripleV4V3V1FaSassignVVtaSifVVVtaSassertVtaSwhileVVVtF">
......@@ -479,7 +479,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="af5162dc3c2c5e55234e4760311c4a0d"
sum="f18c418c598f9362ab0c1259acc1e691"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVavalid_tripleasubstV1V4V5V0V1aSifVVVtaSassertVtaSwhileVVVtF">
......@@ -499,7 +499,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="0015418a278db9380a70ae36fb85ba8f"
sum="f530afffd2fb136a2c17c31939ae49c9"
proved="true"
expanded="false"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVavalid_tripleaFandaFimpliesaFtermV6V10aFimpliesaFnotaFtermV6V9V0V1Iavalid_tripleV10V7V1FIavalid_tripleV9V8V1FaSassertVtaSwhileVVVtF">
......@@ -535,7 +535,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="13135c21d0766e2ebdd73c1232062160"
sum="e21e50f41a61c72f110c52d0ced8b9b4"
proved="true"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVavalid_tripleaFimpliesV9V1V0V1aSwhileVVVtF">
......@@ -580,7 +580,7 @@
locfile="../wp_total.mlw"
loclnum="343" loccnumb="10" loccnume="12"
expl="postcondition"
sum="683f99e64794b63acf4f60f0bab99bd6"
sum="abb6c6de1c3af669e9cd8cd046a9d4ae"
proved="false"
expanded="true"
shape="CV0aSskiptaSseqVVtaSassignVVtaSifVVVtaSassertVtaSwhileVVVavalid_tripleaFandV11aFandaFimpliesaFandaFtermV10V11V13aFimpliesaFandaFnotaFtermV10V11V1V0V1Iavalid_tripleV13V12V11FF">
......
......@@ -53,7 +53,7 @@ theory CauchySchwarzInequality
lemma p_val_part:
forall x1 x2 y1 y2:real.
norm2 y1 y2 > 0.0 ->
p x1 x2 y1 y2 (- dot x1 x2 y1 y2 / norm2 y1 y2) =
p x1 x2 y1 y2 (- (dot x1 x2 y1 y2 / norm2 y1 y2)) =
norm2 x1 x2 - sqr (dot x1 x2 y1 y2) / norm2 y1 y2
lemma p_val_part_pos:
......
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