diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 602f81a..0c74973 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -195,19 +195,6 @@ struct
 
   (* - value construction *)
 
-  let rec valbuild (mem : mem) (t : atype) : mem * value =
-    match t with
-    | UnitT (Rd, _) -> (mem, UnitV (ZeroMV, ZeroRV, ZeroWV))
-    | UnitT (NRd, _) -> (mem, UnitV (BotMV, ZeroRV, ZeroWV))
-    | FunT _ -> raise @@ Typing_error "valbuild: funciton value is not supported"
-    | RefT (_, t) -> let (mem', v') = valbuild mem t in
-                     let (mem'', id'') = mem_add mem' v' in
-                     (mem'', RefV id'') 
-    | TupleT ts -> let folder = fun t (mem, vs') -> let (mem', v') = valbuild mem t in
-                                                        (mem', v' :: vs') in 
-                   let mem', vs' = List.fold_right folder ts (mem, []) in
-                   (mem', TupleV vs')
-
   let rec valcopy (mem : mem) (v : value) (t : atype) : mem * value =
     match t, v with
     | UnitT (Rd, _), UnitV (v_m, _, _) -> (mem, UnitV (v_m, ZeroRV, ZeroWV))
@@ -217,10 +204,10 @@ struct
     | RefT (_, t), RefV id -> let (mem', v') = valcopy mem (mem_get mem id) t in
                                let (mem'', id'') = mem_add mem' v' in
                                (mem'', RefV id'') 
-    | TupleT ts, TupleV vs -> let folder = fun v t (mem, vs') -> let (mem', v') = valcopy mem v t in
+    | TupleT ts, TupleV vs -> let folder = fun (mem, vs') v t -> let (mem', v') = valcopy mem v t in
                                                                  (mem', v' :: vs') in 
-                              let mem', vs' = List.fold_right2 folder vs ts (mem, []) in
-                              (mem', TupleV vs')
+                              let mem', vs' = List.fold_left2 folder (mem, []) vs ts in
+                              (mem', TupleV (List.rev vs')) (* TODO: FIXME: should reverse or not ?? *)
     | _, _ -> raise @@ Typing_error "valcopy: not trivial value, wrong type"
 
   (* - action rules *)
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index c2fec46..1912a7b 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -540,69 +540,9 @@ $action$ - действия, совершаемые с примитивным з
 
 === Value Construction
 
-#let build = `build`
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ build trivial read value],
-
-    $mu xarrowSquiggly(cl Read \, w cr)_build
-     cl cdl 0_m, 0_r, 0_w cdr, mu cr$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ build trivial $not$ read value],
-
-    $mu xarrowSquiggly(cl not Read \, w cr)_build
-     cl cdl bot, 0_r, 0_w cdr, mu cr$,
-  )
-))
-
-#h(10pt)
-
-// TODO: function pointer type ??
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ build reference value],
-
-    $mu xarrowSquiggly(t)_build cl v, mu_v cr$,
-
-    $mu_v xarrowSquiggly(v)_#[add] cl l, mu_a cr$,
-
-    $mu xarrowSquiggly(rf c t)_build cl rf l, mu_a cr$,
-  )
-))
-
-#h(10pt)
-
-#align(center, prooftree(
-  vertical-spacing: 4pt,
-  rule(
-    name: [ build tuple value],
-
-    $mu_0 xarrowSquiggly(t_1)_build cl v_1, mu_1 cr$,
-    $...$,
-    $mu_(n - 1) xarrowSquiggly(t_n)_build cl v_n, mu_n cr$,
-
-    $mu_0 xarrowSquiggly([t_1, ... t_n])_build cl [v_1, ... v_n], mu_n cr$,
-  )
-))
-
-#h(10pt)
-
-// ---
-
 // TODO: FIXME:add ref / copy modes correctness check ??
 
-// #let copy = `copy`
+#let new = `new`
 
 #align(center, prooftree(
   vertical-spacing: 4pt,
@@ -611,26 +551,22 @@ $action$ - действия, совершаемые с примитивным з
 
     $v_m in {0, ?, bot}$,
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl Read \, w cr)_copy
-     cl cdl v_m, 0_r, 0_w cdr, mu cr$,
+     xarrowSquiggly(cl Read \, w cr)_new
+     cl cdl v_m, 0, 0 cdr, mu cr$,
   )
 ))
 
-#h(10pt)
-
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
 //     name: [ new trivial read $top$ value],
 
 //     $cl cdl top, v_r, v_w cdr, mu cr
-//      xarrowSquiggly(cl Read \, w cr)_copy
+//      xarrowSquiggly(cl Read \, w cr)_new
 //      cl cdl 0, 0, 0 cdr, mu cr$,
 //   )
 // ))
 
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
@@ -638,61 +574,53 @@ $action$ - действия, совершаемые с примитивным з
 
     $v_m in {0, ?, bot/*, top */}$,
     $cl cdl v_m, v_r, v_w cdr, mu cr
-     xarrowSquiggly(cl not Read \, w cr)_copy
-     cl cdl bot, 0_r, 0_w cdr, mu cr$,
+     xarrowSquiggly(cl not Read \, w cr)_new
+     cl cdl bot, 0, 0 cdr, mu cr$,
   )
 ))
 
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new funciton pointer value],
 
-    $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_copy cl lambda overline(s), mu cr$,
+    $cl lambda overline(s), mu cr xarrowSquiggly(lambda space c space overline(t))_new cl lambda overline(s), mu cr$,
   )
 ))
 
-#h(10pt)
-
 // #align(center, prooftree(
 //   vertical-spacing: 4pt,
 //   rule(
 //     name: [ new reference ref value],
 
-//     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_copy cl rf l, mu cr$,
+//     $cl rf l, mu cr xarrowSquiggly(rf Ref t)_new cl rf l, mu cr$,
 //   )
 // ))
 
-// #h(10pt)
-
 // NOTE: due to new memory cells types (with rw subcells) valnue should always be copied
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new reference /* copy */ value],
 
-    $cl mu[l], mu cr xarrowSquiggly(t)_copy cl v, mu_v cr$,
+    $cl mu[l], mu cr xarrowSquiggly(t)_new cl v, mu_v cr$,
 
     $mu_v xarrowSquiggly(v)_#[add] cl l', mu_a cr$,
 
-    $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_copy cl rf l', mu_a cr$,
+    $cl rf l, mu cr xarrowSquiggly(rf c /*Copy*/ t)_new cl rf l', mu_a cr$,
   )
 ))
 
-#h(10pt)
-
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
     name: [ new tuple value],
 
-    $cl v_1, mu_0 cr xarrowSquiggly(t_1)_copy cl v'_1, mu_1 cr$,
+    $cl v_1, mu_0 cr xarrowSquiggly(t_1)_new cl lambda v'_1, mu_1 cr$,
     $...$,
-    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_copy cl v'_n, mu_n cr$,
+    $cl v_n, mu_(n - 1) cr xarrowSquiggly(t_n)_new cl lambda v'_n, mu_n cr$,
 
-    $cl [v_1, ... v_n], mu_0 cr xarrowSquiggly([t_1, ... t_n])_copy cl [v'_1, ... 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$,
   )
 ))
 
@@ -1139,7 +1067,7 @@ $action$ - действия, совершаемые с примитивным з
     // expect well typed program
 
     $vals, mu texpre e eqmu v$,
-    $cl v, mu cr xarrowSquiggly(t)_copy cl v', mu' cr$, // TODO: FIXME check (required?)
+    $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$
@@ -1426,7 +1354,7 @@ $action$ - действия, совершаемые с примитивным з
     // 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)_copy 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 <- ??
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 2d699bc..a60eafd 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -588,44 +588,6 @@ struct
 
   (* - value construction *)
 
-  let rec valbuild_foldero mem_with_vs tp mem_with_vs' =
-    ocanren {
-      fresh mem, vs, mem', v', vs' in
-      Std.pair mem vs == mem_with_vs &
-      valbuildo mem tp (Std.pair mem' v') &
-      vs' == v' :: vs &
-      mem_with_vs' == Std.pair mem' vs'
-  }
-  and valbuildo mem tp mem_with_id' = 
-    let open Type in
-    let open Value in
-    let open ReadCap in
-    (* let open CopyCap in *)
-    let open MemVal in
-    let open ReadVal in
-    let open WriteVal in
-    ocanren {
-      { fresh r, w in
-        tp == UnitT (r, w) &
-        { { r == Rd &
-            mem_with_id' == Std.pair mem (UnitV (ZeroMV, ZeroRV, ZeroWV)) } |
-          { r == NRd &
-            mem_with_id' == Std.pair mem (UnitV (BotMV, ZeroRV, ZeroWV)) } } } |
-      (* { fresh ts in *)
-        (* tp == FunT ts & *)
-        (* ??? } | *)
-      { fresh c, tp' in
-        tp == RefT (c, tp') &
-        { fresh mem_cp, v_cp, mem_add, id_add in
-          valbuildo mem tp' (Std.pair mem_cp v_cp) &
-          mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
-          mem_with_id' == (mem_add, RefV id_add) } } |
-      { fresh tps, mem', vs' in
-        tp == TupleT tps &
-        list_foldro valbuild_foldero (Std.pair mem []) tps (Std.pair mem' vs') &
-        mem_with_id' == Std.pair mem' (TupleV vs') }
-  }
-
   let rec valcopy_foldero mem_with_vs v tp mem_with_vs' =
     ocanren {
       fresh mem, vs, mem', v', vs' in
@@ -644,6 +606,7 @@ struct
     let open WriteVal in
     ocanren {
       { fresh r, w in
+        is_trivial_vo v &
         tp == UnitT (r, w) &
         { { fresh v_m, _v_r, _v_w in
             r == Rd &
diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml
index 6f65938..dccaa23 100644
--- a/model_with_structures/tests_f.ml
+++ b/model_with_structures/tests_f.ml
@@ -1018,8 +1018,8 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
                     ReadS sb_access3]
                    sendFBranch &
               seqo [ChoiceS (sendFBranch, SkipS);
-                    WriteS (VarP 0);
-                    ReadS (VarP 0)]
+                    WriteS (VarP 0));
+                    ReadS (VarP 0))]
                    sendF &
 
               fresh sa_access0, sa_access1, sa_access2, sa_access3 in
@@ -1027,7 +1027,7 @@ let prog_eval_compl_test_send _ = show(answer) (Stream.take (run q
               access_deref_accesso 1 1 0 sa_access1 &
               access_deref_access_deref_accesso 0 0 0 0 sa_access2 &
               access_deref_accesso 0 1 0 sa_access3 &
-              seqo [WriteS (VarP 0);
+              seqo [WriteS (VarP 0));
                     CallS (VarP sendID, [PathE (VarP 0)]);
                     CallS (VarP get_version_idID, [PathE (VarP 0)]);
                     CallS (VarP updated_versionID, [PathE (VarP 0)]);