diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 1b5740e..006a42a 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 data (* declaration id for ease of impl (?) *)
+             | FunT of (mode * atype) list (* TODO: declaration id for ease of impl / performance instead (?) *)
 
   type mtype = mode * atype
 
@@ -30,7 +30,8 @@ struct
             (* | RefE *)
             | TupleE of expr list
 
-  type stmt = CallS of path * expr list
+  type stmt = SkipS
+            | CallS of path * expr list
             | WriteS of path
             | ReadS of path
             | SeqS of stmt * stmt
@@ -52,20 +53,22 @@ 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
+                 | FunDV of ((* data list * *) stmt) list
                  | RefDV of deepvalue
                  | TupleDV of deepvalue list
 
   type value = ZeroV
              | SmthV
              | BotV
-             | FunV of (* data list * *) stmt
+             | FunV of ((* data list * *) stmt) list
              | RefV of memid
              | TupleV of value list
 
@@ -73,19 +76,31 @@ struct
 
   (* --- *)
 
-  type mem = (memid * value) list * memid (* NOTE: memory and first free elem *)
+  type mem = value list * memid (* NOTE: memory and first free elem *)
   type types = (data * atype) list
   type vals = (data * memid) list
   type state = mem * types * vals
 
   (* --- *)
 
-  (* TODO: FIXME: use list_replace for memory instead ?? *)
-  let mem_get (mem : mem) (id : memid) : value = List.assoc id (fst mem)
+  (* - 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
   let mem_add (mem : mem) (v : value) : mem * memid =
-    (((snd mem, v) :: fst mem, snd mem + 1), 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)
+    (list_replace (fst mem) id v, snd mem)
 
   let rec v_to_deepv (mem : mem) (v : value) : deepvalue = match v with
     | ZeroV -> ZeroDV
@@ -125,12 +140,11 @@ struct
 
   (* --- eval rules --- *)
 
-  (* - 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
+  (* 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
 
   (* - value construction *)
 
@@ -168,17 +182,54 @@ struct
     if is_trivial_v u && is_trivial_v v
     then (if u == v then u else BotV)
     else match u, v with
-      (* TODO: FIXME: combining semanticsfor funcitons statements *)
-      | FunV s, FunV t  -> if s == t then u else raise @@ Typing_error "valcomb: fun"
+      | FunV ustmts, FunV vstmts  -> FunV (ustmts @ vstmts) 
       | 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"
 
-  (* 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) *)
+  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
 
   (* - call values spoil *)
 
@@ -188,7 +239,7 @@ struct
                       (c : copy_cap) : bool =
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
-    (o != Out || w == AlwaysWr) &&
+    (snd m != Out || w == AlwaysWr) &&
     (* TODO: check *)
     ((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr) &&
     is_trivial_v v
@@ -196,262 +247,161 @@ 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'), _ -> (* TODO FIXME *) raise Not_found
+    | 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)
     | 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 -> (* TODO FIXME *) raise Not_found
+    | 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')
     | _, _, _ ->  raise @@ Typing_error "valspoil"
 
-(* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
+  (* full spoil *)
 
-  (* let rec argsspoil (* full spoil *) *)
+  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 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"
 
-  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 
-    | _, _ -> []
+  (* - funciton argument addition *)
 
-  (* --- combination --- *)
+  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)
 
-  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 (?) *)
+  (* - function evaluation *)
 
-  let memory_combine (left : value list) (right : value list) : value list =
-    list_zip_with value_combine left right
+  (* 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 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 ? *)
+  (* - statement evaluation *)
 
-  (* --- tag accessors --- *)
+  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)
 
-  let is_read (tag : tag) : bool = match tag with
-    | (Rd, _, _, _, _) -> true
-    | _ -> false
+ (* --- program execution --- *)
 
-  let is_always_write (tag : tag) : bool = match tag with
-    | (_, AlwaysWr, _, _, _) -> 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_may_write (tag : tag) : bool = match tag with
-    | (_, AlwaysWr, _, _, _) -> true
-    | (_, MayWr, _, _, _) -> true
-    | _ -> false
+ let prog_eval_noret (prog : prog) : unit =
+   ignore @@ prog_eval prog
 
-  let is_never_write (tag : tag) : bool = match tag with
-    | (_, NeverWr, _, _, _) -> true
-    | _ -> false
+  (* --- tests --- *)
 
-  let is_copy (tag : tag) : bool = match tag with
-    | (_, _, Cp, _, _) -> true
-    | _ -> false
+  (* - tests without functions *)
 
-  let is_in (tag : tag) : bool = match tag with
-    | (_, _, _, In, _) -> true
-    | _ -> false
+  let%expect_test "empty" =
+    prog_eval_noret ([], SkipS);
+    Printf.printf "done!";
+    [%expect {| done! |}]
 
-  let is_out (tag : tag) : bool = match tag with
-    | (_, _, _, _, Out) -> 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%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 |}]
 
-  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
+  (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
-  let inv_id (mem_len : int) (id : data) : data = mem_len - id - 1
+  (* --- tests --- *)
 
-  (* --- 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)
+  (* 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 eae17b8..489258f 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 3449afc..3742b24 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -120,11 +120,12 @@
   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$][control flow operator, xecution ]
-      Or[$stmt | stmt$][control flow operator, excution of one statements]
+      Or[$stmt ; stmt$][sequence of two statements]
+      Or[$stmt | stmt$][choice between the statements]
     }
   ),
   Prod(
@@ -155,7 +156,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 overline(x) stmt$][function pointer value] // `Fun`
+      Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
       Or[$rf deepValue$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[deepValue+]$][tuple value] // `Prod`
     }
@@ -166,7 +167,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 overline(x) stmt$][function pointer value] // `Fun`
+      Or[$lambda space (X+ stmt)+$][function pointer value, set of possible values] // `Fun`
       Or[$rf LL$][reference value, contains label of the value in the memory] // `Ref`
       Or[$[value+]$][tuple value] // `Prod`
     }
@@ -200,7 +201,7 @@ $v in value$ - произвольное значение
 
     $l = #[next] (mu)$,
 
-    $cl mu cr xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
+    $mu xarrowSquiggly(v)_#[add] cl l, mu [l <- v] cr$,
   )
 ))
 
@@ -234,7 +235,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(mu)_path$
+#let arrpath = $xarrowSquiggly(space)_path$
 
 #let ttype = $attach(tack.r, br: type)$
 #let tmode = $attach(tack.r, br: mode)$
@@ -480,7 +481,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$,
 
-    $cl mu_v cr xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
+    $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
 
     $cl rf l, mu cr xarrowSquiggly(rf Copy t)_new cl rf l', mu_a cr$,
   )
@@ -585,11 +586,12 @@ $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) space s_2 plus.o lambda space overline(x_2) space s_2 = lambda$
+    $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]$
   )
 ))
 
@@ -640,6 +642,145 @@ $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`
@@ -753,125 +894,50 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ full spoil],
+    name: [ full spoil for unit expr],
 
-    $p arrpath x$,
-    $l = vals[x]$,
-    $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$,
-
-    $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu'[l <- v']$,
+    $mu stretch(=>)^(m space cl r, w cr space ())_(cl vals, types cr) mu$,
   )
 ))
 
 #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: [ path type],
+    name: [ full spoil for path expr],
 
-    $vals, mu tval p eqmu v$,
-    $vals, mu texpre p eqmu v$,
+    $p : path$,
+    $p arrpath x$,
+    $l = vals[x]$,
+    $vals, mu texpre 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$,
+
+    $mu stretch(=>)^(m space t space p)_(cl vals, types cr) mu''[l <- v'']$,
   )
 ))
 
-#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 ??$,
-//   )
-// ))
+#h(10pt)
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ unit value type],
+    name: [ full spoil for tuple expr],
 
-    $vals, mu texpre e_1 eqmu v_1$,
+    $e = [e_1, ... e_n]$,
+    $mu_0 stretch(=>)^(m space t_1 space e_1)_(cl vals, types cr) mu_1$,
     $...$,
-    $vals, mu texpre e_n eqmu v_n$,
-    $vals, mu texpre [e_1, ... e_n] eqmu [v_1, ... v_n]$,
+    $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$,
   )
 ))
 
-
-=== 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]$,
-  )
-))
+#h(10pt)
 
 === Function Argument Addition
 
@@ -880,19 +946,48 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ add argument],
 
-
-    $vals, mu tval p eqmu v$,
-    $types ttype p : t'$,
+    $vals_#[ctx], mu texpre e eqmu v$,
+    // $types ttype p : t'$, // TODO: not required if there is no check
     // 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$,
-
+    $cl v, mu cr xarrowSquiggly(t)_new cl v', mu' cr$,
+    $mu' xarrowSquiggly(v')_#[add] cl l, 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 p)
-     cl types[x <- t], vals[x <- v], 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$,
   )
 ))
 
@@ -903,39 +998,37 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ CALL $f space [p_1, ... p_n]$],
+    name: [ SKIP],
 
-    $vals, mu texpre f eqmu lambda [x_1, ... x_n] space s$,
+    $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]$,
     $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
-    // 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$,
+    // 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$,
     $...$,
-    $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$,
+    $cl vals, mu_0 cr tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] cr$,
 
     // NOTE: thick arrow to "spoil" context
-    $gamma_0 = mu$,
-    $gamma_0 stretch(=>)^(x_1 space m_1 space t_1 space p_1)_(cl vals, types cr) gamma_1$,
+    $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
     $...$,
-    $gamma_(n - 1) stretch(=>)^(m_n space t_n space p_n)_(cl vals, types cr) gamma_n$,
+    $mu_(n - 1) stretch(=>)^(m_n space t_n space e_n)_(cl vals, types cr) mu_n$,
 
-    $cl vals, types, mu, l cr
-     xarrow("CALL" f space [p_1, ... p_n])
-     cl vals, types, gamma_n, l cr$,
+    $cl types, vals, mu_0 cr
+     xarrow("CALL" f space [e_1, ... e_n])
+     cl types, vals, mu_n cr$,
   )
 ))
 
@@ -946,7 +1039,7 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ READ $p$],
 
-    $mu, types, vals tval p eqmu 0$,
+    $vals, mu tval p eqmu 0$,
 
     $cl types, vals, mu cr
      xarrow("READ" p)
@@ -964,7 +1057,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
@@ -988,7 +1081,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$,
   )