diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 0968b8b..5fff471 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -24,6 +24,8 @@
 #let isPossibleWrite = `isPossibleWrite`
 #let isRef = `isRef`
 #let isCopy = `isCopy`
+#let isIn = `isIn`
+#let isOut = `isOut`
 
 #let readTag = `read`
 #let writeTag = `write`
@@ -40,9 +42,6 @@
 #let In = `In`
 #let Out = `Out`
 
-#let cl = $chevron.l$
-#let cr = $chevron.r$
-
 #let expr = `expr`
 #let stmt = `stmt`
 #let decl = `decl`
@@ -57,9 +56,9 @@
     { Or[Read][read passed value]
       Or[$not$ Read][] } ),
   Prod(`write`,
-    { Or[$square$ Write][in all cases there is a write to the variable] // always write, requre at least one write in each flow variant
-      Or[$diamond$ Write][in some cases there is a write to the variable] // possible write, no requirements (?)
-      Or[$not$ Write][in none cases there is a write to the variable ] } ), // no write, require n owrites in all flow variants
+    { 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 (?)
+      Or[$not$ Write][] } ), // no write, require n owrites in all flow variants
   Prod(`copy`,
     { Or[Ref][pass reference to the value]
       Or[Value][pass copy of the value] } ),
@@ -89,8 +88,8 @@
   Prod(
     `type`,
     {
-      Or[$cl readTag, writeTag cr$][simple type representing all primitive types] // `Unit`
-      Or[$rf copyTag type$][reference to structure, contains copy / ref choice] // `Ref`
+      Or[$readTag writeTag ()$][simple type representing all primitive types] // `Unit`
+      Or[$rf copyTag space 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 ?
@@ -153,7 +152,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 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`
     }
@@ -164,8 +163,9 @@
       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[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
+      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[$[value+]$][tuple value] // `Prod`
     }
   ),
@@ -178,12 +178,15 @@
 $v in value$ - произвольное значение
 
 Получение #deepValue по #value:
-- $rf l xarrowSquiggly(mu)_#[deep] rf mu[l]$
+- $rf c l xarrowSquiggly(mu)_#[deep] rf c mu[l]$
 - $* xarrowSquiggly(mu)_#[deep] *$
 где $*$ - произвольный конструктор значения, кроме $rf$
 
 == Memory Model
 
+#let cl = $chevron.l$
+#let cr = $chevron.r$
+
 #let mem = `mem`
 
 - $LL$ - множество меток памяти
@@ -216,12 +219,8 @@ $X$ - можество переменных
 #let pathenvmem = `pathenvmem`
 #let pathenvtype = `pathenvtype`
 
-#let vals = $Sigma$
-#let types = $Gamma$
-#let envv = $#[env]_Sigma$
-#let envt = $#[env]_Gamma$
-$sigma : envv := X -> LL, space vals : envv$ - #[ метки памяти перменных контекста, частично определённая функция ]
-$sigma : envt := X -> type, space types : envt$ - #[ типы значений перменных контекста, частично определённая функция ]
+#let env = `env`
+$sigma : env := X -> LL times type, space sigma : env$ - #[ метки памяти и типы значений пеерменных контекста, частично определённая функция ]
 
 // $DD : X -> decl$ - глобальные определения, частично определённая функция
 
@@ -240,9 +239,8 @@ $s in stmt, f in X, x in X, a in X$
 #let eqmu = $attach(=, br: mu)$
 #let arrmu = $attach(->, br: mu)$
 
-#let arrpath = $xarrowSquiggly(mu)_path$
-
 #let ttype = $attach(tack.r, br: type)$
+#let tpath = $attach(tack.r, br: path)$
 #let tmode = $attach(tack.r, br: mode)$
 
 #let val = `val`
@@ -250,22 +248,22 @@ $s in stmt, f in X, x in X, a in X$
 #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 tetype = $attach(tack.r.double, br: type)$
+#let temode = $attach(tack.r.double, br: mode)$
 
 #let teval = $attach(tack.r.double, br: val)$
+#let telabel = $attach(tack.r.double, br: label)$
 
 // TODO: env mem label ??, env mem value ??
 
+// TODO: FIXME: backwards, deconstruction ??
 - #[ Конструирование путей по переменой
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ variable path],
 
-    $@x arrpath x$,
+    $x tpath @x$,
   )
 ))
 #align(center, prooftree(
@@ -273,8 +271,8 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ reference path],
 
-    $p arrpath x$,
-    $rf p arrpath x$,
+    $x tpath p$,
+    $x tpath rf p$,
   )
 ))
 #align(center, prooftree(
@@ -282,9 +280,9 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ tuple access path],
 
-    $p arrpath x$,
+    $x tpath p$,
 
-    $p.i arrpath x$,
+    $x tpath p.i$,
   )
 ))
 ]
@@ -295,8 +293,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ variable type access],
 
-    $x : t_x in types$,
-    $types ttype @x : t_x$,
+    $x : t_x ttype @x : t_x$,
   )
 ))
 #align(center, prooftree(
@@ -304,8 +301,9 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ reference type access],
 
-    $types ttype p : rf mode t_p$,
-    $types ttype *p : t_p$,
+    $x tpath p$,
+    $x : t_x ttype p : rf mode t_p$,
+    $x : t_x ttype *p : t_p$,
   )
 ))
 #align(center, prooftree(
@@ -313,24 +311,44 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ tuple type access],
 
-    $types ttype p : [t_1, ... t_n]$,
-    $types ttype p.i : t_i$,
+    $x tpath p$,
+    $x : t_x ttype p : [t_1, ... t_n]$,
+    $x : t_x ttype p.i : t_i$,
   )
 ))
 ]
 
-// TODO: not required (trivial) ??
-// - #[ Получение read-write тега поля
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ rw tag access],
+- #[ Получение read-write тега поля
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ variable rw tag access],
 
-//     $types ttype p : cl r, w cr$,
-//     $types tmode p -> cl r, w cr$,
-//   )
-// ))
-// ]
+    $t_x = r w ()$,
+    $x : t_x tmode @x -> cr r w cl$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ reference rw tag access],
+
+    $x tpath p$,
+    $x : t_x tmode p -> cr r w cl$,
+    $x : t_x tmode *p ->  cr r w cl$,
+  )
+))
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ tuple rw tag access],
+
+    $x tpath p$,
+    $x : t_x tmode p ->  cr r w cl$,
+    $x : t_x tmode p.i -> cr r w cl$,
+  )
+))
+]
 
 - #[ Получение значения поля
 #align(center, prooftree(
@@ -338,9 +356,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ variable value access],
 
-    $x -> l in vals$,
-    $mu[l] = v$,
-    $vals, mu tval x eqmu v$,
+    $x eqmu v_x tval @x eqmu v_x$,
   )
 ))
 #align(center, prooftree(
@@ -348,8 +364,9 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ reference value access],
 
-    $vals, mu tval p eqmu rf l$,
-    $vals, mu tval *p eqmu mu[l]$,
+    $x tpath p$,
+    $x eqmu v_x tval p eqmu rf l$,
+    $x eqmu v_x tval *p eqmu mu[l]$,
   )
 ))
 #align(center, prooftree(
@@ -357,37 +374,52 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ tuple value access],
 
-    $vals, mu tval p eqmu [v_1, ... v_n]$,
-    $vals, mu tval p.i eqmu v_i$,
+    $x tpath p$,
+    $x eqmu v_x tmode p eqmu [v_1, ... v_n]$,
+    $x eqmu v_x tmode p.i eqmu v_i$,
   )
 ))
 ]
 
-// TODO: FIXME: not required (trivial) ??
-// - #[ Получение метки поля
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ access],
+- #[ Получение метки поля
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ access],
 
-//     $vals, mu tval p eqmu rf l$,
-//     $vals, mu tmode p arrmu l$,
-//   )
-// ))
-// ]
+    $v_x = rf l$,
+    $x eqmu v_x tval p eqmu rf l$,
 
-// TODO: not required (trivial) ??
-// - #[ Получение read-write тега поля по окружению
-// #align(center, prooftree(
-//   vertical-spacing: 4pt,
-//   rule(
-//     name: [ access],
+    $x eqmu v_x tmode p arrmu l$,
+  )
+))
+]
 
-//     $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 tpath p$,
+    $x : sigma[x].2 ttype p : t$,
+    $sigma tetype p : t$,
+  )
+))
+]
+
+- #[ Получение read-write тега поля по окружению
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ access],
+
+    $x tpath p$,
+    $x : sigma[x].2 tmode p -> cr r space w cl$,
+    $sigma temode p -> cr r space w cl$,
+  )
+))
+]
 
 - #[ Получение значения поля по окружению
 #align(center, prooftree(
@@ -395,12 +427,33 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ access],
 
-    $x eqmu vals[x] tval p eqmu v$,
-    $types, vals, mu teval p eqmu x$,
+    $x tpath p$,
+    $x eqmu sigma[x].1 tval p eqmu v$,
+    $sigma, mu teval p eqmu x$,
   )
 ))
 ]
 
+- #[ Получение метки поля по окружению
+#align(center, prooftree(
+  vertical-spacing: 4pt,
+  rule(
+    name: [ access],
+
+    $x tpath p$,
+    $x eqmu sigma[x].1 tlabel p arrmu l$,
+    $sigma, mu telabel p arrmu l$,
+  )
+))
+]
+
+=== Mode Accessors
+
+#let modevar = $(i space o)$
+
+$ isIn modevar = i == In $
+$ isOut modevar = o == Out $
+
 // FIXME: move to new mode model
 // === Mode Correctness
 
@@ -457,40 +510,27 @@ $s in stmt, f in X, x in X, a in X$
 // TODO: FIXME: check for mode, is recursion required ??
 // TODO: FIXME: check mode & access corectness in os correct
 
-$ vals in envv, types in envt, space mu in mem, space m in mode,
+$ 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: FIXME: complete rule check
-// + add part about ref -> not copy later
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ unit assignment tags correctness],
 
-    $r = Read => m = (In, \_)$, 
-    $m = (\_, Out) => w = AlwaysWrite$,
+    $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 (m = (\_, Out) or c = Ref) => w' = AlwaysWrite$,
+    $(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$,
 
-    $types, vals, mu, m, c tcorrect v : cl r', w' cr -> cl r, w cr$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ function pointer tags correctness],
-
-    $types, vals, mu, m, c tcorrect lambda : lambda space overline(t) -> lambda space overline(t)$,
+    $sigma, mu, m, c tcorrect v : r' space w' () -> r space w ()$,
   )
 ))
 
@@ -501,10 +541,10 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ ref assignment tags correctness],
 
-    $types, vals, mu, m, c_r tcorrect v : t -> t'$,
+    $sigma, mu, m, c_r tcorrect v : t -> t'$,
 
     // TODO: FIXME: which tag translations are correct ?? <- only assignee?
-    $types, vals, mu, m, c tcorrect rf space v : rf c' space t -> rf c_r space t'$,
+    $sigma, mu, m, c tcorrect rf c_r space v : rf c' space t -> rf c_r space t'$,
   )
 ))
 
@@ -515,13 +555,24 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ tuple assignmenttags correctness],
 
-    $types, vals, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
+    $sigma, mu, m, c tcorrect v_1 : t_1 -> t'_1$,
 
     $...$,
 
-    $types, vals, mu, m, c tcorrect v_n : t_n -> t'_n$,
+    $sigma, mu, m, c tcorrect v_n : t_n -> t'_n$,
 
-    $types, vals, mu, m, c tcorrect [v_1, ... v_n] : [t_1, ..., t_n] -> [t'_1, ... 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)$,
   )
 ))
 
@@ -529,8 +580,6 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
 === Value Construction
 
-// TODO: FIXME:add ref / copy modes correctness check
-
 #let new = `new`
 
 #align(center, prooftree(
@@ -539,7 +588,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     name: [ new $0$ value],
 
     // TODO: check that access is what required ??
-    $cl 0, mu cr xarrowSquiggly(cl r\, w cr)_new cl 0, mu cr$,
+    $cl 0, mu cr xarrowSquiggly(space)_new cl 0, mu cr$,
   )
 ))
 
@@ -549,7 +598,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     name: [ new $\#$ value],
 
     // TODO: check that access is what required ??
-    $cl \#, mu cr xarrowSquiggly(cl r\, w cr)_new cl \#, mu cr$,
+    $cl \#, mu cr xarrowSquiggly(space)_new cl \#, mu cr$,
   )
 ))
 
@@ -558,7 +607,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new $bot$ value],
 
-    $cl bot, mu cr xarrowSquiggly(cl r\, w cr)_new cl bot, mu cr$,
+    $cl bot, mu cr xarrowSquiggly(space)_new cl bot, mu cr$,
   )
 ))
 
@@ -576,10 +625,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new reference ref value],
 
-    // TODO: FIXME: recursive copy ?? (what heppens if ref field has copy substructure ??)
-    // frbidden ??
-
-    $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
+    $cl rf Ref l, mu cr xarrowSquiggly(space)_new cl rf Ref l, mu cr$,
   )
 ))
 
@@ -588,11 +634,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new reference copy value],
 
-    $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
+    $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 l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
+    $cl rf Copy l, mu cr xarrowSquiggly(space)_new cl rf Copy l', mu_a cr$,
   )
 ))
 
@@ -601,11 +647,11 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ new tuple value],
 
-    $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
+    $cl v_1, mu_0 cr xarrowSquiggly(space)_new cl lambda v'_1, mu_1 cr$,
     $...$,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
+    $cl v_n, mu_(n - 1) cr xarrowSquiggly(space)_new cl lambda v'_n, mu_n cr$,
 
-    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_new cl [v'_1, ... v'_n], mu_n cr$,
+    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly(space)_new cl [v'_1, ... v'_n], mu_n cr$,
   )
 ))
 
@@ -639,7 +685,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
 
     $isPossibleWrite mode$, // NOTE: weak requirement: may write
     $not isCopy mode$,
-    $mode = (\_, not Out)$,
+    $not isOut mode$,
 
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
@@ -658,7 +704,7 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
     $mu stretch(=>)^args_sigma gamma$,
 
     $isAlwaysWrite mode$, // NOTE: strong requirement: should write
-    $mode = (\_, not Out)$,
+    $isOut mode$,
 
     $isCorrect_(cl sigma, mu cr) (mode, x)$,
 
@@ -770,11 +816,11 @@ $ 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, sigma teval p eqmu 0$,
 
-    $cl types, vals, mu cr
+    $cl sigma, mu, l cr
      xarrow("READ" p)
-     cl types, vals, mu cr$,
+     cl sigma, mu, l cr$,
   )
 ))
 
@@ -785,14 +831,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ WRITE $x$],
 
-    $types ttype p : cl r, w cr$,
-    $w = MaybeWrite or w = AlwaysWrite$,
-    $p arrpath x$,
+    $sigma temode p -> cr r space w cl$,
+
+    $w == MaybeWrite or w == AlwaysWrite$,
+
+    $x tpath p$,
+
     $mu[x] xarrowSquiggly(p)_write v$,
 
-    $cl types, vals, mu cr
+    $cl sigma, mu cr
      xarrow("WRITE" p)
-     cl types, vals, mu[x <- v] cr$,
+     cl sigma, mu[x <- v] cr$,
   )
 ))
 
@@ -803,17 +852,17 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ $s \; t$],
 
-    $cl types, vals, mu cr
+    $cl sigma, mu cr
      stretch(->)^s
-     cl types_s, vals_s, mu_s cr$,
+     cl sigma_s, mu_s cr$,
 
-    $cl types_s, vals_s, mu_s cr
+    $cl sigma, mu cr
      stretch(->)^t
-     cl types_t, vals_t, mu_t cr$,
+     cl sigma_t, mu_t cr$,
 
-    $cl types, vals, mu, cr
+    $cl sigma, mu, cr
      xarrow(s \; t)
-     cl types_t, vals_t, mu_t cr$,
+     cl sigma_t, mu_t cr$,
   )
 ))
 
@@ -827,22 +876,21 @@ $ vals in envv, types in envt, space mu in mem, space m in mode,
   rule(
     name: [ $s | t$],
 
-    $cl types, vals, mu cr
+    $cl sigma, mu, l cr
      stretch(->)^s
-     cl types_s, vals_s, mu_s cr$,
+     cl sigma_s, mu_s, l_s cr$,
 
-    $cl types, vals, mu cr
+    $cl sigma, mu, l cr
      stretch(->)^t
-     cl types_t, vals_t, mu_t cr$,
+     cl sigma_t, mu_t, l_t cr$,
 
-    $types_s = types_t$,
-    $vals_s = vals_t$,
+    $sigma_s = sigma_t$,
     $mu' = combine(mu_s, mu_t)$,
 
     // TODO changes ?? two ways ??
-    $cl types, vals, mu cr
+    $cl sigma, mu cr
      xarrow(s | t)
-     cl types_t, vals_t, mu' cr$,
+     cl sigma_t, mu' cr$,
   )
 ))