diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 1b5740e..0779a8a 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -1,212 +1,50 @@
 module Functional =
 struct
 
-  type data = int
-  type memid = int
+  (* --- types --- *)
 
-  (* --- syntax --- *)
+  type data = int
 
   type read_cap = Rd | NRd
-
   type write_cap = AlwaysWr | MayWr | NeverWr
-  type copy_cap = Cp | Rf
+  type copy_cap = Cp | NCp
 
   type in_cap = In | NIn
   type out_cap = Out | NOut
 
-  type mode = in_cap * out_cap
+  type tag = read_cap * write_cap * copy_cap * in_cap * out_cap
 
   type path = VarP of data | DerefP of path | AccessP of path * data
+  type argtype = UnitT | RefT of tag * argtype | TupleT of argtype list | FunT of data
+  type argmem = VarM of data | RefM of argmem | TupleM of argmem list | FunM
 
-  type atype = UnitT of read_cap * write_cap
-             | RefT of copy_cap * atype
-             | TupleT of atype list
-             | FunT of data (* declaration id for ease of impl (?) *)
+  type stmt = Call of data * path list | CallLam of path * path list | Read of path | Write of path | Choice of stmt list * stmt list
+  type body = stmt list
 
-  type mtype = mode * atype
-
-  type expr = UnitE
-            | PathE of path
-            (* | RefE *)
-            | TupleE of expr list
-
-  type stmt = CallS of path * expr list
-            | WriteS of path
-            | ReadS of path
-            | SeqS of stmt * stmt
-            | ChoiceS of stmt * stmt
-
-  type decl = VarD of (* data * *) atype * expr
-            | FunD of (* data * *) (* (data * *) mtype (* )  *) list * stmt
-
-  type prog = decl list * stmt
+  type fun_decl = argtype list * body
+  type prog = fun_decl list * fun_decl
 
   (* --- exceptions --- *)
 
-  (* exception Incorrect_memory_access of int *)
-  (* exception Ref_rvalue_argument of int *)
-  (* exception Incorrect_const_cast of int *)
-  (* exception Invalid_argument_tag of int *)
-  (* exception Incompatible_states *)
-  (* exception Incompatible_path_and_type *)
-  (* exception Incompatible_path_and_mem *)
-  (* exception Incompatible_path_and_type_for_tag *)
-  exception Typing_error of string
+  exception Incorrect_memory_access of int
+  exception Ref_rvalue_argument of int
+  exception Incorrect_const_cast of int
+  exception Invalid_argument_tag of int
+  exception Incompatible_states
+  exception Incompatible_path_and_type
+  exception Incompatible_path_and_mem
+  exception Incompatible_path_and_type_for_tag
 
-  (* value model & memory model *)
+  (* --- static interpreter (no rec) --- *)
 
-  type deepvalue = ZeroDV
-                 | SmthDV
-                 | BotDV
-                 | FunDV of (* data list * *) stmt
-                 | RefDV of deepvalue
-                 | TupleDV of deepvalue list
+  (* TODO: allow data (rvalue) in calls ?? *)
+  type arg = RValue | LValue of path
+  type value = UnitV | UndefV | BotV
 
-  type value = ZeroV
-             | SmthV
-             | BotV
-             | FunV of (* data list * *) stmt
-             | RefV of memid
-             | TupleV of value list
+  type env = (int * (argmem * argtype)) list
 
-  (* TODO: any additional difference between rvalue and lvalue now ?? *)
-
-  (* --- *)
-
-  type mem = (memid * value) list * memid (* NOTE: memory and first free elem *)
-  type types = (data * atype) list
-  type vals = (data * memid) list
-  type state = mem * types * vals
-
-  (* --- *)
-
-  (* TODO: FIXME: use list_replace for memory instead ?? *)
-  let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem)
-  let mem_add (mem : mem) (v : value) : mem * memid =
-    (((snd mem, v) :: fst mem, snd mem + 1), snd mem)
-  let mem_set (mem : mem) (id : memid) (v : value) : mem =
-    ((id, v) :: fst mem, snd mem)
-
-  let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
-    | ZeroV -> ZeroDV
-    | SmthV -> SmthDV
-    | BotV -> BotDV
-    | FunV s -> FunDV s
-    | RefV id -> RefDV (v_to_deepv mem @@ mem_get mem id)
-    | TupleV vs -> TupleDV (List.map (v_to_deepv mem) vs)
-
-  let is_trivial_v (v : value) : bool = 
-    v == ZeroV || v == SmthV || v == BotV
-
-  (* --- path accessors --- *)
-
-  let rec pathvar (p : path) : data = match p with
-    | VarP x -> x
-    | DerefP p -> pathvar p
-    | AccessP (p, _) -> pathvar p
-
-  let rec pathtype (types : types) (p : path) : atype = match p with
-    | VarP x -> List.assoc x types
-    | DerefP p -> (match pathtype types p with
-                    | RefT (_, t) -> t
-                    | _ -> raise @@ Typing_error "pathtype: deref")
-    | AccessP (p, id) -> match pathtype types p with
-                           | TupleT ts -> (List.nth ts id)
-                           | _ -> raise @@ Typing_error "pathtype: access"
-
-  let rec pathval (mem :  mem) (vals : vals) (p : path) : value = match p with
-    | VarP x -> mem_get mem @@ List.assoc x vals
-    | DerefP p -> (match pathval mem vals p with
-                    | RefV id -> mem_get mem id
-                    | _ -> raise @@ Typing_error "pathval: deref")
-    | AccessP (p, id) -> match pathval mem vals p with
-                           | TupleV vs -> (List.nth vs id)
-                           | _ -> raise @@ Typing_error "pathval: access"
-
-  (* --- eval rules --- *)
-
-  (* - utils *)
-
-  let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
-   | _ :: xs, 0 -> y :: xs
-   | x :: xs, _ -> x :: list_replace xs (id - 1) y
-   | [], _ -> raise Not_found
-
-  (* - value construction *)
-
-  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 
-                              let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
-                              (mem', TupleV vs')
-    | _, _ -> raise @@ Typing_error "valcopy"
-
-  (* - value update *)
-
-  let rec valupd (mem : mem) (v : value) (p : path) (b : value) : mem * value = match p, v with
-    | VarP x, _ -> (mem, b)
-    | DerefP p, RefV id -> let (mem', v') = valupd mem (mem_get mem id) p b in
-                           (mem_set mem' id v', RefV id)
-    | AccessP (p, id), TupleV vs -> let (mem', v') = valupd mem (List.nth vs id) p b in
-                                    (mem', TupleV (list_replace vs id v'))
-    | _, _ -> raise @@ Typing_error "valupd"
-
-  (* - value combination *)
-
-  let rec valcomb (u : value) (v : value) : value =
-    if is_trivial_v u && is_trivial_v v
-    then (if u == v then u else BotV)
-    else match u, v with
-      (* TODO: FIXME: combining semanticsfor funcitons statements *)
-      | FunV s, FunV t  -> if s == t then u else raise @@ Typing_error "valcomb: fun"
-      | 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"
-
-  (* TODO: func for list memory, not assoc list *)
-  (* let rec memcomb (m : mem) (n : mem) : mem = *)
-    (* if snd m != snd n *)
-    (* then raise @@ Typing_error "memcomb" *)
-    (* else (List.map2 valcomb (fst m) (fst n), snd m) *)
-
-  (* - call values spoil *)
-
-  (* TODO: check all cases *)
-  let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
-                      (r' : read_cap) (w' : write_cap) (m : mode)
-                      (c : copy_cap) : bool =
-    (r != Rd || v == ZeroV) &&
-    (r != Rd || fst m == In) &&
-    (o != Out || w == AlwaysWr) &&
-    (* TODO: check *)
-    ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
-    is_trivial_v v
-
-  let rec valspoil (mem : mem) (v : value) (t : atype)
-                   (u : atype) (m : mode) (c : copy_cap)
-                   : mem * value = match t, u, v with
-    | UnitT (r, w), UnitT (r', w'), _ -> (* TODO FIXME *) raise Not_found
-    | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
-    | RefT (ct, t), RefT (cu, u), RefV id ->
-      let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
-      (mem_set mem id v', RefV id)
-    | TupleT ts, TupleT us, TupleV vs -> (* TODO FIXME *) raise Not_found
-    | _, _, _ ->  raise @@ Typing_error "valspoil"
-
-(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
-
-  (* let rec argsspoil (* full spoil *) *)
+  (* env * memory * last unused memory * visited functions *) 
+  type state = env * value list * int * int list
 
   (* --- *)
 
@@ -439,12 +277,12 @@ struct
   let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
   let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
   let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
-  let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut)
-  let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut)
-  let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut)
-  let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut)
-  let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut)
-  let i_ref : tag = (NRd, NeverWr, Rf, In, NOut)
+  let rwi_ref : tag = (Rd, AlwaysWr, NCp, In, NOut)
+  let rmwi_ref : tag = (Rd, MayWr, NCp, In, NOut)
+  let ri_ref : tag = (Rd, NeverWr, NCp, In, NOut)
+  let wi_ref : tag = (NRd, AlwaysWr, NCp, In, NOut)
+  let mwi_ref : tag = (NRd, MayWr, NCp, In, NOut)
+  let i_ref : tag = (NRd, NeverWr, NCp, In, NOut)
 
   (* >> tests without functions *)
 
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 3449afc..1221071 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -73,7 +73,7 @@
   Prod(
     `mode`,
     {
-      Or[$inTag outTag$][]
+      Or[$inTag space outTag$][]
     }
   ),
   Prod(
@@ -112,7 +112,7 @@
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      // TODO: decide what is the result of ref expr eval
+      // TODO: FIXME: decide what is the result of ref expr eval
       // Or[$rf expr$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
     }
@@ -138,7 +138,7 @@
   Prod(
     `prog`,
     {
-      Or[$decl+ space stmt$][declarations and executed statement]
+      Or[$decl stmt$][declarations and executet statement]
     }
   ),
 )
@@ -155,7 +155,7 @@
       Or[$0$][valid value of simple type] // `Unit`
       Or[$\#$][valid or spoiled value of simple type] // `Unit`
       Or[$bot$][spoiled value of simple type] // `Unit`
-      Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
+      Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
       Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[deepValue+]$][tuple value] // `Prod`
     }
@@ -166,7 +166,7 @@
       Or[$0$][valid value of simple type] // `Unit`
       Or[$\#$][valid or spoiled value of simple type] // `Unit`
       Or[$bot$][spoiled value of simple type] // `Unit`
-      Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
+      Or[$lambda overline(x) space stmt$][function pointer value] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
@@ -225,6 +225,9 @@ $sigma : envt := X -> type, space types : envt$ - #[ типы значений 
 // $d in decl, $
 $s in stmt, f in X, x in X, a in X$
 
+// FIXME ??
+// $d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
+
 === Path Accessors
 
 Набор частично определённых фунций для работы с путями.
@@ -370,61 +373,85 @@ $s in stmt, f in X, x in X, a in X$
 
 // TODO: introduce spep env argument ??
 
-// --- >>> ---
-// === Moded Type Correctness
-// *NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
-// #let tcorrect = $attach(tack.r, br: #[correct])$
-// $ vals in envv, types in envt, space mu in mem, space m in mode,
-//   space c in copyTag, space r, r' in readTag, space w, w' in writeTag,
-//   space v in value, space t, t' in type $
-// #h(10pt)
-// // TODO: FIXME: complete rule check
-// // + add part about ref -> not copy later
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ unit assignment tags correctness],
-//     $r = Read => m = (In, \_)$, 
-//     $m = (\_, Out) => w = AlwaysWrite$,
-//     // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
-//     $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
-//     // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
-//     $v in {0, \#, bot}$,
-//     $r = Read => v = 0$,
-//     $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
-//   )
-// ))
-// #h(10pt)
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ function pointer tags correctness],
-//     $types, vals, mu, m, c tcorrect lambda : lambda space overline(t) -> lambda space overline(t)$,
-//   )
-// ))
-// #h(10pt)
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ ref assignment tags correctness],
-//     $types, vals, mu, m, c_r tcorrect v : t -> t'$,
-//     // TODO: FIXME: which tag translations are correct ?? <- only assignee?
-//     $types, vals, mu, m, c tcorrect rf space v : rf c' space t -> rf c_r space t'$,
-//   )
-// ))
-// #h(10pt)
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ tuple assignmenttags correctness],
-//     $types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
-//     $...$,
-//     $types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
-//     $types, vals, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, ... t'_n]$,
-//   )
-// ))
-// #h(10pt)
-// --- <<< ---
+=== Moded Type Correctness
+
+*NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
+
+#let tcorrect = $attach(tack.r, br: #[correct])$
+
+// TODO: FIXME: well formatness for mode, extract
+// TODO: FIXME: check for mode, is recursion required ??
+// TODO: FIXME: check mode & access corectness in os correct
+
+$ vals in envv, types in envt, space mu in mem, space m in mode,
+  space c in copyTag, space r, r' in readTag, space w, w' in writeTag,
+  space v in value, space t, t' in type $
+
+#h(10pt)
+
+// TODO: FIXME: complete rule check
+// + add part about ref -> not copy later
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit assignment tags correctness],
+
+    $r = Read => m = (In, \_)$, 
+    $m = (\_, Out) => w = AlwaysWrite$,
+    // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
+    $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
+
+    // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
+    $v in {0, \#, bot}$,
+    $r = Read => v = 0$,
+
+    $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ function pointer tags correctness],
+
+    $types, vals, mu, m, c tcorrect lambda : lambda space overline(t) -> lambda space overline(t)$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ ref assignment tags correctness],
+
+    $types, vals, mu, m, c_r tcorrect v : t -> t'$,
+
+    // TODO: FIXME: which tag translations are correct ?? <- only assignee?
+    $types, vals, mu, m, c tcorrect rf space v : rf c' space t -> rf c_r space t'$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ tuple assignmenttags correctness],
+
+    $types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
+
+    $...$,
+
+    $types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
+
+    $types, vals, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, ... t'_n]$,
+  )
+))
+
+#h(10pt)
 
 === Value Construction
 
@@ -448,7 +475,7 @@ $s in stmt, f in X, x in X, a in X$
     name: [ new trivial $not$ read value],
 
     $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl not Read \, w cr)_new cl bot, mu cr$,
+    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl bot, mu cr$,
   )
 ))
 
@@ -457,7 +484,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ new funciton pointer value],
 
-    $cl lambda overline(t) s, mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(t) s, mu cr$,
+    $cl lambda overline(t) s, mu cr xarrowSquiggly(space)_new cl lambda overline(t) s, mu cr$,
   )
 ))
 
@@ -467,7 +494,7 @@ $s in stmt, f in X, x in X, a in X$
     name: [ new reference ref value],
 
     // TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
-    // <- forbidden ??
+    // frbidden ??
 
     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
   )
@@ -552,15 +579,14 @@ $s in stmt, f in X, x in X, a in X$
 
 === Value Combination
 
+#let combine = `combine`
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ combine same trivial values],
+    name: [ combine trivial $0$ values],
 
-    $v_1 in {0, \#, bot}$,
-    $v_2 in {0, \#, bot}$,
-    $v_1 = v_2$,
-    $v_1 plus.o v_2 = v_1$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
   )
 ))
 
@@ -569,12 +595,23 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ combine different trivial values],
+    name: [ combine trivial $bot$ values],
+
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl bot \, bot cr)_combine cl bot, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine other trivial values],
 
     $v_1 in {0, \#, bot}$,
     $v_2 in {0, \#, bot}$,
     $v_1 != v_2$,
-    $v_1 plus.o v_2 = \#$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
   )
 ))
 
@@ -585,11 +622,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ combine lambda values],
 
-    // TODO: FIXME: how to combine statments in the right way? should check both
-    [*TODO: combining semantics for lambda values (sets?)*],
-    $overline(x_1) = overline(x_2)$,
-    $s_1 = s_2$,
-    $lambda space overline(x_1) space s_2 plus.o lambda space overline(x_2) space s_2 = lambda$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
   )
 ))
 
@@ -607,7 +640,7 @@ $s in stmt, f in X, x in X, a in X$
 
     // NOTE: version to use with "combine all"
     $l_1 = l_2$,
-    $rf l_1 plus.o rf l_2 = rf l_1$
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu cr$
   )
 ))
 
@@ -618,23 +651,28 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ combine tuple values],
 
-    $v^1_1 plus.o v^2_1 = v'_1$,
+    $cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
     $...$,
-    $v^1_n plus.o v^2_n = v'_n$,
-    $[v^1_1, ... v^1_n] plus.o [v^2_1 ... v^2_n] = [v'_1, ... v'_n]$
+    $cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
+    $cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl [v^1_1, ... v^1_n] \, [v^2_1 ... v^2_n] cr)_combine cl [v'_1, ... v'_n], mu'_n cr$
   )
 ))
 
-#let dom = `dom`
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ combine memory],
+    name: [ combine tuple values],
 
-    $dom mu_1 = dom mu_2$,
+    $mu'_0 = []$,
+    // NOTE: same labels required
+    $mu_1 = {l_1 -> v^1_1, ... l_n -> v^1_n}$,
+    $mu_2 = {l_1 -> v^2_1, ... l_n -> v^2_n}$,
 
-    $mu_1 plus.o mu_2 = l -> mu_1[l] plus.o mu_2[l]$
+    $cl mu_1, mu_2, mu'_0 cr xarrowSquiggly(cl v^1_1 \, v^2_1 cr)_combine cl v'_1, mu'_1 cr$,
+    $...$,
+    $cl mu_1, mu_2, mu'_(n - 1) cr xarrowSquiggly(cl v^1_n \, v^2_n cr)_combine cl v'_n, mu'_n cr$,
+
+    $cl mu_1, mu_2 cr xarrowSquiggly(space)_#[combine all] mu'_n cr$
   )
 ))
 
@@ -715,8 +753,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ lambda step],
 
-    $overline(t) = overline(t')$,
-    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t') \, m \, c)_spoil cl lambda, mu cr$,
+    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
   )
 ))
 
@@ -741,10 +778,10 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ tuple step],
 
-    $cl v_1, mu_0 cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu_1 cr$,
+    $cl v_1, mu cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu cr$,
     $...$,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu_n cr$,
-    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu_n cr$,
+    $cl v_n, mu cr xarrowSquiggly(t_n \, t'_n \, m \, c)_spoil cl v'_n, mu cr$,
+    $cl [v_1, ... v_n], mu cr xarrowSquiggly([t_1, ... t_n] \, [t'_1, ... t'_n] \, m \, c)_spoil cl [v'_1, ... v'_n], mu' cr$,
   )
 ))
 
@@ -883,9 +920,8 @@ $s in stmt, f in X, x in X, a in X$
 
     $vals, mu tval p eqmu v$,
     $types ttype p : t'$,
-    // TODO: check type compatibility for t and type for path p (?)
-    // [*TODO: check t ~ t' in sme way (?)*],
-    // <- programs considired to be well-typed
+    // TODO: FIXME: check type compatibility for t and type for path p (?)
+    [*TODO: check t ~ t' in sme way (?)*],
     $cl v', mu cr xarrowSquiggly(t)_new cl v, mu' cr$,
 
 
@@ -1011,7 +1047,7 @@ $s in stmt, f in X, x in X, a in X$
 
     $types_s = types_t$,
     $vals_s = vals_t$,
-    $mu_s plus.o mu_t = mu'$,
+    $cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
 
     // TODO changes ?? two ways ??
     $cl types, vals, mu cr