diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 10b74d7..31613ee 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -91,14 +91,6 @@ struct
    | x :: xs, _ -> x :: list_replace xs (id - 1) y
    | [], _ -> raise Not_found
 
-  (* TODO: FIXME: check if this foldl or foldr *)
-  let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
-    | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs 
-    | [], [], [] -> acc
-    | _, _, _ -> raise Cant_fold3_error
-
-  (* --- *)
-
   (* NOTE: old variant with assoc array *)
   (* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *)
   (* let mem_add (mem : mem) (v : value) : mem * memid = *)
@@ -155,32 +147,31 @@ struct
 
   (* --- eval rules --- *)
 
+  (* TODO: FIXME: check if this foldl or foldr *)
+  let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
+    | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs 
+    | [], [], [] -> acc
+    | _, _, _ -> raise Cant_fold3_error
+
   (* - value construction *)
 
-  let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
-    if is_trivial_v v
-    then match t with
-    | UnitT (Rd, _) -> (mem, v)
-    | UnitT (NRd, _) -> (mem, BotV)
-    | _ -> raise @@ Typing_error "valcopy: trivial value, wrong type"
-    else match t, v with
-    (* NOTE: replaced with if | best choice ?? *)
-    (* | UnitT (Rd, w), ZeroV -> (mem, v) *)
-    (* | UnitT (Rd, w), SmthV -> (mem, v) *)
-    (* | UnitT (Rd, w), BotV -> (mem, v) *)
-    (* | UnitT (NRd, w), ZeroV -> (mem, BotV) *)
-    (* | UnitT (NRd, w), SmthV -> (mem, BotV) *)
-    (* | UnitT (NRd, w), BotV -> (mem, BotV) *)
+  let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with
+    | UnitT (Rd, w), ZeroV -> (mem, v)
+    | UnitT (Rd, w), SmthV -> (mem, v)
+    | UnitT (Rd, w), BotV -> (mem, v)
+    | UnitT (NRd, w), ZeroV -> (mem, BotV)
+    | UnitT (NRd, w), SmthV -> (mem, BotV)
+    | UnitT (NRd, w), BotV -> (mem, BotV)
     | FunT _, FunV _ -> (mem, v)
     | RefT (Rf, _), RefV _ -> (mem, v)
     | RefT (Cp, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
                                let (mem'', id'') = mem_add mem' v' in
                                (mem'', RefV id'') 
     | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
-                                                                 (mem, v' :: vs') in 
+                                                                 mem, v' :: vs' in 
                               let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
                               (mem', TupleV vs')
-    | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
+    | _, _ -> raise @@ Typing_error "valcopy"
 
   (* - value update *)
 
@@ -198,7 +189,7 @@ struct
     if is_trivial_v u && is_trivial_v v
     then (if u == v then u else BotV)
     else match u, v with
-      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts)
+      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts) 
       | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
       | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
       | _, _ -> raise @@ Typing_error "valcomb"
@@ -296,7 +287,7 @@ struct
 
   (* full spoil *)
 
-  let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
+  let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
     match state with (mem, types, vals) ->
     let x = pathvar p in
     let id = List.assoc x vals in
@@ -310,8 +301,6 @@ struct
     match state with (mem, types, vals) -> match e, t with
       | UnitE, UnitT _ -> mem
       | PathE p, t -> argsspoilp state m t p
-      | RefE x, t -> argsspoilp state m t (VarP x)
-      (* TODO: FIXME: check RefE case ? *)
       | TupleE es, TupleT ts -> List.fold_left2
                                   (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
                                   mem ts es
@@ -324,10 +313,11 @@ struct
     let v = exprval mem oldvals e in
     (* let t' = pathtype types p in *)
     let (mem', v') = valcopy mem v t in
-    let (mem'', id) = mem_add mem' v' in
+    let (mem'', id) = mem_add mem' v in
     (mem'', (x, t) :: types, (x, id) :: vals)
 
   (* - function evaluation *)
+
   (* NOTE: not needed due to performed optimization in stmt_eval *)
   (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
 
@@ -335,26 +325,21 @@ struct
 
   let rec stmt_eval (state : state) (s : stmt) : state =
     match state with (mem, types, vals) -> match s with
-    (* TODO: FIXME: Add memoization *)
+    (* TODO: FIXME: Add memoisation *)
     | SkipS -> state
-    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *)
-                               pathval mem vals f in
-                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
-                               pathtype types f in
+    | CallS (f, es) -> let v = (* FIXME TMP Printf.printf "call, before v\n"; *) pathval mem vals f in
+                       let t = (* FIXME TMP Printf.printf "call, before t\n"; *) pathtype types f in
                        let types' : types = [] in
                        let vals' : vals = [] in
                        (match v, t with
                           | FunV (* xs, *) fstmts (* ) *), FunT ts ->
                             (* TODO: memoisation of the called functions *)
-                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *)
-                                                       List.fold_left2 (* TODO: FIXME: check x's order *)
-                              (fun (st, x) (m, t) e -> (addarg st vals x t e, x + 1))
+                            let (state_with_args, _) = (* FIXME TMP Printf.printf "call, before args\n"; *) List.fold_left2 (* TODO: FIXME: check x's order *)
+                              (fun (st, x) (m, t) p -> (addarg st vals x t p, x + 1))
                               ((mem, types', vals'), 0) ts es in
                             (* NOTE: same x's, so can use same args for all the statements *)
-                            let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *)
-                                                 List.map (stmt_eval state_with_args) fstmts in
-                            let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *)
-                                              List.fold_left2
+                            let _states_evaled = (* FIXME TMP Printf.printf "call, before eval\n"; *) List.map (stmt_eval state_with_args) fstmts in
+                            let mem_spoiled = (* FIXME TMP Printf.printf "call, before spoil\n"; *) List.fold_left2
                               (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
                               mem ts es in
                             (mem_spoiled, types, vals)
@@ -383,15 +368,15 @@ struct
                           then raise @@ Eval_error "choice"
                           else (memcomb meml memr, typesl, valsl)
 
-  (* --- program execution --- *)
+ (* --- program execution --- *)
 
-  let prog_eval (prog : prog) : state =
-    match prog with (decls, s) ->
-    let init_state = prog_init prog in
-    stmt_eval init_state s
+ let prog_eval (prog : prog) : state =
+   match prog with (decls, s) ->
+   let init_state = prog_init prog in
+   stmt_eval init_state s
 
-  let prog_eval_noret (prog : prog) : unit =
-    ignore @@ prog_eval prog
+ let prog_eval_noret (prog : prog) : unit =
+   ignore @@ prog_eval prog
 
   (* --- tests --- *)
 
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 76424e1..8ca0dc1 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -926,7 +926,7 @@ $s in stmt, f in X, x in X, a in X$
     $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
 
     // TODO:: is c important ?
-    $mu stretch(=>)^(m space rf c space t space rf x)_(cl vals, types cr) mu'$,
+    $mu stretch(=>)^(m space rf c t space rf x_(cl vals, types cr) mu'$,
   )
 ))
 
@@ -1042,6 +1042,21 @@ $s in stmt, f in X, x in X, a in X$
 
 #h(10pt)
 
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ READ $p$],
+
+    $vals, mu tval p eqmu 0$,
+
+    $cl types, vals, mu cr
+     xarrow("READ" p)
+     cl types, vals, mu cr$,
+  )
+))
+
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -1059,21 +1074,6 @@ $s in stmt, f in X, x in X, a in X$
   )
 ))
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ READ $p$],
-
-    $vals, mu tval p eqmu 0$,
-
-    $cl types, vals, mu cr
-     xarrow("READ" p)
-     cl types, vals, mu cr$,
-  )
-))
-
-#h(10pt)
-
 #h(10pt)
 
 #align(center, prooftree(
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 759730a..a277f4d 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -145,16 +145,16 @@ struct
   module Decl = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ((* 'd, *) 't, 'e, 'dl, 'mtl, 's) t = VarD of (* 'd * *) 't * 'e | FunD of (* 'd * *) 'dl * 'mtl * 's
+      type nonrec ('d, 't, 'e, 'dl, 'mtl, 's) t = VarD of 'd * 't * 'e | FunD of 'd * 'dl * 'mtl * 's
       [@@deriving gt ~options:{ show; gmap }]
-      type ground = ((* Nat.ground, *) Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
+      type ground = (Nat.ground, Type.ground, Expr.ground, Nat.ground List.ground, (Mode.ground * Type.ground) List.ground, Stmt.ground) t
     ]
   end
 
-  module Prg = struct
+  module Prog = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('dl, 's) t = Prg of 'dl * 's
+      type nonrec ('dl, 's) t = Prog of 'dl * 's
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = (Decl.ground List.ground, Stmt.ground) t
     ]
@@ -173,39 +173,39 @@ struct
 
   (* --- *)
 
-  module MemEnv = struct
+  module Mem = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('vl, 'd) t = MemEnv of 'vl * 'd
+      type nonrec ('vl, 'd) t = Mem of 'vl * 'd
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = (Value.ground List.ground, Nat.ground) t
     ]
   end
 
-  module TypesEnv = struct
+  module Types = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'dtl t = TypesEnv of 'dtl
+      type nonrec 'dtl t = Types of 'dtl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
     ]
   end
 
-  module ValsEnv = struct
+  module Vals = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'ddl t = ValsEnv of 'ddl
+      type nonrec 'ddl t = Vals of 'ddl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
     ]
   end
 
-  module StEnv = struct
+  module St = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec ('mem, 'types, 'vals) t = StEnv of 'mem * 'types * 'vals
+      type nonrec ('mem, 'types, 'vals) t = St of 'mem * 'types * 'vals
       [@@deriving gt ~options:{ show; gmap }]
-      type nonrec ground = (MemEnv.ground, TypesEnv.ground, ValsEnv.ground) t
+      type nonrec ground = (Mem.ground, Types.ground, Vals.ground) t
     ]
   end
 
@@ -238,651 +238,30 @@ struct
       list_ntho xs' id' x' }
   }
 
-
-  let rec list_foldlo f acc xs acc' = ocanren {
-    xs == [] & acc' == acc |
-    { fresh x', xs', acc_upd in
-      xs == x' :: xs' &
-      list_foldlo f acc xs' acc_upd &
-      f acc_upd x' acc' }
+  let mem_geto mem id v = ocanren {
+    fresh mem_data, mem_len, rev_id  in
+    Std.pair mem_data mem_len == mem &
+    Nat.addo (Nat.s rev_id) id mem_len &
+    list_ntho mem_data rev_id v
   }
 
-  let rec list_foldro f acc xs acc' = ocanren {
-    xs == [] & acc' == acc |
-    { fresh x', xs', acc_upd in
-      xs == x' :: xs' &
-      f acc x' acc_upd &
-      list_foldro f acc_upd xs' acc' }
-    (* TODO: inf search on swap, investigate *)
+  let mem_addo mem v mem_with_id' = ocanren {
+    fresh mem_data, mem_len, mem' in
+    Std.pair mem_data mem_len == mem &
+    mem' == Std.pair (v :: mem_data) (Nat.s mem_len) &
+    Std.pair mem' mem_len == mem_with_id'
   }
 
-
-  let rec list_foldr2o f acc xs ys acc' = ocanren {
-    xs == [] & ys == [] & acc' == acc |
-    { fresh x', xs', y', ys', acc_upd in
-      xs == x' :: xs' &
-      ys == y' :: ys' &
-      f acc x' y' acc_upd &
-      list_foldr2o f acc_upd xs' ys' acc' }
-  }
-
-  let rec list_foldl2o f acc xs ys acc' = ocanren {
-    xs == [] & ys == [] & acc' == acc |
-    { fresh x', xs', y', ys', acc_upd in
-      xs == x' :: xs' &
-      ys == y' :: ys' &
-      list_foldl2o f acc xs' ys' acc_upd &
-      f acc_upd x' y' acc' }
-  }
-
-  let rec list_foldr3o f acc xs ys zs acc' = ocanren {
-    xs == [] & ys == [] & zs == [] & acc' == acc |
-    { fresh x', xs', y', ys', z', zs', acc_upd in
-      xs == x' :: xs' &
-      ys == y' :: ys' &
-      zs == z' :: zs' &
-      f acc x' y' z' acc_upd &
-      list_foldr3o f acc_upd xs' ys' zs' acc' }
-  }
-
-  let rec list_foldl3o f acc xs ys zs acc' = ocanren {
-    xs == [] & ys == [] & zs == [] & acc' == acc |
-    { fresh x', xs', y', ys', z', zs', acc_upd in
-      xs == x' :: xs' &
-      ys == y' :: ys' &
-      zs == z' :: zs' &
-      list_foldl3o f acc xs' ys' zs' acc_upd &
-      f acc_upd x' y' z' acc' }
-  }
-
-  let rec list_zip_witho f xs ys zs = ocanren {
-    { fresh x, xs', y, ys', z, zs' in
-      xs == x :: xs' &
-      ys == y :: ys' &
-      zs == z :: zs' &
-      f x y z &
-      list_zip_witho f xs' ys' zs' } |
-    { fresh x, xs' in
-      xs == x :: xs' &
-      ys == [] &
-      zs == [] } |
-    { fresh y, ys' in
-      xs == [] &
-      ys == y :: ys' &
-      zs == [] } |
-    { xs == [] & ys == [] & zs == [] }
-  }
-
-  (* --- *)
-
-  let mem_geto mem id v =
-    let open MemEnv in
-    ocanren {
-      fresh mem_data, mem_len, rev_id in
-      MemEnv (mem_data, mem_len) == mem &
-      Nat.addo (Nat.s rev_id) id mem_len &
-      list_ntho mem_data rev_id v
-  }
-
-  let mem_addo mem v mem_with_id' =
-    let open MemEnv in
-    ocanren {
-      fresh mem_data, mem_len, mem' in
-      MemEnv (mem_data, mem_len) == mem &
-      mem' == MemEnv (v :: mem_data, Nat.s mem_len) &
-      Std.pair mem' mem_len == mem_with_id'
-  }
-
-  let mem_seto mem id v mem' =
-    let open MemEnv in
-    ocanren {
-      fresh mem_data, mem_len, rev_id, mem_data' in
-      MemEnv (mem_data, mem_len) == mem &
-      Nat.addo (Nat.s rev_id) id mem_len &
-      list_replaceo mem_data rev_id v mem_data' &
-      MemEnv (mem_data', mem_len) == mem'
-  }
-
-  let is_trivial_vo v =
-    let open Value in
-    ocanren {
-    v == ZeroV | v == SmthV | v == BotV
-  }
-
-  let rec pathvaro p x =
-    let open Path in
-    ocanren {
-      p == VarP x |
-      { fresh p' in p == DerefP p' & pathvaro p' x } |
-      { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
-  }
-
-  let types_assoco id types tp =
-    let open TypesEnv in
-    ocanren {
-      fresh tps in
-      types == TypesEnv tps &
-      List.assoco id tps tp
-    }
-
-  let vals_assoco id vals v =
-    let open ValsEnv in
-    ocanren {
-      fresh vs in
-      vals == ValsEnv vs &
-      List.assoco id vs v
-    }
-
-  let rec pathtypeo types p tp =
-    let open Path in
-    let open Type in
-    ocanren {
-      { fresh x in
-        p == VarP x &
-        types_assoco x types tp } |
-      { fresh p', tp', _c in
-        p == DerefP p' &
-        pathtypeo types p' tp' &
-        tp' == RefT (_c, tp) } |
-      { fresh p', id', tp', tps in
-        p == AccessP (p', id') &
-        pathtypeo types p' tp' &
-        tp' == TupleT tps &
-        list_ntho tps id' tp }
-  }
-
-  let rec pathvalo mem vals p v =
-    let open Path in
-    let open Value in
-    ocanren {
-      { fresh x, id in
-        p == VarP x &
-        vals_assoco x vals id &
-        mem_geto mem id v } |
-      { fresh p', v', id in
-        p == DerefP p' &
-        pathvalo mem vals p' v' &
-        v' == RefV id &
-        mem_geto mem id v } |
-      { fresh p', id, v', vs in
-        p == AccessP (p', id) &
-        pathvalo mem vals p' v' &
-        v' == TupleV vs &
-        list_ntho vs id v }
-  }
-
-  (* --- eval rules --- *)
-
-  (* - value construction *)
-
-  let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
-    ocanren {
-      fresh mem, vs, mem', v', mem_with_v', vs' in
-      Std.pair mem vs == mem_with_vs &
-      valcopyo mem v tp mem_with_v' &
-      Std.pair mem' v' == mem_with_v' &
-      vs' == v' :: vs &
-      mem_with_vs' == Std.pair mem vs'
-  }
-  and valcopyo mem v tp mem_with_id' = 
-    let open Type in
-    let open Value in
-    let open ReadCap in
-    let open CopyCap in
-    ocanren {
-      { fresh r, w in
-        is_trivial_vo v &
-        tp == UnitT (r, w) &
-        { { r == Rd & mem_with_id' == Std.pair mem v } |
-          { r == NRd & mem_with_id' == Std.pair mem BotV } } } |
-      { fresh stmts, ts in
-        v == FunV stmts &
-        tp == FunT ts &
-        mem_with_id' == Std.pair mem v } |
-      { fresh c, tp', id in
-        v == RefV id &
-        tp == RefT (c, tp') &
-        { { c == Rf & mem_with_id' == Std.pair mem v } |
-          { fresh v, mem_cp, v_cp, mem_with_v_cp,
-                  mem_add, id_add, mem_with_id_add in
-            c == Cp &
-            mem_geto mem id v &
-            valcopyo mem v tp mem_with_v_cp &
-            Std.pair mem v_cp == mem_with_v_cp &
-            mem_addo mem_cp v_cp mem_with_id_add &
-            Std.pair mem_add id_add == mem_with_id_add &
-            mem_with_id' == (mem_add, RefV id_add) } } } |
-      { fresh vs, tps, init_mem_with_vs, mem_with_vs', mem', vs' in
-        v == TupleV vs &
-        tp == TupleT tps &
-        init_mem_with_vs == Std.pair mem [] &
-        list_foldl2o valcopy_foldero init_mem_with_vs vs tps mem_with_vs' &
-        Std.pair mem' vs' == mem_with_vs' &
-        mem_with_id' == Std.pair mem' (TupleV vs') }
-  }
-
-  (* - value update *)
-
-  let rec valupdo mem v p b mem_with_v' =
-    let open Path in
-    let open Value in
-    ocanren {
-      { fresh x in
-        p == VarP x &
-        mem_with_v' == Std.pair mem b } |
-      { fresh p', id, v', mem_upd, v_upd, mem_with_v_upd, mem_st in
-        p == DerefP p' &
-        v == RefV id &
-        mem_geto mem id v' &
-        valupdo mem v' p' b mem_with_v_upd &
-        Std.pair mem_upd v_upd == mem_with_v_upd &
-        mem_seto mem_upd id v_upd mem_st &
-        mem_with_v' == Std.pair mem_st (RefV id) } |
-      { fresh p', id, vs', v', mem_upd, v_upd, mem_with_v_upd, vs_upd in
-        p == AccessP (p', id) &
-        v == TupleV vs' &
-        list_ntho vs' id v' &
-        valupdo mem v' p' b mem_with_v_upd &
-        Std.pair mem_upd v_upd == mem_with_v_upd &
-        list_replaceo vs' id v_upd vs_upd &
-        mem_with_v' == Std.pair mem_upd (TupleV vs_upd) }
-  }
-
-  (* - value combination *)
-
-  let rec valcombo u v u' =
-    let open Value in
-    ocanren {
-    { is_trivial_vo u &
-      is_trivial_vo v &
-      (* TODO: do not use disequality constraint ? *)
-      { { u == v & u' == u } | { u =/= v & u' == BotV } } } |
-    { fresh ustmts, vstmts, ustmts' in
-      u == FunV ustmts &
-      v == FunV vstmts &
-      (* TODO: swap stmts order o efficiency ? *)
-      List.appendo ustmts vstmts ustmts' &
-      u' == FunV ustmts' } |
-    { fresh a, b in
-      u == RefV a &
-      v == RefV b &
-      a == b } |
-    { fresh us, vs, us' in
-      u == TupleV us &
-      v == TupleV vs &
-      list_zip_witho valcombo us vs us' &
-      u' == TupleV us' }
-  }
-
-  let memcombo m n m' =
-    let open MemEnv in
-    ocanren {
-    fresh mm, ml, nm, nl, mm' in
-    MemEnv (mm, ml) == m &
-    MemEnv (nm, nl) == n &
-    list_zip_witho valcombo mm nm mm' &
-    m' == MemEnv (mm', ml)
-  }
-
-  (* - expression evaluation *)
-
-  let rec exprvalo mem vals e v' = 
-    let open Expr in
-    let open Value in
-    ocanren {
-      { e == UnitE & v' == ZeroV } |
-      { fresh p in
-        e == PathE p &
-        pathvalo mem vals p v' } |
-      { fresh x, v in
-        e == RefE x &
-        vals_assoco x vals v &
-        v' == RefV v } |
-      { fresh es, vs' in
-        e == TupleE es &
-        List.mapo (exprvalo mem vals) es vs' &
-        v' == TupleV vs' }
-  }
-
-  (* - expression typing *)
-
-  let rec exprtypeo types e tp' = 
-    let open Expr in
-    let open Type in
-    let open ReadCap in
-    let open WriteCap in
-    let open CopyCap in
-    ocanren {
-      { e == UnitE & tp' == UnitT (Rd, NeverWr) } |
-      { fresh p in
-        e == PathE p &
-        pathtypeo types p tp' } |
-      { fresh x, tp in
-        e == RefE x &
-        types_assoco x types tp &
-        tp' == RefT (Rf, tp) } |
-      { fresh es, tps' in
-        e == TupleE es &
-        List.mapo (exprtypeo types) es tps' &
-        tp' == TupleT tps' }
-  }
-
-  (* - context initialization *)
-
-  let add_declo st x d st' =
-    let open StEnv in
-    let open Decl in
-    let open TypesEnv in
-    let open ValsEnv in
-    ocanren {
-      fresh mem, types, vals in
-      st == StEnv (mem, TypesEnv types, ValsEnv vals) &
-      {
-        { fresh tp, e, v,
-                mem_with_v_cp, mem_cp, v_cp,
-                mem_with_id_add, mem_add, id_add in
-          d == VarD (tp, e) &
-          exprvalo mem (ValsEnv vals) e v &
-          valcopyo mem v tp mem_with_v_cp &
-          Pair.pair mem_cp v_cp == mem_with_v_cp &
-          mem_addo mem_cp v_cp mem_with_id_add &
-          Pair.pair mem_add id_add == mem_with_id_add &
-          st' == StEnv (mem_add,
-                        TypesEnv ((Pair.pair x tp) :: types),
-                        ValsEnv ((Pair.pair x id_add) :: vals))
-          }
-      }
-  }
-
-  let empty_memo m =
-    let open MemEnv in
-    ocanren { m == MemEnv ([], 0) }
-
-  let empty_stateo st =
-    let open StEnv in
-    let open TypesEnv in
-    let open ValsEnv in
-    ocanren {
-      fresh m in
-      empty_memo m &
-      st == StEnv (m, TypesEnv [], ValsEnv [])
-  }
-
-  (* TODO: better way ??? *)
-  let globals_min_ido x = ocanren { x == 1000 }
-
-  let prog_init_foldero st_with_id d st_with_id' =
-    ocanren {
-      fresh st, x, st' in
-      Std.pair st x == st_with_id &
-      add_declo st x d st' &
-      st_with_id' == Std.pair st' (Nat.s x)
-  }
-
-  let prog_inito prog st' =
-    let open Prg in
-    ocanren {
-      fresh decls, s, st_init, min_id, st_with_id', _id' in
-      prog == Prg (decls, s) &
-      empty_stateo st_init &
-      globals_min_ido min_id &
-      list_foldlo prog_init_foldero (Std.pair st_init min_id) decls st_with_id' &
-      Std.pair st' _id' == st_with_id'
-  }
-
-  (* - call values spoil *)
-
-  (* TODO: check that negation is interpreted correctly *)
-  let is_correct_tagso v r w _r' w' m c =
-    let open Value in
-    let open ReadCap in
-    let open WriteCap in
-    let open Mode in
-    let open CopyCap in
-    ocanren {
-      { r == NRd | v == ZeroV } &
-      { r == NRd | is_ino m } &
-      { is_not_outo m | w == AlwaysWr } &
-      { w == NeverWr |
-        { is_not_outo m & c == Cp } |
-        w' == AlwaysWr } &
-      is_trivial_vo v
-  }
-
-  let rec valspoil_foldero m c mem_with_vs tp u v mem_with_vs' = ocanren {
-    fresh mem, vs, mem', v' in
-    Std.pair mem vs == mem_with_vs &
-    valspoilo mem v tp u m c (Std.pair mem' v') &
-    mem_with_vs' == Std.pair mem' (v' :: vs)
-  }
-  and valspoilo mem v tp u m c mem_with_v' =
-    let open Type in
-    let open Value in
-    let open Mode in
-    let open WriteCap in
-    let open CopyCap in
-    ocanren {
-      { fresh r, w, r', w' in
-        tp == UnitT (r, w) &
-        u == UnitT (r', w') &
-        is_trivial_vo v &
-        is_correct_tagso v r w r' w' m c &
-        {
-          { is_not_outo m &
-            c == Rf &
-            { w == AlwaysWr | w == MayWr } &
-            mem_with_v' == Std.pair mem BotV } |
-          { is_outo m &
-            w == AlwaysWr &
-            mem_with_v' == Std.pair mem ZeroV } |
-          { { is_outo m | c == Cp | w == NeverWr } &
-            { is_not_outo m | w == MayWr | w == NeverWr } &
-            mem_with_v' == Std.pair mem v }
-        } } |
-      { fresh ts, us, _stmts in
-        tp == FunT ts &
-        u == FunT us &
-        v == FunV _stmts &
-        ts == us &
-        mem_with_v' == Std.pair mem v } |
-      { fresh ctp', tp', cu', u', id', v', mem_sp, v_sp, mem_set in
-        tp == RefT (ctp', tp') &
-        u == RefT (cu', u') &
-        v == RefV id' &
-        mem_geto mem id' v' &
-        valspoilo mem v' tp' u' m ctp' (Std.pair mem_sp v_sp) &
-        mem_seto mem_sp id' v_sp mem_set &
-        mem_with_v' == Std.pair mem_set (RefV id') } |
-      { fresh tps, us, vs, mem_sp,vs_sp in
-        tp == TupleT tps &
-        u == TupleT us &
-        v == TupleV vs &
-        list_foldl3o (valspoil_foldero m c)
-                     (Std.pair mem []) tps us vs
-                     (Std.pair mem_sp vs_sp) &
-        mem_with_v' == Std.pair mem_sp (TupleV vs_sp)
-      }
-  }
-
-  (* full spoil *)
-
-  let argspoilpo st m tp p mem' =
-    let open StEnv in
-    let open CopyCap in
-    ocanren {
-      fresh mem, types, vals, x, id, b, tp',
-            mem_sp, b_sp, v_sp, mem_upd, v_upd in
-      st == StEnv (mem, types, vals) &
-      pathvaro p x &
-      vals_assoco x vals id &
-      pathvalo mem vals p b &
-      pathtypeo types p tp' &
-      valspoilo mem b tp tp' m Rf(Std.pair mem_sp b_sp) &
-      mem_geto mem_sp id v_sp &
-      valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
-      mem_seto mem_upd id v_upd mem'
-  }
-
-  let rec argspoile_foldero types vals m mem tp e mem' =
-    let open StEnv in
-    ocanren {
-      fresh st in
-      st == StEnv (mem, types, vals) &
-      argspoileo st m tp e mem'
-  }
-  and argspoileo st m tp e mem' =
-    let open StEnv in
-    let open Expr in
-    let open Type in
-    let open Path in
-    ocanren {
-      fresh _r, _w, mem, types, vals in
-      st == StEnv (mem, types, vals) &
-      {
-        { e == UnitE &
-          tp == UnitT (_r, _w) &
-          mem' == mem } |
-        { fresh p in
-          e == PathE p &
-          argspoilpo st m tp p mem' } |
-        { fresh x in
-          e == RefE x &
-          argspoilpo st m tp (VarP x) mem' } |
-        { fresh es, tps in
-          e == TupleE es &
-          tp == TupleT tps &
-          list_foldl2o (argspoile_foldero types vals m) mem tps es mem'}
-      }
-  }
-
-  (* - funciton argument addition *)
-
-  let addargo st oldvals x tp e st' =
-    let open StEnv in
-    let open TypesEnv in
-    let open ValsEnv in
-    ocanren {
-      fresh mem, types, vals, v, mem_cp, v_cp, mem_add, id_add in
-      st == StEnv (mem, TypesEnv types, ValsEnv vals) &
-      exprvalo mem oldvals e v &
-      valcopyo mem v tp (Std.pair mem_cp v_cp) &
-      mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
-      st' == StEnv (mem_add,
-                    TypesEnv ((Std.pair x tp) :: types),
-                    ValsEnv ((Std.pair x id_add) :: vals))
-  }
-
-  (* - function evaluation *)
-  (* NOTE: not needed due to performed optimization in stmt_eval ? *)
-
-  (* - statement evaluation *)
-  (* TODO *)
-
-  let rec stmt_addarg_foldero vals st_with_id mtp e st_with_id' = ocanren {
-    fresh st, x, m, tp, st' in
-    Std.pair st x == st_with_id &
-    Std.pair m tp == mtp &
-    addargo st vals x tp e st' &
-    st_with_id' == Std.pair st' (Nat.s x)
-  }
-  and stmt_eval_spoil_foldero types vals mem mtp e mem' =
-    let open StEnv in
-    ocanren {
-      fresh m, tp, st in
-      Std.pair m tp == mtp &
-      st == StEnv (mem, types, vals) &
-      argspoileo st m tp e mem'
-  }
-  and stmt_evalo st s st' =
-    let open StEnv in
-    let open Stmt in
-    let open Value in
-    let open Type in
-    let open WriteCap in
-    let open TypesEnv in
-    let open ValsEnv in
-    ocanren {
-      fresh mem, types, vals in
-      st == StEnv (mem, types, vals) &
-      {
-        { s == SkipS & st == st' } |
-        { fresh f, es, v, tp, types', vals',
-                fstmts, tps, st',
-                state_with_args, _arg_id,
-                _states_evaled,
-                mem_spoiled in
-          s == CallS (f, es) &
-          pathvalo mem vals f v &
-          pathtypeo types f tp &
-          types' == TypesEnv [] &
-          vals' == ValsEnv [] &
-          v == FunV fstmts &
-          tp == FunT tps &
-          st' == StEnv (mem, types', vals') &
-          (* TODO: type error, fix required *)
-          list_foldl2o (stmt_addarg_foldero vals)
-                       (Std.pair st' 0) tps es
-                       (Std.pair state_with_args _arg_id) &
-          List.mapo (stmt_evalo state_with_args) fstmts _states_evaled &
-          (* TODO: FIXME check left or right order *)
-          list_foldl2o (stmt_eval_spoil_foldero types vals)
-                      mem tps es mem_spoiled &
-          st' == StEnv (mem_spoiled, types, vals) } |
-        { fresh p, tp, _r, w, x, id, v,
-                mem_upd, v_upd, mem_set in
-          s == WriteS p &
-          pathtypeo types p tp &
-          tp == UnitT (_r, w) &
-          { w == AlwaysWr | w == MayWr } &
-          pathvaro p x &
-          vals_assoco x vals id &
-          mem_geto mem id v &
-          valupdo mem v p ZeroV (Std.pair mem_upd v_upd) &
-          mem_seto mem_upd id v_upd mem_set &
-          st' == StEnv (mem_set, types, vals) } |
-        { fresh p in
-          s == ReadS p &
-          pathvalo mem vals p ZeroV &
-          st == st' } |
-        { fresh sl, sr, stl in
-          s == SeqS (sl, sr) &
-          stmt_evalo st sl stl &
-          stmt_evalo stl sr st' } |
-        { fresh sl, sr, stl, str,
-                meml, typesl, valsl,
-                memr, typesr, valsr,
-                mem' in
-          s == ChoiceS (sl, sr) &
-          stmt_evalo st sl stl &
-          stmt_evalo st sr str &
-          str == StEnv (memr, typesr, valsr) &
-          stl == StEnv (meml, typesl, valsl) &
-          typesl == typesr &
-          valsl == valsr &
-          memcombo meml memr mem' &
-          st' == StEnv (mem', typesl, valsl) }
-      }
-  }
-
-  (* --- program execution --- *)
-
-  let prog_evalo prog st' =
-    let open Prg in
-    ocanren {
-      fresh decls, s, init_st in 
-      prog == Prg (decls, s) &
-      prog_inito prog init_st &
-      stmt_evalo init_st s st'
+  let mem_seto mem id v mem' = ocanren {
+    fresh mem_data, mem_len, rev_id, mem_data' in
+    Std.pair mem_data mem_len == mem &
+    Nat.addo (Nat.s rev_id) id mem_len &
+    list_replaceo mem_data rev_id v mem_data' &
+    Std.pair mem_data' mem_len == mem'
   }
 
   (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
-  (* --- tests --- *)
-  (* TODO *)
-
-  (* - shortcuts *)
-  (* TODO *)
-
   (* --- *)
 
   (* let rec list_zip_witho f xs ys zs = ocanren { *)