diff --git a/src_common/colibrics_lib.ml b/src_common/colibrics_lib.ml
index b4591ef053d62c863d65185fe3e312bdd59b6020..4c4360d578e885c098a6e481bb25c8ead42ffbff 100644
--- a/src_common/colibrics_lib.ml
+++ b/src_common/colibrics_lib.ml
@@ -35,5 +35,5 @@ end
module Interval = struct
module Bound = Interval__Bound
module Convexe = Interval__Convexe
-
+ module Union = Union__Union
end
diff --git a/src_common/dune b/src_common/dune
index c481f4006797a2637c0c9f4f4ad4748b1ae32219..71901f3d15fbdc52a7e3be4d359760308b347d46 100644
--- a/src_common/dune
+++ b/src_common/dune
@@ -2,7 +2,7 @@
(public_name colibrics.lib)
(name colibrics_lib)
(libraries zarith)
- (flags -w -27))
+ (flags -w -27-26-49))
(rule
(targets q__Q.ml)
@@ -35,6 +35,15 @@
interval_with_divider.T))
(mode promote))
+(rule
+ (targets union__Union.ml)
+ (deps q.mlw interval.mlw union.mlw)
+ (action
+ (run why3 extract -D ocaml64 -D %{dep:common.drv} --modular -o . -L .
+ union.Union))
+ (mode promote))
+
+
(rule
(alias runproof)
(deps
diff --git a/src_common/union.mlw b/src_common/union.mlw
index 4c8645ea411be69df49a8a4713386053ce97d11e..e719aa981f9bf4e155f9286e5557184767948a7f 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -38,46 +38,6 @@ module Union
| End -> ()
end
- function nth0 (i:int) (l:t0) : Q.t =
- match l with
- | Singleton q l ->
- if i = 0 then
- q
- else nth0 (i-1) l
-
- | Inter q _ q' _ l ->
- if i = 0 then
- q
- else if i = 1 then
- q'
- else nth0 (i-2) l
-
- | FiniteInf q _ ->
- if i = 0 then
- q
- else Q.make 0 1
- | End -> Q.make 0 1
- end
-
- lemma nth0_rewritted: forall i l.
- match l with
- | Singleton _ l' ->
- if i = -1 then
- true
- else nth0 (i+1) l = nth0 i l'
- | Inter _ _ _ _ l' ->
- if i = -2 then
- true
- else if i = -1 then
- true
- else nth0 (i+2) l = nth0 i l'
- | FiniteInf _ _ -> true
- | End -> true
- end
-
- lemma nth0_singleton: forall i q l.
- if i = 0 then nth0 i (Singleton q l) = q else nth0 i (Singleton q l) = nth0 (i-1) l
-
function length (l:t) : int =
match l with
| InfFinite _ _ l ->
@@ -87,19 +47,6 @@ module Union
| Inf ->
0
end
-
- function nth (i:int) (l:t) : Q.t =
- match l with
- | InfFinite q _ l ->
- if i = 0 then
- q
- else nth0 (i-1) l
-
- | Finite l ->
- nth0 i l
- | Inf ->
- Q.make 0 1
- end
predicate lt_bound0 (x:Q.t) (l:t0) =
match l with
@@ -112,6 +59,21 @@ module Union
| End -> true
end
+ let rec ghost lt_bound0_transitive (x:Q.t) (y:Q.t) (l:t0) (m:t0)
+ requires { forall q. lt_bound0 q l -> q <. x }
+ requires { x <=. y }
+ requires { lt_bound0 y m }
+ ensures { forall q. lt_bound0 q l -> lt_bound0 q m }
+ variant { m } =
+ match m with
+ | Singleton _ m ->
+ lt_bound0_transitive x y l m
+ | Inter _ _ _ _ m ->
+ lt_bound0_transitive x y l m
+ | FiniteInf _ _ -> ()
+ | End -> ()
+ end
+
predicate lt_bound (x:Q.t) (l:t) =
match l with
| InfFinite q _ l ->
@@ -208,23 +170,14 @@ module Union
match u.a with
| Inf -> (None, ghost 0., ghost 1.)
| InfFinite q _ _ -> (None, ghost (Q.real q)-.1., ghost (Q.real q)-.2.)
- | Finite (Singleton q End) -> (Some q,0., 1.)
+ | Finite (Singleton q End) -> (Some q,ghost 0., ghost 1.)
| Finite End -> absurd
| Finite (Inter q _ q' _ _) ->
- (* assert { nth 0 u.a = q }; *)
- (* assert { nth 1 u.a = q' }; *)
- (* assert { (Q.real q) <. (Q.real q') }; *)
(None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
| Finite (FiniteInf q _) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
| Finite (Singleton q (Singleton q' _)) ->
- (* assert { nth 0 u.a = q }; *)
- (* assert { nth 1 u.a = q' }; *)
- (* assert { (Q.real q) <. (Q.real q') }; *)
(None,ghost (Q.real q), ghost (Q.real q'))
| Finite (Singleton _ (Inter q _ q' _ _)) ->
- (* assert { nth 1 u.a = q }; *)
- (* assert { nth 2 u.a = q' }; *)
- (* assert { (Q.real q) <. (Q.real q') }; *)
(None, ghost (Q.real q)*.0.75+.(Q.real q')*.0.25, ghost (Q.real q)*.0.25+.(Q.real q')*.0.75)
| Finite (Singleton _ (FiniteInf q _)) -> (None,ghost (Q.real q)+.1.,ghost (Q.real q)+.2.)
end
@@ -320,22 +273,56 @@ module Union
| FiniteInf q b, FiniteInf q' b' ->
let (q'',b'') = max_bound_inf q b q' b' in
FiniteInf q'' b''
- | Singleton qu lu, FiniteInf qv bv ->
+ | (Singleton qu lu) as u, (FiniteInf qv bv) as v
+ | (FiniteInf qv bv) as v, (Singleton qu lu) as u ->
match Q.compare qu qv with
| Ord.Lt -> aux lu v
- | Ord.Gt -> Singleton qu (aux lu v)
- | Ord.Eq -> match bv with
- | Large -> Singleton qu (aux lu v)
- | Strict -> aux lu v
+ | Ord.Gt -> lt_bound0_transitive qv qu v lu; u
+ | Ord.Eq ->
+ lt_bound0_transitive qv qu v lu;
+ match bv with
+ | Large -> u
+ | Strict -> lu
end
end
- | FiniteInf qv bv, Singleton qu lu ->
- match Q.compare qu qv with
- | Ord.Lt -> aux lu u
- | Ord.Gt -> Singleton qu (aux lu u)
- | Ord.Eq -> match bv with
- | Large -> Singleton qu (aux lu u)
- | Strict -> aux lu u
+ | (FiniteInf q b) as u, (Inter qv0 bv0 qv1 bv1 lv) as v
+ | (Inter qv0 bv0 qv1 bv1 lv) as v, (FiniteInf q b) as u ->
+ match Q.compare q qv0 with
+ | Ord.Lt -> lt_bound0_transitive q qv1 u lv; v
+ | Ord.Gt -> match Q.compare q qv1 with
+ | Ord.Lt -> lt_bound0_transitive q qv1 u lv; Inter q b qv1 bv1 lv
+ | Ord.Gt -> aux u lv
+ | Ord.Eq ->
+ lt_bound0_transitive q qv1 u lv;
+ match b, bv1 with
+ | Large, Large -> Singleton q lv
+ | _ -> lv
+ end
+ end
+ | Ord.Eq ->
+ lt_bound0_transitive q qv1 u lv;
+ match b, bv0 with
+ | Strict, Large -> Inter qv0 b qv1 bv1 lv
+ | _ -> v
+ end
+ end
+ | (Singleton qu lu) as u, (Inter qv0 bv0 qv1 bv1 lv) as v
+ | (Inter qv0 bv0 qv1 bv1 lv) as v, (Singleton qu lu) as u ->
+ match Q.compare qu qv0 with
+ | Ord.Lt -> aux lu v
+ | Ord.Gt -> match Q.compare qu qv1 with
+ | Ord.Lt -> Singleton qu (aux lu v)
+ | Ord.Gt -> aux u lv
+ | Ord.Eq ->
+ match bv1 with
+ | Large -> Singleton qu (aux lu lv)
+ | _ -> aux lu lv
+ end
+ end
+ | Ord.Eq ->
+ match bv0 with
+ | Large -> Singleton qu (aux lu v)
+ | _ -> aux lu v
end
end
| Inter qu0 bu0 qu1 bu1 lu, Inter qv0 bv0 qv1 bv1 lv ->
@@ -372,8 +359,6 @@ module Union
| Ord.Lt -> aux lu v
| Ord.Gt ->
let (qw0,bw0) = max_bound_inf qu0 bu0 qv0 bv0 in
- assert { Q.(qv0 <= qw0 < qu1 < qv1) };
- assert { Q.(qu0 <= qw0 < qu1 < qv1) };
Inter qw0 bw0 qu1 bu1 (aux lu v)
end
in
@@ -389,12 +374,18 @@ module Union
| Ord.Lt -> small_big qu0 bu0 qu1 bu1 lu u qv0 bv0 qv1 bv1 lv v
| Ord.Gt -> small_big qv0 bv0 qv1 bv1 lv v qu0 bu0 qu1 bu1 lu u
end
- | _ -> absurd
end
in
let aux_option lu lv
requires { ordered0 lu }
requires { ordered0 lv }
+ ensures {
+ forall x:real. (mem0 x lu /\ mem0 x lv) <->
+ match result with
+ | None -> false
+ | Some w -> mem x w.a
+ end
+ }
=
match aux lu lv with
| End -> None
@@ -429,8 +420,6 @@ module Union
| Ord.Eq ->
match bu0, bv1 with
| Large, Large ->
- assert { length (InfFinite qv1 bv1 lv) = length0 (Singleton qv1 lv) };
- assert { forall i. nth i (InfFinite qv1 bv1 lv) = nth0 i (Singleton qv1 lv) };
aux_option lu (Singleton qv1 lv)
| _ -> aux_option lu lv
end
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index ed77a419a1c3133e33a6c22b9541d140eadd309b..6b96b6d95b58e27dff4e8a4e9d97bf0db56b7432 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -3,17 +3,14 @@
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="6">
<prover id="3" name="Colibri2" version="n/a" timelimit="5" steplimit="0" memlimit="1000"/>
-<file format="whyml">
+<file format="whyml" proved="true">
<path name=".."/><path name="union.mlw"/>
-<theory name="Union">
+<theory name="Union" proved="true">
<goal name="length0_positive'vc" expl="VC for length0_positive" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="nth0_rewritted" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="nth0_singleton" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="lt_bound0_transitive'vc" expl="VC for lt_bound0_transitive" proved="true">
+ <proof prover="3"><result status="valid" time="0.65"/></proof>
</goal>
<goal name="t''vc" expl="VC for t'" proved="true">
<transf name="split_vc" proved="true" >
@@ -37,7 +34,7 @@
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="is_singleton'vc.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.18"/></proof>
+ <proof prover="3"><result status="valid" time="3.62"/></proof>
</goal>
</transf>
</goal>
@@ -53,8 +50,8 @@
<goal name="max_bound_inf'vc" expl="VC for max_bound_inf" proved="true">
<proof prover="3"><result status="valid" time="0.13"/></proof>
</goal>
- <goal name="inter'vc" expl="VC for inter">
- <transf name="split_vc" >
+ <goal name="inter'vc" expl="VC for inter" proved="true">
+ <transf name="split_vc" proved="true" >
<goal name="inter'vc.0" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
@@ -77,21 +74,21 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.7" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.8" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.9" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.10" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.11" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.12" expl="variant decrease" proved="true">
+ <goal name="inter'vc.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.13" expl="precondition" proved="true">
@@ -100,17 +97,17 @@
<goal name="inter'vc.14" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.15" expl="variant decrease" proved="true">
+ <goal name="inter'vc.15" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.16" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.17" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.18" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.19" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -118,894 +115,1277 @@
<goal name="inter'vc.20" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.21" expl="unreachable point">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.21.0" expl="unreachable point">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.21" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.22" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.23" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.24" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.25" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.26" expl="precondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.26.0" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.22" expl="variant decrease" proved="true">
+ <goal name="inter'vc.27" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.28" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.29" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.23" expl="precondition" proved="true">
+ <goal name="inter'vc.30" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.31" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.24" expl="precondition" proved="true">
+ <goal name="inter'vc.32" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.25" expl="variant decrease" proved="true">
+ <goal name="inter'vc.33" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.26" expl="precondition" proved="true">
+ <goal name="inter'vc.34" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.27" expl="precondition" proved="true">
+ <goal name="inter'vc.35" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.28" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.36" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.29" expl="precondition" proved="true">
+ <goal name="inter'vc.37" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.38" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.39" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.40" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.30" expl="precondition" proved="true">
+ <goal name="inter'vc.41" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.31" expl="variant decrease" proved="true">
+ <goal name="inter'vc.42" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.43" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.32" expl="precondition" proved="true">
+ <goal name="inter'vc.44" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.45" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.33" expl="precondition" proved="true">
+ <goal name="inter'vc.46" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.34" expl="unreachable point">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.34.0" expl="unreachable point">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.47" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.48" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.49" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.50" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.51" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.52" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.53" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.54" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.55" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.35" expl="variant decrease" proved="true">
+ <goal name="inter'vc.56" expl="precondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.35.0" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.35.1" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.56.0" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.36" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.57" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.37" expl="precondition" proved="true">
+ <goal name="inter'vc.58" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.59" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.60" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.61" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.62" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.63" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.64" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.65" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.66" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.67" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.68" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.69" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.70" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.71" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.38" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <goal name="inter'vc.72" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.39" expl="precondition" proved="true">
+ <goal name="inter'vc.73" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.40" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.74" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.41" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.04"/></proof>
+ <goal name="inter'vc.75" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.42" expl="precondition" proved="true">
+ <goal name="inter'vc.76" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.43" expl="precondition" proved="true">
+ <goal name="inter'vc.77" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.78" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.79" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.44" expl="variant decrease" proved="true">
- <proof prover="3"><result status="valid" time="0.03"/></proof>
+ <goal name="inter'vc.80" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.45" expl="precondition" proved="true">
+ <goal name="inter'vc.81" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.82" expl="precondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.82.0" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.83" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.84" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.85" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.86" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.46" expl="precondition" proved="true">
+ <goal name="inter'vc.87" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.88" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.89" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.90" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.91" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.47" expl="assertion" proved="true">
+ <goal name="inter'vc.92" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.93" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.94" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.95" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.96" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.48" expl="assertion" proved="true">
+ <goal name="inter'vc.97" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.49" expl="variant decrease" proved="true">
+ <goal name="inter'vc.98" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.99" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
- <goal name="inter'vc.50" expl="precondition" proved="true">
+ <goal name="inter'vc.100" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.101" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.102" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="inter'vc.51" expl="precondition" proved="true">
+ <goal name="inter'vc.103" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="inter'vc.104" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.105" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="inter'vc.106" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.107" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.108" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="inter'vc.109" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.52" expl="postcondition" proved="true">
+ <goal name="inter'vc.110" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="inter'vc.111" expl="variant decrease" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.52.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.51"/></proof>
- </goal>
- <goal name="inter'vc.52.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.111.0" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.52.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.111.1" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="inter'vc.52.3" expl="postcondition" proved="true">
+ </transf>
+ </goal>
+ <goal name="inter'vc.112" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.113" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.114" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.114.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
+ </goal>
+ <goal name="inter'vc.114.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.52.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.45"/></proof>
+ <goal name="inter'vc.114.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.114.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.114.3.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.114.3.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.114.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.51"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.53" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.53.0" expl="postcondition" proved="true">
+ <goal name="inter'vc.115" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.115.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.53.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.75"/></proof>
+ <goal name="inter'vc.115.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.86"/></proof>
</goal>
- <goal name="inter'vc.53.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.60"/></proof>
+ <goal name="inter'vc.115.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.65"/></proof>
</goal>
- <goal name="inter'vc.53.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.24"/></proof>
+ <goal name="inter'vc.115.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.29"/></proof>
</goal>
- <goal name="inter'vc.53.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.71"/></proof>
+ <goal name="inter'vc.115.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.61"/></proof>
</goal>
- <goal name="inter'vc.53.0.4" expl="postcondition" proved="true">
- <proof prover="3" timelimit="30"><result status="valid" time="8.24"/></proof>
- <transf name="instantiate" proved="true" arg1="Ensures9" arg2="x">
- <goal name="inter'vc.53.0.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.12"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.115.0.4" expl="postcondition" proved="true">
+ <proof prover="3" timelimit="10"><result status="valid" time="9.90"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.53.1" expl="postcondition">
- <transf name="split_vc" >
- <goal name="inter'vc.53.1.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.00"/></proof>
+ <goal name="inter'vc.115.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.115.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.10"/></proof>
</goal>
- <goal name="inter'vc.53.1.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.25"/></proof>
+ <goal name="inter'vc.115.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.53.1.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.115.1.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="inter'vc.53.1.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.22"/></proof>
+ <goal name="inter'vc.115.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.25"/></proof>
</goal>
- <goal name="inter'vc.53.1.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.115.1.4" expl="postcondition" proved="true">
+ <proof prover="3" timelimit="10"><result status="valid" time="9.08"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.53.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.115.2" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.53.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.26"/></proof>
- </goal>
- <goal name="inter'vc.53.2.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
+ <goal name="inter'vc.115.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.33"/></proof>
</goal>
- <goal name="inter'vc.53.2.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.115.2.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="inter'vc.53.2.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.115.2.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="inter'vc.53.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.52"/></proof>
+ <goal name="inter'vc.115.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
+ </goal>
+ <goal name="inter'vc.115.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.48"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.54" expl="postcondition" proved="true">
+ <goal name="inter'vc.116" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.54.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.47"/></proof>
+ <goal name="inter'vc.116.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.45"/></proof>
</goal>
- <goal name="inter'vc.54.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <goal name="inter'vc.116.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.54.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.116.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.54.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.116.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.54.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.51"/></proof>
+ <goal name="inter'vc.116.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.48"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.55" expl="postcondition" proved="true">
+ <goal name="inter'vc.117" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.55.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.32"/></proof>
+ <goal name="inter'vc.117.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.55.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.31"/></proof>
+ <goal name="inter'vc.117.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="inter'vc.55.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.30"/></proof>
+ <goal name="inter'vc.117.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="inter'vc.55.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.30"/></proof>
+ <goal name="inter'vc.117.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.117.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.55.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.27"/></proof>
+ <goal name="inter'vc.117.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.26"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.56" expl="variant decrease" proved="true">
+ <goal name="inter'vc.118" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.57" expl="precondition" proved="true">
+ <goal name="inter'vc.119" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.58" expl="precondition" proved="true">
+ <goal name="inter'vc.120" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.59" expl="precondition" proved="true">
+ <goal name="inter'vc.121" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.60" expl="precondition" proved="true">
+ <goal name="inter'vc.122" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.61" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.123" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.62" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.124" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.63" expl="precondition" proved="true">
+ <goal name="inter'vc.125" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.64" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.65" expl="precondition" proved="true">
+ <goal name="inter'vc.126" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.66" expl="precondition" proved="true">
+ <goal name="inter'vc.127" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.67" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.68" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.69" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.70" expl="precondition" proved="true">
+ <goal name="inter'vc.128" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.71" expl="unreachable point">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.71.0" expl="unreachable point">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.72" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.72.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.72.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.72.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.72.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.21"/></proof>
- </goal>
- <goal name="inter'vc.72.4" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.72.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.72.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
- </goal>
- <goal name="inter'vc.72.4.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.30"/></proof>
- </goal>
- <goal name="inter'vc.72.4.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.72.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.72.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.72.7" expl="postcondition" proved="true">
+ <goal name="inter'vc.129" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.130" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.131" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="inter'vc.132" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.133" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.82"/></proof>
+ </goal>
+ <goal name="inter'vc.134" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.0" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.72.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.72.7.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.24"/></proof>
+ <goal name="inter'vc.134.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.72.7.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.30"/></proof>
+ <goal name="inter'vc.134.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.72.7.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- </transf>
- </goal>
- <goal name="inter'vc.72.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.72.9" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.72.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
+ <goal name="inter'vc.134.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.04"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.5" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.0.5.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.93"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.5.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.85"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.5.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.19"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.5.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.49"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.72.9.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.6" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.72.9.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.7" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.72.9.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.134.0.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.64"/></proof>
</goal>
</transf>
</goal>
- </transf>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.73" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.73.0" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.73.0.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.134.0.8" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.52"/></proof>
</goal>
- <goal name="inter'vc.73.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.134.0.9" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.41"/></proof>
</goal>
- <goal name="inter'vc.73.0.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.0.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.11" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.13"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.12" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.0.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.54"/></proof>
+ <goal name="inter'vc.134.0.12.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.84"/></proof>
+ </goal>
+ <goal name="inter'vc.134.0.12.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.94"/></proof>
</goal>
- <goal name="inter'vc.73.0.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.44"/></proof>
+ <goal name="inter'vc.134.0.12.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
- <goal name="inter'vc.73.0.3.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.12.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.42"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.0.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.92"/></proof>
- </goal>
- <goal name="inter'vc.73.0.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.73.0.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.64"/></proof>
- </goal>
- <goal name="inter'vc.73.0.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.97"/></proof>
- </goal>
- <goal name="inter'vc.73.0.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.73.0.9" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.73.0.9.0" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.134.0.13" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.0.13.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="6.93"/></proof>
</goal>
- <goal name="inter'vc.73.0.9.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.0.13.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.20"/></proof>
</goal>
- <goal name="inter'vc.73.0.9.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <goal name="inter'vc.134.0.13.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.1.0" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.1.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.1.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.1.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.47"/></proof>
+ <goal name="inter'vc.134.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.64"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.09"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.5" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.1.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.46"/></proof>
+ <goal name="inter'vc.134.1.5.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
- <goal name="inter'vc.73.1.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.16"/></proof>
+ <goal name="inter'vc.134.1.5.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.56"/></proof>
</goal>
- <goal name="inter'vc.73.1.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
+ <goal name="inter'vc.134.1.5.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.55"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.5.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.1.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.59"/></proof>
- </goal>
- <goal name="inter'vc.73.1.5" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.6" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.1.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.29"/></proof>
+ <goal name="inter'vc.134.1.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.1.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.41"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.134.1.8" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="inter'vc.73.1.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.63"/></proof>
+ <goal name="inter'vc.134.1.9" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.81"/></proof>
</goal>
- <goal name="inter'vc.73.1.8" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.1.9" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.11" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.1.11.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.96"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.11.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.38"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.11.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.16"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.134.1.12" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.1.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.31"/></proof>
+ <goal name="inter'vc.134.1.12.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.12.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.63"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.12.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.52"/></proof>
+ </goal>
+ <goal name="inter'vc.134.1.12.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.134.1.13" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.1.13.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.22"/></proof>
</goal>
- <goal name="inter'vc.73.1.9.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.1.13.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.19"/></proof>
</goal>
- <goal name="inter'vc.73.1.9.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <goal name="inter'vc.134.1.13.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.2.0" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.73.2.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.2.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.134.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.73"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
- <goal name="inter'vc.73.2.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.5" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.2.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.46"/></proof>
+ <goal name="inter'vc.134.2.5.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
</goal>
- <goal name="inter'vc.73.2.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
+ <goal name="inter'vc.134.2.5.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.57"/></proof>
</goal>
- <goal name="inter'vc.73.2.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.30"/></proof>
+ <goal name="inter'vc.134.2.5.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.5.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.73.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.62"/></proof>
- </goal>
- <goal name="inter'vc.73.2.5" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.6" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.2.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <goal name="inter'vc.134.2.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.2.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.73.2.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.63"/></proof>
+ <goal name="inter'vc.134.2.8" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.13"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.9" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.2.9.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.15"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.9.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.56"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.9.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.41"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.73.2.8" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.73.2.9" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.11" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.05"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.12" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.73.2.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.78"/></proof>
+ <goal name="inter'vc.134.2.12.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
- <goal name="inter'vc.73.2.9.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
+ <goal name="inter'vc.134.2.12.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.34"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.12.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.56"/></proof>
</goal>
- <goal name="inter'vc.73.2.9.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.134.2.12.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.134.2.13" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.134.2.13.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.82"/></proof>
+ </goal>
+ <goal name="inter'vc.134.2.13.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.23"/></proof>
</goal>
+ <goal name="inter'vc.134.2.13.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
+ </goal>
</transf>
</goal>
</transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.74" expl="postcondition" proved="true">
+ <goal name="inter'vc.135" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.74.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.135.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.74.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.74.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.74.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.07"/></proof>
+ <goal name="inter'vc.135.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.08"/></proof>
</goal>
- <goal name="inter'vc.74.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.03"/></proof>
+ <goal name="inter'vc.135.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.63"/></proof>
</goal>
- <goal name="inter'vc.74.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.135.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.21"/></proof>
</goal>
- <goal name="inter'vc.74.6" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.6" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.74.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.98"/></proof>
- </goal>
- <goal name="inter'vc.74.8" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.135.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.74.9" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.17"/></proof>
+ <goal name="inter'vc.135.8" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
- </transf>
- </goal>
- <goal name="inter'vc.75" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.75.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.135.9" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.62"/></proof>
</goal>
- <goal name="inter'vc.75.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.75.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.75.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.11" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.75.3.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <goal name="inter'vc.135.11.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
- <goal name="inter'vc.75.3.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
+ <goal name="inter'vc.135.11.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.80"/></proof>
</goal>
- <goal name="inter'vc.75.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.20"/></proof>
+ <goal name="inter'vc.135.11.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.75.4" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.12" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
- <goal name="inter'vc.75.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.17"/></proof>
+ <goal name="inter'vc.135.12.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
- <goal name="inter'vc.75.4.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.27"/></proof>
+ <goal name="inter'vc.135.12.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.13"/></proof>
</goal>
- <goal name="inter'vc.75.4.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
+ <goal name="inter'vc.135.12.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
- <goal name="inter'vc.75.4.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.12.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.75.5" expl="postcondition" proved="true">
+ <goal name="inter'vc.135.13" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.13"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.136" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.136.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.75.6" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.136.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.75.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.06"/></proof>
+ <goal name="inter'vc.136.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.136.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.20"/></proof>
+ </goal>
+ <goal name="inter'vc.136.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.19"/></proof>
+ </goal>
+ <goal name="inter'vc.136.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.35"/></proof>
+ </goal>
+ <goal name="inter'vc.136.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="inter'vc.136.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.75.8" expl="postcondition" proved="true">
+ <goal name="inter'vc.136.8" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.62"/></proof>
+ </goal>
+ <goal name="inter'vc.136.9" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.66"/></proof>
+ </goal>
+ <goal name="inter'vc.136.10" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.75.9" expl="postcondition" proved="true">
- <transf name="split_vc" proved="true" >
- <goal name="inter'vc.75.9.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.29"/></proof>
- </goal>
- <goal name="inter'vc.75.9.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.19"/></proof>
- </goal>
- <goal name="inter'vc.75.9.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.18"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.136.11" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.23"/></proof>
+ </goal>
+ <goal name="inter'vc.136.12" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.16"/></proof>
+ </goal>
+ <goal name="inter'vc.136.13" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.31"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.76" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.137" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
- <goal name="inter'vc.77" expl="precondition" proved="true">
+ <goal name="inter'vc.138" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.78" expl="precondition" proved="true">
- <transf name="unfold" proved="true" arg1="ordered">
- <goal name="inter'vc.78.0" expl="VC for inter" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- </transf>
+ <goal name="inter'vc.139" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.79" expl="precondition" proved="true">
+ <goal name="inter'vc.140" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.80" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.141" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
</goal>
- <goal name="inter'vc.81" expl="precondition" proved="true">
+ <goal name="inter'vc.142" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.82" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.26"/></proof>
+ <goal name="inter'vc.143" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.83" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.144" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
+ </goal>
+ <goal name="inter'vc.145" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.84" expl="precondition" proved="true">
+ <goal name="inter'vc.146" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.85" expl="precondition" proved="true">
+ <goal name="inter'vc.147" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.86" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.28"/></proof>
+ <goal name="inter'vc.148" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.22"/></proof>
</goal>
- <goal name="inter'vc.87" expl="precondition" proved="true">
+ <goal name="inter'vc.149" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.88" expl="precondition" proved="true">
+ <goal name="inter'vc.150" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.89" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.90" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.23"/></proof>
+ <goal name="inter'vc.151" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.91" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.152" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.21"/></proof>
</goal>
- <goal name="inter'vc.92" expl="unreachable point" proved="true">
+ <goal name="inter'vc.153" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.93" expl="assertion" proved="true">
+ <goal name="inter'vc.154" expl="unreachable point" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.94" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.155" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.95" expl="precondition" proved="true">
+ <goal name="inter'vc.156" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.96" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.157" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.97" expl="precondition" proved="true">
+ <goal name="inter'vc.158" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.98" expl="precondition" proved="true">
+ <goal name="inter'vc.159" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.99" expl="precondition" proved="true">
+ <goal name="inter'vc.160" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.100" expl="precondition" proved="true">
+ <goal name="inter'vc.161" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.101" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- <goal name="inter'vc.102" expl="precondition" proved="true">
+ <goal name="inter'vc.162" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.103" expl="precondition" proved="true">
+ <goal name="inter'vc.163" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.104" expl="precondition" proved="true">
+ <goal name="inter'vc.164" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.105" expl="precondition" proved="true">
+ <goal name="inter'vc.165" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.106" expl="precondition" proved="true">
+ <goal name="inter'vc.166" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.107" expl="unreachable point" proved="true">
+ <goal name="inter'vc.167" expl="unreachable point" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.108" expl="assertion" proved="true">
+ <goal name="inter'vc.168" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.109" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.169" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.110" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
+ <goal name="inter'vc.170" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.111" expl="precondition" proved="true">
+ <goal name="inter'vc.171" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.112" expl="precondition" proved="true">
+ <goal name="inter'vc.172" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.113" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
- </goal>
- <goal name="inter'vc.114" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.173" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.115" expl="precondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.174" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
- <goal name="inter'vc.116" expl="precondition" proved="true">
+ <goal name="inter'vc.175" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.117" expl="precondition" proved="true">
- <transf name="unfold" proved="true" arg1="ordered0">
- <goal name="inter'vc.117.0" expl="VC for inter" proved="true">
- <proof prover="3"><result status="valid" time="0.02"/></proof>
- </goal>
- </transf>
- </goal>
- <goal name="inter'vc.118" expl="precondition" proved="true">
+ <goal name="inter'vc.176" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.119" expl="precondition" proved="true">
+ <goal name="inter'vc.177" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.120.0" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.120.0.0" expl="postcondition" proved="true">
+ <goal name="inter'vc.178" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.0.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.178.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
</goal>
- <goal name="inter'vc.120.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.01"/></proof>
+ <goal name="inter'vc.178.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.120.0.3" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.06"/></proof>
+ <goal name="inter'vc.178.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.0.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.0.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.0.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.51"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.99"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.37"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.4.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.0.4.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.82"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.4.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.12"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.4.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.40"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.0.4.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.55"/></proof>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.120.0.5" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.178.0.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.0.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.0.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
- <goal name="inter'vc.120.0.7" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.0.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.0.7.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.49"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.7.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.01"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.7.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.28"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.7.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.0.7.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.81"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.7.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.11"/></proof>
+ </goal>
+ <goal name="inter'vc.178.0.7.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.40"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.0.7.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.46"/></proof>
+ </goal>
+ </transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.120.1" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.120.1.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
+ <goal name="inter'vc.178.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.1.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.1.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.1.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.1.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.1.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.1.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="3.09"/></proof>
</goal>
- <goal name="inter'vc.120.1.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.1.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.4.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.4.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.66"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.77"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.1.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.19"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.4.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.65"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.89"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.55"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.1.4.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.4.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.05"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.48"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.1.4.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.4.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.91"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.23"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.4.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.74"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
- <goal name="inter'vc.120.1.5" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.1.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.1.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.1.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.19"/></proof>
</goal>
- <goal name="inter'vc.120.1.7" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.1.7" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.7.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.7.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.67"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.92"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.1.7.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.30"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.7.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.62"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.87"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.55"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.1.7.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.7.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.00"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.3.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.43"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.3.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.48"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="inter'vc.178.1.7.4" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.1.7.4.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.93"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.4.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.28"/></proof>
+ </goal>
+ <goal name="inter'vc.178.1.7.4.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.73"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
</goal>
</transf>
</goal>
- <goal name="inter'vc.120.2" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.120.2.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.00"/></proof>
- </goal>
- <goal name="inter'vc.120.2.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.2.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.2.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="inter'vc.178.2.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.2.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.2.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="1.84"/></proof>
</goal>
- <goal name="inter'vc.120.2.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.2.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.47"/></proof>
</goal>
- <goal name="inter'vc.120.2.5" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.2.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.2.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.2.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.17"/></proof>
</goal>
- <goal name="inter'vc.120.2.7" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.2.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.30"/></proof>
</goal>
</transf>
</goal>
- <goal name="inter'vc.120.3" expl="postcondition">
- <proof prover="3" obsolete="true"><result status="timeout" time="5.00"/></proof>
- <transf name="split_vc" >
- <goal name="inter'vc.120.3.0" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.3" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="inter'vc.178.3.0" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.3.1" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.3.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.3.2" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.3.2" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
- <goal name="inter'vc.120.3.3" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.3.3" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="1.54"/></proof>
</goal>
- <goal name="inter'vc.120.3.4" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.3.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.28"/></proof>
</goal>
- <goal name="inter'vc.120.3.5" expl="postcondition" proved="true">
+ <goal name="inter'vc.178.3.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
- <goal name="inter'vc.120.3.6" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.3.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
</goal>
- <goal name="inter'vc.120.3.7" expl="postcondition">
- <proof prover="3"><result status="timeout" time="5.00"/></proof>
+ <goal name="inter'vc.178.3.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.36"/></proof>
</goal>
</transf>
</goal>
diff --git a/src_common/union__Union.ml b/src_common/union__Union.ml
new file mode 100644
index 0000000000000000000000000000000000000000..2c9dcd2a9caa1b13e441c4c710008e039098ed0b
--- /dev/null
+++ b/src_common/union__Union.ml
@@ -0,0 +1,237 @@
+type t0 =
+ | Singleton of (Q.t) * t0
+ | Inter of (Q.t) * Interval__Bound.t * (Q.t) * Interval__Bound.t * t0
+ | FiniteInf of (Q.t) * Interval__Bound.t
+ | End
+
+type t =
+ | InfFinite of (Q.t) * Interval__Bound.t * t0
+ | Finite of t0
+ | Inf
+
+type t' = t
+
+let singleton (q: Q.t) : t' = Finite (Singleton (q, End))
+
+let is_singleton (u: t') : (Q.t) option =
+ match u with
+ | Inf -> None
+ | InfFinite (q, _, _) -> None
+ | Finite Singleton (q, End) -> Some q
+ | Finite End -> assert false (* absurd *)
+ | Finite Inter (q, _, q', _, _) -> None
+ | Finite FiniteInf (q, _) -> None
+ | Finite Singleton (q, Singleton (q', _)) -> None
+ | Finite Singleton (_, Inter (q, _, q', _, _)) -> None
+ | Finite Singleton (_, FiniteInf (q, _)) -> None
+
+let min_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ (v1, Interval__Bound.Large)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Strict)
+ | (Ord.Lt, _, _) -> (v1, b1)
+ | (Ord.Gt, _, _) -> (v2, b2)
+
+let min_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ (v1, Interval__Bound.Strict)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Large)
+ | (Ord.Lt, _, _) -> (v1, b1)
+ | (Ord.Gt, _, _) -> (v2, b2)
+
+let max_bound_sup (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ (v1, Interval__Bound.Strict)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Large)
+ | (Ord.Lt, _, _) -> (v2, b2)
+ | (Ord.Gt, _, _) -> (v1, b1)
+
+let max_bound_inf (v1: Q.t) (b1: Interval__Bound.t) (v2: Q.t)
+ (b2: Interval__Bound.t) : (Q.t) * Interval__Bound.t =
+ match ((Q_extra.compare v1 v2), b1, b2) with
+ | (Ord.Eq,
+ Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ (v1, Interval__Bound.Large)
+ | (Ord.Eq, _, _) -> (v1, Interval__Bound.Strict)
+ | (Ord.Lt, _, _) -> (v2, b2)
+ | (Ord.Gt, _, _) -> (v1, b1)
+
+let inter (u: t') (v: t') : t' option =
+ let rec aux (u1: t0) (v1: t0) : t0 =
+ match (u1, v1) with
+ | ((End, _) | (_, End)) -> End
+ | (Singleton (qu,
+ lu),
+ Singleton (qv,
+ lv)) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Eq -> Singleton (qu, aux lu lv)
+ | Ord.Lt -> aux lu v1
+ | Ord.Gt -> aux u1 lv
+ end
+ | (FiniteInf (q,
+ b),
+ FiniteInf (q',
+ b')) ->
+ (let (q'', b'') = max_bound_inf q b q' b' in FiniteInf (q'', b''))
+ | (((Singleton (qu, lu) as u2),
+ (FiniteInf (qv, bv) as v2)) | ((FiniteInf (qv, bv) as v2),
+ (Singleton (qu, lu) as u2))) ->
+ begin match (Q_extra.compare qu qv) with
+ | Ord.Lt -> aux lu v2
+ | Ord.Gt -> u2
+ | Ord.Eq ->
+ begin match bv with
+ | Interval__Bound.Large -> u2
+ | Interval__Bound.Strict -> lu
+ end
+ end
+ | (((FiniteInf (q, b) as u3),
+ (Inter (qv0, bv0, qv1, bv1, lv) as v3)) | ((Inter (qv0, bv0, qv1, bv1,
+ lv) as v3),
+ (FiniteInf (q, b) as u3))) ->
+ begin match (Q_extra.compare q qv0) with
+ | Ord.Lt -> v3
+ | Ord.Gt ->
+ begin match (Q_extra.compare q qv1) with
+ | Ord.Lt -> Inter (q, b, qv1, bv1, lv)
+ | Ord.Gt -> aux u3 lv
+ | Ord.Eq ->
+ begin match (b, bv1) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ Singleton (q, lv)
+ | _ -> lv
+ end
+ end
+ | Ord.Eq ->
+ begin match (b, bv0) with
+ | (Interval__Bound.Strict,
+ Interval__Bound.Large) ->
+ Inter (qv0, b, qv1, bv1, lv)
+ | _ -> v3
+ end
+ end
+ | (((Singleton (qu, lu) as u4),
+ (Inter (qv0, bv0, qv1, bv1, lv) as v4)) | ((Inter (qv0, bv0, qv1, bv1,
+ lv) as v4),
+ (Singleton (qu, lu) as u4))) ->
+ begin match (Q_extra.compare qu qv0) with
+ | Ord.Lt -> aux lu v4
+ | Ord.Gt ->
+ begin match (Q_extra.compare qu qv1) with
+ | Ord.Lt -> Singleton (qu, aux lu v4)
+ | Ord.Gt -> aux u4 lv
+ | Ord.Eq ->
+ begin match bv1 with
+ | Interval__Bound.Large -> Singleton (qu, aux lu lv)
+ | _ -> aux lu lv
+ end
+ end
+ | Ord.Eq ->
+ begin match bv0 with
+ | Interval__Bound.Large -> Singleton (qu, aux lu v4)
+ | _ -> aux lu v4
+ end
+ end
+ | (Inter (qu0,
+ bu0,
+ qu1,
+ bu1,
+ lu),
+ Inter (qv0,
+ bv0,
+ qv1,
+ bv1,
+ lv)) ->
+ (let v' = v1 in let u' = u1 in
+ let small_big (qu01: Q.t) (bu01: Interval__Bound.t) (qu11: Q.t)
+ (bu11: Interval__Bound.t) (lu1: t0) (u5: t0) (qv01: Q.t)
+ (bv01: Interval__Bound.t) (qv11: Q.t)
+ (bv11: Interval__Bound.t) (lv1: t0) (v5: t0) : t0 =
+ match (Q_extra.compare qu11 qv01) with
+ | Ord.Eq ->
+ begin match (bu11, bv01) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ Singleton (qu11, aux lu1 v5)
+ | _ -> aux lu1 v5
+ end
+ | Ord.Lt -> aux lu1 v5
+ | Ord.Gt ->
+ (let (qw0, bw0) = max_bound_inf qu01 bu01 qv01 bv01 in
+ Inter (qw0, bw0, qu11, bu11, aux lu1 v5)) in
+ match (Q_extra.compare qu1 qv1) with
+ | Ord.Eq ->
+ (let (qw01, bw01) = max_bound_inf qu0 bu0 qv0 bv0 in
+ let b =
+ match (bu1, bv1) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ Interval__Bound.Large
+ | _ -> Interval__Bound.Strict in
+ Inter (qw01, bw01, qv1, b, aux lu lv))
+ | Ord.Lt -> small_big qu0 bu0 qu1 bu1 lu u1 qv0 bv0 qv1 bv1 lv v1
+ | Ord.Gt -> small_big qv0 bv0 qv1 bv1 lv v1 qu0 bu0 qu1 bu1 lu u1) in
+ let aux_option (lu: t0) (lv: t0) : t' option =
+ match aux lu lv with
+ | End -> None
+ | lw -> Some (Finite lw) in
+ match (u, v) with
+ | (Inf, _) -> Some v
+ | (_, Inf) -> Some u
+ | (InfFinite (qu1,
+ bu1,
+ lu),
+ InfFinite (qv1,
+ bv1,
+ lv)) ->
+ begin match (Q_extra.compare qu1 qv1) with
+ | Ord.Eq ->
+ (let b =
+ match (bu1, bv1) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ Interval__Bound.Large
+ | _ -> Interval__Bound.Strict in
+ Some (InfFinite (qu1, b, aux lu lv)))
+ | Ord.Lt ->
+ Some (InfFinite (qu1, bu1,
+ aux lu (Inter (qu1, Interval__Bound.Strict, qv1, bv1, lv))))
+ | Ord.Gt ->
+ Some (InfFinite (qv1, bv1,
+ aux (Inter (qv1, Interval__Bound.Strict, qu1, bu1, lu)) lv))
+ end
+ | (Finite lu, Finite lv) -> aux_option lu lv
+ | ((Finite lu, InfFinite (qv1, bv1, lv)) | (InfFinite (qv1, bv1, lv),
+ Finite lu)) ->
+ (let (qu0, bu0) =
+ match lu with
+ | End -> assert false (* absurd *)
+ | Singleton (qu01, _) -> (qu01, Interval__Bound.Large)
+ | Inter (qu01, bu01, _, _, _) -> (qu01, bu01)
+ | FiniteInf (qu01, bu01) -> (qu01, bu01) in
+ match (Q_extra.compare qu0 qv1) with
+ | Ord.Eq ->
+ begin match (bu0, bv1) with
+ | (Interval__Bound.Large,
+ Interval__Bound.Large) ->
+ aux_option lu (Singleton (qv1, lv))
+ | _ -> aux_option lu lv
+ end
+ | Ord.Lt -> aux_option lu (Inter (qu0, bu0, qv1, bv1, lv))
+ | Ord.Gt -> aux_option lu lv)
+