From 08afcef790c2acad28d14a98449284c24fa21380 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Wed, 27 Oct 2021 16:41:19 +0200
Subject: [PATCH] Add interval first part
---
src_common/union.mlw | 343 +++++++++-
src_common/union/why3session.xml | 1037 ++++++++++++++++++++++++++++--
src_common/union__Union.ml | 103 +++
3 files changed, 1433 insertions(+), 50 deletions(-)
diff --git a/src_common/union.mlw b/src_common/union.mlw
index 91fe01cb8..ffe76f841 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -64,7 +64,7 @@ module Union
length_off l
end
- predicate lt_bound_on (x:Q.t) (l:on) =
+ predicate lt_bound_on (x:real) (l:on) =
match l with
| OnSin q l ->
x <. q /\ lt_bound_on x l
@@ -73,7 +73,7 @@ module Union
| OnInf -> true
end
- with lt_bound_off (x:Q.t) (l:off) =
+ with lt_bound_off (x:real) (l:off) =
match l with
| OffSin q l ->
x <. q /\ lt_bound_off x l
@@ -781,5 +781,344 @@ module Union
end
+ let add_cst l x
+ ensures {
+ forall q. (mem q l.a) <-> mem (q+.x) result.a
+ }
+ =
+ let rec add_cst_on (x:Q.t) (l:on) : on
+ requires { ordered_on l }
+ ensures { ordered_on result }
+ ensures { forall q. (lt_bound_on q l) -> (lt_bound_on (q+.x) result) }
+ ensures { forall q. (mem_on q l) <-> mem_on (q+.x) result }
+ variant { length_on l }
+ =
+ match l with
+ | OnSin q l' -> OnSin Q.(q+x) (add_cst_on x l')
+ | OnEnd q bv l' ->
+ lt_bound_is_not_mem_off q l';
+ OnEnd Q.(q+x) bv (add_cst_off x l')
+ | OnInf -> OnInf
+ end
+
+ with add_cst_off (x:Q.t) (l:off)
+ requires { ordered_off l }
+ ensures { ordered_off result }
+ ensures { forall q. (lt_bound_off q l) -> (lt_bound_off (q+.x) result) }
+ ensures { forall q. (mem_off q l) <-> mem_off (q+.x) result }
+ variant { length_off l }
+ =
+ match l with
+ | OffSin q l' ->
+ lt_bound_is_not_mem_off q l';
+ OffSin Q.(q+x) (add_cst_off x l')
+ | OffEnd q b l' -> OffEnd Q.(q+x) b (add_cst_on x l')
+ | OffInf -> OffInf
+ end
+ in
+ match l.a with
+ | On l ->
+ { a = On (add_cst_on x l) }
+ | Off l_off ->
+ let v = not_bottom l in
+ let l = (add_cst_off x l_off) in
+ assert { mem_off (v+.x) l };
+ { a = Off l }
+ end
+
+ let function add_bound b1 b2 =
+ match b1, b2 with
+ | Large, Large -> Large
+ | Large, Strict -> Strict
+ | Strict, Large -> Strict
+ | Strict, Strict -> Strict
+ end
+
+ let ghost function lt_bound_on_give_space (q:real) (l:on) : real
+ requires { lt_bound_on q l }
+ ensures { q <. result }
+ ensures { forall q'. q' <. result -> mem_on q' l } =
+ match l with
+ | OnSin q _ -> Q.real q
+ | OnEnd q _ _ -> Q.real q
+ | OnInf -> q +. 1.0
+ end
+
+ use real.MinMax
+
+ let add_interval l (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t): (result:t',ghost fq':real -> real)
+ requires { Q.(u < v) }
+ ensures {
+ forall q q'. (mem q l.a /\ cmp u bu q' /\ cmp q' bv v) -> mem (q+.q') result.a
+ }
+ ensures {
+ forall q. mem q result.a -> (mem (fq' q) l.a /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v)
+ }
+ =
+ let rec add_interval_on (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t) (l:on) : (result:on,ghost fq':real -> real)
+ requires { Q.(u < v) }
+ requires { ordered_on l }
+ ensures { ordered_on result }
+ ensures { forall q. (lt_bound_on q l) -> (lt_bound_on (q+.u) result) }
+ ensures { forall q q'. (mem_on q l /\ cmp u bu q' /\ cmp q' bv v) -> mem_on (q+.q') result }
+ ensures { forall q. mem_on q result -> (mem_on (fq' q) l /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v) }
+ variant { length_on l }
+ =
+ match l with
+ | OnSin qs l' ->
+ assert { forall q'. mem_on q' l -> mem_on q' l'};
+ let res,fq' = add_interval_on bu u v bv l' in
+ let ghost space_right = lt_bound_on_give_space (Q.real qs) l' in
+ let ghost fq'' (q:real)
+ ensures { mem_on q res -> (mem_on result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
+ =
+ let q' = fq' q in
+ if pure { q' = Q.real qs } then
+ if pure { (q-.q') = v } then
+ if pure { (space_right-.qs) <. (v-.u) } then
+ pure { qs +. ((space_right-.qs)*.0.5) }
+ else
+ pure {qs +. ((v-.u) *.0.5) }
+ else
+ pure { q' -. (v -. (q-.q'))*.0.5 }
+ else q'
+ in
+ (res,fq'')
+ | OnEnd qs bq l' ->
+ lt_bound_is_not_mem_off qs l';
+ let br = add_bound bq bv in
+ let r = Q.(qs+v) in
+ let res, fq = add_interval_off_remain bu u v bv r br l' in
+ let ghost fq' (q:real) : real
+ ensures { mem_on q res -> (mem_on result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
+ =
+ if pure { cmp q br r }
+ then if pure { q = qs+.v } then Q.real qs
+ else if pure { q <. qs+.v*.0.5+.u*.0.5 } then pure { q -. (v*.0.5+.u*.0.5)} else let d = Q.real qs+.Q.real v-.q in Q.real qs -. d*.0.5
+ else fq q
+ in
+ res, fq'
+ | OnInf -> (OnInf,ghost fun q -> q-.Q.real u*.0.5-.Q.real v*.0.5)
+ end
+
+ with add_interval_off (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t) (l:off) : (result:off,ghost fq':real -> real)
+ requires { Q.(u < v) }
+ requires { ordered_off l }
+ ensures { ordered_off result }
+ ensures { forall q. (lt_bound_off q l) -> (lt_bound_off (q+.u) result) }
+ ensures { forall q q'. (mem_off q l /\ cmp u bu q' /\ cmp q' bv v) -> mem_off (q+.q') result }
+ ensures { forall q. mem_off q result -> (mem_off (fq' q) l /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v) }
+ variant { length_off l }
+ =
+ match l with
+ | OffSin qs l' ->
+ lt_bound_is_not_mem_off qs l';
+ let r = Q.(qs+v) in
+ let res, fq = (add_interval_off_remain bu u v bv r bv l') in
+ let res = OffEnd Q.(qs+u) bu res in
+ let ghost function fq' (q:real) : real
+ ensures { mem_off q res -> (mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
+ =
+ if pure { cmp q bv r }
+ then pure { Q.real qs }
+ else fq q
+ in
+ res, fq'
+ | OffEnd qs b l' ->
+ let bbu = add_bound b bu in
+ let ghost space_right = lt_bound_on_give_space (Q.real qs) l' in
+ let res0, fq = (add_interval_on bu u v bv l') in
+ let res = OffEnd Q.(qs+u) bbu res0 in
+ let ghost function fq' (q:real) : real
+ ensures { mem_off q res -> (mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v) }
+ =
+ if pure { cmp qs b (fq q) } then fq q else begin
+ if pure { q = (qs+.u) } then Q.real qs
+ else
+ let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
+ if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
+ end
+ in
+ res, fq'
+ | OffInf -> OffInf, (ghost fun _ -> 0.)
+ end
+
+ with add_interval_off_remain (bu:Bound.t) (u:Q.t) (v:Q.t) (bv:Bound.t) (r:Q.t) (br:Bound.t) (l:off) : (result:on,ghost fq':real -> real)
+ requires { Q.(u < v) }
+ requires { lt_bound_off (r-.v) l }
+ requires { br = Large -> bv = Large }
+ requires { ordered_off l }
+ ensures { ordered_on result }
+ ensures { forall q. (lt_bound_off q l) -> (q+.u <. r) -> (lt_bound_on (q+.u) result) }
+ ensures { forall q q'. (mem_off q l /\ cmp u bu q' /\ cmp q' bv v) -> mem_on (q+.q') result }
+ ensures { forall q. cmp q br r -> mem_on q result }
+ ensures { forall q. mem_on q result ->
+ ((mem_off (fq' q) l /\ cmp u bu (q-.(fq' q)) /\ cmp (q-.(fq' q)) bv v)
+ \/ cmp q br r) }
+ variant { length_off l }
+ =
+ match l with
+ | OffSin qs l' ->
+ lt_bound_is_not_mem_off qs l';
+ let qu = Q.(qs+u) in
+ match Q.compare r qu with
+ | Ord.Lt ->
+ smaller_lt_bound_off Q.(r-u) qs l';
+ let r' = Q.(qs+v) in
+ let res, fq = (add_interval_off_remain bu u v bv r' bv l') in
+ let res = OnEnd r br (OffEnd qu bu res) in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp q bv r' } then Q.real qs else (fq q)
+ else 0.
+ in
+ res, fq'
+ | Ord.Gt ->
+ let r' = Q.(qs+v) in
+ let res, fq = add_interval_off_remain bu u v bv r' bv l' in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp q bv r' } then Q.real qs else (fq q)
+ else 0.
+ in
+ res, fq'
+ | Ord.Eq ->
+ match br, bu with
+ | Strict, Strict ->
+ let r' = Q.(qs+v) in
+ let res, fq = (add_interval_off_remain bu u v bv r' bv l') in
+ let res = OnSin qu res in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp q bv r' } then Q.real qs else (fq q)
+ else 0.
+ in
+ res, fq'
+ | _ ->
+ let r' = Q.(qs+v) in
+ let res, fq = (add_interval_off_remain bu u v bv r' bv l') in
+ let res = res in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp q bv r' } then Q.real qs else (fq q)
+ else 0.
+ in
+ res, fq'
+ end
+ end
+ | OffEnd qs b l' ->
+ let qu = Q.(qs+u) in
+ let bbu = add_bound b bu in
+ let ghost space_right = lt_bound_on_give_space (Q.real qs) l' in
+ match Q.compare r qu with
+ | Ord.Lt ->
+ smaller_lt_bound_on Q.(r-u) qs l';
+ let res, fq = (add_interval_on bu u v bv l') in
+ let res = OnEnd r br (OffEnd qu bbu res) in
+ let ghost fq' (q:real) : real
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp qs b (fq q) } then fq q else begin
+ if pure { q = qu } then Q.real qs
+ else
+ let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
+ if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
+
+ end
+ else 0.
+ in
+ res, fq'
+ | Ord.Gt ->
+ let res, fq = add_interval_on bu u v bv l' in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp qs b (fq q) } then fq q else begin
+ if pure { q = qu } then Q.real qs
+ else
+ let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
+ if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
+
+ end
+ else 0.
+ in
+(* assert { forall mem_on (r-.v) l'};
+ assert { mem_on r res}; *)
+ let ghost p = pure { 0.5 *. min (qs-.(r-.v)) (v-.u) } in
+ assert { forall q. cmp q br r -> cmp (q-.v+.p) b qs };
+ assert { forall q. cmp q br r -> (mem_on (q-.(v-.p)) l' /\ cmp u bu (v-.p) /\ cmp (v-.p) bv v) };
+ assert { forall q. cmp q br r -> mem_on ((q-.(v-.p))+.(v-.p)) res };
+ assert { forall q. cmp q br r -> mem_on q res };
+ res, fq'
+ | Ord.Eq ->
+ match br, bbu with
+ | Strict, Strict ->
+ let res, fq = (add_interval_on bu u v bv l') in
+ let res = OnSin qu res in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp qs b (fq q) } then fq q else begin
+ if pure { q = qu } then Q.real qs
+ else
+ let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
+ if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
+
+ end
+ else 0.
+ in
+ res, fq'
+ | _ ->
+ let res, fq = (add_interval_on bu u v bv l') in
+ let res = res in
+ let ghost fq' (q:real)
+ ensures { mem_on q res -> ((mem_off result l /\ cmp u bu (q-.result) /\ cmp (q-.result) bv v)
+ \/ cmp q br r) }
+ =
+ if pure { cmp qu bu q } then
+ if pure { cmp qs b (fq q) } then fq q else begin
+ if pure { q = qu } then Q.real qs
+ else
+ let p = pure { min (qs*.0.5+.space_right*.0.5) (qs+.(v-.u)) } in
+ if pure { q-.p <=. u } then pure { qs*.0.5+.(q-.u)*.0.5 } else p
+
+ end
+ else 0.
+ in
+ res, fq'
+ end
+ end
+ | OffInf -> OnEnd r br OffInf,(ghost fun _ -> 0.)
+ end
+ in
+ match l.a with
+ | On l ->
+ let res, fq = add_interval_on bu u v bv l in
+ { a = On res }, fq
+ | Off l_off ->
+ let w = not_bottom l in
+ let l, fq = (add_interval_off bu u v bv l_off) in
+ assert { mem_off (w+.(u*.0.5+.v*.0.5)) l };
+ { a = Off l }, fq
+ end
+
end
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index 264b96c40..4dc76d64e 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -80,7 +80,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.4" 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.5" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -95,7 +95,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.9" expl="precondition" 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.10" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -113,7 +113,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.15" 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.16" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -143,7 +143,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.25" 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.26" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -173,7 +173,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="inter'vc.35" 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.36" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -203,7 +203,7 @@
<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.00"/></proof>
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.46" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -297,7 +297,7 @@
<goal name="inter'vc.61.1.4" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="inter'vc.61.1.4.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.07"/></proof>
+ <proof prover="3"><result status="valid" time="1.30"/></proof>
</goal>
<goal name="inter'vc.61.1.4.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.46"/></proof>
@@ -473,7 +473,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="inter'vc.81" 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.82" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -500,7 +500,7 @@
<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.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="inter'vc.91" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -725,12 +725,12 @@
<proof prover="3"><result status="valid" time="0.40"/></proof>
</goal>
<goal name="inter'vc.125.1.3.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.42"/></proof>
+ <proof prover="3"><result status="valid" time="0.64"/></proof>
</goal>
</transf>
</goal>
<goal name="inter'vc.125.1.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.36"/></proof>
+ <proof prover="3"><result status="valid" time="5.46"/></proof>
</goal>
<goal name="inter'vc.125.1.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -784,7 +784,7 @@
<proof prover="3"><result status="valid" time="3.64"/></proof>
</goal>
<goal name="inter'vc.125.2.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.47"/></proof>
+ <proof prover="3"><result status="valid" time="3.19"/></proof>
</goal>
<goal name="inter'vc.125.2.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1105,14 +1105,14 @@
<proof prover="3"><result status="valid" time="0.15"/></proof>
</goal>
<goal name="inter'vc.174.2.6.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.75"/></proof>
+ <proof prover="3"><result status="valid" time="2.10"/></proof>
</goal>
</transf>
</goal>
<goal name="inter'vc.174.2.7" expl="postcondition" proved="true">
<transf name="split_vc" proved="true" >
<goal name="inter'vc.174.2.7.0" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="2.90"/></proof>
+ <proof prover="3"><result status="valid" time="3.30"/></proof>
</goal>
<goal name="inter'vc.174.2.7.1" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.35"/></proof>
@@ -1282,7 +1282,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.9" 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="union'vc.10" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1294,7 +1294,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.13" 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="union'vc.14" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1303,7 +1303,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.16" 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="union'vc.17" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1312,7 +1312,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.19" 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="union'vc.20" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1351,10 +1351,10 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.32" 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="union'vc.33" 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="union'vc.34" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1396,7 +1396,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.47" 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="union'vc.48" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1411,7 +1411,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.52" 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="union'vc.53" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1420,13 +1420,13 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.55" expl="precondition" 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="union'vc.56" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.57" 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="union'vc.58" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1481,12 +1481,12 @@
<proof prover="3"><result status="valid" time="1.41"/></proof>
</goal>
<goal name="union'vc.67.0.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="3.14"/></proof>
+ <proof prover="3"><result status="valid" time="3.61"/></proof>
</goal>
</transf>
</goal>
<goal name="union'vc.67.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.64"/></proof>
+ <proof prover="3"><result status="valid" time="1.95"/></proof>
</goal>
</transf>
</goal>
@@ -1509,7 +1509,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.74" 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="union'vc.75" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1524,7 +1524,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.79" 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="union'vc.80" expl="assertion" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1566,7 +1566,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.93" 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="union'vc.94" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1578,7 +1578,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union'vc.97" expl="precondition" 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="union'vc.98" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1791,7 +1791,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.133" 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="union'vc.134" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1806,7 +1806,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union'vc.138" 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="union'vc.139" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1821,7 +1821,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union'vc.143" 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="union'vc.144" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1833,13 +1833,13 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.147" 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="union'vc.148" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.149" 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="union'vc.150" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1869,7 +1869,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.159" expl="precondition" 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="union'vc.160" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1893,7 +1893,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.167" 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="union'vc.168" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -1926,7 +1926,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.178" 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="union'vc.179" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1941,7 +1941,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="union'vc.183" expl="precondition" 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="union'vc.184" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -1956,7 +1956,7 @@
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="union'vc.188" expl="precondition" 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="union'vc.189" expl="variant decrease" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
@@ -2022,7 +2022,7 @@
<proof prover="3"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="union'vc.193.0.4" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.85"/></proof>
+ <proof prover="3"><result status="valid" time="6.10"/></proof>
</goal>
<goal name="union'vc.193.0.5" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -2031,7 +2031,7 @@
<proof prover="3"><result status="valid" time="3.44"/></proof>
</goal>
<goal name="union'vc.193.0.7" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.72"/></proof>
+ <proof prover="3"><result status="valid" time="5.83"/></proof>
</goal>
</transf>
</goal>
@@ -2063,10 +2063,10 @@
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="union'vc.193.1.6.0.1" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.92"/></proof>
+ <proof prover="3"><result status="valid" time="2.60"/></proof>
</goal>
<goal name="union'vc.193.1.6.0.2" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="4.51"/></proof>
+ <proof prover="3"><result status="valid" time="5.94"/></proof>
</goal>
</transf>
</goal>
@@ -2145,7 +2145,7 @@
</transf>
</goal>
<goal name="mem'vc" expl="VC for mem" proved="true">
- <proof prover="3"><result status="valid" time="0.47"/></proof>
+ <proof prover="3"><result status="valid" time="0.69"/></proof>
</goal>
<goal name="except'vc" expl="VC for except" proved="true">
<transf name="split_vc" proved="true" >
@@ -2183,7 +2183,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="except'vc.11" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="1.11"/></proof>
+ <proof prover="3"><result status="valid" time="1.73"/></proof>
</goal>
<goal name="except'vc.12" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -2207,7 +2207,7 @@
<proof prover="3"><result status="valid" time="0.05"/></proof>
</goal>
<goal name="except'vc.19" expl="postcondition" proved="true">
- <proof prover="3"><result status="valid" time="0.64"/></proof>
+ <proof prover="3"><result status="valid" time="0.88"/></proof>
</goal>
<goal name="except'vc.20" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.00"/></proof>
@@ -2222,7 +2222,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="except'vc.24" expl="assertion" proved="true">
- <proof prover="3"><result status="valid" time="0.40"/></proof>
+ <proof prover="3"><result status="valid" time="0.55"/></proof>
</goal>
<goal name="except'vc.25" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
@@ -2235,6 +2235,947 @@
</goal>
</transf>
</goal>
+ <goal name="add_cst'vc" expl="VC for add_cst" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_cst'vc.0" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.1" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_cst'vc.2" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.3" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_cst'vc.4" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.5" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_cst'vc.6" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_cst'vc.7" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.26"/></proof>
+ </goal>
+ <goal name="add_cst'vc.8" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_cst'vc.9" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.10" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.11" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_cst'vc.12" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_cst'vc.13" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_cst'vc.14" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_cst'vc.15" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.24"/></proof>
+ </goal>
+ <goal name="add_cst'vc.16" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.17" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.18" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.19" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_cst'vc.20" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_cst'vc.21" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_cst'vc.22" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_cst'vc.23" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="lt_bound_on_give_space'vc" expl="VC for lt_bound_on_give_space" proved="true">
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="add_interval'vc" expl="VC for add_interval" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.0" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.27"/></proof>
+ </goal>
+ <goal name="add_interval'vc.1" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_interval'vc.2" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.3" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.4" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.5.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.5.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.83"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.43"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.5.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.83"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.5.2.0" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="add_interval'vc.5.2.0.0" expl="postcondition" proved="true">
+ <transf name="subst_all" proved="true" >
+ <goal name="add_interval'vc.5.2.0.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ <transf name="subst_all" proved="true" >
+ <goal name="add_interval'vc.5.2.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.5.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.19"/></proof>
+ </goal>
+ <goal name="add_interval'vc.5.2.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.56"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.6" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_interval'vc.7" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.8" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.9" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.10" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.11" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.12" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.90"/></proof>
+ </goal>
+ <goal name="add_interval'vc.13" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.14" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.15" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.15.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.15.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.15.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.22"/></proof>
+ </goal>
+ <goal name="add_interval'vc.15.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.15.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.16" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.16.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.16.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.81"/></proof>
+ </goal>
+ <goal name="add_interval'vc.16.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.72"/></proof>
+ </goal>
+ <goal name="add_interval'vc.16.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.16.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.16.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.64"/></proof>
+ </goal>
+ <goal name="add_interval'vc.16.1.1" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="add_interval'vc.16.1.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.67"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.16.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.16"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.16.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.16.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.65"/></proof>
+ </goal>
+ <goal name="add_interval'vc.16.2.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.64"/></proof>
+ </goal>
+ <goal name="add_interval'vc.16.2.2" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="add_interval'vc.16.2.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.15"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.17" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.18" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.19" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_interval'vc.20" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.21" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.22" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.23" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.24" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.25" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.26" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.27" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.28" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.28.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.84"/></proof>
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.28.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.79"/></proof>
+ </goal>
+ <goal name="add_interval'vc.28.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.28.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.07"/></proof>
+ </goal>
+ <goal name="add_interval'vc.28.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.28.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.85"/></proof>
+ </goal>
+ <goal name="add_interval'vc.28.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.63"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.29" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.29.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.29.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.29.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.30" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="add_interval'vc.31" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.31.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.93"/></proof>
+ </goal>
+ <goal name="add_interval'vc.31.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="add_interval'vc.31.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.32" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.32.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.32.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.45"/></proof>
+ </goal>
+ <goal name="add_interval'vc.32.0.1" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="add_interval'vc.32.0.1.0" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="H3" arg2="q">
+ <goal name="add_interval'vc.32.0.1.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.32.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.32.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.32.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ <goal name="add_interval'vc.32.1.1" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="add_interval'vc.32.1.1.0" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="H3" arg2="q">
+ <goal name="add_interval'vc.32.1.1.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.32.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.32.2" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.32.2.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.51"/></proof>
+ </goal>
+ <goal name="add_interval'vc.32.2.1" expl="postcondition" proved="true">
+ <transf name="eliminate_let_fmla" proved="true" >
+ <goal name="add_interval'vc.32.2.1.0" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="H3" arg2="q">
+ <goal name="add_interval'vc.32.2.1.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.32.2.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.33" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.34" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.07"/></proof>
+ </goal>
+ <goal name="add_interval'vc.35" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.36" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.37" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.38" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.39" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.40" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.41" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.18"/></proof>
+ </goal>
+ <goal name="add_interval'vc.42" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.43" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.44" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.45" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.46" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.47" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.48" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.49" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_interval'vc.50" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.51" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.52" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.53" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.54" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.55" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.56" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.57" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.58" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.59" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="add_interval'vc.60" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.61" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.62" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.63" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.64" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.65" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.07"/></proof>
+ </goal>
+ <goal name="add_interval'vc.66" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.67" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.68" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.69" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.70" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.71" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.72" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.72.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.10"/></proof>
+ </goal>
+ <goal name="add_interval'vc.72.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="add_interval'vc.72.2" expl="postcondition" proved="true">
+ <transf name="left" proved="true" >
+ <goal name="add_interval'vc.72.2.0" expl="left case" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.72.2.0.0" expl="left case" proved="true">
+ <proof prover="3"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="add_interval'vc.72.2.0.1" expl="left case" proved="true">
+ <proof prover="3"><result status="valid" time="0.12"/></proof>
+ </goal>
+ <goal name="add_interval'vc.72.2.0.2" expl="left case" proved="true">
+ <proof prover="3"><result status="valid" time="0.07"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.72.3" expl="postcondition" proved="true">
+ <transf name="instantiate" proved="true" arg1="Ensures" arg2="q">
+ <goal name="add_interval'vc.72.3.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.47"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.72.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.21"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.73" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.74" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.75" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.76" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.76.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.76.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.76.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="add_interval'vc.76.3" expl="postcondition" proved="true">
+ <proof prover="3" timelimit="100"><result status="valid" time="16.89"/></proof>
+ <transf name="left" proved="true" >
+ <goal name="add_interval'vc.76.3.0" expl="left case" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.76.3.0.0" expl="left case" proved="true">
+ <proof prover="3"><result status="valid" time="0.09"/></proof>
+ </goal>
+ <goal name="add_interval'vc.76.3.0.1" expl="left case" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.76.3.0.2" expl="left case" proved="true">
+ <proof prover="3" timelimit="100"><result status="valid" time="7.19"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.76.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.77" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.78" expl="assertion" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.78.0" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="add_interval'vc.78.1" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.78.2" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.79" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.74"/></proof>
+ </goal>
+ <goal name="add_interval'vc.80" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="0.59"/></proof>
+ </goal>
+ <goal name="add_interval'vc.81" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.82" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.83" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.84" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.84.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.84.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.84.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.14"/></proof>
+ </goal>
+ <goal name="add_interval'vc.84.3" expl="postcondition" proved="true">
+ <proof prover="3" timelimit="100"><result status="valid" time="5.85"/></proof>
+ </goal>
+ <goal name="add_interval'vc.84.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.85" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.86" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.87" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.88" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.88.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.88.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.88.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.88.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.23"/></proof>
+ </goal>
+ <goal name="add_interval'vc.88.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.89" expl="variant decrease" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.90" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.91" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.92" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.92.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.92.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="add_interval'vc.92.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.11"/></proof>
+ </goal>
+ <goal name="add_interval'vc.92.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.92.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.93" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.93.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.93.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.80"/></proof>
+ </goal>
+ <goal name="add_interval'vc.93.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.05"/></proof>
+ </goal>
+ <goal name="add_interval'vc.93.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.08"/></proof>
+ </goal>
+ <goal name="add_interval'vc.93.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.93.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.93.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.17"/></proof>
+ </goal>
+ <goal name="add_interval'vc.93.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.94" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.94.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.94.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.10"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.94.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.94.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.94.1.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.94.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.95" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.95.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.95.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.06"/></proof>
+ </goal>
+ <goal name="add_interval'vc.95.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.11"/></proof>
+ </goal>
+ <goal name="add_interval'vc.95.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.20"/></proof>
+ </goal>
+ <goal name="add_interval'vc.95.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="1.29"/></proof>
+ </goal>
+ <goal name="add_interval'vc.95.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="2.10"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.95.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.50"/></proof>
+ </goal>
+ <goal name="add_interval'vc.95.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.96" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.96.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.96.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.83"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.86"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.81"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.96.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.96.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="3.46"/></proof>
+ </goal>
+ <goal name="add_interval'vc.96.1.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="4.18"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.96.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.97" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.97.0" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.97.0.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.0.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.0.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.0.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.0.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.97.1" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.97.1.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.1.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.1.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.1.3" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="add_interval'vc.97.1.4" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.97.2" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.98" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.00"/></proof>
+ </goal>
+ <goal name="add_interval'vc.99" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.100" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.101" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.102" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.103" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.104" expl="assertion" proved="true">
+ <proof prover="3"><result status="valid" time="1.13"/></proof>
+ </goal>
+ <goal name="add_interval'vc.105" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.106" expl="precondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.01"/></proof>
+ </goal>
+ <goal name="add_interval'vc.107" expl="postcondition" proved="true">
+ <transf name="split_vc" proved="true" >
+ <goal name="add_interval'vc.107.0" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="add_interval'vc.107.1" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.06"/></proof>
+ </goal>
+ </transf>
+ </goal>
+ <goal name="add_interval'vc.108" expl="postcondition" proved="true">
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ </transf>
+ </goal>
</theory>
</file>
</why3session>
diff --git a/src_common/union__Union.ml b/src_common/union__Union.ml
index dc9bf52f2..950e7e7de 100644
--- a/src_common/union__Union.ml
+++ b/src_common/union__Union.ml
@@ -434,3 +434,106 @@ let except (l: t') (x: Q.t) : t' option =
| l' -> Some (Off l')
end
+let add_cst (l: t') (x: Q.t) : t' =
+ let rec add_cst_on (x1: Q.t) (l1: on) : on =
+ match l1 with
+ | OnSin (q, l') -> OnSin ((Q.(+) q x1), add_cst_on x1 l')
+ | OnEnd (q, bv, l') -> OnEnd ((Q.(+) q x1), bv, add_cst_off x1 l')
+ | OnInf -> OnInf
+ and add_cst_off (x1: Q.t) (l1: off) : off =
+ match l1 with
+ | OffSin (q, l') -> OffSin ((Q.(+) q x1), add_cst_off x1 l')
+ | OffEnd (q, b, l') -> OffEnd ((Q.(+) q x1), b, add_cst_on x1 l')
+ | OffInf -> OffInf in
+ match l with
+ | On l1 -> On (add_cst_on x l1)
+ | Off l_off -> (let l1 = add_cst_off x l_off in Off l1)
+
+let add_bound (b1: Interval__Bound.t) (b2: Interval__Bound.t) :
+ Interval__Bound.t =
+ match (b1, b2) with
+ | (Interval__Bound.Large, Interval__Bound.Large) -> Interval__Bound.Large
+ | (Interval__Bound.Large, Interval__Bound.Strict) -> Interval__Bound.Strict
+ | (Interval__Bound.Strict, Interval__Bound.Large) -> Interval__Bound.Strict
+ | (Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ Interval__Bound.Strict
+
+let add_interval (l: t') (bu: Interval__Bound.t) (u: Q.t) (v: Q.t)
+ (bv: Interval__Bound.t) : t' =
+ let rec add_interval_on (bu1: Interval__Bound.t) (u1: Q.t) (v1: Q.t)
+ (bv1: Interval__Bound.t) (l1: on) : on =
+ match l1 with
+ | OnSin (qs, l') -> (let res = add_interval_on bu1 u1 v1 bv1 l' in res)
+ | OnEnd (qs,
+ bq,
+ l') ->
+ (let br = add_bound bq bv1 in let r = (Q.(+) qs v1) in
+ let res = add_interval_off_remain bu1 u1 v1 bv1 r br l' in res)
+ | OnInf -> OnInf
+ and add_interval_off (bu1: Interval__Bound.t) (u6: Q.t) (v6: Q.t)
+ (bv1: Interval__Bound.t) (l1: off) : off =
+ match l1 with
+ | OffSin (qs,
+ l') ->
+ (let r = (Q.(+) qs v6) in
+ let res = add_interval_off_remain bu1 u6 v6 bv1 r bv1 l' in
+ let res1 = OffEnd ((Q.(+) qs u6), bu1, res) in res1)
+ | OffEnd (qs,
+ b,
+ l') ->
+ (let bbu = add_bound b bu1 in
+ let res0 = add_interval_on bu1 u6 v6 bv1 l' in
+ let res = OffEnd ((Q.(+) qs u6), bbu, res0) in res)
+ | OffInf -> OffInf
+ and add_interval_off_remain (bu1: Interval__Bound.t) (u10: Q.t) (v10: Q.t)
+ (bv1: Interval__Bound.t) (r: Q.t)
+ (br: Interval__Bound.t) (l1: off) : on =
+ match l1 with
+ | OffSin (qs,
+ l') ->
+ (let qu = (Q.(+) qs u10) in
+ match (Q_extra.compare r qu) with
+ | Ord.Lt ->
+ (let r' = (Q.(+) qs v10) in
+ let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in
+ let res1 = OnEnd (r, br, OffEnd (qu, bu1, res)) in res1)
+ | Ord.Gt ->
+ (let r' = (Q.(+) qs v10) in
+ let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in res)
+ | Ord.Eq ->
+ begin match (br, bu1) with
+ | (Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ (let r' = (Q.(+) qs v10) in
+ let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in
+ let res1 = OnSin (qu, res) in res1)
+ | _ ->
+ (let r' = (Q.(+) qs v10) in
+ let res = add_interval_off_remain bu1 u10 v10 bv1 r' bv1 l' in
+ let res1 = res in res1)
+ end)
+ | OffEnd (qs,
+ b,
+ l') ->
+ (let qu = (Q.(+) qs u10) in let bbu = add_bound b bu1 in
+ match (Q_extra.compare r qu) with
+ | Ord.Lt ->
+ (let res = add_interval_on bu1 u10 v10 bv1 l' in
+ let res1 = OnEnd (r, br, OffEnd (qu, bbu, res)) in res1)
+ | Ord.Gt -> (let res = add_interval_on bu1 u10 v10 bv1 l' in res)
+ | Ord.Eq ->
+ begin match (br, bbu) with
+ | (Interval__Bound.Strict,
+ Interval__Bound.Strict) ->
+ (let res = add_interval_on bu1 u10 v10 bv1 l' in
+ let res1 = OnSin (qu, res) in res1)
+ | _ ->
+ (let res = add_interval_on bu1 u10 v10 bv1 l' in let res1 = res in
+ res1)
+ end)
+ | OffInf -> OnEnd (r, br, OffInf) in
+ match l with
+ | On l1 -> (let res = add_interval_on bu u v bv l1 in On res)
+ | Off l_off -> (let l1 = add_interval_off bu u v bv l_off in Off l1)
+
--
GitLab