diff --git a/src_common/union.mlw b/src_common/union.mlw
index 0f1cd7f2891f9e173376413d3fedef834bb8d394..d048e7d23f7b76e3760dcceafe1d7bc136f4e8a8 100644
--- a/src_common/union.mlw
+++ b/src_common/union.mlw
@@ -209,6 +209,19 @@ module Union
      | Off l ->
        mem_off x l
      end
+     
+  let ghost not_bottom (l:t') : real
+     ensures { mem result l.a } =
+      match l.a with
+      | Off (OffSin q _) -> Q.real q
+      | Off (OffEnd q _ (OnSin q' _)) -> (Q.real q*.0.5+.Q.real q'*.0.5)
+      | Off (OffEnd q _ (OnEnd q' _ _)) -> (Q.real q*.0.5+.Q.real q'*.0.5)
+      | Off (OffEnd q _ OnInf) -> (Q.real q+.1.)
+      | On (OnSin q _) -> (Q.real q-.1.)
+      | On (OnEnd q _ _) -> (Q.real q-.1.)
+      | On OnInf -> 0.
+      | Off OffInf -> absurd
+      end
 
   let rec ghost lt_bound_is_not_mem_off (q:Q.t) (l:off)
      requires { lt_bound_off q l }
@@ -485,200 +498,165 @@ module Union
           | On u, Off v | Off v, On u -> mk_off_option (inter_on_off u v)
           | Off u, Off v -> mk_off_option (inter_off_off u v)
           end
-(*
-    let inter (u:t') (v:t') : option t'
+
+
+    let union (u:t') (v:t') : t'
        ensures {
-         forall x:real. (mem x u.a /\ mem x v.a) <->
-            match result with
-            | None -> false
-            | Some w -> mem x w.a
-            end
+         forall x:real. (mem x u.a \/ mem x v.a) <-> mem x result.a
        } =
-         let rec aux (u:t0) (v:t0) : t0
-           requires { ordered0 u }
-           requires { ordered0 v }
-           ensures { ordered0 result }
+
+         let rec union_on_on (u:on) (v:on) : on
+           requires { ordered_on u }
+           requires { ordered_on v }
+           ensures { ordered_on result }
            ensures {
-             forall x:real. (mem0 x u /\ mem0 x v) <-> mem0 x result
+             forall x:real. (mem_on x u \/ mem_on x v) <-> mem_on x result
            }
            ensures {
              forall q.
-             (lt_bound0 q u) ->
-             (lt_bound0 q result )
+             (lt_bound_on q u) -> (lt_bound_on q v) ->
+             (lt_bound_on q result )
+           }
+           variant { length_on u + length_on v } =
+           match u, v with
+           | _, OnInf | OnInf, _ -> OnInf
+           | OnSin qu lu, OnSin qv lv ->
+             match Q.compare qu qv with
+             | Ord.Eq -> OnSin qu (union_on_on lu lv)
+             | Ord.Lt -> smaller_lt_bound_on qu qv lv; (union_on_on lu v)
+             | Ord.Gt -> smaller_lt_bound_on qv qu lu; (union_on_on u lv)
+             end
+           | OnEnd qu bu lu, OnEnd qv bv lv ->
+               match Q.compare qu qv with
+                | Ord.Eq ->
+                  let b = match bu, bv with
+                    | Strict, Strict -> Strict
+                    | _ -> Large
+                    end
+                  in
+                  lt_bound_is_not_mem_off qu lv;
+                  lt_bound_is_not_mem_off qu lu;
+                  OnEnd qu b (union_off_off lu lv)
+                | Ord.Lt -> smaller_lt_bound_off qu qv lv; (union_on_off v lu)
+                | Ord.Gt -> smaller_lt_bound_off qv qu lu; (union_on_off u lv)
+               end
+           | (OnSin qu lu) as u, (OnEnd qv bv lv) as v
+           | (OnEnd qv bv lv) as v, (OnSin qu lu) as u ->
+               lt_bound_is_not_mem_off qv lv;
+               match Q.compare qu qv with
+                | Ord.Eq ->
+                  smaller_lt_bound_on qv qu lu;
+                  match bv with
+                    | Strict -> OnSin qv (union_on_off lu lv)
+                    | _ -> (union_on_off lu lv)
+                    end
+                | Ord.Lt -> smaller_lt_bound_off qu qv lv; (union_on_on lu v)
+                | Ord.Gt -> smaller_lt_bound_on qv qu lu; (union_on_off u lv)
+               end
+           end
+         with  union_on_off (u:on) (v:off) : on
+           requires { ordered_on u }
+           requires { ordered_off v }
+           ensures { ordered_on result }
+           ensures {
+             forall x:real. (mem_on x u \/ mem_off x v) <-> mem_on x result
            }
            ensures {
              forall q.
-             (lt_bound0 q v) ->
-             (lt_bound0 q result )
+             (lt_bound_on q u) -> (lt_bound_off q v) ->
+             (lt_bound_on q result )
            }
-           variant { length0 u + length0 v } =
+           variant { length_on u + length_off v } =
            match u, v with
-           | End, _ | _, End -> End
-           | Singleton qu lu, Singleton qv lv ->
+           | u, OffInf -> u
+           | OnInf, _ -> OnInf
+           | OnSin qu lu, OffSin qv lv ->
+             lt_bound_is_not_mem_off qv lv;
              match Q.compare qu qv with
-             | Ord.Eq -> Singleton qu (aux lu lv)
-             | Ord.Lt -> aux lu v
-             | Ord.Gt -> aux u lv
+             | Ord.Eq -> union_on_off lu lv
+             | Ord.Lt -> smaller_lt_bound_off qu qv lv; OnSin qu (union_on_off lu v)
+             | Ord.Gt -> smaller_lt_bound_on  qv qu lu; assert { lt_bound_on qv u };
+                         (union_on_off u 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 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 -> 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 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 ->
-               let v' = v in let u' = u in
-               let small_big qu0 bu0 qu1 bu1 (lu:t0) (u:t0) qv0 bv0 (qv1:Q.t) (bv1:Bound.t) (lv:t0) v
-                  requires { ordered0 u }
-                  requires { ordered0 v }
-                  requires { u = Inter qu0 bu0 qu1 bu1 lu }
-                  requires { v = Inter qv0 bv0 qv1 bv1 lv }
-                  requires { (v = v' /\ length0 lu + 2 = length0 u') || (v = u' /\ length0 lu + 2 = length0 v') }
-                  requires { Q.( qu1 < qv1 ) }
-                  ensures { ordered0 result }
-                  ensures {
-                     forall x:real. (mem0 x u /\ mem0 x v) <-> mem0 x result
-                  }
-                  ensures {
-                    forall q.
-                    (lt_bound0 q u) ->
-                    (lt_bound0 q result )
-                  }
-                  ensures {
-                    forall q.
-                    (lt_bound0 q v) ->
-                    (lt_bound0 q result )
-                  }
-                =
-                match Q.compare qu1 qv0 with
-                 | Ord.Eq ->
-                   match bu1, bv0 with
-                     | Large, Large -> Singleton qu1 (aux lu v)
-                     | _ ->
-                      aux lu v
-                     end
-                 | Ord.Lt -> aux lu v
-                 | Ord.Gt ->
-                   let (qw0,bw0) = max_bound_inf qu0 bu0 qv0 bv0 in
-                   Inter qw0 bw0 qu1 bu1 (aux lu v)
-                end
-               in
-               match Q.compare qu1 qv1 with
+           | OnEnd qu bu lu, OffEnd qv bv lv ->
+               lt_bound_is_not_mem_off qu lu;
+               match Q.compare qu qv with
                 | Ord.Eq ->
-                  let (qw0,bw0) = max_bound_inf qu0 bu0 qv0 bv0 in
-                  let b = match bu1, bv1 with
-                    | Large, Large -> Large
-                    | _ -> Strict
+                  match bu, bv with
+                    | Strict, Strict -> OnSin qu (union_on_off lv lu)
+                    | _ -> (union_on_off lv lu)
                     end
-                  in
-                  Inter qw0 bw0 qv1 b (aux lu lv)
-                | 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
+                | Ord.Lt -> smaller_lt_bound_on qu qv lv; OnEnd qu bu (union_off_off lu v)
+                | Ord.Gt -> (union_on_on u lv)
                end
-            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
-              | lw -> Some { a = Finite lw }
-              end
-            in
-            match u.a, v.a with
-            | Inf, _ -> Some v
-            | _, Inf -> Some u
-            | InfFinite qu1 bu1 lu, InfFinite qv1 bv1 lv ->
-               match Q.compare qu1 qv1 with
+           | (OnSin qu lu) as u, (OffEnd qv bv lv) as v ->
+               match Q.compare qu qv with
+                | Ord.Eq -> match bv with Large -> (union_on_on lu lv) | Strict -> OnSin qu (union_on_on lu lv) end
+                | Ord.Lt -> smaller_lt_bound_on qu qv lv; OnSin qu (union_on_off lu v)
+                | Ord.Gt -> (union_on_on u lv)
+               end
+           | (OnEnd qv bv lv) as v, (OffSin qu lu) as u ->
+               lt_bound_is_not_mem_off qu lu;
+               lt_bound_is_not_mem_off qv lv;
+               match Q.compare qu qv with
+                | Ord.Eq -> OnEnd qv Large (union_off_off lu lv)
+                | Ord.Lt -> (union_on_off v lu)
+                | Ord.Gt -> smaller_lt_bound_off qv qu lu; OnEnd qv bv (union_off_off u lv)
+               end
+           end
+         with union_off_off (u:off) (v:off) : off
+           requires { ordered_off u}
+           requires { ordered_off v }
+           ensures { ordered_off result }
+           ensures {
+             forall x:real. (mem_off x u \/ mem_off x v) <-> mem_off x result
+           }
+           ensures {
+             forall q.
+             (lt_bound_off q u) -> (lt_bound_off q v) ->
+             (lt_bound_off q result )
+           }
+           variant { length_off u + length_off v } =
+           match u, v with
+           | u, OffInf | OffInf, u -> u
+           | OffSin qu lu, OffSin qv lv ->
+             lt_bound_is_not_mem_off qv lv;
+             lt_bound_is_not_mem_off qu lu;
+             match Q.compare qu qv with
+             | Ord.Eq -> OffSin qu (union_off_off lu lv)
+             | Ord.Lt -> smaller_lt_bound_off qu qv lv; OffSin qu (union_off_off lu v)
+             | Ord.Gt -> smaller_lt_bound_off qv qu lu; OffSin qv (union_off_off u lv)
+             end
+           | OffEnd qu bu lu, OffEnd qv bv lv ->
+               match Q.compare qu qv with
                 | Ord.Eq ->
-                  let b = match bu1, bv1 with
-                    | Large, Large -> Large
-                    | _ -> Strict
+                  let b = match bu, bv with
+                    | Strict, Strict -> Strict
+                    | _ -> Large
                     end
                   in
-                  Some { a = InfFinite qu1 b (aux lu lv) }
-                | Ord.Lt -> Some { a = InfFinite qu1 bu1 (aux lu (Inter qu1 Strict qv1 bv1 lv)) }
-                | Ord.Gt -> Some { a = InfFinite qv1 bv1 (aux (Inter qv1 Strict qu1 bu1 lu) lv) }
+                  OffEnd qu b (union_on_on lu lv)
+                | Ord.Lt -> smaller_lt_bound_on qu qv lv; OffEnd qu bu (union_on_off lu v)
+                | Ord.Gt -> smaller_lt_bound_on qv qu lu; OffEnd qv bv (union_on_off lv u)
                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 -> absurd
-                 | Singleton qu0 _ -> qu0, Large
-                 | Inter qu0 bu0 _ _ _ -> qu0,bu0
-                 | FiniteInf qu0 bu0 -> qu0,bu0
-                 end
-               in
-                match Q.compare qu0 qv1 with
-                | Ord.Eq ->
-                  match bu0, bv1 with
-                    | Large, 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
+           | (OffSin qu lu) as u, (OffEnd qv bv lv) as v
+           | (OffEnd qv bv lv) as v, (OffSin qu lu) as u ->
+               lt_bound_is_not_mem_off qu lu;
+               match Q.compare qu qv with
+                | Ord.Eq -> smaller_lt_bound_off qv qu lu; OffEnd qv Large (union_on_off lv lu)
+                | Ord.Lt -> smaller_lt_bound_on  qu qv lv; OffSin qu (union_off_off lu v)
+                | Ord.Gt -> smaller_lt_bound_off qv qu lu; OffEnd qv bv (union_on_off lv u)
                end
-            end
-*)
+           end
+           in
+          match u.a,v.a with
+          | On u, On v -> { a = On (union_on_on u v) }
+          | On u, Off v | Off v, On u -> { a = On (union_on_off u v) }
+          | Off u', Off v' -> let w = (union_off_off u' v') in
+                            let ghost x = not_bottom u in
+                            assert { mem_off x w };
+                            { a = Off w }
+          end
 
 
 end
diff --git a/src_common/union/why3session.xml b/src_common/union/why3session.xml
index 0662568acacf3286cf31a89521e7a499f37b7078..a64167c5d2fc9501640e062cdaab32c6526063f7 100644
--- a/src_common/union/why3session.xml
+++ b/src_common/union/why3session.xml
@@ -34,6 +34,9 @@
   </goal>
  </transf>
  </goal>
+ <goal name="not_bottom&#39;vc" expl="VC for not_bottom" proved="true">
+ <proof prover="3"><result status="valid" time="0.73"/></proof>
+ </goal>
  <goal name="lt_bound_is_not_mem_off&#39;vc" expl="VC for lt_bound_is_not_mem_off" proved="true">
  <proof prover="3"><result status="valid" time="0.16"/></proof>
  </goal>
@@ -1249,6 +1252,898 @@
   </goal>
  </transf>
  </goal>
+ <goal name="union&#39;vc" expl="VC for union" proved="true">
+ <transf name="split_vc" proved="true" >
+  <goal name="union&#39;vc.0" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.1" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.2" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.3" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.4" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.5" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.6" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.7" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.8" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.9" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.10" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.11" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.12" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.13" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.14" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.15" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.16" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.17" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.18" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.19" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.20" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.21" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.22" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.23" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.24" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.25" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.26" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.27" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.28" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.29" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.30" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.31" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.32" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.33" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.34" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.35" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.36" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.37" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.38" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.39" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.40" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.41" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.42" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.43" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.44" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.45" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.46" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.47" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.48" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.49" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.50" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.51" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.52" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.53" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.54" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.55" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.56" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.57" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.58" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.59" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.60" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.61" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.62" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.63" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.64" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.65" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.66" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.11"/></proof>
+  </goal>
+  <goal name="union&#39;vc.67" expl="postcondition" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="union&#39;vc.67.0" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.67.0.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.3" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.06"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="3.18"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.5" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.6" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="1.41"/></proof>
+    </goal>
+    <goal name="union&#39;vc.67.0.7" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="3.14"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="union&#39;vc.67.1" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="1.64"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="union&#39;vc.68" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.17"/></proof>
+  </goal>
+  <goal name="union&#39;vc.69" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.70" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.71" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.72" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.73" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.74" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.75" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.76" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.77" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.78" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.79" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.80" expl="assertion" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.81" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.82" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.83" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.84" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.85" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.86" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.87" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.88" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.89" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.90" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.91" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.92" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.93" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.94" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.95" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.96" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.97" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.98" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.99" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.100" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.101" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.102" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.103" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.104" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.105" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.106" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.107" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.108" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.109" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.110" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.111" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.112" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.113" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.114" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.115" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.116" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.117" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.118" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.119" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.120" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.121" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.122" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.123" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.124" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.125" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.126" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.127" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.128" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.129" expl="postcondition" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="union&#39;vc.129.0" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
+   </goal>
+   <goal name="union&#39;vc.129.1" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
+   </goal>
+   <goal name="union&#39;vc.129.2" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
+   </goal>
+   <goal name="union&#39;vc.129.3" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.129.3.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.129.3.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.36"/></proof>
+    </goal>
+    <goal name="union&#39;vc.129.3.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="union&#39;vc.129.4" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.59"/></proof>
+   </goal>
+   <goal name="union&#39;vc.129.5" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
+   </goal>
+   <goal name="union&#39;vc.129.6" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.47"/></proof>
+   </goal>
+   <goal name="union&#39;vc.129.7" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.24"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="union&#39;vc.130" expl="postcondition" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="union&#39;vc.130.0" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.130.0.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.3" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="1.80"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.89"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.5" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.6" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="3.81"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.0.7" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="1.22"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="union&#39;vc.130.1" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.130.1.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.3" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.05"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.64"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.5" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.6" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="3.69"/></proof>
+    </goal>
+    <goal name="union&#39;vc.130.1.7" expl="postcondition" proved="true">
+    <transf name="split_vc" proved="true" >
+     <goal name="union&#39;vc.130.1.7.0" expl="postcondition" proved="true">
+     <proof prover="3"><result status="valid" time="3.51"/></proof>
+     </goal>
+     <goal name="union&#39;vc.130.1.7.1" expl="postcondition" proved="true">
+     <proof prover="3"><result status="valid" time="0.03"/></proof>
+     </goal>
+     <goal name="union&#39;vc.130.1.7.2" expl="postcondition" proved="true">
+     <proof prover="3"><result status="valid" time="0.03"/></proof>
+     </goal>
+     <goal name="union&#39;vc.130.1.7.3" expl="postcondition" proved="true">
+     <proof prover="3"><result status="valid" time="0.49"/></proof>
+     </goal>
+    </transf>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="union&#39;vc.131" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.13"/></proof>
+  </goal>
+  <goal name="union&#39;vc.132" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.133" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.134" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.135" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.136" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.137" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.138" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.139" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.140" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.141" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.142" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.143" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.144" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.145" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.146" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.147" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.148" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.149" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.150" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.151" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.152" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.153" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.154" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.155" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.156" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.157" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.158" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.159" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.160" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.161" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.162" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.163" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.164" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.165" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.166" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.167" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.168" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.169" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.170" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.171" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.172" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.173" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.174" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.175" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.176" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.177" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.178" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.179" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.180" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.181" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.182" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.183" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.184" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.185" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.186" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.187" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.188" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.189" expl="variant decrease" proved="true">
+  <proof prover="3"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="union&#39;vc.190" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.191" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.192" expl="postcondition" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="union&#39;vc.192.0" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
+   </goal>
+   <goal name="union&#39;vc.192.1" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
+   </goal>
+   <goal name="union&#39;vc.192.2" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.01"/></proof>
+   </goal>
+   <goal name="union&#39;vc.192.3" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.192.3.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.02"/></proof>
+    </goal>
+    <goal name="union&#39;vc.192.3.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.57"/></proof>
+    </goal>
+    <goal name="union&#39;vc.192.3.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.43"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="union&#39;vc.192.4" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.71"/></proof>
+   </goal>
+   <goal name="union&#39;vc.192.5" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.00"/></proof>
+   </goal>
+   <goal name="union&#39;vc.192.6" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.47"/></proof>
+   </goal>
+   <goal name="union&#39;vc.192.7" expl="postcondition" proved="true">
+   <proof prover="3"><result status="valid" time="0.70"/></proof>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="union&#39;vc.193" expl="postcondition" proved="true">
+  <transf name="split_vc" proved="true" >
+   <goal name="union&#39;vc.193.0" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.193.0.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.3" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.08"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="4.85"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.5" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.6" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="3.44"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.0.7" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="4.72"/></proof>
+    </goal>
+   </transf>
+   </goal>
+   <goal name="union&#39;vc.193.1" expl="postcondition" proved="true">
+   <transf name="split_vc" proved="true" >
+    <goal name="union&#39;vc.193.1.0" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.1.1" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.1.2" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.01"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.1.3" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.07"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.1.4" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.77"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.1.5" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.00"/></proof>
+    </goal>
+    <goal name="union&#39;vc.193.1.6" expl="postcondition" proved="true">
+    <transf name="split_vc" proved="true" >
+     <goal name="union&#39;vc.193.1.6.0" expl="postcondition" proved="true">
+     <transf name="split_vc" proved="true" >
+      <goal name="union&#39;vc.193.1.6.0.0" expl="postcondition" proved="true">
+      <proof prover="3"><result status="valid" time="0.03"/></proof>
+      </goal>
+      <goal name="union&#39;vc.193.1.6.0.1" expl="postcondition" proved="true">
+      <proof prover="3"><result status="valid" time="1.92"/></proof>
+      </goal>
+      <goal name="union&#39;vc.193.1.6.0.2" expl="postcondition" proved="true">
+      <proof prover="3"><result status="valid" time="4.51"/></proof>
+      </goal>
+     </transf>
+     </goal>
+     <goal name="union&#39;vc.193.1.6.1" expl="postcondition" proved="true">
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
+     </goal>
+     <goal name="union&#39;vc.193.1.6.2" expl="postcondition" proved="true">
+     <proof prover="3"><result status="valid" time="0.02"/></proof>
+     </goal>
+    </transf>
+    </goal>
+    <goal name="union&#39;vc.193.1.7" expl="postcondition" proved="true">
+    <proof prover="3"><result status="valid" time="0.76"/></proof>
+    </goal>
+   </transf>
+   </goal>
+  </transf>
+  </goal>
+  <goal name="union&#39;vc.194" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.15"/></proof>
+  </goal>
+  <goal name="union&#39;vc.195" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.196" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.197" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.198" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.199" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.200" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.201" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.202" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.203" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.204" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.205" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.206" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.207" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.208" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.209" expl="assertion" proved="true">
+  <proof prover="3"><result status="valid" time="0.13"/></proof>
+  </goal>
+  <goal name="union&#39;vc.210" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.00"/></proof>
+  </goal>
+  <goal name="union&#39;vc.211" expl="precondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="union&#39;vc.212" expl="postcondition" proved="true">
+  <proof prover="3"><result status="valid" time="0.04"/></proof>
+  </goal>
+ </transf>
+ </goal>
 </theory>
 </file>
 </why3session>
diff --git a/src_common/union__Union.ml b/src_common/union__Union.ml
index 38b000f8c9bdb5a7903e974435a18040d087d028..f7bf1263e29977316017f665456832ebcbd09097 100644
--- a/src_common/union__Union.ml
+++ b/src_common/union__Union.ml
@@ -223,3 +223,133 @@ let inter (u: t') (v: t') : t' option =
   | ((On u8, Off v8) | (Off v8, On u8)) -> mk_off_option (inter_on_off u8 v8)
   | (Off u8, Off v8) -> mk_off_option (inter_off_off u8 v8)
 
+let union (u: t') (v: t') : t' =
+  let rec union_on_on (u1: on) (v1: on) : on =
+    match (u1, v1) with
+    | ((_, OnInf) | (OnInf, _)) -> OnInf
+    | (OnSin (qu,
+      lu),
+      OnSin (qv,
+      lv)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq -> OnSin (qu, union_on_on lu lv)
+      | Ord.Lt -> union_on_on lu v1
+      | Ord.Gt -> union_on_on u1 lv
+      end
+    | (OnEnd (qu,
+      bu,
+      lu),
+      OnEnd (qv,
+      bv,
+      lv)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq ->
+        (let b =
+           match (bu, bv) with
+           | (Interval__Bound.Strict,
+             Interval__Bound.Strict) ->
+             Interval__Bound.Strict
+           | _ -> Interval__Bound.Large in
+         OnEnd (qu, b, union_off_off lu lv))
+      | Ord.Lt -> union_on_off v1 lu
+      | Ord.Gt -> union_on_off u1 lv
+      end
+    | (((OnSin (qu, lu) as u3),
+       (OnEnd (qv, bv, lv) as v3)) | ((OnEnd (qv, bv, lv) as v3),
+       (OnSin (qu, lu) as u3))) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq ->
+        begin match bv with
+        | Interval__Bound.Strict -> OnSin (qv, union_on_off lu lv)
+        | _ -> union_on_off lu lv
+        end
+      | Ord.Lt -> union_on_on lu v3
+      | Ord.Gt -> union_on_off u3 lv
+      end
+  and union_on_off (u6: on) (v6: off) : on =
+    match (u6, v6) with
+    | (u8, OffInf) -> u8
+    | (OnInf, _) -> OnInf
+    | (OnSin (qu,
+      lu),
+      OffSin (qv,
+      lv)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq -> union_on_off lu lv
+      | Ord.Lt -> OnSin (qu, union_on_off lu v6)
+      | Ord.Gt -> union_on_off u6 lv
+      end
+    | (OnEnd (qu,
+      bu,
+      lu),
+      OffEnd (qv,
+      bv,
+      lv)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq ->
+        begin match (bu, bv) with
+        | (Interval__Bound.Strict,
+          Interval__Bound.Strict) ->
+          OnSin (qu, union_on_off lv lu)
+        | _ -> union_on_off lv lu
+        end
+      | Ord.Lt -> OnEnd (qu, bu, union_off_off lu v6)
+      | Ord.Gt -> union_on_on u6 lv
+      end
+    | ((OnSin (qu, lu) as u8),
+      (OffEnd (qv, _, lv) as v8)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq -> union_on_on lu lv
+      | Ord.Lt -> OnSin (qu, union_on_off lu v8)
+      | Ord.Gt -> union_on_on u8 lv
+      end
+    | ((OnEnd (qv, bv, lv) as v9),
+      (OffSin (qu, lu) as u9)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq -> OnEnd (qv, Interval__Bound.Large, union_off_off lu lv)
+      | Ord.Lt -> union_on_off v9 lu
+      | Ord.Gt -> OnEnd (qv, bv, union_off_off u9 lv)
+      end
+  and union_off_off (u10: off) (v10: off) : off =
+    match (u10, v10) with
+    | ((u11, OffInf) | (OffInf, u11)) -> u11
+    | (OffSin (qu,
+      lu),
+      OffSin (qv,
+      lv)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq -> OffSin (qu, union_off_off lu lv)
+      | Ord.Lt -> OffSin (qu, union_off_off lu v10)
+      | Ord.Gt -> OffSin (qv, union_off_off u10 lv)
+      end
+    | (OffEnd (qu,
+      bu,
+      lu),
+      OffEnd (qv,
+      bv,
+      lv)) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq ->
+        (let b =
+           match (bu, bv) with
+           | (Interval__Bound.Strict,
+             Interval__Bound.Strict) ->
+             Interval__Bound.Strict
+           | _ -> Interval__Bound.Large in
+         OffEnd (qu, b, union_on_on lu lv))
+      | Ord.Lt -> OffEnd (qu, bu, union_on_off lu v10)
+      | Ord.Gt -> OffEnd (qv, bv, union_on_off lv u10)
+      end
+    | (((OffSin (qu, lu) as u11),
+       (OffEnd (qv, bv, lv) as v11)) | ((OffEnd (qv, bv, lv) as v11),
+       (OffSin (qu, lu) as u11))) ->
+      begin match (Q_extra.compare qu qv) with
+      | Ord.Eq -> OffEnd (qv, Interval__Bound.Large, union_on_off lv lu)
+      | Ord.Lt -> OffSin (qu, union_off_off lu v11)
+      | Ord.Gt -> OffEnd (qv, bv, union_on_off lv u11)
+      end in
+  match (u, v) with
+  | (On u12, On v12) -> On (union_on_on u12 v12)
+  | ((On u12, Off v12) | (Off v12, On u12)) -> On (union_on_off u12 v12)
+  | (Off u12, Off v12) -> Off (union_off_off u12 v12)
+