diff --git a/model_with_structures/analyzer.ml b/model_with_structures/analyzer.ml
index 826bde5..10b74d7 100644
--- a/model_with_structures/analyzer.ml
+++ b/model_with_structures/analyzer.ml
@@ -78,35 +78,12 @@ struct
   (* --- *)
 
   type mem = value list * memid (* NOTE: memory and first free elem *)
-  type types = (data * atype) list (* glob *) * (data * atype) list (* glob + loc *)
-  type vals = (data * memid) list (* glob *) * (data * memid) list (* glob + loc *)
+  type types = (data * atype) list
+  type vals = (data * memid) list
   type state = mem * types * vals
 
   (* --- *)
 
-  (* - state utils *)
-
-  let types_assoc (x : data) (types : types) : atype =
-    (* try ( List.assoc x (fst types) ) *)
-    (* with Not_found -> *)
-    List.assoc x (snd types)
-  let vals_assoc (x : data) (vals : vals) : memid =
-    (* try ( List.assoc x (fst vals) ) *)
-    (* with Not_found -> *)
-    List.assoc x (snd vals)
-
-  let types_glob_add (types : types) (x : data) (t : atype) =
-    ((x, t) :: fst types, (x, t) :: snd types)
-
-  let types_add (types : types) (x : data) (t : atype) =
-    (fst types, (x, t) :: snd types)
-
-  let vals_glob_add (vals : vals) (x : data) (id : memid) =
-    ((x, id) :: fst vals, (x, id) :: snd vals)
-
-  let vals_add (vals : vals) (x : data) (id : memid) =
-    (fst vals, (x, id) :: snd vals)
-
   (* - utils *)
 
   let rec list_replace (xs : 'a list) (id : int) (y : 'a) : 'a list = match xs, id with
@@ -154,7 +131,7 @@ struct
     | AccessP (p, _) -> pathvar p
 
   let rec pathtype (types : types) (p : path) : atype = match p with
-    | VarP x -> types_assoc x types
+    | VarP x -> List.assoc x types
     | DerefP p -> (match pathtype types p with
                     | RefT (_, t) -> t
                     | _ -> raise @@ Typing_error "pathtype: deref")
@@ -168,7 +145,7 @@ struct
                                 Printf.printf "mem size: %i, " (List.length (fst mem));
                                 Printf.printf "mem size stored: %i " (snd mem);
                                 Printf.printf "\n"; *)
-                                vals_assoc x vals)
+                                List.assoc x vals)
     | DerefP p -> (match pathval mem vals p with
                     | RefV id -> mem_get mem id
                     | _ -> raise @@ Typing_error "pathval: deref")
@@ -236,7 +213,7 @@ struct
   let rec exprval (mem : mem) (vals : vals) (e : expr) : value = match e with
     | UnitE -> ZeroV
     | PathE p -> pathval mem vals p
-    | RefE x -> RefV (vals_assoc x vals)
+    | RefE x -> RefV (List.assoc x vals)
     | TupleE es -> TupleV (List.map (exprval mem vals) es)
 
   (* - expression typing *)
@@ -244,7 +221,7 @@ struct
   let rec exprtype (types : types) (e : expr) : atype = match e with
     | UnitE -> UnitT (Rd, NeverWr)
     | PathE p -> pathtype types p
-    | RefE x -> RefT (Rf, types_assoc x types)
+    | RefE x -> RefT (Rf, List.assoc x types)
     | TupleE es -> TupleT (List.map (exprtype types) es)
 
   (* - context initialization *)
@@ -257,12 +234,12 @@ struct
     | 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'', types_glob_add types x t, vals_glob_add vals x id)
+                     (mem'', (x, t) :: types, (x, id) :: vals)
     | FunD (ts, s)  -> let (mem', id) = mem_add mem (FunV [s]) in
-                       (mem', types_glob_add types x (FunT ts), vals_glob_add vals x id)
+                       (mem', (x, FunT ts) :: types, (x, id) :: vals)
 
   let empty_mem : mem = ([], 0)
-  let empty_state : state = (empty_mem, ([], []), ([], []))
+  let empty_state : state = (empty_mem, [], [])
 
   (* TODO: better way ??? *)
   let globals_min_id : data = 1000
@@ -279,14 +256,13 @@ struct
   let is_correct_tags (v : value) (r : read_cap) (w : write_cap)
                       (r' : read_cap) (w' : write_cap) (m : mode)
                       (c : copy_cap) : bool =
-    (* FIXME TMP *)
-    (* Printf.printf "%b %b %b %b %b\n" *)
-      (* (r != Rd || v == ZeroV) *)
-      (* (r != Rd || fst m == In) *)
-      (* (snd m != Out || w == AlwaysWr) *)
-      (* (* TODO: FIXME: why always write ?? *) *)
-      (* (((not ((w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf))) || w' == AlwaysWr)) *)
-      (* (is_trivial_v v); *)
+    (* FIXME TMP
+    Printf.printf "%b %b %b %b %b\n"
+      (r != Rd || v == ZeroV)
+      (r != Rd || fst m == In)
+      (snd m != Out || w == AlwaysWr)
+      (((not @@ (w == AlwaysWr || w == MayWr) && (snd m == Out || c == Rf)) || w' == AlwaysWr))
+      (is_trivial_v v); *)
     (r != Rd || v == ZeroV) &&
     (r != Rd || fst m == In) &&
     (snd m != Out || w == AlwaysWr) &&
@@ -323,12 +299,11 @@ struct
   let argsspoilp (state : state) (m : mode) (t : atype) (p : path) : mem =
     match state with (mem, types, vals) ->
     let x = pathvar p in
-    let id = vals_assoc x vals in (* base var address *)
-    let b = pathval mem vals p in (* subvalue in var *)
-    let t' = pathtype types p in (* type of subvalue *)
-    let (mem', b') = valspoil mem b t t' m Cp in (* spoil subvalue *)
-    (* TODO: FIXME: why copy (Cp)? *)
-    let (mem'', v'') = valupd mem' (mem_get mem' id) p b' in (* set subvalue into var *)
+    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 =
@@ -350,7 +325,7 @@ struct
     (* let t' = pathtype types p in *)
     let (mem', v') = valcopy mem v t in
     let (mem'', id) = mem_add mem' v' in
-    (mem'', types_add types x t, vals_add vals x id)
+    (mem'', (x, t) :: types, (x, id) :: vals)
 
   (* - function evaluation *)
   (* NOTE: not needed due to performed optimization in stmt_eval *)
@@ -366,8 +341,8 @@ struct
                                pathval mem vals f in
                        let t = (* FIXME TMP Printf.printf "call, before t\n"; *)
                                pathtype types f in
-                       let types' : types = (fst types, fst types) in
-                       let vals' : vals = (fst vals, fst vals) in
+                       let types' : types = [] in
+                       let vals' : vals = [] in
                        (match v, t with
                           | FunV (* xs, *) fstmts (* ) *), FunT ts ->
                             (* TODO: memoisation of the called functions *)
@@ -391,14 +366,12 @@ struct
                        if w == NeverWr
                        then raise @@ Eval_error "write: write tag"
                        else let x = pathvar p in
-                            let id = vals_assoc x vals 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 == SmthV || pathval mem vals p == BotV 
-                 then raise @@ Eval_error "read: spoiled value"
-                 else if pathval mem vals p != ZeroV 
-                 then raise @@ Eval_error "read: nontrivial value"
+    | 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
@@ -426,45 +399,13 @@ struct
 
   let ( #. ) x y = SeqS (x, y)
 
-  let v0 = VarP 0
-  let v1 = VarP 1
-  let v2 = VarP 2
-  let v3 = VarP 3
-  let v4 = VarP 4
-  let v5 = VarP 5
-  let v6 = VarP 6
-  let v7 = VarP 7
-  let v8 = VarP 8
-  let vg0 = VarP globals_min_id
-  let vg1 = VarP (globals_min_id + 1)
-  let vg2 = VarP (globals_min_id + 2)
-  let vg3 = VarP (globals_min_id + 3)
-  let vg4 = VarP (globals_min_id + 4)
-  let vg5 = VarP (globals_min_id + 5)
-  let vg6 = VarP (globals_min_id + 6)
-  let vg7 = VarP (globals_min_id + 7)
-  let vg8 = VarP (globals_min_id + 8)
+  let vx = VarP 0
+  let vy = VarP 1
+  let vz = VarP 2
 
-  let rf0E = RefE 0
-  let rf1E = RefE 1
-  let rf2E = RefE 2
-  let rf3E = RefE 3
-  let rf4E = RefE 4
-  let rf5E = RefE 5
-  let rf3E = RefE 3
-  let rf4E = RefE 4
-  let rf5E = RefE 5
-  let rfg0E = RefE globals_min_id
-  let rfg1E = RefE (globals_min_id + 1)
-  let rfg2E = RefE (globals_min_id + 2)
-  let rfg3E = RefE (globals_min_id + 3)
-  let rfg4E = RefE (globals_min_id + 4)
-  let rfg5E = RefE (globals_min_id + 5)
-  let rfg6E = RefE (globals_min_id + 6)
-  let rfg7E = RefE (globals_min_id + 7)
-  let rfg8E = RefE (globals_min_id + 8)
-
-  let pE p = PathE p
+  let vgx = VarP (globals_min_id)
+  let vgy = VarP (globals_min_id + 1)
+  let vgz = VarP (globals_min_id + 2)
 
   let drf p = DerefP p
   let access p i = AccessP (p, i)
@@ -485,12 +426,7 @@ struct
 
   let moded t = ((In, NOut), t)
 
-  let defgu t = VarD (t, UnitE)
-  let defg t e = VarD (t, e)
-
-  let wrS p = WriteS p 
-  let rdS p = ReadS p 
-  let callS f args = CallS (f, args)
+  let defg t = VarD (t, UnitE)
 
   (* - utils tests *)
 
@@ -527,7 +463,7 @@ struct
     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: spoiled value |}]
+    [%expect {| read |}]
 
   let%expect_test "simple vars, no read & read" =
     prog_eval_noret ([VarD (UnitT (NRd, MayWr), UnitE);
@@ -555,284 +491,23 @@ struct
 
   (* - basic call tests *)
 
-  (* let%expect_test "simple call with read" = *)
-    (* prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE); *)
-                      (* FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))], *)
-                     (* CallS (VarP (globals_min_id + 1), *)
-                            (* [PathE (VarP globals_min_id)])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  (* let%expect_test "simple call with write" = *)
-    (* prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE); *)
-                      (* VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id); *)
-                      (* FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))], *)
-                     (* CallS (VarP (globals_min_id + 2), *)
-                            (* [PathE (VarP (globals_min_id + 1))])); *)
-    (* Printf.printf "done!"; *)
-    (* [%expect {| done! |}] *)
-
-  let%expect_test "simple call with read, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
-        FunD (
-          [moded @@ cpT @@ uT_r],
-          rdS @@ drf @@ v0
-        )
-      ],
-      callS vg2 [pE vg1]
-    );
+  let%expect_test "simple call with read" =
+    prog_eval_noret ([VarD (UnitT (Rd, NeverWr), UnitE);
+                      FunD ([(In, NOut), UnitT (Rd, NeverWr)], ReadS (VarP 0))],
+                     CallS (VarP (globals_min_id + 1),
+                            [PathE (VarP globals_min_id)]));
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  let%expect_test "simple call with write, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
-        FunD (
-          [moded @@ cpT @@ uT_r_mw],
-          wrS @@ drf @@ v0
-        )
-      ],
-      callS vg2 [pE vg1]
-    );
+  let%expect_test "simple call with write" =
+    prog_eval_noret ([VarD ((UnitT (Rd, MayWr)), UnitE);
+                      VarD (RefT (Rf, (UnitT (Rd, MayWr))), RefE globals_min_id);
+                      FunD ([(In, NOut), RefT (Cp, UnitT (Rd, MayWr))], WriteS (DerefP (VarP 0)))],
+                     CallS (VarP (globals_min_id + 2),
+                            [PathE (VarP (globals_min_id + 1))]));
     Printf.printf "done!";
     [%expect {| done! |}]
 
-  let%expect_test "simple call with read after write, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
-        FunD (
-          [moded @@ cpT @@ uT_mw],
-          (wrS @@ drf @@ v0) #.
-          (rdS @@ drf @@ v0)
-        )
-      ],
-      callS vg2 [pE vg1]
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with forbidden write, dsl" =
-    try (prog_eval_noret (
-      [
-        defgu uT_r_mw;
-        defg (rfT uT_r_mw) rfg0E;
-        FunD (
-          [moded @@ cpT @@ uT_r],
-          wrS @@ drf @@ v0
-        )
-      ],
-      callS vg2 [pE vg1]
-    );
-    [%expect.unreachable]);
-    with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| write: write tag |}]
-
-  (* TODO: FIXME: why is condition on always write in parent ?? *)
-  let%expect_test "simple call with write to ref, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        FunD (
-          [moded @@ rfT @@ uT_aw],
-          wrS @@ drf @@ v0
-        )
-      ],
-      callS vg2 [pE vg1]
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with forbidden write to ref, dsl" =
-    try (prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        FunD (
-          [moded @@ rfT @@ uT_aw],
-          wrS @@ drf @@ v0
-        )
-      ],
-      (callS vg2 [pE vg1]) #.
-      (rdS @@ drf @@ vg1)
-    );
-    [%expect.unreachable]);
-    with Eval_error msg -> Printf.printf "%s" msg;
-    [%expect {| read: spoiled value |}]
-
-  let%expect_test "simple call with write to ref with fix, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        FunD (
-          [moded @@ rfT @@ uT_aw],
-          wrS @@ drf @@ v0
-        )
-      ],
-      (callS vg2 [pE vg1]) #.
-      (wrS @@ drf @@ vg1) #.
-      (rdS @@ drf @@ vg1)
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "call inside call, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        FunD (
-          [moded @@ rfT @@ uT_aw],
-          wrS @@ drf @@ v0
-        );
-        FunD (
-          [moded @@ cpT @@ uT_aw],
-          (callS vg2 [pE v0]) #.
-          (wrS @@ drf @@ v0)
-        )
-      ],
-      (callS vg3 [pE vg1]) #.
-      (rdS @@ drf @@ vg1)
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "call to fix after call, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        FunD (
-          [moded @@ rfT @@ uT_aw],
-          wrS @@ drf @@ v0
-        );
-        FunD (
-          [((In, Out), rfT @@ uT_aw)],
-          wrS @@ drf @@ v0
-        )
-      ],
-      (callS vg2 [pE vg1]) #.
-      (callS vg3 [pE vg1]) #.
-      (rdS @@ drf @@ vg1)
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with global variable usage, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        FunD (
-          [moded @@ cpT @@ uT_aw],
-          (wrS @@ vg0) #.
-          (rdS @@ drf @@ vg1)
-        )
-      ],
-      (callS vg2 [pE vg1]) #.
-      (rdS @@ drf @@ vg1)
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with read & write (2 args), dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
-        FunD (
-          [
-            moded @@ rfT @@ uT_r;
-            moded @@ rfT @@ uT_aw;
-          ],
-          (rdS @@ drf @@ v0) #.
-          (wrS @@ drf @@ v1)
-        )
-      ],
-      callS vg4 [pE vg1; pE vg3]
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with different arguments modifiers, copy, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E;
-        FunD (
-          [
-            ((NIn, NOut), cpT @@ uT_aw);
-            ((In, NOut), cpT @@ uT_r_aw);
-            ((NIn, Out), cpT @@ uT_aw);
-            ((In, Out), cpT @@ uT_r_aw);
-          ],
-          (rdS @@ drf @@ v1) #.
-          (rdS @@ drf @@ v3) #.
-          (wrS @@ drf @@ v1) #.
-          (wrS @@ drf @@ v2) #.
-          (wrS @@ drf @@ v3)
-        )
-      ],
-      (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
-      (rdS @@ drf @@ vg1) #.
-      (rdS @@ drf @@ vg3) #.
-      (rdS @@ drf @@ vg5) #.
-      (rdS @@ drf @@ vg7)
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  let%expect_test "simple call with different arguments modifiers, ref, dsl" =
-    prog_eval_noret (
-      [
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg0E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg2E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg4E;
-        defgu uT_r_aw;
-        defg (rfT uT_r_aw) rfg6E;
-        FunD (
-          [
-            ((NIn, NOut), rfT @@ uT);
-            ((In, NOut), rfT @@ uT_r);
-            ((NIn, Out), rfT @@ uT_aw);
-            ((In, Out), rfT @@ uT_r_aw);
-          ],
-          (rdS @@ drf @@ v1) #.
-          (rdS @@ drf @@ v3) #.
-          (wrS @@ drf @@ v2) #.
-          (wrS @@ drf @@ v3)
-        )
-      ],
-      (callS vg8 [pE vg1; pE vg3; pE vg5; pE vg7]) #.
-      (rdS @@ drf @@ vg1) #.
-      (rdS @@ drf @@ vg3) #.
-      (rdS @@ drf @@ vg5) #.
-      (rdS @@ drf @@ vg7)
-    );
-    Printf.printf "done!";
-    [%expect {| done! |}]
-
-  (* TODO: recursive call test (for the future when memoization will be implemented) *)
-
   (* --- FIXME --- CURRENT REWRITE POINT --- FIXME --- *)
 
   (* --- tests --- *)
diff --git a/model_with_structures/dune b/model_with_structures/dune
index eae17b8..54383e4 100644
--- a/model_with_structures/dune
+++ b/model_with_structures/dune
@@ -13,34 +13,34 @@
  (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)
diff --git a/model_with_structures/model.typ b/model_with_structures/model.typ
index b3bc24b..76424e1 100644
--- a/model_with_structures/model.typ
+++ b/model_with_structures/model.typ
@@ -15,8 +15,6 @@
 
 *TODO: top-level value copy mode ??* // TODO: FIXME
 
-*TODO: add formal global env to all types and vals (as in code) ??* // TODO: FIXME
-
 #h(10pt)
 
 #let rf = $\& #h(3pt)$
@@ -908,10 +906,9 @@ $s in stmt, f in X, x in X, a in X$
     $l = vals[x]$,
     $vals, mu texpre p eqmu b$,
     $types ttype p : t'$,
-    // TODO: FIXME: Ref or Copy ?? in root <- Copy ??,
-    // <- otherwise all subsequent copy capabilities will be ref (in current impl)
+    // 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 \, Copy)_spoil cl b', mu' cr$,
+    $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'']$,
@@ -923,7 +920,7 @@ $s in stmt, f in X, x in X, a in X$
 #align(center, prooftree(
   vertical-spacing: 4pt,
   rule(
-    name: [ full spoil for ref expr],
+    name: [ full spoil for tuple expr],
 
     // NOTE: x as path
     $mu stretch(=>)^(m space t space x)_(cl vals, types cr) mu'$,
@@ -944,7 +941,7 @@ $s in stmt, f in X, x in X, a in X$
     $...$,
     $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$,
+    $mu_0 stretch(=>)^(m space [t_1, ... t_n] space [e_1, ... e_n]_(cl vals, types cr) mu_n$,
   )
 ))
 
@@ -982,9 +979,8 @@ $s in stmt, f in X, x in X, a in X$
   rule(
     name: [ new reference copy value],
 
-    // TODO: FIXME: introduce global types and vals
-    $types_0 = types_#[glob]$,
-    $vals_0 = vals_#[glob]$,
+    $types_0 = []$,
+    $vals_0 = []$,
 
     // NOTE: dashed arrow to fill context
     $cl types_0, vals_0,  mu_0 cr
@@ -999,7 +995,7 @@ $s in stmt, f in X, x in X, a in X$
      xarrow(s)
      cl types', vals', mu' cr$,
 
-    $vals, mu_0 tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
+    $cl vals, mu_0 cr tfunceval cl s, [x_1, .. x_n], [t_1, ... t_n], [e_1, ... e_n] cr$,
   )
 ))
 
@@ -1029,9 +1025,9 @@ $s in stmt, f in X, x in X, a in X$
     $types ttype f : lambda [m_1 t_1, ... m_n t_n] $,
 
     // NOTE: check that all the possible bodies are possible to eval
-    $vals, mu_0 tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
+    $cl vals, mu_0 cr tfunceval cl s_1, overline(x)_1, [t_1, ... t_n], [e_1, ... e_n] cr$,
     $...$,
-    $vals, mu_0 tfunceval cl s_n, overline(x)_n, [t_1, ... t_n], [e_1, ... e_n] 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
     $mu_0 stretch(=>)^(m_1 space t_1 space e_1)_(cl vals, types cr) mu_1$,
diff --git a/model_with_structures/synthesizer.ml b/model_with_structures/synthesizer.ml
index 1908033..1ce75a1 100644
--- a/model_with_structures/synthesizer.ml
+++ b/model_with_structures/synthesizer.ml
@@ -167,7 +167,7 @@ struct
     [%%ocanren_inject
       type nonrec ('sl, 'd, 'vl) t = ZeroV | SmthV | BotV | FunV of 'sl | RefV of 'd | TupleV of 'vl
       [@@deriving gt ~options:{ show; gmap }]
-      type ground = (((* Nat.ground List.ground * *) Stmt.ground) List.ground, Nat.ground, ground List.ground) t
+      type ground = ((Nat.ground List.ground * Stmt.ground) List.ground, Nat.ground, ground List.ground) t
     ]
   end
 
@@ -185,7 +185,7 @@ struct
   module TypesEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'dtl t = TypesEnv of 'dtl (* glob *) * 'dtl (* glob + loc *)
+      type nonrec 'dtl t = TypesEnv of 'dtl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Type.ground) List.ground) t
     ]
@@ -194,7 +194,7 @@ struct
   module ValsEnv = struct
     [@@@warning "-26-27-32-33-34-35-36-37-38-39-60-66-67"]
     [%%ocanren_inject
-      type nonrec 'ddl t = ValsEnv of 'ddl (* glob *) * 'ddl (* glob + loc *)
+      type nonrec 'ddl t = ValsEnv of 'ddl
       [@@deriving gt ~options:{ show; gmap }]
       type nonrec ground = ((Nat.ground * Nat.ground) List.ground) t
     ]
@@ -211,58 +211,6 @@ struct
 
   (* --- *)
 
-  (* - state utils *)
-
-  let types_assoco id types tp =
-    let open TypesEnv in
-    ocanren {
-      fresh _glob_tps, tps in
-      types == TypesEnv (_glob_tps, tps) &
-      List.assoco id tps tp
-    }
-
-  let vals_assoco id vals v =
-    let open ValsEnv in
-    ocanren {
-      fresh _glob_vs, vs in
-      vals == ValsEnv (_glob_vs, vs) &
-      List.assoco id vs v
-    }
-
-  let types_glob_addo types x tp types' = 
-    let open TypesEnv in
-    ocanren {
-      fresh glob_tps, tps in
-      types == TypesEnv (glob_tps, tps) &
-      types' == TypesEnv ((Std.pair x tp) :: glob_tps,
-                          (Std.pair x tp) :: tps)
-  }
-
-  let types_addo types x tp types' = 
-    let open TypesEnv in
-    ocanren {
-      fresh glob_tps, tps in
-      types == TypesEnv (glob_tps, tps) &
-      types' == TypesEnv (glob_tps, (Std.pair x tp) :: tps)
-  }
-
-  let vals_glob_addo vals x v vals' = 
-    let open ValsEnv in
-    ocanren {
-      fresh glob_vs, vs in
-      vals == ValsEnv (glob_vs, vs) &
-      vals' == ValsEnv ((Std.pair x v) :: glob_vs,
-                        (Std.pair x v) :: vs)
-  }
-
-  let vals_addo vals x v vals' = 
-    let open ValsEnv in
-    ocanren {
-      fresh glob_vs, vs in
-      vals == ValsEnv (glob_vs, vs) &
-      vals' == ValsEnv (glob_vs, (Std.pair x v) :: vs)
-  }
-
   (* - utils *)
 
   let rec list_replaceo xs id value ys = ocanren {
@@ -409,6 +357,22 @@ struct
       { fresh p', _id in p == AccessP (p', _id) & pathvaro p' x }
   }
 
+  let types_assoco id types tp =
+    let open TypesEnv in
+    ocanren {
+      fresh tps in
+      types == TypesEnv tps &
+      List.assoco id tps tp
+    }
+
+  let vals_assoco id vals v =
+    let open ValsEnv in
+    ocanren {
+      fresh vs in
+      vals == ValsEnv vs &
+      List.assoco id vs v
+    }
+
   let rec pathtypeo types p tp =
     let open Path in
     let open Type in
@@ -608,23 +572,24 @@ struct
   let add_declo st x d st' =
     let open StEnv in
     let open Decl in
+    let open TypesEnv in
+    let open ValsEnv in
     ocanren {
       fresh mem, types, vals in
-      st == StEnv (mem, types, vals) &
+      st == StEnv (mem, TypesEnv types, ValsEnv vals) &
       {
         { fresh tp, e, v,
                 mem_with_v_cp, mem_cp, v_cp,
-                mem_with_id_add, mem_add, id_add,
-                types', vals' in
+                mem_with_id_add, mem_add, id_add in
           d == VarD (tp, e) &
-          exprvalo mem vals e v &
+          exprvalo mem (ValsEnv vals) e v &
           valcopyo mem v tp mem_with_v_cp &
           Pair.pair mem_cp v_cp == mem_with_v_cp &
           mem_addo mem_cp v_cp mem_with_id_add &
           Pair.pair mem_add id_add == mem_with_id_add &
-          types_glob_addo types x tp types' &
-          vals_glob_addo vals x id_add vals' &
-          st' == StEnv (mem_add, types', vals')
+          st' == StEnv (mem_add,
+                        TypesEnv ((Pair.pair x tp) :: types),
+                        ValsEnv ((Pair.pair x id_add) :: vals))
           }
       }
   }
@@ -640,7 +605,7 @@ struct
     ocanren {
       fresh m in
       empty_memo m &
-      st == StEnv (m, TypesEnv ([], []), ValsEnv ([], []))
+      st == StEnv (m, TypesEnv [], ValsEnv [])
   }
 
   (* TODO: better way ??? *)
@@ -752,7 +717,7 @@ struct
       vals_assoco x vals id &
       pathvalo mem vals p b &
       pathtypeo types p tp' &
-      valspoilo mem b tp tp' m Cp (Std.pair mem_sp b_sp) &
+      valspoilo mem b tp tp' m Rf(Std.pair mem_sp b_sp) &
       mem_geto mem_sp id v_sp &
       valupdo mem_sp v_sp p b_sp (Std.pair mem_upd v_upd) &
       mem_seto mem_upd id v_upd mem'
@@ -794,18 +759,17 @@ struct
 
   let addargo st oldvals x tp e st' =
     let open StEnv in
+    let open TypesEnv in
+    let open ValsEnv in
     ocanren {
-      fresh mem, types, vals, v,
-            mem_cp, v_cp,
-            mem_add, id_add,
-            types', vals' in
-      st == StEnv (mem, types, vals) &
+      fresh mem, types, vals, v, mem_cp, v_cp, mem_add, id_add in
+      st == StEnv (mem, TypesEnv types, ValsEnv vals) &
       exprvalo mem oldvals e v &
       valcopyo mem v tp (Std.pair mem_cp v_cp) &
       mem_addo mem_cp v_cp (Std.pair mem_add id_add) &
-      types_addo types x tp types' &
-      vals_addo vals x id_add vals' &
-      st' == StEnv (mem_add, types', vals')
+      st' == StEnv (mem_add,
+                    TypesEnv ((Std.pair x tp) :: types),
+                    ValsEnv ((Std.pair x id_add) :: vals))
   }
 
   (* - function evaluation *)
@@ -842,20 +806,16 @@ struct
       st == StEnv (mem, types, vals) &
       {
         { s == SkipS & st == st' } |
-        { fresh f, es, v, tp,
-                glob_tps, _tps,
-                glob_vs, _vs,
-                types', vals',
+        { fresh f, es, v, tp, types', vals',
                 fstmts, tps, st',
                 state_with_args, _arg_id,
-                _states_evaled, mem_spoiled in
+                _states_evaled,
+                mem_spoiled in
           s == CallS (f, es) &
           pathvalo mem vals f v &
           pathtypeo types f tp &
-          types == TypesEnv (glob_tps, _tps) &
-          vals == ValsEnv (glob_vs, _vs) &
-          types' == TypesEnv (glob_tps, glob_tps) &
-          vals' == ValsEnv (glob_vs, glob_vs) &
+          types' == TypesEnv [] &
+          vals' == ValsEnv [] &
           v == FunV fstmts &
           tp == FunT tps &
           st' == StEnv (mem, types', vals') &
@@ -907,12 +867,9 @@ struct
 
   let prog_evalo prog st' =
     let open Prg in
-    let open Stmt in
     ocanren {
-      fresh decls, s, init_st in
+      fresh decls, s, init_st in 
       prog == Prg (decls, s) &
-      decls == [] &
-      s == SkipS &
       prog_inito prog init_st &
       stmt_evalo init_st s st'
   }
diff --git a/model_with_structures/tests.ml b/model_with_structures/tests.ml
index 8e3ae24..8017884 100644
--- a/model_with_structures/tests.ml
+++ b/model_with_structures/tests.ml
@@ -2,63 +2,60 @@ open Tests_f
 open Synthesizer
 open Relational
 
-let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ());
-  [%expect {| [StEnv (MemEnv ([], O), TypesEnv ([], []), ValsEnv ([], []))] |}]
-
 (* type tests *)
-(* let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}] *)
-(* let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}] *)
-(* let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}] *)
-(* let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}] *)
-(* let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}] *)
-(* let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}] *)
-(* let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}] *)
-(* let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}] *)
+let%expect_test "Tag type test" = print_endline (Tag.Test.test ()); [%expect {| [Tag (Rd, NeverWr, Ref, In, NOut)] |}]
+let%expect_test "Stmt type test (1)" = print_endline (Stmt.Test.test1 ()); [%expect {| [[S (S (O))]] |}]
+let%expect_test "Stmt type test (2)" = print_endline (Stmt.Test.test2 ()); [%expect {| [Call (S (O), [S (S (O))])] |}]
+let%expect_test "FunDecl type test" = print_endline (FunDecl.Test.test ()); [%expect {| [FunDecl ([Tag (Rd, AlwaysWr, Ref, In, NOut); Tag (Rd, AlwaysWr, Val, In, NOut)], [Call (S (O), [O]); Write (S (O))])] |}]
+let%expect_test "Prog type test" = print_endline (Prog.Test.test ()); [%expect {| [Prog ([], FunDecl ([Tag (Rd, NeverWr, Val, In, NOut)], [Write (O); Read (O)]))] |}]
+let%expect_test "Arg type test" = print_endline (Arg.Test.test ()); [%expect {| [LValue (S (S (S (O))))] |}]
+let%expect_test "Value type test" = print_endline (Value.Test.test ()); [%expect {| [Bot; Unit] |}]
+let%expect_test "St type test" = print_endline (St.Test.test ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Bot], S (O), [O])] |}]
 
 (* function tests *)
-(* let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}] *)
-(* let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}] *)
-(* let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}] *)
-(* let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}] *)
-(* let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}] *)
-(* let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}] *)
-(* let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
-(* let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}] *)
-(* let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}] *)
-(* let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}] *)
-(* let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}] *)
-(* let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}] *)
-(* let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}] *)
-(* let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
-(* let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}] *)
-(* let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}] *)
-(* let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}] *)
-(* let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}] *)
-(* let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
-(* let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}] *)
-(* let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}] *)
-(* let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}] *)
-(* let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
-(* let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}] *)
-(* let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}] *)
-(* let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}] *)
-(* let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}] *)
-(* let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}] *)
-(* let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}] *)
-(* let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}] *)
-(* let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}] *)
-(* let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}] *)
-(* let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}] *)
-(* let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}] *)
-(* let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}] *)
-(* let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}] *)
-(* let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
-(* let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}] *)
-(* let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}] *)
-(* let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}] *)
-(* let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}] *)
-(* let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}] *)
-(* let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}] *)
+let%expect_test "inv_id test 1" = print_endline (inv_id_t ()); [%expect {| [O] |}]
+let%expect_test "inv_id test 2" = print_endline (inv_id_t2 ()); [%expect {| [S (O)] |}]
+let%expect_test "inv_id test 3" = print_endline (inv_id_t3 ()); [%expect {| [S (O)] |}]
+let%expect_test "list_drop test" = print_endline (list_drop_t ()); [%expect {| [[S (S (S (O)))]] |}]
+let%expect_test "list_replace test" = print_endline (list_replace_t ()); [%expect {| [[S (O); O; S (S (S (O))); S (S (S (S (O))))]] |}]
+let%expect_test "arG_to_value test 1" = print_endline (arg_to_value_t ()); [%expect {| [Unit] |}]
+let%expect_test "st_add_arg test" = print_endline (st_add_arg_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "write eval test 1" = print_endline (write_eval_t1 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "write eval test 2" = print_endline (write_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [])] |}]
+let%expect_test "multiple writes eval test" = print_endline (writes_eval_t ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Unit], S (S (O)), [])] |}]
+let%expect_test "call eval test 1" = print_endline (call_eval_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [O])] |}]
+let%expect_test "call eval test 2" = print_endline (call_eval_t2 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 3" = print_endline (call_eval_t3 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Unit], S (S (O)), [O])] |}]
+let%expect_test "call eval test 4" = print_endline (call_eval_t4 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
+let%expect_test "call eval test 5" = print_endline (call_eval_t5 ()); [%expect {| [St ([(S (O), (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O))); (O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot; Bot], S (S (O)), [O])] |}]
+let%expect_test "mem_set test 1" = print_endline (mem_set_t1 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "mem_set test 2" = print_endline (mem_set_t2 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), O))], [Bot], S (O), [])] |}]
+let%expect_test "mem_set test 3" = print_endline (meem_set_t3 ()); [%expect {| [St ([(O, (Tag (NRd, AlwaysWr, Ref, In, NOut), S (O)))], [Bot; Unit], S (S (O)), [])] |}]
+let%expect_test "add_arg_folder test" = print_endline (add_arg_folder_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "foldl2 test" = print_endline (foldl2_t ()); [%expect {| [St ([(O, (Tag (Rd, AlwaysWr, Val, In, NOut), O))], [Unit], S (O), [])] |}]
+let%expect_test "rvalue test" = print_endline (rvalue_t ()); [%expect {| [[]; [RValue]; [RValue; RValue]] |}]
+let%expect_test "empty_state test" = print_endline (empty_state_t ()); [%expect {| [St ([], [], O, [])] |}]
+let%expect_test "function eval test 1" = print_endline (fun_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
+let%expect_test "function eval test 2" = print_endline (fun_eval_t2 ()); [%expect {| [St ([], [], O, [])] |}]
+let%expect_test "function eval test 3" = print_endline (fun_eval_t3 ()); [%expect {| [] |}]
+let%expect_test "function eval test 4" = print_endline (fun_eval_t4 ()); [%expect {| [] |}]
+let%expect_test "function eval test 5" = print_endline (fun_eval_t5 ()); [%expect {| [] |}]
+let%expect_test "function eval test 6" = print_endline (fun_eval_t6 ()); [%expect {| [St ([], [], O, [O])] |}]
+let%expect_test "prog eval test 1" = print_endline (prog_eval_t1 ()); [%expect {| [St ([], [], O, [])] |}]
+let%expect_test "prog eval test 2" = print_endline (prog_eval_t2 ()); [%expect {| [St ([], [], O, [O])] |}]
+let%expect_test "prog eval test 3" = print_endline (prog_eval_t3 ()); [%expect {| [St ([], [], O, [O])] |}]
+let%expect_test "prog eval test 4" = print_endline (prog_eval_t4 ()); [%expect {| [] |}]
+let%expect_test "prog eval test 5" = print_endline (prog_eval_t5 ()); [%expect {| [St ([], [], O, [O])] |}]
+let%expect_test "prog eval test 6" = print_endline (prog_eval_t6 ()); [%expect {| [] |}]
+let%expect_test "synthesis test 1" = print_endline (synt_t1 ()); [%expect {| [Tag (Rd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)] |}]
+let%expect_test "synthesis test 2" = print_endline (synt_t2 ()); [%expect {| [Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Ref, In, NOut)] |}]
+let%expect_test "synthesis test 3" = print_endline (synt_t3 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]; [Tag (NRd, AlwaysWr, Ref, In, NOut); Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
+let%expect_test "synthesis test 4" = print_endline (synt_t4 ()); [%expect {| [[Tag (NRd, AlwaysWr, Val, In, NOut)]] |}]
+let%expect_test "synthesis test 5" = print_endline (synt_t5 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Val]; [Ref; Ref]] |}]
+let%expect_test "synthesis test 6" = print_endline (synt_t6 ()); [%expect {| [[Val; Val]; [Val; Ref]; [Ref; Ref]; [Ref; Val]] |}]
+let%expect_test "synthesis test 7" = print_endline (synt_t7 ()); [%expect {| [[Val; Val]; [Ref; Val]] |}]
+let%expect_test "synthesis test 8" = print_endline (synt_t8 ()); [%expect {| [[Val; Val]; [Val; Ref]] |}]
+let%expect_test "synthesis test 9" = print_endline (synt_t9 ()); [%expect {| [[Val; Ref]; [Val; Val]] |}]
 
-(* let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}] *)
+let%expect_test "recursive eval test" = print_endline (rec_eval_t ()); [%expect {| [St ([], [], O, [O])] |}]
 
diff --git a/model_with_structures/tests_f.ml b/model_with_structures/tests_f.ml
index 6737d97..5427966 100644
--- a/model_with_structures/tests_f.ml
+++ b/model_with_structures/tests_f.ml
@@ -4,516 +4,506 @@ open GT
 open OCanren
 open OCanren.Std
 
-@type answer  = StEnv.ground GT.list with show
+@type answer  = St.ground GT.list with show
+@type answerArgs = (Arg.ground List.ground) GT.list with show
+@type answerValue = Value.ground GT.list with show
+@type answerNat = Nat.ground GT.list with show
+@type answerNats = (Nat.ground List.ground) GT.list with show
+@type answerTag = Tag.ground GT.list with show
+@type answerTags = (Tag.ground List.ground) GT.list with show
+@type answerCopyCap = CopyCap.ground GT.list with show
+@type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show
 
-let prog_eval_t1 _ = show(answer) (Stream.take (run q
-  (fun q -> let open Prg in
-            let open Stmt in
+let inv_id_t _ = show(answerNat) (Stream.take (run q
+  (fun q -> ocanren { inv_ido 2 1 q })
+  (fun q -> q#reify Nat.prj_exn)))
+
+let inv_id_t2 _ = show(answerNat) (Stream.take (run q
+  (fun q -> ocanren { inv_ido 2 0 q })
+  (fun q -> q#reify Nat.prj_exn)))
+
+let inv_id_t3 _ = show(answerNat) (Stream.take (run q
+  (fun q -> ocanren { inv_ido 2 q 0 })
+  (fun q -> q#reify Nat.prj_exn)))
+
+let list_drop_t _ = show(answerNats) (Stream.take (run q
+  (fun q -> ocanren { list_dropo 2 [1; 2; 3] q })
+  (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+
+let list_replace_t  _ = show(answerNats) (Stream.take (run q
+  (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q })
+  (fun q -> q#reify (List.prj_exn Nat.prj_exn))))
+
+let arg_to_value_t _ = show(answerValue) (Stream.take (run q
+  (fun q -> let open Arg in
             ocanren {
-              fresh prog in
-              prog == Prg ([], SkipS) &
-              prog_evalo prog q})
-  (fun q -> q#reify (StEnv.prj_exn))))
+    fresh s in
+      empty_stateo s &
+      arg_to_valueo s RValue q })
+  (fun q -> q#reify (Value.prj_exn))))
 
-(* @type answerArgs = (Arg.ground List.ground) GT.list with show *)
-(* @type answerValue = Value.ground GT.list with show *)
-(* @type answerNat = Nat.ground GT.list with show *)
-(* @type answerNats = (Nat.ground List.ground) GT.list with show *)
-(* @type answerTag = Tag.ground GT.list with show *)
-(* @type answerTags = (Tag.ground List.ground) GT.list with show *)
-(* @type answerCopyCap = CopyCap.ground GT.list with show *)
-(* @type answerCopyCaps = (CopyCap.ground List.ground) GT.list with show *)
+let st_add_arg_t _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            ocanren {
+    fresh s, s', cnt in
+      empty_stateo s &
+      empty_stateo s' &
+      st_add_argo s  s' Nat.o rwi_val RValue q })
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let inv_id_t _ = show(answerNat) (Stream.take (run q *)
-  (* (fun q -> ocanren { inv_ido 2 1 q }) *)
-  (* (fun q -> q#reify Nat.prj_exn))) *)
+let write_eval_t1 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
+      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
+      stmt == Write 0 &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let inv_id_t2 _ = show(answerNat) (Stream.take (run q *)
-  (* (fun q -> ocanren { inv_ido 2 0 q }) *)
-  (* (fun q -> q#reify Nat.prj_exn))) *)
+let write_eval_t2 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
+      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
+      stmt == Write 1 &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let inv_id_t3 _ = show(answerNat) (Stream.take (run q *)
-  (* (fun q -> ocanren { inv_ido 2 q 0 }) *)
-  (* (fun q -> q#reify Nat.prj_exn))) *)
+let writes_eval_t _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmts in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) &
+      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
+      stmts == [Write 0; Write 1] &
+      eval_bodyo s p stmts q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let list_drop_t _ = show(answerNats) (Stream.take (run q *)
-  (* (fun q -> ocanren { list_dropo 2 [1; 2; 3] q }) *)
-  (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
+let call_eval_t1 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
+      p == [FunDecl ([wi_ref], [Write 0])] &
+      stmt == Call (0, [0]) &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let list_replace_t  _ = show(answerNats) (Stream.take (run q *)
-  (* (fun q -> ocanren { list_replaceo [1; 2; 3; 4] 1 0 q }) *)
-  (* (fun q -> q#reify (List.prj_exn Nat.prj_exn)))) *)
+let call_eval_t2 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_ref], [Write 0])] &
+      stmt == Call (0, [0]) &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let arg_to_value_t _ = show(answerValue) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* empty_stateo s & *)
-      (* arg_to_valueo s RValue q }) *)
-  (* (fun q -> q#reify (Value.prj_exn)))) *)
+let call_eval_t3 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_ref], [Write 0])] &
+      stmt == Call (0, [1]) &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let st_add_arg_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* ocanren { *)
-    (* fresh s, s', cnt in *)
-      (* empty_stateo s & *)
-      (* empty_stateo s' & *)
-      (* st_add_argo s  s' Nat.o rwi_val RValue q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let call_eval_t4 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
+      stmt == Call (0, [0; 1]) &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let write_eval_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Write 0 & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let call_eval_t5 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            let open Stmt in
+            let open FunDecl in
+            ocanren {
+    fresh s, p, stmt in
+      s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) &
+      p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
+      stmt == Call (0, [1; 0]) &
+      eval_stmto s p stmt q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let write_eval_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Write 1 & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let mem_set_t1 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            ocanren {
+    fresh s in
+      s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) &
+      mem_seto s 0 Unit q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let writes_eval_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmts in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Bot; Bot], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmts == [Write 0; Write 1] & *)
-      (* eval_bodyo s p stmts q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let mem_set_t2 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            ocanren {
+    fresh s in
+      s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) &
+      mem_seto s 0 Bot q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let call_eval_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
-      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-      (* stmt == Call (0, [0]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let meem_set_t3 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            let open Value in
+            let open St in
+            ocanren {
+    fresh s in
+      s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) &
+      mem_seto s 0 Bot q})
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let call_eval_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-      (* stmt == Call (0, [0]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let add_arg_folder_t _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            ocanren {
+    fresh s, s', cnt in
+      empty_stateo s &
+      empty_stateo s' &
+      add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) })
+  (fun q -> q#reify (St.prj_exn))))
 
-(* let call_eval_t3 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-      (* stmt == Call (0, [1]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t4 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Call (0, [0; 1]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let call_eval_t5 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* let open Stmt in *)
-            (* let open FunDecl in *)
-            (* ocanren { *)
-    (* fresh s, p, stmt in *)
-      (* s == St ([Std.pair 1 (Std.pair wi_ref 1); Std.pair 0 (Std.pair wi_ref 0)], [Unit; Unit], 2, []) & *)
-      (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-      (* stmt == Call (0, [1; 0]) & *)
-      (* eval_stmto s p stmt q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let mem_set_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Bot], 1, []) & *)
-      (* mem_seto s 0 Unit q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let mem_set_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 0)], [Unit], 1, []) & *)
-      (* mem_seto s 0 Bot q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let meem_set_t3 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* let open Value in *)
-            (* let open St in *)
-            (* ocanren { *)
-    (* fresh s in *)
-      (* s == St ([Std.pair 0 (Std.pair wi_ref 1)], [Unit; Unit], 2, []) & *)
-      (* mem_seto s 0 Bot q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let add_arg_folder_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* ocanren { *)
-    (* fresh s, s', cnt in *)
-      (* empty_stateo s & *)
-      (* empty_stateo s' & *)
-      (* add_arg_foldero s (Std.pair s' Nat.o) rwi_val RValue (Std.pair q cnt) }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
-
-(* let foldl2_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Arg in *)
-            (* let open Tag in *)
-            (* ocanren { *)
-    (* fresh s, s', cnt, arg_tags, args in *)
-      (* arg_tags == [rwi_val] & *)
-      (* args == [RValue] & *)
-      (* empty_stateo s & *)
-      (* empty_stateo s' & *)
-      (* list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let foldl2_t _ = show(answer) (Stream.take (run q
+  (fun q -> let open Arg in
+            let open Tag in
+            ocanren {
+    fresh s, s', cnt, arg_tags, args in
+      arg_tags == [rwi_val] &
+      args == [RValue] &
+      empty_stateo s &
+      empty_stateo s' &
+      list_foldl2o (add_arg_foldero s) (Std.pair s' Nat.o) arg_tags args (Std.pair q cnt) })
+  (fun q -> q#reify (St.prj_exn))))
 
 
-(* let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q *)
-  (* (fun q -> let open Arg in *)
-            (* ocanren {fresh v in List.mapo arg_to_rvalueo v q}) *)
-  (* (fun q -> q#reify (List.prj_exn Arg.prj_exn)))) *)
+let rvalue_t _ = show(answerArgs) (Stream.take ~n:3 (run q
+  (fun q -> let open Arg in
+            ocanren {fresh v in List.mapo arg_to_rvalueo v q})
+  (fun q -> q#reify (List.prj_exn Arg.prj_exn))))
 
 (* empty state test *)
-(* let empty_state_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> ocanren {empty_stateo q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let empty_state_t _ = show(answer) (Stream.take (run q
+  (fun q -> ocanren {empty_stateo q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* fun eval test *)
-(* let fun_eval_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> (* let open Prog in *) *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [] & *)
-                        (* d == FunDecl ([], []) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let fun_eval_t1 _ = show(answer) (Stream.take (run q
+  (fun q -> (* let open Prog in *)
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren { fresh s, p, d in
+                        empty_stateo s &
+                        p == [] &
+                        d == FunDecl ([], []) &
+                        eval_fun_empty_argso s p d q })
+  (fun q -> q#reify (St.prj_exn))))
 
 (* fun eval test *)
-(* let fun_eval_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> (* let open Prog in *) *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [] & *)
-                        (* d == FunDecl ([wi_val], [Write 0; Read 0]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let fun_eval_t2 _ = show(answer) (Stream.take (run q
+  (fun q -> (* let open Prog in *)
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren { fresh s, p, d in
+                        empty_stateo s &
+                        p == [] &
+                        d == FunDecl ([wi_val], [Write 0; Read 0]) &
+                        eval_fun_empty_argso s p d q })
+  (fun q -> q#reify (St.prj_exn))))
 
 (* fun eval test *)
-(* let fun_eval_t3 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> (* let open Prog in *) *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-                        (* d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let fun_eval_t3 _ = show(answer) (Stream.take (run q
+  (fun q -> (* let open Prog in *)
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren { fresh s, p, d in
+                        empty_stateo s &
+                        p == [FunDecl ([wi_ref], [Write 0])] &
+                        d == FunDecl ([wi_val], [Call (0, [0]); Read 0]) &
+                        eval_fun_empty_argso s p d q })
+  (fun q -> q#reify (St.prj_exn))))
 
 (* fun eval test *)
-(* let fun_eval_t4 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> (* let open Prog in *) *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [FunDecl ([wi_ref], [Write 0])] & *)
-                        (* d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let fun_eval_t4 _ = show(answer) (Stream.take (run q
+  (fun q -> (* let open Prog in *)
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren { fresh s, p, d in
+                        empty_stateo s &
+                        p == [FunDecl ([wi_ref], [Write 0])] &
+                        d == FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]) &
+                        eval_fun_empty_argso s p d q })
+  (fun q -> q#reify (St.prj_exn))))
 
 (* fun eval test *)
-(* let fun_eval_t5 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> (* let open Prog in *) *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] & *)
-                        (* d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let fun_eval_t5 _ = show(answer) (Stream.take (run q
+  (fun q -> (* let open Prog in *)
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren { fresh s, p, d in
+                        empty_stateo s &
+                        p == [FunDecl ([wi_ref; wi_ref], [Write 0; Write 1])] &
+                        d == FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]) &
+                        eval_fun_empty_argso s p d q })
+  (fun q -> q#reify (St.prj_exn))))
 
 (* fun eval test *)
-(* let fun_eval_t6 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> (* let open Prog in *) *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren { fresh s, p, d in *)
-                        (* empty_stateo s & *)
-                        (* p == [FunDecl ([wi_val], [Write 0])] & *)
-                        (* d == FunDecl ([wi_val], [Call (0, [0])]) & *)
-                        (* eval_fun_empty_argso s p d q }) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let fun_eval_t6 _ = show(answer) (Stream.take (run q
+  (fun q -> (* let open Prog in *)
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren { fresh s, p, d in
+                        empty_stateo s &
+                        p == [FunDecl ([wi_val], [Write 0])] &
+                        d == FunDecl ([wi_val], [Call (0, [0])]) &
+                        eval_fun_empty_argso s p d q })
+  (fun q -> q#reify (St.prj_exn))))
 
 (* prog eval test *)
-(* let prog_eval_t1 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let prog_eval_t1 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([], FunDecl ([wi_val], [Write 0; Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-(* let prog_eval_t2 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])], *)
-                                       (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let prog_eval_t2 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0; Read 0])],
+                                       FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-(* let prog_eval_t3 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])], *)
-                                       (* FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let prog_eval_t3 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Read 0])],
+                                       FunDecl ([wi_val], [Write 0; Read 0; Call (0, [0])]))) q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-(* let prog_eval_t4 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])], *)
-                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let prog_eval_t4 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-(* let prog_eval_t5 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])], *)
-                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let prog_eval_t5 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([FunDecl ([wi_val], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* prog with func eval test *)
-(* let prog_eval_t6 _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])], *)
-                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let prog_eval_t6 _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([FunDecl ([ri_val], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))
 
 (* annotation gen prog test *)
-(* let synt_t1 _ = show(answerTag) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {i_any q & *)
-                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
-                                       (* FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q -> q#reify (Tag.prj_exn)))) *)
+let synt_t1 _ = show(answerTag) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {i_any q &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Read 0]))) (St ([], [], 0, [0]))})
+  (fun q -> q#reify (Tag.prj_exn))))
 
 (* annotation gen prog test *)
-(* let synt_t2 _ = show(answerTag) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {i_any q & is_not_reado q & *)
-                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
-                                       (* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q -> q#reify (Tag.prj_exn)))) *)
+let synt_t2 _ = show(answerTag) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {i_any q & is_not_reado q &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
+  (fun q -> q#reify (Tag.prj_exn))))
 
 (* annotation gen prog test *)
-(* let synt_t3 _ = show(answerTags) (Stream.take (run qr *)
-  (* (fun q r -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r & *)
-                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
-                                       (* FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)]))) *)
+let synt_t3 _ = show(answerTags) (Stream.take (run qr
+  (fun q r -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {i_any q & is_not_reado q & i_any r & is_not_reado r &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([r], [Call (0, [0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (Tag.prj_exn); r#reify (Tag.prj_exn)])))
 
 (* annotation gen prog test *)
-(* let synt_t4 _ = show(answerTags) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {i_any q & is_not_reado q & *)
-                     (* eval_progo (Prog ([FunDecl ([q], [Write 0])], *)
-                                       (* FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *) *)
+let synt_t4 _ = show(answerTags) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {i_any q & is_not_reado q &
+                     eval_progo (Prog ([FunDecl ([q], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1]); Write 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q -> [q#reify (Tag.prj_exn)]))) (* -> [Val] *)
 
 (* annotation gen prog test *)
-(* let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr *)
-  (* (fun q r -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {fresh q', r' in *)
-                     (* i_any q' & is_not_reado q' & *)
-                     (* i_any r' & is_not_reado r' & is_never_writeo r' & *)
-                     (* eq_copyo q' q & eq_copyo r' r & *)
-                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
-                                       (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
+let synt_t5 _ = show(answerCopyCaps) (Stream.take (run qr
+  (fun q r -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {fresh q', r' in
+                     i_any q' & is_not_reado q' &
+                     i_any r' & is_not_reado r' & is_never_writeo r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
 
 (* annotation gen prog test *)
-(* let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr *)
-  (* (fun q r -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {fresh q', r' in *)
-                     (* i_any q' & is_not_reado q' & *)
-                     (* i_any r' & is_not_reado r' & is_never_writeo r' & *)
-                     (* eq_copyo q' q & eq_copyo r' r & *)
-                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])], *)
-                                       (* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *) *)
+let synt_t6 _ = show(answerCopyCaps) (Stream.take (run qr
+  (fun q r -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {fresh q', r' in
+                     i_any q' & is_not_reado q' &
+                     i_any r' & is_not_reado r' & is_never_writeo r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) (* all variants *)
 
 (* annotation gen prog test *)
-(* let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr *)
-  (* (fun q r -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {fresh q', r' in *)
-                     (* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
-                     (* eq_copyo q' q & eq_copyo r' r & *)
-                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
-                                       (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
+let synt_t7 _ = show(answerCopyCaps) (Stream.take (run qr
+  (fun q r -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {fresh q', r' in
+                     i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
 
 (* annotation gen prog test *)
-(* let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr *)
-  (* (fun q r -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {fresh q', r' in *)
-                     (* i_any q' & is_not_reado q' & i_any r' & is_not_reado r' & *)
-                     (* eq_copyo q' q & eq_copyo r' r & *)
-                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])], *)
-                                       (* FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
+let synt_t8 _ = show(answerCopyCaps) (Stream.take (run qr
+  (fun q r -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {fresh q', r' in
+                     i_any q' & is_not_reado q' & i_any r' & is_not_reado r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Write 1])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [1; 0]); Write 0; Read 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
 
 (* annotation gen prog test *)
-(* let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr *)
-  (* (fun q r -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* let open St in *)
-            (* ocanren {fresh q', r' in *)
-                     (* i_any q' & is_not_reado q' & *)
-                     (* i_any r' & is_reado r' & is_never_writeo r' & *)
-                     (* eq_copyo q' q & eq_copyo r' r & *)
-                     (* eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])], *)
-                                       (* FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))}) *)
-  (* (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)]))) *)
+let synt_t9 _ = show(answerCopyCaps) (Stream.take (run qr
+  (fun q r -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            let open St in
+            ocanren {fresh q', r' in
+                     i_any q' & is_not_reado q' &
+                     i_any r' & is_reado r' & is_never_writeo r' &
+                     eq_copyo q' q & eq_copyo r' r &
+                     eval_progo (Prog ([FunDecl ([q'; r'], [Write 0; Read 1])],
+                                       FunDecl ([wi_val; wi_val], [Call (0, [0; 1]); Read 0; Read 1]))) (St ([], [], 0, [0]))})
+  (fun q r -> [q#reify (CopyCap.prj_exn); r#reify (CopyCap.prj_exn)])))
 
 (* TODO: FIXME: implement memoization cuts *)
 (* prog with recursive function call *)
-(* let rec_eval_t _ = show(answer) (Stream.take (run q *)
-  (* (fun q -> let open Prog in *)
-            (* let open FunDecl in *)
-            (* let open Tag in *)
-            (* let open Stmt in *)
-            (* ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])], *)
-                                       (* FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q}) *)
-  (* (fun q -> q#reify (St.prj_exn)))) *)
+let rec_eval_t _ = show(answer) (Stream.take (run q
+  (fun q -> let open Prog in
+            let open FunDecl in
+            let open Tag in
+            let open Stmt in
+            ocanren {eval_progo (Prog ([FunDecl ([wi_ref], [Write 0; Call (0, [0])])],
+                                       FunDecl ([wi_val], [Call (0, [0]); Write 0; Read 0]))) q})
+  (fun q -> q#reify (St.prj_exn))))