From 20a8de678b3d8ba4e9bc74be018df343f2310e4b Mon Sep 17 00:00:00 2001
From: Raphael Rieu-Helft <raphael.rieu-helft@lri.fr>
Date: Tue, 12 Dec 2017 14:40:46 +0100
Subject: [PATCH] Interpreter for ML compiled code, reification fixes, linear
 decision toy example (not proved)

---
 .../multiprecision/compute/why3session.xml    |  16 +-
 .../multiprecision/lineardecision.mlw         | 383 +++++---
 .../lineardecision/why3session.xml            | 891 +++++++++++-------
 .../lineardecision/why3shapes.gz              | Bin 10756 -> 13387 bytes
 src/transform/reification.ml                  | 436 +++++++--
 src/transform/reification.mli                 |   2 +-
 6 files changed, 1178 insertions(+), 550 deletions(-)

diff --git a/examples/in_progress/multiprecision/compute/why3session.xml b/examples/in_progress/multiprecision/compute/why3session.xml
index 198a9b78f6..4ecae76018 100644
--- a/examples/in_progress/multiprecision/compute/why3session.xml
+++ b/examples/in_progress/multiprecision/compute/why3session.xml
@@ -145,7 +145,7 @@
    <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
    </goal>
    <goal name="VC insert_mon.2.1" expl="postcondition" proved="true">
-   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.81"/></proof>
+   <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="1.03"/></proof>
    </goal>
   </transf>
   </goal>
@@ -212,7 +212,7 @@
  <goal name="VC mon" expl="VC for mon" proved="true">
  <proof prover="4"><result status="valid" time="0.00"/></proof>
  </goal>
- <goal name="VC interp&apos;" expl="VC for interp'" proved="true">
+ <goal name="VC interp&#39;" expl="VC for interp'" proved="true">
  <proof prover="4"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC mon_append" expl="VC for mon_append" proved="true">
@@ -220,7 +220,7 @@
  <proof prover="1"><result status="valid" time="0.09"/></proof>
  </goal>
  <goal name="interp_cons" proved="true">
- <proof prover="1"><result status="valid" time="0.66"/></proof>
+ <proof prover="1"><result status="valid" time="0.49"/></proof>
  <transf name="compute_in_goal" proved="true" >
   <goal name="interp_cons.0" proved="true">
   <proof prover="0"><result status="valid" time="0.01" steps="42"/></proof>
@@ -375,7 +375,7 @@
   </goal>
  </transf>
  </goal>
- <goal name="VC normalize&apos;" expl="VC for normalize'" proved="true">
+ <goal name="VC normalize&#39;" expl="VC for normalize'" proved="true">
  <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
  </goal>
  <goal name="VC normalize" expl="VC for normalize" proved="true">
@@ -384,7 +384,7 @@
  <goal name="VC norm" expl="VC for norm" proved="true">
  <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
  </goal>
- <goal name="VC norm&apos;" expl="VC for norm'" proved="true">
+ <goal name="VC norm&#39;" expl="VC for norm'" proved="true">
  <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
  </goal>
  <goal name="VC norm_f" expl="VC for norm_f" proved="true">
@@ -508,7 +508,7 @@
   <proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
   </goal>
   <goal name="h.1" proved="true">
-  <proof prover="0"><result status="valid" time="0.87" steps="79"/></proof>
+  <proof prover="0"><result status="valid" time="0.51" steps="79"/></proof>
   </goal>
   <goal name="h.2" proved="true">
   <transf name="compute_in_goal" proved="true" >
@@ -889,7 +889,7 @@
  <goal name="opp_involutive" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="opp_involutive.0" proved="true">
-  <proof prover="0"><result status="valid" time="0.22" steps="413"/></proof>
+  <proof prover="0"><result status="valid" time="0.35" steps="413"/></proof>
   </goal>
   <goal name="opp_involutive.1" proved="true">
   <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
@@ -1144,7 +1144,7 @@
   <goal name="VC mul_assoc_get.3" expl="assertion" proved="true">
   <transf name="split_goal_wp" proved="true" >
    <goal name="VC mul_assoc_get.3.0" expl="assertion" proved="true">
-   <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.43" steps="700"/></proof>
+   <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.71" steps="700"/></proof>
    <proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="0.05"/></proof>
    </goal>
    <goal name="VC mul_assoc_get.3.1" expl="VC for mul_assoc_get" proved="true">
diff --git a/examples/in_progress/multiprecision/lineardecision.mlw b/examples/in_progress/multiprecision/lineardecision.mlw
index 2db87dc09a..193f09363a 100644
--- a/examples/in_progress/multiprecision/lineardecision.mlw
+++ b/examples/in_progress/multiprecision/lineardecision.mlw
@@ -1,38 +1,37 @@
 module LinearEquationsCoeffs
 
 use import int.Int
+use import real.Real
 
 type t
-type vars = int -> int
+type vars
 
 exception Unknown
 
-function interp t vars : int
+function interp t vars : real
 
-val constant zero : t
-val constant one : t
-
-axiom zero_def: forall y. interp zero y = 0
-axiom one_def: forall y. interp one y = 1
+val constant czero : t
+val constant cone : t
 
+axiom zero_def: forall y. interp czero y = zero
+axiom one_def: forall y. interp cone y = one
+(*
 function add_f t t : t
 function opp_f t : t
 function mul_f t t : t
 function inv_f t : t
+*)
 predicate (<=) t t
 
 val add (a b: t) : t
   ensures { forall v: vars. interp result v = interp a v + interp b v }
-  ensures { result = add_f a b }
   raises  { Unknown -> true }
 
 val mul (a b: t) : t
   ensures { forall v: vars. interp result v = interp a v * interp b v }
-  ensures { result = mul_f a b }
 
 val opp (a:t) : t
   ensures { forall v: vars. interp result v = - (interp a v) }
-  ensures { result = opp_f a }
 
 val predicate eq (a b:t)
   ensures { result <-> forall y:vars. interp a y = interp b y }
@@ -47,37 +46,40 @@ val solve (a b:t) : t
 *)
 
 val inv (a:t) : t
-  requires { not (eq a zero) }
-  ensures { mul_f result a = one }
-  ensures { not (eq result zero) }
+  requires { not (eq a czero) }
+  ensures { forall v: vars. interp result v * interp a v = one }
+  ensures { not (eq result czero) }
+  raises { Unknown -> true }
 
 val le (a b:t) : bool
   ensures { result <-> a <= b }
-  ensures { result -> forall y:vars. Int.(<=) (interp a y) (interp b y) }
+  ensures { result -> forall y:vars. Real.(<=) (interp a y) (interp b y) }
   raises  { Unknown -> true }
 
-clone export algebra.OrderedField with type t, function (+) = add_f, function (-_) = opp_f, function ( *) = mul_f, function inv = inv_f, constant zero = zero, constant one = one, predicate (<=) = (<=)
 
-(*FIXME equality test ? *)
+
+(*
+clone export algebra.OrderedField with type t, function (+) = add_f, function (-_) = opp_f, function (*) = mul_f, function inv = inv_f, constant zero = zero, constant one = one, predicate (<=) = (<=)
+*)
+(*FIXME equality test, extensionality, specs for le and eq ? *)
 
 end
 
 module LinearEquationsDecision
 
 use import int.Int
+use import real.RealInfix
 
 type coeff
 
 clone LinearEquationsCoeffs as C with type t = coeff
 
-type var = int
-
-type expr = Term coeff var | Add expr expr | Cst coeff
+type expr = Term coeff int | Add expr expr | Cst coeff | UTerm int
 
 let rec predicate valid_expr (e:expr)
   variant { e }
 = match e with
-  | Term _ i -> 0 <= i
+  | Term _ i | UTerm i -> 0 <= i
   | Cst _ -> true
   | Add e1 e2 -> valid_expr e1 && valid_expr e2
   end
@@ -85,17 +87,18 @@ let rec predicate valid_expr (e:expr)
 let rec predicate expr_bound (e:expr) (b:int)
   variant { e }
 = match e with
-  | Term _ i -> 0 <= i <= b
+  | Term _ i | UTerm i -> 0 <= i <= b
   | Cst _ -> true
   | Add e1 e2 -> expr_bound e1 b && expr_bound e2 b
   end
 
-type vars = var -> int
+type vars = int -> real
 
-function interp (e:expr) (y: vars) (z:C.vars) : int
+function interp (e:expr) (y: vars) (z:C.vars) : real
 = match e with
-  | Term c v -> (C.interp c z) * (y v)
-  | Add e1 e2 -> interp e1 y z + interp e2 y z
+  | UTerm v -> y v
+  | Term c v -> (C.interp c z) *. (y v)
+  | Add e1 e2 -> interp e1 y z +. interp e2 y z
   | Cst c -> C.interp c z
   end
 
@@ -126,6 +129,7 @@ let rec lemma expr_bound_w (e:expr) (b1 b2:int)
   | Add e1 e2 -> expr_bound_w e1 b1 b2; expr_bound_w e2 b1 b2
   | Cst _ -> ()
   | Term _ _ -> ()
+  | UTerm _ -> ()
   end
 
 lemma eq_bound_w: forall e:equality, b1 b2:int. eq_bound e b1 -> b1 <= b2 -> eq_bound e b2
@@ -144,7 +148,7 @@ function interp_eq (g:equality) (y:vars) (z:C.vars) : bool
 function interp_ctx (l: context) (g: equality) (y: vars) (z:C.vars) : bool
 = match l with
   | Nil -> interp_eq g y z
-  | Cons h t->  implb (interp_eq h y z) (interp_ctx t g y z)
+  | Cons h t -> implb (interp_eq h y z) (interp_ctx t g y z)
   end
 
 use import array.Array
@@ -155,7 +159,7 @@ let apply_r (m: matrix coeff) (v: array coeff) : array coeff
   ensures  { result.length = m.rows }
   raises   { C.Unknown -> true }
   (*TODO semantics*)
-= let r = Array.make m.rows C.zero in
+= let r = Array.make m.rows C.czero in
   for i = 0 to m.rows - 1 do
     for j = 0 to m.columns - 1 do
       r[i] <- C.add r[i] (C.mul (get m i j) v[j]);
@@ -167,7 +171,7 @@ let apply_l (v: array coeff) (m: matrix coeff) : array coeff
   requires { v.length = m.rows }
   ensures  { result.length = m.columns }
   raises   { C.Unknown -> true }
-= let r = Array.make m.columns C.zero in
+= let r = Array.make m.columns C.czero in
   for j = 0 to m.columns - 1 do
     for i = 0 to m.rows - 1 do
       r[j] <- C.add r[j] (C.mul (get m i j) v[i]);
@@ -180,7 +184,7 @@ use import ref.Ref
 let sprod (a b: array coeff) : coeff
   requires { a.length = b.length }
   raises   { C.Unknown -> true }
-= let r = ref C.zero in
+= let r = ref C.czero in
   for i = 0 to a.length - 1 do
     r := C.add !r (C.mul a[i] b[i]);
   done;
@@ -193,7 +197,7 @@ let m_append (m: matrix coeff) (v:array coeff) : matrix coeff
   ensures  { forall i j. 0 <= i < m.rows -> 0 <= j < m.columns ->
              result.elts i j = m.elts i j }
   ensures  { forall i. 0 <= i < m.rows -> result.elts i m.columns = v[i] }
-= let r = Matrix.make m.rows (m.columns + 1) C.zero in
+= let r = Matrix.make m.rows (m.columns + 1) C.czero in
   for i = 0 to m.rows - 1 do
     invariant { forall k j. 0 <= k < i -> 0 <= j < m.columns ->
                 r.elts k j = m.elts k j }
@@ -239,7 +243,7 @@ let rec function max_var (e:expr) : int
   ensures { 0 <= result }
   ensures { expr_bound e result }
 = match e with
-  | Term _ i -> i
+  | Term _ i | UTerm i -> i
   | Cst _ -> 0
   | Add e1 e2 -> max (max_var e1) (max_var e2)
   end
@@ -261,22 +265,41 @@ let rec function max_var_ctx (l:context) : int
   end
 
 let rec function opp_expr (e:expr) : expr
-  ensures { forall y z. interp result y z = - (interp e y z) }
+  ensures { forall y z. interp result y z = -. (interp e y z) }
   ensures { forall b. expr_bound e b -> expr_bound result b }
   variant { e }
 = match e with
   | Cst c -> Cst (C.opp c)
   | Term c j -> Term (C.opp c) j
+  | UTerm j -> Term (C.opp C.cone) j
   | Add e1 e2 -> Add (opp_expr e1) (opp_expr e2)
   end
 
 predicate no_cst (e:expr)
 = match e with
-  | Cst c -> C.eq c C.zero
-  | Term _ _ -> true
+  | Cst c -> C.eq c C.czero
+  | Term _ _ | UTerm _ -> true
   | Add e1 e2 -> no_cst e1 && no_cst e2
   end
 
+(*TODO put this back in norm_eq*)
+let rec norm_eq_aux (ex acc_e:expr) (acc_c:coeff) : (expr, coeff)
+  requires { no_cst acc_e }
+  returns { (rex, rc) -> forall y z.
+            interp rex y z +. interp (Cst rc) y z
+            = interp ex y z +. interp acc_e y z +. interp (Cst acc_c) y z }
+  returns { (rex, _) -> no_cst rex }
+  returns { (rex, _) -> forall b:int. expr_bound ex b /\ expr_bound acc_e b
+                        -> expr_bound rex b }
+  raises  { C.Unknown -> true }
+  variant { ex }
+= match ex with
+  | Cst c -> acc_e, (C.add c acc_c)
+  | Term _ _ | UTerm _ -> (Add acc_e ex, acc_c)
+  | Add e1 e2 -> let ae, ac = norm_eq_aux e1 acc_e acc_c in
+                 norm_eq_aux e2 ae ac
+  end
+
 let norm_eq (e:equality) : (expr, coeff)
   returns { (ex, c) -> forall y z.
             interp_eq e y z -> interp_eq (ex, Cst c) y z }
@@ -285,26 +308,9 @@ let norm_eq (e:equality) : (expr, coeff)
   raises  { C.Unknown -> true }
 = match e with
   | (e1, e2) ->
-    let rec aux (ex acc_e:expr) (acc_c:coeff) : (expr, coeff)
-      requires { no_cst acc_e }
-      returns { (rex, rc) -> forall y z.
-                interp rex y z + interp (Cst rc) y z
-                = interp ex y z + interp acc_e y z + interp (Cst acc_c) y z }
-      returns { (rex, _) -> no_cst rex }
-      returns { (rex, _) -> forall b:int. expr_bound ex b /\ expr_bound acc_e b
-                            -> expr_bound rex b }
-      raises  { C.Unknown -> true }
-      variant { ex }
-    = match ex with
-      | Cst c -> acc_e, (C.add c acc_c)
-      | Term _ _ -> (Add acc_e ex, acc_c)
-      | Add e1 e2 -> let ae, ac = aux e1 acc_e acc_c in
-                     aux e2 ae ac
-      end
-    in
     let s = Add e1 (opp_expr e2) in
     assert { forall b. eq_bound e b -> expr_bound s b };
-    match aux s (Cst C.zero) C.zero with
+    match norm_eq_aux s (Cst C.czero) C.czero with
       (e, c) -> e, C.opp c
     end
   end
@@ -314,7 +320,7 @@ let norm_eq (e:equality) : (expr, coeff)
 let transpose (m:matrix coeff) : matrix coeff
   ensures { result.rows = m.columns /\ result.columns = m.rows }
 =
-  let r = Matrix.make m.columns m.rows C.zero in
+  let r = Matrix.make m.columns m.rows C.czero in
   for i = 0 to m.rows - 1 do
     for j = 0 to m.columns - 1 do
       set r j i (get m i j)
@@ -332,7 +338,7 @@ let swap_rows (m:matrix coeff) (i1 i2: int) : unit
 
 let mul_row (m:matrix coeff) (i: int) (c: coeff) : unit
   requires { 0 <= i < m.rows }
-  requires { not (C.eq c C.zero) }
+  requires { not (C.eq c C.czero) }
 = for j = 0 to m.columns - 1 do
     set m i j (C.mul c (get m i j))
   done
@@ -347,6 +353,19 @@ let addmul_row (m:matrix coeff) (src dst: int) (c: coeff) : unit
 use import ref.Refint
 use import option.Option
 
+(*TODO this goes inside gauss_jordan*)
+let rec find_nonz (a:matrix coeff) (i j m n:int)
+  requires { 0 <= i <= n }
+  requires { 0 <= j < m }
+  variant { n-i }
+  ensures { i <= result <= n }
+  ensures { result < n -> not (C.eq (a.elts result j) C.czero) }
+= if i >= n then n
+  else
+    if C.eq (get a i j) C.czero
+    then find_nonz a (i+1) j m n
+    else i
+
 let gauss_jordan (a: matrix coeff) : option (array coeff)
   (*AX=B, a=(A|B), result=X*)
   returns { Some r -> Array.length r = a.columns - 1 | None -> true }
@@ -355,18 +374,6 @@ let gauss_jordan (a: matrix coeff) : option (array coeff)
 =
   let n = a.rows in
   let m = a.columns in
-  let rec find_nonz i j
-    requires { 0 <= i <= n }
-    requires { 0 <= j < m }
-    variant { n-i }
-    ensures { i <= result <= n }
-    ensures { result < n -> not (C.eq (a.elts result j) C.zero) }
-  = if i >= n then n
-    else
-      if C.eq (get a i j) C.zero
-      then find_nonz (i+1) j
-      else i
-  in
   let pivots = Array.make n 0 in
   let r = ref (-1) in
   for j = 0 to m-1 do
@@ -375,7 +382,7 @@ let gauss_jordan (a: matrix coeff) : option (array coeff)
     invariant { forall i1 i2: int. 0 <= i1 < i2 <= !r -> pivots[i1] < pivots[i2] }
     invariant { !r >= 0 -> pivots[!r] < j }
     label Start in
-    let k = find_nonz (!r+1) j in
+    let k = find_nonz a (!r+1) j m n in
     if k < n
     then begin
       incr r;
@@ -391,65 +398,70 @@ let gauss_jordan (a: matrix coeff) : option (array coeff)
   if !r < 0 then None (* matrix is all zeroes *)
   else if pivots[!r] >= m-1 then None (*pivot on last column, no solution*)
   else begin
-    let v = Array.make (m-1) C.zero in
+    let v = Array.make (m-1) C.czero in
     for i = 0 to !r do
       v[pivots[i]] <- get a i (m-1)
     done;
     Some v
   end
 
+(*TODO put fill_ back in linear_decision, remove a, b, v, l, nv params*)
+let rec fill_expr (a:matrix coeff) (ex: expr) (i:int)
+                  (ghost l: context) (ghost nv: int): unit
+  variant { ex }
+  requires { no_cst ex }
+  raises  { C.Unknown -> true }
+  requires { 0 <= i < length l }
+  requires { expr_bound ex nv }
+= match ex with
+  | Cst c -> if C.eq c C.czero then () else absurd
+  | Term c j -> set a i j (C.add (get a i j) c)
+  | UTerm j -> set a i j (C.add (get a i j) C.cone)
+  | Add e1 e2 -> fill_expr a e1 i l nv; fill_expr a e2 i l nv
+  end
+
+let rec fill_ctx (a:matrix coeff) (b:array coeff) (ctx:context) (i:int)
+                 (ghost l: context) (ghost nv: int) : unit
+  requires { ctx_bound ctx nv }
+  variant { length l - i }
+  requires { length l - i = length ctx }
+  requires { 0 <= i <= length l }
+  raises  { C.Unknown -> true }
+= match ctx with
+  | Nil -> ()
+  | Cons e t ->
+    assert { i < length l };
+    let ex, c = norm_eq e in
+    if (not (C.eq c C.czero)) then b[i] <- C.add b[i] c;
+    fill_expr a ex i l nv;
+    fill_ctx a b t (i+1) l nv
+  end
+
+let rec fill_goal (v:array coeff) (ex:expr) (ghost nv: int) : unit
+  requires { expr_bound ex nv }
+  variant { ex }
+  requires { no_cst ex }
+  raises { C.Unknown -> true }
+= match ex with
+  | Cst c -> if C.eq c C.czero then () else absurd
+  | Term c j -> v[j] <- C.add v[j] c
+  | UTerm j -> v[j] <- C.add v[j] C.cone
+  | Add e1 e2 -> fill_goal v e1 nv; fill_goal v e2 nv
+  end
+  
 let linear_decision (l: context) (g: equality) : bool
   requires { valid_ctx l }
   requires { valid_eq g }
-  (*ensures { result = true -> forall y z. interp_ctx l g y z = true }*)
+  ensures { forall y z. result -> interp_ctx l g y z }
   raises  { C.Unknown -> true }
 =
   let nv = max (max_var_e g) (max_var_ctx l) in
-  let a = Matrix.make (length l) (nv+1) C.zero in
-  let b = Array.make (length l) C.zero in      (* ax = b *)
-  let v = Array.make (nv+1) C.zero in      (* goal *)
-  let rec fill_expr (ex: expr) (i:int) : unit
-    variant { ex }
-    requires { no_cst ex }
-    raises  { C.Unknown -> true }
-    requires { 0 <= i < length l }
-    requires { expr_bound ex nv }
-  = match ex with
-    | Cst c -> if C.eq c C.zero then () else absurd
-    | Term c j -> set a i j (C.add (get a i j) c)
-    | Add e1 e2 -> fill_expr e1 i; fill_expr e2 i
-    end
-  in
-  let rec fill_ctx (ctx:context) (i:int) : unit
-    requires { ctx_bound ctx nv }
-    variant { length l - i }
-    requires { length l - i = length ctx }
-    requires { 0 <= i <= length l }
-    raises  { C.Unknown -> true }
-  = match ctx with
-    | Nil -> ()
-    | Cons e t ->
-      assert { i < length l };
-      let ex, c = norm_eq e in
-      if (not (C.eq c C.zero)) then b[i] <- C.add b[i] c;
-      fill_expr ex i;
-      fill_ctx t (i+1)
-    end
-  in
-  let rec fill_goal (ex:expr) : unit
-    requires { expr_bound ex nv }
-    variant { ex }
-    requires { no_cst ex }
-    raises { C.Unknown -> true }
-  = match ex with
-    | Cst c -> if C.eq c C.zero then () else absurd
-    | Term c j -> v[j] <- C.add v[j] c
-    | Add e1 e2 -> fill_goal e1; fill_goal e2
-    end
-  in
-  fill_ctx l 0;
+  let a = Matrix.make (length l) (nv+1) C.czero in
+  let b = Array.make (length l) C.czero in      (* ax = b *)
+  let v = Array.make (nv+1) C.czero in          (* goal *)
+  fill_ctx a b l 0 l nv;
   let (ex, d) = norm_eq g in
-  fill_goal ex;
+  fill_goal v ex nv;
   let ab = m_append a b in
   let cd = v_append v d in
   let ab' = transpose ab in
@@ -458,4 +470,149 @@ let linear_decision (l: context) (g: equality) : bool
     | None -> false
   end
 
+(* forall eq in list interp_eq  est vraie -> interp_eq (toute combinaison linéaire) est vraie *)
+
+end
+
+module RealCoeffs
+
+use export real.Real
+
+type vars = int -> real
+
+let constant rzero = 0.0
+let constant rone = 1.0
+
+function interp (r:real) (v:vars) : real = r
+
+let radd a b = a+b
+let rmul a b = a*b
+let ropp a = - a
+let predicate req a b = a=b
+let rinv a
+ requires { a <> rzero }
+ ensures { result = rone/a }
+ = rone/a
+
+let rle a b = a <= b
+
+clone export LinearEquationsCoeffs with type t = real, type vars = vars, function interp,val czero=rzero, val cone=rone, lemma zero_def, lemma one_def, val add=radd, val mul=rmul, val opp=ropp, val eq=req, val inv=rinv, lemma eq_def, predicate (<=), val le=rle
+
+end
+
+module LinearDecisionReal
+
+use import RealCoeffs
+
+clone export LinearEquationsDecision with type coeff = real, type C.vars = vars, function C.interp=interp, val C.czero=rzero, val C.cone=rone, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, lemma C.eq_def, predicate C.(<=)=(<=), val C.le=rle
+
+end
+
+module RationalCoeffs
+
+use import int.Int
+use import real.RealInfix
+use import real.FromInt
+use import int.Abs
+
+meta coercion function from_int
+
+type t = (int, int)
+type rvars = int -> real
+
+function of_int (n:int) : t = (n,1)
+(*meta coercion function of_int*)
+
+
+let constant rzero = (0,1)
+let constant rone = (1,1)
+
+function rinterp (t:t) (v:rvars) : real
+= match t with
+  | (n,d) ->  from_int n /. from_int d
+  end
+
+use import int.ComputerDivision
+use import ref.Ref
+use import number.Gcd
+
+let gcd (x:int) (y:int)
+  requires { x >= 0 /\ y >= 0 }
+  ensures { result = gcd x y }
+  =
+  let x = ref x in let y = ref y in
+  label Pre in
+  while (!y > 0) do
+     invariant { !x >= 0 /\ !y >= 0 }
+     invariant { gcd !x !y = gcd (!x at Pre) (!y at Pre) }
+     variant { !y }
+     let r = mod !x !y in let ghost q = div !x !y in
+     assert { r = !x - q * !y };
+     x := !y; y := r;
+  done;
+  !x
+
+let simp (t:t) : t
+  ensures { forall v:rvars. rinterp result v = rinterp t v }
+= match t with
+  | (n,d) ->
+    let g = gcd (abs n) (abs d) in (div n g, div d g)
+  end
+
+let radd (a b:t)
+= match (a,b) with
+  | (n1,d1), (n2,d2) -> simp ((n1*d2 + n2*d1),(d1*d2))
+  end
+
+let rmul (a b:t)
+= match (a,b) with
+  | (n1,d1), (n2, d2) -> simp (n1*n2, d1*d2)
+  end
+
+let ropp (a:t)
+= match a with
+  | (n,d) -> (-n, d)
+  end
+
+let predicate req (a b:t)
+= match (a,b) with
+  | (n1,d1), (n2,d2) -> n1 * d2 = n2 * d1
+  end
+
+let rinv a
+= match a with
+  | (n,d) -> (d,n)
+  end
+
+let function rle (a b:t)
+= match (a,b) with
+  | (n1,d1), (n2,d2) -> n1 * d2 <= n2 * d1
+  end
+
+predicate (<=) (a b:t) = rle a b
+
+end
+
+module LinearDecisionRational
+
+use import RationalCoeffs
+
+clone export LinearEquationsDecision with type coeff = t, type C.vars = rvars, function C.interp=rinterp, val C.czero=rzero, val C.cone=rone, lemma C.zero_def, lemma C.one_def, val C.add=radd, val C.mul=rmul, val C.opp=ropp, val C.eq=req, val C.inv=rinv, lemma C.eq_def, predicate C.(<=)=(<=), val C.le=rle
+
+end
+
+theory Test
+
+use import RationalCoeffs
+use import LinearDecisionRational
+use import int.Int
+use import real.RealInfix
+use import real.FromInt
+
+meta coercion function from_int
+
+goal g: forall x y: real.
+        (from_int 3 /. from_int 1) *. x +. (from_int 2/. from_int 1) *. y = (from_int 21/. from_int 1) ->
+        (from_int 7 /. from_int 1) *. x +. (from_int 4/. from_int 1) *. y = (from_int 47/. from_int 1) ->
+        x = (from_int 5 /. from_int 1)
 end
\ No newline at end of file
diff --git a/examples/in_progress/multiprecision/lineardecision/why3session.xml b/examples/in_progress/multiprecision/lineardecision/why3session.xml
index 442df3af78..b9e28f6eae 100644
--- a/examples/in_progress/multiprecision/lineardecision/why3session.xml
+++ b/examples/in_progress/multiprecision/lineardecision/why3session.xml
@@ -6,17 +6,17 @@
 <prover id="1" name="CVC4" version="1.4" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="2" name="Z3" version="4.5.0" timelimit="1" steplimit="0" memlimit="1000"/>
 <prover id="3" name="Eprover" version="1.9.1-001" timelimit="5" steplimit="0" memlimit="2000"/>
-<file name="../lineardecision.mlw" proved="true">
-<theory name="LinearEquationsCoeffs" proved="true" sum="0ddc620243700595ee2068433d7c1835">
- <goal name="VC zero" expl="VC for zero" proved="true">
+<file name="../lineardecision.mlw">
+<theory name="LinearEquationsCoeffs" proved="true" sum="d2cd9e3b7921b7aaf50b840ab00d24f0">
+ <goal name="VC czero" expl="VC for czero" proved="true">
+ <proof prover="2"><result status="valid" time="0.02"/></proof>
+ </goal>
+ <goal name="VC cone" expl="VC for cone" proved="true">
  <transf name="split_goal_wp" proved="true" >
  </transf>
  </goal>
- <goal name="VC one" expl="VC for one" proved="true">
- <proof prover="2"><result status="valid" time="0.02"/></proof>
- </goal>
 </theory>
-<theory name="LinearEquationsDecision" proved="true" sum="a09a7412ea1130fde26f0258600d9676">
+<theory name="LinearEquationsDecision" sum="8ac278778b7b383543ca383f50b896d6">
  <goal name="VC valid_expr" expl="VC for valid_expr" proved="true">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
@@ -44,7 +44,8 @@
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC expr_bound_w.2" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="2" obsolete="true"><result status="highfailure" time="0.82"/></proof>
   </goal>
   <goal name="VC expr_bound_w.3" expl="variant decrease" proved="true">
   <proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -53,15 +54,15 @@
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC expr_bound_w.5" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="13"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="11"/></proof>
   </goal>
   <goal name="VC expr_bound_w.6" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="34"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="39"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="eq_bound_w" proved="true">
- <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="18"/></proof>
+ <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="15"/></proof>
  </goal>
  <goal name="VC ctx_bound_w" expl="VC for ctx_bound_w" proved="true">
  <transf name="split_goal_wp" proved="true" >
@@ -69,197 +70,197 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC ctx_bound_w.1" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="12"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="10"/></proof>
   </goal>
   <goal name="VC ctx_bound_w.2" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
   <goal name="VC ctx_bound_w.3" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="31"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="27"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC apply_r" expl="VC for apply_r" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="VC apply_r.0" expl="array creation size" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
   </goal>
   <goal name="VC apply_r.1" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="VC apply_r.2" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="VC apply_r.3" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="VC apply_r.4" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="VC apply_r.5" expl="exceptional postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
   </goal>
   <goal name="VC apply_r.6" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC apply_r.7" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC apply_l" expl="VC for apply_l" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="VC apply_l.0" expl="array creation size" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
   </goal>
   <goal name="VC apply_l.1" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="VC apply_l.2" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="VC apply_l.3" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="VC apply_l.4" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
   <goal name="VC apply_l.5" expl="exceptional postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
   </goal>
   <goal name="VC apply_l.6" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC apply_l.7" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC sprod" expl="VC for sprod" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="VC sprod.0" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC sprod.1" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC sprod.2" expl="exceptional postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="2"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC m_append" expl="VC for m_append" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="VC m_append.0" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
   <goal name="VC m_append.1" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
   <goal name="VC m_append.2" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
   <goal name="VC m_append.3" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
   </goal>
   <goal name="VC m_append.4" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
   </goal>
   <goal name="VC m_append.5" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="13"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="11"/></proof>
   </goal>
   <goal name="VC m_append.6" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
   <goal name="VC m_append.7" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="18"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="16"/></proof>
   </goal>
   <goal name="VC m_append.8" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="28"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
   <goal name="VC m_append.9" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
   </goal>
   <goal name="VC m_append.10" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
   </goal>
   <goal name="VC m_append.11" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
   <goal name="VC m_append.12" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
   <goal name="VC m_append.13" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="43"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="40"/></proof>
   </goal>
   <goal name="VC m_append.14" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
   <goal name="VC m_append.15" expl="out of loop bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
   </goal>
   <goal name="VC m_append.16" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
   </goal>
   <goal name="VC m_append.17" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="11"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
   </goal>
   <goal name="VC m_append.18" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="17"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="15"/></proof>
   </goal>
   <goal name="VC m_append.19" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
   <goal name="VC m_append.20" expl="out of loop bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC v_append" expl="VC for v_append" proved="true">
  <transf name="split_goal_wp" proved="true" >
   <goal name="VC v_append.0" expl="array creation size" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
   </goal>
   <goal name="VC v_append.1" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="4"/></proof>
   </goal>
   <goal name="VC v_append.2" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
   <goal name="VC v_append.3" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="10"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
   </goal>
   <goal name="VC v_append.4" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="10"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
   </goal>
   <goal name="VC v_append.5" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="31"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="VC v_append.6" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
   </goal>
   <goal name="VC v_append.7" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
   <goal name="VC v_append.8" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="14"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="12"/></proof>
   </goal>
   <goal name="VC v_append.9" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="9"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="7"/></proof>
   </goal>
   <goal name="VC v_append.10" expl="out of loop bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="8"/></proof>
+  <proof prover="0"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
  </transf>
  </goal>
  <goal name="VC max_var" expl="VC for max_var" proved="true">
- <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.04" steps="199"/></proof>
+ <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.04" steps="248"/></proof>
  </goal>
  <goal name="VC max_var_e" expl="VC for max_var_e" proved="true">
  <proof prover="2"><result status="valid" time="0.01"/></proof>
  </goal>
  <goal name="VC max_var_ctx" expl="VC for max_var_ctx" proved="true">
- <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.04" steps="146"/></proof>
+ <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.04" steps="137"/></proof>
  </goal>
  <goal name="VC opp_expr" expl="VC for opp_expr" proved="true">
  <transf name="split_goal_wp" proved="true" >
@@ -270,90 +271,101 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC opp_expr.2" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="89"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="90"/></proof>
   </goal>
   <goal name="VC opp_expr.3" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="82"/></proof>
-  <proof prover="2"><result status="timeout" time="1.00"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="89"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
  </transf>
  </goal>
+ <goal name="VC norm_eq_aux" expl="VC for norm_eq_aux">
+ </goal>
  <goal name="VC norm_eq" expl="VC for norm_eq" proved="true">
  <transf name="split_goal_wp" proved="true" >
-  <goal name="VC norm_eq.0" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="20"/></proof>
+  <goal name="VC norm_eq.0" expl="assertion" proved="true">
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
+  <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC norm_eq.1" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="8"/></proof>
+  <goal name="VC norm_eq.1" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC norm_eq.2" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="10"/></proof>
-  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
+  <proof prover="1"><result status="valid" time="0.06"/></proof>
   </goal>
-  <goal name="VC norm_eq.3" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC norm_eq.3" expl="postcondition" proved="true">
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="6"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
   <goal name="VC norm_eq.4" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="8"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="27"/></proof>
+  <proof prover="1" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
+  <proof prover="3" obsolete="true"><result status="timeout" time="4.96"/></proof>
   </goal>
-  <goal name="VC norm_eq.5" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC norm_eq.5" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC norm_eq.6" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="11"/></proof>
-  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
+  <goal name="VC norm_eq.10">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC norm_eq.7" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC norm_eq.12">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC norm_eq.8" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC norm_eq.13">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC norm_eq.9" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC norm_eq.11">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC norm_eq.10" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC norm_eq.5">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC norm_eq.11" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="10"/></proof>
+  <goal name="VC norm_eq.8">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="12"/></proof>
   </goal>
-  <goal name="VC norm_eq.12" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="9"/></proof>
+  <goal name="VC norm_eq.1">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.00" steps="5"/></proof>
   </goal>
-  <goal name="VC norm_eq.13" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="42"/></proof>
-  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
+  <goal name="VC norm_eq.15">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="7"/></proof>
   </goal>
-  <goal name="VC norm_eq.14" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC norm_eq.4">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.00" steps="6"/></proof>
   </goal>
-  <goal name="VC norm_eq.15" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC norm_eq.7">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
-  <goal name="VC norm_eq.16" expl="assertion" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="30"/></proof>
-  <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
-  <proof prover="2"><result status="timeout" time="1.00"/></proof>
+  <goal name="VC norm_eq.0">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.00" steps="17"/></proof>
   </goal>
-  <goal name="VC norm_eq.17" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC norm_eq.14">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="8"/></proof>
   </goal>
-  <goal name="VC norm_eq.18" expl="postcondition" proved="true">
-  <proof prover="1"><result status="valid" time="0.06"/></proof>
+  <goal name="VC norm_eq.6">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="9"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
+  </goal>
+  <goal name="VC norm_eq.9">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.00" steps="9"/></proof>
   </goal>
-  <goal name="VC norm_eq.19" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="9"/></proof>
+  <goal name="VC norm_eq.2">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="7"/></proof>
   <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC norm_eq.20" expl="postcondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="35"/></proof>
-  <proof prover="1" timelimit="10" memlimit="4000" obsolete="true"><result status="timeout" time="10.00"/></proof>
+  <goal name="VC norm_eq.16">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="39"/></proof>
   <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
-  <proof prover="3" obsolete="true"><result status="timeout" time="4.96"/></proof>
   </goal>
-  <goal name="VC norm_eq.21" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC norm_eq.3">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC norm_eq.18">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC norm_eq.17">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
   </goal>
  </transf>
  </goal>
@@ -364,167 +376,186 @@
  <proof prover="2"><result status="valid" time="0.02"/></proof>
  </goal>
  <goal name="VC mul_row" expl="VC for mul_row" proved="true">
- <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="18"/></proof>
+ <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="13"/></proof>
  </goal>
  <goal name="VC addmul_row" expl="VC for addmul_row" proved="true">
- <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="22"/></proof>
+ <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="19"/></proof>
+ </goal>
+ <goal name="VC find_nonz" expl="VC for find_nonz">
  </goal>
  <goal name="VC gauss_jordan" expl="VC for gauss_jordan" proved="true">
  <transf name="split_goal_wp" proved="true" >
-  <goal name="VC gauss_jordan.0" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="15"/></proof>
+  <goal name="VC gauss_jordan.0" expl="array creation size" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.1" expl="variant decrease" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <goal name="VC gauss_jordan.1" expl="loop invariant init" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.2" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <goal name="VC gauss_jordan.2" expl="loop invariant init" proved="true">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.3" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
+  <goal name="VC gauss_jordan.3" expl="loop invariant init" proved="true">
+  <proof prover="2"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.4" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
+  <goal name="VC gauss_jordan.4" expl="loop invariant init" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.5" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
+  <goal name="VC gauss_jordan.5" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="14"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.6" expl="array creation size" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="7"/></proof>
+  <goal name="VC gauss_jordan.6" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.7" expl="loop invariant init" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="9"/></proof>
+  <goal name="VC gauss_jordan.7" expl="index in array bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.8" expl="loop invariant init" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <goal name="VC gauss_jordan.8" expl="index in matrix bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.9" expl="loop invariant init" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <goal name="VC gauss_jordan.9" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.10" expl="loop invariant init" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.10" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
   </goal>
   <goal name="VC gauss_jordan.11" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
   <goal name="VC gauss_jordan.12" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+  <proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.13" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
+  <goal name="VC gauss_jordan.13" expl="index in matrix bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="35"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.14" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="25"/></proof>
+  <goal name="VC gauss_jordan.14" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="34"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.15" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+  <goal name="VC gauss_jordan.15" expl="exceptional postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.00" steps="3"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.16" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="26"/></proof>
+  <goal name="VC gauss_jordan.16" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="31"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.17" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.17" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="86"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.18" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="29"/></proof>
+  <goal name="VC gauss_jordan.18" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.08" steps="102"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.19" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
+  <goal name="VC gauss_jordan.19" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.03" steps="35"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.20" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="38"/></proof>
+  <goal name="VC gauss_jordan.20" expl="out of loop bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.21" expl="exceptional postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
+  <goal name="VC gauss_jordan.21" expl="index in matrix bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="33"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.22" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="34"/></proof>
+  <goal name="VC gauss_jordan.22" expl="precondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="32"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.23" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="89"/></proof>
+  <goal name="VC gauss_jordan.23" expl="exceptional postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
   <goal name="VC gauss_jordan.24" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="29"/></proof>
   </goal>
   <goal name="VC gauss_jordan.25" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.03" steps="87"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.26" expl="out of loop bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.26" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.06" steps="103"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.27" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="36"/></proof>
+  <goal name="VC gauss_jordan.27" expl="loop invariant preservation" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="33"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.28" expl="precondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.02" steps="36"/></proof>
+  <goal name="VC gauss_jordan.28" expl="out of loop bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
   <goal name="VC gauss_jordan.29" expl="exceptional postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.00" steps="5"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
   <goal name="VC gauss_jordan.30" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="32"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="17"/></proof>
   </goal>
   <goal name="VC gauss_jordan.31" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
   </goal>
   <goal name="VC gauss_jordan.32" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC gauss_jordan.33" expl="loop invariant preservation" proved="true">
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.34" expl="out of loop bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.34" expl="postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.35" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="19"/></proof>
+  <goal name="VC gauss_jordan.35" expl="index in array bounds" proved="true">
+  <proof prover="2"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.36" expl="loop invariant preservation" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="24"/></proof>
+  <goal name="VC gauss_jordan.36" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.37" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.37" expl="array creation size" proved="true">
+  <proof prover="3"><result status="valid" time="0.05"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.38" expl="loop invariant preservation" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.38" expl="index in matrix bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.39" expl="postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC gauss_jordan.39" expl="index in array bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
   </goal>
   <goal name="VC gauss_jordan.40" expl="index in array bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC gauss_jordan.41" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.42" expl="array creation size" proved="true">
-  <proof prover="3"><result status="valid" time="0.05"/></proof>
+  <goal name="VC gauss_jordan.42" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="16"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.43" expl="index in matrix bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
+  <goal name="VC gauss_jordan.43" expl="out of loop bounds" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="6"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.44" expl="index in array bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="22"/></proof>
+  <goal name="VC gauss_jordan.1">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.45" expl="index in array bounds" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC gauss_jordan.3">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="15"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.46" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="20"/></proof>
+  <goal name="VC gauss_jordan.2">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="13"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.47" expl="postcondition" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="18"/></proof>
+  <goal name="VC gauss_jordan.4">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
-  <goal name="VC gauss_jordan.48" expl="out of loop bounds" proved="true">
-  <proof prover="0"><result status="valid" time="0.01" steps="8"/></proof>
+  <goal name="VC gauss_jordan.5">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="21"/></proof>
+  </goal>
+  <goal name="VC gauss_jordan.0">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="13"/></proof>
   </goal>
  </transf>
  </goal>
- <goal name="VC linear_decision" expl="VC for linear_decision" proved="true">
+ <goal name="VC fill_expr" expl="VC for fill_expr">
+ </goal>
+ <goal name="VC fill_ctx" expl="VC for fill_ctx">
+ </goal>
+ <goal name="VC fill_goal" expl="VC for fill_goal">
+ </goal>
+ <goal name="VC linear_decision" expl="VC for linear_decision">
  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="timeout" time="1.01"/></proof>
  <proof prover="1" obsolete="true"><result status="timeout" time="1.00"/></proof>
  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
- <transf name="split_goal_wp" proved="true" >
+ <transf name="split_goal_wp" >
   <goal name="VC linear_decision.0" expl="precondition" proved="true">
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
@@ -532,7 +563,8 @@
   <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC linear_decision.2" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <proof prover="0"><result status="valid" time="0.01" steps="15"/></proof>
+  <proof prover="2" obsolete="true"><result status="timeout" time="1.00"/></proof>
   </goal>
   <goal name="VC linear_decision.3" expl="array creation size" proved="true">
   <proof prover="2"><result status="valid" time="0.02"/></proof>
@@ -540,201 +572,392 @@
   <goal name="VC linear_decision.4" expl="array creation size" proved="true">
   <proof prover="2"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC linear_decision.5" expl="unreachable point" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="24"/></proof>
+  <goal name="VC linear_decision.5" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC linear_decision.6" expl="index in matrix bounds" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="87"/></proof>
+  <goal name="VC linear_decision.6" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.7" expl="index in matrix bounds" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="91"/></proof>
+  <goal name="VC linear_decision.7" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC linear_decision.8" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.8" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC linear_decision.9" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.05"/></proof>
+  <goal name="VC linear_decision.9" expl="precondition" proved="true">
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="18"/></proof>
   </goal>
   <goal name="VC linear_decision.10" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="40"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC linear_decision.11" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="23"/></proof>
+  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="24"/></proof>
+  <proof prover="2"><result status="valid" time="0.03"/></proof>
   </goal>
   <goal name="VC linear_decision.12" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="41"/></proof>
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC linear_decision.13" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.06"/></proof>
+  <goal name="VC linear_decision.13" expl="precondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
   <goal name="VC linear_decision.14" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="40"/></proof>
+  <proof prover="2"><result status="valid" time="0.03"/></proof>
   </goal>
-  <goal name="VC linear_decision.15" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="23"/></proof>
+  <goal name="VC linear_decision.15" expl="postcondition">
+  <proof prover="0" obsolete="true"><result status="timeout" time="4.96"/></proof>
   </goal>
-  <goal name="VC linear_decision.16" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="41"/></proof>
+  <goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.17" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
   <goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true">
   <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.19" expl="assertion" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC linear_decision.19" expl="postcondition" proved="true">
+  <proof prover="0"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
-  <goal name="VC linear_decision.20" expl="index in array bounds" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.00" steps="25"/></proof>
+  <goal name="VC linear_decision.20" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.00"/></proof>
   </goal>
-  <goal name="VC linear_decision.21" expl="index in array bounds" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="26"/></proof>
+  <goal name="VC linear_decision.21" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.22" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="29"/></proof>
+  <goal name="VC linear_decision.22" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.23" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="29"/></proof>
+  <goal name="VC linear_decision.23" expl="exceptional postcondition" proved="true">
+  <proof prover="2"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC linear_decision.24" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="57"/></proof>
+  <goal name="VC linear_decision.28">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="26"/></proof>
   </goal>
-  <goal name="VC linear_decision.25" expl="variant decrease" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="29"/></proof>
+  <goal name="VC linear_decision.38">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="22"/></proof>
   </goal>
-  <goal name="VC linear_decision.26" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="55"/></proof>
+  <goal name="VC linear_decision.16">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.06"/></proof>
   </goal>
-  <goal name="VC linear_decision.27" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="34"/></proof>
+  <goal name="VC linear_decision.12">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.05"/></proof>
   </goal>
-  <goal name="VC linear_decision.28" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="31"/></proof>
+  <goal name="VC linear_decision.55">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC linear_decision.29" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <goal name="VC linear_decision.52">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.04"/></proof>
   </goal>
-  <goal name="VC linear_decision.30" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.5">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="22"/></proof>
   </goal>
-  <goal name="VC linear_decision.31" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.45">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="19"/></proof>
   </goal>
-  <goal name="VC linear_decision.32" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="24"/></proof>
+  <goal name="VC linear_decision.25">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="26"/></proof>
   </goal>
-  <goal name="VC linear_decision.33" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="24"/></proof>
+  <goal name="VC linear_decision.35">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="22"/></proof>
   </goal>
-  <goal name="VC linear_decision.34" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="45"/></proof>
+  <goal name="VC linear_decision.17">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="38"/></proof>
   </goal>
-  <goal name="VC linear_decision.35" expl="variant decrease" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="24"/></proof>
+  <goal name="VC linear_decision.13">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.00" steps="38"/></proof>
   </goal>
-  <goal name="VC linear_decision.36" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="43"/></proof>
+  <goal name="VC linear_decision.57">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
   </goal>
-  <goal name="VC linear_decision.37" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="29"/></proof>
+  <goal name="VC linear_decision.54">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="35"/></proof>
   </goal>
-  <goal name="VC linear_decision.38" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="26"/></proof>
+  <goal name="VC linear_decision.30">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="31"/></proof>
   </goal>
-  <goal name="VC linear_decision.39" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.40">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="27"/></proof>
   </goal>
-  <goal name="VC linear_decision.40" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.26">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="26"/></proof>
   </goal>
-  <goal name="VC linear_decision.41" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.36">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="22"/></proof>
   </goal>
-  <goal name="VC linear_decision.42" expl="unreachable point" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="21"/></proof>
+  <goal name="VC linear_decision.18">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="21"/></proof>
   </goal>
-  <goal name="VC linear_decision.43" expl="index in array bounds" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="79"/></proof>
+  <goal name="VC linear_decision.14">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="21"/></proof>
   </goal>
-  <goal name="VC linear_decision.44" expl="index in array bounds" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.03" steps="86"/></proof>
+  <goal name="VC linear_decision.31">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="28"/></proof>
   </goal>
-  <goal name="VC linear_decision.45" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.41">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="24"/></proof>
   </goal>
-  <goal name="VC linear_decision.46" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <goal name="VC linear_decision.27">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="52"/></proof>
   </goal>
-  <goal name="VC linear_decision.47" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.02" steps="36"/></proof>
+  <goal name="VC linear_decision.37">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="43"/></proof>
   </goal>
-  <goal name="VC linear_decision.48" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="37"/></proof>
+  <goal name="VC linear_decision.19">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="39"/></proof>
   </goal>
-  <goal name="VC linear_decision.49" expl="variant decrease" proved="true">
-  <proof prover="2"><result status="valid" time="0.04"/></proof>
+  <goal name="VC linear_decision.56">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="34"/></proof>
   </goal>
-  <goal name="VC linear_decision.50" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="36"/></proof>
+  <goal name="VC linear_decision.15">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="39"/></proof>
   </goal>
-  <goal name="VC linear_decision.51" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.53">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="34"/></proof>
   </goal>
-  <goal name="VC linear_decision.52" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.29">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="50"/></proof>
   </goal>
-  <goal name="VC linear_decision.53" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.39">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="41"/></proof>
   </goal>
-  <goal name="VC linear_decision.54" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.7">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
   </goal>
-  <goal name="VC linear_decision.55" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.6">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="84"/></proof>
   </goal>
-  <goal name="VC linear_decision.56" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.10">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="81"/></proof>
   </goal>
-  <goal name="VC linear_decision.57" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.9">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="81"/></proof>
   </goal>
-  <goal name="VC linear_decision.58" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="20"/></proof>
+  <goal name="VC linear_decision.47">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.03" steps="76"/></proof>
   </goal>
-  <goal name="VC linear_decision.59" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.46">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.02" steps="76"/></proof>
   </goal>
-  <goal name="VC linear_decision.60" expl="precondition" proved="true">
-  <proof prover="0" timelimit="1" memlimit="1000"><result status="valid" time="0.01" steps="26"/></proof>
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC linear_decision.24">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.01" steps="23"/></proof>
   </goal>
-  <goal name="VC linear_decision.61" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.50">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="73"/></proof>
   </goal>
-  <goal name="VC linear_decision.62" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.49">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.03" steps="73"/></proof>
   </goal>
-  <goal name="VC linear_decision.63" expl="precondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.03"/></proof>
+  <goal name="VC linear_decision.23">
+  <proof prover="0" timelimit="1" memlimit="1000" obsolete="true"><result status="valid" time="0.00" steps="23"/></proof>
   </goal>
-  <goal name="VC linear_decision.64" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.32">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.00"/></proof>
   </goal>
-  <goal name="VC linear_decision.65" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.42">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.66" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.00"/></proof>
+  <goal name="VC linear_decision.33">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
   </goal>
-  <goal name="VC linear_decision.67" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.11">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.02" steps="3"/></proof>
   </goal>
-  <goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.02"/></proof>
+  <goal name="VC linear_decision.51">
+  <proof prover="0" obsolete="true"><result status="valid" time="0.01" steps="3"/></proof>
   </goal>
-  <goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true">
-  <proof prover="2"><result status="valid" time="0.01"/></proof>
+  <goal name="VC linear_decision.8">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.48">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.21">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.20">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC linear_decision.59">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.58">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.44">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.02"/></proof>
+  </goal>
+  <goal name="VC linear_decision.34">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.43">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.01"/></proof>
+  </goal>
+  <goal name="VC linear_decision.22">
+  <proof prover="2" obsolete="true"><result status="valid" time="0.03"/></proof>
+  </goal>
+ </transf>
+ </goal>
+</theory>
+<theory name="RealCoeffs" proved="true" sum="c2e470c836537254f7007d63f6693a29">
+ <goal name="VC rzero" expl="VC for rzero" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC rone" expl="VC for rone" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC radd" expl="VC for radd" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC rmul" expl="VC for rmul" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC ropp" expl="VC for ropp" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC req" expl="VC for req" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC rinv" expl="VC for rinv" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC rle" expl="VC for rle" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC czero" expl="VC for czero" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC cone" expl="VC for cone" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="zero_def" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="one_def" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC add" expl="VC for add" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC mul" expl="VC for mul" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC opp" expl="VC for opp" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC eq" expl="VC for eq" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="eq_def" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="VC inv" expl="VC for inv" proved="true">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.03"/></proof>
+ </goal>
+ <goal name="VC le" expl="VC for le" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+</theory>
+<theory name="LinearDecisionReal" proved="true" sum="b530cfecbc23428f062f49770f3b52a1">
+ <goal name="C.VC czero" expl="VC for czero" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.VC cone" expl="VC for cone" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.zero_def" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.one_def" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.VC add" expl="VC for add" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.VC mul" expl="VC for mul" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.VC opp" expl="VC for opp" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.VC eq" expl="VC for eq" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.eq_def" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+ <goal name="C.VC inv" expl="VC for inv" proved="true">
+ <proof prover="0" obsolete="true"><result status="unknown" time="0.01"/></proof>
+ <proof prover="3"><result status="valid" time="0.04"/></proof>
+ </goal>
+ <goal name="C.VC le" expl="VC for le" proved="true">
+ <proof prover="0"><result status="valid" time="0.00" steps="1"/></proof>
+ </goal>
+</theory>
+<theory name="RationalCoeffs" sum="335b439ff4826214f067ffae8ae5b2f0">
+ <goal name="VC rzero" expl="VC for rzero">
+ </goal>
+ <goal name="VC rone" expl="VC for rone">
+ </goal>
+ <goal name="VC gcd" expl="VC for gcd">
+ </goal>
+ <goal name="VC simp" expl="VC for simp">
+ </goal>
+ <goal name="VC radd" expl="VC for radd">
+ </goal>
+ <goal name="VC rmul" expl="VC for rmul">
+ </goal>
+ <goal name="VC ropp" expl="VC for ropp">
+ </goal>
+ <goal name="VC req" expl="VC for req">
+ </goal>
+ <goal name="VC rinv" expl="VC for rinv">
+ </goal>
+ <goal name="VC rle" expl="VC for rle">
+ </goal>
+</theory>
+<theory name="LinearDecisionRational" sum="4feae965f9954cc5120ad56cd4023cd3">
+ <goal name="C.VC czero" expl="VC for czero">
+ </goal>
+ <goal name="C.VC cone" expl="VC for cone">
+ </goal>
+ <goal name="C.zero_def">
+ </goal>
+ <goal name="C.one_def">
+ </goal>
+ <goal name="C.VC add" expl="VC for add">
+ </goal>
+ <goal name="C.VC mul" expl="VC for mul">
+ </goal>
+ <goal name="C.VC opp" expl="VC for opp">
+ </goal>
+ <goal name="C.VC eq" expl="VC for eq">
+ </goal>
+ <goal name="C.eq_def">
+ </goal>
+ <goal name="C.VC inv" expl="VC for inv">
+ </goal>
+ <goal name="C.VC le" expl="VC for le">
+ </goal>
+</theory>
+<theory name="Test" sum="20e422485d50758d8a121b35d1fb0bd3">
+ <goal name="g">
+ <transf name="introduce_premises" >
+  <goal name="g.0">
+  <transf name="reflection_f" arg1="linear_decision">
+   <goal name="g.0.0" expl="reification check">
+   </goal>
+   <goal name="g.0.1" proved="true">
+   <transf name="compute_in_goal" proved="true" >
+   </transf>
+   </goal>
+   <goal name="g.0.2" proved="true">
+   <transf name="compute_in_goal" proved="true" >
+   </transf>
+   </goal>
+   <goal name="g.0.3">
+   </goal>
+  </transf>
   </goal>
  </transf>
  </goal>
diff --git a/examples/in_progress/multiprecision/lineardecision/why3shapes.gz b/examples/in_progress/multiprecision/lineardecision/why3shapes.gz
index 5f5b70634c6303e39556ac96b46ada4413a12c6e..fed1874649e505bdd774b383a85f61c4a5e1110f 100644
GIT binary patch
literal 13387
zcmb2|=3oGW|8Hv}`(-RAJ=^`C%l7+%>da%Od0u3#33$Q6!ePsAJz2lI@xW&H-C9e%
zPQ6++H-5icKS%kl_G-5!>n3elzFJXJ=|#z>#j^818r*7Ov75X-?)m~*@wKZj-TK8a
z<%a$4zaJy_R{z)e8(vvoZolBES4zlM!<QY6!IxyFGWBxaY+L!`?(HIbi`TZtW*ktc
zy2kmGH{;~4B|OCq!7uAu%-4Tj{pt4Z@AmiF>;G^6^l$m?dfvC|<MZDi?w5a8|97LD
z-9M?g{cG3PSARRacK6l)R<#?pTiKld`E6U@($@?7;`6U|uk7Ib|Lx!OqR)T!sO>ts
zQ?0)HwyEsCy`kpK#+)(&kqm1DLc)%$G`QJx?`hL=zpd}~bd~SlbN0UD@(r^Nt&Hjp
zdp=>2YQNEi8B^Bt702~nIsctmns=sP%(<1va=a#;7rVhKU(7Tw;m1z~r)nja=9Mh5
z!CYz~i%oW|SYtD(RO@v4lHd2=vBws1S$S;U(z#QMB_T6K$<6E2AC<iC`{&+kQgahk
zc)fsQX-e6&EFV`@<xS~kZO^Z+PyAP~I`8Ar{=eeS#O8mW|CRIXVU2t83-`|tsNGj_
z=kB4;k3IhUY>%FBYMa~XuZy34JGOWAwRKUc>nnIyME_o&_~De1#?SrR&6ur%Qyw^l
zHfdacw3X+;@9PiW{@omN>9>&G6o2t6%}ZWJ7k^Ib{JQF*xwF9m$C(`0u1alqwkC9q
zs54`F&4%;$_Ub3ae0u%+dU?M1`MNW=*L1C`h-cb(UhrUb;M<73=2jE0W&YgODsZ6N
zzizi?tK`%@rc0Y{S#vRRuYNKoN&ZkMbK<W?gK&?&e>;vXV&z>Y@%BWOVP%TNk&ce2
zHwnu=T{uwl>$YxMx8JOU&8ebmiZwTx9!<Npb;cg+fM+!e?Dm>IiB*|i%F`&iVZj1h
zwdKkR({t`@E-#mVXFmJ0$Lpf%4SH`cA8cN8tjN3ZNSAv5F~!uwyIj-?B37MSFsJBQ
zq($VDjfUAd&+b1+TXFNLz|OW9&)sJt&**a-YrN2s4nKcp{ftX5@3-%}*S>#m-R0Vw
zzrH`ddz*j%Ju~OZAEk-gc5N~$JKJ^El~1Xzs^-`6?z>XQ;v`f8SHIfBChT%G_T<Hl
zCyc~6M6OPo^>**(>C?X54UCbiv3K_La!;C`wb89mWU<<Rc6C4f9aBA{Oa3Rvi6?m~
zb>Et`!0X(x8!HY(s4}ngV*NW|QQfE0noTDkt*BiytJF`0<)H8cv3~t)d21!bTaL=K
zKK=GdfjjZ)gT>}ovz(7|pZ>Dch)dUSs={0s(>>MSpZ(ukRsSlgBKY3FzyIuyHt*g4
z`|II9)Ap;B{<*&Y4%hwaeR}!*Pv_tF|D~Sy`-k#btC?5U&Mug;|NZIT<=YvyH!OeE
zAKx}V?*BEr|L^~2<UIKBd*Ox>{`@?<XQrQ)*wy`PH)xUBBfM{3(I(B~I(GWf8xzij
zh|50M{NZ2ikNWeoxVCJp{Pyr`{ZwHo`#W61H9HSwFflvrs{VZ1-^lNf%2U-VF|&#e
z&RUgy<(9Ow;;I=UtpDG9y&Y3G*}nh1^zjdeuUOC1iv7~J`{DEG{eRv*TjOfd8?3(J
z?u1_~`u+0%EX?h`u5+?^Ep-3$_8Xp6+wLd*+AgzUayU=O(SH&1*LJ(@=sobL`AC4<
z8Dnk5bYmy`*5BVheGpv4tS?tDGPB&Db8@I|vrCvzt5=4U>I$u+(yn$H!Aw(>4BK`p
zxbz1J&Ioz3qO-mKfAO!~dv^XWVE7YIv2>k5U48NAt?tPaHk^66re!6Y^2Hgcop+m#
zyq{qz8G9w2`K9uitE|Z-te2|TGyi%lVSg)pYfV>h(&tHnY}{TC1Y5b|(!U6CF8h>M
z;+{Y4-OGQTCr>-yvYsL`$>P<C$TxzspJ-{ihwiAIlwf#d>iv5k+v1N&nVhq*ejw?g
zt7PNn?HlSXUU>EB?ALq3ctTptS(a+KzRnTZHGA$>rx}Z`bIHH^&-(3yX6%;NdbdKw
z-)@a{;ry<8AY`WR%GRE<PS>^wXXVIht@3XB@@!B4@?8nbXG^PORz2DM&{OEPD5uWC
zC$D18E=^M0a*fL&YWl3Rq9!kSR&WZIN@zY@?a4Ditc`C~i^z@NGjcX)u9|gwN$9R=
zYAe^fP3F`6zo;gGY28JYKB1!=$*Rs$(%anyW82;waXR|uu&K$)n^E6O3?g@LJ9Rbs
z@lE5bFoEt9h5{0uMvILP*4EB4VcPfd+m-3%)z23jdYm|zbUa&2WkJV9VM`|Y1!B2J
zH$QzpMOilS-UE+Ui!Fq>q>M5Y*`hUXIGx(OdgZQ=si8+}B>TSfa-MEx;cS)pc|yo&
zb0(uq7U#m&pjWHbe&*5>Tv9v#!_GAamtR_vy+^Fe`^>T3JdR8?%KKKY{h6>$t$O*w
zm_?q`HIAs4eX-h9;_JTIz3@j!57#0#wWJC2ybrvaW9<3QZsJn@_xJ8U?YsRVcmEo5
zFCBG@67}|~tFL4a9*|pqIotd}&}Hd-w!r+yJ?oBY>7I%!(n;}b%2D7?lGVR)`2O~f
zQ7?s>lFKe#i`Xpe8DjaP=YgU6u5BM*eb3mlNl{B9SB^(;j?kS@Uzu9gXCkLX)xMoJ
zGjLE@vFMhSr0x`xNX~ykMOUn*1TAO1J3r2|CE(t(bMNwRlwDqPPV+~E%l>tnotH;m
zS!!5Sw=zqAS>0##t97$pFW<@89bV%4Crr5JdP^{`8V{ea+w2%4OOE9N`y*nW33-c%
ziTU1{6={Ej<@|I1s(Bu^ychT9u)eXE;VxBnIk$My#1m^KXRKYX8DelUUHZh8Mf3LV
z++D5ys6Og^#oupV{~iq#VkuiNWq#G1Z42LY?bsrB!uRGDe)c2QZ&f%e!;Z}j-*w<T
zyM~dS(w<dOB}YRqL>6oK+^YzfWyiHp`$@(2=kcyBm!qn_7s}t-6>w&wS|>k4t9W+V
zqr;nz>=D_-+3%h)=Xp@|+|2!FeWw=PzWb8<t?^#h`WJ_KuICjqmbr<f8Ci&^Hj1is
zTGxJ6V>6j$QLyHegwvz`Lz&O_*7)B4zWegWx5ht?%Ul0R<o~~KLX;`fm1i70O+CV|
zmrp#=e&$~HvB-5o1`#52jpdssiccx~x`;hX^-DP8R`YkScAc|V2rT}x{ZFC5veq+)
zW=v&WrlJ#+{cwV5GMjYG&b*Ds%X9B!vTk?UUGyM4N#X0-WB(^ze|qhx?4J#*rLO;Y
z*gA{-LelJJ4>iv_k{0T%dKuZJUnMr}&$8{AZ|2g<F}Kh)n|0N(fRjodD!0lGc}$si
zeU_Tb6X(kR{Tn(CnccSOdS~;tAkX1ef9&nA^B6Dkmlw#*dYr9Z@$b*^|1;XsKR*3=
z<876sy};t&U2DIppXJ=-#=J1h|AFr*Hao$E{W90MnQpGSwmqTjV7`4>zCrba@2y{U
zN$#3`tl;Fvud2U;L?#9Ny;b%p?CoORqf3pqf76)pXP&4{#&xFECwrT{J{WFz+uN~E
zsB7;kb{-))ZwA#p=aVmPYd!ix#Um_N-*cV#BA@-TO24ynF7K;Z9~t7_bnV`&O%r!D
z{qH%vGy5OgCP(qdE$&hdvxC;m%bjMi(dzBSRj+-&*~osbT>IV5DgI~=ztvN%yfqn9
z8IRO>UwJmUQS7t0;+vPzn{Nom{ZlOcqjLK$^UHW12gLv_PVFjn!JNeSq_vG(ziEm7
zkrMm8E3V%4_FeOg0JC2Sn^=D4D&2cFXUmc8rYx_QzI-$9?%$&SZ`R2*M9o;Z*KBq6
z)Oz_D-LIHmy*~LoVREy?7S7zKankcevwhwKG5ut}bgt!##oGtxrkyp9e)DT*|5SnU
zu>V)=b~BxcKXkgcSlT+_qSCXQj;pktZoie#$qJprvT0gOPFK2VE633V;>Tn^^Z70R
zzB70$|Cx~5`vrV+y0^=8AD(q2VzSphiBuB~7cZa7d`{K1e;yf6(ckw*A@^J;kI3G&
zQ;auHjBt4r9`4f6bRsAyaQ5EN4gP{H+;jg+X>Gm8QpNF~F?WOIghZpLCR28XlNx&K
zT!a?|_nY1E&o!&%P_ufT9H<x2yFes5<kZszt=tkb_{#n!@4azB_q%Vm#P++_7C$XY
z*uN-eck02nQx$HTmPBo`d3oih)~R>jmj7J)&Ph7feRh;|`bl}4@MNuGgSQIqBJ-Z;
zcvwVRHu*}dztLWD@5^k(AfL$RNi%P|Z5MGaX1b=>Qr2Q@XOUhmyCbvr)zj3s?9*0!
z3*WkXvh8i{ThV{rFN8kT*`_to{M^QK(}GL;Y&7!a=3T!lwolxjQ~s&xvlgjaA#=W7
zROO8KIpD*$)$rFXUSn<TEv*yxE|4h;x4b2JQdamgYgs~WgMC99_fD%Y)-6FN)--K5
zWLtkgMSOkhNxkS_MHe6TyYz}p{lZq$Dpl)vrA<ld84r^{LvfV*Qo#*N1YG`S?bX}!
zx;)@xQGLMs!~VPl+M90Za+R#`sL|5cX<21|Y^#Xfl;4N#bNBz)xpn^wW1cGtYU;Cn
z_WerQoIl%sVV4PGX2Fv+bvjPsK9|0?KM07_Xk7fjc4~mi7U8p}OxY6y+h)94>Kp!h
z-|s@Hr`vA-dOq{hSC$9fl5=&t?YAh`-m?;KSY*I_(VUret^u3YKC#Wr7pLyMZT2iW
z_IFIc``LeDSNv@b;6K_LQLHrC$@7izau&wg#G_Ltg-#dTwIJfYbyM@zzJo_Hjx1c6
zpu!_o8+=HpIWv9j&xHj~Z$EuJf1)j~XLsheluZk_{XZiT#5PAw<XjBHvMuWNt@q<P
zciyvIba&a-xIY$=Av=zSrcL;%{?f<#h<&}_lA_FMv9jXvyGp)ae}4M%Q}3q4|5i)?
zRP38PRprddh`dbgPL_L@<`gkF<m?Ku3@FR(yY&2m->)K}1zH<Sb7uy9Fw$;`oBDHw
zW!Y_Iap_NW6CUQx-PSuxM<Mp>t5l1y+bk=zIkf$fpEc!5ZGQdoQ-tlBz_;_FZPbj4
zPIVM@>mT0#_tQJygNGZRs2t3_6sCDvBav<4TCb*i4w~K9(_@$?y{nI&mw9ixlwj|_
z8mkh8voqc~ep#jC@BiA=t$uD_%>6lhFZ^pu{t6cEza{D~yd=nN$H7+;wb4ouGI!+z
zc0W<nTH4bc_=b1EN6YAssal3Uvvc0x+bjJrj!$r%k)n?HMgHiE(eIl+EW60}=jE5J
zR&!F`3&<Ah?%4c1x}vV?*O$2xH)iked%F9$yKU1p*0*aoA5ZzcODOB}i+bB<WfrU5
zyC<EMv)kPCC|BcNLh8b+KKB-J&MOjHaYr=L$!9*V$NN;~Sy$gp;9R_P@(xL(thaNM
zzNi$fi7}P2jZ%2{$?Q|wx0b7~-|GI!zAm;y%d<1O=Gax2YaNT^majY4CVu<+-H%<a
z<r<Y;Ck(HJ6y1LC)Z2Uap?yw?!iV4SJPTZKBqEnn#4KpLm`3%rM{c6mHYF^{zRh%W
zbCa)WPxaetp<AAAtu1sC+*Z6(W_m`LXzR3X*(X{J-MqCpR;P$>a@iSiVnf6_jcv8|
zyH8FF+Glb61E)r6;HlzgYu56f@+in=QQ_lTp|!{)^85Dk_w_=De`@{tbi4n%_WhJ_
zyW{KT&hhwjdv~~J)mDl96CeJ`Z2P>SwOnR@o5TL)<vQDR*6;fCoIm;Zqna~k_G~cG
zmOsm-{;JHO{@sBGb4tCqWj#)cvfVAZ*x-H0bgKEbSE4T7B^h@<T-dp}F!``xukqRm
z$Nl$BKUVgkkax#Y_vrGpFIVrrpSv)_efhFozh6#@EIOuopZBk^d423MULmH;aLL^X
zmWP~gC&YW5E)96KquohGGxGJ3by>Nq>&5Im4%E-PctUSN=E9QA`O1Y=2U-p(`)Ks2
zeMz;bycZoYQM!}&fK{K@ow74Rh6yWm>Q6|BrxxxM{%4VM$T20yZ}$#y+oEo{op<Ga
zhW7sn>%Zl4+^zq~YxXLYH;Yd>R5)DH5KMkB?ZO4|!+us<s~KwI|G5c&ZusN7U;in;
z{)zk3ZsvVjZvN!_ny2U2G%-)S<+<|CzRt`=I)(vhlNYaiBv<58$l{eTt3a?NCcE*g
z&?nDu^IiX2HcH7neQ;A+YuTn;V`EjND%srII~Km(_xX-drM?{N<L&vMSlp~#o^Sqe
zBV~q4OJC0IbsIZOC$y)z%2{xJ)r}UIopVg<;kwU{o;ZY>__1DllYBaqGh86`-DihO
zesU*VEADW~*nA5NICFMW=v6TnotQ+Qr);yDDkOZ_X69&p><ZhuwjuV&`WC}CTe3CJ
z?vPT7NZVE1&RZO9SDRUvaVx|0qDb7Ey|)r9^FI1i|J=n@{liP((~8ws18oeZC;0ls
zEs_n4c;w+wczOE8U7NG+Ms9ugMy}EFwayv$qvEsv2Bhy!zjgY0=#9hSwE-oqZ*ItN
zPW>9?s`K{9Qn5))$7TrJ%KW&gv!`-Sg_-|pH_Zpz?&&J#CFxeBBr_ye?tT3%;B>^=
zmm-P1CsrOPl=fghyhlHU`S`v+A5Yx;^^mn8IpIUX_n>PEcY~Cot*!;^46?S%SrlN)
zk@%KZ?zXLc;fG}I=WAtV-<^Hh|F+#Ue*InLGh|EnPqd#u+M*RTsjDcbW=llxjY6M8
zjFI`qOq*}7FFx}(U1r0%V&Bh4=CZB4ygxViDyu-U%r1WCg$b+pk1c7@3tW-(Jvr+q
zd#<Y4>(Euf9_8EES9iaBraL7#KkRm$`NbFVQoQe0@m2rGdb!nc?M?o*H~Zr^%>Nm4
zrtI`n-MpKh6sK%EFrkHC^XY~eVy4proV8|7EXY@UA07IdXAW;gxU*;P-?X)})FhtX
zGHU$V|K{BLHOFQdOyiP?d9uxZ%YvRMYfs%i<hk;%=Emg<_NWBPb9jm$&Gq#14&A!#
zj*lSE)|Q0uvVSWx-+Z~d@WX`7pTkt*o=f!pc$MMB6;Py5cxBqP-)o*vJ7cw5$zw~@
z@kN<E>%Q09^#2iD`%dGN+P%BNL5IJ6?l)lzowG-{^`pkIeXYlxX6J;=nUl8mjp&6R
zq9%2$z5h8f_O0pMlMyVG{!PN`pn#D|?vYQyr&d1mIk4fL#-1rXt5u&S>TQ&Z{XcW*
z;?16yD?87r&AlYm`{ef-HD0G##|}G4HBWw_+{O`@G+|mO6Lb65mdjp$^^b)8Drk7>
zwQ3_@Z<u@ZHs0$~A6}jLa8vf-)az~8^S;Xoc!*{PyNU`~7AdM;7Ag-iiZPCvJpC1y
ze8QgRi)#90HVG7etkF9CJ89bY!jSNNPm?wrzBF~(QY+RcQ;xPQ^2?aCO3QtIP{jvZ
zfBQQ==M-0pb>C*$cO}ijr$a0Ceba=Amzxg${r%xv^MT-HadW>deSP)Y=f?}#YwL~`
zl)wMBa>?Cwr@mD`_<gzOidz1>`jWn9!D~OuRqw9){7~XhLa*3rMzh;mA9paMs5}u0
zTdSb`{LvQSr-#=+yu13_kwu>C){3v``@FL*`u<Cw1D`tXFZ@%Iz_9GDS9&_9*wypw
z%F9%&R{P2J>&%#~TJ&s#)V4od=l3_|316(>_bh*Oa-;6CEmL2ea{6?uZ~dG-d|gME
zxy&<P^5@gChg;%5Cq4Z5;i~4^*yt>~lYjXX4A%MPea&D0v|IOK?Z1VaFN?bioDB@w
zUM~7-uZgD6KJPzyN0}KDmat5Wj6Szh?ab7#Dqf1ul|8<n&bwiDxr!~=-9+w4T1{1&
z?4!BY4RWvFZ)Lb_@#0+Q`#n5-ZXe%>ZtxJ;b%WJ5V|h$M@3pPktQzc`F)Qy@J*~;x
zx!aE;bmg0?w|8&<|8;vn-Mzeqti6{0{@3^BeqHH#;`Q~(f2Xw7?K`FZu;EI{&OdkZ
zSG;eScgRP5$?NCIJEy-k<2ia|Nw<K6sCSOK=9KW8lT+1~@K@}re)#_3bbk4`zw>v0
zx7;&#ciFA3@-8#8$v;cJS^X6>E8_jVcKLF-^FNEi)qXrpx_p1n{LFhR_gwLbn*Aeq
z!N23viq{IOOiKH9ZN-xw)md4sYKfWR$sNZk#V2<MDBIS|V*j<~Q2KWRkHgz8|2lBe
zfJfu8qR8T?crJr1F4drGSGH-J9Q%1-<#c;*cd^+QS^n7{TDJ0~dF;1>lHI!B%i7eg
za_g;G^YHBQulu|*-fN^NX>>mI5A#y*JZBJf<>$eB+yCiC-J1ROsDyt1ryAZXG5xc4
z$L2fim)q(n9=yUsAv*T#+h_Y<g;*=CX{ihC`Ks7bw*AMerKxWZW=SuUvtqd#{%E(?
zAF0CsqJr`cP6F<a0%mTyU=VHOF5jr5GF@W5+e*{iv_<whc6HAS_-<MCa_BA))HE`U
zC|vZU_f%8@clCDukH7X!e_0Y`&A5-XFZ;5PaYuJ@X?Ifh8R2#3iw*R0&;3r}|IIV)
zcHY&qpK}#r=X)mI5#4*I;I=ArWaJjcwI7{sb9+AUpU1TDyyBEun^@*AZSn26)!XOo
z|K-uiMdnvl@v7xoyq1Z+#<b$o`$Z<fnaj`X&soPj!{X>B+q+Z4V!OB-GsJ#xl-B>Y
zGAwz%u2*!CZp54GarH9Gd+i=iNRZ%hwwAP6rtD+dGOb&^H7d#~M(BN=FVj5da4V03
z!UNenpLefpb}r(d(_bOWHAm84v&iZHv+swi6W&`?JbV=@o)H<nGB+jl__1XT8}{7V
zxVQd{%cZztw}Ri(Y-D$^akiC;?O(ciN9AnWXyLAp_a<#vEc0obY*X^2H>J~#h_myY
zeR%h^<Z{iR=54GQzZTqX-@QH6uJ?~_qg}$)x8H7>v5IQDbVPBsmpduk)|FMwJ2AoX
z_&?6arZ+_PW~X^9dR&$~q4CLPK7~D2TRwAI8<jkHw&Byv4}W;Jl}>EC{pDY)=lsvR
z&QC76%Xl?8_xQmbl`MbOwcocD`ses#i<8evt018~h1)zy3wu{8{4tE3dROR$Sj4Nh
zyUuBc>&y=q+Ge_!<MSV-9j0c-UDP*B-Y)s;weYmcpU<s!J4S@R_j4}TEOW>)rYc~c
zz>|Q<+t_Z19xBUTtUd4YJlRLVo5Szc)#;^eacA~Z?tUe9o{uGm|6`%fl0Rq9UYDA%
zP|WMZx@nI>)DkZVowd%F)#!<uojvJzy?*WAh=<ZOIh;YwN%_5HFN9eiP7vW;m~Hl_
z>+zTNE$h1%q~AVN)0|auQ;5$idfJ1jwcZo+j?Q-7z>~mgq<Z9q&iB(|PTq3&&D1}5
z2_^Uo?W-+mUv;xHOY@Xn!D#{Ejd$(V332fUT#aqMAT{r4`WyXCN2i`o{+TAe*Z9fC
z>y9m^pE%-~elo7wloWCDR#pJ3?!`4(nwR!?nVs4$&v;QOGF_bU;JG~~w)4JD(DqpI
z(C3P4y4S(*wiAvzlU%ZdF1?dqUe99?y)m)6ZC%*;=E`^`=W4;<hb8(ClwADR{OQ|t
zMQzR_Jrd8?aQ}|kH0i<ODkts#Pp7PV<g#yT{lU(Rr_)wUeiZ!OtmU44Lhj$3T=TQN
z(X(gouNAAZx{{K+d;6T*t$BeeCs(iFslK55KCeO6uVho7cD~Qw13BWB&s`SZia9CF
zmweIX!Lw}M69Rj#&vZ@;b5q^m=TmPzoh7MtQTpE%)~ENq-B&l~1Fv0l-@U9)oSho!
z0>w{^u3efGb|t$=ApWi8K1bDEM#rSrJm2;;c(N<&$t?wEwX$75OQ?L>e`@jE%Sut4
z%x^dkZ|DDb;oaqrD|{NJ`0CE-eVBAYr1NX&#p^29|KG`b#rVJWqHitZ6LymaMv`lL
zjz3x%W#Z~&YI1NB@6%+3UlLJY-X5~5Fj&=fHjVSxD*Xu6M;YobdRKd?tg4HQda^$3
zd~<6&(_{GsuG5(pWM@viE)}S{DsY9stXHkls-Z0Ux4%8v&Cc(ZXSG`0EZtTiYkh8B
zxFNUvr!XH=x3H<rf9wyMYJR@<oBQ7lvs-`Oe%@aC@5j#R^$A<0wnTVHJ51CHonyCc
z%SRnYyX+3TW<6Dj+NqcAqu1Py{c63erT$}WqxA$+#V}>RxSM7>^OavsaN6y)Jk`qf
zwqVi0sCcO<M~yT~*sq`eVC}qb|6HLjQk8#IC(7sSjys_ev_|D#-uL;Iib8EOZxj_h
zy{O^q`7W&OcAoW?e7S3ln=+?KIxZ4;JG(mg+_XaiE0!MBs1~n$_r0R+#2Uq0X6##j
zY`K$v=b`g<@A&=FFLwW1H8b$;HEn}xX=%O(Yi?c+ka;0t)AePCPK=HFf->fEYpMPl
z`l0!H&u+in`X_G3{$c}mE(OCV5xtN}D|H1!doFI@?BcZE@|LXTuhaaq=i26ERvEpR
z6S6j}FJp`M#0lOx;wD!Xs4QCgVsdI-1-t6mpBJY8s3{fr>BZo7ep^Gc{DHtYTZs>k
zu6q1XTFN3B&{4YOk`B+QRN3`+gqgTG)_wkMY&_@P>bpC)Ue3$e9{t2}_U_Uh?U}A@
z1yf5l%r&aKbAm61Rs5V!UryRY&Cc&zryDF;aCydA_4j(e?j4lkY22)4-8qX(cvl2t
z(K(^*o&}2zFYVs;{6j)*tJ1zd7I8n9DqK#V@X|D;N`6!0oL))OD@#_SuD$TKBsp(k
zZc5K?&&AL7$-JKXe3Mz!|Czga(qr37r$5}N^|fK6%$!3azMrBdE_BlQ-=NZ`x3lX(
zc8!E`9mk^mH6|Qc$|n|VegCsYA?C4Rn^4HoH##q;ncYv}=kj$aiHw>5xiY!#$^170
zu3b4ndE&1t3yWu&vQACn&WV;1vOB-Q<YE0Pxn1FFCozA&zdwfW;=?<qZ!T(_&#&JZ
zecxWbm}6s!_nq&bG|D&YY~7qtyJ2HbqE+(^F1<SA=chTHQ?q^4%nX^5wjG>!Y{g{W
zqg)$(Zl88b&wtyV@HOmL+{T&yjeKg;GCU@W)fyjMF5=q7Bci`?cDS{){CpJ=Y4_CQ
zH{VQ}`uK$244$biYK=Dv%&wd$%lxby?N)7L$KJhc$3KqQyG?%^3si0C(O$i0P2R_q
z?Qv`7C3yYyy6{NnQOUj!&y#m*Z+IWY+Z{Ng_QQlt4<{rU-{!HD40&{Sfo~@J`U2VQ
zw)@`e@2gK}Kjb8Nob_fxjn<s*-d0hr{v&EZ*I88WxA@&z<!{q^>}1xdPVZA)1~Vsc
zb6femwR`VjBd=EbInBr5N3yL>!Y$s#NzY~Wz4iHf{&<o4!`$`{@2|&+J)clJmGh^?
zlZOjS-+%n6xBBP|-JfZXWskF*l3qW5`TMYws{QZ9JN9U5RhBG^kj~*flhf3_Gem1q
zfUV2Rf7_j_e*J#F{{8&>`pY`DS01mFn)5P`<F4(KUtfOwZG3RH{oKC8x?vap+EnxA
zJjt5)JE`uvZr;~KgR(i=UaXs$Uf<dmz}+@=Q-n*;A*O}<@3)$(D_%Msqj@~|^5t_y
zfg73yULLCxb1KQYP_psstFrx@v&{J#^z&3Ae;uBEI)8@htB@kOHK7eF*)l4>2CUpx
zlgq{0Z#pe2@=ej{x%MY7%)XxQUGd**#iQ5!xnXaAKHM+wIx9?8YQ1sB%aa%HE6ED2
zxi<UvR^K^YnLi&-Ik!zUE_ZkG`OU{pT(3H{kTK3qhV4PXpPpHdP57-|p60i|vq(DJ
z=;*ie9H+~pzI#tmnV)XG@~grVb@nXD{;B#7Ldi#zeqC!aS$I8h>c^semmEvC$G-Tt
zj@?xCQ-<d^_FNq=fyY~YmmE;t=5=P?s+-5xtlA#^b-Px)j^2SAyLUYf^nIu>&1`b$
ztSRcLDi2iLISn^1Ut;z>@b6ODo;gomnN(Ix+8$YZ+*b7XYV%!hHov~wa`dWn{G$G2
z-aIM_)*C{!QdTFe@?6MrODoY!{M@wF`^xvu$g^k+&YSVMbJ^F>7u{25ZvNRCxyRpb
z^7(HcKg?+Sv-yDCjspP)qe}KwEa0)6q?lin+P{cdT;Wyz<(&8S^A|U^7QdXrzfFDS
zHR0sPI+wpT8_01*UC+ASd_li|=2wLoz0r}2FRBPwaxUxjGh9}-JJ4Y2WFb*4?W1p5
zZ_ahzw8LOwyG#DuNk-|X%a`q5^y%Y*{DYg>?%MH{Y}{Jsk#Qm=Y*Aj)!!;H0hB{(N
z8Pna=Z}n_Af1_<h%=dfCTOTi26*`A=^HsS$0y`#nWljI4`pNXhTgwjlOWWN2(;t5l
zagf<`#6iO1Rlr6Lr&U&2<-e~4g?!8__1brS!Lw`It>#D^nDeuD*OC78$k<(bK0e^P
zdGAl*@7Hn9D(?QR+q|{C^j`N#ZRxsO-6x+{%#_^On^|Y;;j#8ec`)a>;?t)hlg%Qn
zwOtNXZk<~rb?!jrsSMtA48_(}H-(})Uq0J5S#S9ahMoy?&t9JXdH1qi=i}W!JKUMW
zc*2|E=S2oNzXflZE&l&I$-u{PPvBQT)>TIt>0?<c?><Q~|D0epSyv|eaOOh(tChwd
zwoI(M%P~itN$mIotG0D%3wHPZIIXn3!&|8T^RwySZigH`6rh;b!dHCk&dY^Yx+gwd
zq<V?%<Hws}`ewIJ*C!o~=CWIzc|7U--y`>;<O&`4JO~ub5By%BSAD-#XNCU>z2B?!
z@8;f*ON@H4<*&9(-P^d7-QT_>nui@0+9ARnb8&ZB_}tUSsyOy-i7~hxWYV7J{&J4M
zMDh0jrQd@m-ruFYei{3@@WKG@b&rL=Kg=)Be|m7O<r+EvnC_>XN1jfNv0m}>Z{y26
z5!ZUD84Im)wJJF69d<9^iYy2y<#EY<-M_!(!cN0my?GbcizMG%#Cc@thMc2U^1?bk
zU!NyFPxr#vt;&|V=B<q$F?*+PV9qtvTySY!tJ0(In;WCPPj1tHuCQeP9bdg4Z%?w;
zuU_u6Ew{)~R$YAB(eLU438sw~e79uXXpA_#+|fqjs+sLhp9Q&nFLc@>L_^Q8t^QMX
zwsW4knrZqkdjVzPhHqZ2T18Ky-zCU8ZjENIiCsSXp77#2t!%qvTl(eJUwECz?|#p@
zzn=dK8>{I8Q$>r_i&k-6xUM4DvHn!p(odl;Yv#{te8-;FajTGrRc4#XCa3;2+j4~@
zSDE+8o%peTisJ1Ci<1HUG0X|fTR*>Ljh8mP<=$&`C8I;=e)YAsJ>|!?bf&DnxOBmR
zNqwi{N_Twty#4;0?e|OGn%}ND8FP608=bq-H7oyGwQszo^61U&a|Nk;!f$O(EIT+c
zkn3;gtZ!eE`t&lSC$SgUT@@+5q__3=!A0L(SDW3|V|f`^^u?9wExVfAotsBGtY=FU
z&Nnf9^j~`6X%11Nb5GA0HcicN{_Qi(*~^Uk^0EZ|yy{uYPR>fT_?=hjQ~CP)&Yu^y
z@4vb3pUKS`+L?(D`O=)vKR@Z`dd_z5Jon`0bB|<><gU@=)0%e1%KLTg2d)Um4cojN
zW>4Cn#L@4_VbAPTFFifReR9#g>0&$l<QKSZwD(`?KU+rZS-<;ZyP5mb&ivXPdv2Zi
zySMW4d0#`DPqi-4UDiE2{7G}_hf~{9<aW;JsW@ue@b-dwsW@ZN=9|&xjNcm9t+-q9
zbDRAfy|=%ws_W*i+Ol`i>u2-wmb$WUUjNbE{KR$buL+)y!dD30THf+jYk>;O0;Wxq
z-Z$%pA9^y~AUA%-581<4-n|RTQQj(fvy9uom5c4R-24@*ZOuKUw|jjOQmf+ec_(np
z&$e!#Th3zrw1fI`iBCV~Y&Tf7b*lT;EuR+UdnWx3iKrG_vMqC~$n3e^oiY>FhATap
z#*urU<5#WHl&-ZWt0qq=(mFaput(4ANkWpyj(LASg*ABomwYt4tj{m!cA@s^6)MlI
zJ8vEN^JU@OT>BeWH-0&t`rB;=-;od20cO)?tXa~~<a?rRi^02?<cWGmg63ZT?O>{C
z!M>{XmTlJYEB}&T#xA%MF03Yb)O6(|<DjE^4S0oCbryg2YpPy+Vu9%9wcIa)TCF>6
za@UJ~e19Zm+26e9KF=avmu$QwapSIx@XR-#J2R!PODxL$(5WcMAz&KipUZm0`J|m?
zypU=^*mK(!JwwSi_j|$(B=;s6{o3gB%wq9=@squ8UW6p@Jrz5(XUe<XhKG+QC~Zsr
zyf0Fj^UvZUzn!aMdz1Ex=ErC9f7!e1L;s~M3twCjdYCHI-TS2HWUj1>O#SJQ#It-J
z|K@Y6Y+3appd|6RR^aI`x1MFq_4Bg(B^w(Z>vM0u%8%MPR&&ym7Hsaje4K5&bHk~e
z;w!45x;3}eduP>JuaU|sv^J~GuKlmM_=(94k=55P2DU^j{*XO?mA_A%`tF@3)%${%
zRZhvfR(nrdIrs0g#lMr+Ztl<K%m3ENEGp8*yC~mj+wDoFftR!#Ji;okyo&1hkkzqo
z?}vT!yY2PuZcIDStx@15v!+Sl#0{NyYwvCdSas7*Y+HVFyp1KFX~D6sgyPa`+Df9v
zPeZ0Ub3WR__d`>_R#M1R<FumJgK0r#LX|hB6<IbGHT1<?`uI4oO35WFVSUszE;s&1
zuWwI%zUHJAbJL`=zl5K>=-jYk+S4=J*1FBP9VfLyWlu*`TFpj}6<5yvyKt^m_jglz
zIfFg#eshnW{)TNqALDK;G1L7h<fg)O_Qf{Um+j~J*A`ga?*Dq%dcWevi30amH~;t7
z+CJ0t3+L^xD`qCtOY4?T&$LZ+H@A@2vTB{uY~C4=w1sC`$EuCxiqFn>UHJauIos8s
zN4J7h?X=ff^mb1El;g5UXy#Y8i~AbCM6~RSmN&OpJclV-Mx_7L(L={3aH>U3pPIIn
z|59*&@^N_!o|V@W9`1|CTw%!0#dZAm9giDjUv|Z`UJzDiYW6;7d?kx%yUL-co{}rq
zEV5-CE<8K5vAv$jP-xW*-%qWf>!#ND1)dR3m3lAO@#4E*LM?mCvmk~2&rO%To<8e(
z0ke31^27>e?JYV54RIY?SDU4%O00BO_`(}FbM>Pi8_%sgaPP^tgwlf#vcy`wJiRY0
z-0a;HAb40-`ReMtaD(NWjkII<+M~mgYkutTn^M2#QNX_~w@j9ueQ#Q6bNg>8?~R6q
z(;lqe;KsdCbp@B(9jVQxap|0Y?YS1-UuhhlQdIrH_2`1^-9AQA+J?Eexe~RrUC+II
zA=h}}7?+Cdw5;{h7UpG!3sgiO<NVJ0;eVaWzt<-P6vPSwBa=O6uXtL2io18qqZ3>Q
zOUq}h5&RXq>r<vs$w^(lh+xjE$EKaQ(-oclyRUZAhWpc%E=KQ~;&b7=Ui!`J+N{|x
z8^m_A+}Wuhd*J`7Gf5wW4s%)T+$NioA?Z40k+1Jhk(J$&Me7}3l)t+5T*=pYr2<nj
z3(w)H!N=AFW|(Ds3Ck4McYN|q!ODMavBmVV&ZB4UB-nJ6O+0!gu*$l$jCJ}3ZM{VO
zf=<O_uO^rGZ9eO?DJS#g{XJRjGDnX-{UE6*WqU`pW0|j-`()qSYQJCS>PU7STo5aE
z@SxNrNA{kKV`n7qwal?+cG~ZK{MKI;ZQal5QP0+M__Ce5${F0VR95HNF{Oi7Pc6z-
zidykdSl}1m^R{i*9Tqq(EL&d^a*%U!iP_exf1j8L?GjqIW9eg0_YCu9<2jlUOH0nS
ziL?tTIyfdWtef%WLhjQ4B7#v8PRo)u@tZC<@*`<ebMZAzjeWa<ex6d!x_{p0%e5P^
zx3;J$EWN?Eu$g5GTaQG(+M%A6YU(w&<5@3VR=$#b%4EV*FGZ_ujvoYFwL_a%@mQ|n
z__wP2!@m6eTkV&Yu@ncGrZXP9nX@uMEO&FA3Pan%w598gzF5ifqdRQt-R$Pfa_`O0
z=Sa#P6;j!9Rd6cvRH0j|{cP%<2Oet<-t0a*q*f<D)k?TP$?L~Kzt@wJm7-mbt#f^8
zJ!@<I9kmnx-Ch_uJ-Q*ZOXOxE&yBDRlP{@0vd~Ui|1I0Ug!jpcjQ_lsQYWnG*eII1
z`ItD<nq_S=TQk4=H=g<>b-unZ`Ol}Y6YQpWYL#!_A7wnbGJ2c;x@y5+$LAf7)qd#U
zb~Nk6>oTh=OI2>Dyx-!fps-X#-s#0kmo@x-9|D364rUeUYHpvj!^JwgL6ePdiKLv%
zi}}op7VvKM7O9!d#JQ}?{BjhJ$dV|pPakw@egxcmpZlV^$gA|-O}5!FohP+DEX9_*
zU|q$qt;##H!@*WHw(h>xF8QE!T00iaNnCSHuI&HTquVFVu`w6lUmg99-S_6pvT4zE
zeIi;J1{YcV=WNZ@yyLgj`CPxo-^=>>a)H0z-QDdzMbG{||0nNWznMX{tMB-|iF|IN
zIawrS@!gOgUvJmnv7f&_In48~XQ_GjYJ){(#!Du}o=LiK+f7(Bc*8O&)@v?o%Psvx
z_hl|n^?LiH!S!;{R3Y)lw{#z<9i2AGelFMY!yPfPH8O%BQi~X$tL`&7v$W!{NXmh&
zYM0zZl2%r=%X#?o$p%Vf7d%-Mq{GOzj7N-#J7$S$!_v>kZ?kOT`t<zlg0(w#O<Uo%
zafU{CPsx3;k5x%evu7`|*%s207<=~Q{Z-S<D^2HLG;^Hy@8%}0`#d=_Z*c^lm2&V&
z**%+mQgTpe=!xaxoie%mU+{N}|4sbv${EOJyj(&vk$0ii^-HIYu4uKL9l6Sd<+{Gr
z-H7}5w(Q%tuU38Q@i&@Nc#cJ}7)fjjyBdB}Z~Gg;ry;*f>W}bS^ZvE$i0GfncWs&0
zDsQV_O3BZ1y))Zx6}nzETWx18Iyd+Jk2%@>3p&<%DMhH{9NqnjC1tYDmAp&U7d!U%
zh8}P%x)%0<KX&)8Yi5j=7gzl+oHFZq`m8UH0=_Q^KPJMzb?Mdo%Kp7QE(>L}B$fAm
zs&smBc8XaN|DtnC^z&Cv^|#lzySpX#!l@VAz8iGB6lUaW)7^48>Ez5cf4v;n>(vDW
zJc^Q->BzV}J4X41&Z=Xf$GgH}11`+bXo}d{q$jODCFn&%vC)RQFO|~$-?^d=h^<ay
zzBE~)YLdT07ngwMeEZo=UHh~{n@@V#bZYOKkSKdZ=tqL1%E!%`D?TX%a)?hg)Qr!)
zsHCA~8Ja9y^*xhoR!)iP1m3G0A3qs}vcG+Fj7h2bUR!@)KyHrj(awurdLk3WGS`S*
zKbXQh?NBw>s%HO-2_o_VQxe4^s(&U}BzPozdB1o;B)fFX8oSjBZ>E?|QL<tFG~?Kk
z75a-8oZ0x}g=JE~ve=-0%h!)McvKfPX!`~8aws41X^P4#-(4WPc}2MJD*aVDmcA=I
zZz%L`X>4-6nEsF}PF-O0`^;TSAHCPyKkvasN4vgBB~H6*#dekd`gdjF{yz$asrAi{
z_0libM&F%ctk1sXw%;z-sOsCPllRUIV!!(;bIRw}^;_;l20gUtNZ#~k{<}{VqNg6c
z4z9knKVIjTg6sL;3JNb}rt;l%>b#k7d)Cx0i<v>*3^Q`>wO_YC+x7k5ipt|B7;g8f
zz1E+7>$~jLWcOXa)tByk9RApp>Cy&)N9+@ie^b9xGI!CEY4eX=dRw*r?!pgiFGSou
zom}fI^j_F?pNn~92E%j(v13Zo-BTiesvg|C>x)OhdOcgAJFC6Tn@&6R-VzgyttmQS
z$+mDuavtN;*<a%Y?!5Lk|8}cySJ;=9ITxl*Dc+rAocU19$9F>5xsR_NvERMy8X5Q~
zrPxtZD=k)IUO{Q%Qm6QzH)rbT?p+)jsi`ayXA;J-<FknG78SFY9`hHwKGr;!Yt_D8
zwsc~W=Ia(0&b1<sva+owYyQvOc|6(n?W*M`wevc*+!y+1XZ<FIe{EOUxo=M-)pe(5
zCHykqA}yD{jN9YZUdQAVp;aBc8?+8Rx_C-p18)>-^NDl0m5)B#{e5`)%S(QD^$!le
zZ&&u0wQsrn$f)_yf~a{vTTXg!Ik+#+^2gQPRqplH^><!fI`Q+MR><2Un*y{%OU3Rt
zMM#%V6j+tF@l&w-?7jAXZ+on$FZjLfuAK4yC#mey_xQ5(L~UAMc6WyG&G3Dy*<u^N
zI=*ncwU}8)=xxh`83$ghb(z1;;X|0p{);=i(n}oPUu+C+wocaZHFkG0xSO`PZ=F2<
z*Dtn0QVMP>EW-=eE|?r-CK499xM$XOA+NlP4U#7J8?T)_|2A>uzQs&UPtLE7k7wKH
z#qX^1CB|b~#Dqs8o-y~Dx*}R;Su@W#VLyAK?Z^4{t-t=gTONLCRm$^vy|hbibN^iC
zJZhh7^K!TP@>S;Ev-YXvh<=d2%T=4JeQPS~Il(Sgk+7$8GUl%I<8~JEQxCc-dH=rN
z0}~6wLyQaOZWqit^=9t04M$l;gE(WlDpp?qT55IY#pHjRm;A4;y=!Rf;S=S_{j)>m
zmgmN$rc)d4NHf%!#UD30_j2x;13TLEnu~tSHmkE<x0zf2eSNjwwSBd<f9AAsblrco
z-|^?OkoL+Ck@er!yqtIS?WsMEnO9tGHnjA)`pC0{OYU*m-KS}>dcJSCzi#yUzWT!f
t*=C-ueP*sD7o{f_t=24@w%}gCJoZm&dwvGE*-HJhXAL^bn<vJ|003!>OELfe

literal 10756
zcmb2|=3oGW|8Hxf`(?~0y{rDmWh;M}q1lnG`M?Q_CPQA6gbMj{i{kmjnAY#MnxNWy
zMXvh$_4x^RC(WE1Id$#rlJ7h@9;?>q#M!Ya?^9@YT))awVAFQX1&k&u44+TZtmxkP
zLcH95|BCna`+m&-^zrZC2f>UV&K;j5lfc`!wq1zVdOovtY0dAyyNm1{u6Q=qtoK<G
z)RdOXwXt|7la+<&-|rv3`PRk$`}5)B^WPudKYg5Ef9G!deEYlqKNjDu|D(L8GW`CZ
zpO2o(-hH@#uH6l5p7llhcCX&O{r#1<FSUjL{eArY>9ebqoHfgj3*DJJZ`y|cCCl^J
z0z56duWmBU$X0y6CD^dgblsAqzTW(^b+Y&W|I@QybZqj;V++G94MSFFy1TD%GD-0{
zo0E3pzwa@vmjN>Ai?yq@j6Spp95}^qv0!O%`TuS2bENNPZ0X7NRkPrZ(^_M6D)9HC
zz1I!aD&PHIX)p1`MKir@r@+SZhV4>5zH+)rJ;&#tIDI^7%1M`FuU0i*(|eLq^VKjV
z*2yR6$WMbk|CD>=-(8uz@9)m~gm+(7|1*{gywiUxk%#qc_~iK)W%pPq{GUF(T%lE`
zm+$Lh=g%MCc5U7qc7yk5^RCUwKmVP3cS?TCr?vx34Q2vOs*M`WUze$9@Win_cs%>V
zyML~FFOxavpL)*yEbh>Ub9e6e8O}5PmnOjJkuueEjg54GY09aii#>R({5~FS?^oSh
zKmGol{gwaoKHWaQ(pP2iB-IadOgZ_udNtWPoqhG#P1oic{V4c-bgT5zNj^eu1uN6q
zRX23LSUb_aG@$e{!;CtHGpr{Mp3hzqZh8Dk$W|-Q%N{#(G?Q0-a&+7{o$bl#Y<<T@
zLDqu|KF5@$p0CiDZeVn(CQeqN*v=vTo|Nk?D+8<W^;5%Sc-xkEPFb=-Px7R={Jr{J
z@j2(1x1PKkH``=xjp#z9vR0XD!G#BIMG7Xw7K=IREfLwz;eK{^_7R!MAFTx%eKgxW
z7M|QM+<V~Su7-P?lQ+h!oU<}AaOU#*_rELT>uNu5tG@B;>*wF)^Z)J0?kfEM)+M&|
z{izwIZ%y}Y5`X#ly#N0lvAT)(xwYAjrOk|S75#RtQ&1s5>FAsbH@29pz4q$O(j~Um
z9Vd_eTJ6WF8UDJ6%ZVkaNraR6+9FeN`>8iQzuPaj3ZHW@Vs6pKsGv2AZ|pfW?c!$9
zx0RVqb%jr@*m5JD+&A{V+m(}=`!sQrr<C(%$wJqNGma7O*6|nlPH1Ih$rY{$^qbiI
z(Qd-0QxfYxYOH#AxPANozrP-D%zl_#`F;NP|EkkoJ^pQP*Sq!4lq(P8?eB1|t~IT{
zFL$rLw0>57(lY+|PZsKvcP$olH&A@?XV<;P8{D>Hzn<N#{rSUj-#+H*HQ&AneCPiz
zzoll!&Y!A(zCAnt?b`pp{l`S*F0?2vJ8_Kb;}zHRiM>naUMM!X=ze_bEb)hrkAJwY
zf6FC9`OBlrv;S+l`^4Sj<o%!8c7;=j<K^Gm_v<HL6uQ^p*)hNDoa3jyRidUZ_Zmtr
zn#d{fs@wd1(a+$2HdnSwpY&f|_ak`W<hmbz9DnA{t}8FTrexO}roQd&fn6;7W$gY~
znAv@8b9(bq<mBh5H=b?NvJGo>tKTf?QWP<qwP<F<6Jr&xlil0CKC(>InP}3>@mK7f
z{i%L_fwz$#-g!@~+4Xs^!2#o@j1x{fjlv&(b28cC;^@A|yTgGmP%&=eLf*@P?f2{I
zZ!c5kP`8`kXLR$!hY$60<qrLO_^)||T+Zdf|Cj#T{f)hMum0D!#l{wovvhBYh;MP`
zUdN=8=HTl2@oMBZ{@@6HDW)hXrdRC^VeJVEX7~tBpH#}ll486l;?NV}j4vm2-o<Ij
zmu-9T_KMlvde7NsgJ%2QPy5_2Jp1GlxjlO8R=FGs+OR-?WqOY1irBtKTXx%QzM)<A
zK|AxP@#dQAoOe4ox?XHcT@rkfY34l5g|l<px;9<AYOb!WnNi$k?3#b8rRbze@y_4j
z8HcBTxp1y3Bi(jObajN0cH#A=i?_PdrDH!>amt6NE?u%`zR}|C&tq+-v1;#)QE*>A
z--fl$#N~+w-%>8a&hJZF_HGL9+EZb9NVd_uV3Bc;U&4yN3Y@N~-lnZ9rik{-wN9RV
z#(bjbG%shNz}qJ}uarM_`8};ZIJ=%{U7?cSRndzMVINj#M(W#jTjV-Do_x;gu$Z69
ztxtVbj1_(Yyw^5)_8gHsx;xyfWZJixM>d~d=rUc-TK(6v#mZ|gM)9<HMN6m|e$jHv
z-)r%JFSh7m{G1h8;tZ=al#_*{&pcVh{8nhU!YoZ&C%-SX>R%VI$j|Q4ke59ww&0Ul
zg;^Vu*0Gp%g^NnFKiu5)@wL%n-Dh4r_7WdheGfEjYcN$(dvLJp;;D~X#=G34_idOz
z`^Uv;bx}(-6}#`J)C7fPIIMc1F_ouvvR$rT-LDTHYu~-#(Yu`-Q<1!@t8wm=M{BNX
zCoQbr(RWpE!BRiddpwPvmXa&87PDU2>EIRlQsJ9OQQ`F$$LzO#j7sKQv~W$?q7&L%
zo|Yu6yBZX5F#hx3>&Kq`Ho2$DyK94B{pKSA5|%HN=Cy8I`XuNrE9>uCsff-auLTv)
zznJQ=d%NG8M#aagJQZ6OpZNbRYEIK9z4BKzj+W9FE!FFjA8ij>-qy#xEI9VdtEh{9
zCf^^0uc|ejc0O5HEwp6)j-_fl)^Q#e@)4Mqn#{Scs?Rbkc*e?YSAVy7FwTjJa=HJT
zY5g&Oi*?iF+F!IUb=@+(eR`GPCoe^gmsgKQY;^WqdL(YUYw7z`t34IJ|NUhb{Qvmc
z(b?ts@7DKCQrN(>wC3vLEj+2;xt9KP&^xtk?;ED|TP7d9I`dVT{cNs(Q+p;9UQ89{
zTD?Y7KuB|GsL1T2om%x`PSQ^*wm!e_+HyIj>UyF46s>6i1{XP<CrHlEKH?>~wOEDk
z-C;o`NzQ=mxtaHSeRIo7Hd_DnetjhOlKj3+TzhZDG)xt2y_hKN<j8PFjcxvk1f>t>
zRA;BoOS~dx$Gv=N)!%9R)|b0)m0NpY|L;wQ<*$8sA0M>Yts&~$Dy<zdn@f%MPI{!}
zm)@c?>txvCnx1dP21QMmUhR3&IE(YI+JbAxVsl^rVeQP?cka^k=C0hyd)-1AcDk_(
zHdVZE{By49;`Cf=t999ry|inpGei0A`0!ZOzcKiCea*W3*qDR<<*u(S>wbBibe@tX
zeL;XXQfPgQ_(j))X=?+dPuFp~{Ht_!@tgBVW~G6MQ2FW?b3|Qz*&4hJKhIQic@q5d
z$9IFmLt?l02;VLI`7EY!i~jCyk7qF*JS{8J{w&}v=e+%Ye#kF>IMc>Pes`$$W46U>
zW*C2DtBGE{Rd-$UNf&948W#62tsJ$_HpB^@xGQyY2S*WK-S17S53XsvzrW>kT94hK
z(+7X02rU#|Cf_C88{6ft+QEE2?#h*!KkEg2@_f19rC(=RJz0`{>Vx8hXlcPa97m%r
zHh=Fb^=j)by_fR1(~04=<B8N#pYT0C+utbd*4>pEyYIQqDrLvw?9y1z+z0l%AI5~%
zJL^6ApWt-ZYSOu|k|3|Gt_H`m<{o>iRUOm!bJwkE*@f>H9b>=F6w9;GqfgW^Y4NIl
zyN(UlMJAW_`zFu-P&9qnWAT^o<UGo)MMAZtq^B4ho8f&<<(GQ(##}A7r(eHcxN*Dc
zuWV`g{RN5}yyILnR8JYUELwX`vFkj)m6Y)7?(h5W@2`me?%;dnLe%W5*G}%|J9G6V
z^Q+${mkTW3rY4l-qxkHBh4aZnj7~X!E~dmq_TSUBzHrm;XHxgd_}?=)3zvWGf4kZE
zz#Y>)8QZsQWD@hQnJ2nrS9rxv+2%9q%BN;soV;mTiQ&Y_Oc!r1*l^(1uD=`iJ-&8n
z>C{!rd7m#h^3-ADFD)st@@vlLrYdL$v+T&a#O0J-`{$YVl<oJ+CWu|vVvAi|A?LWW
zM`qK}S51r7Sh||H7S<?uM6*2fdcObol&B1*_(Sy@SodhH2uzK(_^s7f7kX~%U6o6w
zwh@K)+pm6EIOB~|ff`G)M?{0sO{=M%Z)PnO@tb(Fety1L$?n?azCFA3Ze{F}zVV*-
zc3yNrrTU37UfZ`3a?h{))H{`R<Z^^|Y^HMQmX%uzr~FZTxyXr6wDF>bnI7}D3*n2q
zy${~z{pkMOcfaH<ONPm!Av2Fju~toW=6b}ls3^?i#!=JVxeu0EuDWi%RX-<i?fcB~
z_VQ`wTc-b-Z@fie-<s7I&Ztb@?0Qs7d79uRJ=MIo_2wJ4pXZd%S)_1<^M=b?tp#6Q
zJJQXLMJK#nU$K9S&E^bF<?7U;8&^+W?6Y6DVn)6|)>ejp4_e#Of*V(RS+VkIWryww
zXnnLgb+4$Jb?!@(Sx=1vAA2h9WtzY6*nNSm2fH2#)#k~vZTd9d;DXAO%azwd_VCZX
zv)gXNiS;hO=IH$8FE>%{zPrq!z3a#FCZXPYzYnf|`eEgr_y040pFO{{VBva$0B7DO
zD_tv(X>=V=f2(V}#osFM;*Wrqbt{%EZ(ks>TIk67?we26G-<p#rEA~Nd#*F|%&({u
zS9iUwyV0}g>9&8VOKNNxe}s9Zdp_pZi%beT6|Vm$dd~eQ1IMHiv#TE2eRq%D)7AdG
zbX~3PitC~Ow645Uy5jtFRj;-ii~2MPFI8=(5T4>IQ%}UXzc_WI>J<l{(bTA#H3Ekg
z967UD`^clqovF_2FC0)UfBNy$$Mq-Xxd;|s+M2s<;SP<2Ru^mWl9L*rc}~4N^Ev<F
z`Rj|;h5ILOPhER^zQ2^{yDy3>kN@znx_ItsKYx>m*4d4lCqD=d_N%WowY9KQ75lb+
z`5W2wX`L>IX2?J7oBqk^g|*yfc7_hVcwc#gC5u9hoW!H=SavN>x}j+C<xyIPk&*G7
zxal8rcD`#;QBSPYPrV?`vQ2Ob=Z4L8|AhFCni;-|YmwY+__#aQaP#Z`Uu1007{04B
z|2fm+l;PErbN{LS`Tbu0p4eXd#y6Hx>zmZotxmj-(NYNxxMO+o(yj|K6H5L+|03{t
z*PD(7U)V1#WX?QN!n^2tYE_KXbBVuSOOE||R-yF&iu<ecExRKFZ00LWEpJggbMEZ+
z-lmh0e-ApAKG2$U?U;1Na_im~=`6aNM5b7){{8tOk^Or~#}}Qi2TQbT<z4SpiMQCk
z-Fooh%3Jee-ZR{N8e+k_)8NsCRcn;nmJ7|kZKv-q^8Rdmxoe5)yHCak^vvFV36Sl2
z`nm1hwCB%RKTqHlO1OG+k%Yn2MS&-^HYP=0De;L8YM5cSmH%Au@1Ee?`Og+T?b$K$
zWX{YIretT0Twar?$+ld*;bAjwOv`#J`zQK3+m0EPEo$?>=Df^mXMHEO`WeT|Z(p9J
z?G!)Me4--uhSs-7lS9@k2WmNHzMtE4RrPf9n~u1s39@%R?!=V2ISO`flTRtW)_P3r
z*;C1vuQ$E<;pfw`>^*mBdh0u-56_lv^EKBjo3Fe?yQ009hwWQbP(hHcI%~uP%j=gi
zQ`HVG*IL~BqcF=h_v9s&J+|zhGW`#UNeZ~gPMoM2!JPeC#?@fwDxR>-x+PX3AKv{v
zen0Bg>Q2!|cg5<K&nl1p`u^U2ze~3^r=2+8U)ECo_hWnP*=f78`QDv-S8~7H_~84t
zpHB{cJ;AiD>vCOkvE#fmXXBUu%x_V<$;n(08T~YPmCV8k{Zl2T1V>z~G_Vj~yz!Ck
zYHQz)zf5(%H@x2WI_yjRjQzcLZ$G!+`qq)X(|XR8MXWPlB^lI7Jk9z3Mj_rP%iPxZ
zX6I@fOP(b=XWpvsk-W7nTJ61SR@UN)Pd013o#y0zK6t*2_ssYCHuecq&MQ3Oa1Cma
zPYherRJ!KqGEuJ5b<@=EOv_K7pMGV=?ks(Um&d=!FZgmf?%akq_u_wSy=!}uPhIB#
zr|g_Xc`KexYxT2CUv%hF(Ur{kTgA){n6BnkciZN%;+lx|CXOXqcBu^6i}WrwsTa;E
zyxem4rik&x?SV)3^_4t|>%V;NZv0Dbme`|L4d$F|=~%W)>uy)z)mfeAFNwYJw%k_h
z8zkp>Kc%k1@Jz#<89tZnI)A@p7V0$C+IQqti{$P7mA7)*QYwXNwrXx+6;IzI>UCz0
ztmu*}m!4bnM{sptJh-WG=`Xv@O6QHV{r+6|b~Ke!$8YNzla@mlw4Y^on^|q`=ssfl
z?4{sBW7VxoxkQaMl~wjU3F!4@oO~l{;ZDux9SqV|cba}%&5!F`H><SLE9Q$&QNpZg
zecu-5d&i_1{j2GkVa2<1K1<+SPafa8i&^u;6TbIX-8ODn6SdDUI#P2}pv7#_>e);w
zp=%R&TX5LC-!iK_>a6u%w+GMW+Rfp6VSQItBH~ra_wKOIdl+`to0#qhXFZ-K>Ui}|
z(ZX9Q`%0B~-<~lKnSF9+?v*v%@2$3`i%r^L@bUNjH!K-pO?T~QP4d3se%!Y`br;8$
z$4iz6&X6;*&)z26e|Y|^+~dWc?Rh+1-`;GUrW2^1TC=q4(Pyi|rj56D_Ss(D<z+Na
zIwGlcQ)=GHM<Le#IF4wF1Pgckay|PxEQ9}Os%_Kn4X1NAoD)5$BUj9Mt#{QEo-ph7
ztLGB8sz<QT3^;VdLv&`^LJ@V7F4w^D4<~PCyj04rekRpnv1NsG{Dr9WwR(;kQ5~+u
z1*@Kh-a3}C{#x*s?+#nL7A1S=8tX(R?oew^jL)qVw5!#UKQGH|U3lTPT<U7CvpkP#
zmU3-dA965n>8t4lF{k%5&&<8PCct9NDJ|n7KT9F8!pRDmQ=dmV^6%Zge~Y5!oW8kV
z+SUFpy!vlPWc{6>dZ~8X_x{S8UjOxcp{SB<BR08&A=aztROVx4iQ<DhBchpa>Yj^<
zV79Eak7d4?ovlz+%bT*iRQ#GlK_YL;s*1NUA7^zwTDp0r)sz>d9EZXcmq%pzO^saa
zx9iok9VK$%mO<0%#g4FDf42Eth)AQZY1XEIMOoTAI1V*j=RJSv(CxR)3N>8Z`Q^>U
zT^bD5-G-HyZWtxa5_>Ca&^>eCjDycNY6&QdgogLA_F9y^N%lFYH9a^w#>Gx`>5l&r
z_i88kO%2|9JR)>X>k>Jpg&+UixtL}1{G;#gm?>``C;b-oyJK@Y{Q1eq<1hNVpYQEo
z+E=)}EbOzLN#%!y9V-RuUWIyB3%H(tCeU*}F8a*7Ew6vQ?Emnv^!L#vo>zSCzUkoq
zy3p>p#lx2y=l}h^Tp`KA)nLw1asMv)=B56frfGAnS`25;)-2ks^{oHPPvsX(+-28!
zOO`7*6o<Z*>zZV1nH*z%S^wO^+;df)%YVB@UDL`uQgt%7G=KgrFaN7Q6Zgq6ukz1a
z`{mum#+Z*;UaOD##l5(wQnTfJXpz{;T88T~E)|wcob3rpQS*BX!bK+Sx8|A|og}fG
zX`$WO?GrvTF8Q5Voa>y@!g(c8^ve3Yt!H*De?QGpx;XaesdpRq2UyA<;}AE|?f>%K
z#N$R`-1g+{&qMjQx?C{quIf$kc9b{TwL&raZPVv(9T)1`?%UT^{r!Kh{>;O>v(1;k
z;xANppI>ZP?7F<;QvZet-j{X%{!$T54mvS2?`NveL!-Rg{fU*q7a#3>XVvw!U-w{u
z`edE6Z}?LS1-^DA%&Bm=>5`g!%q7I6v#TiY^vi&pl0Vb;`u_Ubar*ShUf$<7_wFhP
zGv=Oaz<oL8;gg#utz?#YmfMuhiwNzCJ-3YUxIDjN*EB(<=ax;OOQs}UG=9O=z3E`Z
zKC?=lCoRS$GtNJX`1O2w#JjW|v(DxTUP`atkQXyaOuOXs_QTcMpI=w^9C)x;eDTpK
zE4ij_o)IIokDE0lF~liq+I!UpkvIQ@Fz(Q5Y7Q53D!nQ#psRD{T%=IDfObLODIK-B
zQ5o0Y7PI9aSTea&#%Q5YpnA&G4cioKIn<8qdXfIF>0V-x`rW=&yIha_*P0viT7GV-
z^qgsCKd&h3oQhxY*mdy}>n+~}PFG)7e0PgSc!RsO{fvysnuqw;vI)u0G0+lcTFo)R
z`0Tr-l?CVX=i97m?z`w9@Rmn$$(#rYlk~imvB}>ae0r)JeqnjdKbh>rEQ4bWhTFKl
z3f)`cboN%p)RwF2`=-o#t)JAOF6@?ZxPQZmkH1dbxYtvzxH0?TZqKj9<yQ9UGfnN6
zf49uKte1HC%?*ofPIk6GV~RcEChxxS``Ug_@9KRv57jPz4!h56`YLeo?w^{CZ&&c@
zb%*Sj<hg9M1hWs@(UPdMZg*-wCh93}k!tUa-LdP;I=MAstG2b>ktw_``si85?)M!(
z9-O!>(7+tomXv&Hs;PFclgY|UOP8bwPl>vGY-!{4$^HH^=Ne1CXj(MPNLre+x!X`o
zK6~kuojXLYJ$-KezURonvVRAj)U1}Bext6+((<=OW$q-omR~6%yYIf5DEVgYvCNPy
zyDGQxsC<2CSGMrY<%$=2$)|l5^Qz6x>UCnB=PancBkN1wqWj19%}Tv>)Y$Ft_VZ$U
z4_b*I5PQE#<IR%;mWL&sR`wM!*1uh{qT;7}e8sJK@47bX@pn3ybp2f?z5TVxBG=WO
zk4>Hm8gwq3Uw_ASUd>U#i*vnJxw7W&S-YfX#-=GDnhq~+_xjyx_x<-_pSP^ZuK3>D
z?{Ac9>-_f7sj}(cUjNXi^OW}Sz#Tu2KeP)lc)QF+acNt~X=V<!W2-tY-0~=sGQ0dL
zzx&17S)y5gd@f2|Xb$JweEbc^!mi_!OKwZ9QQ=e6iGO_k%Hh6<Gs4mL-c2;wtyZ$F
zWd7#+Z_KprP2Ku+yL;Ei1r6C-)H;jjlnQhPDS1rO+_`4a+}P3^$_2munQkylo4Q#l
z*L%;&w<}gySRI<Qsq<>{QBh5+g3=i`11d_}ZvPQ2jbf^>JnLco>yyE|MI~}~7H&D5
zai_-rPkY17P2Vy$7i3=#Qajbs>=DP|s4#b1M(zXa4?*eIYweBCf2veV^R9L<$YWwW
z`_VFGMdQ?#+ZW=K4fpyd>TH(osQg$W(>D910pHHGDM=-6I#TLgp}(^f#IJbWFkf?W
zqP<!5wYTBV7ad!D#o=(GaOnJaokb7*UVjdD@|w3UUhR{w+p4?U14P&_UZ1h*n%Py6
zP3JAeuJygVwCqjr>(|pgo;rlCymjqWji{JFt#{pHL)Pq7C-w4Awr)6o)4H&2n(0~P
zIbPRI9|?H)%n*_~c`7L9WAIU<_7i5aqTWV6nx)#Z?9aZV**|VBIDBh?eO(E=xG|&Z
zLPxc2OLVk~T2y=%G<dqrt^DWBarWWNx@&)14_BrAt}(Ygf5F;0?)zom!!nh;_nCe&
zx`gGp&P>^w=6`Ww;iAo(`PH~QZ%uNq;=8DFIqSL9!BbTyAGeh<JQTQhyi9t2-_h4P
z>pDw!b)1f0>sw_je#p5YvPkN7e#Pf6ceFoh8ti#?GX7WvyU%v6g1~!qQaiT!tWCI;
z*UdUtOD#9*(Y9w#gz`S69o+iOUq|4)jzD=(&6|5o7j|>sy4HKEEb#7yn7e;|g=V}8
zXi;Da?Xu)@7W#W8>fae9yGNI|?S4AF@?xO%IUfD*%$xsso$u~bk9L13vD0Zb!*j)m
zeZJkH>pu9pWd%%K!><^4*><Y$#C4ImTa8Zmh3@SYx9!|l*BR1v_`F`BqU*%D1-a3p
zr~XIGQN6O|<g5Ix^8E!`xgUP86`q^5$Smy3#53kolXbP6pH9g&d@k*NyF>82o9s2W
zzaI}<CtPC;Y!&+}r+qzP=Q1hZ;wvo6eVx8c<-N+vU3WF0mibBhsvS$Ef*-wzR=j+#
zTVm^;x+xpB)!e?{DPbEI!OpHLXX}u2J)wx}Sn%dwp~hP8TdnGXlb)FQpWiDspXsrl
zz~a|>7s8T4=6bz-u<?h?#+4cGH;Ux%`4)I5>ei%B_50TUOYZ*rr*zH#i}}?DzC14Z
zpW)$F^V>!A*3?;3S9LDTTG$`AQt90Pn|$9&Lu)fPXZ!bB?X2Uv!52E6hhbl<zuNrC
zJJMX2Mwr~{;5xT%!|p|$>v~V76btMsmQVjMm+^l598L>%x&4YCoF_&u+uF9vJLvJs
zr-_103g_zhI1(o-_#RJiRlk`U`}akl?3N_`UAu&|PfL1QOyt#LU(2=qbndlv60z?;
za!j1*yk!kf#iz`wR|^lfzh9P?bG3WvKcP8yb7toouX+3I{lS^S&5nCaIHEMRWo<v@
zJT3E?;i_pt-9f44sqDA)@)N#q`g`P{%mtCPChaSnKc1YaG{s}-wCzU|bY_Mvd9i$Y
z_uRY3KiWu_^abnA=9v`|omaAkaj%<UPT(BVQ!5(v+Ic_CSXtY3zMTDHK1)LS4Yh(F
z+!kI}n}g;QH$`Q0-q1_SG;a@HI_Jj1h~2%60tSr<v#-i;_w+Y^x$cg7mUz+`wdG;Q
z^4{ik%nD?*J>7gmUjC-phUN<{i`Fz%{PCM;%r_<Agih0u458S|?$?#G=2?X?Z|!yc
z^k~biNnV*h7x83xn+hfugeUiXxp6p>x$dV;(9g9Bhb>bq+Ig-kN;{q9<Mj4=5Fy%b
zm#}-A+-=)>ho?pN-UKtv|5!0GI^$3HJHs>8JfGzbJF8z|^|dVcC?k};E+N`$O2Vog
z8D<&kEDBe(S04SV+EVu`hv&-9`h&&0KYum2k)+FZ@zP3`)lKC~Mb<s)GqBS0Tj(_R
zaMSJo{$;m(r(a0gu*fx)$?~q=240aEAH^9n{N2^=@2d<ybo~0xCFb*`BCEFkfB*d3
z@ja)19nn4h`eEF@J(ssc{}c$%d^5}D^5m<6)6OsEczL;YN>!HV7VGot*82ZEb)0qD
z##^7KA5Y!dy6H`!Z!w4EZ4J4o)2E(tNeABR*)^l(i0bReIVWb=M3h!e-FRMWjbHnb
z=)UWYjk-ztsjrTi^}8OMYMx}sTEA)HouHp<Pu%ug^>nMsMgA<WFL8TxF7BOCy1QXs
zvh`sHU51dWbG}@<cHUqAxAvX>DIaERsfls8q01yc$)^1Ir{{K$R8D?2f0?|IsZjKB
zx8@tYTe_x_!AEzgBp4o=-hXn%zVgK(Z~w>bSW`05{!IS8IXiBrmnDmwTYTi#W?T0C
z-e*3A2FQ!d;%eO~(zPJTKy6W0xNwz*;nOPCh5tS+3;VzG<y-yb??nIqOS@zI${^j^
z`rU?F4xigTGeonVJ6~8|G2^Gej8^Rf0aG>7R4V)5tl&5vx^2OF(bluAC-m#;)qgDc
z&-F1^SttMA-Rp<*Cd^*3`0=%Q*@djf`Ev_v>Mvz~|E53r+5VirH=p(tZBFt3E7&WR
zy{SUi@iwE)vlUTRwfAGczD##wYybScuF)ZBe#z2qxqMGvTaAy0T~CIptvDJ`ra3dD
zm3y}D@3%%R!m9TKZafXUbMW(zz#Fv>pF8b1A8f4Ab+ho(nKi}UKbJ6zrk5skGj5Mn
zsPCI#w@hya%i*(TGx#@~eEEHPu1nmloPY0}jXHvqk|%{agsl!a%I&TmS0Tvg%>6W}
zZHD`$&U}UND!1M2TcT{dvZpey*d;qH>5^sS3d7{9(MCDjWVhKJO%q<|+2^}K_)MAQ
z&G|ej&VlE+_pTC<-IA?av|IA7Q<0%cVP%1#zvK?}J5NL3UN%2fzWo)i&bjS^r>ALc
ze^PJC@_JK7`z)F8!yANHx7>Po`+4W%1<eY=w_VSPt$1o}e0F1qTeSMVW%D+E-`Bow
zf7Z)LX7iRwtv+2kl9$hA3Q0cnervQ^s8+;!d!Xva5Y>;yL7qo+_v)_X@-cHcJIAY}
zYqfwnYpCvOmAXT*bvwL@4z+ikK6O(@bj#zwsX-$5byY(4O!H1TeWohRg3ocW@b@Eu
z$KH7D?$QvsAj!1#L#FJtP$ByeRolo1ZCrYpA2UO{*Rz`$UFLdzr{HjcfLUvS-CDc)
zYfFBM``s=OijL>qR_f?s7GY$yMS9lL^NYMn7kb~?ec|@X{Qv*%E*B0v&ZVDZY*qgD
z{l`-W-nr+tCdYVZZ_sB*I;J{nJ>T>n`S-Mv7gZ?9HD%p=lWThKNz+uN_Uzs9$>C>W
z<ll;gmFc~`dFa$ToyZscv)_t`mF3HehgCI-$V=>=y6G8P^7OJlI$^uLcWP;DDV-U%
zB~$xEwr6<s%;n<8RIb!ZZt~eyc0M3%rq;<d-ly0mD~378$ksBtC{H|e_)x>OZuL(`
z7Qfj%;l2E;zlVhvJxeQMes^x-J~OUu@~qXhA{k~}y1rip)(EW@tDU@HN$HfGtn(Q5
zN|>=L>U>tYUwYrC@9ewj3}0rvDcf(PkUy7CPd?uAzLUgq@9Fomxet_aCRj7RHfFF>
z+mpYttV=gR_u8c9)@_TX`1T$>kz%}M(%<Cnz4dAie0FKer{q?y6gep)%=#oG;iB7A
z<|(`UCjN2OymYxGr(>0BQMiD`@oh{3M?#tPuic+j=E@M~`_DpZVenMp!zP_OBY)K0
zac-y+epuLG5x480UZn08sf_76qoPIju3fC@R{3D(<7<%#`>K^<-#l%pvRv3}mDREA
z>8s?hz$-ysw<7iBqEEc>=BTP$dqHdF%WYGCev5RpOj)+9U4ea*XGIXx*`^tn1WGT|
z2`(%XN_zS#GdF*}WKXl^x@BJTnv9bEtzK^x)ure%d(G87iC_O;EPbWzZ=7wrE#iTW
zRj1eP?6aaO%60YYPO@%)8}cZb;i>e;#RtXv`1TxbQd=OrUhK&1r3p7~#yq(6){KAM
z+Y;8G#k(u!zMCa^*Ob59DrfQ>Z@=R&ThG0mv11|g^)mCIt#fRZvxS1&UPLj)ubL1V
z^Z5FHJ7MuRtAgz|tPQc;zC-Y%t-#{qw{v23HdbgATK<0Ew(LhtfK1Zq%2!!O9Zqh(
z+$D5;2FH{Sx#xa_{`@-GC0F6~DzBu&B2mkoHyN_#M`(Y%Bhsl?#c=T2^Yd~(8`dxU
zarf)Z2fp4XQg*KJnXt(<G{<aT>Vogr)V?!h{e5Be-E>N+MAOM*8L_cFx~khuWlWt;
zn7)|Q{e10_sQk1Re;$vGKUCGCl_K8CvQMqO=oeacF)d~5p5DKkoKxJ^d{s^QE0QRq
zB%K<}<y7x*K&jC!u=JFbhKk+ovZTKiR$ookZ%&L=)=G5Ix>9y~zQMwtxAT51$kx4K
z=AyUpwR+}4xl?^?^QRt;n46~Nl6!LFj_i|1LV9-mj^4D$=DqL4g^L=aV!LI&ni{k5
zJi6DeFpHD3H=18+sokH)8oIk5Y`xqrYgTW)cdwYqt=MIDyE(sP{r`CT-NL(pLbbjt
z9hlTz1dl$~n3a{HUcY#g>9uTYg}j_^TNY)0IAeFB|C{2L`<%U-AAhfDWAncl!8KRz
zNT9EkP~`!My$0^<LVct*?Z`NILg%*>$Is*s8t0c?()8Q1U+u5NmNlX3Go$A2esMol
zfGunGx=<gx#pQ8l>cyrnwrx%l*>&36^?w6f{Zq>=wh!tWL^`G>2OoJ~FvmAc_1T0j
zBR4h0{GC0qw=Unc-!D94bz$Uv(L<FDZ}g_*a4ihW7U0|Ebgi|>?2XShv+O1gr)@{?
zZZ~~e>OW1*{N!Kds(({M&b3~as(vYRVCOVVy-9~B#D02Fq@+LX%(jZfUZ+>PZLaQ^
zZyERY%(4$z^Sjb|CQSZ%^5?ebDQozyt?r$C)>r-Z*Bx)vO>T0rEj_}Yc=p1!_7=BA
zUyUAnJ)Ke!ZSb~OWM18-MBNFUO_w~=#U|Kr?>EbR?@=SPIDGN-|D7MCqB?dxW?E*M
zX?i<Kcyn=N<d+$Vx8qKHKD>1L;(Est(M5A^N8WERYn?IYPxQa?xGh`V-g@z7Yfo6U
zzoEdp{oJ|&gLGM=_$v!rg(rMYp875ExYq5Cc1D3I7QaH<j#Nx_x}>SL;6-Eciqwy6
zXNsrWtX%i#IqPGAgW0)Gi4zq&b_O&==xmeS)^LbvTDXF>%dbb5ZyvCz6=<I_*Q~>D
z;<u!ubA*~ibkg#R3~v6`7ODP~FhB7@$(hROp}$-#^mThLKJ<BeaCdC9)Zur(XZz*q
zK54b(cC~vV@?m<&!$(q=6_UHPthe!;TqSnxxLLxYIU(ni!f$ha+w7Xnv9K$SZ(Hg*
zwudeu#iw>ZHlA5BCqMT5YpbcXakBnzuJAb6vtF>5IPll=PAS9j_xmLdDDIY$b#_~P
zYhmR1kUe7dW+{e6ePLU^t`n*CI=|#<rSTWTt>5<uR_$RbDq?q^&gjzX;P0pPef<{I
zPnnY@7$!eVxu3c%dh>)E$uT>u{%U+pY7se7-s}1^Ao|7{iQ221OvO&Gn-I-;^wqju
zSN3kQc~G=3-^6%@?g7?ni{*QduiIYXQg$nRPi5&|F5_d@&g^gfyFJ!*Teg4r^@am+
z-KW%4?Kq+q_pE!+dpf2_fNiIatNS1S&QLcY&1WC~@A<!W%Zhoo=bx`Dm{;e%_`$B<
zM{9q4{k!|pwl=X8A@Q~+8q?ebzMgGsEPTyud^WULV#dN<61U!d^g1)kB4ejoX!j)*
z`2`jccS>sx-7MbL_e4`QP(ny(3By9S_zicfWNR|6hp_y-pSt~J+QRg<lQT>B&s7_K
zam&;d(JVd@D6)g=n4^f&%WZS_R^?4zEx%=<R$})`t<~HoYPwe>Gdc)+a0aR6JHC+q
za&pc0lO?rAr)S;Cx%i|^W;d&EUitC#J{IfaLA;f7k6!POS>yW9&G6T&7$=|EYPUZp
zJIl_Msrj-bC@J>nMt5bF&hqQr62})!$+#SKVtXm0o<)vH`HdH65*O<i-MCX{`XpW<
Rm*M4qX1jzd{l@PY7yw`PA%Xw^

diff --git a/src/transform/reification.ml b/src/transform/reification.ml
index a2c2d5a71d..45836a9d35 100644
--- a/src/transform/reification.ml
+++ b/src/transform/reification.ml
@@ -25,19 +25,24 @@ type reify_env = { kn: known_map;
                    lv: vsymbol list;
                    var_maps: ty Mvs.t; (* type of values pointed by each map*)
                    ty_to_map: vsymbol Mty.t;
+                   env: Env.env;
+                   task: Task.task;
                  }
 
-let init_renv kn lv = { kn=kn;
-                        store = Mterm.empty;
-                        fr = 0;
-                        subst = Mvs.empty;
-                        lv = lv;
-                        var_maps = Mvs.empty;
-                        ty_to_map = Mty.empty;
-                      }
+let init_renv kn lv env task =
+  { kn=kn;
+    store = Mterm.empty;
+    fr = 0;
+    subst = Mvs.empty;
+    lv = lv;
+    var_maps = Mvs.empty;
+    ty_to_map = Mty.empty;
+    env = env;
+    task = task;
+  }
 
 let rec reify_term renv t rt =
-  let rec invert_pat vl (renv:reify_env) interp (p,f) t =
+  let rec invert_nonvar_pat vl (renv:reify_env) interp (p,f) t =
     if debug
     then Format.printf
            "invert_pat p %a f %a t %a@."
@@ -58,12 +63,16 @@ let rec reify_term renv t rt =
            (renv, []) pl la1 la2 in
        if debug then Format.printf "building app %a of type %a with args %a@."
                                    Pretty.print_ls cs
-                                   Pretty.print_ty (Opt.get cs.ls_value)
+                                   Pretty.print_ty p.pat_ty
                                    (Pp.print_list Pp.comma Pretty.print_term)
                                    (List.rev rl);
-       let t = t_app cs (List.rev rl) cs.ls_value in
+       let t = t_app cs (List.rev rl) (Some p.pat_ty) in
        if debug then Format.printf "app ok@.";
        renv, t
+    | Pvar v, Tapp (ls, [{t_node = Tvar v'}]), Tapp (ls', [t])
+         when ls_equal ls ls' && vs_equal v v' ->
+       if debug then Format.printf "case app_var@.";
+       renv, t
     | Papp _, Tapp (ls1, _), Tapp(ls2, _) ->
        if debug then Format.printf "head symbol mismatch %a %a@."
                                    Pretty.print_ls ls1 Pretty.print_ls ls2;
@@ -77,20 +86,23 @@ let rec reify_term renv t rt =
       | Pvar _, Tvar _, Tconst _
       -> if debug then Format.printf "case vars@.";
          (renv, t)
-    | Pvar _, Tapp (ls, _la), _ when ls_equal ls interp
+    | Pvar _, Tapp (ls, _hd::_tl), _ (*when ls_equal ls interp FIXME ?*)
       -> if debug then Format.printf "case interp@.";
          invert_interp renv ls t
-    (*| Papp (cs, pl), Tapp (ls1, la1), _ when Sls.mem ls1 !reify_invert
-    -> (* Cst c -> morph c <- 42 ? *) *)
+    | Papp (cs, [{pat_node = Pvar _}]), Tapp(ls, _hd::_tl), Tconst _
+      -> if debug then Format.printf "case const@.";
+         let renv, rt = invert_interp renv ls t in
+         renv, (t_app cs [rt] (Some p.pat_ty))
     | _ -> raise NoReification
-  and invert_var_pat  vl (renv:reify_env) _interp (p,f) t =
+  and invert_var_pat vl (renv:reify_env) _interp (p,f) t =
     if debug
     then Format.printf
            "invert_var_pat p %a f %a t %a@."
            Pretty.print_pat p Pretty.print_term f Pretty.print_term t;
-    match p.pat_node, f.t_node, t.t_node with
-    | Papp (cs, [{pat_node = Pvar v1}]),
-      Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}]), _
+    match p.pat_node, f.t_node with
+    | Papp (_, [{pat_node = Pvar v1}]),
+      Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}])
+      | Pvar v1, Tapp (ffa,[{t_node = Tvar vy}; {t_node = Tvar v2}])
          when ty_equal v1.vs_ty ty_int
               && Svs.mem v1 p.pat_vars
               && vs_equal v1 v2
@@ -98,12 +110,16 @@ let rec reify_term renv t rt =
               && List.exists (fun vs -> vs_equal vs vy) vl (*FIXME*)
       ->
        if debug then Format.printf "case var@.";
-       let rty = cs.ls_value in
+       let rty = (Some p.pat_ty) in
+       let app_pat trv = match p.pat_node with
+         | Papp (cs, _) -> t_app cs [trv] rty
+         | Pvar _ -> trv
+         | _ -> assert false in
        if Mterm.mem t renv.store
        then
          begin
            if debug then Format.printf "%a exists@." Pretty.print_term t;
-           (renv, t_app cs [t_nat_const (snd (Mterm.find t renv.store))] rty)
+           (renv, app_pat (t_nat_const (snd (Mterm.find t renv.store))))
          end
        else
          begin
@@ -112,20 +128,34 @@ let rec reify_term renv t rt =
            let vy = Mty.find vy.vs_ty renv.ty_to_map in
            let store = Mterm.add t (vy, fr) renv.store in
            let renv = { renv with store = store; fr = fr + 1 } in
-           (renv, t_app cs [t_nat_const fr] rty)
+           (renv, app_pat (t_nat_const fr))
          end
     | _ -> raise NoReification
+  and invert_pat vl renv interp (p,f) t =
+    try invert_nonvar_pat vl renv interp (p,f) t
+    with NoReification -> invert_var_pat vl renv interp (p,f) t
   and invert_interp renv ls (t:term) = (*la ?*)
-    let ld = Opt.get (find_logic_definition renv.kn ls) in
+    let ld = try Opt.get (find_logic_definition renv.kn ls)
+             with _ ->
+                  if debug
+                  then Format.printf "did not find def of %a@." Pretty.print_ls ls;
+                  raise NoReification
+    in
     let vl, f = open_ls_defn ld in
     if debug then Format.printf "invert_interp ls %a t %a@."
                                 Pretty.print_ls ls Pretty.print_term t;
-    match f.t_node, t.t_node with
-    | Tcase (x, bl), _ ->
-       assert (List.length vl = 2);
+    invert_body renv ls vl f t
+  and invert_body renv ls vl f t =
+    match f.t_node with
+    | Tvar v when vs_equal v (List.hd vl) -> renv, t
+    | Tif (f, th, el) when t_equal th t_bool_true && t_equal el t_bool_false ->
+       invert_body renv ls vl f t
+    | Tcase (x, bl)
+      ->
        (match x.t_node with
         | Tvar v when vs_equal v (List.hd vl) -> ()
-        | _ -> assert false);
+        | _ -> if debug then Format.printf "not matching on first param@.";
+               raise NoReification);
        if debug then Format.printf "case match@.";
        let rec aux invert = function
          | [] -> raise NoReification
@@ -133,38 +163,145 @@ let rec reify_term renv t rt =
             try invert vl renv ls (t_open_branch tb) t
             with NoReification ->
                  if debug then Format.printf "match failed@."; aux invert l in
-       (try aux invert_pat bl with NoReification -> aux invert_var_pat bl)
-    | _ -> raise NoReification in
+       (try aux invert_nonvar_pat bl with NoReification -> aux invert_var_pat bl)
+    | _ -> if debug then Format.printf "function body not handled@.";
+           if debug then Format.printf "f: %a@." Pretty.print_term f;
+           raise NoReification
+  and invert_ctx_interp renv ls t l g =
+    let ld = try Opt.get (find_logic_definition renv.kn ls)
+             with _ ->
+                  if debug
+                  then Format.printf "did not find def of %a@." Pretty.print_ls ls;
+                  raise NoReification
+    in
+    let vl, f = open_ls_defn ld in
+    if debug then Format.printf "invert_ctx_interp ls %a @."
+                                Pretty.print_ls ls;
+    match f.t_node with
+    | Tcase ({t_node = Tvar v}, [tbn; tbc] )
+         when vs_equal v (List.hd vl) ->
+       let open Theory in
+       let th_list = Env.read_theory renv.env ["list"] "List" in
+       let ty_g = g.vs_ty in
+       let ty_list = ns_find_ts th_list.th_export ["list"] in
+       let ty_list_g = ty_app ty_list [ty_g] in
+       if (not (ty_equal ty_list_g l.vs_ty))
+       then (if debug
+             then Format.printf "bad type for context interp function@.";
+             raise NoReification);
+       let nil = ns_find_ls th_list.th_export ["Nil"] in
+       let cons = ns_find_ls th_list.th_export ["Cons"] in
+       let th_bool = Env.read_theory renv.env ["bool"] "Bool" in
+       (* FIXME add use export list.List and bool.Bool to the task ? *)
+       let implb = ns_find_ls th_bool.th_export ["implb"] in
+       let (pn, fn) = t_open_branch tbn in
+       let (pc, fc) = t_open_branch tbc in
+       begin match pn.pat_node, fn.t_node, pc.pat_node, fc.t_node with
+       | Papp(n, []), Tapp(leq,{t_node = Tvar g'}::_),
+         Papp (c, [{pat_node = Pvar hdl};{pat_node = Pvar tll}]),
+         Tapp(ib, [({t_node = Tapp(leq', _)} as thd);
+                   ({t_node =
+                       Tapp(ls', {t_node = Tvar tll'}::{t_node=Tvar g''}::_)}
+                    as ttl)])
+            when ls_equal n nil && ls_equal c cons && ls_equal ls ls'
+                 && ls_equal ib implb && vs_equal tll tll'
+                 && vs_equal g' g'' && ls_equal leq leq'
+                 && List.mem g' vl
+                 && not (Mvs.mem tll (t_vars thd))
+                 && not (Mvs.mem hdl (t_vars ttl))
+         ->
+          if debug then Format.printf "reifying goal@.";
+          let (renv, rg) = invert_interp renv leq t in
+          let renv = { renv with subst = Mvs.add g rg renv.subst } in
+          if debug then Format.printf "filling context@.";
+          let renv, ctx =
+              task_fold
+                (fun (renv,ctx) td ->
+                  match td.td_node with
+                  | Decl {d_node = Dprop (Paxiom, _, e)}
+                    ->
+                     begin try
+                         let (renv,req) = invert_interp renv leq e in
+                         (renv,(t_app cons [req; ctx] (Some ty_list_g)))
+                       with
+                       | NoReification -> renv,ctx
+                       | TypeMismatch _ -> raise NoReification
+                     end
+                  | _-> renv,ctx)
+                             (renv, (t_app nil [] (Some ty_list_g))) renv.task in
+          { renv with subst = Mvs.add l ctx renv.subst }
+       | _ -> if debug then Format.printf "unhandled interp structure@.";
+              raise NoReification
+       end
+    | _ -> if debug then Format.printf "not a match on list@.";
+           raise NoReification
+  in
+  let add_to_maps renv vyl =
+     let var_maps, ty_to_map =
+       List.fold_left
+         (fun (var_maps, ty_to_map) vy ->
+           if Mty.mem vy.vs_ty ty_to_map
+           then (Mvs.add vy vy.vs_ty var_maps, ty_to_map)
+           else (Mvs.add vy vy.vs_ty var_maps,
+                 Mty.add vy.vs_ty vy ty_to_map))
+         (renv.var_maps, renv.ty_to_map)
+         (List.map
+            (fun t -> match t.t_node with Tvar vy -> vy | _ -> assert false)
+            vyl)
+     in
+     { renv with var_maps = var_maps; ty_to_map = ty_to_map }
+  in
   if debug then Format.printf "reify_term t %a rt %a@."
                               Pretty.print_term t Pretty.print_term rt;
   if not (oty_equal t.t_ty rt.t_ty)
   then (if debug
         then Format.printf "reification type mismatch %a %a@."
-                           Pretty.print_ty (Opt.get t.t_ty) Pretty.print_ty (Opt.get rt.t_ty);
+                           Pretty.print_ty (Opt.get t.t_ty)
+                           Pretty.print_ty (Opt.get rt.t_ty);
         raise NoReification);
   match t.t_node, rt.t_node with
-  | _, Tapp(interp, [{t_node = Tvar vx}; {t_node = Tvar vy} ])
-       when List.mem vx renv.lv && List.mem vy renv.lv  ->
+  | _, Tapp(interp, {t_node = Tvar vx}::vyl)
+       when List.mem vx renv.lv
+            && List.for_all
+                 (fun t -> match t.t_node with
+                           | Tvar vy -> List.mem vy renv.lv
+                           | _ -> false)
+                 vyl  ->
      if debug then Format.printf "case interp@.";
-     let var_maps, ty_to_map =
-       if Mty.mem vy.vs_ty renv.ty_to_map
-       then renv.var_maps, renv.ty_to_map
-       else (Mvs.add vy (Opt.get interp.ls_value) renv.var_maps,
-             Mty.add vy.vs_ty vy renv.ty_to_map) in
-     let renv = { renv with var_maps = var_maps; ty_to_map = ty_to_map } in
+     let renv = add_to_maps renv vyl in
      let renv, x = invert_interp renv interp t in
      { renv with subst = Mvs.add vx x renv.subst }
   | Tapp(eq, [t1; t2]), Tapp (eq', [rt1; rt2])
-       when ls_equal eq ps_equ && ls_equal eq' ps_equ ->
+       when ls_equal eq ps_equ && ls_equal eq' ps_equ
+            && oty_equal t1.t_ty rt1.t_ty && oty_equal t2.t_ty rt2.t_ty
+    ->
      if debug then Format.printf "case eq@.";
      reify_term (reify_term renv t1 rt1) t2 rt2
-  | _ -> if debug then Format.printf "no reify_term match@."; raise NoReification
+  | _, Tapp(eq,[{t_node=Tapp(interp, {t_node = Tvar l}::{t_node = Tvar g}::vyl)}; tr])
+       when ls_equal eq ps_equ && t_equal tr t_bool_true
+            && List.mem l renv.lv
+            && List.mem g renv.lv
+            && List.for_all
+                 (fun t -> match t.t_node with
+                           | Tvar vy -> List.mem vy renv.lv
+                           | _ -> false)
+                 vyl
+    ->
+     if debug then Format.printf "case context@.";
+     let renv = add_to_maps renv vyl in
+     invert_ctx_interp renv interp t l g
+  | _ -> if debug then Format.printf "no reify_term match@.";
+         if debug then Format.printf "lv = [%a]@."
+                                     (Pp.print_list Pp.space Pretty.print_vs)
+                                     renv.lv;
+         raise NoReification
 
 let build_vars_map renv prev =
   if debug then Format.printf "building vars map@.";
   let subst, prev = Mvs.fold
-                (fun vy ty_val (subst, prev) ->
-                  let ty_vars = ty_func ty_int ty_val in
+                (fun vy ty_vars (subst, prev) ->
+                  if debug then Format.printf "creating var map %a@."
+                                              Pretty.print_vs vy;
                   let ly = create_fsymbol (Ident.id_fresh vy.vs_name.id_string)
                                           [] ty_vars in
                   let y = t_app ly [] (Some ty_vars) in
@@ -172,19 +309,38 @@ let build_vars_map renv prev =
                   let prev = Task.add_decl prev d in
                   Mvs.add vy y subst, prev)
                 renv.var_maps (renv.subst, prev) in
+  let prev = Mvs.fold
+               (fun vy _ prev ->
+                 if debug then Format.printf "checking %a@." Pretty.print_vs vy;
+                 let vs = Mty.find vy.vs_ty renv.ty_to_map in
+                 if vs_equal vy vs then prev
+                 else begin
+                   if debug
+                   then Format.printf "aliasing %a and %a@."
+                                      Pretty.print_vs vy Pretty.print_vs vs;
+                   let y = Mvs.find vy subst in
+                   let z = Mvs.find vs subst in
+                   let et = t_equ y z in
+                   let pr = create_prsymbol (Ident.id_fresh "map_alias") in
+                   let d = create_prop_decl Paxiom pr et in
+                   Task.add_decl prev d end)
+               renv.var_maps prev in
   if not (List.for_all (fun v -> Mvs.mem v subst) renv.lv)
   then (if debug
-        then Format.printf "some vars not matched, todo use context@.";
+        then Format.printf "vars not matched: %a@."
+                           (Pp.print_list Pp.space Pretty.print_vs)
+                           (List.filter (fun v -> not (Mvs.mem v subst)) renv.lv);
         raise Exit);
+  if debug then Format.printf "all vars matched@.";
   let prev = Mterm.fold
                (fun t (vy,i) prev ->
                  let y = Mvs.find vy subst in
-                 let ty_val = Mvs.find vy renv.var_maps in
                  let et = t_equ
                             (t_app fs_func_app [y; t_nat_const i]
-                                   (Some ty_val))
+                                   t.t_ty)
                             t in
-                 if debug then Format.printf "eq_term ok@.";
+                 if debug then Format.printf "%a %d = %a@."
+                                             Pretty.print_vs vy i Pretty.print_term t;
                  let pr = create_prsymbol (Ident.id_fresh "y_val") in
                  let d = create_prop_decl Paxiom pr et in
                  Task.add_decl prev d)
@@ -204,27 +360,29 @@ let build_goals prev subst lp g rt =
                        ~label:(Slab.singleton expl_reification_check)) in
   let d = create_prop_decl Pgoal pr g in
   let task_r = Task.add_decl (Task.add_decl prev d_r) d in
-  if debug then Format.printf "building cut indication@.";
-  let ci =
-    match (rt.t_node, g.t_node) with
-    | (Tapp(eq, rh::rl),
-       Tapp(eq', h::l))
-         when ls_equal eq eq' ->
-       List.fold_left2 (fun ci st rst -> t_and ci (t_equ (t_subst subst rst) st))
-                       (t_equ (t_subst subst rh) h)
-                       l rl
-    | _,_ when g.t_ty <> None -> t_equ (t_subst subst rt) g
-    | _ -> raise Exit in
-  if debug then Format.printf "building tasks@.";
-  let ltask_r = Trans.apply (Cut.cut ci (Some "interp")) task_r in
-  if debug then Format.printf "cut ok@.";
+  if debug then Format.printf "building cut indication rt %a g %a@."
+                              Pretty.print_term rt Pretty.print_term g;
+  let ltask_r =
+    try let ci =
+          match (rt.t_node, g.t_node) with
+          | (Tapp(eq, rh::rl),
+             Tapp(eq', h::l))
+               when ls_equal eq eq' ->
+             List.fold_left2 (fun ci st rst -> t_and ci (t_equ (t_subst subst rst) st))
+                             (t_equ (t_subst subst rh) h)
+                             l rl
+          | _,_ when g.t_ty <> None -> t_equ (t_subst subst rt) g
+          | _ -> raise Exit in
+        if debug then Format.printf "cut ok@.";
+        Trans.apply (Cut.cut ci (Some "interp")) task_r
+    with _ -> if debug then Format.printf "no cut found@."; [task_r] in
   let lt = List.map (fun ng -> Task.add_decl prev
                        (create_prop_decl Pgoal (create_prsymbol (id_fresh "G")) ng))
                     inst_lp in
   if debug then Format.printf "done@.";
   ltask_r@lt
 
-let reflection_by_lemma pr : Task.task Trans.tlist = Trans.store (fun task ->
+let reflection_by_lemma pr env : Task.task Trans.tlist = Trans.store (fun task ->
   let kn = task_known task in
   let g, prev = Task.task_separate_goal task in
   let g = Apply.term_decl g in
@@ -235,7 +393,7 @@ let reflection_by_lemma pr : Task.task Trans.tlist = Trans.store (fun task ->
     let d = Opt.get d in
     let l = Apply.term_decl d in
     let (lp, lv, rt) = Apply.intros l in
-    let renv = reify_term (init_renv kn lv) g rt in
+    let renv = reify_term (init_renv kn lv env prev) g rt in
     let subst, prev = build_vars_map renv prev in
     build_goals prev subst lp g rt
   with NoReification | Exit -> [task])
@@ -253,6 +411,7 @@ type value =
   | Vvoid
   | Varray of value array
   | Vmatrix of value array array
+  | Vref of value ref
 
 and field = Fimmutable of value | Fmutable of value ref
 
@@ -268,6 +427,8 @@ let rec print_value fmt = function
   | Varray a -> fprintf fmt "Varray [|%a|]"
                         (Pp.print_list Pp.space print_value) (Array.to_list a)
   | Vmatrix m -> fprintf fmt "Vmatrix %a" print_matrix m
+  | Vref r -> fprintf fmt "Vref %a" print_value !r
+
 and print_field fmt = function
   | Fimmutable v -> fprintf fmt "Fimmutable %a" print_value v
   | Fmutable vr -> fprintf fmt "Fmutable %a" print_value !vr
@@ -282,7 +443,11 @@ let field_get f = match f with
 
 open Stdlib
 
-let find_module_path env mm path m = match path with
+let find_module_path env mm path m =
+  if debug
+  then Format.printf "find_module_path path %a m %s@."
+                     (Pp.print_list Pp.space Pp.string) path m;
+  match path with
   | [] -> Mstr.find m mm
   | path -> let mm = Env.read_library Pmodule.mlw_language env path in
             Mstr.find m mm
@@ -301,11 +466,16 @@ let translate_module =
       pm
 
 exception Constructor
+exception Field
 
 let get_decl env mm rs =
   let open Pdecl in
+  if debug then Format.printf "get_decl@.";
   let id = rs.rs_name in
+  if debug then Format.printf "looking for rs %s@." id.id_string;
   let pm = find_module_id env mm id in
+  if debug then Format.printf "pmodule %s@."
+                              (pm.Pmodule.mod_theory.Theory.th_name.id_string);
   let tm = translate_module pm in
   if Mid.mem id tm.mod_known
   then Mid.find id tm.mod_known
@@ -314,10 +484,12 @@ let get_decl env mm rs =
     match pd.pd_node with
     | PDtype l ->
        let rec aux = function
-         | [] -> false
-         | d::t -> List.mem rs d.itd_constructors || aux t
+         | [] -> raise Not_found
+         | d::t -> if List.mem rs d.itd_constructors then raise Constructor
+                   else if List.mem rs d.itd_fields then raise Field
+                   else aux t
        in
-       if aux l then raise Constructor else raise Not_found
+       aux l
     | _ -> raise Not_found
 
 let builtin_progs = Hrs.create 17
@@ -449,6 +621,24 @@ let exec_matrix_copy _ args =
      Vmatrix a
   | _ -> raise CannotReduce
 
+let exec_ref_make _ args =
+  match args with
+  | [v] ->
+     Vref (ref v)
+  | _ -> raise CannotReduce
+
+let exec_ref_get _ args =
+  match args with
+  | [Vref r] -> !r
+  | _ -> raise CannotReduce
+
+let exec_ref_set _ args =
+  match args with
+  | [Vref r; v] ->
+     r := v;
+     Vvoid
+  | _ -> raise CannotReduce
+
 let built_in_modules =
   [
     ["bool"],"Bool", [],
@@ -496,6 +686,12 @@ let built_in_modules =
      "set", exec_matrix_set ;
      "copy", exec_matrix_copy ;
     ] ;
+    ["ref"],"Ref",
+    [], (* ? *)
+    ["ref", exec_ref_make ;
+     "prefix !", exec_ref_get;
+     "infix :=", exec_ref_set;
+    ] ;
   ]
 
 let add_builtin_mo env (l,n,t,d) =
@@ -521,6 +717,7 @@ type info = {
     mm  : Pmodule.pmodule Mstr.t;
     vars: value Mid.t;
     recs: rsymbol Mrs.t;
+    funs: decl Mrs.t;
   }
 
 let print_id fmt id = fprintf fmt "%s" id.id_string
@@ -531,6 +728,10 @@ let add_id id v info = {info with vars = Mid.add id v info.vars}
 let add_vs vs = add_id vs.vs_name
 let add_pv pv = add_vs pv.pv_vs
 
+let add_fundecl rs decl info =
+  if debug then Format.printf "adding decl for %s@." rs.rs_name.id_string;
+  { info with funs = Mrs.add rs decl info.funs }
+
 exception NoMatch
 
 let rec matching info v pat =
@@ -560,11 +761,9 @@ let rec matching info v pat =
      | _ -> raise CannotReduce
 
 let rec interp_expr info (e:Mltree.expr) : value =
-  if debug then Format.printf "interp_expr@.";
   Mltree.(match e.e_node with
   | Econst nc -> Vint (Number.compute_int_constant nc)
   | Evar pv ->
-     if debug then Format.printf "Evar %a@." print_pv pv;
      (try get pv info
       with Not_found ->
            if debug
@@ -592,22 +791,25 @@ let rec interp_expr info (e:Mltree.expr) : value =
           let f = Hrs.find builtin_progs rs in
           f rs (List.map (interp_expr info) le)
         else begin
-        let decl = get_decl info.env info.mm rs in
-        if debug then Format.printf "decl found@.";
-        match decl with
-        | Dlet (Lsym (_rs, _ty, vl, e)) ->
-           eval_call info vl e
-        | Dlet(Lrec([{rec_args = vl; rec_exp = e;
-                      rec_sym = rs; rec_rsym = rrs; rec_res=_ty}])) ->
-           eval_call { info with recs = Mrs.add rrs rs info.recs } vl e
-        | Dlet (Lrec _) ->
-           if debug then Format.printf "Lrec@."; raise CannotReduce
-        | Dlet (Lvar _) ->
-           if debug then Format.printf "Lvar@."; raise CannotReduce
-        | Dlet (Lany _) ->
-           if debug then Format.printf "Lany@."; raise CannotReduce
-        | _ -> if debug then Format.printf "not a let decl@.";
-               raise CannotReduce
+          let decl = try Mrs.find rs info.funs
+                     with Not_found -> get_decl info.env info.mm rs in
+          if debug then Format.printf "decl found@.";
+          match decl with
+          | Dlet (Lsym (_rs, _ty, vl, e)) ->
+             eval_call info vl e
+          | Dlet(Lrec([{rec_args = vl; rec_exp = e;
+                        rec_sym = rs; rec_rsym = rrs; rec_res=_ty}])) ->
+             eval_call { info with recs = Mrs.add rrs rs info.recs } vl e
+          | Dlet (Lrec _) ->
+             if debug
+             then Format.printf "unhandled mutually recursive functions@.";
+             raise CannotReduce
+          | Dlet (Lvar _) ->
+             if debug then Format.printf "Lvar@."; raise CannotReduce
+          | Dlet (Lany _) ->
+             if debug then Format.printf "Lany@."; raise CannotReduce
+          | _ -> if debug then Format.printf "not a let decl@.";
+                 raise CannotReduce
           end
         end
       with
@@ -622,15 +824,18 @@ let rec interp_expr info (e:Mltree.expr) : value =
            if is_mutable then Fmutable (ref v) else Fimmutable v
          in
          Vconstr(rs, List.map2 field_of_expr rs.rs_cty.cty_args le)
+      | Field ->
+         if debug then Format.printf "field@.";
+         (* TODO keep field info when applying constructors, use here ?*)
+         raise CannotReduce
       | Not_found ->
          if debug
          then Format.printf "decl not found@.";
          raise CannotReduce end
-  | Efun _ -> raise CannotReduce
+  | Efun _ -> if debug then Format.printf "Efun@."; raise CannotReduce
   | Elet (Lvar(pv, e), ein) ->
      let v = interp_expr info e in
      interp_expr (add_pv pv v info) ein
-  (* FIXME other let decls *)
   | Eif (c, th, el) ->
      begin match interp_expr info c with
      | Vbool true -> interp_expr info th
@@ -678,13 +883,46 @@ let rec interp_expr info (e:Mltree.expr) : value =
        Vvoid l
   | Eignore e -> ignore (interp_expr info e); Vvoid
   | Ewhile (c, b) ->
+     if debug then Format.printf "while@.";
      begin match interp_expr info c with
      | Vbool true ->
         ignore (interp_expr info b);
         interp_expr info e
      | Vbool false -> Vvoid
      | _ -> raise CannotReduce end
-  | _ -> raise CannotReduce)
+  | Efor (x, pv1, dir, pv2, e) ->
+     if debug then Format.printf "for@.";
+     begin match (get pv1 info, get pv2 info) with
+     | (Vint i1, Vint i2) ->
+        if dir = To
+        then
+          for i = BigInt.to_int i1 to BigInt.to_int i2 do
+            ignore (interp_expr (add_pv x (Vint (BigInt.of_int i)) info) e)
+          done
+        else
+          for i = BigInt.to_int i1 downto BigInt.to_int i2 do
+            ignore (interp_expr (add_pv x (Vint (BigInt.of_int i)) info) e)
+          done;
+        Vvoid
+     | _ -> if debug then Format.printf "Non-integer for bounds@.";
+            raise CannotReduce
+     end
+  | Elet (Lany _,_) -> if debug then Format.printf "unhandled Lany@.";
+                       raise CannotReduce
+  | Elet ((Lsym(rs,_,_,_) as ld), e) ->
+     interp_expr (add_fundecl rs (Dlet ld) info) e
+  | Elet ((Lrec rdl as ld), e) ->
+     let info = List.fold_left
+                  (fun info rd -> add_fundecl rd.rec_sym (Dlet ld) info)
+                  info rdl in
+     interp_expr info e
+  | Eexn _ | Eraise _ -> if debug then Format.printf "unhandled exn/raise@.";
+                         raise CannotReduce
+  | Eabsurd -> if debug then Format.printf "Eabsurd@.";
+               raise CannotReduce
+  | Ehole -> if debug then Format.printf "Ehole@.";
+             raise CannotReduce
+  | Etry _-> if debug then Format.printf "Etry@."; raise CannotReduce)
 
 let eval_fun decl info = match decl with
   | Dlet (Lsym (_rs, _, _vl, expr)) ->
@@ -713,6 +951,7 @@ let rec term_of_value = function
      t_app (ls_of_rs rs) (List.map (fun f -> term_of_value (field_get f)) lf)
            (ls_of_rs rs).ls_value
   | Vvoid -> t_void
+  | Vref _ -> raise CannotReduce (* TODO ? *)
   | Varray _ -> raise CannotReduce
   | Vmatrix _ -> raise CannotReduce
 
@@ -735,24 +974,32 @@ let reflection_by_function s env = Trans.store (fun task ->
                 raise Exit)
         with Not_found -> o)
       ths None in
-  let (pmod, rs) = if o = None
+  let (_pmod, rs) = if o = None
                    then (if debug then Format.printf "Symbol %s not found@." s;
                          raise Exit)
                    else Opt.get o in
-  let (_, ms, _) = Pmodule.restore_path rs.rs_name in
+  (*let (_, ms, _) = Pmodule.restore_path rs.rs_name in*) (*FIXME remove or adapt*)
   let lpost = List.map open_post rs.rs_cty.cty_post in
   if List.exists (fun pv -> pv.pv_ghost) rs.rs_cty.cty_args
   then (if debug then Format.printf "ghost parameter@.";
         raise Exit);
   if debug then Format.printf "building module map@.";
-  let mm = Mstr.singleton ms pmod in
+  let mm = Mid.fold
+             (fun id th acc ->
+               try
+                 let pm = Pmodule.restore_module th in
+                 Mstr.add id.id_string pm acc
+               with Not_found -> acc)
+             ths Mstr.empty in
+  (*let mm = Mstr.singleton ms pmod in*)
   if debug then Format.printf "module map built@.";
   get_builtin_progs env;
   let decl = get_decl env mm rs in
   if debug then Format.printf "initial decl found@.";
   let args = List.map (fun pv -> pv.pv_vs) rs.rs_cty.cty_args in
   let rec reify_post = function
-    | [] -> raise NoReification
+    | [] -> if debug then Format.printf "no postcondition reifies@.";
+            raise NoReification
     | (vres, p)::t -> begin
         try
           if debug then Format.printf "new post@.";
@@ -760,10 +1007,11 @@ let reflection_by_function s env = Trans.store (fun task ->
           then Format.printf "post: %a, %a@."
                              Pretty.print_vs vres Pretty.print_term p;
           let (lp, lv, rt) = Apply.intros p in
-          let lv = lv @  args in
-          let renv = reify_term (init_renv kn lv) g rt in
+          let lv = lv @ args in
+          let renv = reify_term (init_renv kn lv env prev) g rt in
           let info = { env = env;
                        mm = mm;
+                       funs = Mrs.empty;
                        recs = Mrs.empty;
                        vars =
                          List.fold_left
@@ -789,10 +1037,10 @@ let reflection_by_function s env = Trans.store (fun task ->
 let () = wrap_and_register
            ~desc:"reflection_l <prop> attempts to prove the goal by reflection using the lemma prop"
            "reflection_l"
-           (Tprsymbol Ttrans_l) reflection_by_lemma
+           (Tprsymbol Tenvtrans_l) reflection_by_lemma
 
 let () = wrap_and_register
-           ~desc:"reflection_f <f> attempts to prove the goal by reflection using the contract of the function f"
+           ~desc:"reflection_f <f> attempts to prove the goal by reflection using the contract of the program function f"
            "reflection_f"
            (Tstring Tenvtrans_l) reflection_by_function
 
diff --git a/src/transform/reification.mli b/src/transform/reification.mli
index 950fa5c82c..24193c5f80 100644
--- a/src/transform/reification.mli
+++ b/src/transform/reification.mli
@@ -1,3 +1,3 @@
-val reflection_by_lemma: Decl.prsymbol -> Task.task Trans.tlist
+val reflection_by_lemma: Decl.prsymbol -> Env.env -> Task.task Trans.tlist
 
 val reflection_by_function: string -> Env.env -> Task.task Trans.tlist
-- 
GitLab