diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 1221071..0968b8b 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -9,7 +9,7 @@
 
 #h(10pt)
 
-// TODO: check correctness for path, mem & type ??
+// TODO: check correctnes for path, mem & type ??
 
 == Syntax
 
@@ -36,7 +36,6 @@
 #let Ref = `Ref`
 #let MaybeWrite = [$diamond$ `Write`]
 #let AlwaysWrite = [$square$ `Write`]
-#let NotWrite = [$not$ `Write`]
 #let Read = `Read`
 #let In = `In`
 #let Out = `Out`
@@ -112,15 +111,14 @@
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      // TODO: FIXME: decide what is the result of ref expr eval
-      // Or[$rf expr$][reference expr] // `Ref`
+      Or[$rf expr$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
     }
   ),
   Prod(
     `stmt`,
     {
-      Or[`CALL` $path expr+$][call function]
+      Or[`CALL` $path space expr+$][call function]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
       Or[$stmt ; stmt$][control flow operator, xecution ]
@@ -155,7 +153,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 overline(x) space stmt$][function pointer value] // `Fun`
+      Or[$lambda$][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 +164,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 overline(x) space stmt$][function pointer value] // `Fun`
+      Or[$lambda$][function pointer value] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
@@ -206,12 +204,17 @@ $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$
@@ -243,7 +246,18 @@ $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(
@@ -349,8 +363,70 @@ $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`
@@ -375,8 +451,6 @@ $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
@@ -455,27 +529,36 @@ $ 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 trivial read value],
+    name: [ new $0$ value],
 
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl v, mu cr$,
+    // TODO: check that access is what required ??
+    $cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
   )
 ))
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new trivial $not$ read value],
+    name: [ new $\#$ value],
 
-    $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl Read \, w cr)_new cl bot, mu cr$,
+    // 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$,
   )
 ))
 
@@ -528,190 +611,40 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Value Update
 
-#let modify = `modify`
+#let write = `write`
 
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ modify trivial value],
+*TODO: write to value*
 
-//     $v in {0, \#, bot}$,
-//     $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
-//   )
-// ))
+=== Call Finalization
+
+// FIXME: make connected to syntax
+*TODO*
 
-// TODO: add type check ??
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ modify end value],
-
-    // $v in {0, \#, bot}$,
-    $cl v, mu cr xarrowSquiggly(cl \@ x \, b cr)_modify cl b, mu cr$,
+    name: [ spoil init],
+    $mu stretch(=>)^nothing_(cl sigma, mu cr) mu$,
   )
 ))
 
 #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],
 
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+    $mu stretch(=>)^args_sigma gamma$,
 
-    $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$,
+    $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]$
   )
 ))
 
@@ -722,11 +655,15 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ fix step],
 
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+    $mu stretch(=>)^args_sigma gamma$,
 
-    $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$,
+    $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]$
   )
 ))
 
@@ -737,12 +674,49 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ skip step],
 
-    $ tcorrectnew cl v, r, w, r', w', m, c cr $,
+    $mu stretch(=>)^args_sigma gamma$,
 
     $not "spoil step"$,
     $not "fix step"$,
-    $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$,
+
+    $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$,
   )
 ))
 
@@ -751,184 +725,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ lambda step],
+    name: [decl body],
 
-    $cl lambda, mu cr xarrowSquiggly(lambda overline(t) \, lambda overline(t) \, m \, c)_spoil cl lambda, mu cr$,
-  )
-))
+    $cl sigma, mu, l cr
+     attach(stretch(->)^overline(s), tr: *)
+     cl sigma', mu', l' cr$,
 
-#h(10pt)
+    $d = overline(s)$,
 
-#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$,
+    $cl sigma, mu, l cr
+     xarrowDashed(d space @)
+     cl sigma', mu', l' cr$,
   )
 ))
 
@@ -936,42 +743,23 @@ $ 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 [p_1, ... p_n]$],
+    name: [ CALL $f space overline(p)$],
 
-    $vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
-    $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
+    $cl [], mu, l cr
+     xarrowDashed(f space @ space overline(p))
+     cl sigma', mu', l' cr$,
 
-    // TODO: add args before statement eval
+    // TODO: FIXME define args in some way
+    $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
 
-    $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$,
+    $cl sigma, mu, l cr
+     xarrow("CALL" f space overline(p))
+     cl sigma, gamma, l cr$,
   )
 ))
 
@@ -982,7 +770,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ READ $p$],
 
-    $mu, types, vals tval p eqmu 0$,
+    $mu, types, vals teval p eqmu 0$,
 
     $cl types, vals, mu cr
      xarrow("READ" p)
@@ -995,17 +783,16 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ WRITE $p$],
+    name: [ WRITE $x$],
 
     $types ttype p : cl r, w cr$,
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
-    $l = vals(x)$,
-    $mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
+    $mu[x] xarrowSquiggly(p)_write v$,
 
     $cl types, vals, mu cr
      xarrow("WRITE" p)
-     cl types, vals, mu[l <- v'] cr$,
+     cl types, vals, mu[x <- v] cr$,
   )
 ))
 
@@ -1032,6 +819,9 @@ $ 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(
@@ -1047,7 +837,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
     $types_s = types_t$,
     $vals_s = vals_t$,
-    $cl mu_s, mu_t cr xarrowSquiggly(space)_#[combine all] mu'$,
+    $mu' = combine(mu_s, mu_t)$,
 
     // TODO changes ?? two ways ??
     $cl types, vals, mu cr
@@ -1056,4 +846,20 @@ $ 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 ??
+
 ]