diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 569c97a..5071c36 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -11,20 +11,7 @@
 
 // TODO: check correctnes for path, mem & type ??
 
-Нужно будет добавить во write-flag модальности: `not write` | `may write` | `always write`
-
-Добавление condition-исполнения - выбор из нескольких блоков. Варианты:
-- & of | of & -вложенные блоки ?
-- добавить несколько альтернативны тел функциям. Но тогда придётся при трансляции if-блоки выносить в функции
-
-Лямбды - нужно тоже будет как-то находить лямбды и ля них тоже синтезировать атрибуты
-вызов лямбд будет нужен в модели?
-- lambda-аргумент - вложенные теги?, должна быть одна и та же сигнтура
-можно ввести отдельные сигнатуры-определения?
-
-проблема простой семантики: вызов лямбд: могут быть модифицируемые функции
-
-== Синтаксис
+== Syntax
 
 #h(10pt)
 
@@ -38,18 +25,19 @@
 #let isIn = `isIn`
 #let isOut = `isOut`
 
-#let tag = `tag`
-#let value = `value`
+#let mode = `mode`
+#let expr = `expr`
 #let stmt = `stmt`
 #let decl = `decl`
 #let prog = `prog`
 #let path = `path`
-#let argtype = `argtype`
-#let argmem = `argmem`
+#let type = `type`
 #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 (?)
@@ -59,117 +47,276 @@
       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][parametr value returned]
-      Or[Not Out][] } ),
+    { Or[Out][parameter value returned]
+      Or[$not$ Out][] } ),
   Prod(
-    `tag`,
+    `mode`,
     {
       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`,
     {
-      Or[$@x$][fuction argument or variable itself]
+      // 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[$* 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(
-    `argtype`,
+    `type`,
     {
       Or[$()$][simple type representing all primitive types] // `Unit`
-      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`
+      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`
     }
   ),
+  // FIXME: replace with expr
   Prod(
-    `argmem`,
+    `expr`,
     {
-      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 ??
+      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`
     }
   ),
-  // Prod(
-  //   `arg`,
-  //   {
-  //     Or[$0$][new value, no associated variable]
-  //     Or[$ amp d$][value from some variable]
-  //   }
-  // ),
   Prod(
     `stmt`,
     {
-      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[`CALL` $f space expr+$][call function]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
-      // 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 ?
+      Or[$stmt ; stmt$][control flow operator, xecution ]
+      Or[$stmt | stmt$][control flow operator, excution of one statements]
     }
   ),
   Prod(
     `decl`,
     {
-      Or[$overline(stmt)$][function body]
-      Or[$lambda a : argtype.$ `decl`][argument with argument pass strategy annotation]
+      // TODO: path not allowed ??
+      Or[$"var" X : type = expr$][global variable declaration]
+      Or[$"fun" X ((X : type)+) = stmt$][function declaration]
     }
   ),
   Prod(
     `prog`,
     {
-      Or[`decl`][main function]
-      Or[`decl` `prog`][with supplimentary funcitons]
+      Or[$decl stmt$][declarations and executet statement]
     }
   ),
 )
-== Семантика статического интерпретатора
 
-#h(10pt)
+== Value Model
 
-$V := value$ - значения памяти
+// 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`
+    }
+  ),
+)
 
-$L := NN$ - позиции в памяти
+$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$ - значения памяти
 
 $X$ - можество переменных
 
-$sigma : X -> argmem times argtype$ - #[ позиции памяти, соответстующие переменным контекста,
-                           частично определённая функция ]
+#let env = `env`
+$sigma : env = X -> valuemem times type$ - #[ позиции памяти, соответстующие переменным контекста, частично определённая функция ]
 
-$mu : NN -> V$ - память, частично определённая функция
+$DD : X -> decl$ - глобальные определения, частично определённая функция
 
-$l in NN$ - длина используемого фрагмента памяти
-
-$DD : NN -> decl$ - определения функций, частично определённая функция
-
-$d in decl, s in stmt, f in NN, x in X, a in NN$
+$d in decl, s in stmt, f in X, x in X, a in X$
 
 $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`
 
 #[
@@ -199,66 +346,23 @@ $d space @ space overline(x)$ - запись применения функции
 
 #h(10pt)
 
-=== Path
-
-#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: FIXME: well formatness for mode, extract
+// TODO: FIXME: check for mode, is recursion required ??
+// TODO: FIXME: check mode & access corectness in os correct
+
 // TODO: check all requirements
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ is correct],
-    $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$,
+    $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$,
 
-    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+    $isCorrect_(cl sigma, mu cr) (mode, x)$,
   )
 ))
 
@@ -266,10 +370,10 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
 
 === Call Initialization
 
-Отсутствующий ижний индекс ($ref$, $copy$) означает произвольный индекс.
+Отсутствующий нижний индекс ($ref$, $copy$) означает произвольный индекс.
 Считается, что выбранный индекс одинаков в рамках одного правила.
 
-// NOTE: no empty argtype
+// NOTE: no empty type
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
@@ -287,7 +391,7 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
     name: [ add paths field by copy],
 
     // TODO: check that access is what required ??
-    $cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl accessmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : ())_copy cl pathenvmem(sigma, p) <- l, mu [l <- 0], l + 1 cr$,
   )
 ))
 
@@ -310,9 +414,9 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
   rule(
     name: [ add paths ref],
     $cl sigma, mu, l cr xarrowSquiggly(*p : t)_ref cl sigma', mu', l' cr$,
-    $isRef tag$,
+    $isRef mode$,
 
-    $cl sigma, mu, l cr xarrowSquiggly(p : \& tag t) cl sigma', mu', l' cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
   )
 ))
 
@@ -323,9 +427,9 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
   rule(
     name: [ add paths ref],
     $cl sigma, mu, l cr xarrowSquiggly(*p : t)_copy cl sigma, mu, l cr$,
-    $isCopy tag$,
+    $isCopy mode$,
 
-    $cl sigma, mu, l cr xarrowSquiggly(p : \& tag t) cl sigma', mu', l' cr$,
+    $cl sigma, mu, l cr xarrowSquiggly(p : \& mode t) cl sigma', mu', l' cr$,
   )
 ))
 
@@ -375,14 +479,14 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
 
     $mu stretch(=>)^args_sigma gamma$,
 
-    $isPossibleWrite tag$, // NOTE: weak requirement: may write
-    $not isCopy tag$,
-    $not isOut tag$,
+    $isPossibleWrite mode$, // NOTE: weak requirement: may write
+    $not isCopy mode$,
+    $not isOut mode$,
 
-    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+    $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- bot]$
+    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- bot]$
   )
 ))
 
@@ -395,13 +499,13 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
 
     $mu stretch(=>)^args_sigma gamma$,
 
-    $isAlwaysWrite tag$, // NOTE: strong requirement: should write
-    $isOut tag$,
+    $isAlwaysWrite mode$, // NOTE: strong requirement: should write
+    $isOut mode$,
 
-    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+    $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // gamma - memory (as mu)
-    $gamma stretch(=>)^((tag, x) : args)_sigma access(gamma, sigma, x) <- 0]$
+    $gamma stretch(=>)^((mode, x) : args)_sigma pathenvval(gamma, sigma, x) <- 0]$
   )
 ))
 
@@ -417,10 +521,10 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
     $not "spoil step"$,
     $not "fix step"$,
 
-    $isCorrect_(cl sigma, mu cr) (tag, x)$,
+    $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
     // mu
-    $gamma stretch(=>)^((tag, x) : args)_sigma gamma$
+    $gamma stretch(=>)^((mode, x) : args)_sigma gamma$
   )
 ))
 
@@ -444,8 +548,8 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
      xarrowDashed(d space @ space overline(y))
      cl sigma'', mu'', l'' cr$,
 
-    $isRead tag$,
-    $not isCopy tag$,
+    $isRead mode$,
+    $not isCopy mode$,
 
     // NOTE: correctness checked in CALL f
 
@@ -505,7 +609,7 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
   rule(
     name: [ CALL_LAM $y space overline(x)$],
 
-    $typeof(sigma, y) = F_f$,
+    $pathenvtype(sigma, y) = F_f$,
 
     $cl sigma, mu, l cr
      xarrow("CALL" f space overline(x))
@@ -524,8 +628,8 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
   rule(
     name: [ READ $x$],
 
-    $access(mu, sigma, x) != bot$,
-    $access(mu, sigma, x) != X$,
+    $pathenvval(mu, sigma, x) != bot$,
+    $pathenvval(mu, sigma, x) != X$,
 
     $cl sigma, mu, l cr
      xarrow("READ" x)
@@ -544,7 +648,7 @@ $ access(sigma, mu, p) = mu[accessmem(sigma, p)] $
 
     $cl sigma, mu, l cr
      xarrow("WRITE" x)
-     cl sigma, access(mu, sigma, x) <- 0, l cr$,
+     cl sigma, pathenvval(mu, sigma, x) <- 0, l cr$,
   )
 ))