diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 006a42a..1b5740e 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -21,7 +21,7 @@ struct
   type atype = UnitT of read_cap * write_cap
              | RefT of copy_cap * atype
              | TupleT of atype list
-             | FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)
+             | FunT of data (* declaration id for ease of impl (?) *)
 
   type mtype = mode * atype
 
@@ -30,8 +30,7 @@ struct
             (* | RefE *)
             | TupleE of expr list
 
-  type stmt = SkipS
-            | CallS of path * expr list
+  type stmt = CallS of path * expr list
             | WriteS of path
             | ReadS of path
             | SeqS of stmt * stmt
@@ -53,22 +52,20 @@ struct
   (* exception Incompatible_path_and_mem *)
   (* exception Incompatible_path_and_type_for_tag *)
   exception Typing_error of string
-  exception Eval_error of string
-  exception Cant_fold3_error
 
   (* value model & memory model *)
 
   type deepvalue = ZeroDV
                  | SmthDV
                  | BotDV
-                 | FunDV of ((* data list * *) stmt) list
+                 | FunDV of (* data list * *) stmt
                  | RefDV of deepvalue
                  | TupleDV of deepvalue list
 
   type value = ZeroV
              | SmthV
              | BotV
-             | FunV of ((* data list * *) stmt) list
+             | FunV of (* data list * *) stmt
              | RefV of memid
              | TupleV of value list
 
@@ -76,31 +73,19 @@ struct
 
   (* --- *)
 
-  type mem = value list * memid (* NOTE: memory and first free elem *)
+  type mem = (memid * value) list * memid (* NOTE: memory and first free elem *)
   type types = (data * atype) list
   type vals = (data * memid) list
   type state = mem * types * vals
 
   (* --- *)
 
-  (* - utils *)
-
-  let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
-   | _ :: xs, 0 -> y :: xs
-   | x :: xs, _ -> x :: list_replace xs (id - 1) y
-   | [], _ -> raise Not_found
-
-  (* NOTE: old variant with assoc array *)
-  (* let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem) *)
-  (* let mem_add (mem : mem) (v : value) : mem * memid = *)
-    (* (((snd mem, v) :: fst mem, snd mem + 1), snd mem) *)
-  (* let mem_set (mem : mem) (id : memid) (v : value) : mem = *)
-    (* ((id, v) :: fst mem, snd mem) *)
-  let mem_get (mem : mem) (id : memid) : value = List.nth (fst mem) id
+  (* TODO: FIXME: use list_replace for memory instead ?? *)
+  let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem)
   let mem_add (mem : mem) (v : value) : mem * memid =
-    ((v :: fst mem, snd mem + 1), snd mem)
+    (((snd mem, v) :: fst mem, snd mem + 1), snd mem)
   let mem_set (mem : mem) (id : memid) (v : value) : mem =
-    (list_replace (fst mem) id v, snd mem)
+    ((id, v) :: fst mem, snd mem)
 
   let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
     | ZeroV -> ZeroDV
@@ -140,11 +125,12 @@ struct
 
   (* --- eval rules --- *)
 
-  (* TODO: FIXME: check if this foldl or foldr *)
-  let rec list_foldl3 f (acc : 'a) (xs : 'b list) (ys : 'c list) (zs : 'd list) : 'a = match xs, ys, zs with
-    | x :: xs, y :: ys, z :: zs -> list_foldl3 f (f acc x y z) xs ys zs 
-    | [], [], [] -> acc
-    | _, _, _ -> raise Cant_fold3_error
+  (* - utils *)
+
+  let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
+   | _ :: xs, 0 -> y :: xs
+   | x :: xs, _ -> x :: list_replace xs (id - 1) y
+   | [], _ -> raise Not_found
 
   (* - value construction *)
 
@@ -182,54 +168,17 @@ struct
     if is_trivial_v u && is_trivial_v v
     then (if u == v then u else BotV)
     else match u, v with
-      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts) 
+      (* TODO: FIXME: combining semanticsfor funcitons statements *)
+      | FunV s, FunV t  -> if s == t then u else raise @@ Typing_error "valcomb: fun"
       | RefV a, RefV b -> if a == b then u else raise @@ Typing_error "valcomb: ref"
       | TupleV us, TupleV vs -> TupleV (List.map2 valcomb us vs)
-      | _, _ -> raise @@ Typing_error "valcomb"
+      | _, _ ->  raise @@ Typing_error "valcomb"
 
-  let rec memcomb (m : mem) (n : mem) : mem =
-    if snd m != snd n
-    then raise @@ Typing_error "memcomb"
-    else (List.map2 valcomb (fst m) (fst n), snd m)
-
-  (* - expression evaluation *)
-
-  let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
-    | UnitE -> ZeroV
-    | PathE p -> pathval mem vals p
-    | TupleE es -> TupleV (List.map (exprval mem vals) es)
-
-  (* - expression typing *)
-
-  let rec exprtype (types : types) (e : expr) : atype = match e with
-    | UnitE -> UnitT (Rd, NeverWr)
-    | PathE p -> pathtype types p
-    | TupleE es -> TupleT (List.map (exprtype types) es)
-
-  (* - context initialization *)
-
-  (* let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value = match t, v with *)
-  
-  (* TODO: check new in vars *)
-  let add_decl (state : state) (x : data) (d : decl) : state =
-    match state with (mem, types, vals) -> match d with
-    | VarD (t, e) -> let v = exprval mem vals e in
-                     let (mem', v') = valcopy mem v t in
-                     let (mem'', id) = mem_add mem' v' in
-                     (mem'', (x, t) :: types, (x, id) :: vals)
-    | FunD (ts, s)  -> let (mem', id) = mem_add mem (FunV [s]) in
-                       (mem', (x, FunT ts) :: types, (x, id) :: vals)
-
-  let empty_state : state = (([], 0), [], [])
-
-  (* TODO: better way ??? *)
-  let globals_min_id : data = 1000
-
-  let prog_init (prog : prog) : state =
-    match prog with (decls, _) -> fst @@ List.fold_left (* TODO: FIXME: check x's order *)
-                                    (fun (st, x) d -> (add_decl st x d, x + 1))
-                                    (empty_state, globals_min_id)
-                                    decls
+  (* TODO: func for list memory, not assoc list *)
+  (* let rec memcomb (m : mem) (n : mem) : mem = *)
+    (* if snd m != snd n *)
+    (* then raise @@ Typing_error "memcomb" *)
+    (* else (List.map2 valcomb (fst m) (fst n), snd m) *)
 
   (* - call values spoil *)
 
@@ -239,7 +188,7 @@ struct
                       (c : copy_cap) : bool =
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
-    (snd m != Out || w == AlwaysWr) &&
+    (o != Out || w == AlwaysWr) &&
     (* TODO: check *)
     ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
     is_trivial_v v
@@ -247,161 +196,262 @@ struct
   let rec valspoil (mem : mem) (v : value) (t : atype)
                    (u : atype) (m : mode) (c : copy_cap)
                    : mem * value = match t, u, v with
-    | UnitT (r, w), UnitT (r', w'), _ ->
-      if not @@ is_trivial_v v
-        then raise @@ Typing_error "valspoil: unit, not trivial"
-      else if not @@ is_correct_tags v r w r' w' m c
-        then raise @@ Typing_error "valspoil: unit, not correct"
-      else if snd m == NOut && c == Rf && (w == AlwaysWr || w == MayWr)
-        then (mem, BotV)
-      else if snd m == Out && w == AlwaysWr
-        then (mem, ZeroV)
-      else (mem, v)
+    | UnitT (r, w), UnitT (r', w'), _ -> (* TODO FIXME *) raise Not_found
     | FunT ts, FunT us, FunV _ -> if ts == us then (mem, v) else raise @@ Typing_error "valspoil: fun"
     | RefT (ct, t), RefT (cu, u), RefV id ->
       let (mem', v') = valspoil mem (mem_get mem id) t u m ct in
       (mem_set mem id v', RefV id)
-    | TupleT ts, TupleT us, TupleV vs ->
-        let folder = fun (mem, vs') t u v ->
-          let (mem', v') = valspoil mem v t u m c in (mem', v' :: vs') in
-        let (mem', vs') = list_foldl3 folder (mem, []) ts us vs in
-        (mem', TupleV vs')
+    | TupleT ts, TupleT us, TupleV vs -> (* TODO FIXME *) raise Not_found
     | _, _, _ ->  raise @@ Typing_error "valspoil"
 
-  (* full spoil *)
+(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
-  let rec argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
-    match state with (mem, types, vals) ->
-    let x = pathvar p in
-    let id = List.assoc x vals in
-    let b = pathval mem vals p in
-    let t' = pathtype types p in
-    let (mem', b') = valspoil mem b t t' m Rf in
-    let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in
-    mem_set mem'' id v''
+  (* let rec argsspoil (* full spoil *) *)
 
-  let rec argsspoile (state : state) (m : mode) (t : atype) (e : expr) : mem =
-    match state with (mem, types, vals) -> match e, t with
-      | UnitE, UnitT _ -> mem
-      | PathE p, t -> argsspoilp state m t p
-      | TupleE es, TupleT ts -> List.fold_left2
-                                  (fun mem' t' e' -> argsspoile (mem', types, vals) m t' e')
-                                  mem ts es
-      | _, _ ->  raise @@ Typing_error "valspoile"
+  (* --- *)
 
-  (* - funciton argument addition *)
+  let rec list_zip_with f xs ys = match xs, ys with (* TODO: alternative from stdlib *)
+    | x :: xs, y :: ys -> f x y :: list_zip_with f xs ys 
+    | _, _ -> []
 
-  let addarg (state : state) (x : data) (t : atype) (e : expr) : state =
-    match state with (mem, types, vals) ->
-    let v = exprval mem vals e in
-    (* let t' = pathtype types p in *)
-    let (mem', v') = valcopy mem v t in
-    let (mem'', id) = mem_add mem' v in
-    (mem', (x, t) :: types, (x, id) :: vals)
+  (* --- combination --- *)
 
-  (* - function evaluation *)
+  let value_combine (left : value) (right : value) : value = match left, right with
+    | UnitV, UnitV -> UnitV
+    | BotV, BotV -> BotV
+    | _, _ -> UndefV (* NOTE: should be expanded in relational interpreter to not use ineq (?) *)
 
-  (* NOTE: not needed due to performed optimization in stmt_eval *)
-  (* let func_eval (mem : mem) (vals : vals) (s : stmt) (ts : mtype list) (es : expr list) = *)
+  let memory_combine (left : value list) (right : value list) : value list =
+    list_zip_with value_combine left right
 
-  (* - statement evaluation *)
+  let state_combine (left : state) (right : state) : state = match left, right with
+    (lenv, lmem, lmem_len, lvisited), (renv, rmem, rmem_len, rvisited) ->
+    if lenv != renv || lmem_len != rmem_len then raise Incompatible_states
+    else (lenv, memory_combine lmem rmem, lmem_len, List.append lvisited rvisited)
+    (* TODO: union visited lists instead ? *)
 
-  let rec stmt_eval (state : state) (s : stmt) : state =
-    match state with (mem, types, vals) -> match s with
-    (* TODO: FIXME: Add memoisation *)
-    | SkipS -> state
-    | CallS (f, es) -> let v = pathval mem vals f in
-                       let t = pathtype types f in
-                       let types' : types = [] in
-                       let vals' : vals = [] in
-                       (match v, t with
-                          | FunV (* xs, *) fstmts (* ) *), FunT ts ->
-                            (* TODO: memoisation of the called functions *)
-                            let (state_with_args, _) = List.fold_left2 (* TODO: FIXME: check x's order *)
-                              (fun (st, x) (m, t) p -> (addarg st x t p, x + 1))
-                              ((mem, types', vals'), 0) ts es in
-                            (* NOTE: same x's, so can use same args for all the statements *)
-                            let _states_evaled = List.map (stmt_eval state_with_args) fstmts in
-                            let mem_spoiled = List.fold_left2
-                              (fun mem (m, t) e -> argsspoile (mem, types, vals) m t e)
-                              mem ts es in
-                            (mem_spoiled, types, vals)
-                          | _, _ -> raise @@ Eval_error "call: function")
-    | WriteS p -> (match pathtype types p with
-                     | UnitT (_, w) ->
-                       if w == NeverWr
-                       then raise @@ Eval_error "write: write tag"
-                       else let x = pathvar p in
-                            let id = List.assoc x vals in
-                            let (mem', v') = valupd mem (mem_get mem id) p ZeroV in
-                            (mem_set mem' id v', types, vals)
-                     | _ -> raise @@ Eval_error "write: type")
-    | ReadS p -> if pathval mem vals p != ZeroV
-                 then raise @@ Eval_error "read"
-                 else state
-    | SeqS (sl, sr) -> let statel = stmt_eval state sl in
-                       stmt_eval statel sr
-    | ChoiceS (sl, sr) -> let statel = stmt_eval state sl in
-                          let stater = stmt_eval state sr in
-                          match statel with (meml, typesl, valsl) ->
-                          match stater with (memr, typesr, valsr) ->
-                          if typesl != typesr || valsl != valsr
-                          then raise @@ Eval_error "choice"
-                          else (memcomb meml memr, typesl, valsl)
+  (* --- tag accessors --- *)
 
- (* --- program execution --- *)
+  let is_read (tag : tag) : bool = match tag with
+    | (Rd, _, _, _, _) -> true
+    | _ -> false
 
- let prog_eval (prog : prog) : state =
-   match prog with (decls, s) ->
-   let init_state = prog_init prog in
-   stmt_eval init_state s
+  let is_always_write (tag : tag) : bool = match tag with
+    | (_, AlwaysWr, _, _, _) -> true
+    | _ -> false
 
- let prog_eval_noret (prog : prog) : unit =
-   ignore @@ prog_eval prog
+  let is_may_write (tag : tag) : bool = match tag with
+    | (_, AlwaysWr, _, _, _) -> true
+    | (_, MayWr, _, _, _) -> true
+    | _ -> false
 
-  (* --- tests --- *)
+  let is_never_write (tag : tag) : bool = match tag with
+    | (_, NeverWr, _, _, _) -> true
+    | _ -> false
 
-  (* - tests without functions *)
+  let is_copy (tag : tag) : bool = match tag with
+    | (_, _, Cp, _, _) -> true
+    | _ -> false
 
-  let%expect_test "empty" =
-    prog_eval_noret ([], SkipS);
-    Printf.printf "done!";
-    [%expect {| done! |}]
+  let is_in (tag : tag) : bool = match tag with
+    | (_, _, _, In, _) -> true
+    | _ -> false
 
-  let%expect_test "simple var" =
-    prog_eval_noret ([VarD (UnitT (Rd, MayWr), UnitE)], ReadS (VarP globals_min_id));
-    Printf.printf "done!";
-    [%expect {| done! |}]
+  let is_out (tag : tag) : bool = match tag with
+    | (_, _, _, _, Out) -> true
+    | _ -> false
 
-  let%expect_test "simple var, no read" =
-    try(prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE)], ReadS (VarP globals_min_id));
-         [%expect.unreachable]);
-    with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| read |}]
+  (* --- *)
 
-  (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
+  let rec list_replace xs id value = match (xs, id) with
+   | (_x :: xs, 0) -> value :: xs
+   | (x :: xs, _n) -> x :: list_replace xs (id - 1) value 
+   | ([], _) -> raise Not_found
 
-  (* --- tests --- *)
+  let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
 
-  (* let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut) *)
-  (* let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut) *)
-  (* let ri_value : tag = (Rd, NeverWr, Cp, In, NOut) *)
-  (* let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut) *)
-  (* let mwi_value : tag = (NRd, MayWr, Cp, In, NOut) *)
-  (* let i_value : tag = (NRd, NeverWr, Cp, In, NOut) *)
-  (* let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut) *)
-  (* let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut) *)
-  (* let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut) *)
-  (* let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut) *)
-  (* let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut) *)
-  (* let i_ref : tag = (NRd, NeverWr, Rf, In, NOut) *)
+  (* --- path accessors --- *)
+
+  let rec pathtype (t : argtype) (p : path) : argtype = match t, p with
+    | t, VarP x -> t
+    | RefT (tag, t), DerefP p -> pathtype t p
+    | TupleT ts, AccessP (p, n) -> pathtype (List.nth ts n) p
+    | _, _ -> raise Incompatible_path_and_type
+
+  let rec pathmem (m : argmem) (p : path) : data = match m, p with
+    | VarM m, VarP x -> m
+    | RefM m, DerefP p -> pathmem m p
+    | TupleM ms, AccessP (p, n) -> pathmem (List.nth ms n) p
+    | _, _ -> raise Incompatible_path_and_mem
+
+  let rec pathtag (t : argtype) (p : path) : tag = match t, p with
+    | RefT (tag, t), VarP x -> tag
+    | RefT (tag, t), DerefP p -> pathtag t p
+    | TupleT ts, AccessP (p, n) -> pathtag (List.nth ts n) p
+    | _, _ -> raise Incompatible_path_and_type_for_tag
+
+  let rec pathvar (p : path) : data = match p with
+    | VarP x -> x
+    | DerefP p -> pathvar p
+    | AccessP (p, n) -> pathvar p
+
+  let typeof (env : env) (p : path) : argtype = pathtype (snd (List.assoc (pathvar p) env)) p
+  let accessmem (env : env) (p : path) : data = pathmem (fst (List.assoc (pathvar p) env)) p
+  let argtag (env : env) (p : path) : tag = pathtag (snd (List.assoc (pathvar p) env)) p
+  (* TODO: check indices *)
+  let access_get (env : env) (mem : value list) (mem_len : data) (p : path) : value = List.nth mem @@ inv_id mem_len @@ accessmem env p
+  let access_set (env : env) (mem : value list) (mem_len : data) (p : path) (value : value) : value list = list_replace mem (inv_id mem_len @@ accessmem env p) value
+
+  (* --- *)
+
+  let visited_add (state : state) (id : data) : state =
+    match state with (env, mem, mem_len, visited) -> (env, mem, mem_len, id :: visited)
+
+  let visited_check (state : state) (id : data) : bool =
+    match state with (_, _, _, visited) -> List.exists (fun i -> i == id) visited
+
+  (* --- *)
+
+  (* TODO: replacewith more useful path versions *)
+  let env_get (state : state) (id : data) : (argmem * argtype) =
+    match state with (env, _mem, _mem_len, _visited) -> List.assoc id env
+
+  let env_add (state : state) (id : data) (argmem : argmem) (argtype : argtype) : state = match state with
+    (env, mem, mem_len, visited) -> let env = (id, (argmem, argtype)) :: env in
+                           (env, mem, mem_len, visited)
+
+  let mem_get (state : state) (p : path) : value = match state with
+    (env, mem, mem_len, _visited) -> access_get env mem mem_len p
+
+  let mem_set (state : state) (p : path) (value : value) : state = match state with
+    (env, mem, mem_len, visited) -> (env, access_set env mem mem_len p value, mem_len, visited)
+
+  let mem_add (state : state) (value : value) : state = match state with
+    (env, mem, mem_len, visited) -> let mem = value :: mem in (env, mem, mem_len + 1, visited)
+
+  let mem_check (state : state) (p : path) : unit =
+    (* TODO: use path in error instead *)
+    if mem_get state p == BotV then raise @@ Incorrect_memory_access (pathvar p) else ()
+
+  (* --- *)
+
+  let arg_to_value (state : state) (arg : arg) : value = match arg with
+    | RValue -> UnitV
+    | LValue p -> mem_get state p
+  (* TODO: FIXME: args as argmem ?? *)
+
+  let st_mem_len (state : state) : int =
+    match state with (_, _, mem_len, _) -> mem_len
+
+  let check_tag_correct (tag : tag) (id : data) : unit =
+    if (* (is_in tag && not (is_read tag)) || *) (* TODO: required ?? *)
+       is_out tag > is_always_write tag ||
+       is_read tag > is_in tag
+       (* || is_copy tag && is_out tag *) (* ?? *)
+    then raise @@ Invalid_argument_tag id
+    else ()
+
+  let st_add_arg (state : state) (state_before : state)
+      (id : data) (arg_tag : tag) (arg : arg) : state =
+    check_tag_correct arg_tag id;
+    if is_copy arg_tag
+    then let state = mem_add state (arg_to_value state_before arg) in
+         env_add state id arg_tag (st_mem_len state - 1)
+    else match arg with
+      | RValue -> raise @@ Ref_rvalue_argument id (* TODO: allow later ?? *)
+      | LValue arg -> let (parent_tag, mem_id) = env_get state_before arg in
+                      if is_may_write arg_tag > is_always_write parent_tag (* TODO: FIXME: not updated semantics ?? *)
+                      then raise @@ Incorrect_const_cast id
+                      else if is_read arg_tag
+                      then env_add state id arg_tag mem_id
+                      (* TODO: parent state is spoiled, check that this is correct *)
+                      else let state_ext = env_add state id arg_tag mem_id in
+                           mem_set state_ext id BotV
+
+  (* TODO: FIXME: not enough tests on incorrect const cast (passed without ref or out check) *)
+  (* TODO; FIXME: forbid duplicates,  collect lists of all spoils & checks ? *)
+  let st_spoil_by_args (state : state) (arg_tags : tag list) (args : data list) : state =
+    match state with (env, mem, mem_len, _visited) ->
+    let state_before = state in
+    let spoil_folder (state : state) (tag : tag) (id : data) : state =
+      let parent_tag = fst (env_get state id) in
+      (* NOTE: replaced with later condition *)
+      (* if is_write tag > is_write parent_tag && (not (is_copy tag) || is_out tag) then raise @@ Incorrect_const_cast idi else *)
+      let state = if is_read tag then (mem_check state_before id; state) else state (* NOTE: state override *)
+      in if is_never_write tag then state (* TODO: FIXME: check *)
+      else match is_out tag with
+        | true -> if not @@ is_always_write parent_tag then raise @@ Incorrect_const_cast id
+                  else mem_set state id UnitV
+        | false -> if is_copy tag then state
+                   else if not @@ is_may_write parent_tag then raise @@ Incorrect_const_cast id (* TODO: check that may modifier correct *)
+                   else mem_set state id BotV
+    in List.fold_left2 spoil_folder state arg_tags args
+
+  let list_drop n xs = List.of_seq @@ Seq.drop n @@ List.to_seq xs
+
+  let rec eval_stmt (state : state) (prog : fun_decl list) (stmt : stmt) : state =
+    match stmt with
+      | Call (f_id, args) -> let (arg_tags, _) as f_decl = List.nth prog f_id in
+                             let state_with_visited = if visited_check state f_id
+                                          then state
+                                          else let new_state_with_visited = visited_add state f_id in
+                                               let state_fun = eval_fun new_state_with_visited prog f_decl (List.map (fun arg -> LValue arg) args) in
+                                               (* NOTE: now memory in function is not spoiled  *)
+                                               state_fun
+                             in st_spoil_by_args state_with_visited arg_tags args
+      | Read id -> mem_check state id; state
+      | Write id -> if is_may_write @@ fst @@ env_get state id
+                    then mem_set state id UnitV
+                    else raise @@ Incorrect_const_cast id
+      | Choice (xs, ys) -> let state_x = eval_body state prog xs in
+                           let state_y = eval_body state prog ys in
+                           state_combine state_x state_y
+                           (* TODO: FIXME: additional may write / always write checks ?? *)
+
+  and eval_body (state : state) (prog : fun_decl list) (body : body) : state =
+    List.fold_left (fun state stmt -> eval_stmt state prog stmt) state body
+
+  and eval_fun (state : state) (prog : fun_decl list) (decl : fun_decl) (args : arg list) : state =
+    match decl with (arg_tags, body) ->
+    match state with (env_before, mem_before, len_before, visited_before) as state_before ->
+    let state : state = ([], mem_before, len_before, visited_before) in
+    let (state, _) = List.fold_left2 (fun (state, id) arg_tag arg -> (st_add_arg state state_before id arg_tag arg, id + 1))
+                                     (state, 0) arg_tags args in
+    let state = eval_body state prog body in
+    match state with (_env, mem, len, visited) ->
+    (env_before, mem_before, len_before, visited)
+    (* (env_before, list_drop (len - len_before) mem, len_before, visited) (* TODO: save some assignments ?? *) *)
+
+  and eval_fun_empty_args (state : state) (prog : fun_decl list) (decl : fun_decl) : state =
+    match decl with (arg_tags, _) ->
+    let args = List.map (fun _ -> RValue) arg_tags in
+    eval_fun state prog decl args
+
+  let empty_state : state = ([], [], 0, [])
+
+  let eval_prog ((prog, main_decl) : prog) = ignore @@ eval_fun_empty_args empty_state prog main_decl
+
+  (* tests *)
+
+  let rwi_value : tag = (Rd, AlwaysWr, Cp, In, NOut)
+  let rmwi_value : tag = (Rd, MayWr, Cp, In, NOut)
+  let ri_value : tag = (Rd, NeverWr, Cp, In, NOut)
+  let wi_value : tag = (NRd, AlwaysWr, Cp, In, NOut)
+  let mwi_value : tag = (NRd, MayWr, Cp, In, NOut)
+  let i_value : tag = (NRd, NeverWr, Cp, In, NOut)
+  let rwi_ref : tag = (Rd, AlwaysWr, Rf, In, NOut)
+  let rmwi_ref : tag = (Rd, MayWr, Rf, In, NOut)
+  let ri_ref : tag = (Rd, NeverWr, Rf, In, NOut)
+  let wi_ref : tag = (NRd, AlwaysWr, Rf, In, NOut)
+  let mwi_ref : tag = (NRd, MayWr, Rf, In, NOut)
+  let i_ref : tag = (NRd, NeverWr, Rf, In, NOut)
 
   (* >> tests without functions *)
 
-  (* let%expect_test "empty" = *)
-    (* eval_prog ([], ([], [])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
+  let%expect_test "empty" =
+    eval_prog ([], ([], []));
+    Printf.printf "done!";
+    [%expect {| done! |}]
 
   (* let%expect_test "ref param in main failure" = *)
     (* try (eval_prog ([], ([i_ref], [])); *)
diff --git a/model_with_structures/dune b/model_with_structures/dune
index 489258f..eae17b8 100644
--- a/model_with_structures/dune
+++ b/model_with_structures/dune
@@ -13,52 +13,52 @@
  (preprocess
   (pps GT.ppx GT.ppx_all ppx_expect ppx_inline_test)))
 
-; (library
-;  (name tests_st)
-;  (modules tests)
-;  (flags (-rectypes))
-;  (libraries synthesizer_st tests_f_st)
-;  (inline_tests)
-;  (wrapped false)
-;  (preprocess
-;   (pps ppx_expect ppx_inline_test)))
+(library
+ (name tests_st)
+ (modules tests)
+ (flags (-rectypes))
+ (libraries synthesizer_st tests_f_st)
+ (inline_tests)
+ (wrapped false)
+ (preprocess
+  (pps ppx_expect ppx_inline_test)))
 
-; (library
-;  (name tests_f_st)
-;  (modules tests_f)
-;  (flags (-rectypes))
-;  (libraries OCanren OCanren.tester synthesizer_st)
-;  (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
-;  (wrapped false)
-;  (preprocess
-;   (pps
-;    OCanren-ppx.ppx_repr
-;    OCanren-ppx.ppx_deriving_reify
-;    OCanren-ppx.ppx_fresh
-;    GT.ppx
-;    GT.ppx_all
-;    OCanren-ppx.ppx_distrib
-;    --
-;    -pp
-;    camlp5/pp5+gt+plugins+ocanren+dump.exe)))
+(library
+ (name tests_f_st)
+ (modules tests_f)
+ (flags (-rectypes))
+ (libraries OCanren OCanren.tester synthesizer_st)
+ (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
+ (wrapped false)
+ (preprocess
+  (pps
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_deriving_reify
+   OCanren-ppx.ppx_fresh
+   GT.ppx
+   GT.ppx_all
+   OCanren-ppx.ppx_distrib
+   --
+   -pp
+   camlp5/pp5+gt+plugins+ocanren+dump.exe)))
 
-; (library
-;  (name synthesizer_st)
-;  (modules synthesizer)
-;  (flags
-;   ; (-dsource)
-;   (:standard -rectypes))
-;  (libraries OCanren OCanren.tester)
-;  (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
-;  (wrapped false)
-;  (preprocess
-;   (pps
-;    OCanren-ppx.ppx_repr
-;    OCanren-ppx.ppx_deriving_reify
-;    OCanren-ppx.ppx_fresh
-;    GT.ppx
-;    GT.ppx_all
-;    OCanren-ppx.ppx_distrib
-;    --
-;    -pp
-;    camlp5/pp5+gt+plugins+ocanren+dump.exe)))
+(library
+ (name synthesizer_st)
+ (modules synthesizer)
+ (flags
+  ; (-dsource)
+  (:standard -rectypes))
+ (libraries OCanren OCanren.tester)
+ (preprocessor_deps ../camlp5/pp5+gt+plugins+ocanren+dump.exe)
+ (wrapped false)
+ (preprocess
+  (pps
+   OCanren-ppx.ppx_repr
+   OCanren-ppx.ppx_deriving_reify
+   OCanren-ppx.ppx_fresh
+   GT.ppx
+   GT.ppx_all
+   OCanren-ppx.ppx_distrib
+   --
+   -pp
+   camlp5/pp5+gt+plugins+ocanren+dump.exe)))
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index 3742b24..3449afc 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -120,12 +120,11 @@
   Prod(
     `stmt`,
     {
-      Or[`SKIP`][do nothing]
       Or[`CALL` $path expr+$][call function]
       Or[`WRITE` $path$][write to variable]
       Or[`READ` $path$][read from variable]
-      Or[$stmt ; stmt$][sequence of two statements]
-      Or[$stmt | stmt$][choice between the statements]
+      Or[$stmt ; stmt$][control flow operator, xecution ]
+      Or[$stmt | stmt$][control flow operator, excution of one statements]
     }
   ),
   Prod(
@@ -156,7 +155,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 space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
+      Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
       Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[deepValue+]$][tuple value] // `Prod`
     }
@@ -167,7 +166,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 space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
+      Or[$lambda space overline(x) stmt$][function pointer value] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
@@ -201,7 +200,7 @@ $v in value$ - произвольное значение
 
     $l = #[next] (mu)$,
 
-    $mu xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
+    $cl mu cr xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
   )
 ))
 
@@ -235,7 +234,7 @@ $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(space)_path$
+#let arrpath = $xarrowSquiggly(mu)_path$
 
 #let ttype = $attach(tack.r, br: type)$
 #let tmode = $attach(tack.r, br: mode)$
@@ -481,7 +480,7 @@ $s in stmt, f in X, x in X, a in X$
 
     $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
 
-    $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a 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$,
   )
@@ -586,12 +585,11 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ combine lambda values],
 
+    // TODO: FIXME: how to combine statments in the right way? should check both
+    [*TODO: combining semantics for lambda values (sets?)*],
     $overline(x_1) = overline(x_2)$,
     $s_1 = s_2$,
-    $lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1]
-     plus.o lambda space [overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]
-     = lambda space [overline(x^1_1) space s^1_1, ... overline(x^n_1) space s^n_1,
-                     overline(x^1_2) space s^1_2, ... overline(x^m_2) space s^m_2]$
+    $lambda space overline(x_1) space s_2 plus.o lambda space overline(x_2) space s_2 = lambda$
   )
 ))
 
@@ -642,145 +640,6 @@ $s in stmt, f in X, x in X, a in X$
 
 #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: [ unit value type],
-
-    $vals, mu texpre () eqmu 0$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ path type],
-
-    $vals, mu tval p eqmu v$,
-    $vals, mu texpre p eqmu v$,
-  )
-))
-
-// 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: [ unit value type],
-
-    $types texprt () : cl Read, NotWrite cr$,
-  )
-))
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ path type],
-
-    $types ttype p : t$,
-    $types texprt p : t$,
-  )
-))
-
-// 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]$,
-  )
-))
-
-===  Context Initialization
-
-#let init = `init`
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ add variable declaration],
-
-    // NOTE: expr type expected to ~ match t (maybe except some automaticc modifiers)
-    // expect well typed program
-
-    $vals, mu texpre e eqmu v$,
-    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$, // TODO: FIXME check (required?)
-    $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
-
-    $cl types, vals, mu cr xarrowSquiggly("var" x : t = e)_init cl types[x <- t], vals[x <- l], mu'' cr$
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ add function declaration],
-
-    $mu xarrowSquiggly(lambda space [[x_1, ... x_n] s])_#[add] cl l, mu' cr$,
-
-    $cl types, vals, mu cr
-     xarrowSquiggly("fun" f (x_1 space : space m_1 t_1, ... space x_n space : space m_n t_n) space = space s)_init
-     cl types[f <- lambda space [t_1, ... t_n]], vals[f <- l], mu' cr$
-  )
-))
-
-#h(10pt)
-
 === Call Values Spoil
 
 #let spoil = `spoil`
@@ -894,50 +753,125 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ full spoil for unit expr],
+    name: [ full spoil],
 
-    $mu stretch(=>)^(m space cl r, w cr space ())_(cl vals, types cr) mu$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ full spoil for path expr],
-
-    $p : path$,
     $p arrpath x$,
     $l = vals[x]$,
-    $vals, mu texpre p eqmu b$,
+    $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$,
+    $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'']$,
+    $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: [ full spoil for tuple expr],
+    name: [ path type],
 
-    $e = [e_1, ... e_n]$,
-    $mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
-    $...$,
-    $mu_(n - 1) stretch(=>)^(m space t_n space e_n)_(cl vals, types cr) mu_n$,
-
-    $mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
+    $vals, mu tval p eqmu v$,
+    $vals, mu texpre p eqmu v$,
   )
 ))
 
-#h(10pt)
+#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
 
@@ -946,48 +880,19 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ add argument],
 
-    $vals_#[ctx], mu texpre e eqmu v$,
-    // $types ttype p : t'$, // TODO: not required if there is no check
+
+    $vals, mu tval p eqmu v$,
+    $types ttype p : t'$,
     // TODO: check type compatibility for t and type for path p (?)
     // [*TODO: check t ~ t' in sme way (?)*],
     // <- programs considired to be well-typed
-    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$,
-    $mu' xarrowSquiggly(v')_#[add] cl l, mu'' cr$,
+    $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 e)_(vals_#[ctx])
-     cl types[x <- t], vals[x <- l], mu'' cr$,
-  )
-))
-
-#h(10pt)
-
-=== Function Evaluation
-
-#let tfunceval = $attach(tack.r.double, br: #[func eval])$
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ new reference copy value],
-
-    $types_0 = []$,
-    $vals_0 = []$,
-
-    // NOTE: dashed arrow to fill context
-    $cl types_0, vals_0,  mu_0 cr
-     xarrowDashed(x_1 space t_1 space e_1)_vals
-     cl types', vals_1, mu_1 cr$,
-    $...$,
-    $cl types_(n - 1), vals_(n - 1),  mu_(n - 1) cr
-     xarrowDashed(x_n space t_n space e_n)_vals
-     cl types_n, vals_n, mu_n cr$,
-
-    $cl types_n, vals_n,  mu_n cr
-     xarrow(s)
-     cl types', vals', mu' cr$,
-
-    $cl vals, mu_0 cr tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
+     xarrowDashed(x space t space p)
+     cl types[x <- t], vals[x <- v], mu' cr$,
   )
 ))
 
@@ -998,37 +903,39 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ SKIP],
+    name: [ CALL $f space [p_1, ... p_n]$],
 
-    $cl types, vals, mu cr
-     xarrow("SKIP")
-     cl types, vals, mu cr$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ CALL $f space [e_1, ... e_n]$],
-
-    $vals, mu_0 tval f eqmu lambda [overline(x)_1 space s_1, ... overline(x)_n space s_n]$,
+    $vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
     $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
-    // NOTE: check that all the possible bodies are possible to eval
-    $cl vals, mu_0 cr tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
+    // TODO: add args before statement eval
+
+    $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 vals, mu_0 cr tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] 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
-    $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
+    $gamma_0 = mu$,
+    $gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$,
     $...$,
-    $mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$,
+    $gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$,
 
-    $cl types, vals, mu_0 cr
-     xarrow("CALL" f space [e_1, ... e_n])
-     cl types, vals, mu_n cr$,
+    $cl vals, types, mu, l cr
+     xarrow("CALL" f space [p_1, ... p_n])
+     cl vals, types, gamma_n, l cr$,
   )
 ))
 
@@ -1039,7 +946,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ READ $p$],
 
-    $vals, mu tval p eqmu 0$,
+    $mu, types, vals tval p eqmu 0$,
 
     $cl types, vals, mu cr
      xarrow("READ" p)
@@ -1057,7 +964,7 @@ $s in stmt, f in X, x in X, a in X$
     $types ttype p : cl r, w cr$,
     $w = MaybeWrite or w = AlwaysWrite$,
     $p arrpath x$,
-    $l = vals[x]$,
+    $l = vals(x)$,
     $mu[l] xarrowSquiggly(cl p \, 0 cr)_modify v'$,
 
     $cl types, vals, mu cr
@@ -1081,7 +988,7 @@ $s in stmt, f in X, x in X, a in X$
      stretch(->)^t
      cl types_t, vals_t, mu_t cr$,
 
-    $cl types, vals, mu cr
+    $cl types, vals, mu, cr
      xarrow(s \; t)
      cl types_t, vals_t, mu_t cr$,
   )