diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 0968b8b..1221071 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -9,7 +9,7 @@
 
 #h(10pt)
 
-// TODO: check correctnes for path, mem & type ??
+// TODO: check correctness for path, mem & type ??
 
 == Syntax
 
@@ -36,6 +36,7 @@
 #let Ref = `Ref`
 #let MaybeWrite = [$diamond$ `Write`]
 #let AlwaysWrite = [$square$ `Write`]
+#let NotWrite = [$not$ `Write`]
 #let Read = `Read`
 #let In = `In`
 #let Out = `Out`
@@ -111,14 +112,15 @@
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      Or[$rf expr$][reference expr] // `Ref`
+      // TODO: FIXME: decide what is the result of ref expr eval
+      // Or[$rf expr$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
     }
   ),
   Prod(
     `stmt`,
     {
-      Or[`CALL` $path space expr+$][call function]
+      Or[`CALL` $path expr+$][call function]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
       Or[$stmt ; stmt$][control flow operator, xecution ]
@@ -153,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$][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`
     }
@@ -164,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$][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`
     }
@@ -204,17 +206,12 @@ $v in value$ - произвольное значение
 
 == Semantics
 
+// TODO: FIXME: add vars & funcs from global context in the beginnning
+
 // $V := memelem$ - значения памяти
 
 $X$ - можество переменных
 
-// FIXME: TMP
-#let valuemem = `valuemem`
-#let memelem = `memelem`
-#let pathenvmode = `pathenvmode`
-#let pathenvval = `pathenvval`
-#let pathenvmem = `pathenvmem`
-#let pathenvtype = `pathenvtype`
 
 #let vals = $Sigma$
 #let types = $Gamma$
@@ -246,18 +243,7 @@ $s in stmt, f in X, x in X, a in X$
 #let tmode = $attach(tack.r, br: mode)$
 
 #let val = `val`
-#let label = `label`
 #let tval = $attach(tack.r, br: val)$
-#let tlabel = $attach(tack.r, br: label)$
-
-// TODO: TMP, deprecated
-// #let tetype = $attach(tack.r.double, br: type)$
-// #let temode = $attach(tack.r.double, br: mode)$
-// #let telabel = $attach(tack.r.double, br: label)$
-
-#let teval = $attach(tack.r.double, br: val)$
-
-// TODO: env mem label ??, env mem value ??
 
 - #[ Конструирование путей по переменой
 #align(center, prooftree(
@@ -363,70 +349,8 @@ $s in stmt, f in X, x in X, a in X$
 ))
 ]
 
-// TODO: FIXME: not required (trivial) ??
-// - #[ Получение метки поля
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ access],
-
-//     $vals, mu tval p eqmu rf l$,
-//     $vals, mu tmode p arrmu l$,
-//   )
-// ))
-// ]
-
-// TODO: not required (trivial) ??
-// - #[ Получение read-write тега поля по окружению
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ access],
-
-//     $x : types[x] tmode p -> cr r space w cl$,
-//     $sigma temode p -> cr r space w cl$,
-//   )
-// ))
-// ]
-
-- #[ Получение значения поля по окружению
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ access],
-
-    $x eqmu vals[x] tval p eqmu v$,
-    $types, vals, mu teval p eqmu x$,
-  )
-))
-]
-
-// FIXME: move to new mode model
-// === Mode Correctness
-
-// Функции проверки тегов, имеют тип $mode -> #[bool]$:
-
-// #let modevar = $(r space w space c space i space o)$
-
-// $ isRead modevar = r == "Read" $
-// $ isAlwaysWrite modevar = w == square "Write" $
-// $ isPossibleWrite modevar = w == diamond "Write" || w == square "Write" $
-// $ isRef modevar = c == "Ref" $
-// $ isCopy modevar = c == "Copy" $
-// $ isIn modevar = i == "In" $
-// $ isOut modevar = o == "Out" $
-
-// Требования к тегам:
-
-// $ isOut mode -> isAlwaysWrite mode $
-// $ isRead mode -> isIn mode $
-
-// TODO: rest conditions ??
-
 === Eval Rules
 
-#let args = `args`
-
 #[
 
 #let ref = `ref`
@@ -451,6 +375,8 @@ $s in stmt, f in X, x in X, a in X$
 
 === Moded Type Correctness
 
+*NOTE: скорее всего не нужна в таком виде, перенесено в spoil*
+
 #let tcorrect = $attach(tack.r, br: #[correct])$
 
 // TODO: FIXME: well formatness for mode, extract
@@ -529,36 +455,27 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Value Construction
 
-// TODO: FIXME:add ref / copy modes correctness check
+// TODO: FIXME:add ref / copy modes correctness check ??
 
 #let new = `new`
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new $0$ value],
+    name: [ new trivial read value],
 
-    // TODO: check that access is what required ??
-    $cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$,
   )
 ))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new $\#$ value],
+    name: [ new trivial $not$ read value],
 
-    // TODO: check that access is what required ??
-    $cl \#, mu cr xarrowSquiggly(cl r\, w cr)_new cl \#, mu cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new $bot$ value],
-
-    $cl bot, mu cr xarrowSquiggly(cl r\, w cr)_new cl bot, mu cr$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl bot, mu cr$,
   )
 ))
 
@@ -611,40 +528,190 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Value Update
 
-#let write = `write`
+#let modify = `modify`
 
-*TODO: write to value*
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ modify trivial value],
 
-=== Call Finalization
-
-// FIXME: make connected to syntax
-*TODO*
+//     $v in {0, \#, bot}$,
+//     $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
+//   )
+// ))
 
+// TODO: add type check ??
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ spoil init],
-    $mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
+    name: [ modify end value],
+
+    // $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
   )
 ))
 
 #h(10pt)
 
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ new reference copy value],
+
+    $cl mu[l], mu cr xarrowSquiggly(cl p \, b cr)_modify cl v', mu' cr$,
+    $cl rf l, mu cr xarrowSquiggly(cl *p \, b cr)_modify cl rf l, mu'[l <- v'] cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ modify tuple value],
+
+    $cl v_i, mu cr xarrowSquiggly(cl p \, b cr)_modify cl v'_i, mu', cr$,
+    $cl [v_1, ... v_i, ... v_n], mu cr xarrowSquiggly(cl p.i \, b cr)_modify cl [v_1, ... v'_i, ... v_n], mu' cr$,
+  )
+))
+
+#h(10pt)
+
+=== Value Combination
+
+#let combine = `combine`
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine trivial $0$ values],
+
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl 0 \, 0 cr)_combine cl 0, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    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$,
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl v_1 \, v_2 cr)_combine cl \#, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine lambda values],
+
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl lambda \, lambda cr)_combine cl lambda, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine reference values (inplace)],
+
+    // NOTE: standalome version
+    // $cl mu_1, mu_2, mu cr xarrowSquiggly(cl mu_1[l_1] \, mu_2[l_2] cr)_combine cl v', mu' cr$,
+    // $mu' xarrowSquiggly(v')_#[add] cl rf l', mu'' cr$,
+    // $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l', mu'' cr$
+
+    // NOTE: version to use with "combine all"
+    $l_1 = l_2$,
+    $cl mu_1, mu_2, mu cr xarrowSquiggly(cl rf l_1 \, rf l_2 cr)_combine cl rf l_1, mu cr$
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine tuple values],
+
+    $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, 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$
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ combine tuple values],
+
+    $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}$,
+
+    $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$
+  )
+))
+
+#h(10pt)
+
+=== Call Values Spoil
+
+#let spoil = `spoil`
+
+// TODO: FIXME: complete rule check
+#let tcorrectnew = $attach(tack.r.double, br: #[correct])$
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ correctness],
+
+    $r = Read => v = 0$,
+    $r = Read => m = (In, \_)$, 
+    $m = (\_, Out) => w = AlwaysWrite$,
+    $(w = AlwaysWrite or w = MaybeWrite) and (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
+
+    $v in {0, \#, bot}$,
+
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+  )
+))
+
+// TODO: extract correctness
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ spoil step],
 
-    $mu stretch(=>)^args_sigma gamma$,
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
 
-    $isPossibleWrite mode$, // NOTE: weak requirement: may write
-    $not isCopy mode$,
-    $mode = (\_, not Out)$,
-
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
-
-    // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- bot]$
+    $w = AlwaysWrite or w = MaybeWrite$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, not Copy)_spoil cl bot, mu cr$,
   )
 ))
 
@@ -655,15 +722,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ fix step],
 
-    $mu stretch(=>)^args_sigma gamma$,
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
 
-    $isAlwaysWrite mode$, // NOTE: strong requirement: should write
-    $mode = (\_, not Out)$,
-
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
-
-    // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- 0]$
+    $w = AlwaysWrite$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \,  (\_, Out) \, c)_spoil cl 0, mu cr$,
   )
 ))
 
@@ -674,49 +737,12 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ skip step],
 
-    $mu stretch(=>)^args_sigma gamma$,
+    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
 
     $not "spoil step"$,
     $not "fix step"$,
-
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
-
-    // mu
-    $gamma stretch(=>)^((mode, x) : args)_sigma gamma$
-  )
-))
-
-
-#h(10pt)
-
-=== Function Evaluation
-
-// FIXME: make connected to syntax
-*TODO*
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ $(lambda a : t. d) m$],
-
-    // TODO: verify that type of m is t ??
-
-    $cl sigma [a <- (m, t)], mu, l cr
-     xarrowSquiggly(t)
-     cl sigma', mu', l' cr$,
-
-    $cl sigma', mu', l' cr
-     xarrowDashed(d space @ space overline(y))
-     cl sigma'', mu'', l'' cr$,
-
-    $isRead mode$,
-    $not isCopy mode$,
-
-    // NOTE: correctness checked in CALL f
-
-    $cl sigma, mu, l cr
-     xarrowDashed((lambda a. d) space @ space x space overline(y))
-     cl sigma'', mu'', l'' cr$,
+    $v in {0, \#, bot}$,
+    $cl v, mu cr xarrowSquiggly(cl r \, w cr \, cl r' \, w' cr \, (\_, not Out) \, c)_spoil cl v, mu cr$,
   )
 ))
 
@@ -725,17 +751,184 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [decl body],
+    name: [ lambda step],
 
-    $cl sigma, mu, l cr
-     attach(stretch(->)^overline(s), tr: *)
-     cl sigma', mu', l' cr$,
+    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
+  )
+))
 
-    $d = overline(s)$,
+#h(10pt)
 
-    $cl sigma, mu, l cr
-     xarrowDashed(d space @)
-     cl sigma', mu', l' cr$,
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ reference step],
+
+    $cl mu[l], mu cr xarrowSquiggly(t \, t' m \, c')_spoil cl v', mu' cr$,
+    // NOTE: copy mode of assigned type is not important (c'')
+    $cl rf l, mu cr xarrowSquiggly(rf c' space  t \, rf c'' space  t' \, m \, c)_spoil cl rf l, mu'[l <- v'] cr$,
+  )
+))
+
+#h(10pt)
+
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ tuple step],
+
+    $cl v_1, mu cr xarrowSquiggly(t_1 \, t'_1 \, m \, c)_spoil cl v'_1, mu 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$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ full spoil],
+
+    $p arrpath x$,
+    $l = vals[x]$,
+    $vals, mu tval p eqmu b$,
+    $types ttype p : t'$,
+    // TODO: FIXME: Ref or Copy ?? in root <- Ref ??, because otherwise there could not b any Refs
+    // FIXME depends on parent ??
+    $cl b, mu cr xarrowSquiggly(t \, t' \, m \, Ref)_spoil cl b', mu' cr$,
+    $cl mu[l], mu cr xarrowSquiggly(cl p \, b' cr)_modify cl v', mu' cr$,
+
+    $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu'[l <- v']$,
+  )
+))
+
+#h(10pt)
+
+=== Expression Evaluation
+
+// TODO: check
+
+#let eval = `eval`
+#let texpre = $attach(tack.r.double, br: eval)$
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ path type],
+
+    $vals, mu tval p eqmu v$,
+    $vals, mu texpre p eqmu v$,
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $vals, mu texpre () eqmu 0$,
+  )
+))
+
+// NOTE: tmp removed
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ unit value type],
+
+//     $vals, mu texpre e : t$,
+
+//     [*TODO*],
+
+//     // TODO: reference to what ??
+//     $vals, mu texpre rf e eqmu rf ??$,
+//   )
+// ))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $vals, mu texpre e_1 eqmu v_1$,
+    $...$,
+    $vals, mu texpre e_n eqmu v_n$,
+    $vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
+  )
+))
+
+
+=== Expresion Typing
+
+// TODO: check
+
+#let texprt = $attach(tack.r.double, br: type)$
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ path type],
+
+    $types ttype p : t$,
+    $types texprt p : t$,
+  )
+))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $types texprt () : cl Read, NotWrite cr$,
+  )
+))
+
+// NOTE: tmp removed
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ unit value type],
+
+//     $types texprt e : t$,
+//     // TODO: why Ref mode ?? <- due to immutability ??
+//     $types texprt rf e : rf Ref t$,
+//   )
+// ))
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ unit value type],
+
+    $types texprt e_1 : t_1$,
+    $...$,
+    $types texprt e_n : t_n$,
+    $types texprt [e_1, ... e_n] : [t_1, ... t_n]$,
+  )
+))
+
+=== Function Argument Addition
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ add argument],
+
+
+    $vals, mu tval p eqmu v$,
+    $types ttype p : t'$,
+    // 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$,
+
+
+    // TODO save type mode somewhere ?? // <- not needed because is described by other params <- ??
+    $cl types, vals, mu cr
+     xarrowDashed(x space t space p)
+     cl types[x <- t], vals[x <- v], mu' cr$,
   )
 ))
 
@@ -743,23 +936,42 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Statement Evaluation
 
-// FIXME: make connected to syntax
-*TODO: check type of lambda?, args from type?*
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ CALL $f space overline(p)$],
+    name: [ CALL $f space [p_1, ... p_n]$],
 
-    $cl [], mu, l cr
-     xarrowDashed(f space @ space overline(p))
-     cl sigma', mu', l' cr$,
+    $vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
+    $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
-    // TODO: FIXME define args in some way
-    $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
+    // TODO: add args before statement eval
 
-    $cl sigma, mu, l cr
-     xarrow("CALL" f space overline(p))
-     cl sigma, gamma, l cr$,
+    $types_0 = []$,
+    $vals_0 = []$,
+    $mu_0 = mu$,
+
+    // NOTE: dashed arrow to fill context
+    $cl types_0, vals_0,  mu_0, l cr
+     xarrowDashed(x_1 space t_1 space p_1)
+     cl types', vals_1, mu_1, l' cr$,
+    $...$,
+    $cl types_(n - 1), vals_(n - 1),  mu_(n - 1), l cr
+     xarrowDashed(x_n space t_n space p_n)
+     cl types', vals_n, mu_n, l' cr$,
+
+    $cl types_n, vals_n,  mu_n, l cr
+     xarrow(s)
+     cl types', vals', mu', l' cr$,
+
+    // NOTE: thick arrow to "spoil" context
+    $gamma_0 = mu$,
+    $gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$,
+    $...$,
+    $gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$,
+
+    $cl vals, types, mu, l cr
+     xarrow("CALL" f space [p_1, ... p_n])
+     cl vals, types, gamma_n, l cr$,
   )
 ))
 
@@ -770,7 +982,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ READ $p$],
 
-    $mu, types, vals teval p eqmu 0$,
+    $mu, types, vals tval p eqmu 0$,
 
     $cl types, vals, mu cr
      xarrow("READ" p)
@@ -783,16 +995,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ WRITE $x$],
+    name: [ WRITE $p$],
 
     $types ttype p : cl r, w cr$,
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
-    $mu[x] xarrowSquiggly(p)_write v$,
+    $l = vals(x)$,
+    $mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)
-     cl types, vals, mu[x <- v] cr$,
+     cl types, vals, mu[l <- v'] cr$,
   )
 ))
 
@@ -819,9 +1032,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 #h(10pt)
 
-#let combine = `combine`
-
-*TODO: combine replacement* // FIXME
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -837,7 +1047,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
     $types_s = types_t$,
     $vals_s = vals_t$,
-    $mu' = combine(mu_s, mu_t)$,
+    $cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
 
     // TODO changes ?? two ways ??
     $cl types, vals, mu cr
@@ -846,20 +1056,4 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   )
 ))
 
-#h(10pt)
-
-=== Combination
-
-*TODO: rewrite as rules, fix* // FIXME
-
-$ combine(mu_1, mu_2)[i] = combine_e (mu_1[i], mu_2[i]) $
-$ combine_e (bot, bot) = bot $
-$ combine_e (0, 0) = 0 $
-$ combine_e (\_, \_) = \# $
-// FIXME: ref to combined memory
-$ combine_e (rf c l_1, rf c' l_2) | c == c' = rf c combine_e(mu_1[l_1], mu_2[l_2])$
-$ combine_e (v^1_1, ... v^1_n, v^2_1 ... v^2_n) = [combine_e(v^1_1, v^2_1), ..., combine_e(v^1_n, v^2_n)]$
-$ combine_e (lambda space overline(t_1) space s_1, lambda space overline(t_2) space s_2) | overline(t_1) == overline(t_2)  = lambda space overline(t_1) space s_1 $
-// TODO: FIXME: statemient in lambda is not important ??
-
 ]