diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 5071c36..569c97a 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -11,7 +11,20 @@
 
 // TODO: check correctnes for path, mem & type ??
 
-== Syntax
+Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
+
+Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
+- & of | of & -вложенные блоки ?
+- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
+
+Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
+вызов лямбд будет нужен в модели?
+- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
+можно ввести отдельные сигнатуры-определения?
+
+проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
+
+== Синтаксис
 
 #h(10pt)
 
@@ -25,19 +38,18 @@
 #let isIn = `isIn`
 #let isOut = `isOut`
 
-#let mode = `mode`
-#let expr = `expr`
+#let tag = `tag`
+#let value = `value`
 #let stmt = `stmt`
 #let decl = `decl`
 #let prog = `prog`
 #let path = `path`
-#let type = `type`
+#let argtype = `argtype`
+#let argmem = `argmem`
 #bnf(
   Prod(`read`,
-    // NOTE: not three modalities for write, because read does not change value
-    // => it is not important to observe rsult, no differenc between always and maybe
     { Or[Read][read passed value]
-      Or[$not$ Read][] } ),
+      Or[Not Read][] } ),
   Prod(`write`,
     { Or[$square$ Write][in all cases there is a write to passed variable] // always write, requre at least one write in each flow variant
       Or[$diamond$ Write][in some cases there is a write to passed variable] // possible write, no requirements (?)
@@ -47,276 +59,117 @@
       Or[Value][pass copy of the value] } ),
   Prod(`in`,
     { Or[In][parameter value used as input]
-      Or[$not$ In][] } ),
+      Or[Not In][] } ),
   Prod(`out`,
-    { Or[Out][parameter value returned]
-      Or[$not$ Out][] } ),
+    { Or[Out][parametr value returned]
+      Or[Not Out][] } ),
   Prod(
-    `mode`,
+    `tag`,
     {
       Or[`read` #h(3pt) `write` #h(3pt) `copy` #h(3pt) `in` #h(3pt) `out`][]
     }
   ),
+  Prod(
+    `value`,
+    {
+      Or[$0$][cell with some value (always)]
+      Or[$X$][cell with possible value or $bot$]
+      Or[$bot$][spoiled cell (always)]
+    }
+  ),
   Prod(
     `path`,
     {
-      // NOTE: global vars & local vars names could be used with one constructor
-      // Or[$\#x$][funciton or global variable itself]
-      Or[$@ X$][function argument or variable itself]
+      Or[$@x$][fuction argument or variable itself]
       Or[$* path$][reference insede path]
       Or[$path . n$][access $n$-th cell of the tuple]
       // Or[$path : n$][access $n$-th cell of the union] // TODO: another notation ??
     }
   ),
   Prod(
-    `type`,
+    `argtype`,
     {
       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_(type+)$][type of lambda or function pointer, defined by function declaration] // `Fun`
+      Or[\& #h(3pt) `tag` #h(3pt) `argtype`][reference to structure, contains copy / ref choice] // `Ref`
+      Or[\[#overline(`argtype`)\]][pair type, allows to make tuples] // `Prod`
+      // Or[`argtype` $times$ `argtype`][pair type, allows to make tuples] // `Prod`
+      // Or[`argtype` $+$ `argtype`][union type (important in some way ???)] // `Sum` // TODO ?
+      Or[$F_x$][type of lambda or function pointer, defined by function declaration id] // `Fun`
     }
   ),
-  // FIXME: replace with expr
   Prod(
-    `expr`,
+    `argmem`,
     {
-      Or[$()$][value of simple type] // `Unit`
-      Or[$path$][value from variable] // `Path`
-      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`
+      Or[$@m$][memory id for simple type variable] // `Unit`
+      Or[\& #h(3pt) `argmem`][reference to structure, contains copy / ref choice] // `Ref`
+      // Or[\& #h(3pt) `tag` #h(3pt) `argmem`][reference to structure, contains copy / ref choice] // `Ref`
+      Or[\[#overline(`argmem`)\]][pair type, allows specify memory for tuples] // `Prod`
+      // Or[`argmem` $times$ `argmem`][pair type, allows specify memory for tuples] // `Prod`
+      // Or[`argmem` $+$ `argmem`][union type (important in some way ???)] // `Sum` // TODO ?
+      Or[$F$][memory for lambda or function pointer, defined by function declaration id] // `Fun` // why separated ??
+      // Or[$F_m$][memory for lambda or function pointer, defined by function declaration id] // `Fun` // why separated ??
     }
   ),
+  // Prod(
+  //   `arg`,
+  //   {
+  //     Or[$0$][new value, no associated variable]
+  //     Or[$ amp d$][value from some variable]
+  //   }
+  // ),
   Prod(
     `stmt`,
     {
-      Or[`CALL` $f space expr+$][call function]
+      Or[`CALL` $f space overline(path)$][call function by id]
+      Or[`CALL_LAM` $path space overline(path)$][call lambda funciton (variable or funcitona argument field)]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
-      Or[$stmt ; stmt$][control flow operator, xecution ]
-      Or[$stmt | stmt$][control flow operator, excution of one statements]
+      // TODO: or introduce block statement ?? // vars definiiton statment ??
+      // (for example, for same named vars in nested spaces)
+      Or[`CHOICE` #overline(`stmt`) #overline(`stmt`)][control flow operator, xecution of one of the blocks]
+      // NOTE: var: replaced with arguments (use rvalue as init) (?)
+      // Or[`VAR`][variables inside functions] // NOTE: no modifiers required, because it is in the new memory ?? // TODO: not required ??
+      // NOTE: lambda: compile to call to the funciton with CHOICE between possible lambda bodies <- do this analysis inside synthesizer ?
     }
   ),
   Prod(
     `decl`,
     {
-      // TODO: path not allowed ??
-      Or[$"var" X : type = expr$][global variable declaration]
-      Or[$"fun" X ((X : type)+) = stmt$][function declaration]
+      Or[$overline(stmt)$][function body]
+      Or[$lambda a : argtype.$ `decl`][argument with argument pass strategy annotation]
     }
   ),
   Prod(
     `prog`,
     {
-      Or[$decl stmt$][declarations and executet statement]
+      Or[`decl`][main function]
+      Or[`decl` `prog`][with supplimentary funcitons]
     }
   ),
 )
+== Семантика статического интерпретатора
 
-== Value Model
+#h(10pt)
 
-// FIXME: check & add details
-#let value = `value`
-#bnf(
-  Prod(
-    `value`,
-    {
-      Or[$()$][value of simple type] // `Unit`
-      Or[$lambda_X$][function pointer value] // `Fun`
-      Or[$\& #h(3pt) value$][reference value] // `Ref`
-      Or[$[value+]$][tuple value] // `Prod`
-    }
-  ),
-)
+$V := value$ - значения памяти
 
-$value$ - значения, которые могут лежать в переменных и передаваться как аргументы функций (то, во что вычисляется $expr$)
-
-== Memory Model
-
-// FIXME: check & add details
-#let memelem = `memelem`
-#let valuemem = `valuemem`
-#bnf(
-  Prod(
-    `memelem`,
-    {
-      Or[$0$][cell with some value (always)]
-      Or[$\#$][cell with possible value or $bot$]
-      Or[$bot$][spoiled cell (always)]
-    }
-  ),
-  Prod(
-    `valuemem`,
-    {
-      Or[$()$][one unit of memory, for simple vars] // `Unit`
-      Or[$lambda$][memory for lambda or function pointer, is not important in the memory model, 0 units] // `Fun`
-      Or[$\& #h(3pt) LL valuemem$][reference to structure memory start] // `Ref`
-      Or[$[valuemem+]$][memory specification for each tuple member] // `Prod`
-    }
-  ),
-)
-
-#let mem = `mem`
-Память преставляется в виде стека из значений `memelem`:
-- $LL = NN$ - множество меток памяти
-- $mu : mem = LL -> V$ - память, частично определённая функция
-- $l in LL$ - длина используемого фрагмента памяти
-
-Каждому значению $value$ в соответствие ставится $valuemem$ - расположние этого значения в пaмяти
-
-Соответствие:
-- $() -> ()$
-- $lambda_X -> lambda$
-- $\& #h(3pt) value -> \& #h(3pt) LL valuemem$
-- $[value+] -> [valuemem+]$
-
-// TODO: move allocation semantics there ??
-
-== Semantics
-
-// $V := memelem$ - значения памяти
+$L := NN$ - позиции в памяти
 
 $X$ - можество переменных
 
-#let env = `env`
-$sigma : env = X -> valuemem times type$ - #[ позиции памяти, соответстующие переменным контекста, частично определённая функция ]
+$sigma : X -> argmem times argtype$ - #[ позиции памяти, соответстующие переменным контекста,
+                           частично определённая функция ]
 
-$DD : X -> decl$ - глобальные определения, частично определённая функция
+$mu : NN -> V$ - память, частично определённая функция
 
-$d in decl, s in stmt, f in X, x in X, a in X$
+$l in NN$ - длина используемого фрагмента памяти
+
+$DD : NN -> decl$ - определения функций, частично определённая функция
+
+$d in decl, s in stmt, f in NN, x in X, a in NN$
 
 $d space @ space overline(x)$ - запись применения функции (вида #decl) к аргументам
 
-=== Path Accessors
-
-Набор частично определённых фунций для работы с путями.
-Для удобства значение, получаемое из текущего применением пути, будем называть полем.
-// Все эти функции используются с префиксом `path.`.
-
-// FIXME: types & description for functios
-#let pathtype = `path.type`
-#let pathmem = `path.mem`
-#let pathmode = `path.mode`
-#let pathvar = `path.var`
-
-#let pathsize = `path.memsize`
-#let pathbasepos = `path.membasepos`
-#let pathoffset = `path.memoffset`
-#let pathpos = `path.mempos`
-
-#let pathenvtype = `path.envtype`
-#let pathenvmem = `path.envmem`
-#let pathenvmode = `path.envmode`
-
-#let pathenvpos = `path.envpos`
-#let pathenvval = `path.envval`
-
-- #[ Получение типа поля
-$ pathtype : type -> path -> type $
-$ pathtype(t, @x) = t $
-$ pathtype(\& #h(3pt) mode #h(3pt) t, *p) = pathtype(t, p) $
-$ pathtype([t_1, t_2, ..., t_n], p.i) = pathtype(t_i, p) $
-]
-- #[ Получение начала памяти поля (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
-$ pathmem : valuemem -> path -> LL $
-$ pathmem(\& #h(3pt) y m, @x) = y $ // NOTE: only memory for refsi in midel ?? // TODO: decide
-$ pathmem(\& #h(3pt) y m, *p) = pathmem(m, p) $
-$ pathmem([m_1, m_2, ..., m_n], p.i) = pathmem(m_i, p) $
-]
-- #[ Получения тега поля (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
-$ pathmode : type -> path -> mode $
-$ pathmode(\& #h(3pt) mode #h(3pt) t, @x) = mode $
-$ pathmode(\& #h(3pt) mode #h(3pt) t, *p) = pathmode(t, p) $
-$ pathmode([t_1, t_2, ..., t_n], p.i) = pathmode(t_i, p) $
-]
-- #[ Получение \"корневой\" переменной пути
-$ pathvar : path -> X $
-$ pathvar(@x) = x $
-$ pathvar(* p) = pathvar(p) $
-$ pathvar(p.i) = pathvar(p) $
-]
-- #[ Получение размера поля в памяти
-$ pathsize : valuemem -> path -> LL $
-$ pathsize((), @x) = 1 $
-$ pathsize(lambda, @x) = 0 $
-$ pathsize(\& #h(3pt) y m, @x) = 0 $ // TODO: FIXME ?? always disconnected location ??
-$ pathsize([m_1, m_2, ..., m_n], @x) = pathsize(m_1, @x) + ... + pathsize(m_n, @x) $
-$ pathsize(\& #h(3pt) y m, *p) = pathsize(m, p) $
-$ pathsize([m_1, m_2, ..., m_n], p.i) = pathsize(m_i, p) $
-]
-// TODO: FIXME ??
-- #[ Получение позиции последного ссылочного предка поля в пaмяти
-$ pathbasepos : value -> path -> X $
-// $ pathbasepos(m, @x) = bot $ // NOTE: trivial if not present ??
-$ pathbasepos(\& #h(3pt) y m, *p) = pathbasepos(m, p) | y $
-$ pathbasepos([m_1, m_2, ..., m_n], p.i) = pathbasepos(m_i, p) $
-]
-- #[ Получение смещения поля в последнем монолитном отрезке памяти
-$ pathoffset : value -> path -> X $
-$ pathoffset(m, @x) = 0 $
-$ pathoffset(\& #h(3pt) y m, *p) = pathoffset(m, p) $
-$ pathoffset([m_1, m_2, ..., m_n], p.i) = (i - 1) + pathoffset(m_i, p) $
-]
-- #[ Получение позиции поля в пaмяти
-$ pathpos : value -> path -> X $
-$ pathpos(m, p) = pathbasepos(m, p) + pathoffset(m, p)$
-]
-- #[ Получение типа поля по окружению
-$ pathenvtype : env -> path -> type $
-$ pathenvtype(sigma, p) = pathtype(sigma[pathvar(p)].2, p) $
-]
-- #[ Получение начала памяти поля по окружению (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
-$ pathenvmem : env -> path -> LL $
-$ pathenvmem(sigma, p) = pathmem(sigma[pathvar(p)].1, p) $
-]
-- #[ Получения тега поля по окружению (предусловие: $pathtype(t, p) = \& #h(3pt) ...$)
-$ pathenvmode : env -> path -> mode $
-$ pathenvmode(sigma, p) = pathmode(sigma[pathvar(p)].2, p) $
-]
-- #[ Получение позиции поля в пaмяти по окружению
-$ pathenvpos : env -> path -> X $
-$ pathenvpos(m, p) = pathpos(sigma[pathvar(p)].1, p)$
-]
-- #[ Получение поля в пaмяти
-$ pathenvval : env -> mem -> path -> memelem $
-$ pathenvval(sigma, mu, p) = mu[pathenvpos(sigma, p)]$
-]
-
-=== 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
-
-// FIXME: make connected to syntax
-*TODO*
-
-#h(10pt)
-
 #let args = `args`
 
 #[
@@ -346,23 +199,66 @@ $ isRead mode -> isIn mode $
 
 #h(10pt)
 
-=== Correctness
+=== Path
 
-// TODO: FIXME: well formatness for mode, extract
-// TODO: FIXME: check for mode, is recursion required ??
-// TODO: FIXME: check mode & access corectness in os correct
+#let pathtype = `pathtype`
+$ pathtype(t, @x) = t $
+$ pathtype(\& #h(3pt) tag #h(3pt) t, *p) = pathtype(t, p) $
+$ pathtype([t_1, t_2, ..., t_n], p.i) = pathtype(t_i, p) $
+
+#let pathmem = `pathmem`
+$ pathmem(@m, @x) = m $
+$ pathmem(\& #h(3pt) m, *p) = pathmem(m, p) $
+$ pathmem([m_1, m_2, ..., m_n], p.i) = pathmem(m_i, p) $
+
+// NOTE: is replaced with pathtype
+// #let pathfun = `pathfun`
+// $ pathfun(F_m, @x) = m $
+// $ pathfun(\& #h(3pt) m, *p) = pathfun(m, p) $
+// $ pathfun([m_1, m_2, ..., m_n], p.i) = pathfun(m_i, p) $
+
+#let pathtag = `pathtag`
+$ pathtag(\& #h(3pt) tag #h(3pt) t, @x) = tag $
+$ pathtag(\& #h(3pt) tag #h(3pt) t, *p) = pathtag(t, p) $
+$ pathtag([t_1, t_2, ..., t_n], p.i) = pathtag(t_i, p) $
+
+#let pathvar = `pathvar`
+$ pathvar(@x) = x $
+$ pathvar(* p) = pathvar(p) $
+$ pathvar(p.i) = pathvar(p) $
+
+#h(10pt)
+
+// $ pathtype({t_1, t_2, ..., t_n}, x -> i) = t_i$
+
+#let typeof = `typeof`
+$ typeof(sigma, p) = pathtype(sigma[pathvar(p)].2, p) $
+
+// TODO: two versions: write with change & read ??
+#let accessmem = `accessmem`
+$ accessmem(sigma, p) = pathmem(sigma[pathvar(p)].1, p) $
+
+#let argtag = `argtag`
+$ argtag(sigma, p) = pathtag(sigma[pathvar(p)].2, p) $
+
+#let access = `access`
+$ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
+
+#h(10pt)
+
+=== Correctness
 
 // TODO: check all requirements
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     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$,
+    $isOut tag -> isAlwaysWrite tag$, // NOTE; strong requirment should write
+    $isRead tag -> isIn tag$,
+    $isPossibleWrite tag and (isOut tag or not isCopy tag) -> isAlwaysWrite argtag(sigma, x)$, // NOTE: may tag => should sigma(x)
+    $isRead tag -> access(mu, sigma, x) != bot and access(mu, sigma, x) != X$,
 
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
   )
 ))
 
@@ -370,10 +266,10 @@ $ isRead mode -> isIn mode $
 
 === Call Initialization
 
-Отсутствующий нижний индекс ($ref$, $copy$) означает произвольный индекс.
+Отсутствующий ижний индекс ($ref$, $copy$) означает произвольный индекс.
 Считается, что выбранный индекс одинаков в рамках одного правила.
 
-// NOTE: no empty type
+// NOTE: no empty argtype
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
@@ -391,7 +287,7 @@ $ isRead mode -> isIn mode $
     name: [ add paths field by copy],
 
     // TODO: check that access is what required ??
-    $cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl pathenvmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl accessmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
   )
 ))
 
@@ -414,9 +310,9 @@ $ isRead mode -> isIn mode $
   rule(
     name: [ add paths ref],
     $cl sigma, mu, l cr xarrowSquiggly(*p : t)_ref cl sigma', mu', l' cr$,
-    $isRef mode$,
+    $isRef tag$,
 
-    $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : \& tag t) cl sigma', mu', l' cr$,
   )
 ))
 
@@ -427,9 +323,9 @@ $ isRead mode -> isIn mode $
   rule(
     name: [ add paths ref],
     $cl sigma, mu, l cr xarrowSquiggly(*p : t)_copy cl sigma, mu, l cr$,
-    $isCopy mode$,
+    $isCopy tag$,
 
-    $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : \& tag t) cl sigma', mu', l' cr$,
   )
 ))
 
@@ -479,14 +375,14 @@ $ isRead mode -> isIn mode $
 
     $mu stretch(=>)^args_sigma gamma$,
 
-    $isPossibleWrite mode$, // NOTE: weak requirement: may write
-    $not isCopy mode$,
-    $not isOut mode$,
+    $isPossibleWrite tag$, // NOTE: weak requirement: may write
+    $not isCopy tag$,
+    $not isOut tag$,
 
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- bot]$
+    $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- bot]$
   )
 ))
 
@@ -499,13 +395,13 @@ $ isRead mode -> isIn mode $
 
     $mu stretch(=>)^args_sigma gamma$,
 
-    $isAlwaysWrite mode$, // NOTE: strong requirement: should write
-    $isOut mode$,
+    $isAlwaysWrite tag$, // NOTE: strong requirement: should write
+    $isOut tag$,
 
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- 0]$
+    $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- 0]$
   )
 ))
 
@@ -521,10 +417,10 @@ $ isRead mode -> isIn mode $
     $not "spoil step"$,
     $not "fix step"$,
 
-    $isCorrect_(cl sigma, mu cr) (mode, x)$,
+    $isCorrect_(cl sigma, mu cr) (tag, x)$,
 
     // mu
-    $gamma stretch(=>)^((mode, x) : args)_sigma gamma$
+    $gamma stretch(=>)^((tag, x) : args)_sigma gamma$
   )
 ))
 
@@ -548,8 +444,8 @@ $ isRead mode -> isIn mode $
      xarrowDashed(d space @ space overline(y))
      cl sigma'', mu'', l'' cr$,
 
-    $isRead mode$,
-    $not isCopy mode$,
+    $isRead tag$,
+    $not isCopy tag$,
 
     // NOTE: correctness checked in CALL f
 
@@ -609,7 +505,7 @@ $ isRead mode -> isIn mode $
   rule(
     name: [ CALL_LAM $y space overline(x)$],
 
-    $pathenvtype(sigma, y) = F_f$,
+    $typeof(sigma, y) = F_f$,
 
     $cl sigma, mu, l cr
      xarrow("CALL" f space overline(x))
@@ -628,8 +524,8 @@ $ isRead mode -> isIn mode $
   rule(
     name: [ READ $x$],
 
-    $pathenvval(mu, sigma, x) != bot$,
-    $pathenvval(mu, sigma, x) != X$,
+    $access(mu, sigma, x) != bot$,
+    $access(mu, sigma, x) != X$,
 
     $cl sigma, mu, l cr
      xarrow("READ" x)
@@ -648,7 +544,7 @@ $ isRead mode -> isIn mode $
 
     $cl sigma, mu, l cr
      xarrow("WRITE" x)
-     cl sigma, pathenvval(mu, sigma, x) <- 0, l cr$,
+     cl sigma, access(mu, sigma, x) <- 0, l cr$,
   )
 ))