Commit bbb8bbd7 authored by Andrei Paskevich's avatar Andrei Paskevich

update sessions

parent 289f12c8
This diff is collapsed.
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="3">
<why3session shape_version="4">
<prover
id="0"
name="Alt-Ergo"
......@@ -62,7 +62,7 @@
name="G1"
locfile="../explicit_subst.why"
loclnum="75" loccnumb="7" loccnume="9"
sum="5903afdb505b8843946340fbcce7aade"
sum="9d61884adfb50bab312f819c51fc4685"
proved="true"
expanded="false"
shape="ainfix =aappaLambdaaVaraZeroaaaa">
......@@ -151,7 +151,7 @@
name="G2"
locfile="../explicit_subst.why"
loclnum="81" loccnumb="7" loccnume="9"
sum="0d5390957350a094633a3a0214248f90"
sum="63fab76f43ac1fc0fd49c8a15fee1dd4"
proved="true"
expanded="false"
shape="ainfix =aappaLambdaaVaraZeroaaab">
......@@ -201,7 +201,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.55"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
......@@ -209,7 +209,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.41"/>
<result status="valid" time="0.06"/>
</proof>
<proof
prover="7"
......@@ -240,7 +240,7 @@
name="G5b"
locfile="../explicit_subst.why"
loclnum="85" loccnumb="7" loccnume="10"
sum="23f6972dc38bd7e049fd40a41d4ee44f"
sum="4b789e543e21787266f3792ae4657ee8"
proved="true"
expanded="false"
shape="ainfix =V0V1LaLambdaaaLaLambdaasubstaVaraSaZeroaSaZeroaa">
......@@ -329,7 +329,7 @@
name="G5c"
locfile="../explicit_subst.why"
loclnum="90" loccnumb="7" loccnume="10"
sum="75389bebe26b15ead47174ca8940c5f0"
sum="794fb2ba59dab4c81285256139cb0bba"
proved="true"
expanded="false"
shape="ainfix =V0V1LaLambdaaaLasubstaLambdaaVaraSaZeroaZeroaa">
......@@ -418,7 +418,7 @@
name="G5"
locfile="../explicit_subst.why"
loclnum="95" loccnumb="7" loccnume="9"
sum="4a5362f02aa61f2a024bed46f986b896"
sum="f2bc93dd51df0bb4ba4aff9475ab642a"
proved="true"
expanded="false"
shape="ainfix =aappV0aaV1LaLambdaaaLaLambdaaLambdaaVaraSaZero">
......@@ -507,9 +507,9 @@
name="G3"
locfile="../explicit_subst.why"
loclnum="100" loccnumb="7" loccnume="9"
sum="329ef3023a344e8d1a5617a450ec9757"
sum="a9e5095e7b01c12fb6647ad1bfa2b0f5"
proved="true"
expanded="true"
expanded="false"
shape="ainfix =aappaappV0aaaidaaLaLambdaaLambdaaappaVaraZeroaVaraSaZero">
<proof
prover="0"
......@@ -533,7 +533,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.06"/>
<result status="valid" time="0.17"/>
</proof>
<proof
prover="4"
......@@ -549,7 +549,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.48"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
......@@ -557,7 +557,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.43"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="7"
......@@ -581,14 +581,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.95"/>
<result status="timeout" time="2.98"/>
</proof>
</goal>
<goal
name="G4"
locfile="../explicit_subst.why"
loclnum="104" loccnumb="7" loccnume="9"
sum="2c712f21cd0fb3aafbcbcd1f66089bbc"
sum="c0df2c5391772ab159dce0a39e23924d"
proved="true"
expanded="false"
shape="ainfix =aappV0aaV1LaLambdaaappaVaraZeroaaLaLambdaaLambdaaappaVaraZeroaVaraSaZero">
......@@ -606,7 +606,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
<result status="valid" time="0.51"/>
</proof>
<proof
prover="2"
......@@ -614,7 +614,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
<result status="valid" time="0.53"/>
</proof>
<proof
prover="3"
......@@ -638,7 +638,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="1.48"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="6"
......@@ -646,7 +646,7 @@
memlimit="0"
obsolete="false"
archived="false">
<result status="valid" time="0.45"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="7"
......@@ -686,12 +686,12 @@
locfile="../explicit_subst.why"
loclnum="159" loccnumb="7" loccnume="15"
verified="true"
expanded="false">
expanded="true">
<goal
name="G1"
locfile="../explicit_subst.why"
loclnum="168" loccnumb="7" loccnume="9"
sum="ece7e47e3ef4850287428fa000deb782"
sum="b7fbdb0f012ccfe5f7d1414fcb4ed68d"
proved="true"
expanded="false"
shape="ainfix =aappalambdaavaraZeroaaaa">
......@@ -772,7 +772,7 @@
name="G2"
locfile="../explicit_subst.why"
loclnum="174" loccnumb="7" loccnume="9"
sum="a3f57dca9da7938bf6106594f2f8d220"
sum="273a22e47215c1a2b161639c04adfd2c"
proved="true"
expanded="false"
shape="ainfix =aappalambdaavaraZeroaaab">
......@@ -830,7 +830,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.97"/>
<result status="valid" time="0.07"/>
</proof>
<proof
prover="8"
......@@ -846,14 +846,14 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.63"/>
<result status="timeout" time="4.97"/>
</proof>
</goal>
<goal
name="G5b"
locfile="../explicit_subst.why"
loclnum="178" loccnumb="7" loccnume="10"
sum="997b5cf3d46c5e9e7ef3d700f25d773b"
sum="b23792ff3f632e3564a2dfc4ecf34391"
proved="true"
expanded="false"
shape="ainfix =V0V1LalambdaaaLalambdaasubstavaraSaZeroaSaZeroaa">
......@@ -934,7 +934,7 @@
name="G5c"
locfile="../explicit_subst.why"
loclnum="183" loccnumb="7" loccnume="10"
sum="a42cae3ee5b899f04cfc4bb97ce5878c"
sum="b38e4332720a850bca4a5e9eef0e758d"
proved="true"
expanded="false"
shape="ainfix =V0V1LalambdaaaLasubstalambdaavaraSaZeroaZeroaa">
......@@ -1015,7 +1015,7 @@
name="G5"
locfile="../explicit_subst.why"
loclnum="188" loccnumb="7" loccnume="9"
sum="8f1910faa42831536765bf750cec4958"
sum="285eb993216a7d601f90e6ec04f0a491"
proved="true"
expanded="false"
shape="ainfix =aappV0aaV1LalambdaaaLalambdaalambdaavaraSaZero">
......@@ -1096,7 +1096,7 @@
name="G3"
locfile="../explicit_subst.why"
loclnum="193" loccnumb="7" loccnume="9"
sum="bcd791cf92362c4ff0cffde1b30e8963"
sum="b606f7f49f7adff34cbede9dffeff7fb"
proved="true"
expanded="false"
shape="ainfix =aappaappV0aaaidaaLalambdaalambdaaappavaraZeroavaraSaZero">
......@@ -1122,7 +1122,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.18"/>
<result status="valid" time="0.04"/>
</proof>
<proof
prover="4"
......@@ -1169,7 +1169,7 @@
name="G4"
locfile="../explicit_subst.why"
loclnum="197" loccnumb="7" loccnume="9"
sum="21e2978de2e61ae0800a2658551e13fb"
sum="9180aeb394d788f4bd9018a21558ca82"
proved="true"
expanded="false"
shape="ainfix =aappV0aaV1LalambdaaappavaraZeroaaLalambdaalambdaaappavaraZeroavaraSaZero">
......@@ -1195,7 +1195,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="2.14"/>
<result status="valid" time="0.03"/>
</proof>
<proof
prover="4"
......
(* This file is generated by Why3's Coq driver *)
(* This file is generated by Why3's Coq 8.4 driver *)
(* Beware! Only edit allowed sections below *)
Require Import BuiltIn.
Require BuiltIn.
......@@ -16,7 +16,7 @@ Existing Instance ref_WhyType.
Implicit Arguments mk_ref [[a] [a_WT]].
(* Why3 assumption *)
Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
Definition contents {a:Type} {a_WT:WhyType a} (v:(@ref a a_WT)): a :=
match v with
| (mk_ref x) => x
end.
......@@ -24,34 +24,35 @@ Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
(* Why3 assumption *)
Inductive array
(a:Type) {a_WT:WhyType a} :=
| mk_array : Z -> (map.Map.map Z a) -> array a.
| mk_array : Z -> (@map.Map.map Z _ a a_WT) -> array a.
Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
Existing Instance array_WhyType.
Implicit Arguments mk_array [[a] [a_WT]].
(* Why3 assumption *)
Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
match v with
Definition elts {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): (@map.Map.map
Z _ a a_WT) := match v with
| (mk_array x x1) => x1
end.
(* Why3 assumption *)
Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
Definition length {a:Type} {a_WT:WhyType a} (v:(@array a a_WT)): Z :=
match v with
| (mk_array x x1) => x
end.
(* Why3 assumption *)
Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
Definition get {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z): a :=
(map.Map.get (elts a1) i).
(* Why3 assumption *)
Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
Definition set {a:Type} {a_WT:WhyType a} (a1:(@array a a_WT)) (i:Z)
(v:a): (@array a a_WT) := (mk_array (length a1) (map.Map.set (elts a1) i
v)).
(* Why3 assumption *)
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
(mk_array n (map.Map.const v:(map.Map.map Z a))).
Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (@array a a_WT) :=
(mk_array n (map.Map.const v:(@map.Map.map Z _ a a_WT))).
Parameter n: Z.
......@@ -77,12 +78,12 @@ Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem WP_parameter_distance : let o := n in ((0%Z <= o)%Z ->
(((0%Z < o)%Z \/ (0%Z = o)) -> ((((0%Z < 0%Z)%Z \/ (0%Z = 0%Z)) /\
(0%Z < o)%Z) -> forall (g:(map.Map.map Z Z)), (((0%Z < o)%Z \/
(0%Z = o)) /\ (g = (map.Map.set (map.Map.const 0%Z:(map.Map.map Z Z)) 0%Z
(((0%Z < o)%Z \/ (0%Z = o)) -> ((0%Z < o)%Z -> forall (g:(@map.Map.map Z _
Z _)), (((0%Z < o)%Z \/ (0%Z = o)) /\
(g = (map.Map.set (map.Map.const 0%Z:(@map.Map.map Z _ Z _)) 0%Z
(-1%Z)%Z))) -> let o1 := n in ((0%Z <= o1)%Z -> (((0%Z < o1)%Z \/
(0%Z = o1)) -> let o2 := (n - 1%Z)%Z in (((1%Z < o2)%Z \/ (1%Z = o2)) ->
forall (count:Z) (d:(map.Map.map Z Z)) (g1:(map.Map.map Z Z)),
forall (count:Z) (d:(@map.Map.map Z _ Z _)) (g1:(@map.Map.map Z _ Z _)),
(((((map.Map.get d 0%Z) = 0%Z) /\ (((map.Map.get g1 0%Z) = (-1%Z)%Z) /\
(((count + (map.Map.get d
((o2 + 1%Z)%Z - 1%Z)%Z))%Z < ((o2 + 1%Z)%Z - 1%Z)%Z)%Z \/
......@@ -99,13 +100,12 @@ Theorem WP_parameter_distance : let o := n in ((0%Z <= o)%Z ->
((count < n)%Z -> forall (k:Z), (((0%Z < k)%Z \/ (0%Z = k)) /\
(k < n)%Z) -> forall (d':Z), (path d' k) -> ((map.Map.get d
k) <= d')%Z))))))).
(* Why3 intros o h1 h2 (h3,h4) g (h5,h6) o1 h7 h8 o2 h9 count d g1
(((h10,(h11,h12)),h13),h14) h15 k (h16,h17) d' h18. *)
intros o _ h1 (h2,h3) g _ o1 h4 h5 o2 h6 count d g1 (((h7,(h8,h9)),h10),h11) h12 k
(* Why3 intros o h1 h2 h3 g (h4,h5) o1 h6 h7 o2 h8 count d g1
(((h9,(h10,h11)),h12),h13) h14 k (h15,h16) d' h17. *)
intros o _ _ h3 g _ o1 h4 h5 o2 h6 count d g1 (((h7,(h8,h9)),h10),h11) h12 k
(h13,h14) d' h15.
subst o o1 o2.
clear h1 h2.
clear h5 h6.
clear h4 h5 h6.
replace (n-1+1)%Z with n in * by omega.
clear count h9 h12.
generalize h13 h14 d' h15.
......
This diff is collapsed.
This diff is collapsed.
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -1875,7 +1875,7 @@
locfile="../vstte12_bfs.mlw"
loclnum="104" loccnumb="6" loccnume="9"
expl="5."
sum="32a3440e5c0a4c02aaedc554f30e25a0"
sum="adb691a4310a24a3c0b03ab1e47feccb"
proved="true"
expanded="true"
shape="amemV15V10Iainfix &lt;=V16V14IapathV0V15V16FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueINamemV17V7Fqainfix =V11aTrueFIamemV19V10IamemV19asuccV18FINamemV18V9INamemV18V7IamemV18V10FAamemV20V10IamemV20asuccV8FAamemV1V9OamemV1V7IamemV1V10ANamemV21V10OamemV21V9Iashortest_pathV0V21ainfix +V2c1FAainfix &lt;=V23ainfix +V2c1AapathV0V22V23EIamemV22V10FAamemV24V10Iainfix &lt;=V25V2IapathV0V24V25FAashortest_pathV0V26ainfix +V2c1IamemV26V9FAasubsetV9V10Aashortest_pathV0V27V2IamemV27V7FAasubsetV7V10FIamemV29V5IamemV29asuccV28FINamemV28V3INamemV28V7IamemV28V5INainfix =V28V8FANapathV0V8V30Iainfix &lt;V30V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5ANamemV31V5OamemV31V3Iashortest_pathV0V31ainfix +V2c1FAainfix &lt;=V33ainfix +V2c1AapathV0V32V33EIamemV32V5FAamemV34V5Iainfix &lt;=V35V2IapathV0V34V35FAashortest_pathV0V36ainfix +V2c1IamemV36V3FAasubsetV3V5Aashortest_pathV0V37V2IamemV37V7FAasubsetV7V5INainfix =V8V1Iainfix =V7aremoveV8V4AamemV8V4FFINNamemV38V4FINainfix =V6aTrueINamemV39V4Fqainfix =V6aTrueFIainfix =c0V2Oainfix &lt;c0V2AamemV41V5IamemV41asuccV40FINamemV40V3INamemV40V4IamemV40V5FANamemV42V3FINamemV43V4FAamemV1V3OamemV1V4IamemV1V5ANamemV44V5OamemV44V3Iashortest_pathV0V44ainfix +V2c1FAainfix &lt;=V46ainfix +V2c1AapathV0V45V46EIamemV45V5FAamemV47V5Iainfix &lt;=V48V2IapathV0V47V48FAashortest_pathV0V49ainfix +V2c1IamemV49V3FAasubsetV3V5Aashortest_pathV0V50V2IamemV50V4FAasubsetV4V5FF">
......@@ -1890,7 +1890,7 @@
locfile="../vstte12_bfs.mlw"
loclnum="104" loccnumb="6" loccnume="9"
expl="1."
sum="597ad4b35c4a76e68db019ca50b68b06"
sum="e820738e6524a221ebfc103912c65fff"
proved="true"
expanded="true"
shape="amemV15V10Iainfix &lt;=V16V14IapathV0V15V16FIainfix =V14ainfix +V2c1FIainfix =V13aemptyFIainfix =V12V9FIainfix =V11aTrueINamemV17V7Fqainfix =V11aTrueFIamemV19V10IamemV19asuccV18FINamemV18V9INamemV18V7IamemV18V10FAamemV20V10IamemV20asuccV8FAamemV1V9OamemV1V7IamemV1V10ANamemV21V10OamemV21V9Iashortest_pathV0V21ainfix +V2c1FAainfix &lt;=V23ainfix +V2c1AapathV0V22V23EIamemV22V10FAamemV24V10Iainfix &lt;=V25V2IapathV0V24V25FAashortest_pathV0V26ainfix +V2c1IamemV26V9FAasubsetV9V10Aashortest_pathV0V27V2IamemV27V7FAasubsetV7V10FIamemV29V5IamemV29asuccV28FINamemV28V3INamemV28V7IamemV28V5INainfix =V28V8FANapathV0V8V30Iainfix &lt;V30V2FAapathV0V8V2AamemV1V3OamemV1V7IamemV1V5ANamemV31V5OamemV31V3Iashortest_pathV0V31ainfix +V2c1FAainfix &lt;=V33ainfix +V2c1AapathV0V32V33EIamemV32V5FAamemV34V5Iainfix &lt;=V35V2IapathV0V34V35FAashortest_pathV0V36ainfix +V2c1IamemV36V3FAasubsetV3V5Aashortest_pathV0V37V2IamemV37V7FAasubsetV7V5INainfix =V8V1Iainfix =V7aremoveV8V4AamemV8V4FFINNamemV38V4FINainfix =V6aTrueINamemV39V4Fqainfix =V6aTrueFIainfix =c0V2Oainfix &lt;c0V2AamemV41V5IamemV41asuccV40FINamemV40V3INamemV40V4IamemV40V5FANamemV42V3FINamemV43V4FAamemV1V3OamemV1V4IamemV1V5ANamemV44V5OamemV44V3Iashortest_pathV0V44ainfix +V2c1FAainfix &lt;=V46ainfix +V2c1AapathV0V45V46EIamemV45V5FAamemV47V5Iainfix &lt;=V48V2IapathV0V47V48FAashortest_pathV0V49ainfix +V2c1IamemV49V3FAasubsetV3V5Aashortest_pathV0V50V2IamemV50V4FAasubsetV4V5FF">
......@@ -1910,7 +1910,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="1.20"/>
<result status="valid" time="0.33"/>
</proof>
</goal>
</transf>
......@@ -2018,7 +2018,7 @@
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="3.85"/>
<result status="valid" time="2.58"/>
</proof>
<proof
prover="5"
......
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