diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 5fff471..a3936de 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -15,8 +15,6 @@
 
 #h(10pt)
 
-#let rf = $\& #h(3pt)$
-
 #let isCorrect = `isCorrect`
 
 #let isRead = `isRead`
@@ -27,28 +25,13 @@
 #let isIn = `isIn`
 #let isOut = `isOut`
 
-#let readTag = `read`
-#let writeTag = `write`
-#let copyTag = `copy`
-#let inTag = `in`
-#let outTag = `out`
 #let mode = `mode`
-
-#let Copy = `Copy`
-#let Ref = `Ref`
-#let MaybeWrite = [$diamond$ `Write`]
-#let AlwaysWrite = [$square$ `Write`]
-#let Read = `Read`
-#let In = `In`
-#let Out = `Out`
-
 #let expr = `expr`
 #let stmt = `stmt`
 #let decl = `decl`
 #let prog = `prog`
 #let path = `path`
 #let type = `type`
-#let modedType = `modedtype`
 #bnf(
   Prod(`read`,
     // NOTE: not three modalities for write, because read does not change value
@@ -71,7 +54,7 @@
   Prod(
     `mode`,
     {
-      Or[$inTag space outTag$][]
+      Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
     }
   ),
   Prod(
@@ -88,36 +71,33 @@
   Prod(
     `type`,
     {
-      Or[$readTag writeTag ()$][simple type representing all primitive types] // `Unit`
-      Or[$rf copyTag space type$][reference to structure, contains copy / ref choice] // `Ref`
+      Or[$()$][simple type representing all primitive types] // `Unit`
+      Or[\& #h(3pt) `mode` #h(3pt) `type`][reference to structure, contains copy / ref choice] // `Ref`
       Or[$[type+]$][tuple type] // `Prod`
       // Or[`type` $times$ `type`][pair type, allows to make tuples] // `Prod`
       // Or[`type` $+$ `type`][union type (important in some way ???)] // `Sum` // TODO ?
 
       // NOTE: do not use names in type
       // Or[$lambda_((x type)+)$][type of lambda or function pointer, defined by function declaration] // `Fun`
-      Or[$lambda (modedType)+$][type of lambda or function pointer, defined by function declaration] // `Fun`
-    }
-  ),
-  Prod(
-    `modedtype`,
-    {
-      Or[$mode type$][type woth in and out modifiers]
+      Or[$lambda type+$][type of lambda or function pointer, defined by function declaration] // `Fun`
     }
   ),
+  // FIXME: replace with expr
   Prod(
     `expr`,
     {
       Or[$()$][value of simple type] // `Unit`
       Or[$path$][value from variable] // `Path`
-      Or[$rf expr$][reference expr] // `Ref`
+      Or[$\& #h(3pt) expr$][reference expr] // `Ref`
       Or[$[expr+]$][tuple expr] // `Prod`
+      // NOTE: replaced with simple path value
+      // Or[$lambda_path$][function value from variable] // `Fun`
     }
   ),
   Prod(
     `stmt`,
     {
-      Or[`CALL` $path space expr+$][call function]
+      Or[`CALL` $f space expr+$][call function]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
       Or[$stmt ; stmt$][control flow operator, xecution ]
@@ -129,7 +109,7 @@
     {
       // TODO: path not allowed ??
       Or[$"var" X : type = expr$][global variable declaration]
-      Or[$"fun" X ((X : modedType)+) = stmt$][function declaration]
+      Or[$"fun" X ((X : type)+) = stmt$][function declaration]
     }
   ),
   Prod(
@@ -142,19 +122,21 @@
 
 == Value Model
 
-#let deepValue = `deepvalue`
-#let value = `value`
+#let rf = $\& #h(3pt)$
 
+// FIXME: check & add details
+#let deepvalue = `deepvalue`
+#let value = `value`
 #bnf(
   Prod(
-    $deepValue$,
+    $deepvalue$,
     {
       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 type+ stmt$][function pointer value] // `Fun`
-      Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
-      Or[$[deepValue+]$][tuple value] // `Prod`
+      Or[$rf deepvalue$][reference value, contains label of the value in the memory] // `Ref`
+      Or[$[deepvalue+]$][tuple value] // `Prod`
     }
   ),
   Prod(
@@ -164,23 +146,22 @@
       Or[$\#$][valid or spoiled value of simple type] // `Unit`
       Or[$bot$][spoiled value of simple type] // `Unit`
       Or[$lambda type+ stmt$][function pointer value] // `Fun`
-      // FIXME: embed mode into value for simplification ??
-      Or[$rf copyTag LL$][reference value, contains label of the value in the memory] // `Ref`
+      Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
   ),
 )
 
-#deepValue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
+#deepvalue - полное значение, #value - слой значения, привязан к конкретной памяти $mu$
 
 Значения, могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
 
 $v in value$ - произвольное значение
 
-Получение #deepValue по #value:
-- $rf c l xarrowSquiggly(mu)_#[deep] rf c mu[l]$
+Получение #value по #deepvalue:
+- $rf LL xarrowSquiggly(mu)_#[deep] rf mu[LL]$
 - $* xarrowSquiggly(mu)_#[deep] *$
-где $*$ - произвольный конструктор значения, кроме $rf$
+где $*$ - произвольный конструктор значения кроме $rf$
 
 == Memory Model
 
@@ -192,16 +173,17 @@ $v in value$ - произвольное значение
 - $LL$ - множество меток памяти
 - $mem := LL -> value, space mu : mem$ - память, частично определённая функция
 - $l in LL$ - новый тег памяти (ранее не использованный)
-- `next` - получение следующей неиспользованной метки в памяти
+- `next` - получение следующей неиспользованной метки
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ add value to memory],
 
-    $l = #[next] (mu)$,
+    $l' = #[next] (l)$,
 
-    $cl mu cr xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
+    // TODO: check that access is what required ??
+    $cl mu, l cr xarrowSquiggly(v)_#[add] cl mu [l <- v], l' cr$,
   )
 ))
 
@@ -278,7 +260,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple access path],
+    name: [ access path],
 
     $x tpath p$,
 
@@ -291,7 +273,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ variable type access],
+    name: [ variable typing],
 
     $x : t_x ttype @x : t_x$,
   )
@@ -299,7 +281,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ reference type access],
+    name: [ reference typing],
 
     $x tpath p$,
     $x : t_x ttype p : rf mode t_p$,
@@ -309,7 +291,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple type access],
+    name: [ access typing],
 
     $x tpath p$,
     $x : t_x ttype p : [t_1, ... t_n]$,
@@ -318,34 +300,34 @@ $s in stmt, f in X, x in X, a in X$
 ))
 ]
 
-- #[ Получение read-write тега поля
+- #[ Получение тега поля
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ variable rw tag access],
+    name: [ variable typing],
 
-    $t_x = r w ()$,
-    $x : t_x tmode @x -> cr r w cl$,
+    $t_x = rf mode t$,
+    $x : t_x tmode @x -> mode$,
   )
 ))
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ reference rw tag access],
+    name: [ reference typing],
 
     $x tpath p$,
-    $x : t_x tmode p -> cr r w cl$,
-    $x : t_x tmode *p ->  cr r w cl$,
+    $x : t_x tmode p : rf mode t_p$,
+    $x : t_x tmode *p : t_p$,
   )
 ))
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple rw tag access],
+    name: [ access typing],
 
     $x tpath p$,
-    $x : t_x tmode p ->  cr r w cl$,
-    $x : t_x tmode p.i -> cr r w cl$,
+    $x : t_x tmode p : [t_1, ... t_n]$,
+    $x : t_x tmode p.i : t_i$,
   )
 ))
 ]
@@ -354,7 +336,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ variable value access],
+    name: [ variable typing],
 
     $x eqmu v_x tval @x eqmu v_x$,
   )
@@ -362,7 +344,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ reference value access],
+    name: [ reference typing],
 
     $x tpath p$,
     $x eqmu v_x tval p eqmu rf l$,
@@ -372,7 +354,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple value access],
+    name: [ access typing],
 
     $x tpath p$,
     $x eqmu v_x tmode p eqmu [v_1, ... v_n]$,
@@ -385,11 +367,11 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ access],
+    name: [ variable typing],
 
     $v_x = rf l$,
-    $x eqmu v_x tval p eqmu rf l$,
 
+    $x eqmu v_x tval p eqmu rf l$,
     $x eqmu v_x tmode p arrmu l$,
   )
 ))
@@ -399,7 +381,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ access],
+    name: [ access typing],
 
     $x tpath p$,
     $x : sigma[x].2 ttype p : t$,
@@ -408,15 +390,15 @@ $s in stmt, f in X, x in X, a in X$
 ))
 ]
 
-- #[ Получение read-write тега поля по окружению
+- #[ Получение тега поля по окружению
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ access],
+    name: [ access typing],
 
     $x tpath p$,
-    $x : sigma[x].2 tmode p -> cr r space w cl$,
-    $sigma temode p -> cr r space w cl$,
+    $x : sigma[x].2 tmode p -> mode$,
+    $sigma temode p -> mode$,
   )
 ))
 ]
@@ -425,7 +407,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ access],
+    name: [ access typing],
 
     $x tpath p$,
     $x eqmu sigma[x].1 tval p eqmu v$,
@@ -438,7 +420,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ access],
+    name: [ access typing],
 
     $x tpath p$,
     $x eqmu sigma[x].1 tlabel p arrmu l$,
@@ -447,37 +429,34 @@ $s in stmt, f in X, x in X, a in X$
 ))
 ]
 
-=== Mode Accessors
+=== Mode Correctness
 
-#let modevar = $(i space o)$
+Функции проверки тегов, имеют тип $mode -> #[bool]$:
 
-$ isIn modevar = i == In $
-$ isOut modevar = o == Out $
+#let modevar = $(r space w space c space i space o)$
 
-// FIXME: move to new mode model
-// === Mode Correctness
+$ 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" $
 
-// Функции проверки тегов, имеют тип $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 $
+$ isOut mode -> isAlwaysWrite mode $
+$ isRead mode -> isIn mode $
 
 // TODO: rest conditions ??
 
 === Eval Rules
 
+// FIXME: make connected to syntax
+*TODO*
+
+#h(10pt)
+
 #let args = `args`
 
 #[
@@ -502,170 +481,124 @@ $ isOut modevar = o == Out $
 
 // TODO: introduce spep env argument ??
 
-=== Moded Type Correctness
+#h(10pt)
 
-#let tcorrect = $attach(tack.r, br: #[correct])$
+=== Correctness
 
 // TODO: FIXME: well formatness for mode, extract
 // TODO: FIXME: check for mode, is recursion required ??
 // TODO: FIXME: check mode & access corectness in os correct
 
-$ sigma in env, 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: check all requirements
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit assignment tags correctness],
+    name: [ is correct],
+    $isOut mode -> isAlwaysWrite mode$, // NOTE; strong requirment should write
+    $isRead mode -> isIn mode$,
+    $isPossibleWrite mode and (isOut mode or not isCopy mode) -> isAlwaysWrite pathenvmode(sigma, x)$, // NOTE: may mode => should sigma(x)
+    $isRead mode -> pathenvval(mu, sigma, x) != bot and pathenvval(mu, sigma, x) != X$,
 
-    $r = Read => isIn m$, 
-    $isOut m => w = AlwaysWrite$,
-    // $sigma temode x -> cr r' space w' cl$, // NOTE: not required, value passed
-    $(w = AlwaysWrite or w = MaybeWrite) and (isOut m or c = Ref) => w' = AlwaysWrite$,
-
-    // $sigma, mu teval x eqmu v$, // NOTE: not required, value passed
-    $v in {0, \#, bot}$,
-    $r = Read => v = 0$,
-
-    $sigma, mu, m, c tcorrect v : r' space w' () -> r space w ()$,
+    $isCorrect_(cl sigma, mu cr) (mode, x)$,
   )
 ))
 
 #h(10pt)
 
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ ref assignment tags correctness],
+=== Call Initialization
 
-    $sigma, mu, m, c_r tcorrect v : t -> t'$,
+Отсутствующий нижний индекс ($ref$, $copy$) означает произвольный индекс.
+Считается, что выбранный индекс одинаков в рамках одного правила.
 
-    // TODO: FIXME: which tag translations are correct ?? <- only assignee?
-    $sigma, mu, m, c tcorrect rf c_r space v : rf c' space t -> rf c_r space t'$,
-  )
-))
+// NOTE: no empty type
+// #align(center, prooftree(
+//   vertical-spacing: 4pt,
+//   rule(
+//     name: [ add paths init],
 
-#h(10pt)
+//     $cl sigma, mu, l cr stretch(~>)^nothing cl sigma, mu, l cr$,
+//   )
+// ))
+
+// #h(10pt)
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ tuple assignmenttags correctness],
-
-    $sigma, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
-
-    $...$,
-
-    $sigma, mu, m, c tcorrect v_n : t_n -> t'_n$,
-
-    $sigma, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, t'_n]$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ function pointer tags correctness],
-
-    $sigma, mu, m, c tcorrect lambda space overline(t) space s : lambda space overline(t) -> lambda space overline(t)$,
-  )
-))
-
-#h(10pt)
-
-=== Value Construction
-
-#let new = `new`
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new $0$ value],
+    name: [ add paths field by copy],
 
     // TODO: check that access is what required ??
-    $cl 0, mu cr xarrowSquiggly(space)_new cl 0, mu cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl pathenvmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
   )
 ))
 
+#h(10pt)
+
+// NOTE: do nothing, ref init by default
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ add paths field by reference],
+
+    $cl sigma, mu, l cr xarrowSquiggly(p : ())_ref cl sigma, mu, l cr$,
+  )
+))
+
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new $\#$ value],
+    name: [ add paths ref],
+    $cl sigma, mu, l cr xarrowSquiggly(*p : t)_ref cl sigma', mu', l' cr$,
+    $isRef mode$,
 
-    // TODO: check that access is what required ??
-    $cl \#, mu cr xarrowSquiggly(space)_new cl \#, mu cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
   )
 ))
 
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new $bot$ value],
+    name: [ add paths ref],
+    $cl sigma, mu, l cr xarrowSquiggly(*p : t)_copy cl sigma, mu, l cr$,
+    $isCopy mode$,
 
-    $cl bot, mu cr xarrowSquiggly(space)_new cl bot, mu cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
   )
 ))
 
+#h(10pt)
+
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ new funciton pointer value],
-
-    $cl lambda overline(t) s, mu cr xarrowSquiggly(space)_new cl lambda overline(t) s, mu cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new reference ref value],
-
-    $cl rf Ref l, mu cr xarrowSquiggly(space)_new cl rf Ref l, mu cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new reference copy value],
-
-    $cl mu[l], mu cr xarrowSquiggly(space)_new cl v, mu_v cr$,
-
-    $cl mu_v cr xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
-
-    $cl rf Copy l, mu cr xarrowSquiggly(space)_new cl rf Copy l', mu_a cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new tuple value],
-
-    $cl v_1, mu_0 cr xarrowSquiggly(space)_new cl lambda v'_1, mu_1 cr$,
+    name: [ add paths tuple],
+    $cl sigma, mu, l cr xarrowSquiggly(p.1 : t_1) cl sigma_1, mu_1, l_1 cr$,
     $...$,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(space)_new cl lambda v'_n, mu_n cr$,
+    $cl sigma_(n - 1), mu_(n - 1), l_(n - 1) cr xarrowSquiggly(p.n : t_n) cl sigma_n, mu_n, l_n cr$,
 
-    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly(space)_new cl [v'_1, ... v'_n], mu_n cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : [t_1, ... t_n]) cl sigma_n, mu_n, l_n cr$,
   )
 ))
 
-=== Value Update
+#h(10pt)
 
-#let write = `write`
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ add paths funciton pointer],
 
-*TODO: write to value*
+    $cl sigma, mu, l cr xarrowSquiggly(F_x) cl sigma, mu, l cr$,
+  )
+))
+
+#h(10pt)
 
 === Call Finalization
 
-// FIXME: make connected to syntax
-*TODO*
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -737,9 +670,6 @@ $ sigma in env, space mu in mem, space m in mode,
 
 === Function Evaluation
 
-// FIXME: make connected to syntax
-*TODO*
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -789,22 +719,22 @@ $ sigma in env, 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 overline(x)$],
 
     $cl [], mu, l cr
-     xarrowDashed(f space @ space overline(p))
+     xarrowDashed(d space @ space overline(x))
      cl sigma', mu', l' cr$,
 
     // TODO: FIXME define args in some way
     $mu attach(stretch(=>)^args_sigma, tr: *) gamma$,
 
+    $DD(f) := d$,
+
     $cl sigma, mu, l cr
-     xarrow("CALL" f space overline(p))
+     xarrow("CALL" f space overline(x))
      cl sigma, gamma, l cr$,
   )
 ))
@@ -814,12 +744,32 @@ $ sigma in env, space mu in mem, space m in mode,
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ READ $p$],
+    name: [ CALL_LAM $y space overline(x)$],
 
-    $mu, sigma teval p eqmu 0$,
+    $pathenvtype(sigma, y) = F_f$,
 
     $cl sigma, mu, l cr
-     xarrow("READ" p)
+     xarrow("CALL" f space overline(x))
+     cl sigma, gamma, l cr$,
+
+    $cl sigma, mu, l cr
+     xarrow("CALL_LAM" y space overline(x))
+     cl sigma, gamma, l cr$,
+  )
+))
+
+#h(10pt)
+
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ READ $x$],
+
+    $pathenvval(mu, sigma, x) != bot$,
+    $pathenvval(mu, sigma, x) != X$,
+
+    $cl sigma, mu, l cr
+     xarrow("READ" x)
      cl sigma, mu, l cr$,
   )
 ))
@@ -831,38 +781,11 @@ $ sigma in env, space mu in mem, space m in mode,
   rule(
     name: [ WRITE $x$],
 
-    $sigma temode p -> cr r space w cl$,
+    $isPossibleWrite sigma(x)$,
 
-    $w == MaybeWrite or w == AlwaysWrite$,
-
-    $x tpath p$,
-
-    $mu[x] xarrowSquiggly(p)_write v$,
-
-    $cl sigma, mu cr
-     xarrow("WRITE" p)
-     cl sigma, mu[x <- v] cr$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ $s \; t$],
-
-    $cl sigma, mu cr
-     stretch(->)^s
-     cl sigma_s, mu_s cr$,
-
-    $cl sigma, mu cr
-     stretch(->)^t
-     cl sigma_t, mu_t cr$,
-
-    $cl sigma, mu, cr
-     xarrow(s \; t)
-     cl sigma_t, mu_t cr$,
+    $cl sigma, mu, l cr
+     xarrow("WRITE" x)
+     cl sigma, pathenvval(mu, sigma, x) <- 0, l cr$,
   )
 ))
 
@@ -870,27 +793,26 @@ $ sigma in env, space mu in mem, space m in mode,
 
 #let combine = `combine`
 
-*TODO: combine replacement* // FIXME
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ $s | t$],
+    name: [ CHOICE $overline(s)$ $overline(t)$],
 
     $cl sigma, mu, l cr
-     stretch(->)^s
+     attach(stretch(->)^overline(s), tr: *)
      cl sigma_s, mu_s, l_s cr$,
 
     $cl sigma, mu, l cr
-     stretch(->)^t
+     attach(stretch(->)^overline(t), tr: *)
      cl sigma_t, mu_t, l_t cr$,
 
+    $l_t = l_s$,
     $sigma_s = sigma_t$,
-    $mu' = combine(mu_s, mu_t)$,
 
     // TODO changes ?? two ways ??
-    $cl sigma, mu cr
-     xarrow(s | t)
-     cl sigma_t, mu' cr$,
+    $cl sigma, mu, l cr
+     xarrow("CHOICE" overline(s) space overline(t))
+     cl sigma, combine(mu_s, mu_t), l cr$,
   )
 ))
 
@@ -898,16 +820,9 @@ $ sigma in env, space mu in mem, space m in mode,
 
 === 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 ??
+$ combine_e (\_, \_) = X $
 
 ]