diff --git a/Makefile b/Makefile
index 1bb28078..07f53e90 100644
--- a/Makefile
+++ b/Makefile
@@ -3,6 +3,7 @@
 MAKEFILE_DIR:=$(dir $(realpath $(lastword $(MAKEFILE_LIST))))
 
 default: build exercises build/tutorial.html build/exercises.zip
+all: default
 
 clean:
 	rm -rf build TAGS
@@ -43,6 +44,10 @@ build/solutions/%: src/examples/%
 build/exercises.zip: $(EXERCISES)
 	cd build; zip -r exercises.zip exercises > /dev/null
 
+WORKING=$(wildcard src/examples/list_*.c)
+WORKING_AUX=$(patsubst src/examples/%, build/solutions/%, $(WORKING))
+temp: $(WORKING_AUX) build 
+#     build/tutorial.html 
 
 ##############################################################################
 # Check that the examples all run correctly 
diff --git a/NAMING-CONVENTIONS.md b/NAMING-CONVENTIONS.md
new file mode 100644
index 00000000..55051066
--- /dev/null
+++ b/NAMING-CONVENTIONS.md
@@ -0,0 +1,105 @@
+CN Naming Conventions
+---------------------
+
+This document describes our (Benjamin and Liz's) current best shot at
+a good set of conventions for naming identifiers in CN, based on
+numerous discussions and worked examples. Everything in the tutorial
+(in src/examples) follows these conventions. Future CN coders are
+encouraged to follow suit.
+
+# Principles
+
+- When similar concepts exist in both C and CN, they should be named
+  so that the correspondence is immediately obvious.
+     - In particular, the C and CN versions of a given data structure
+       should have very similar names.
+
+- In text, we use the modifiers _CN-level_ vs. _C-level_ to
+  distinguish the two worlds.
+
+# General conventions
+
+ ## For new code
+
+When writing both C and CN code from scratch (e.g., in the tutorial),
+aim for maximal correspondence between
+
+- In general, identifiers are written in `snake_case` (or
+  `Snake_Case`) rather than `camlCase` (or `CamlCase`).
+
+- C-level identifiers are `lowercase` wherever possible.
+
+- CN-level identifiers are `Uppercase_Consistently_Throughout`.
+
+- A CN identifier that represents the state of a mutable data
+  structure after some function returns should be named the same as
+  the starting state of the data structure, with an `_post` at the
+  end.
+      - E.g., The list copy function takes a linked list `l`
+        representing a sequence `L` and leaves `l` at the end pointing
+        to a final sequence `L_post` such that `L == L_post`.
+        (Moreover, it returns a new sequence `Ret` with `L == Ret`.)
+
+- Predicates that extract some structure from the heap should be named
+  the same as the structure they extract, plus the suffix `_At`.
+  E.g., the result type of the `Queue` predicate is also called
+  `Queue_At`.
+
+## For existing code
+
+In existing C codebases, uppercase-initial identifiers are often used
+for typedefs, structs, and enumerations.  We should choose a
+recommended standard convention for such cases -- e.g., "prefix
+CN-level identifiers with `CN` when needed to avoid confusion with
+C-level identifiers".  Some experimentation will be needed to see
+which convention we like best; this is left for future discussions.
+
+# Built-ins
+
+This proposal may ultimately suggest changing some built-ins for
+consistency.
+
+      - `i32` should change to `I32`, `u64` to `U64`
+      - `is_null` to `Is_null` (or `Is_Null`)
+
+*Discussion*: One point against this change is that CN currently tries
+to use names reminiscent of Rust (`i32`, `u64`, etc.).  I (BCP) do not
+personally find this argument persuasive -- internal consistency seems
+more important than miscellaeous points of similarity with some other
+language.  One way or the other, this will require a global decision.
+
+# Polymorphism
+
+One particularly tricky issue is how to name the "monomorphic
+instances" of "morally polymorphic" functions (i.e., whether to write
+`append__Int` or `append__List_Int` rather than just `append`).  On
+one hand, `append__Int` is "more correct".  On the other hand, these
+extra annotations can get pretty heavy.
+
+We propose a compromise:
+
+1. If a project needs to use two or more instances of some polymorphic
+   type, then the names of the C and CN types, the C and CN functions
+   operating over them, and the CN predicates describing them are all
+   suffixed with `__xxx`, where `xxx` is the appropriate "type
+   argument".  E.g., if some codebase uses lists of both signed and
+   unsigned 32-bit ints, then we would use names like this:
+      - `list__int` / `list__uint`
+      - `append__int` / `append__uint`
+      - `List__I32` / `List__U32`
+      - `Cons__I32` / `Cons__U32`
+      - etc.
+
+2. However, if, in a given project, a set of "morally polymorphic"
+   type definitions and library functions is *only used at one
+   monomorphic instance* (e.g., if some codebase only ever uses lists
+   of 32-bit signed ints), then the `__int` or `__I32` annotations are
+   omitted.
+
+   This convention is used in the CN tutorial, for example.
+
+*Discussion*: One downside of this convention is that it might
+sometimes require some after-the-fact renaming: If a project starts
+out using just lists of signed ints and later needs to introduce lists
+of unsigned ints, the old signed operations will need to be renamed.
+This seems like an acceptable cost for keeping things light.
diff --git a/src/example-archive/SAW/broken/error-cerberus/00001.swap.c b/src/example-archive/SAW/broken/error-cerberus/00001.swap.c
index 7b7169e1..d9ceae6b 100644
--- a/src/example-archive/SAW/broken/error-cerberus/00001.swap.c
+++ b/src/example-archive/SAW/broken/error-cerberus/00001.swap.c
@@ -75,7 +75,7 @@ let argmin_spec len = do {
 
 // NOTE: Another mistake I made was to use the override below.
 // This works for size a_len, but on the second time through the loop the override
-// doesn't match because the size of the list has changed!  Ultimately need a
+// doesn't match because the size of the ./headers.has changed!  Ultimately need a
 // loop here.
 
 {-/
diff --git a/src/example-archive/simple-examples/working/malloc_1.c b/src/example-archive/simple-examples/working/malloc_1.c
index cd837ed7..9259c221 100644
--- a/src/example-archive/simple-examples/working/malloc_1.c
+++ b/src/example-archive/simple-examples/working/malloc_1.c
@@ -3,19 +3,19 @@
 // malloc() is not defined by default in CN. We can define a fake malloc()
 // function that only works on ints.
 
-int *my_malloc_int()
+int *my_malloc__int()
 /*@ trusted; @*/
 /*@ ensures take New = Block<int>(return); @*/
 {}
 
-int *malloc_1()
+int *malloc__1()
 /*@ ensures 
       take New = Owned<int>(return);
       New == 7i32;
       *return == 7i32; @*/  // <-- Alternative syntax 
 {
   int *new;
-  new = my_malloc_int();
+  new = my_malloc__int();
   *new = 7; // Have to initialize the memory before it's owned
   return new;
 }
diff --git a/src/examples/3.c b/src/examples/3.c
deleted file mode 100644
index 0ce28df8..00000000
--- a/src/examples/3.c
+++ /dev/null
@@ -1,9 +0,0 @@
-void zero (int *p)
-/* --BEGIN-- */
-/*@ requires take v1 = Block<int>(p);
-    ensures take v2 = Owned<int>(p);
-@*/
-/* --END-- */
-{
-  *p = 0;
-}
diff --git a/src/examples/Dbl_Linked_List/add.c b/src/examples/Dbl_Linked_List/add.c
deleted file mode 100644
index b988d9a4..00000000
--- a/src/examples/Dbl_Linked_List/add.c
+++ /dev/null
@@ -1,35 +0,0 @@
-#include "./headers.h"
-
-// Adds after the given node and returns a pointer to the new node
-struct node *add(int element, struct node *n)
-/*@ requires take Before = Dll_at(n);
-    ensures  take After = Dll_at(return);
-
-             is_null(n) ? After == Dll { left: Seq_Nil{}, curr: Node(After), right: Seq_Nil{}}
-                        : After == Dll { left: Seq_Cons{head: Node(Before).data, tail: Left(Before)}, curr: Node(After), right: Right(Before)};
-@*/
-{
-    struct node *new_node = malloc_node();
-    new_node->data = element;
-    new_node->prev = 0;
-    new_node->next = 0;
-
-    if (n == 0) //empty list case
-    {
-        new_node->prev = 0;
-        new_node->next = 0;
-        return new_node;
-    } else { 
-        /*@ split_case(is_null(n->prev)); @*/
-        new_node->next = n->next;
-        new_node->prev = n;
-
-        if (n->next !=0) {
-            /*@ split_case(is_null(n->next->next)); @*/
-            n->next->prev = new_node;
-        }
-
-        n->next = new_node;
-        return new_node;
-    }
-}
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/add_orig.broken.c b/src/examples/Dbl_Linked_List/add_orig.broken.c
deleted file mode 100644
index f8b9b306..00000000
--- a/src/examples/Dbl_Linked_List/add_orig.broken.c
+++ /dev/null
@@ -1,27 +0,0 @@
-#include "./headers.h"
-
-// Adds after the given node and returns a pointer to the new node
-struct node *add(int element, struct node *n)
-{
-    struct node *new_node = malloc_node();
-    new_node->data = element;
-    new_node->prev = 0;
-    new_node->next = 0;
-
-    if (n == 0) //empty list case
-    {
-        new_node->prev = 0;
-        new_node->next = 0;
-        return new_node;
-    } else { 
-        new_node->next = n->next;
-        new_node->prev = n;
-
-        if (n->next !=0) {
-            n->next->prev = new_node;
-        }
-
-        n->next = new_node;
-        return new_node;
-    }
-}
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/c_types.h b/src/examples/Dbl_Linked_List/c_types.h
deleted file mode 100644
index 2e3e7f16..00000000
--- a/src/examples/Dbl_Linked_List/c_types.h
+++ /dev/null
@@ -1,5 +0,0 @@
-struct node {
-  int data;  
-  struct node* prev;
-  struct node* next;
-};
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/cn_types.h b/src/examples/Dbl_Linked_List/cn_types.h
deleted file mode 100644
index 59278fb2..00000000
--- a/src/examples/Dbl_Linked_List/cn_types.h
+++ /dev/null
@@ -1,6 +0,0 @@
-/*@
-datatype Dll {
-    Empty_Dll {},
-    Dll {datatype seq left, struct node curr, datatype seq right}
-}
-@*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/getters.h b/src/examples/Dbl_Linked_List/getters.h
deleted file mode 100644
index 9e180623..00000000
--- a/src/examples/Dbl_Linked_List/getters.h
+++ /dev/null
@@ -1,22 +0,0 @@
-/*@
-function (datatype seq) Right (datatype Dll L) {
-    match L {
-        Empty_Dll {} => { Seq_Nil{} }
-        Dll {left: _, curr: _, right: r} => { r }
-    }
-}
-
-function (datatype seq) Left (datatype Dll L) {
-    match L {
-        Empty_Dll {} => { Seq_Nil {} }
-        Dll {left: l, curr: _, right: _} => { l }
-    }
-}
-
-function (struct node) Node (datatype Dll L) {
-    match L {
-        Empty_Dll {} => {  default<struct node> }
-        Dll {left: _, curr: n, right: _} => { n }
-    }
-}
-@*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/malloc_free.h b/src/examples/Dbl_Linked_List/malloc_free.h
deleted file mode 100644
index 1937a5a3..00000000
--- a/src/examples/Dbl_Linked_List/malloc_free.h
+++ /dev/null
@@ -1,12 +0,0 @@
-extern struct node *malloc_node();
-/*@ spec malloc_node();
-    requires true;
-    ensures take u = Block<struct node>(return);
-            !ptr_eq(return,NULL);
-@*/ 
-
-extern void free_node (struct node *p);
-/*@ spec free_node(pointer p);
-    requires take u = Block<struct node>(p);
-    ensures true;
-@*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/node_and_int.h b/src/examples/Dbl_Linked_List/node_and_int.h
deleted file mode 100644
index faef87c7..00000000
--- a/src/examples/Dbl_Linked_List/node_and_int.h
+++ /dev/null
@@ -1,17 +0,0 @@
-struct node_and_int {
-  struct node* node;
-  int data;
-};
-
-extern struct node_and_int *malloc_node_and_int();
-/*@ spec malloc_node_and_int();
-    requires true;
-    ensures take u = Block<struct node_and_int>(return);
-            !ptr_eq(return,NULL);
-@*/ 
-
-extern void free_node_and_int (struct node_and_int *p);
-/*@ spec free_node_and_int(pointer p);
-    requires take u = Block<struct node_and_int>(p);
-    ensures true;
-@*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/predicates.h b/src/examples/Dbl_Linked_List/predicates.h
deleted file mode 100644
index a5353591..00000000
--- a/src/examples/Dbl_Linked_List/predicates.h
+++ /dev/null
@@ -1,36 +0,0 @@
-/*@
-predicate (datatype Dll) Dll_at (pointer p) {
-    if (is_null(p)) {
-        return Empty_Dll{};
-    } else {
-        take n = Owned<struct node>(p);
-        take Left = Own_Backwards(n.prev, p, n);
-        take Right = Own_Forwards(n.next, p, n);
-        return Dll{left: Left, curr: n, right: Right};
-    }
-}
-
-predicate (datatype seq) Own_Forwards(pointer p, pointer prev_pointer, struct node prev_node) {
-    if (is_null(p)) {
-        return Seq_Nil{};
-    } else {
-        take n = Owned<struct node>(p);
-        assert (ptr_eq(n.prev, prev_pointer));
-        assert(ptr_eq(prev_node.next, p));
-        take Right = Own_Forwards(n.next, p, n);
-        return Seq_Cons{head: n.data, tail: Right};
-    }
-}
-
-predicate (datatype seq) Own_Backwards(pointer p, pointer next_pointer, struct node next_node) {
-    if (is_null(p)) {
-        return Seq_Nil{};
-    } else {
-        take n = Owned<struct node>(p);
-        assert (ptr_eq(n.next, next_pointer));
-        assert(ptr_eq(next_node.prev, p));
-        take Left = Own_Backwards(n.prev, p, n);
-        return Seq_Cons{head: n.data, tail: Left};
-    }
-}
-@*/
\ No newline at end of file
diff --git a/src/examples/Dbl_Linked_List/remove.c b/src/examples/Dbl_Linked_List/remove.c
deleted file mode 100644
index 2a610db8..00000000
--- a/src/examples/Dbl_Linked_List/remove.c
+++ /dev/null
@@ -1,36 +0,0 @@
-#include "./headers.h"
-#include "./node_and_int.h"
-
-// removes the given node from the list and returns another pointer 
-// to somewhere in the list, or a null pointer if the list is empty.
-struct node_and_int *remove(struct node *n)
-/*@ requires !is_null(n);
-             take Before = Dll_at(n);
-             let del = Node(Before);
-    ensures  take ret = Owned<struct node_and_int>(return);
-             take After = Dll_at(ret.node);
-             ret.data == del.data;
-             (is_null(del.prev) && is_null(del.next)) ? After == Empty_Dll{}
-                 : (!is_null(del.next) ? After == Dll{left: Left(Before), curr: Node(After), right: tl(Right(Before))}
-                     : After == Dll{left: tl(Left(Before)), curr: Node(After), right: Right(Before)});
-@*/
-{
-    struct node *temp = 0;
-    if (n->prev != 0) {
-        /*@ split_case(is_null(n->prev->prev)); @*/
-        n->prev->next = n->next;
-        temp = n->prev;
-    }
-    if (n->next != 0) {
-        /*@ split_case(is_null(n->next->next)); @*/
-        n->next->prev = n->prev;
-        temp = n->next;
-    }
-
-    struct node_and_int *pair = malloc_node_and_int();
-    pair->node = temp;
-    pair->data = n->data;
-
-    free_node(n);       
-    return pair;
-}
diff --git a/src/examples/Dbl_Linked_List/singleton.c b/src/examples/Dbl_Linked_List/singleton.c
deleted file mode 100644
index 15c8fd8a..00000000
--- a/src/examples/Dbl_Linked_List/singleton.c
+++ /dev/null
@@ -1,13 +0,0 @@
-#include "./headers.h"
-
-struct node *singleton(int element)
-/*@ ensures take Ret = Dll_at(return);
-        Ret == Dll{left: Seq_Nil{}, curr: struct node{data: element, prev: NULL, next: NULL}, right: Seq_Nil{}};
-@*/
-{
-   struct node *n = malloc_node();
-   n->data = element;
-   n->prev = 0;
-   n->next = 0;
-   return n;
-}
\ No newline at end of file
diff --git a/src/examples/abs.c b/src/examples/abs.c
index 206ee580..79da4d60 100644
--- a/src/examples/abs.c
+++ b/src/examples/abs.c
@@ -7,8 +7,7 @@ int abs (int x)
 {
   if (x >= 0) {
     return x;
-  }
-  else {
+  } else {
     return -x;
   }
 }
diff --git a/src/examples/abs_mem.c b/src/examples/abs_mem.c
index 488c2992..978fefa0 100644
--- a/src/examples/abs_mem.c
+++ b/src/examples/abs_mem.c
@@ -2,8 +2,8 @@ int abs_mem (int *p)
 /* --BEGIN-- */
 /*@ requires take x = Owned<int>(p);
              MINi32() < x;
-    ensures take x2 = Owned<int>(p);
-            x == x2;
+    ensures take x_post = Owned<int>(p);
+            x == x_post;
             return == ((x >= 0i32) ? x : (0i32-x));
 @*/
 /* --END-- */
diff --git a/src/examples/add_0.c b/src/examples/add_0.c
index 56a35cfd..f0f52745 100644
--- a/src/examples/add_0.c
+++ b/src/examples/add_0.c
@@ -1,7 +1,7 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             -2147483648i64 <= sum; sum <= 2147483647i64; @*/
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64; @*/
 /* --END-- */
 {
   return x+y;
diff --git a/src/examples/add_1.c b/src/examples/add_1.c
index ebd141df..ac30ccc5 100644
--- a/src/examples/add_1.c
+++ b/src/examples/add_1.c
@@ -1,8 +1,8 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             -2147483648i64 <= sum; sum <= 2147483647i64;
-    ensures return == (i32) sum;
+/*@ requires let Sum = (i64) x + (i64) y;
+             -2147483648i64 <= Sum; Sum <= 2147483647i64;
+    ensures return == (i32) Sum;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/add_2.c b/src/examples/add_2.c
index 17339707..0afd69e0 100644
--- a/src/examples/add_2.c
+++ b/src/examples/add_2.c
@@ -1,8 +1,8 @@
 int add(int x, int y)
 /* --BEGIN-- */
-/*@ requires let sum = (i64) x + (i64) y;
-             (i64)MINi32() <= sum; sum <= (i64)MAXi32();
-    ensures return == (i32) sum;
+/*@ requires let Sum = (i64) x + (i64) y;
+             (i64)MINi32() <= Sum; Sum <= (i64)MAXi32();
+    ensures return == (i32) Sum;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/add_read.c b/src/examples/add_read.c
index c15c6484..2341bd04 100644
--- a/src/examples/add_read.c
+++ b/src/examples/add_read.c
@@ -1,10 +1,10 @@
 unsigned int add (unsigned int *p, unsigned int *q)
-/*@ requires take m = Owned<unsigned int>(p);
-             take n = Owned<unsigned int>(q);
-    ensures take m2 = Owned<unsigned int>(p);
-            take n2 = Owned<unsigned int>(q);
-            m == m2 && n == n2;
-            return == m + n;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P == P_post && Q == Q_post;
+            return == P + Q;
 @*/
 {
   unsigned int m = *p;
diff --git a/src/examples/add_two_array.c b/src/examples/add_two_array.c
index 799edaf7..70a8e5fc 100644
--- a/src/examples/add_two_array.c
+++ b/src/examples/add_two_array.c
@@ -1,12 +1,14 @@
 unsigned int array_read_two (unsigned int *p, int n, int i, int j)
 /* --BEGIN-- */
-/*@ requires take a1 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+/*@ requires take A = each(i32 k; 0i32 <= k && k < n) { 
+                        Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
              0i32 <= i && i < n;
              0i32 <= j && j < n;
              j != i;
-    ensures take a2 = each(i32 k; 0i32 <= k && k < n) { Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
-            a1 == a2;
-            return == a1[i] + a1[j];
+    ensures take A_post = each(i32 k; 0i32 <= k && k < n) { 
+                            Owned<unsigned int>(array_shift<unsigned int>(p,k)) };
+            A == A_post;
+            return == A[i] + A[j];
 @*/
 /* --END-- */
 {
diff --git a/src/examples/append.c b/src/examples/append.c
deleted file mode 100644
index ff3309a0..00000000
--- a/src/examples/append.c
+++ /dev/null
@@ -1,19 +0,0 @@
-#include "list.h"
-#include "list_append.h"
-
-struct int_list* IntList_append(struct int_list* xs, struct int_list* ys)
-/*@ requires take L1 = IntList(xs); @*/
-/*@ requires take L2 = IntList(ys); @*/
-/*@ ensures take L3 = IntList(return); @*/
-/*@ ensures L3 == append(L1, L2); @*/
-{
-  if (xs == 0) {
-    /*@ unfold append(L1, L2); @*/
-    return ys;
-  } else {
-    /*@ unfold append(L1, L2); @*/
-    struct int_list *new_tail = IntList_append(xs->tail, ys);
-    xs->tail = new_tail;
-    return xs;
-  }
-}
diff --git a/src/examples/append2.c b/src/examples/append2.c
deleted file mode 100644
index a966e428..00000000
--- a/src/examples/append2.c
+++ /dev/null
@@ -1,44 +0,0 @@
-#include "list.h"
-#include "list_append.h"
-
-struct int_list* IntList_copy (struct int_list *xs)
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            take L2 = IntList(return);
-            L1 == L1_;
-            L1 == L2;
-@*/
-{
-  if (xs == 0) {
-    return IntList_nil();
-  } else {
-    struct int_list *new_tail = IntList_copy(xs->tail);
-    return IntList_cons(xs->head, new_tail);
-  }
-}
-
-struct int_list* IntList_append2 (struct int_list *xs, struct int_list *ys)
-/* --BEGIN-- */
-/*@ requires take L1 = IntList(xs); @*/
-/*@ requires take L2 = IntList(ys); @*/
-/*@ ensures take L1_ = IntList(xs); @*/
-/*@ ensures take L2_ = IntList(ys); @*/
-/*@ ensures take L3 = IntList(return); @*/
-/*@ ensures L3 == append(L1, L2); @*/
-/*@ ensures L1 == L1_; @*/
-/*@ ensures L2 == L2_; @*/
-/* --END-- */
-{
-  if (xs == 0) {
-/* --BEGIN-- */
-    /*@ unfold append(L1, L2); @*/
-/* --END-- */
-    return IntList_copy(ys);
-  } else {
-/* --BEGIN-- */
-    /*@ unfold append(L1, L2); @*/
-/* --END-- */
-    struct int_list *new_tail = IntList_append2(xs->tail, ys);
-    return IntList_cons(xs->head, new_tail);
-  }
-}
diff --git a/src/examples/array_load.broken.c b/src/examples/array_load.broken.c
index 3f4b6e63..446072cf 100644
--- a/src/examples/array_load.broken.c
+++ b/src/examples/array_load.broken.c
@@ -1,7 +1,10 @@
 int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) };
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) };
              0i32 <= i && i < n; 
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { Owned<int>(array_shift<int>(p,j)) }; @*/
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) }; 
+@*/
 {
   return p[i];
 }
diff --git a/src/examples/array_load.c b/src/examples/array_load.c
index eef0dab2..6cd87216 100644
--- a/src/examples/array_load.c
+++ b/src/examples/array_load.c
@@ -1,9 +1,10 @@
 int read (int *p, int n, int i)
-/*@ requires take a1 = each(i32 j; 0i32 <= j && j < n) { 
-                          Owned<int>(array_shift<int>(p,j)) };
-             0i32 <= i && i < n;
-    ensures take a2 = each(i32 j; 0i32 <= j && j < n) { 
-                            Owned<int>(array_shift<int>(p,j)) }; @*/
+/*@ requires take A = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) };
+             0i32 <= i && i < n; 
+    ensures take A_post = each(i32 j; 0i32 <= j && j < n) { 
+                        Owned<int>(array_shift<int>(p,j)) }; 
+@*/
 {
   /*@ extract Owned<int>, i; @*/
   return p[i];
diff --git a/src/examples/dll/add.c b/src/examples/dll/add.c
new file mode 100644
index 00000000..2962a820
--- /dev/null
+++ b/src/examples/dll/add.c
@@ -0,0 +1,42 @@
+#include "./headers.h"
+
+// Adds after the given node and returns a pointer to the new node
+struct dllist *add(int element, struct dllist *n)
+/*@ requires take Before = Dll_at(n);
+    ensures  take After = Dll_at(return);
+             is_null(n) ? 
+                After == Nonempty_Dll { 
+                           left: Nil{}, 
+                           curr: Node(After), 
+                           right: Nil{}}
+              : After == Nonempty_Dll { 
+                           left: Cons {Head: Node(Before).data, 
+                                       Tail: Left_Sublist(Before)}, 
+                           curr: Node(After), 
+                           right: Right_Sublist(Before)};
+@*/
+{
+    struct dllist *new_dllist = malloc__dllist();
+    new_dllist->data = element;
+    new_dllist->prev = 0;
+    new_dllist->next = 0;
+
+    if (n == 0) //empty list case
+    {
+        new_dllist->prev = 0;
+        new_dllist->next = 0;
+        return new_dllist;
+    } else { 
+        /*@ split_case(is_null(n->prev)); @*/
+        new_dllist->next = n->next;
+        new_dllist->prev = n;
+
+        if (n->next != 0) {
+            /*@ split_case(is_null(n->next->next)); @*/
+            n->next->prev = new_dllist;
+        }
+
+        n->next = new_dllist;
+        return new_dllist;
+    }
+}
diff --git a/src/examples/dll/add_orig.broken.c b/src/examples/dll/add_orig.broken.c
new file mode 100644
index 00000000..8d23ea48
--- /dev/null
+++ b/src/examples/dll/add_orig.broken.c
@@ -0,0 +1,27 @@
+#include "./headers.h"
+
+// Adds after the given node and returns a pointer to the new node
+struct dllist *add(int element, struct dllist *n)
+{
+    struct dllist *new_dllist = malloc__dllist();
+    new_dllist->data = element;
+    new_dllist->prev = 0;
+    new_dllist->next = 0;
+
+    if (n == 0) //empty list case
+    {
+        new_dllist->prev = 0;
+        new_dllist->next = 0;
+        return new_dllist;
+    } else { 
+        new_dllist->next = n->next;
+        new_dllist->prev = n;
+
+        if (n->next != 0) {
+            n->next->prev = new_dllist;
+        }
+
+        n->next = new_dllist;
+        return new_dllist;
+    }
+}
diff --git a/src/examples/dll/c_types.h b/src/examples/dll/c_types.h
new file mode 100644
index 00000000..9a7dc233
--- /dev/null
+++ b/src/examples/dll/c_types.h
@@ -0,0 +1,5 @@
+struct dllist {
+  int data;  
+  struct dllist* prev;
+  struct dllist* next;
+};
\ No newline at end of file
diff --git a/src/examples/dll/cn_types.h b/src/examples/dll/cn_types.h
new file mode 100644
index 00000000..479d3626
--- /dev/null
+++ b/src/examples/dll/cn_types.h
@@ -0,0 +1,8 @@
+/*@
+datatype Dll {
+    Empty_Dll    {},
+    Nonempty_Dll {datatype List left, 
+                  struct dllist curr, 
+                  datatype List right}
+}
+@*/
diff --git a/src/examples/dll/dllist_and_int.h b/src/examples/dll/dllist_and_int.h
new file mode 100644
index 00000000..229350e4
--- /dev/null
+++ b/src/examples/dll/dllist_and_int.h
@@ -0,0 +1,17 @@
+struct dllist_and_int {
+  struct dllist* dllist;
+  int data;
+};
+
+extern struct dllist_and_int *malloc__dllist_and_int();
+/*@ spec malloc__dllist_and_int();
+    requires true;
+    ensures take R = Block<struct dllist_and_int>(return);
+            !ptr_eq(return,NULL);
+@*/ 
+
+extern void free__dllist_and_int (struct dllist_and_int *p);
+/*@ spec free__dllist_and_int(pointer p);
+    requires take R = Block<struct dllist_and_int>(p);
+    ensures true;
+@*/
diff --git a/src/examples/dll/getters.h b/src/examples/dll/getters.h
new file mode 100644
index 00000000..4f75bf23
--- /dev/null
+++ b/src/examples/dll/getters.h
@@ -0,0 +1,22 @@
+/*@
+function (datatype List) Right_Sublist (datatype Dll L) {
+    match L {
+        Empty_Dll {} => { Nil{} }
+        Nonempty_Dll {left: _, curr: _, right: r} => { r }
+    }
+}
+
+function (datatype List) Left_Sublist (datatype Dll L) {
+    match L {
+        Empty_Dll {} => { Nil {} }
+        Nonempty_Dll {left: l, curr: _, right: _} => { l }
+    }
+}
+
+function (struct dllist) Node (datatype Dll L) {
+    match L {
+        Empty_Dll {} => {  default<struct dllist> }
+        Nonempty_Dll {left: _, curr: n, right: _} => { n }
+    }
+}
+@*/
diff --git a/src/examples/Dbl_Linked_List/headers.h b/src/examples/dll/headers.h
similarity index 60%
rename from src/examples/Dbl_Linked_List/headers.h
rename to src/examples/dll/headers.h
index 963902fb..2a029dde 100644
--- a/src/examples/Dbl_Linked_List/headers.h
+++ b/src/examples/dll/headers.h
@@ -1,7 +1,6 @@
-#include "../list.h"
-#include "../list_append.h"
-#include "../list_rev.h"
-
+#include "../list/headers.h"
+#include "../list/append.h"
+#include "../list/rev.h"
 #include "./c_types.h"
 #include "./cn_types.h"
 #include "./getters.h"
diff --git a/src/examples/dll/malloc_free.h b/src/examples/dll/malloc_free.h
new file mode 100644
index 00000000..a18b81c6
--- /dev/null
+++ b/src/examples/dll/malloc_free.h
@@ -0,0 +1,12 @@
+extern struct dllist *malloc__dllist();
+/*@ spec malloc__dllist();
+    requires true;
+    ensures take R = Block<struct dllist>(return);
+            !ptr_eq(return,NULL);
+@*/ 
+
+extern void free__dllist (struct dllist *p);
+/*@ spec free__dllist(pointer p);
+    requires take R = Block<struct dllist>(p);
+    ensures true;
+@*/
diff --git a/src/examples/dll/predicates.h b/src/examples/dll/predicates.h
new file mode 100644
index 00000000..52a00a66
--- /dev/null
+++ b/src/examples/dll/predicates.h
@@ -0,0 +1,40 @@
+/*@
+predicate (datatype Dll) Dll_at (pointer p) {
+    if (is_null(p)) {
+        return Empty_Dll{};
+    } else {
+        take n = Owned<struct dllist>(p);
+        take L = Own_Backwards(n.prev, p, n);
+        take R = Own_Forwards(n.next, p, n);
+        return Nonempty_Dll{left: L, curr: n, right: R};
+    }
+}
+
+predicate (datatype List) Own_Forwards (pointer p, 
+                                        pointer prev_pointer, 
+                                        struct dllist prev_dllist) {
+    if (is_null(p)) {
+        return Nil{};
+    } else {
+        take P = Owned<struct dllist>(p);
+        assert (ptr_eq(P.prev, prev_pointer));
+        assert(ptr_eq(prev_dllist.next, p));
+        take T = Own_Forwards(P.next, p, P);
+        return Cons{Head: P.data, Tail: T};
+    }
+}
+
+predicate (datatype List) Own_Backwards (pointer p, 
+                                         pointer next_pointer, 
+                                         struct dllist next_dllist) {
+    if (is_null(p)) {
+        return Nil{};
+    } else {
+        take P = Owned<struct dllist>(p);
+        assert (ptr_eq(P.next, next_pointer));
+        assert(ptr_eq(next_dllist.prev, p));
+        take T = Own_Backwards(P.prev, p, P);
+        return Cons{Head: P.data, Tail: T};
+    }
+}
+@*/
diff --git a/src/examples/dll/remove.c b/src/examples/dll/remove.c
new file mode 100644
index 00000000..7c87360c
--- /dev/null
+++ b/src/examples/dll/remove.c
@@ -0,0 +1,42 @@
+#include "./headers.h"
+#include "./dllist_and_int.h"
+
+// Remove the given node from the list and returns another pointer 
+// to somewhere in the list, or a null pointer if the list is empty
+struct dllist_and_int *remove(struct dllist *n)
+/*@ requires !is_null(n);
+             take Before = Dll_at(n);
+             let Del = Node(Before);
+    ensures  take Ret = Owned<struct dllist_and_int>(return);
+             take After = Dll_at(Ret.dllist);
+             Ret.data == Del.data;
+             (is_null(Del.prev) && is_null(Del.next)) 
+               ? After == Empty_Dll{}
+               : (!is_null(Del.next) ? 
+                    After == Nonempty_Dll {left: Left_Sublist(Before), 
+                                           curr: Node(After), 
+                                           right: Tl(Right_Sublist(Before))}
+                   : After == Nonempty_Dll {left: Tl(Left_Sublist(Before)), 
+                                            curr: Node(After), 
+                                            right: Right_Sublist(Before)});
+@*/
+{
+    struct dllist *temp = 0;
+    if (n->prev != 0) {
+        /*@ split_case(is_null(n->prev->prev)); @*/
+        n->prev->next = n->next;
+        temp = n->prev;
+    }
+    if (n->next != 0) {
+        /*@ split_case(is_null(n->next->next)); @*/
+        n->next->prev = n->prev;
+        temp = n->next;
+    }
+
+    struct dllist_and_int *pair = malloc__dllist_and_int();
+    pair->dllist = temp;
+    pair->data = n->data;
+
+    free__dllist(n);       
+    return pair;
+}
diff --git a/src/examples/Dbl_Linked_List/remove_orig.broken.c b/src/examples/dll/remove_orig.broken.c
similarity index 63%
rename from src/examples/Dbl_Linked_List/remove_orig.broken.c
rename to src/examples/dll/remove_orig.broken.c
index b2617c69..ba1ff586 100644
--- a/src/examples/Dbl_Linked_List/remove_orig.broken.c
+++ b/src/examples/dll/remove_orig.broken.c
@@ -1,11 +1,11 @@
 #include "./headers.h"
-#include "./node_and_int.h"
+#include "./dllist_and_int.h"
 
 // removes the given node from the list and returns another pointer 
 // to somewhere in the list, or a null pointer if the list is empty.
-struct node_and_int *remove(struct node *n)
+struct dllist_and_int *remove(struct dllist *n)
 {
-    struct node *temp = 0;
+    struct dllist *temp = 0;
     if (n->prev != 0) {
         n->prev->next = n->next;
         temp = n->prev;
@@ -15,10 +15,10 @@ struct node_and_int *remove(struct node *n)
         temp = n->next;
     }
 
-    struct node_and_int *pair = malloc_node_and_int();
-    pair->node = temp;
+    struct dllist_and_int *pair = malloc__dllist_and_int();
+    pair->dllist = temp;
     pair->data = n->data;
 
-    free_node(n);       
+    free__dllist(n);       
     return pair;
 }
\ No newline at end of file
diff --git a/src/examples/dll/singleton.c b/src/examples/dll/singleton.c
new file mode 100644
index 00000000..31679c9f
--- /dev/null
+++ b/src/examples/dll/singleton.c
@@ -0,0 +1,18 @@
+#include "./headers.h"
+
+struct dllist *singleton(int element)
+/*@ ensures take Ret = Dll_at(return);
+        Ret == Nonempty_Dll {
+                 left: Nil{}, 
+                 curr: struct dllist {prev: NULL, 
+                                      data: element, 
+                                      next: NULL}, 
+                 right: Nil{}};
+@*/
+{
+   struct dllist *n = malloc__dllist();
+   n->data = element;
+   n->prev = 0;
+   n->next = 0;
+   return n;
+}
diff --git a/src/examples/free.h b/src/examples/free.h
index 9643f4f3..b5eb5832 100644
--- a/src/examples/free.h
+++ b/src/examples/free.h
@@ -1,13 +1,13 @@
 extern void freeInt (int *p);
 /*@ spec freeInt(pointer p);
-    requires take v = Block<int>(p);
+    requires take P = Block<int>(p);
     ensures true;
 @*/
 
 
 extern void freeUnsignedInt (unsigned int *p);
 /*@ spec freeUnsignedInt(pointer p);
-    requires take v = Block<unsigned int>(p);
+    requires take P = Block<unsigned int>(p);
     ensures true;
 @*/
 
diff --git a/src/examples/init_array.c b/src/examples/init_array.c
index 5fb3c97a..b288cb1c 100644
--- a/src/examples/init_array.c
+++ b/src/examples/init_array.c
@@ -1,13 +1,17 @@
 void init_array (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+/*@ requires take A = each(u32 i; i < n) { 
+                         Owned<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take ai = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
-          {p} unchanged; {n} unchanged;
+  /*@ inv take Ai = each(u32 i; i < n) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          {p} unchanged; 
+          {n} unchanged;
   @*/
 /* --END-- */
   {
diff --git a/src/examples/init_array2.c b/src/examples/init_array2.c
index e1217845..f447f553 100644
--- a/src/examples/init_array2.c
+++ b/src/examples/init_array2.c
@@ -1,13 +1,17 @@
 void init_array2 (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Block<char>( array_shift<char>(p, i)) };
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+/*@ requires take A = each(u32 i; i < n) { 
+                        Block<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take al = each(u32 i; i < j) { Owned<char>( array_shift<char>(p, i)) };
-          take ar = each(u32 i; j <= i && i < n) { Block<char>( array_shift<char>(p, i)) };
+  /*@ inv take Al = each(u32 i; i < j) { 
+                      Owned<char>( array_shift<char>(p, i)) };
+          take Ar = each(u32 i; j <= i && i < n) { 
+                      Block<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           j <= n;
   @*/
diff --git a/src/examples/init_array_rev.c b/src/examples/init_array_rev.c
index dd8de2b7..e46b4f3f 100644
--- a/src/examples/init_array_rev.c
+++ b/src/examples/init_array_rev.c
@@ -1,14 +1,18 @@
-void init_array2 (char *p, unsigned int n)
-/*@ requires take a1 = each(u32 i; i < n) { Block<char>( array_shift<char>(p, i)) };
+void init_array_rev (char *p, unsigned int n)
+/*@ requires take A = each(u32 i; i < n) { 
+                        Block<char>( array_shift<char>(p, i)) };
     n > 0u32;
-    ensures  take a2 = each(u32 i; i < n) { Owned<char>( array_shift<char>(p, i)) };
+    ensures  take A_post = each(u32 i; i < n) { 
+                             Owned<char>( array_shift<char>(p, i)) };
 @*/
 {
   unsigned int j = 0;
   while (j < n)
 /* --BEGIN-- */
-  /*@ inv take al = each(u32 i; i < n-j) { Block<char>( array_shift<char>(p, i)) };
-          take ar = each(u32 i; n-j <= i && i < n) { Owned<char>( array_shift<char>(p, i)) };
+  /*@ inv take Al = each(u32 i; i < n-j) { 
+                      Block<char>( array_shift<char>(p, i)) };
+          take Ar = each(u32 i; n-j <= i && i < n) { 
+                      Owned<char>( array_shift<char>(p, i)) };
           {p} unchanged; {n} unchanged;
           0u32 <= j && j <= n;
   @*/
diff --git a/src/examples/init_point.c b/src/examples/init_point.c
index b907a950..4ecb67f3 100644
--- a/src/examples/init_point.c
+++ b/src/examples/init_point.c
@@ -1,18 +1,18 @@
-void zero (int *p) 
-/*@ requires take u = Block<int>(p);
-    ensures take v = Owned<int>(p);
-            v == 0i32; @*/
+void zero (int *coord) 
+/*@ requires take Coord = Block<int>(coord);
+    ensures take Coord_post = Owned<int>(coord);
+            Coord_post == 0i32; @*/
 {
-  *p = 0;
+  *coord = 0;
 }
 
 struct point { int x; int y; };
 
 void init_point(struct point *p) 
-/*@ requires take s = Block<struct point>(p);
-    ensures take s2 = Owned<struct point>(p);
-            s2.x == 0i32;
-            s2.y == 0i32;
+/*@ requires take P = Block<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == 0i32;
+            P_post.y == 0i32;
 @*/
 {
   zero(&p->x);
diff --git a/src/examples/list.h b/src/examples/list.h
deleted file mode 100644
index d93830dc..00000000
--- a/src/examples/list.h
+++ /dev/null
@@ -1,9 +0,0 @@
-#ifndef _LIST_H
-#define _LIST_H
-
-#include "list_c_types.h"
-#include "list_cn_types.h"
-#include "list_hdtl.h"
-#include "list_constructors.h"
-
-#endif //_LIST_H
diff --git a/src/examples/list/append.c b/src/examples/list/append.c
new file mode 100644
index 00000000..18f516c7
--- /dev/null
+++ b/src/examples/list/append.c
@@ -0,0 +1,19 @@
+#include "./headers.h"
+#include "./append.h"
+
+struct sllist* IntList_append(struct sllist* xs, struct sllist* ys)
+/*@ requires take L1 = SLList_At(xs);
+             take L2 = SLList_At(ys); @*/
+/*@ ensures take L3 = SLList_At(return);
+            L3 == Append(L1, L2); @*/
+{
+  if (xs == 0) {
+    /*@ unfold Append(L1, L2); @*/
+    return ys;
+  } else {
+    /*@ unfold Append(L1, L2); @*/
+    struct sllist *new_tail = IntList_append(xs->tail, ys);
+    xs->tail = new_tail;
+    return xs;
+  }
+}
diff --git a/src/examples/list/append.h b/src/examples/list/append.h
new file mode 100644
index 00000000..2c95a823
--- /dev/null
+++ b/src/examples/list/append.h
@@ -0,0 +1,12 @@
+/*@
+function [rec] (datatype List) Append(datatype List L1, datatype List L2) {
+  match L1 {
+    Nil {} => {
+      L2
+    }
+    Cons {Head : H, Tail : T}  => {
+      Cons {Head: H, Tail: Append(T, L2)}
+    }
+  }
+}
+@*/
diff --git a/src/examples/list/append2.c b/src/examples/list/append2.c
new file mode 100644
index 00000000..5b6979dd
--- /dev/null
+++ b/src/examples/list/append2.c
@@ -0,0 +1,44 @@
+#include "./headers.h"
+#include "./append.h"
+
+struct sllist* IntList_copy (struct sllist *xs)
+/*@ requires take Xs = SLList_At(xs);
+    ensures take Xs_post = SLList_At(xs);
+            take R = SLList_At(return);
+            Xs == Xs_post;
+            Xs == R;
+@*/
+{
+  if (xs == 0) {
+    return slnil();
+  } else {
+    struct sllist *new_tail = IntList_copy(xs->tail);
+    return slcons(xs->head, new_tail);
+  }
+}
+
+struct sllist* IntList_append2 (struct sllist *xs, struct sllist *ys)
+/* --BEGIN-- */
+/*@ requires take Xs = SLList_At(xs); @*/
+/*@ requires take Ys = SLList_At(ys); @*/
+/*@ ensures take Xs_post = SLList_At(xs); @*/
+/*@ ensures take Ys_post = SLList_At(ys); @*/
+/*@ ensures take Ret = SLList_At(return); @*/
+/*@ ensures Ret == Append(Xs, Ys); @*/
+/*@ ensures Xs == Xs_post; @*/
+/*@ ensures Ys == Ys_post; @*/
+/* --END-- */
+{
+  if (xs == 0) {
+/* --BEGIN-- */
+    /*@ unfold Append(Xs, Ys); @*/
+/* --END-- */
+    return IntList_copy(ys);
+  } else {
+/* --BEGIN-- */
+    /*@ unfold Append(Xs, Ys); @*/
+/* --END-- */
+    struct sllist *new_tail = IntList_append2(xs->tail, ys);
+    return slcons(xs->head, new_tail);
+  }
+}
diff --git a/src/examples/list/c_types.h b/src/examples/list/c_types.h
new file mode 100644
index 00000000..7caa03b3
--- /dev/null
+++ b/src/examples/list/c_types.h
@@ -0,0 +1,17 @@
+struct sllist {
+  int head;
+  struct sllist* tail;
+};
+
+extern struct sllist *malloc__sllist();
+/*@ spec malloc__sllist();
+    requires true;
+    ensures take R = Block<struct sllist>(return);
+@*/
+
+extern void free__sllist (struct sllist *p);
+/*@ spec free__sllist(pointer p);
+    requires take P = Block<struct sllist>(p);
+    ensures true;
+@*/
+
diff --git a/src/examples/list/cn_types.h b/src/examples/list/cn_types.h
new file mode 100644
index 00000000..102923c5
--- /dev/null
+++ b/src/examples/list/cn_types.h
@@ -0,0 +1,16 @@
+/*@
+datatype List {
+  Nil {},
+  Cons {i32 Head, datatype List Tail}
+}
+
+predicate (datatype List) SLList_At(pointer p) {
+  if (is_null(p)) {
+    return Nil{};
+  } else {
+    take H = Owned<struct sllist>(p);
+    take T = SLList_At(H.tail);
+    return (Cons { Head: H.head, Tail: T });
+  }
+}
+@*/
diff --git a/src/examples/list/constructors.h b/src/examples/list/constructors.h
new file mode 100644
index 00000000..fdc2e343
--- /dev/null
+++ b/src/examples/list/constructors.h
@@ -0,0 +1,19 @@
+struct sllist* slnil()
+/*@ ensures take Ret = SLList_At(return);
+            Ret == Nil{};
+ @*/
+{
+  return 0;
+}
+
+struct sllist* slcons(int h, struct sllist* t)
+/*@ requires take T = SLList_At(t);
+    ensures take Ret = SLList_At(return);
+            Ret == Cons{ Head: h, Tail: T};
+ @*/
+{
+  struct sllist *p = malloc__sllist();
+  p->head = h;
+  p->tail = t;
+  return p;
+}
diff --git a/src/examples/list/copy.c b/src/examples/list/copy.c
new file mode 100644
index 00000000..f76e9a98
--- /dev/null
+++ b/src/examples/list/copy.c
@@ -0,0 +1,17 @@
+#include "./headers.h"
+
+struct sllist* slcopy (struct sllist *l)
+/*@ requires take L = SLList_At(l);
+    ensures take L_ = SLList_At(l);
+            take Ret = SLList_At(return);
+            L == L_;
+            L == Ret;
+@*/
+{
+  if (l == 0) {
+    return slnil();
+  } else {
+    struct sllist *new_tail = slcopy(l->tail);
+    return slcons(l->head, new_tail);
+  }
+}
diff --git a/src/examples/list/free.c b/src/examples/list/free.c
new file mode 100644
index 00000000..92e1037a
--- /dev/null
+++ b/src/examples/list/free.c
@@ -0,0 +1,14 @@
+#include "./headers.h"
+
+void free__rec_sllist(struct sllist* l)
+// You fill in the rest...
+/* --BEGIN-- */
+/*@ requires take L = SLList_At(l); @*/
+{
+  if (l == 0) {
+  } else {
+    free__rec_sllist(l->tail);
+    free__sllist(l);
+  }
+}
+/* --END-- */
diff --git a/src/examples/list/hdtl.h b/src/examples/list/hdtl.h
new file mode 100644
index 00000000..e36738ff
--- /dev/null
+++ b/src/examples/list/hdtl.h
@@ -0,0 +1,23 @@
+/*@
+function (i32) Hd (datatype List L) {
+  match L {
+    Nil {} => {
+      0i32
+    }
+    Cons {Head : H, Tail : _} => {
+      H
+    }
+  }
+}
+
+function (datatype List) Tl (datatype List L) {
+  match L {
+    Nil {} => {
+      Nil{}
+    }
+    Cons {Head : _, Tail : T} => {
+      T
+    }
+  }
+}
+@*/
diff --git a/src/examples/list/headers.h b/src/examples/list/headers.h
new file mode 100644
index 00000000..5f787e85
--- /dev/null
+++ b/src/examples/list/headers.h
@@ -0,0 +1,9 @@
+#ifndef _LIST_H
+#define _LIST_H
+
+#include "./c_types.h"
+#include "./cn_types.h"
+#include "./hdtl.h"
+#include "./constructors.h"
+
+#endif //_LIST_H
diff --git a/src/examples/list/length.c b/src/examples/list/length.c
new file mode 100644
index 00000000..0dc195cf
--- /dev/null
+++ b/src/examples/list/length.c
@@ -0,0 +1,38 @@
+#include "./headers.h"
+
+/* --BEGIN-- */
+/*@
+function [rec] (u32) Length(datatype List L) {
+  match L {
+    Nil {} => {
+      0u32
+    }
+    Cons {Head: H, Tail : T}  => {
+      1u32 + Length(T)
+    }
+  }
+}
+@*/
+
+/* --END-- */
+unsigned int length (struct sllist *l)
+/* --BEGIN-- */
+/*@ requires take L = SLList_At(l);
+    ensures take L_post = SLList_At(l);
+            L == L_post;
+            return == Length(L);
+@*/
+/* --END-- */
+{
+  if (l == 0) {
+/* --BEGIN-- */
+    /*@ unfold Length(L); @*/
+/* --END-- */
+    return 0;
+  } else {
+/* --BEGIN-- */
+    /*@ unfold Length(L); @*/
+/* --END-- */
+    return 1 + length(l->tail);
+  }
+}
diff --git a/src/examples/list/mergesort.c b/src/examples/list/mergesort.c
new file mode 100644
index 00000000..8a36b63b
--- /dev/null
+++ b/src/examples/list/mergesort.c
@@ -0,0 +1,134 @@
+#include "./headers.h"
+
+/*@
+function [rec] ({datatype List fst, datatype List snd}) 
+                 split (datatype List xs)
+{
+  match xs {
+    Nil {} => {
+      {fst: Nil{}, snd: Nil{}}
+    }
+    Cons {Head: h1, Tail: Nil{}} => {
+      {fst: Nil{}, snd: xs}
+    }
+    Cons {Head: h1, Tail: Cons {Head : h2, Tail : tl2 }} => {
+      let P = split(tl2);
+      {fst: Cons { Head: h1, Tail: P.fst},
+       snd: Cons { Head: h2, Tail: P.snd}}
+    }
+  }
+}
+
+function [rec] (datatype List) merge(datatype List xs, datatype List ys) {
+  match xs {
+      Nil {} => { ys }
+      Cons {Head: x, Tail: xs1} => {
+        match ys {
+          Nil {} => { xs }
+          Cons{ Head: y, Tail: ys1} => {
+            (x < y) ?
+              (Cons{ Head: x, Tail: merge(xs1, ys) })
+            : (Cons{ Head: y, Tail: merge(xs, ys1) })
+          }
+        }
+      }
+  }
+}
+
+function [rec] (datatype List) mergesort(datatype List xs) {
+  match xs {
+      Nil{} => { xs }
+      Cons{Head: x, Tail: Nil{}} => { xs }
+      Cons{Head: x, Tail: Cons{Head: y, Tail: zs}} => {
+        let P = split(xs);
+        let L1 = mergesort(P.fst);
+        let L2 = mergesort(P.snd);
+        merge(L1, L2)
+      }
+    }
+}
+@*/
+
+struct sllist_pair {
+  struct sllist* fst;
+  struct sllist* snd;
+};
+
+struct sllist_pair split(struct sllist *xs)
+/*@ requires take Xs = SLList_At(xs); @*/
+/*@ ensures take Ys = SLList_At(return.fst); @*/
+/*@ ensures take Zs = SLList_At(return.snd); @*/
+/*@ ensures {fst: Ys, snd: Zs} == split(Xs); @*/
+{
+  if (xs == 0) {
+    /*@ unfold split(Xs); @*/
+    struct sllist_pair r = {.fst = 0, .snd = 0};
+    return r;
+  } else {
+    struct sllist *cdr = xs -> tail;
+    if (cdr == 0) {
+      /*@ unfold split(Xs); @*/
+      struct sllist_pair r = {.fst = 0, .snd = xs};
+      return r;
+    } else {
+      /*@ unfold split(Xs); @*/
+      struct sllist_pair p = split(cdr->tail);
+      xs->tail = p.fst;
+      cdr->tail = p.snd;
+      struct sllist_pair r = {.fst = xs, .snd = cdr};
+      return r;
+    }
+  }
+}
+
+struct sllist* merge(struct sllist *xs, struct sllist *ys)
+/*@ requires take Xs = SLList_At(xs); @*/
+/*@ requires take Ys = SLList_At(ys); @*/
+/*@ ensures take Zs = SLList_At(return); @*/
+/*@ ensures Zs == merge(Xs, Ys); @*/
+{
+  if (xs == 0) {
+    /*@ unfold merge(Xs, Ys); @*/
+    return ys;
+  } else {
+    /*@ unfold merge(Xs, Ys); @*/
+    if (ys == 0) {
+      /*@ unfold merge(Xs, Ys); @*/
+      return xs;
+    } else {
+      /*@ unfold merge(Xs, Ys); @*/
+      if (xs->head < ys->head) {
+        struct sllist *zs = merge(xs->tail, ys);
+        xs->tail = zs;
+        return xs;
+      } else {
+        struct sllist *zs = merge(xs, ys->tail);
+        ys->tail = zs;
+        return ys;
+      }
+    }
+  }
+}
+
+struct sllist* mergesort(struct sllist *xs)
+/*@ requires take Xs = SLList_At(xs); @*/
+/*@ ensures take Ys = SLList_At(return); @*/
+/*@ ensures Ys == mergesort(Xs); @*/
+{
+  if (xs == 0) {
+    /*@ unfold mergesort(Xs); @*/
+    return xs;
+  } else {
+    struct sllist *tail = xs->tail;
+    if (tail == 0) {
+      /*@ unfold mergesort(Xs); @*/
+      return xs;
+    } else {
+      /*@ unfold mergesort(Xs); @*/
+      struct sllist_pair p = split(xs);
+      p.fst = mergesort(p.fst);
+      p.snd = mergesort(p.snd);
+      return merge(p.fst, p.snd);
+    }
+  }
+}
diff --git a/src/examples/list/rev.c b/src/examples/list/rev.c
new file mode 100644
index 00000000..ee1b4eed
--- /dev/null
+++ b/src/examples/list/rev.c
@@ -0,0 +1,32 @@
+#include "./headers.h"
+#include "./append.h"
+#include "./rev.h"
+#include "./rev_lemmas.h"
+
+struct sllist* rev_aux(struct sllist* l1, struct sllist* l2)
+/*@ requires take L1 = SLList_At(l1); @*/
+/*@ requires take L2 = SLList_At(l2); @*/
+/*@ ensures take R = SLList_At(return); @*/
+/*@ ensures R == Append(RevList(L2), L1); @*/
+{
+  if (l2 == 0) {
+    /*@ unfold RevList(L2); @*/
+    /*@ unfold Append(Nil{}, L1); @*/
+    return l1;
+  } else {
+    /*@ unfold RevList(L2); @*/
+    /*@ apply Append_Cons_RList(RevList(Tl(L2)), Hd(L2), L1); @*/
+    struct sllist *tmp = l2->tail;
+    l2->tail = l1;
+    return rev_aux(l2, tmp);
+  }
+}
+
+struct sllist* rev(struct sllist* l1)
+/*@ requires take L1 = SLList_At(l1); @*/
+/*@ ensures take L1_Rev = SLList_At(return); @*/
+/*@ ensures L1_Rev == RevList(L1); @*/
+{
+  /*@ apply Append_Nil_RList(RevList(L1)); @*/
+  return rev_aux (0, l1);
+}
diff --git a/src/examples/list/rev.h b/src/examples/list/rev.h
new file mode 100644
index 00000000..a06e6342
--- /dev/null
+++ b/src/examples/list/rev.h
@@ -0,0 +1,14 @@
+#include "./snoc.h"
+
+/*@
+function [rec] (datatype List) RevList(datatype List L) {
+  match L {
+    Nil {} => {
+      Nil {}
+    }
+    Cons {Head : H, Tail : T}  => {
+      Snoc (RevList(T), H)
+    }
+  }
+}
+@*/
diff --git a/src/examples/list/rev_alt.c b/src/examples/list/rev_alt.c
new file mode 100644
index 00000000..6a651f32
--- /dev/null
+++ b/src/examples/list/rev_alt.c
@@ -0,0 +1,33 @@
+#include "./headers.h"
+#include "./append.h"
+#include "./rev.h"
+#include "./rev_lemmas.h"
+
+struct sllist* rev_loop(struct sllist *l)
+/*@ requires take L = SLList_At(l);
+    ensures  take L_post = SLList_At(return);
+             L_post == RevList(L);
+@*/
+{
+  struct sllist *last = 0;
+  struct sllist *cur = l;
+  /*@ apply Append_Nil_RList(RevList(L)); @*/
+  while(1)
+  /*@ inv take Last = SLList_At(last);
+          take Cur = SLList_At(cur);
+          Append(RevList(Cur), Last) == RevList(L);
+  @*/
+  {
+    if (cur == 0) {
+      /*@ unfold RevList(Nil{}); @*/
+      /*@ unfold Append(Nil{}, Last); @*/
+      return last;
+    }
+    struct sllist *tmp = cur->tail;
+    cur->tail = last;
+    last = cur;
+    cur = tmp;
+    /*@ unfold RevList(Cur); @*/
+    /*@ apply Append_Cons_RList(RevList(Tl(Cur)), Hd(Cur), Last); @*/
+  }
+}
diff --git a/src/examples/list/rev_lemmas.h b/src/examples/list/rev_lemmas.h
new file mode 100644
index 00000000..8e6dd044
--- /dev/null
+++ b/src/examples/list/rev_lemmas.h
@@ -0,0 +1,10 @@
+/*@
+lemma Append_Nil_RList (datatype List L1)
+  requires true;
+  ensures Append(L1, Nil{}) == L1;
+
+lemma Append_Cons_RList (datatype List L1, i32 X, datatype List L2)
+  requires true;
+  ensures Append(L1, Cons {Head: X, Tail: L2})
+          == Append(Snoc(L1, X), L2);
+@*/
diff --git a/src/examples/list/snoc.h b/src/examples/list/snoc.h
new file mode 100644
index 00000000..97a27f77
--- /dev/null
+++ b/src/examples/list/snoc.h
@@ -0,0 +1,12 @@
+/*@
+function [rec] (datatype List) Snoc(datatype List Xs, i32 Y) {
+  match Xs {
+    Nil {} => {
+      Cons {Head: Y, Tail: Nil{}}
+    }
+    Cons {Head: X, Tail: Zs}  => {
+      Cons{Head: X, Tail: Snoc (Zs, Y)}
+    }
+  }
+}
+@*/
diff --git a/src/examples/list_append.h b/src/examples/list_append.h
deleted file mode 100644
index d6305abb..00000000
--- a/src/examples/list_append.h
+++ /dev/null
@@ -1,14 +0,0 @@
-// append.h
-
-/*@
-function [rec] (datatype seq) append(datatype seq xs, datatype seq ys) {
-  match xs {
-    Seq_Nil {} => {
-      ys
-    }
-    Seq_Cons {head : h, tail : zs}  => {
-      Seq_Cons {head: h, tail: append(zs, ys)}
-    }
-  }
-}
-@*/
diff --git a/src/examples/list_c_types.h b/src/examples/list_c_types.h
deleted file mode 100644
index c9b6d7a0..00000000
--- a/src/examples/list_c_types.h
+++ /dev/null
@@ -1,17 +0,0 @@
-struct int_list {
-  int head;
-  struct int_list* tail;
-};
-
-extern struct int_list *mallocIntList();
-/*@ spec mallocIntList();
-    requires true;
-    ensures take u = Block<struct int_list>(return);
-@*/
-
-extern void freeIntList (struct int_list *p);
-/*@ spec freeIntList(pointer p);
-    requires take u = Block<struct int_list>(p);
-    ensures true;
-@*/
-
diff --git a/src/examples/list_cn_types.h b/src/examples/list_cn_types.h
deleted file mode 100644
index d45e6537..00000000
--- a/src/examples/list_cn_types.h
+++ /dev/null
@@ -1,16 +0,0 @@
-/*@
-datatype seq {
-  Seq_Nil {},
-  Seq_Cons {i32 head, datatype seq tail}
-}
-
-predicate (datatype seq) IntList(pointer p) {
-  if (is_null(p)) {
-    return Seq_Nil{};
-  } else {
-    take H = Owned<struct int_list>(p);
-    take tl = IntList(H.tail);
-    return (Seq_Cons { head: H.head, tail: tl });
-  }
-}
-@*/
diff --git a/src/examples/list_constructors.h b/src/examples/list_constructors.h
deleted file mode 100644
index 2108a861..00000000
--- a/src/examples/list_constructors.h
+++ /dev/null
@@ -1,19 +0,0 @@
-struct int_list* IntList_nil()
-/*@ ensures take ret = IntList(return);
-            ret == Seq_Nil{};
- @*/
-{
-  return 0;
-}
-
-struct int_list* IntList_cons(int h, struct int_list* t)
-/*@ requires take l = IntList(t);
-    ensures take ret = IntList(return);
-            ret == Seq_Cons{ head: h, tail: l};
- @*/
-{
-  struct int_list *p = mallocIntList();
-  p->head = h;
-  p->tail = t;
-  return p;
-}
diff --git a/src/examples/list_copy.c b/src/examples/list_copy.c
deleted file mode 100644
index 4a1f8ef6..00000000
--- a/src/examples/list_copy.c
+++ /dev/null
@@ -1,17 +0,0 @@
-#include "list.h"
-
-struct int_list* IntList_copy (struct int_list *xs)
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            take L2 = IntList(return);
-            L1 == L1_;
-            L1 == L2;
-@*/
-{
-  if (xs == 0) {
-    return IntList_nil();
-  } else {
-    struct int_list *new_tail = IntList_copy(xs->tail);
-    return IntList_cons(xs->head, new_tail);
-  }
-}
diff --git a/src/examples/list_free.c b/src/examples/list_free.c
deleted file mode 100644
index f1441f4b..00000000
--- a/src/examples/list_free.c
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "list.h"
-
-void IntList_free_list(struct int_list* xs)
-// You fill in the rest...
-/* --BEGIN-- */
-/*@ requires take L1 = IntList(xs); @*/
-{
-  if (xs == 0) {
-  } else {
-    IntList_free_list(xs->tail);
-    freeIntList(xs);
-  }
-}
-/* --END-- */
diff --git a/src/examples/list_hdtl.h b/src/examples/list_hdtl.h
deleted file mode 100644
index e92b51ed..00000000
--- a/src/examples/list_hdtl.h
+++ /dev/null
@@ -1,23 +0,0 @@
-/*@
-function (i32) hd (datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
-      0i32
-    }
-    Seq_Cons {head : h, tail : _} => {
-      h
-    }
-  }
-}
-
-function (datatype seq) tl (datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
-      Seq_Nil {}
-    }
-    Seq_Cons {head : _, tail : tail} => {
-      tail
-    }
-  }
-}
-@*/
diff --git a/src/examples/list_length.c b/src/examples/list_length.c
deleted file mode 100644
index 047b2c30..00000000
--- a/src/examples/list_length.c
+++ /dev/null
@@ -1,40 +0,0 @@
-/* list_length.c */
-
-#include "list.h"
-
-/* --BEGIN-- */
-/*@
-function [rec] (u32) length(datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
-      0u32
-    }
-    Seq_Cons {head : h, tail : zs}  => {
-      1u32 + length(zs)
-    }
-  }
-}
-@*/
-
-/* --END-- */
-unsigned int IntList_length (struct int_list *xs)
-/* --BEGIN-- */
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            L1 == L1_;
-            return == length(L1);
-@*/
-/* --END-- */
-{
-  if (xs == 0) {
-/* --BEGIN-- */
-    /*@ unfold length(L1); @*/
-/* --END-- */
-    return 0;
-  } else {
-/* --BEGIN-- */
-    /*@ unfold length(L1); @*/
-/* --END-- */
-    return 1 + IntList_length (xs->tail);
-  }
-}
diff --git a/src/examples/list_rev.c b/src/examples/list_rev.c
deleted file mode 100644
index 653ad0af..00000000
--- a/src/examples/list_rev.c
+++ /dev/null
@@ -1,32 +0,0 @@
-#include "list.h"
-#include "list_append.h"
-#include "list_rev.h"
-#include "list_rev_lemmas.h"
-
-struct int_list* IntList_rev_aux(struct int_list* xs, struct int_list* ys)
-/*@ requires take L1 = IntList(xs); @*/
-/*@ requires take L2 = IntList(ys); @*/
-/*@ ensures take R = IntList(return); @*/
-/*@ ensures R == append(rev(L2), L1); @*/
-{
-  if (ys == 0) {
-    /*@ unfold rev(L2); @*/
-    /*@ unfold append(Seq_Nil {},L1); @*/
-    return xs;
-  } else {
-    /*@ unfold rev(L2); @*/
-    /*@ apply append_cons_r(rev(tl(L2)), hd(L2), L1); @*/
-    struct int_list *tmp = ys->tail;
-    ys->tail = xs;
-    return IntList_rev_aux(ys, tmp);
-  }
-}
-
-struct int_list* IntList_rev(struct int_list* xs)
-/*@ requires take L1 = IntList(xs); @*/
-/*@ ensures take L1_rev = IntList(return); @*/
-/*@ ensures L1_rev == rev(L1); @*/
-{
-  /*@ apply append_nil_r(rev(L1)); @*/
-  return IntList_rev_aux (0, xs);
-}
diff --git a/src/examples/list_rev.h b/src/examples/list_rev.h
deleted file mode 100644
index 7260f3eb..00000000
--- a/src/examples/list_rev.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "list_snoc.h"
-
-/*@
-function [rec] (datatype seq) rev(datatype seq xs) {
-  match xs {
-    Seq_Nil {} => {
-      Seq_Nil {}
-    }
-    Seq_Cons {head : h, tail : zs}  => {
-      snoc (rev(zs), h)
-    }
-  }
-}
-@*/
diff --git a/src/examples/list_rev_alt.c b/src/examples/list_rev_alt.c
deleted file mode 100644
index 7cb4eaa5..00000000
--- a/src/examples/list_rev_alt.c
+++ /dev/null
@@ -1,33 +0,0 @@
-#include "list.h"
-#include "list_append.h"
-#include "list_rev.h"
-#include "list_rev_lemmas.h"
-
-struct int_list* IntList_rev_loop(struct int_list *xs)
-/*@ requires take L = IntList(xs);
-    ensures  take L_ = IntList(return);
-             L_ == rev(L);
-@*/
-{
-  struct int_list *last = 0;
-  struct int_list *cur = xs;
-  /*@ apply append_nil_r(rev(L)); @*/
-  while(1)
-  /*@ inv take L1 = IntList(last);
-          take L2 = IntList(cur);
-          append(rev(L2), L1) == rev(L);
-  @*/
-  {
-    if (cur == 0) {
-      /*@ unfold rev(Seq_Nil {}); @*/
-      /*@ unfold append(Seq_Nil {}, L1); @*/
-      return last;
-    }
-    struct int_list *tmp = cur->tail;
-    cur->tail = last;
-    last = cur;
-    cur = tmp;
-    /*@ unfold rev(L2); @*/
-    /*@ apply append_cons_r (rev (tl(L2)), hd(L2), L1); @*/
-  }
-}
diff --git a/src/examples/list_rev_lemmas.h b/src/examples/list_rev_lemmas.h
deleted file mode 100644
index 28f21937..00000000
--- a/src/examples/list_rev_lemmas.h
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-lemma append_nil_r (datatype seq l1)
-  requires true;
-  ensures append(l1, Seq_Nil {}) == l1;
-
-lemma append_cons_r (datatype seq l1, i32 x, datatype seq l2)
-  requires true;
-  ensures append(l1, Seq_Cons {head: x, tail: l2})
-          == append(snoc(l1, x), l2);
-@*/
diff --git a/src/examples/list_snoc.h b/src/examples/list_snoc.h
deleted file mode 100644
index 52cbdcb4..00000000
--- a/src/examples/list_snoc.h
+++ /dev/null
@@ -1,12 +0,0 @@
-/*@
-function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
-  match xs {
-    Seq_Nil {} => {
-      Seq_Cons {head: y, tail: Seq_Nil{}}
-    }
-    Seq_Cons {head: x, tail: zs}  => {
-      Seq_Cons{head: x, tail: snoc (zs, y)}
-    }
-  }
-}
-@*/
diff --git a/src/examples/liste_rev_lemmas.h b/src/examples/liste_rev_lemmas.h
deleted file mode 100644
index c4554e40..00000000
--- a/src/examples/liste_rev_lemmas.h
+++ /dev/null
@@ -1,10 +0,0 @@
-/*@
-lemma append_nil_r (datatype seq l1)
-  requires true
-  ensures append(l1, Seq_Nil {}) == l1
-
-lemma append_cons_r (datatype seq l1, i32 x, datatype seq l2)
-  requires true
-  ensures append(l1, Seq_Cons {head: x, tail: l2})
-          == append(snoc(l1, x), l2)
-@*/
diff --git a/src/examples/malloc.h b/src/examples/malloc.h
index 7182d1a2..fe2c2fc2 100644
--- a/src/examples/malloc.h
+++ b/src/examples/malloc.h
@@ -1,13 +1,12 @@
 extern int *mallocInt ();
 /*@ spec mallocInt();
     requires true;
-    ensures take v = Block<int>(return);
+    ensures take R = Block<int>(return);
 @*/
 
-
 extern unsigned int *mallocUnsignedInt ();
 /*@ spec mallocUnsignedInt();
     requires true;
-    ensures take v = Block<unsigned int>(return);
+    ensures take R = Block<unsigned int>(return);
 @*/
 
diff --git a/src/examples/mergesort.c b/src/examples/mergesort.c
deleted file mode 100644
index 5c6c13bd..00000000
--- a/src/examples/mergesort.c
+++ /dev/null
@@ -1,133 +0,0 @@
-#include "list.h"
-
-/*@
-function [rec] ({datatype seq fst, datatype seq snd}) split(datatype seq xs)
-{
-  match xs {
-    Seq_Nil {} => {
-      {fst: Seq_Nil{}, snd: Seq_Nil{}}
-    }
-    Seq_Cons {head: h1, tail: Seq_Nil{}} => {
-      {fst: Seq_Nil{}, snd: xs}
-    }
-    Seq_Cons {head: h1, tail: Seq_Cons {head : h2, tail : tl2 }} => {
-      let P = split(tl2);
-      {fst: Seq_Cons { head: h1, tail: P.fst},
-       snd: Seq_Cons { head: h2, tail: P.snd}}
-    }
-  }
-}
-
-function [rec] (datatype seq) merge(datatype seq xs, datatype seq ys) {
-  match xs {
-      Seq_Nil {} => { ys }
-      Seq_Cons {head: x, tail: xs1} => {
-        match ys {
-          Seq_Nil {} => { xs }
-          Seq_Cons{ head: y, tail: ys1} => {
-            (x < y) ?
-              (Seq_Cons{ head: x, tail: merge(xs1, ys) })
-            : (Seq_Cons{ head: y, tail: merge(xs, ys1) })
-          }
-        }
-      }
-  }
-}
-
-function [rec] (datatype seq) mergesort(datatype seq xs) {
-  match xs {
-      Seq_Nil{} => { xs }
-      Seq_Cons{head: x, tail: Seq_Nil{}} => { xs }
-      Seq_Cons{head: x, tail: Seq_Cons{head: y, tail: zs}} => {
-        let P = split(xs);
-        let L1 = mergesort(P.fst);
-        let L2 = mergesort(P.snd);
-        merge(L1, L2)
-      }
-    }
-}
-@*/
-
-struct int_list_pair {
-  struct int_list* fst;
-  struct int_list* snd;
-};
-
-struct int_list_pair split(struct int_list *xs)
-/*@ requires take Xs = IntList(xs); @*/
-/*@ ensures take Ys = IntList(return.fst); @*/
-/*@ ensures take Zs = IntList(return.snd); @*/
-/*@ ensures {fst: Ys, snd: Zs} == split(Xs); @*/
-{
-  if (xs == 0) {
-    /*@ unfold split(Xs); @*/
-    struct int_list_pair r = {.fst = 0, .snd = 0};
-    return r;
-  } else {
-    struct int_list *cdr = xs -> tail;
-    if (cdr == 0) {
-      /*@ unfold split(Xs); @*/
-      struct int_list_pair r = {.fst = 0, .snd = xs};
-      return r;
-    } else {
-      /*@ unfold split(Xs); @*/
-      struct int_list_pair p = split(cdr->tail);
-      xs->tail = p.fst;
-      cdr->tail = p.snd;
-      struct int_list_pair r = {.fst = xs, .snd = cdr};
-      return r;
-    }
-  }
-}
-
-struct int_list* merge(struct int_list *xs, struct int_list *ys)
-/*@ requires take Xs = IntList(xs); @*/
-/*@ requires take Ys = IntList(ys); @*/
-/*@ ensures take Zs = IntList(return); @*/
-/*@ ensures Zs == merge(Xs, Ys); @*/
-{
-  if (xs == 0) {
-    /*@ unfold merge(Xs, Ys); @*/
-    return ys;
-  } else {
-    /*@ unfold merge(Xs, Ys); @*/
-    if (ys == 0) {
-      /*@ unfold merge(Xs, Ys); @*/
-      return xs;
-    } else {
-      /*@ unfold merge(Xs, Ys); @*/
-      if (xs->head < ys->head) {
-        struct int_list *zs = merge(xs->tail, ys);
-        xs->tail = zs;
-        return xs;
-      } else {
-        struct int_list *zs = merge(xs, ys->tail);
-        ys->tail = zs;
-        return ys;
-      }
-    }
-  }
-}
-
-struct int_list* mergesort(struct int_list *xs)
-/*@ requires take Xs = IntList(xs); @*/
-/*@ ensures take Ys = IntList(return); @*/
-/*@ ensures Ys == mergesort(Xs); @*/
-{
-  if (xs == 0) {
-    /*@ unfold mergesort(Xs); @*/
-    return xs;
-  } else {
-    struct int_list *tail = xs->tail;
-    if (tail == 0) {
-      /*@ unfold mergesort(Xs); @*/
-      return xs;
-    } else {
-      /*@ unfold mergesort(Xs); @*/
-      struct int_list_pair p = split(xs);
-      p.fst = mergesort(p.fst);
-      p.snd = mergesort(p.snd);
-      return merge(p.fst, p.snd);
-    }
-  }
-}
diff --git a/src/examples/queue/allocation.h b/src/examples/queue/allocation.h
new file mode 100644
index 00000000..c507bf2e
--- /dev/null
+++ b/src/examples/queue/allocation.h
@@ -0,0 +1,23 @@
+extern struct queue *malloc_queue();
+/*@ spec malloc_queue();
+    requires true;
+    ensures take R = Block<struct queue>(return);
+@*/ 
+
+extern void free_queue (struct queue *p);
+/*@ spec free_queue(pointer p);
+    requires take P = Block<struct queue>(p);
+    ensures true;
+@*/
+
+extern struct queue_cell *malloc_queue_cell();
+/*@ spec malloc_queue_cell();
+    requires true;
+    ensures take R = Block<struct queue_cell>(return);
+@*/ 
+
+extern void free_queue_cell (struct queue_cell *p);
+/*@ spec free_queue_cell(pointer p);
+    requires take P = Block<struct queue_cell>(p);
+    ensures true;
+@*/
diff --git a/src/examples/queue/c_types.h b/src/examples/queue/c_types.h
new file mode 100644
index 00000000..9c915508
--- /dev/null
+++ b/src/examples/queue/c_types.h
@@ -0,0 +1,9 @@
+struct queue {
+  struct queue_cell* front;  
+  struct queue_cell* back;
+};
+
+struct queue_cell {
+  int first;  
+  struct queue_cell* next;
+};
diff --git a/src/examples/queue_cn_types_1.h b/src/examples/queue/cn_types_1.h
similarity index 50%
rename from src/examples/queue_cn_types_1.h
rename to src/examples/queue/cn_types_1.h
index 705eff65..9bc4e1d0 100644
--- a/src/examples/queue_cn_types_1.h
+++ b/src/examples/queue/cn_types_1.h
@@ -1,9 +1,9 @@
 /*@
-predicate (datatype seq) IntQueuePtr (pointer q) {
-  take Q = Owned<struct int_queue>(q);
+predicate (datatype List) QueuePtr_At (pointer q) {
+  take Q = Owned<struct queue>(q);
   assert (   (is_null(Q.front)  && is_null(Q.back)) 
           || (!is_null(Q.front) && !is_null(Q.back)));
-  take L = IntQueueFB(Q.front, Q.back);
+  take L = QueueFB(Q.front, Q.back);
   return L;
 }
 @*/
diff --git a/src/examples/queue/cn_types_2.h b/src/examples/queue/cn_types_2.h
new file mode 100644
index 00000000..b478b7e5
--- /dev/null
+++ b/src/examples/queue/cn_types_2.h
@@ -0,0 +1,13 @@
+/*@
+predicate (datatype List) QueueFB (pointer front, pointer back) {
+  if (is_null(front)) {
+    return Nil{};
+  } else {
+    take B = Owned<struct queue_cell>(back);
+    assert (is_null(B.next));
+    assert (ptr_eq(front, back) || !addr_eq(front, back));
+    take L = QueueAux (front, back);
+    return Snoc(L, B.first);
+  }
+}
+@*/
diff --git a/src/examples/queue/cn_types_3.h b/src/examples/queue/cn_types_3.h
new file mode 100644
index 00000000..73bfca7f
--- /dev/null
+++ b/src/examples/queue/cn_types_3.h
@@ -0,0 +1,13 @@
+/*@
+predicate (datatype List) QueueAux (pointer f, pointer b) {
+  if (ptr_eq(f,b)) {
+    return Nil{};
+  } else {
+    take F = Owned<struct queue_cell>(f);
+    assert (!is_null(F.next));  
+    assert (ptr_eq(F.next, b) || !addr_eq(F.next, b));
+    take B = QueueAux(F.next, b);
+    return Cons{Head: F.first, Tail: B};
+  }
+}
+@*/
diff --git a/src/examples/queue/empty.c b/src/examples/queue/empty.c
new file mode 100644
index 00000000..ccbd8119
--- /dev/null
+++ b/src/examples/queue/empty.c
@@ -0,0 +1,14 @@
+#include "./headers.h"
+
+struct queue* empty_queue ()
+/* --BEGIN-- */
+/*@ ensures take ret = QueuePtr_At(return);
+            ret == Nil{};
+@*/
+/* --END-- */
+{
+  struct queue *p = malloc_queue();
+  p->front = 0;
+  p->back = 0;
+  return p;
+}
diff --git a/src/examples/queue/headers.h b/src/examples/queue/headers.h
new file mode 100644
index 00000000..87fbffc7
--- /dev/null
+++ b/src/examples/queue/headers.h
@@ -0,0 +1,11 @@
+#include "../list/c_types.h"
+#include "../list/cn_types.h"
+#include "../list/hdtl.h"
+#include "../list/snoc.h"
+
+#include "./c_types.h"
+#include "./cn_types_1.h"
+#include "./cn_types_2.h" 
+#include "./cn_types_3.h" 
+
+#include "./allocation.h" 
diff --git a/src/examples/queue/pop.c b/src/examples/queue/pop.c
new file mode 100644
index 00000000..e840be00
--- /dev/null
+++ b/src/examples/queue/pop.c
@@ -0,0 +1,29 @@
+#include "./headers.h"
+#include "./pop_lemma.h"
+
+int pop_queue (struct queue *q)
+/*@ requires take Q = QueuePtr_At(q);
+             Q != Nil{};
+    ensures take Q_post = QueuePtr_At(q);
+            Q_post == Tl(Q);
+            return == Hd(Q);
+@*/
+{
+  /*@ split_case is_null(q->front); @*/
+  struct queue_cell* h = q->front;
+  if (h == q->back) {
+    /*@ assert ((alloc_id) h == (alloc_id) (q->back)); @*/
+    int x = h->first;
+    free_queue_cell(h);
+    q->front = 0;
+    q->back = 0;
+    /*@ unfold Snoc(Nil{}, x); @*/
+    return x;
+  } else {
+    int x = h->first;
+    /*@ apply snoc_facts(h->next, q->back, x); @*/
+    q->front = h->next;
+    free_queue_cell(h);
+    return x;
+  }
+}
diff --git a/src/examples/queue/pop_lemma.h b/src/examples/queue/pop_lemma.h
new file mode 100644
index 00000000..0188cda5
--- /dev/null
+++ b/src/examples/queue/pop_lemma.h
@@ -0,0 +1,13 @@
+/*@
+lemma snoc_facts (pointer front, pointer back, i32 x)
+  requires
+      take Q = QueueAux(front, back);
+      take B = Owned<struct queue_cell>(back);
+  ensures
+      take Q_post = QueueAux(front, back);
+      take B_post = Owned<struct queue_cell>(back);
+      Q == Q_post; B == B_post;
+      let L = Snoc (Cons{Head: x, Tail: Q}, B.first);
+      Hd(L) == x;
+      Tl(L) == Snoc (Q, B.first);
+@*/
diff --git a/src/examples/queue_pop_orig.broken.c b/src/examples/queue/pop_orig.broken.c
similarity index 52%
rename from src/examples/queue_pop_orig.broken.c
rename to src/examples/queue/pop_orig.broken.c
index ea203a7f..f6d28084 100644
--- a/src/examples/queue_pop_orig.broken.c
+++ b/src/examples/queue/pop_orig.broken.c
@@ -1,18 +1,18 @@
-#include "queue_headers.h"
+#include "./headers.h"
 
-int IntQueue_pop (struct int_queue *q)
+int pop_queue (struct queue *q)
 {
-  struct int_queueCell* h = q->front;
+  struct queue_cell* h = q->front;
   if (h == q->back) {
     int x = h->first;
-    freeIntQueueCell(h);
+    free_queue_cell(h);
     q->front = 0;
     q->back = 0;
     return x;
   } else {
     int x = h->first;
     q->front = h->next;
-    freeIntQueueCell(h);
+    free_queue_cell(h);
     return x;
   }
 }
diff --git a/src/examples/queue/pop_unified.c b/src/examples/queue/pop_unified.c
new file mode 100644
index 00000000..cecaa39b
--- /dev/null
+++ b/src/examples/queue/pop_unified.c
@@ -0,0 +1,71 @@
+#include "./headers.h"
+
+/*@
+type_synonym result = { datatype List after, datatype List before }
+
+predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) {
+  if (is_null(front)) {
+    return { after: Nil{}, before: Snoc(Nil{}, popped) };
+  } else {
+    take B = Owned<struct queue_cell>(back);
+    assert (is_null(B.next));
+    take L = QueueAux (front, back);
+    return { after: Snoc(L, B.first), before: Snoc(Cons {Head: popped, Tail: L}, B.first) };
+  }
+}
+@*/
+
+void snoc_fact(struct queue_cell *front, struct queue_cell *back, int x)
+/*@
+requires
+    take Q = QueueAux(front, back);
+    take B = Owned<struct queue_cell>(back);
+ensures
+    take Q_post = QueueAux(front, back);
+    take B_post = Owned<struct queue_cell>(back);
+    Q == Q_post; B == B_post;
+    let L = Snoc (Cons{Head: x, Tail: Q}, B.first);
+    Hd(L) == x;
+    Tl(L) == Snoc (Q, B.first);
+@*/
+{
+    /*@ unfold Snoc (Cons{Head: x, Tail: Q}, B.first); @*/
+}
+
+void snoc_fact_unified(struct queue_cell *front, struct queue_cell *back, int x)
+/*@
+requires
+      take AB = Queue_pop_lemma(front, back, x);
+ensures
+      take NewAB = Queue_pop_lemma(front, back, x);
+      AB == NewAB;
+      AB.after == Tl(AB.before);
+      x == Hd(AB.before);
+@*/
+{
+    if (!front) {
+        /*@ unfold Snoc(Nil{}, x); @*/
+    } else {
+        snoc_fact(front, back, x);
+    }
+}
+
+int pop_queue (struct queue *q)
+/*@ requires take before = QueuePtr_At(q);
+             before != Nil{};
+    ensures take after = QueuePtr_At(q);
+            after == Tl(before);
+            return == Hd(before);
+@*/
+{
+  /*@ split_case is_null(q->front); @*/
+  struct queue_cell* h = q->front;
+  /*@ split_case ptr_eq(h, q->back); @*/
+  int x = h->first;
+  q->front = h->next;
+  free_queue_cell(h);
+  if (!q->front) q->back = 0;
+  snoc_fact_unified(q->front, q->back, x);
+  return x;
+}
+
diff --git a/src/examples/queue/push.c b/src/examples/queue/push.c
new file mode 100644
index 00000000..19e27637
--- /dev/null
+++ b/src/examples/queue/push.c
@@ -0,0 +1,24 @@
+#include "./headers.h" 
+#include "./push_lemma.h" 
+
+void push_queue (int x, struct queue *q)
+/*@ requires take Q = QueuePtr_At(q);
+    ensures take Q_post = QueuePtr_At(q);
+            Q_post == Snoc (Q, x);
+@*/
+{
+  struct queue_cell *c = malloc_queue_cell();
+  c->first = x;
+  c->next = 0;
+  if (q->back == 0) {
+    q->front = c;
+    q->back = c;
+    return;
+  } else {
+    struct queue_cell *oldback = q->back;
+    q->back->next = c;
+    q->back = c;
+    /*@ apply push_lemma (q->front, oldback); @*/
+    return;
+  }
+}
diff --git a/src/examples/queue_push_induction.c b/src/examples/queue/push_induction.c
similarity index 50%
rename from src/examples/queue_push_induction.c
rename to src/examples/queue/push_induction.c
index dc1b012d..06c0117f 100644
--- a/src/examples/queue_push_induction.c
+++ b/src/examples/queue/push_induction.c
@@ -1,40 +1,40 @@
-#include "queue_headers.h" 
+#include "./headers.h" 
 
-void push_induction(struct int_queueCell* front
-        , struct int_queueCell* second_last
-        , struct int_queueCell* last)
+void push_induction(struct queue_cell* front
+        , struct queue_cell* second_last
+        , struct queue_cell* last)
 /*@
   requires
       ptr_eq(front, second_last) || !addr_eq(front, second_last);
-      take Q = IntQueueAux(front, second_last);
+      take Q = QueueAux(front, second_last);
       take Second_last = Owned(second_last);
       ptr_eq(Second_last.next, last);
       take Last = Owned(last);
   ensures
       ptr_eq(front, last) || !addr_eq(front, last);
-      take NewQ = IntQueueAux(front, last);
+      take Q_post = QueueAux(front, last);
       take Last2 = Owned(last);
-      NewQ == snoc(Q, Second_last.first);
+      Q_post == Snoc(Q, Second_last.first);
       Last == Last2;
 @*/
 {
     if (front == second_last) {
-        /*@ unfold snoc(Q, Second_last.first); @*/
+        /*@ unfold Snoc(Q, Second_last.first); @*/
         return;
     } else {
         push_induction(front->next, second_last, last);
-        /*@ unfold snoc(Q, Second_last.first); @*/
+        /*@ unfold Snoc(Q, Second_last.first); @*/
         return;
     }
 }
 
-void IntQueue_push (int x, struct int_queue *q)
-/*@ requires take before = IntQueuePtr(q);
-    ensures take after = IntQueuePtr(q);
-            after == snoc (before, x);
+void push_queue (int x, struct queue *q)
+/*@ requires take before = QueuePtr_At(q);
+    ensures take after = QueuePtr_At(q);
+            after == Snoc (before, x);
 @*/
 {
-  struct int_queueCell *c = mallocIntQueueCell();
+  struct queue_cell *c = malloc_queue_cell();
   c->first = x;
   c->next = 0;
   if (q->back == 0) {
@@ -42,7 +42,7 @@ void IntQueue_push (int x, struct int_queue *q)
     q->back = c;
     return;
   } else {
-    struct int_queueCell *oldback = q->back;
+    struct queue_cell *oldback = q->back;
     q->back->next = c;
     q->back = c;
     push_induction(q->front, oldback, c);
diff --git a/src/examples/queue_push_lemma.h b/src/examples/queue/push_lemma.h
similarity index 51%
rename from src/examples/queue_push_lemma.h
rename to src/examples/queue/push_lemma.h
index a93abe50..0692c1d0 100644
--- a/src/examples/queue_push_lemma.h
+++ b/src/examples/queue/push_lemma.h
@@ -2,10 +2,10 @@
 lemma push_lemma (pointer front, pointer p)
   requires
       ptr_eq(front, p) || !addr_eq(front, p);
-      take Q = IntQueueAux(front, p);
-      take P = Owned<struct int_queueCell>(p);
+      take Q = QueueAux(front, p);
+      take P = Owned<struct queue_cell>(p);
   ensures
       ptr_eq(front, P.next) || !addr_eq(front, P.next);
-      take NewQ = IntQueueAux(front, P.next);
-      NewQ == snoc(Q, P.first);
+      take Q_post = QueueAux(front, P.next);
+      Q_post == Snoc(Q, P.first);
 @*/
diff --git a/src/examples/queue_push_orig.broken.c b/src/examples/queue/push_orig.broken.c
similarity index 50%
rename from src/examples/queue_push_orig.broken.c
rename to src/examples/queue/push_orig.broken.c
index d342ef2b..97116c4a 100644
--- a/src/examples/queue_push_orig.broken.c
+++ b/src/examples/queue/push_orig.broken.c
@@ -1,8 +1,8 @@
-#include "queue_headers.h" 
+#include "./headers.h" 
 
-void IntQueue_push (int x, struct int_queue *q)
+void push_queue (int x, struct queue *q)
 {
-  struct int_queueCell *c = mallocIntQueueCell();
+  struct queue_cell *c = malloc_queue_cell();
   c->first = x;
   c->next = 0;
   if (q->back == 0) {
@@ -10,7 +10,7 @@ void IntQueue_push (int x, struct int_queue *q)
     q->back = c;
     return;
   } else {
-    struct int_queueCell *oldback = q->back;
+    struct queue_cell *oldback = q->back;
     q->back->next = c;
     q->back = c;
     return;
diff --git a/src/examples/queue_allocation.h b/src/examples/queue_allocation.h
deleted file mode 100644
index 6415601f..00000000
--- a/src/examples/queue_allocation.h
+++ /dev/null
@@ -1,23 +0,0 @@
-extern struct int_queue *mallocIntQueue();
-/*@ spec mallocIntQueue();
-    requires true;
-    ensures take u = Block<struct int_queue>(return);
-@*/ 
-
-extern void freeIntQueue (struct int_queue *p);
-/*@ spec freeIntQueue(pointer p);
-    requires take u = Block<struct int_queue>(p);
-    ensures true;
-@*/
-
-extern struct int_queueCell *mallocIntQueueCell();
-/*@ spec mallocIntQueueCell();
-    requires true;
-    ensures take u = Block<struct int_queueCell>(return);
-@*/ 
-
-extern void freeIntQueueCell (struct int_queueCell *p);
-/*@ spec freeIntQueueCell(pointer p);
-    requires take u = Block<struct int_queueCell>(p);
-    ensures true;
-@*/
diff --git a/src/examples/queue_c_types.h b/src/examples/queue_c_types.h
deleted file mode 100644
index bbc89972..00000000
--- a/src/examples/queue_c_types.h
+++ /dev/null
@@ -1,9 +0,0 @@
-struct int_queue {
-  struct int_queueCell* front;  
-  struct int_queueCell* back;
-};
-
-struct int_queueCell {
-  int first;  
-  struct int_queueCell* next;
-};
diff --git a/src/examples/queue_cn_types_2.h b/src/examples/queue_cn_types_2.h
deleted file mode 100644
index 440a2cb2..00000000
--- a/src/examples/queue_cn_types_2.h
+++ /dev/null
@@ -1,13 +0,0 @@
-/*@
-predicate (datatype seq) IntQueueFB (pointer front, pointer back) {
-  if (is_null(front)) {
-    return Seq_Nil{};
-  } else {
-    take B = Owned<struct int_queueCell>(back);
-    assert (is_null(B.next));
-    assert (ptr_eq(front, back) || !addr_eq(front, back));
-    take L = IntQueueAux (front, back);
-    return snoc(L, B.first);
-  }
-}
-@*/
diff --git a/src/examples/queue_cn_types_3.h b/src/examples/queue_cn_types_3.h
deleted file mode 100644
index 83deddf8..00000000
--- a/src/examples/queue_cn_types_3.h
+++ /dev/null
@@ -1,13 +0,0 @@
-/*@
-predicate (datatype seq) IntQueueAux (pointer f, pointer b) {
-  if (ptr_eq(f,b)) {
-    return Seq_Nil{};
-  } else {
-    take F = Owned<struct int_queueCell>(f);
-    assert (!is_null(F.next));
-    assert (ptr_eq(F.next, b) || !addr_eq(F.next, b));
-    take B = IntQueueAux(F.next, b);
-    return Seq_Cons{head: F.first, tail: B};
-  }
-}
-@*/
diff --git a/src/examples/queue_empty.c b/src/examples/queue_empty.c
deleted file mode 100644
index d2a8f3c7..00000000
--- a/src/examples/queue_empty.c
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "queue_headers.h"
-
-struct int_queue* IntQueue_empty ()
-/* --BEGIN-- */
-/*@ ensures take ret = IntQueuePtr(return);
-            ret == Seq_Nil{};
-@*/
-/* --END-- */
-{
-  struct int_queue *p = mallocIntQueue();
-  p->front = 0;
-  p->back = 0;
-  return p;
-}
diff --git a/src/examples/queue_headers.h b/src/examples/queue_headers.h
deleted file mode 100644
index 5b0d9b02..00000000
--- a/src/examples/queue_headers.h
+++ /dev/null
@@ -1,11 +0,0 @@
-#include "list_c_types.h"
-#include "list_cn_types.h"
-#include "list_hdtl.h"
-#include "list_snoc.h"
-
-#include "queue_c_types.h"
-#include "queue_cn_types_1.h"
-#include "queue_cn_types_2.h" 
-#include "queue_cn_types_3.h" 
-
-#include "queue_allocation.h" 
diff --git a/src/examples/queue_pop.c b/src/examples/queue_pop.c
deleted file mode 100644
index 56f8a87a..00000000
--- a/src/examples/queue_pop.c
+++ /dev/null
@@ -1,29 +0,0 @@
-#include "queue_headers.h"
-#include "queue_pop_lemma.h"
-
-int IntQueue_pop (struct int_queue *q)
-/*@ requires take before = IntQueuePtr(q);
-             before != Seq_Nil{};
-    ensures take after = IntQueuePtr(q);
-            after == tl(before);
-            return == hd(before);
-@*/
-{
-  /*@ split_case is_null(q->front); @*/
-  struct int_queueCell* h = q->front;
-  if (h == q->back) {
-    /*@ assert ((alloc_id) h == (alloc_id) (q->back)); @*/
-    int x = h->first;
-    freeIntQueueCell(h);
-    q->front = 0;
-    q->back = 0;
-    /*@ unfold snoc(Seq_Nil{}, x); @*/
-    return x;
-  } else {
-    int x = h->first;
-    /*@ apply snoc_facts(h->next, q->back, x); @*/
-    q->front = h->next;
-    freeIntQueueCell(h);
-    return x;
-  }
-}
diff --git a/src/examples/queue_pop_lemma.h b/src/examples/queue_pop_lemma.h
deleted file mode 100644
index 80d2ab90..00000000
--- a/src/examples/queue_pop_lemma.h
+++ /dev/null
@@ -1,13 +0,0 @@
-/*@
-lemma snoc_facts (pointer front, pointer back, i32 x)
-  requires
-      take Q = IntQueueAux(front, back);
-      take B = Owned<struct int_queueCell>(back);
-  ensures
-      take NewQ = IntQueueAux(front, back);
-      take NewB = Owned<struct int_queueCell>(back);
-      Q == NewQ; B == NewB;
-      let L = snoc (Seq_Cons{head: x, tail: Q}, B.first);
-      hd(L) == x;
-      tl(L) == snoc (Q, B.first);
-@*/
diff --git a/src/examples/queue_pop_lemma_stages.c b/src/examples/queue_pop_lemma_stages.c
deleted file mode 100644
index 66043b8d..00000000
--- a/src/examples/queue_pop_lemma_stages.c
+++ /dev/null
@@ -1,105 +0,0 @@
-#include "queue_headers.h"
-
-// Step 1: Understand the state we have upon lemma entry accurately.
-//         This is a sanity check that keeps your lemmas honest.
-
-/*@
-
-predicate (datatype seq) Pre(pointer front, pointer back, i32 popped, datatype seq before) {
-  if (is_null(front)) {
-    let after = Seq_Nil{};
-    assert (before == snoc(Seq_Nil{}, popped));
-    return after;
-  } else {
-    take B = Owned<struct int_queueCell>(back);
-    assert (is_null(B.next));
-    take L = IntQueueAux (front, back);
-    assert (before == snoc(Seq_Cons {head: popped, tail: L}, B.first));
-    let after = snoc(L, B.first);
-    return after;
-  }
-}
-
-lemma lemma1(pointer front, pointer back, i32 popped, datatype seq before)
-requires
-    take Q = Pre(front, back, popped, before);
-ensures
-    take NewQ = Pre(front, back, popped, before);
-    Q == NewQ;
-@*/
-
-// Step 2: Copy the state into the post-condition, adding the asserts the SMT solver can't manage.
-
-/*@
-
-predicate (datatype seq) Post(pointer front, pointer back, i32 popped, datatype seq before) {
-  if (is_null(front)) {
-    assert (before == snoc(Seq_Nil{}, popped));
-    let after = Seq_Nil{};
-    assert (after == tl(before));
-    assert (popped == hd(before));
-    return after;
-  } else {
-    take B = Owned<struct int_queueCell>(back);
-    assert (is_null(B.next));
-    take L = IntQueueAux (front, back);
-    assert (before == snoc(Seq_Cons {head: popped, tail: L}, B.first));
-    let after = snoc(L, B.first);
-    assert (after == tl(before));
-    assert (popped == hd(before));
-    return after;
-  }
-}
-
-lemma lemma2(pointer front, pointer back, i32 popped, datatype seq before)
-requires
-    take Q = Pre(front, back, popped, before);
-ensures
-    take NewQ = Post(front, back, popped, before);
-    Q == NewQ;
-@*/
-
-// Step 3: Expose the values of the predicate you wish to constrain as an output.
-//         Arguments used for only for the sanity check are now deleted from the predicate.
-//         Assertions are moved outside the predicate, and into the lemma.
-
-/*@
-
-type_synonym result = { datatype seq after, datatype seq before }
-
-predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) {
-  if (is_null(front)) {
-    return { after: Seq_Nil{}, before: snoc(Seq_Nil{}, popped) };
-  } else {
-    take B = Owned<struct int_queueCell>(back);
-    assert (is_null(B.next));
-    take L = IntQueueAux (front, back);
-    return { after: snoc(L, B.first), before: snoc(Seq_Cons {head: popped, tail: L}, B.first) };
-  }
-}
-
-lemma lemma3(pointer front, pointer back, i32 popped, datatype seq before)
-requires
-    take Q = Queue_pop_lemma(front, back, popped);
-    before == Q.before;
-ensures
-    take NewQ = Queue_pop_lemma(front, back, popped);
-    Q == NewQ;
-    Q.after == tl(Q.before);
-    popped == hd(Q.before);
-@*/
-
-// Step 4 (optional): Remove the sanity checking from the pre-condition.
-
-/*@
-
-lemma snoc_fact_unified(pointer front, pointer back, i32 popped)
-requires
-    take Q = Queue_pop_lemma(front, back, popped);
-ensures
-    take NewQ = Queue_pop_lemma(front, back, popped);
-    Q == NewQ;
-    Q.after == tl(Q.before);
-    popped == hd(Q.before);
-
-@*/
diff --git a/src/examples/queue_pop_unified.c b/src/examples/queue_pop_unified.c
deleted file mode 100644
index da0b8018..00000000
--- a/src/examples/queue_pop_unified.c
+++ /dev/null
@@ -1,71 +0,0 @@
-#include "queue_headers.h"
-
-/*@
-type_synonym result = { datatype seq after, datatype seq before }
-
-predicate (result) Queue_pop_lemma(pointer front, pointer back, i32 popped) {
-  if (is_null(front)) {
-    return { after: Seq_Nil{}, before: snoc(Seq_Nil{}, popped) };
-  } else {
-    take B = Owned<struct int_queueCell>(back);
-    assert (is_null(B.next));
-    take L = IntQueueAux (front, back);
-    return { after: snoc(L, B.first), before: snoc(Seq_Cons {head: popped, tail: L}, B.first) };
-  }
-}
-@*/
-
-void snoc_fact(struct int_queueCell *front, struct int_queueCell *back, int x)
-/*@
-requires
-    take Q = IntQueueAux(front, back);
-    take B = Owned<struct int_queueCell>(back);
-ensures
-    take NewQ = IntQueueAux(front, back);
-    take NewB = Owned<struct int_queueCell>(back);
-    Q == NewQ; B == NewB;
-    let L = snoc (Seq_Cons{head: x, tail: Q}, B.first);
-    hd(L) == x;
-    tl(L) == snoc (Q, B.first);
-@*/
-{
-    /*@ unfold snoc (Seq_Cons{head: x, tail: Q}, B.first); @*/
-}
-
-void snoc_fact_unified(struct int_queueCell *front, struct int_queueCell *back, int x)
-/*@
-requires
-      take AB = Queue_pop_lemma(front, back, x);
-ensures
-      take NewAB = Queue_pop_lemma(front, back, x);
-      AB == NewAB;
-      AB.after == tl(AB.before);
-      x == hd(AB.before);
-@*/
-{
-    if (!front) {
-        /*@ unfold snoc(Seq_Nil{}, x); @*/
-    } else {
-        snoc_fact(front, back, x);
-    }
-}
-
-int IntQueue_pop (struct int_queue *q)
-/*@ requires take before = IntQueuePtr(q);
-             before != Seq_Nil{};
-    ensures take after = IntQueuePtr(q);
-            after == tl(before);
-            return == hd(before);
-@*/
-{
-  /*@ split_case is_null(q->front); @*/
-  struct int_queueCell* h = q->front;
-  /*@ split_case ptr_eq(h, q->back); @*/
-  int x = h->first;
-  q->front = h->next;
-  freeIntQueueCell(h);
-  if (!q->front) q->back = 0;
-  snoc_fact_unified(q->front, q->back, x);
-  return x;
-}
-
diff --git a/src/examples/queue_push.c b/src/examples/queue_push.c
deleted file mode 100644
index 98e9826f..00000000
--- a/src/examples/queue_push.c
+++ /dev/null
@@ -1,24 +0,0 @@
-#include "queue_headers.h" 
-#include "queue_push_lemma.h" 
-
-void IntQueue_push (int x, struct int_queue *q)
-/*@ requires take before = IntQueuePtr(q);
-    ensures take after = IntQueuePtr(q);
-            after == snoc (before, x);
-@*/
-{
-  struct int_queueCell *c = mallocIntQueueCell();
-  c->first = x;
-  c->next = 0;
-  if (q->back == 0) {
-    q->front = c;
-    q->back = c;
-    return;
-  } else {
-    struct int_queueCell *oldback = q->back;
-    q->back->next = c;
-    q->back = c;
-    /*@ apply push_lemma(q->front, oldback); @*/
-    return;
-  }
-}
diff --git a/src/examples/read.c b/src/examples/read.c
index 5a09f6dd..04892f56 100644
--- a/src/examples/read.c
+++ b/src/examples/read.c
@@ -1,7 +1,7 @@
 int read (int *p)
 /* --BEGIN-- */
-/*@ requires take v1 = Owned<int>(p);
-    ensures take v2 = Owned<int>(p);
+/*@ requires take P = Owned<int>(p);
+    ensures take P_post = Owned<int>(p);
 @*/
 /* --END-- */
 {
diff --git a/src/examples/read2.c b/src/examples/read2.c
index d7fb90a7..94ca64ea 100644
--- a/src/examples/read2.c
+++ b/src/examples/read2.c
@@ -1,11 +1,9 @@
 int read (int *p)
-/* --BEGIN-- */
-/*@ requires take v1 = Owned<int>(p);
-    ensures take v2 = Owned<int>(p);
-            return == v1;
-            v1 == v2;
+/*@ requires take P = Owned<int>(p);
+    ensures take P_post = Owned<int>(p);
+            return == P;
+            P_post == P;
 @*/
-/* --END-- */
 {
   return *p;
 }
diff --git a/src/examples/ref.h b/src/examples/ref.h
index cbd68d5f..bbb83fa0 100644
--- a/src/examples/ref.h
+++ b/src/examples/ref.h
@@ -1,15 +1,14 @@
 extern unsigned int *refUnsignedInt (unsigned int v);
 /*@ spec refUnsignedInt(u32 v);
     requires true;
-    ensures take vr = Owned(return);
-            vr == v;
+    ensures take R = Owned(return);
+            R == v;
 @*/
 
-
 extern int *refInt (int v);
 /*@ spec refInt(i32 v);
     requires true;
-    ensures take vr = Owned(return);
-            vr == v;
+    ensures take R = Owned(return);
+            R == v;
 @*/
 
diff --git a/src/examples/runway/funcs2.c b/src/examples/runway/funcs2.c
index 635ae972..2b0fd609 100644
--- a/src/examples/runway/funcs2.c
+++ b/src/examples/runway/funcs2.c
@@ -20,7 +20,6 @@ struct State increment_Runway_Time(struct State s)
   return temp;
 }
 
-
 struct State reset_Runway_Time(struct State s)
 /* --BEGIN-- */
 /*@ requires valid_state(s);
@@ -49,8 +48,10 @@ struct State arrive(struct State s)
              s.ModeA == return.ModeA;
              s.ModeD == return.ModeD;
              s.W_D == return.W_D;
-             s.W_D == 0i32 implies s.Plane_Counter == return.Plane_Counter;
-             s.W_D > 0i32 implies s.Plane_Counter == return.Plane_Counter - 1i32;
+             s.W_D == 0i32 
+               implies s.Plane_Counter == return.Plane_Counter;
+             s.W_D > 0i32 
+               implies s.Plane_Counter == return.Plane_Counter - 1i32;
 @*/
 /* --END-- */
 {
@@ -117,7 +118,6 @@ struct State switch_modes(struct State s)
   return temp;
 }
 
-
 // This function represents what happens every minute at the airport. 
 // One `tick` corresponds to one minute.
 struct State tick(struct State s)
@@ -127,12 +127,13 @@ struct State tick(struct State s)
              (i64) s.W_A < 2147483647i64;
              (i64) s.W_D < 2147483647i64;
     ensures valid_state(return);
-            (s.W_A > 0i32 && s.W_D == 0i32 && s.Runway_Time == 0i32 implies return.ModeA == ACTIVE());
-            (s.W_D > 0i32 && s.W_A == 0i32 && s.Runway_Time == 0i32 implies return.ModeD == ACTIVE());
+            (s.W_A > 0i32 && s.W_D == 0i32 && s.Runway_Time == 0i32 
+               implies return.ModeA == ACTIVE());
+            (s.W_D > 0i32 && s.W_A == 0i32 && s.Runway_Time == 0i32 
+               implies return.ModeD == ACTIVE());
 @*/
 /* --END-- */
 {
-
     // Plane on the runway
     if (s.Runway_Time > 0)
     {
@@ -174,11 +175,9 @@ struct State tick(struct State s)
         s = reset_Plane_Counter(s);
         s = switch_modes(s);
 
-
         // If there are planes waiting to arrive, let one arrive
         if (s.W_A > 0) {
           s = arrive(s);
-          
           s = increment_Runway_Time(s);
         }
         return s;
@@ -202,4 +201,4 @@ struct State tick(struct State s)
         }
       }
     }
-}
\ No newline at end of file
+}
diff --git a/src/examples/runway/valid_state.h b/src/examples/runway/valid_state.h
index c36c7e73..b7e8b2e5 100644
--- a/src/examples/runway/valid_state.h
+++ b/src/examples/runway/valid_state.h
@@ -3,14 +3,17 @@ function (boolean) valid_state (struct State s) {
      (s.ModeA == INACTIVE() || s.ModeA == ACTIVE()) &&
      (s.ModeD == INACTIVE() || s.ModeD == ACTIVE()) &&
      (s.ModeA == INACTIVE() || s.ModeD == INACTIVE()) &&
+
      (s.W_A >= 0i32 && s.W_D >= 0i32) &&
      (0i32 <= s.Runway_Time && s.Runway_Time <= 5i32) && 
      (0i32 <= s.Plane_Counter && s.Plane_Counter <= 3i32) && 
-     (s.ModeA == INACTIVE() && s.ModeD == INACTIVE() implies s.Plane_Counter == 0i32) &&
-     (s.Runway_Time > 0i32 implies (s.ModeA == ACTIVE() || s.ModeD == ACTIVE())) &&
+
+     (s.ModeA == INACTIVE() && s.ModeD == INACTIVE() 
+        implies s.Plane_Counter == 0i32) &&
+     (s.Runway_Time > 0i32 
+        implies (s.ModeA == ACTIVE() || s.ModeD == ACTIVE())) &&
 
      (s.Plane_Counter > 0i32 && s.ModeA == ACTIVE() implies s.W_D > 0i32) &&
      (s.Plane_Counter > 0i32 && s.ModeD == ACTIVE() implies s.W_A > 0i32)
-
 }
-@*/
\ No newline at end of file
+@*/
diff --git a/src/examples/slf0_basic_incr.c b/src/examples/slf0_basic_incr.c
index f954c842..51aa8f43 100644
--- a/src/examples/slf0_basic_incr.c
+++ b/src/examples/slf0_basic_incr.c
@@ -1,10 +1,8 @@
 void incr (unsigned int *p)
-/* --BEGIN-- */
 /*@ requires take n1 = Owned<unsigned int>(p);
     ensures take n2 = Owned<unsigned int>(p);
             n2 == n1 + 1u32;
 @*/
-/* --END-- */
 {
   unsigned int n = *p;
   unsigned int m = n+1;
diff --git a/src/examples/slf0_basic_incr.signed.broken.c b/src/examples/slf0_basic_incr.signed.broken.c
index a4959035..3fbd627d 100644
--- a/src/examples/slf0_basic_incr.signed.broken.c
+++ b/src/examples/slf0_basic_incr.signed.broken.c
@@ -1,6 +1,6 @@
 void incr (int *p)
-/*@ requires take u = Block<int>(p); 
-    ensures take v = Owned<int>(p); 
+/*@ requires take P = Block<int>(p); 
+    ensures take P_post = Owned<int>(p); 
 @*/
 {
   *p = *p+1;
diff --git a/src/examples/slf0_basic_incr.signed.c b/src/examples/slf0_basic_incr.signed.c
index ae0656d5..2986c617 100644
--- a/src/examples/slf0_basic_incr.signed.c
+++ b/src/examples/slf0_basic_incr.signed.c
@@ -1,11 +1,9 @@
 void incr (int *p)
-/* --BEGIN-- */
-/*@ requires take v1 = Owned<int>(p);
-             ((i64) v1) + 1i64 <= (i64)MAXi32();
-    ensures take v2 = Owned<int>(p);
-            v2 == v1+1i32;
+/*@ requires take P = Owned<int>(p);
+             ((i64) P) + 1i64 <= (i64) MAXi32();
+    ensures take P_post = Owned<int>(p);
+            P_post == P + 1i32;
 @*/
-/* --END-- */
 {
   *p = *p+1;
 }
diff --git a/src/examples/slf17_get_and_free.c b/src/examples/slf17_get_and_free.c
index 8c6e59aa..a2238315 100644
--- a/src/examples/slf17_get_and_free.c
+++ b/src/examples/slf17_get_and_free.c
@@ -1,8 +1,9 @@
 #include "free.h"
 
 unsigned int get_and_free (unsigned int *p)
-/*@ requires take v1_ = Owned(p);
-    ensures return == v1_; @*/
+/*@ requires take P = Owned(p);
+    ensures return == P; 
+@*/
 {
   unsigned int v = *p;
   freeUnsignedInt (p);
diff --git a/src/examples/slf1_basic_example_let.signed.c b/src/examples/slf1_basic_example_let.signed.c
index c3102646..44064ebd 100644
--- a/src/examples/slf1_basic_example_let.signed.c
+++ b/src/examples/slf1_basic_example_let.signed.c
@@ -1,8 +1,8 @@
 int doubled (int n)
 /* --BEGIN-- */
-/*@ requires let n_ = (i64) n;
-             (i64)MINi32() <= n_ - 1i64; n_ + 1i64 <= (i64)MAXi32();
-             (i64)MINi32() <= n_ + n_; n_ + n_ <= (i64)MAXi32();
+/*@ requires let N = (i64) n;
+             (i64)MINi32() <= N - 1i64; N + 1i64 <= (i64)MAXi32();
+             (i64)MINi32() <= N + N; N + N <= (i64)MAXi32();
     ensures return == n * 2i32;
 @*/
 /* --END-- */
diff --git a/src/examples/slf2_basic_quadruple.signed.c b/src/examples/slf2_basic_quadruple.signed.c
index 23a1d495..92e71f5d 100644
--- a/src/examples/slf2_basic_quadruple.signed.c
+++ b/src/examples/slf2_basic_quadruple.signed.c
@@ -1,7 +1,7 @@
 int quadruple (int n)
 /* --BEGIN-- */
-/*@ requires let n_ = (i64) n;
-             (i64)MINi32() <= n_ * 4i64; n_ * 4i64 <= (i64)MAXi32();
+/*@ requires let N = (i64) n;
+             (i64)MINi32() <= N * 4i64; N * 4i64 <= (i64)MAXi32();
     ensures return == 4i32 * n;
  @*/
 /* --END-- */
diff --git a/src/examples/slf3_basic_inplace_double.c b/src/examples/slf3_basic_inplace_double.c
index 065a96f5..ca7cddde 100644
--- a/src/examples/slf3_basic_inplace_double.c
+++ b/src/examples/slf3_basic_inplace_double.c
@@ -1,10 +1,10 @@
 void inplace_double (int *p)
 /* --BEGIN-- */
-/*@ requires take n_ = Owned<int>(p);
-             let r = 2i64 * ((i64) n_);
-             (i64)MINi32() <= r; r <= (i64)MAXi32();
-    ensures  take m_ = Owned<int>(p);
-             m_ == (i32) r;
+/*@ requires take P = Owned<int>(p);
+             let M = 2i64 * ((i64) P);
+             (i64) MINi32() <= M; M <= (i64) MAXi32();
+    ensures  take P_post = Owned<int>(p);
+             P_post == (i32) M;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/slf8_basic_transfer.c b/src/examples/slf8_basic_transfer.c
index ffa37489..71a80c6a 100644
--- a/src/examples/slf8_basic_transfer.c
+++ b/src/examples/slf8_basic_transfer.c
@@ -1,11 +1,11 @@
 void transfer (unsigned int *p, unsigned int *q)
 /* --BEGIN-- */
-/*@ requires take n1 = Owned(p);
-             take m1 = Owned(q);
-    ensures  take n2 = Owned(p);
-             take m2 = Owned(q);
-             n2 == n1 + m1;
-             m2 == 0u32;
+/*@ requires take P = Owned(p);
+             take Q = Owned(q);
+    ensures  take P_post = Owned(p);
+             take Q_post = Owned(q);
+             P_post == P + Q;
+             Q_post == 0u32;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/slf_incr2.c b/src/examples/slf_incr2.c
index cd4b9c23..6ed25927 100644
--- a/src/examples/slf_incr2.c
+++ b/src/examples/slf_incr2.c
@@ -1,42 +1,42 @@
 /*@
-predicate { u32 pv, u32 qv } BothOwned (pointer p, pointer q)
+predicate { u32 P, u32 Q } BothOwned (pointer p, pointer q)
 {
   if (ptr_eq(p,q)) {
-    take pv = Owned<unsigned int>(p);
-    return {pv: pv, qv: pv};
+    take PX = Owned<unsigned int>(p);
+    return {P: PX, Q: PX};
   }
   else {
-    take pv = Owned<unsigned int>(p);
-    take qv = Owned<unsigned int>(q);
-    return {pv: pv, qv: qv};
+    take PX = Owned<unsigned int>(p);
+    take QX = Owned<unsigned int>(q);
+    return {P: PX, Q: QX};
   }
 }
 @*/
 
-void incr2 (unsigned int *p, unsigned int *q)
-/*@ requires take vs = BothOwned(p,q);
-    ensures take vs_ = BothOwned(p,q);
-            vs_.pv == (!ptr_eq(p,q) ? (vs.pv + 1u32) : (vs.pv + 2u32));
-            vs_.qv == (!ptr_eq(p,q) ? (vs.qv + 1u32) : vs_.pv);
+void incr2(unsigned int *p, unsigned int *q)
+/*@ requires take PQ = BothOwned(p,q);
+    ensures take PQ_post = BothOwned(p,q);
+            PQ_post.P == (!ptr_eq(p,q) ? (PQ.P + 1u32) : (PQ.P + 2u32));
+            PQ_post.Q == (!ptr_eq(p,q) ? (PQ.Q + 1u32) : PQ_post.P);
 @*/
 {
   /*@ split_case ptr_eq(p,q); @*/
   unsigned int n = *p;
-  unsigned int m = n+1;
+  unsigned int m = n + 1;
   *p = m;
   n = *q;
-  m = n+1;
+  m = n + 1;
   *q = m;
 }
 
-void call_both_better (unsigned int *p, unsigned int *q)
-/*@ requires take pv = Owned<unsigned int>(p);
-             take qv = Owned<unsigned int>(q);
+void call_both_better(unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
              !ptr_eq(p,q);
-    ensures take pv_ = Owned<unsigned int>(p);
-            take qv_ = Owned<unsigned int>(q);
-            pv_ == pv + 3u32;
-            qv_ == qv + 1u32;
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 3u32;
+            Q_post == Q + 1u32;
 @*/
 {
   incr2(p, q);
diff --git a/src/examples/slf_incr2_alias.c b/src/examples/slf_incr2_alias.c
index 2eff193b..2f8cd75c 100644
--- a/src/examples/slf_incr2_alias.c
+++ b/src/examples/slf_incr2_alias.c
@@ -1,9 +1,28 @@
+// Increment two different pointers (same as above)
+void incr2a (unsigned int *p, unsigned int *q)
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 1u32;
+            Q_post == Q + 1u32;
+@*/
+{
+  unsigned int n = *p;
+  unsigned int m = n+1;
+  *p = m;
+  n = *q;
+  m = n+1;
+  *q = m;
+}
+
+// Increment the same pointer twice
 void incr2b (unsigned int *p, unsigned int *q)
-/*@ requires take pv = Owned<unsigned int>(p);
+/*@ requires take P = Owned<unsigned int>(p);
              ptr_eq(q,p);
-    ensures take pv_ = Owned<unsigned int>(p);
+    ensures take P_post = Owned<unsigned int>(p);
             ptr_eq(q,p);
-            pv_ == pv + 2u32;
+            P_post == P + 2u32;
 @*/
 {
   unsigned int n = *p;
@@ -14,8 +33,6 @@ void incr2b (unsigned int *p, unsigned int *q)
   *q = m;
 }
 
-#include "slf_incr2_noalias.c"
-
 void call_both (unsigned int *p, unsigned int *q)
 /*@ requires take pv = Owned<unsigned int>(p);
              take qv = Owned<unsigned int>(q);
@@ -25,6 +42,6 @@ void call_both (unsigned int *p, unsigned int *q)
             qv_ == qv + 1u32;
 @*/
 {
-  incr2a(p, q);
-  incr2b(p, p);
+  incr2a(p, q);   // increment two different pointers
+  incr2b(p, p);   // increment the same pointer twice
 }
diff --git a/src/examples/slf_incr2_noalias.c b/src/examples/slf_incr2_noalias.c
index d4966069..7c7e2369 100644
--- a/src/examples/slf_incr2_noalias.c
+++ b/src/examples/slf_incr2_noalias.c
@@ -1,10 +1,10 @@
 void incr2a (unsigned int *p, unsigned int *q)
-/*@ requires take pv = Owned<unsigned int>(p);
-             take qv = Owned<unsigned int>(q);
-    ensures take pv_ = Owned<unsigned int>(p);
-            take qv_ = Owned<unsigned int>(q);
-            pv_ == pv + 1u32;
-            qv_ == qv + 1u32;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures take P_post = Owned<unsigned int>(p);
+            take Q_post = Owned<unsigned int>(q);
+            P_post == P + 1u32;
+            Q_post == Q + 1u32;
 @*/
 {
   unsigned int n = *p;
diff --git a/src/examples/slf_length_acc.c b/src/examples/slf_length_acc.c
index 34d85294..f3fa4389 100644
--- a/src/examples/slf_length_acc.c
+++ b/src/examples/slf_length_acc.c
@@ -1,27 +1,27 @@
-#include "list.h"
+#include "list/headers.h"
 #include "ref.h"
 #include "free.h"
 
 /*@
-function [rec] (u32) length(datatype seq xs) {
+function [rec] (u32) length(datatype List xs) {
   match xs {
-    Seq_Nil {} => {
+    Nil {} => {
       0u32
     }
-    Seq_Cons {head : h, tail : zs}  => {
+    Cons {Head: h, Tail: zs}  => {
       1u32 + length(zs)
     }
   }
 }
 @*/
 
-void IntList_length_acc_aux (struct int_list *xs, unsigned int *p)
-/*@ requires take L1 = IntList(xs);
-             take n = Owned<unsigned int>(p);
-    ensures take L1_ = IntList(xs);
-            take n_ = Owned<unsigned int>(p);
-            L1 == L1_;
-            n_ == n + length(L1);
+void IntList_length_acc_aux (struct sllist *xs, unsigned int *p)
+/*@ requires take L1 = SLList_At(xs);
+             take P = Owned<unsigned int>(p);
+    ensures take L1_post = SLList_At(xs);
+            take P_post = Owned<unsigned int>(p);
+            L1 == L1_post;
+            P_post == P + length(L1);
 @*/
 {
   /*@ unfold length(L1); @*/
@@ -32,11 +32,11 @@ void IntList_length_acc_aux (struct int_list *xs, unsigned int *p)
   }
 }
 
-unsigned int IntList_length_acc (struct int_list *xs)
-/*@ requires take L1 = IntList(xs);
-    ensures take L1_ = IntList(xs);
-            L1 == L1_;
-            return == length(L1);
+unsigned int IntList_length_acc (struct sllist *xs)
+/*@ requires take Xs = SLList_At(xs);
+    ensures take Xs_post = SLList_At(xs);
+            Xs == Xs_post;
+            return == length(Xs);
 @*/
 {
   unsigned int *p = refUnsignedInt(0);
diff --git a/src/examples/slf_quadruple_mem.c b/src/examples/slf_quadruple_mem.c
index 0c7e647b..c7a86dc3 100644
--- a/src/examples/slf_quadruple_mem.c
+++ b/src/examples/slf_quadruple_mem.c
@@ -1,11 +1,11 @@
 int quadruple_mem (int *p)
 /* --BEGIN-- */
-/*@ requires take n = Owned<int>(p);
-             let n_ = (i64) n;
-             (i64)MINi32() <= n_ * 4i64; n_ * 4i64 <= (i64)MAXi32();
-    ensures take n2 = Owned<int>(p);
-            n2 == n;
-            return == 4i32 * n;
+/*@ requires take P = Owned<int>(p);
+             let P64 = (i64) P;
+             (i64)MINi32() <= P64 * 4i64; P64 * 4i64 <= (i64)MAXi32();
+    ensures take P_post = Owned<int>(p);
+            P_post == P;
+            return == 4i32 * P;
  @*/
 /* --END-- */
 {
diff --git a/src/examples/slf_ref_greater.c b/src/examples/slf_ref_greater.c
index 23c54c9c..96138e91 100644
--- a/src/examples/slf_ref_greater.c
+++ b/src/examples/slf_ref_greater.c
@@ -2,12 +2,12 @@
 
 unsigned int *ref_greater_abstract (unsigned int *p)
 /* --BEGIN-- */
-/*@ requires take m1 = Owned<unsigned int>(p);
-             m1 < 4294967295u32;
-    ensures take m2 = Owned<unsigned int>(p);
-            take n2 = Owned<unsigned int>(return);
-            m1 == m2;
-            m1 <= n2;
+/*@ requires take P = Owned<unsigned int>(p);
+             P < 4294967295u32;
+    ensures take P_post = Owned<unsigned int>(p);
+            take R = Owned<unsigned int>(return);
+            P == P_post;
+            P <= R;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/slf_sized_stack.c b/src/examples/slf_sized_stack.c
index a258057d..929d6bef 100644
--- a/src/examples/slf_sized_stack.c
+++ b/src/examples/slf_sized_stack.c
@@ -1,119 +1,124 @@
-#include "list.h"
-#include "list_length.c"
+#include "list/headers.h"
+#include "list/length.c"
 
-struct sized_stack {
+struct sized_stack
+{
   unsigned int size;
-  struct int_list* data;
+  struct sllist *data;
 };
 
 /*@
-type_synonym sizeAndData = {u32 s, datatype seq d}
+type_synonym SizedStack = {u32 Size, datatype List Data}
 
-predicate (sizeAndData) SizedStack(pointer p) {
-    take S = Owned<struct sized_stack>(p);
-    let s = S.size;
-    take d = IntList(S.data);
-    assert(s == length(d));
-    return { s: s, d: d };
+predicate (SizedStack) SizedStack_At (pointer p) {
+    take P = Owned<struct sized_stack>(p);
+    take D = SLList_At(P.data);
+    assert(P.size == Length(D));
+    return { Size: P.size, Data: D };
 }
 @*/
 
-extern struct sized_stack *malloc_sized_stack ();
+extern struct sized_stack *malloc__sized_stack();
 /*@
-spec malloc_sized_stack();
+spec malloc__sized_stack();
      requires true;
-     ensures take u = Block<struct sized_stack>(return);
+     ensures take R = Block<struct sized_stack>(return);
 @*/
 
-extern void *free_sized_stack (struct sized_stack *p);
+extern void *free__sized_stack(struct sized_stack *s);
 /*@
-spec free_sized_stack(pointer p);
-     requires take u = Block<struct sized_stack>(p);
+spec free__sized_stack(pointer s);
+     requires take R = Block<struct sized_stack>(s);
      ensures true;
 @*/
 
-struct sized_stack* create()
-/*@ ensures take S = SizedStack(return);
-            S.s == 0u32;
+struct sized_stack *create()
+/*@ ensures take R = SizedStack_At(return);
+            R.Size == 0u32;
 @*/
 {
-  struct sized_stack *p = malloc_sized_stack();
-  p->size = 0;
-  p->data = 0;
-  /*@ unfold length(Seq_Nil {}); @*/
-  return p;
+  struct sized_stack *s = malloc__sized_stack();
+  s->size = 0;
+  s->data = 0;
+  /*@ unfold Length(Nil {}); @*/
+  return s;
 }
 
-unsigned int sizeOf (struct sized_stack *p)
+unsigned int sizeOf(struct sized_stack *s)
 /* FILL IN HERE */
 /* ---BEGIN--- */
-/*@ requires take S = SizedStack(p);
-    ensures take S_ = SizedStack(p);
-            S_ == S;
-            return == S.s;
+/*@ requires take S = SizedStack_At(s);
+    ensures take S_post = SizedStack_At(s);
+            S_post == S;
+            return == S.Size;
 @*/
 /* ---END--- */
 {
-  return p->size;
+  return s->size;
 }
 
-void push (struct sized_stack *p, int x)
+void push(struct sized_stack *s, int x)
 /* FILL IN HERE */
 /* ---BEGIN--- */
-/*@ requires take S = SizedStack(p);
-    ensures take S_ = SizedStack(p);
-            S_.d == Seq_Cons {head:x, tail:S.d};
+/*@ requires take S = SizedStack_At(s);
+    ensures take S_post = SizedStack_At(s);
+            S_post.Data == Cons {Head:x, Tail:S.Data};
 @*/
 /* ---END--- */
 {
-  struct int_list *data = IntList_cons(x, p->data);
-  p->size++;
-  p->data = data;
-/* ---BEGIN--- */
-  /*@ unfold length (Seq_Cons {head: x, tail: S.d}); @*/
-/* ---END--- */
+  struct sllist *data = slcons(x, s->data);
+  s->size++;
+  s->data = data;
+  /* ---BEGIN--- */
+  /*@ unfold Length (Cons {Head: x, Tail: S.Data}); @*/
+  /* ---END--- */
 }
 
-int pop (struct sized_stack *p)
+int pop(struct sized_stack *s)
 /* FILL IN HERE */
 /* ---BEGIN--- */
-/*@ requires take S = SizedStack(p);
-             S.s > 0u32;
-    ensures  take S_ = SizedStack(p);
-             S_.d == tl(S.d);
+/*@ requires take S = SizedStack_At(s);
+             S.Size > 0u32;
+    ensures  take S_post = SizedStack_At(s);
+             S_post.Data == Tl(S.Data);
+             return == Hd(S.Data);
 @*/
 /* ---END--- */
 {
-  struct int_list *data = p->data;
-  if (data != 0) {
+  struct sllist *data = s->data;
+  /* ---BEGIN--- */
+  /*@ unfold Length(S.Data); @*/
+  // from S.Size > 0u32 it follows that the 'else' branch is impossible
+  /* ---END--- */
+  if (data != 0)
+  {
     int head = data->head;
-    struct int_list *tail = data->tail;
-    freeIntList(data);
-    p->data = tail;
-    p->size--;
-/* ---BEGIN--- */
-    /*@ unfold length(S.d); @*/
-/* ---END--- */
+    struct sllist *tail = data->tail;
+    free__sllist(data);
+    s->data = tail;
+    s->size--;
     return head;
   }
   return 42;
 }
 
-int top (struct sized_stack *p)
-/*@ requires take S = SizedStack(p);
-             S.s > 0u32;
-    ensures  take S_ = SizedStack(p);
-             S_ == S;
-             return == hd(S.d);
+int top(struct sized_stack *s)
+/*@ requires take S = SizedStack_At(s);
+             S.Size > 0u32;
+    ensures  take S_post = SizedStack_At(s);
+             S_post == S;
+             return == Hd(S.Data);
 @*/
 {
-  /*@ unfold length(S.d); @*/ 
-  // from S.s > 0u32 it follows that the 'else' branch is impossible
-  if (p->data != 0) {
-    return (p->data)->head;
+  /*@ unfold Length(S.Data); @*/
+  // from S.Size > 0u32 it follows that the 'else' branch is impossible
+  if (s->data != 0)
+  {
+    return (s->data)->head;
   }
-  else {
+  else
+  {
     // provably dead code
-    return 42; 
+    return 42;
   }
 }
diff --git a/src/examples/swap.c b/src/examples/swap.c
index 31a8c119..435ef1b0 100644
--- a/src/examples/swap.c
+++ b/src/examples/swap.c
@@ -1,10 +1,10 @@
 void swap (unsigned int *p, unsigned int *q)
 /* --BEGIN-- */
-/*@ requires take v = Owned<unsigned int>(p);
-             take w = Owned<unsigned int>(q);
-    ensures  take v2 = Owned<unsigned int>(p);
-             take w2 = Owned<unsigned int>(q);
-             v2 == w && w2 == v;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures  take P_post = Owned<unsigned int>(p);
+             take Q_post = Owned<unsigned int>(q);
+             P_post == Q && Q_post == P;
 @*/
 /* --END-- */
 {
diff --git a/src/examples/transpose.broken.c b/src/examples/transpose.broken.c
index 3bb2ca95..47ef9479 100644
--- a/src/examples/transpose.broken.c
+++ b/src/examples/transpose.broken.c
@@ -1,10 +1,10 @@
 struct point { int x; int y; };
 
 void transpose (struct point *p) 
-/*@ requires take s = Owned<struct point>(p); 
-    ensures take s2 = Owned<struct point>(p); 
-            s2.x == s.y;
-            s2.y == s.x; 
+/*@ requires take P = Owned<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
 @*/
 {
   int temp_x = p->x;
diff --git a/src/examples/transpose.c b/src/examples/transpose.c
index 5bab82bf..03b1d9d8 100644
--- a/src/examples/transpose.c
+++ b/src/examples/transpose.c
@@ -1,10 +1,10 @@
 struct point { int x; int y; };
 
 void transpose (struct point *p) 
-/*@ requires take s = Owned<struct point>(p);
-    ensures take s2 = Owned<struct point>(p);
-            s2.x == s.y;
-            s2.y == s.x;
+/*@ requires take P = Owned<struct point>(p);
+    ensures take P_post = Owned<struct point>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
 @*/
 {
   int temp_x = p->x;
diff --git a/src/examples/transpose2.c b/src/examples/transpose2.c
index 6a903ad3..31b390fd 100644
--- a/src/examples/transpose2.c
+++ b/src/examples/transpose2.c
@@ -1,9 +1,9 @@
 void swap (unsigned int *p, unsigned int *q)
-/*@ requires take v = Owned<unsigned int>(p);
-             take w = Owned<unsigned int>(q);
-    ensures  take v2 = Owned<unsigned int>(p);
-             take w2 = Owned<unsigned int>(q);
-             v2 == w && w2 == v;
+/*@ requires take P = Owned<unsigned int>(p);
+             take Q = Owned<unsigned int>(q);
+    ensures  take P_post = Owned<unsigned int>(p);
+             take Q_post = Owned<unsigned int>(q);
+             P_post == Q && Q_post == P;
 @*/
 {
   unsigned int m = *p;
@@ -16,12 +16,12 @@ struct upoint { unsigned int x; unsigned int y; };
 
 void transpose2 (struct upoint *p)
 /* --BEGIN-- */
-/*@ requires take s = Owned<struct upoint>(p);
-    ensures take s2 = Owned<struct upoint>(p);
-            s2.x == s.y;
-            s2.y == s.x;
+/*@ requires take P = Owned<struct upoint>(p);
+    ensures take P_post = Owned<struct upoint>(p);
+            P_post.x == P.y;
+            P_post.y == P.x;
 @*/
+/* --END-- */
 {
   swap(&p->x, &p->y);
 }
-/* --END-- */
diff --git a/src/examples/zero.c b/src/examples/zero.c
index e6ac6cdd..c7fbf8c7 100644
--- a/src/examples/zero.c
+++ b/src/examples/zero.c
@@ -1,8 +1,8 @@
 void zero (int *p)
 /* --BEGIN-- */
-/*@ requires take u = Block<int>(p);
-    ensures take v = Owned<int>(p);
-            v == 0i32;
+/*@ requires take P = Block<int>(p);
+    ensures take P_post = Owned<int>(p);
+            P_post == 0i32;
 @*/
 /* --END-- */
 {
diff --git a/src/queue-example-notes.md b/src/queue-example-notes.md
deleted file mode 100644
index 09eb24c9..00000000
--- a/src/queue-example-notes.md
+++ /dev/null
@@ -1,222 +0,0 @@
-2# Notes
-
-- Bad definition of snoc (same as rev). How to spot? Look at constraint context, specifically snoc(listQ, x) == match listQ {Seq\_Nil {} => {Seq\_Nil {}}Seq\_Cons {head: h, tail: zs} => {snoc(rev(zs), h)}}. Other big clue: applying lemma snoc_nil results in an inconsistent context. This is really nasty because snoc(Seq_Nil{}, x) ends up reducing to itself.
-
-- Code used q->tail == 0 but predicate was testing q->head. Can adjust predicate, code, or use a split_case.
-
-- Under-constrained counter-examples are something to be aware of (though the inconsitency came because of the definition of snoc here rather than l here).
-
-d99e65ed01c7a35408b0e409af3f17ece25bc0bf is the tutorial commit (with the correct definition of snoc, but the point at which you originally asked for help)
-
-More notes:
-  - path explosion means you can't look at path to error in HTML output
-      - it can help to move the return statement (manually explode!)
-        to see which path is failing
-      - (should be able to annotate after a conditional to pull things
-        back together)
-  - conclude that l is not properly constrained
-        because the SMT solver is making crazy choices
-
-# --------------------------------------------------------------------------
-# Original version
-
-Here's the predicate for queues:
-
-    predicate (datatype seq) IntQueue(pointer q) {
-      take H = Owned<struct int_queue>(q);
-      take Q = IntQueue1(q,H);
-      return Q;
-    }
-
-    predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) {
-      if (is_null(H.head)) {
-        assert (is_null(H.tail));
-        return (Seq_Nil{});
-      } else {
-        assert (!is_null(H.tail));
-        take Q = IntQueueAux (H.head, H.tail);
-        return Q;
-      }
-    }
-
-    predicate (datatype seq) IntQueueAux(pointer h, pointer t) {
-      take C = Owned<struct int_queueCell>(h);
-      take L = IntQueueAux1(h, C, t);
-      return L;
-    }
-
-    predicate (datatype seq) IntQueueAux1
-                               (pointer h, struct int_queueCell C, pointer t) {
-      if (is_null(C.next)) {
-        assert (h == t);
-        return (Seq_Cons{head: C.first, tail: Seq_Nil{}});
-      } else {
-        take TL = IntQueueAux(C.next, t);
-        return (Seq_Cons { head: C.first, tail: TL });
-      }
-    }
-
-And here's the push operation.
-
-    void IntQueue_push (int x, struct int_queue *q)
-    /*@ requires take l = IntQueue(q);
-        ensures take ret = IntQueue(q);
-                ret == snoc (l, x);
-    @*/
-    {
-      struct int_queueCell *c = mallocIntQueueCell();
-      c->first = x;
-      c->next = 0;
-      if (q->tail == 0) {
-        q->head = c;
-        q->tail = c;
-      } else {
-        q->tail->next = c;
-        q->tail = c;
-      }
-    }
-
-This fails because there are not enough annotations in the body of push.
-
-Confusingly, the HTML error report gives this as the unproven constraint
-
-    Seq_Cons {head: x, tail: Seq_Nil {}} == snoc(l, x)
-
-while the list of Terms shows that
-
-    Seq_Cons {head: x, tail: Seq_Nil {}} == snoc(l, x)
-
-has value false!
-
-I.e., something is very wrong.
-
-First, we have to find the path to the error.  Either decode the HTML
-or put in some returns in the branches of the if.  This tells us that
-the problem is in the first branch.
-
-We see
-
-    temp-queue1b.broken.c:95:5: error: Unprovable constraint
-        return;
-        ^~~~~~~
-    Constraint from temp-queue1b.broken.c:86:13:
-                ret == snoc (l, x);
-                ^~~~~~~~~~~~~~~~~~~
-
-To make progress, we need to unfold snoc.  How do we know this?
-Because the constraint that is problematic involves a snoc, and snoc
-is recursive, so we should expect to have to unfold at some point.
-(Non-recursive things are always inlined, but recursive ones obviously
-not, so even to look "one level deep" we need an unfold.)
-
-Once we've unfolded, we get some more hints:
-
-  - Look at the value of l in Terms: Seq_Cons {head: 0i32, tail: Seq_Nil {}}
-  - But we are in the empty queue case, so this seems fishy.
-  - Now, in the constraints, we see   l == unpack_IntQueue1.Q
-  - Then look at the resources and see that unpack_IntQueue1.Q has not
-    been unpacked in the final line:
-        IntQueue1(q, unpack_IntQueue1.H)(unpack_IntQueue1.Q)
-  - This means that CN did not have enough information to decide which
-    way the conditional at the beginning of IntQueue1 is going to go.
-  - But the condition is testing H.head, while the conditional in the
-    code is testing the tail field!
-  - We could get around this mismatch by adjusting the condition
-    itself, or by adjusting the predicate.  E.g., we could change the
-    predicate to test *both* for null at the beginning, so that it
-    doesn't matter which one you test.
-
-This tells us to look at snoc, which turns out to be very wrong!
-
-    function [rec] (datatype seq) snoc(datatype seq xs, i32 y) {
-      match xs {
-        Seq_Nil {} => {
-          Seq_Nil {}
-        }
-        Seq_Cons {head : h, tail : zs}  => {
-          snoc (rev(zs), h)
-        }
-      }
-    }
-
-
-# --------------------------------------------------------------------------
-# Next try
-
-    void IntQueue_push (int x, struct int_queue *q)
-    /*@ requires take l = IntQueue(q);
-        ensures take ret = IntQueue(q);
-                ret == snoc (l, x);
-    @*/
-    {
-      struct int_queueCell *c = mallocIntQueueCell();
-      c->first = x;
-      c->next = 0;
-      if (q->tail == 0) {
-        /*@ split_case q->head == NULL; @*/
-        /*@ apply snac_nil(x); @*/
-        q->head = c;
-        q->tail = c;
-      } else {
-        q->tail->next = c;
-        q->tail = c;
-      }
-    }
-
-This time the error is:
-
-    temp-queue2.broken.c:86:5: error: Missing resource for writing
-        q->tail->next = c;
-        ~~~~~~~~~~~~~~^~~
-    Resource needed: Block<struct
-        int_queueCell*>(member_shift<int_queueCell>(unpack_IntQueue1
-        .H
-        .tail, next))
-
-This makes more sense.  [But how to articulate the sense that it
-makes??]
-
-# --------------------------------------------------------------------------
-# Getting closer
-
-We could fix this by rewriting the push function so that, instead of
-following the tail pointer, it recurses down from the head until it
-reaches the tail.  This would work (might be a good exercise?), but it
-nullifies the whole purpose of having the tail pointer in the first
-place.
-
-Instead, we need to rearrange IntQueue and friends so that we take
-ownership of the very last cell in the list at the very beginning,
-instead of at the very end.
-
-    predicate (datatype seq) IntQueue(pointer q) {
-      take H = Owned<struct int_queue>(q);
-      take Q = IntQueue1(q,H);
-      return Q;
-    }
-
-    predicate (datatype seq) IntQueue1(pointer dummy, struct int_queue H) {
-      if (is_null(H.head)) {
-        assert (is_null(H.tail));
-        return (Seq_Nil{});
-      } else {
-        assert (!is_null(H.tail));
-        take T = Owned<struct int_queueCell>(H.tail);
-        assert (is_null(T.next));
-        take Q = IntQueueAux (H.head, H.tail, T.first);
-        return Q;
-      }
-    }
-
-    predicate (datatype seq) IntQueueAux (pointer h, pointer t, i32 lastVal) {
-      if (h == t) {
-        return (Seq_Cons{head: lastVal, tail: Seq_Nil{}});
-      } else {
-        take C = Owned<struct int_queueCell>(h);
-        take TL = IntQueueAux(C.next, t, lastVal);
-        return (Seq_Cons { head: C.first, tail: TL });
-      }
-    }
-
-This matches the access pattern of the push implementation, and
-it... works??
diff --git a/src/tutorial.adoc b/src/tutorial.adoc
index e641a65c..fa7744b4 100644
--- a/src/tutorial.adoc
+++ b/src/tutorial.adoc
@@ -10,11 +10,13 @@ By Christopher Pulte and Benjamin C. Pierce, with contributions from Elizabeth A
 
 [abstract]
 --
-CN is a type system for verifying C code, focusing especially on low-level systems code. Compared to the normal C type system, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — according to strong user-defined specifications. 
-// 
-This tutorial introduces CN along a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures. 
+CN is an extension of the C programming language for verifying the correctness of C code, especially on low-level systems code. Compared to standard C, CN checks not only that expressions and statements follow the correct typing discipline for C-types, but also that the C code executes _safely_ — does not raise C undefined behaviour — and _correctly_ — satisfying to strong, user-defined specifications.
+This tutorial introduces CN through a series of examples, starting with basic usage of CN on simple arithmetic functions and slowly moving towards more elaborate separation logic specifications of data structures.
 
-CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, Neel Krishnaswami.
+This tutorial is a work in progress -- your suggestions are greatly appreciated!
+
+**Origins.**
+CN was first described in https://dl.acm.org/doi/10.1145/3571194[CN: Verifying Systems C Code with Separation-Logic Refinement Types] by Christopher Pulte, Dhruv C. Makwana, Thomas Sewell, Kayvan Memarian, Peter Sewell, and Neel Krishnaswami.
 //
 To accurately handle the complex semantics of C, CN builds on the https://github.com/rems-project/cerberus/[Cerberus semantics for C].
 //
@@ -23,55 +25,49 @@ https://softwarefoundations.cis.upenn.edu[Separation Logic
 Foundations] textbook, and one of the case studies is based on an
 extended exercise due to Bryan Parno.
 
-This tutorial is a work in progress -- your suggestions are greatly appreciated!
+--
 
 **Acknowledgment of Support and Disclaimer.**
 This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google.  The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
 
---
-
 == Installing CN
 
-To fetch and install CN, check the Cerberus repository at https://github.com/rems-project/cerberus and follow the instructions in https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md[backend/cn/README.md].
+To fetch and install CN, visit the Cerberus repository at https://github.com/rems-project/cerberus and follow the instructions in https://github.com/rems-project/cerberus/blob/master/backend/cn/README.md[backend/cn/README.md].
 
-Once completed, type `+cn --help+` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with.
+Once the installation is completed, type `+cn --help+` in your terminal to ensure CN is installed and found by your system. This should print the list of available options CN can be executed with.
 
-To apply CN to a C file, run `+cn CFILE+`.
+To apply CN to a C file, run `+cn verify CFILE+`.
 
-== Source files for the exercises and examples
+== Source files
 
-The source files can be downloaded from link:exercises.zip[here].
+The source files for all the exercises and examples below can be downloaded
+from link:exercises.zip[here].
 
-== Basic usage
+== Basics
 
 === First example
 
-For a first example, let’s look at a simple arithmetic function: `+add+`, shown below, takes two `+int+` arguments, `+x+` and `+y+`, and returns their sum.
+The simple arithmetic function: `+add+` shown below takes two `+int+` arguments, `+x+` and `+y+`, and returns their sum.
 
-// TODO: BCP: We should probably adopt the convention that all the files in
-// the exercises directory have a comment at the top giving their name.
-// (We could actually auto-generate those header comments when we process
-// /src/examples into build/exercises, to avoid having to maintain them
-// and possibly get them wrong...)
 include_example(exercises/add_0.c)
 
 Running CN on the example produces an error message:
 
 ....
-cn exercises/add_0.c
+cn verify exercises/add_0.c
 [1/1]: add
 exercises/add_0.c:3:10: error: Undefined behaviour
   return x+y;
          ~^~
 an exceptional condition occurs during the evaluation of an expression (§6.5#5)
-Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_393431.html
+Consider the state in /var/folders/_v/ndl32rvc8ph0000gn/T/state_393431.html
 ....
 
-CN rejects the program because it has _C undefined behaviour_, meaning it is not safe to execute. CN points to the relevant source location, the addition `+x+y+`, and paragraph §6.5#5 of the C language standard that specifies the undefined behaviour. It also puts a link to an HTML file with more details on the error to help in diagnosing the problem.
+CN rejects the program because it has _undefined behaviour_ according to the C standard, meaning it is not safe to execute. CN points to the relevant source location, the addition `+x+y+`, and paragraph §6.5#5 of the standard, which specifies the undefined behaviour. It also includes a link to an HTML file with more details on the error to help in diagnosing the problem.
 
 Inspecting this HTML report (as we do in a moment) gives us possible example values for `+x+` and `+y+` that cause the undefined behaviour and hint at the problem: for very large values for `+x+` and `+y+`, such as `+1073741825+` and `+1073741824+`, the sum of `+x+` and `+y+` can exceed the representable range of a C `+int+` value: `+1073741825 + 1073741824 = 2^31+1+`, so their sum is larger than the maximal `+int+` value, `+2^31-1+`.
 
-Here `+x+` and `+y+` are _signed integers_, and in C, signed integer _overflow_ is undefined behaviour (UB). Hence, `+add+` is only safe to execute for smaller values. Similarly, _large negative_ values of `+x+` and `+y+` can cause signed integer _underflow_, also UB in C. We therefore need to rule out too large values for `+x+` and `+y+`, both positive and negative, which we do by writing a CN function specification.
+Here `+x+` and `+y+` are _signed integers_, and in C, signed integer _overflow_ is undefined behaviour (UB). Hence, `+add+` is only safe to execute for smaller values. Similarly, _large negative_ values of `+x+` and `+y+` can cause signed integer _underflow_, also UB in C. We therefore need to rule out too-large values for `+x+` and `+y+`, both positive and negative, which we do by writing a CN function specification.
 
 === First function specification
 
@@ -89,22 +85,28 @@ In detail:
 
 * In function specifications, the names of the function arguments, here `+x+` and `+y+`, refer to their _initial values_. (Function arguments are mutable in C.)
 
-* `+let sum = (i64) x + (i64) y+` is a let-binding, which defines `+sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification.
+* `+let Sum = (i64) x + (i64) y+` is a let-binding, which defines `+Sum+` as the value `+(i64) x + (i64) y+` in the remainder of the function specification.
 
-* Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`.
+* Instead of C syntax, CN uses Rust-like syntax for integer types, such as `+u32+` for 32-bit unsigned integers and `+i64+` for signed 64-bit integers, to make their sizes unambiguous. Here, `+x+` and `+y+`, of C-type `+int+`, have CN type `+i32+`.
 // TODO: BCP: I understand this reasoning, but I wonder whether it introduces more confusion than it avoids -- it means there are two ways of writing everything, and people have to remember whether the particular thing they are writing right now is C or CN...
+// BCP: Hopefully we are moving toward unifying these notations anyway?
 
-* To define `+sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values.
+* To define `+Sum+` we cast `+x+` and `+y+` to the larger `+i64+` type, using syntax `+(i64)+`, which is large enough to hold the sum of any two `+i32+` values.
 
-* Finally, we require this sum to be in-between the minimal and maximal `+int+` value. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`).
+* Finally, we require this sum to be between the minimal and maximal `+int+` values. Integer constants, such as `+-2147483648i64+`, must specifiy their CN type (`+i64+`).
+// TODO: BCP: We should use the new ' syntax (or whatever it turned out to be) for numeric constants
+// Dhruv: Yet to be implemented: rems-project/cerberus#337
 
-Running CN on the annotated program passes without errors. This means with our specified precondition, `+add+` is safe to execute.
+Running CN on the annotated program passes without errors. This means that, with our specified precondition, `+add+` is safe to execute.
 
-We may, however, wish to be more precise. So far the specification gives no information to callers of `+add+` about its output. To also specify the return values we add a postcondition, using the `+ensures+` keyword.
+We may, however, wish to be more precise. So far, the specification gives no information to callers of `+add+` about its output. To describe its return value we add a postcondition to the specification using the `+ensures+` keyword.
 
 include_example(solutions/add_1.c)
 
-Here we use the keyword `+return+`, only available in function postconditions, to refer to the return value, and equate it to `+sum+` as defined in the preconditions, cast back to `+i32+` type: `+add+` returns the sum of `+x+` and `+y+`.
+Here we use the keyword `+return+`, which is only available in function
+postconditions, to refer to the return value, and we equate it to `+Sum+`
+as defined in the precondition, cast back to `+i32+` type: that is, `+add+`
+returns the sum of `+x+` and `+y+`.
 
 Running CN confirms that this postcondition also holds.
 
@@ -112,77 +114,136 @@ One final refinement of this example.  CN defines constant functions `MINi32`, `
 
 include_example(solutions/add_2.c)
 
-Two things to note:
-   * These are constant _functions_, so they require a following `()`.
-   * The type of `MINi32()` is `i32`, so if we want to use it as a 64-bit constant
-     we need to add the explicit coercion `(i64)`.
+Two things to note: (1) These are constant _functions_, so they
+require a following `()`.  And (2) The type of `MINi32()` is `i32`, so
+if we want to use it as a 64-bit constant we need to add the explicit
+coercion `(i64)`.
 
 === Error reports
 
-In the original example CN reported a type error due to C undefined behaviour. While that example was perhaps simple enough to guess the problem and solution, this can become quite challenging as program and specification complexity increases. Diagnosing type errors is therefore an important part of using CN. CN tries to help with that by producing detailed error information, in the form of an HTML error report.
+In the original example, CN reported a type error due to C undefined
+behaviour. While that example was perhaps simple enough to guess the
+problem and solution, this can become quite challenging as program and
+specification complexity increases. Diagnosing errors is
+therefore an important part of using CN. CN tries to help with this by
+producing detailed error information, in the form of an HTML error
+report.
 
-Let’s return to the type error from earlier (`+add+` without precondition) and take a closer look at this report. The report comprises two sections.
+Let’s return to the type error from earlier -- `+add+` without
+precondition -- and take a closer look at this report. It
+comprises two sections:
 
-// TODO: BCP: It looks different now!
+// TODO: BCP: It looks quite different now!
 .*CN error report*
 image::images/0.error.png[*CN error report*]
 
-*Path.* The first section, "`Path to error`", contains information about the control-flow path leading to the error.
-
-When type checking a C function, CN checks each possible control-flow path through the program individually. If CN detects UB or a violation of user-defined specifications, CN reports the problematic control-flow path, as a nested structure of statements: paths are split into sections, which group together statements between high-level control-flow positions (e.g. function entry, the start of a loop, the invocation of a `+continue+`, `+break+`, or `+return+` statement, etc.); within each section, statements are listed by source code location; finally, per statement, CN lists the typechecked sub-expressions, and the memory accesses and function calls within these.
-
-In our example, there is only one possible control-flow path: entering the function body (section "`function body`") and executing the block from lines 2 to 4, followed by the return statement at line 3. The entry for the latter contains the sequence of sub-expressions in the return statement, including reads of the variables `+x+` and `+y+`.
-
-In C, local variables in a function, including its arguments, are mutable and their address can be taken and passed as a value. CN therefore represents local variables as memory allocations that are manipulated using memory reads and writes. Here, type checking the return statement includes checking memory reads for `+x+` and `+y+`, at their locations `+&ARG0+` and `+&ARG1+`. The path report lists these reads and their return values: the read at `+&ARG0+` returns `+x+` (that is, the value of `+x+` originally passed to `+add+`); the read at `+&ARG1+` returns `+y+`. Alongside this symbolic information, CN displays concrete values:
+*Path to error.* The first section contains information about the
+control-flow path leading to the error.
+
+When checking a C function, CN examines each possible control-flow
+path individually. If it detects UB or a violation of user-defined
+specifications, CN reports the problematic control-flow path as a
+nested structure of statements: the path is split into sections that
+group together statements between high-level control-flow positions
+(e.g. function entry, the start of a loop, the invocation of a
+`+continue+`, `+break+`, or `+return+` statement, etc.); within each
+section, statements are listed by source code location; finally, per
+statement, CN lists the typechecked sub-expressions, and the memory
+accesses and function calls within these.
+
+In our example, there is only one possible control-flow path: entering
+the function body (section "`function body`") and executing the block
+from lines 2 to 4, followed by the return statement at line 3. The
+entry for the latter contains the sequence of sub-expressions in the
+return statement, including reads of the variables `+x+` and `+y+`.
+
+In C, local variables in a function, including its arguments, are
+mutable,  their addresses can be taken and passed as values. CN
+therefore represents local variables as memory allocations that are
+manipulated using memory reads and writes. Here, type checking the
+return statement includes checking memory reads for `+x+` and `+y+`,
+at their locations `+&ARG0+` and `+&ARG1+`. The path report lists
+these reads and their return values: the read at `+&ARG0+` returns
+`+x+` (that is, the value of `+x+` originally passed to `+add+`); the
+read at `+&ARG1+` returns `+y+`. Alongside this symbolic information,
+CN displays concrete values:
 
 * `+1073741825i32 /* 0x40000001 */+` for x (the first value is the decimal representation, the second, in `+/*...*/+` comments, the hex equivalent) and
 
 * `+1073741824i32 /* 0x40000000 */+` for `+y+`.
 
 For now, ignore the pointer values `+{@0; 4}+` for `+x+` and `+{@0; 0}+` for `+y+`.
+// TODO: BCP: Where are these things discussed?  Anywhere?  (When) are they useful?
+// Dhruv:  These are part of VIP memory model things I'm working on, which will hopefully be implemented and enabled in the next few weeks.
 
-These concrete values are part of a _counterexample_: a concrete valuation of variables and pointers in the program that that leads to the error. (The exact values may vary on your machine, depending on the version of Z3 installed on your system.)
+These concrete values are part of a _counterexample_: a concrete
+valuation of variables and pointers in the program that that leads to
+the error. (The exact values may vary on your machine, depending on
+the SMT solver -- i.e., the particular version of Z3, CVC5, or
+whatever installed on your system.)
 
 *Proof context.* The second section, below the error trace, lists the proof context CN has reached along this control-flow path.
 
 "`Available resources`" lists the owned resources, as discussed in later sections.
 
 "`Variables`" lists counterexample values for program variables and pointers. In addition to `+x+` and `+y+`, assigned the same values as above, this includes values for their memory locations `+&ARG0+` and `+&ARG1+`, function pointers in scope, and the `+__cn_alloc_history+`, all of which we ignore for now.
-
-Finally, "`Constraints`" records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here (`+add+` without precondition) the only constraints are some contraints inferred from C-types in the code.
-
-* For instance, `+good<signed int>(x)+` says that the initial value of `+x+` is a "`good`" `+signed int+` value (i.e. in range). Here `+signed int+` is the same type as `+int+`, CN just makes the sign explicit. For integer types `+T+`, `+good<T>+` requires the value to be in range of type `+T+`; for pointer types `+T+` it also requires the pointer to be aligned. For structs and arrays this extends in the obvious way to struct members or array cells.
+// TODO: BCP: Again, where are these things discussed?  Should they be?
+// Dhruv: Also VIP.
+
+Finally, "`Constraints`" records all logical facts CN has learned along the path. This includes user-specified assumptions from preconditions or loop invariants, value ranges inferred from the C-types of variables, and facts learned during the type checking of the statements. Here -- when checking `+add+` without precondition -- the only constraints are those inferred from C-types in the code:
+
+* For instance, `+good<signed int>(x)+` says that the initial value of
+`+x+` is a "`good`" `+signed int+` value (i.e. in range). Here
+`+signed int+` is the same type as `+int+`, CN just makes the sign
+explicit.
+// TODO: BCP: Yikes!  This seems potentially confusing
+For an integer type `+T+`, the type `+good<T>+` requires the value to
+be in range of type `+T+`; for pointer types `+T+`, it also requires
+the pointer to be aligned. For structs and arrays, this extends in the
+obvious way to struct members or array cells.
+// TODO: BCP: Is this information actually ever useful?  Is it currently suppressed?
 
 * `+repr<T>+` requires representability (not alignment) at type `+T+`, so `+repr<signed int*>(&ARGO)+`, for instance, records that the pointer to `+x+` is representable at C-type `+signed int*+`;
 
 * `+aligned(&ARGO, 4u64)+`, moreover, states that it is 4-byte aligned.
 
+// TODO: URGENT: BCP: Some of the above (especially the bit at the end) feels like TMI for many/most users, especially at this point in the tutorial.
+// Dhruv: Probably true, we actually even hide some of these by default.
+// BCP: I propose we hide the rest and move this discussion to somewhere else ("Gory Details" section of the tutorial, or better yet reference manual).
+// Dhruv: Thumbs up
+
 === Another arithmetic example
 
 Let’s apply what we know so far to another simple arithmetic example.
 
 The function `+doubled+`, shown below, takes an int `+n+`, defines `+a+` as `+n+` incremented, `+b+` as `+n+` decremented, and returns the sum of the two.
 
-// TODO: BCP: Is it important to number the slf examples?  If so, we should do it consistently, but IMO it is not.
+// TODO: BCP: Is it important to number the slf examples?  If so, we should do it consistently, but IMO it is not.  Better to rename them without numbers.
 include_example(exercises/slf1_basic_example_let.signed.c)
 
 We would like to verify this is safe, and that `+doubled+` returns twice the value of `+n+`. Running CN on `+doubled+` leads to a type error: the increment of `+a+` has undefined behaviour.
 
-As in the first example, we need to ensure that `+n+1+` does not overflow and `+n-1+` does not underflow. Similarly also `+a+b+` has to be representable at `+int+` type.
+As in the first example, we need to ensure that `+n+1+` does not overflow and `+n-1+` does not underflow. Similarly `+a+b+` has to be representable at `+int+` type.
 
 include_example(solutions/slf1_basic_example_let.signed.c)
+// TODO: BCP: WHy n_+n_ in some places and n*2i32 in others?
+// Dhruv: Unlikely to be meaningful, either is fine.
 
-We can specify these using a similar style of precondition as in the first example. We first define `+n_+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+` and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+n_+` does not go below the minimal `+int+` value, that incrementing `+n_+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution.
+We encode these expectations using a similar style of precondition as in the first example. We first define `+N+` as `+n+` cast to type `+i64+` — i.e. a type large enough to hold `+n+1+`, `+n-1+`, and `+a+b+` for any possible `+i32+` value for `+n+`. Then we specify that decrementing `+N+` does not go below the minimal `+int+` value, that incrementing `+N+` does not go above the maximal value, and that `+n+` doubled is also in range. These preconditions together guarantee safe execution.
+// TODO: BCP: How about renaming N to n64?
+// Dhruv: Sensible.
+// BCP: (someone do it on next pass)
 
 To capture the functional behaviour, the postcondition specifies that `+return+` is twice the value of `+n+`.
 
-=== Exercise
+=== Exercises
 
 *Quadruple.* Specify the precondition needed to ensure safety of the C function `+quadruple+`, and a postcondition that describes its return value.
 
 include_example(exercises/slf2_basic_quadruple.signed.c)
 
 *Abs.* Give a specification to the C function `+abs+`, which computes the absolute value of a given `+int+` value. To describe the return value, use CN’s ternary "`+_ ? _ : _+`" operator. Given a boolean `+b+`, and expressions `+e1+` and `+e2+` of the same basetype, `+b ? e1 : e2+` returns `+e1+` if `+b+` holds and `+e2+` otherwise.
+Note that most binary operators in CN have higher precedence than the ternary operator, so depending on your solution you may need to place the ternary expression in parentheses.
 
 include_example(exercises/abs.c)
 
@@ -190,7 +251,7 @@ include_example(exercises/abs.c)
 
 So far we’ve only considered example functions manipulating integer values. Verification becomes more interesting and challenging when _pointers_ are involved, because the safety of memory accesses via pointers has to be verified.
 
-CN uses _separation logic resource types_ and the concept of _ownership_ to reason about memory accesses. A resource is the permission to access a region of memory. Unlike logical constraints, resource ownership is _unique_, meaning resources cannot be duplicated.
+CN uses _separation logic resources_ and the concept of _ownership_ to reason about memory accesses. A resource is the permission to access a region of memory. Unlike logical constraints, resource ownership is _unique_, meaning resources cannot be duplicated.
 
 Let’s look at a simple example. The function `+read+` takes an `+int+` pointer `+p+` and returns the pointee value.
 
@@ -199,7 +260,7 @@ include_example(exercises/read.c)
 Running CN on this example produces the following error:
 
 ....
-cn exercises/read.c
+cn verify exercises/read.c
 [1/1]: read
 exercises/read.c:3:10: error: Missing resource for reading
   return *p;
@@ -210,15 +271,28 @@ Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_403
 
 For the read `+*p+` to be safe, ownership of a resource is missing: a resource `+Owned<signed int>(p)+`.
 
-=== The Owned resource type
+=== Owned resources
+
+// TODO: BCP: Perhaps this is a good time for one last discussion of the keyword "Owned", which I have never found very helpful: the resource itself isn't owned -- it's a description of something that *can* be owned.  (It's "take" that does the owning.)  Moreover, "Owned" and "Block" are badly non-parallel, both grammatically and semantically.  I suggest "Resource" instead of "Owned".  (We can keep "Block" -- it's not too bad, IMO.)
+////
+Dhruv:
+We use the word "resources" to describe any "resource predicate" owned, or user-defined, (and eventually live allocations and locks) so I'm not sure that suggestion works any better. It is just a points-to with read and write permissions, so perhaps a RW(p)? (or ReadWrite(p)?).
+
+@bcpierce00
+Both of these are better than Owned!
+
+(And then Block can become WriteOnly.)
+
+BCP: I think this discussion is reflected in the GitHub exchange
+////
 
 Given a C-type `+T+` and pointer `+p+`, the resource `+Owned<T>(p)+` asserts ownership of a memory cell at location `+p+` of the size of C-type `+T+`. It is CN’s equivalent of a points-to assertion in separation logic (indexed by C-types `+T+`).
 
-In this example we can ensure the safe execution of `+read+` by adding a precondition that requires ownership of `+Owned<int>(p)+`, as shown below. For now ignore the notation `+take ... = Owned<int>(p)+`. Since `+read+` maintains this ownership, we also add a corresponding postcondition, whereby `+read+` returns ownership of `+p+` after it is finished executing, in the form of another `+Owned<int>(p)+` resource.
+In this example we can ensure the safe execution of `+read+` by adding a precondition that requires ownership of `+Owned<int>(p)+`, as shown below. For now ignore the notation `+take ... = Owned<int>(p)+`. Since reading the pointer does not disturb its value, we also add a corresponding postcondition, whereby `+read+` returns ownership of `+p+` after it is finished executing, in the form of another `+Owned<int>(p)+` resource.
 
 include_example(solutions/read.c)
 
-This specifications means that
+This specification means that:
 
 * any function calling `+read+` has to be able to provide a resource `+Owned<int>(p)+` to pass into `+read+`, and
 
@@ -226,39 +300,42 @@ This specifications means that
 
 === Resource outputs
 
-However, a caller of `+read+` may also wish to know that `+read+` actually returns the correct value, the pointee of `+p+`, and also that it does not change memory at location `+p+`. To phrase both we need a way to refer to the pointee of `+p+`.
+A caller of `+read+` may also wish to know that `+read+` actually returns the correct value, the pointee of `+p+`, and also that it does not change memory at location `+p+`. To phrase both we need a way to refer to the pointee of `+p+`.
 
-In CN resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned<T>(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`.
+// TODO: BCP: The idea that "resources have outputs" is very mind-boggling to many new users, *especially* folks with some separation logic background.  Needs to be explained very carefully.  Also, there's some semantic muddle in the terminology: Is a resource (1) a thing in the heap, (2) a thing in the heap that one is currently holding, or (3) the act of holding a thing in the heap?  These are definitely not at all the same thing, but our language at different points suggests all three!  To me, (1) is the natural sense of the word "resource"; (2) is somewhat awkward, and (3) is extremely awkward.
 
-CN uses the `+take+`-notation seen in the example above to refer to the output of a resource, introducing a new name binding for the output. The precondition `+take v1 = Owned<int>(p)+` from the precondition does two things: (1) it assert ownership of resource `+Owned<int>(p)+`, and (2) it binds the name `+v1+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+v2+` for the pointee value on function return.
+In CN, resources have _outputs_. Each resource outputs the information that can be derived from ownership of the resource. What information is returned is specific to the type of resource. A resource `+Owned<T>(p)+` (for some C-type `+T+`) outputs the _pointee value_ of `+p+`, since that can be derived from the resource ownership: assume you have a pointer `+p+` and the associated ownership, then this uniquely determines the pointee value of `+p+`.
+// TODO: BCP: ... in a given heap!  (The real problem here is that "and the associated ownership" is pretty vague.)
+// Dhruv: Perhaps mentioning sub-heaps will help?
 
-That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions: we specify
+CN uses the `+take+`-notation seen in the example above to bind the output of a resource to a new name. The precondition `+take P = Owned<int>(p)+` does two things: (1) it assert ownership of resource `+Owned<int>(p)+`, and (2) it binds the name `+P+` to the resource output, here the pointee value of `+p+` at the start of the function. Similarly, the postcondition introduces the name `+P_post+` for the pointee value on function return.
 
-. that `+read+` returns `+v1+` (the initial pointee value of `+p+`), and
-. that the pointee values `+v1+` and `+v2+` before and after execution of `+read+` (respectively) are the same.
+// TODO: BCP: But, as we've discussed, the word "take" in the postcondition is quite confusing: What it's doing is precisely the *opposite* of "taking" the resournce, not taking it but giving it back!!  It would be much better if we could choose a more neutral word that doesn't imply either taking or giving.  E.g. "resource".
 
-include_example(solutions/read2.c)
+// TODO: BCP: This might be a good place for a comment on naming conventions.  Plus a pointer to a longer discussion if needed
 
-*Aside.* In standard separation logic the equivalent specification for `+read+` could have been phrased as follows (where `+return+` binds the return value in the postcondition):
+That means we can use the resource outputs from the pre- and postcondition to strengthen the specification of `+read+` as planned. We add two new postconditions specifying
 
-....
-∀p.
-∀v1. { p ↦ v1 }
-     read(p)
-     { return. ∃v2. (p ↦ v2) /\ return = v1 /\ v1 = v2 }
-....
+. that `+read+` returns `+P+` (the initial pointee value of `+p+`), and
+. that the pointee values `+P+` and `+P_post+` before and after execution of `+read+` (respectively) are the same.
 
-CN’s `+take+` notation is just alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them.
+include_example(exercises/read2.c)
 
-=== Exercises
+*Aside.* In standard separation logic, the equivalent specification for `+read+` could have been phrased as follows (where `+\return+` binds the return value in the postcondition):
 
-*Quadruple*. Specify the function `+quadruple_mem+`, that is similar to the earlier `+quadruple+` function, except that the input is passed as an `+int+` pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged.
+// TODO: Sainati: as a separation logic noob, I would love a more detailed explanation about what is going on here. 
 
-include_example(exercises/slf_quadruple_mem.c)
+// Why do we need to have v2 existentially quantified, for example, when p is only pointing to a single value?
 
-*Abs*. Give a specification to the function `+abs_mem+`, which computes the absolute value of a number passed as an `+int+` pointer.
+....
+∀p.
+  ∀v1.
+    { p ↦ P }
+    read(p)
+    { \return. ∃P_post. (p ↦ P_post) /\ return = P /\ P = P_post }
+....
 
-include_example(exercises/abs_mem.c)
+CN’s `+take+` notation is just an alternative syntax for quantification over the values of resources, but a useful one: the `+take+` notation syntactically restricts how these quantifiers can be used to ensure CN can always infer them.
 
 === Linear resource ownership
 
@@ -271,45 +348,89 @@ include_example(exercises/read.broken.c)
 CN rejects this program with the following message:
 
 ....
-cn build/exercises/read.broken.c
+cn verify exercises/read.broken.c
 [1/1]: read
-build/exercises/read.broken.c:4:3: error: Left-over unused resource 'Owned<signed int>(p)(v1)'
+build/exercises/read.broken.c:4:3: error: Left_Sublist-over unused resource 'Owned<signed int>(p)(v1)'
   return *p;
   ^~~~~~~~~~
 Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_17eb4a.html
 ....
 
-CN has typechecked the function, verified that it is safe to execute under the precondition (given ownership `+Owned<int>(p)+`), and that the function (vacuously) satisfies its postcondition. But, following the check of the postcondition it finds that not all resources have been "`used up`".
+CN has typechecked the function and verified (1) that it is safe to
+execute under the precondition (given ownership `+Owned<int>(p)+`)
+and (2) that the function (vacuously) satisfies its postcondition. But
+following the check of the postcondition it finds that not all
+resources have been "`used up`".
+
+Indeed, given the above specification, `+read+` leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error.
 
-Given the above specification, `+read+` leaks memory: it takes ownership, does not return it, but also does not deallocate the owned memory or otherwise dispose of it. In CN this is a type error.
+CN’s resources are _linear_. This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or "`forgotten`". Every resource passed into a function has to be either _returned_ to the caller or else _destroyed_ by deallocating the owned area of memory (as we shall see later).
 
-CN’s resource types are _linear_ (as opposed to affine). This means not only that resources cannot be duplicated, but also that resources cannot simply be dropped or "`forgotten`". Every resource passed into a function has to either be used up by it, by returning it or passing it to another function that consumes it, or destroyed, by deallocating the owned area of memory (as we shall see later).
+CN’s motivation for linear tracking of resources is its focus on
+low-level systems software in which memory is managed manually; in
+this context, memory leaks are typically very undesirable.  As a
+consequence, function specifications have to do precise bookkeeping of
+their resource footprint and, in particular, return any unused
+resources back to the caller.
+
+=== Exercises
+
+*Quadruple*. Specify the function `+quadruple_mem+`, which is similar to the earlier `+quadruple+` function, except that the input is passed as an `+int+` pointer. Write a specification that takes ownership of this pointer on entry and returns this ownership on exit, leaving the pointee value unchanged.
+
+include_example(exercises/slf_quadruple_mem.c)
 
-CN’s motivation for linear tracking of resources is its focus on low-level systems software. CN checks C programs, in which, unlike higher-level garbage-collected languages, memory is managed manually, and memory leaks are typically very undesirable.
+*Abs*. Give a specification to the function `+abs_mem+`, which computes the absolute value of a number passed as an `+int+` pointer.
 
-As a consequence, function specifications have to do precise "`book-keeping`" of their resource footprint, and, in particular, return any unused resources back to the caller.
+include_example(exercises/abs_mem.c)
 
-=== The Block resource type
+=== Block resources
 
-Aside from the `+Owned+` resource seen so far, CN has another built-in resource type: `+Block+`. Given a C-type `+T+` and pointer `+p+`, `+Block<T>(p)+` asserts the same ownership as `+Owned<T>(p)+` — so ownership of a memory cell at `+p+` the size of type `+T+` — but in contrast to `+Owned+`, `+Block+` memory is not necessarily initialised.
+Aside from the `+Owned+` resources seen so far, CN has another
+built-in type of resource called `+Block+`. Given a C-type `+T+` and
+pointer `+p+`, `+Block<T>(p)+` asserts the same ownership as
+`+Owned<T>(p)+` — ownership of a memory cell at `+p+` the size of type
+`+T+` — but, in contrast to `+Owned+`, `+Block+` memory is not assumed
+to be initialised.
 
 CN uses this distinction to prevent reads from uninitialised memory:
 
-* A read at C-type `+T+` and pointer `+p+` requires a resource `+Owned<T>(p)+`, i.e., ownership of _initialised_ memory at the right C-type. The load returns the `+Owned+` resource unchanged.
+* A read at C-type `+T+` and pointer `+p+` requires a resource
+  `+Owned<T>(p)+`, i.e., ownership of _initialised_ memory at the
+  right C-type. The load returns the `+Owned+` resource unchanged.
 
-* A write at C-type `+T+` and pointer `+p+` needs only a `+Block<T>(p)+` (so, unlike reads, writes to uninitialised memory are fine). The write consumes ownership of the `+Block+` resource (it destroys it) and returns a new resource `+Owned<T>(p)+` with the value written as the output. This means the resource returned from a write records the fact that this memory cell is now initialised and can be read from.
+* A write at C-type `+T+` and pointer `+p+` needs only a
+  `+Block<T>(p)+` (so, unlike reads, writes to uninitialised memory
+  are fine). The write consumes ownership of the `+Block+` resource
+  (it destroys it) and returns a new resource `+Owned<T>(p)+` with the
+  value written as the output. This means the resource returned from a
+  write records the fact that this memory cell is now initialised and
+  can be read from.
+// TODO: BCP: Not sure I understand "returns a new resource `+Owned<T>(p)+` with the value written as the output" -- perhaps in part because I don't understand what the output of a resource means when the resource is not in the context o a take expression.
 
-Since `+Owned+` carries the same ownership as `+Block+`, just with the additional information that the `+Owned+` memory is initalised, a resource `+Owned<T>(p)+` is "`at least as good`" as `+Block<T>(p)+` — an `+Owned<T>(p)+` resource can be used whenever `+Block<T>(p)+` is needed. For instance CN’s type checking of a write to `+p+` requires a `+Block<T>(p)+`, but if an `+Owned<T>(p)+` resource is what is available, this can be used just the same. This allows an already-initialised memory cell to be over-written again.
+Since `+Owned+` carries the same ownership as `+Block+`, just with the
+additional information that the `+Owned+` memory is initalised, a
+resource `+Owned<T>(p)+` is "`at least as good`" as `+Block<T>(p)+` —
+an `+Owned<T>(p)+` resource can be used whenever `+Block<T>(p)+` is
+needed. For instance CN’s type checking of a write to `+p+` requires a
+`+Block<T>(p)+`, but if an `+Owned<T>(p)+` resource is what is
+available, this can be used just the same. This allows an
+already-initialised memory cell to be over-written again.
 
-Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output: its output is `+void+`/`+unit+`.
+Unlike `+Owned+`, whose output is the pointee value, `+Block+` has no meaningful output.
 
-=== Write example
+=== Writing through pointers
 
-Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the pointee value.
+Let’s explore resources and their outputs in another example. The C function `+incr+` takes an `+int+` pointer `+p+` and increments the value in the memory cell that it poinbts to.
 
-include_example(solutions/slf0_basic_incr.signed.c)
+include_example(exercises/slf0_basic_incr.signed.c)
 
-In the precondition we assert ownership of resource `+Owned<int>(p)+`, binding its output/pointee value to `+v1+`, and use `+v1+` to specify that `+p+` must point to a sufficiently small value at the start of the function not to overflow when incremented. The postcondition asserts ownership of `+p+` with output `+v2+`, as before, and uses this to express that the value `+p+` points to is incremented by `+incr+`: `+v2 == v1+1i32+`.
+In the precondition we assert ownership of resource `+Owned<int>(p)+`,
+binding its output/pointee value to `+P+`, and use `+P+` to specify
+that `+p+` must point to a sufficiently small value at the start of
+the function so as not to overflow when incremented. The postcondition
+asserts ownership of `+p+` with output `+P_post+`, as before, and uses
+this to express that the value `+p+` points to is incremented by
+`+incr+`: `+P_post == P + 1i32+`.
 
 If we incorrectly tweaked this specification and used `+Block<int>(p)+` instead of `+Owned<int>(p)+` in the precondition, as below, then CN would reject the program.
 
@@ -325,13 +446,23 @@ Resource needed: Owned<signed int>(p)
 Consider the state in /var/folders/_v/ndl32wpj4bb3y9dg11rvc8ph0000gn/T/state_5da0f3.html
 ....
 
-The `+Owned<int>(p)+` resource required for reading is missing, since, as per precondition, only `+Block<int>(p)+` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure:
+The `+Owned<int>(p)+` resource required for reading is missing, since, per the precondition, only `+Block<int>(p)+` is available. Checking the linked HTML file confirms this. Here the section "`Available resources`" lists all resource ownership at the point of the failure:
 
-* `+Block<signed int>(p)(u)+`, so ownership of uninitialised memory at location `+p+`; the output is a `+void+`/`+unit+` value `+u+` (specified in the second pair of parentheses)
+* `+Block<signed int>(p)(u)+`, i.e., ownership of uninitialised memory
+  at location `+p+`; the output is a `+void+`/`+unit+` value `+u+`
+  (specified in the second pair of parentheses)
 
-* `+Owned<signed int*>(&ARG0)(p)+`, the ownership of (initialised) memory at location `+&ARG0+`, so the memory location where the first function argument is stored; its output is the pointer `+p+` (not to be confused with the pointee of `+p+`); and finally
+* `+Owned<signed int*>(&ARG0)(p)+`, the ownership of (initialised)
+  memory at location `+&ARG0+`, i.e., the memory location where the
+  first function argument is stored; its output is the pointer `+p+`
+  (not to be confused with the pointee of `+p+`); and finally
 
-* `+__CN_Alloc(&ARG0)(void)+` is a resource that records allocation information for location `+&ARG0+`; this is related to CN’s memory-object semantics, which we ignore for the moment.
+* `+__CN_Alloc(&ARG0)(void)+` is a resource that records allocation
+  information for location `+&ARG0+`; this is related to CN’s
+  memory-object semantics, which we ignore for the moment.
+
+// TODO: BCP: These bullet points are all a bit mysterious and maybe TMI.  More generally, we should double check that this is actually the information displayed in the current HTML output...
+// Dhruv: It is displayed, but hidden. And perhaps TMI right now, but once the memory model lands properly, will sadly be the price of entry to writing verifiable (semantically well-defined) C.
 
 === Exercises
 
@@ -345,17 +476,30 @@ include_example(exercises/slf3_basic_inplace_double.c)
 
 === Multiple owned pointers
 
-When functions manipulate multiple pointers, we can assert their ownership just like before. However (as in standard separation logic) pointer ownership is unique, so simultaneous ownership of `+Owned+` or `+Block+` resources for two pointers requires these pointers to be disjoint.
+When functions manipulate multiple pointers, we can assert their
+ownership just like before. However
+pointer ownership in CN is unique -- that is, simultaneously owning
+`+Owned+` or `+Block+` resources for two pointers implies that these
+pointers are disjoint.
+
+The following example shows the use of two `+Owned+` resources for
+accessing two different pointers by a function `+add+`, which reads
+two `+int+` values in memory, at locations `+p+` and `+q+`, and
+returns their sum.
 
-The following example shows the use of two `+Owned+` resources for accessing two different pointers: function `+add+` reads two `+int+` values in memory, at locations `+p+` and `+q+`, and returns their sum.
+// TODO: BCP: Hmmm -- I'm not very sure that the way I've been naming things is actually working that well.  The problem is that in examples like this we computer "thing pointed to by p" at both C and CN levels.  At the C level, the thing pointed to by p obviously cannot also be called p, so it doesn't make sense for it to be called P at the CN level, right?  Maybe we need to think again, but hoinestly I am not certain that it is *not* working either.  So I'm going to opush on for now...
 
 include_example(exercises/add_read.c)
 
 This time we use C’s `+unsigned int+` type. In C, over- and underflow of unsigned integers is not undefined behaviour, so we do not need any special preconditions to rule this out. Instead, when an arithmetic operation at unsigned type goes outside the representable range, the value "`wraps around`".
 
-The CN variables `+m+` and `+n+` (resp. `+m2+` and `+n2+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type.
+The CN variables `+P+` and `+Q+` (resp. `+P_post+` and `+Q_post+`) for the pointee values of `+p+` and `+q+` before (resp. after) the execution of `+add+` have CN basetype `+u32+`, so unsigned 32-bit integers, matching the C `+unsigned int+` type. Like C’s unsigned integer arithmetic, CN unsigned int values wrap around when exceeding the value range of the type.
 
-Hence, the postcondition `+return == m+n+` holds also when the sum of `+m+` and `+n+` is greater than the maximal `+unsigned int+` value.
+Hence, the postcondition `+return == P + Q+` holds also when the sum of `+P+` and `+Q+` is greater than the maximal `+unsigned int+` value.
+
+// TODO: BCP: I wonder whether we should uniformly use i32 integers everywhere in the tutorial (just mentioning in the bullet list below that there are other integer types, and using i64 for calculations that may overflow).  Forgetting which integer type I was using was a common (and silly) failure mode when I was first working through the tutorial.
+// Dhruv: Sensible.
+// BCP: ... On second thought, maybe settling on u32 instead of i32 in most places is better (fewer things to prove).  Or maybe it doesn't matter much.  For the start of the tutorial, i32 is important because the examples are all about overflow.  But after that we could go either way.
 
 In the following we will sometimes use unsigned integer types to focus on specifying memory ownership, rather than the conditions necessary to show absence of C arithmetic undefined behaviour.
 
@@ -371,23 +515,38 @@ include_example(exercises/slf8_basic_transfer.c)
 
 == Ownership of compound objects
 
-So far all examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types.
+So far, our examples have worked with just integers and pointers, but larger programs typically also manipulate compound values, often represented using C struct types. Specifying functions manipulating structs works in much the same way as with basic types.
 
 For instance, the following example uses a `+struct+` `+point+` to represent a point in two-dimensional space. The function `+transpose+` swaps a point’s `+x+` and `+y+` coordinates.
 
 include_example(exercises/transpose.c)
 
-Here the precondition asserts ownership for `+p+`, at type `+struct point+`; the output `+s+` is a value of CN type `+struct point+`, i.e. a record with members `+i32+` `+x+` and `+i32+` `+y+`. The postcondition similarly asserts ownership of `+p+`, with output `+s2+`, and asserts the coordinates have been swapped, by referring to the members of `+s+` and `+s2+` individually.
+Here the precondition asserts ownership for `+p+`, at type `+struct
+point+`; the output `+P_post+` is a value of CN type `+struct point+`,
+i.e. a record with members `+i32+` `+x+` and `+i32+` `+y+`. The
+postcondition similarly asserts ownership of `+p+`, with output
+`+P_post+`, and asserts the coordinates have been swapped, by referring to
+the members of `+P+` and `+P_post+` individually.
+
+// TODO: BCP: This paragraph is quite confusing if read carefully: it seems to say that the "take" in the requires clause returns a different type than the "tajke" in the "ensures" clause.  Moreover, even if the reader decides that this cannot be the case and they have to return the same type, they may wonder whether thius type is a C type (which is what it looks like, since there is only one struct declaration, and it is not in a magic comment) or a CN type (which might be expected, since it is the result of a "take").  I *guess* what's going on here is that every C type is automatically reflected as a CN type with the same name.  But this story is also not 100% satisfying, since the basic numeric types don't work this way: each C numeric type has an *analog* in CN, but with a different name.
+////
+// Dhruv:
+C supports strong updates in certain situations and so take _ = Owned<ct>(p) in the requires clause could very well have a different C type than take _ = Owned<ct2>(p) in the ensures clause.
+
+The reason Owned needs a C-type is so that it can (a) figure out the size of the sub-heap being claimed and (b) figure out how one may need to destructure the type (unions, struct fields and padding, arrays). The relationship is that for take x = Owned<ct>(expr), expr : pointer, x : to_basetype(ct).
+
+There is a design decision to consider here rems-project/cerberus#349
+////
 
 === Compound Owned and Block resources
 
-While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and pass these as values, even to other functions.
+While one might like to think of a struct as a single (compound) object that is manipulated as a whole, C permits more flexible struct manipulation: given a struct pointer, programmers can construct pointers to _individual struct members_ and manipulate these as values, including even passing them to other functions.
 
-CN therefore cannot treat resources for compound C types, such as structs, as primitive, indivisible units. Instead, `+Owned<T>+` and `+Block<T>+` are defined inductively in the structure of the C-type `+T+`.
+CN therefore cannot treat resources for compound C types like structs as primitive, indivisible units. Instead, `+Owned<T>+` and `+Block<T>+` are defined inductively on the structure of the C-type `+T+`.
 
-For struct types `+T+`, the `+Owned<T>+` resource is defined as the collection of `+Owned+` resources for its members (as well as `+Block+` resources for any padding bytes in-between). The resource `+Block<T>+`, similarly, is made up of `+Block+` resources for all members (and padding bytes).
+For struct types `+T+`, the `+Owned<T>+` resource is defined as the collection of `+Owned+` resources for its members (as well as `+Block+` resources for any padding bytes in-between them). The resource `+Block<T>+`, similarly, is made up of `+Block+` resources for all members (and padding bytes).
 
-To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and recompose it, as needed. The following example illustrates this.
+To handle code that manipulates pointers into parts of a struct object, CN can automatically decompose a struct resource into the member resources, and it can recompose the struct later, as needed. The following example illustrates this.
 
 Recall the function `+zero+` from our earlier exercise. It takes an `+int+` pointer to uninitialised memory, with `+Block<int>+` ownership, and initialises the value to zero, returning an `+Owned<int>+` resource with output `+0+`.
 
@@ -397,25 +556,29 @@ include_example(exercises/init_point.c)
 
 As stated in its precondition, `+init_point+` receives ownership `+Block<struct point>(p)+`. The `+zero+` function, however, works on `+int+` pointers and requires `+Block<int>+` ownership.
 
-CN can prove the calls to `+zero+` with `+&p->x+` and `+&p->y+` are safe because it decomposes the `+Block<struct point>(p)+` into two `+Block<int>+`, one for member `+x+`, one for member `+y+`. Later, the reverse happens: following the two calls to `+zero+`, as per `+zero+`’s precondition, `+init_point+` has ownership of two adjacent `+Owned<int>+` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `+init_point+` requires ownership `+Owned<struct point>(p)+`, CN combines these back into a compound resource. The resulting `+Owned<point struct>+` resource has for an output the struct value `+s2+` that is composed of the zeroed member values for `+x+` and `+y+`.
+CN can prove the calls to `+zero+` with `+&p->x+` and `+&p->y+` are safe because it decomposes the `+Block<struct point>(p)+` into a `+Block<int>+` for member `+x+` and a `+Block<int>+` for member `+y+`. Later, the reverse happens: following the two calls to `+zero+`, as per `+zero+`’s precondition, `+init_point+` has ownership of two adjacent `+Owned<int>+` resources – ownership for the two struct member pointers, with the member now initialised. Since the postcondition of `+init_point+` requires ownership `+Owned<struct point>(p)+`, CN combines these back into a compound resource. The resulting `+Owned<point struct>+` resource has for an output the struct value `+P_post+` that is composed of the zeroed member values for `+x+` and `+y+`.
 
 === Resource inference
 
 To handle the required resource inference, CN "`eagerly`" decomposes all `+struct+` resources into resources for the struct members, and "`lazily`" re-composes them as needed.
 
-We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function (more on CN assertions later), so we can inspect CN’s proof context shown in the error report.
+We can see this if, for instance, we experimentally change the `+transpose+` example from above to force a type error. Let’s insert an `+/*@ assert(false) @*/+` CN assertion in the middle of the `+transpose+` function, so we can inspect CN’s proof context shown in the error report.  (More on CN assertions later.)
+
+// TODO: BCP: Recheck that what we say here matches what it actually looks like
 
 include_example(exercises/transpose.broken.c)
 
 The precondition of `+transpose+` asserts ownership of an `+Owned<struct point>(p)+` resource. The error report now instead lists under "`Available resources`" two resources:
 
-* `+Owned<signed int>(member_shift<point>(p, x))+` with output `+s.x+` and
+* `+Owned<signed int>(member_shift<point>(p, x))+` with output `+P.x+` and
 
-* `+Owned<signed int>(member_shift<point>(p, y))+` with output `+s.y+`
+* `+Owned<signed int>(member_shift<point>(p, y))+` with output `+P.y+`
+
+// TODO: BCP: We should verify that it really does say this.
 
 Here `+member_shift<s>(p,m)+` is the CN expression that constructs, from a `+struct s+` pointer `+p+`, the "`shifted`" pointer for its member `+m+`.
 
-When the function returns the two member resources are recombined "`on demand`" to satisfy the postcondition `+Owned<struct point>(p)+`.
+When the function returns, the two member resources are recombined "`on demand`" to satisfy the postcondition `+Owned<struct point>(p)+`.
 
 === Exercises
 
@@ -437,9 +600,11 @@ CP: Agreed. For now continuing with arrays, but will return to this later.
 
 == Arrays and loops
 
-Another common datatype in C is arrays. Reasoning about memory ownership for arrays is more difficult than for the datatypes we have seen so far: C allows the programmer to access arrays using _computed pointers_, and the size of an array does not need to be known as a constant at compile time.
+Another common datatype in C is arrays. Reasoning about memory ownership for arrays is more difficult than for the datatypes we have seen so far, for two reasons: (1) C allows the programmer to access arrays using _computed pointers_, and (2) the size of an array does not need to be known as a constant at compile time.
+
+To support reasoning about code manipulating arrays and computed pointers, CN has _iterated resources_. For instance, to specify ownership of an `+int+` array with 10 cells starting at pointer `+p+`, CN uses the following iterated resource:
 
-To support reasoning about code manipulating arrays and computed pointers, CN has _iterated resources_. For instance, to specify ownership of an `+int+` array with 10 cells starting at pointer `+p+`, CN uses the iterated resource
+// TODO: BCP: Another tricky naming / capitalization puzzle: The index of an "each" has CN type i32, so strictly speaking I believe it should be written with a capital "I".  But insisting on this feels like insisting on a distinction that most CN programmers would never even notice, much less be confused by.  I think this is another instance of the way C and CN integer types are partly but not completely squished together.
 
 [source,c]
 ----
@@ -476,7 +641,7 @@ comprising three parts:
 
 === First array example
 
-Let’s see how this applies to a first example of an array-manipulating function. Function `+read+` takes three arguments: the base pointer `+p+` of an `+int+` array, the length `+n+` of the array, and an index `+i+` into the array; `+read+` then returns the value of the `+i+`-th array cell.
+Let’s see how this applies to a simple array-manipulating function. Function `+read+` takes three arguments: the base pointer `+p+` of an `+int+` array, the length `+n+` of the array, and an index `+i+` into the array; `+read+` then returns the value of the `+i+`-th array cell.
 
 include_example(exercises/array_load.broken.c)
 
@@ -490,7 +655,7 @@ On exit the array ownership is returned again.
 This specification, in principle, should ensure that the access `+p[i]+` is safe. However, running CN on the example produces an error: CN is unable to find the required ownership for reading `+p[i]+`.
 
 ....
-cn build/solutions/array_load.broken.c
+cn verify solutions/array_load.broken.c
 [1/1]: read
 build/solutions/array_load.broken.c:5:10: error: Missing resource for reading
   return p[i];
@@ -498,13 +663,13 @@ build/solutions/array_load.broken.c:5:10: error: Missing resource for reading
 Resource needed: Owned<signed int>(array_shift<signed int>(p, (u64)i))
 ....
 
-The reason is that when searching for a required resource, such as the `+Owned+` resource for `+p[i]+` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user.
+The reason is that, when searching for a required resource, such as the `+Owned+` resource for `+p[i]+` here, CN’s resource inference does not consider iterated resources. Quantifiers, as used by iterated resources, can make verification undecidable, so, in order to maintain predictable type checking, CN delegates this aspect of the reasoning to the user.
 
-To make the `+Owned+` resource required for accessing `+p[i]+` available to CN’s resource inference we have to "`extract`" ownership for index `+i+` out of the iterated resource.
+To make the `+Owned+` resource required for accessing `+p[i]+` available to CN’s resource inference we have to explicitly "`extract`" ownership for index `+i+` out of the iterated resource.
 
 include_example(exercises/array_load.c)
 
-Here the CN comment `+/*@ extract Owned<int>, i; @*/+` is a CN "`ghost statement`"/proof hint that instructs CN to instantiate any available iterated `+Owned<int>+` resource for index `+i+`. In our example this operation splits the iterated resource into two:
+Here the CN comment `+/*@ extract Owned<int>, i; @*/+` is a proof hint in the form of a "`ghost statement`" that instructs CN to instantiate any available iterated `+Owned<int>+` resource for index `+i+`. In our example this operation splits the iterated resource into two:
 
 [source,c]
 ----
@@ -527,27 +692,42 @@ each(i32 j; 0i32 <= j && j < n && j != i)
     { Owned<int>(array_shift<int>(p,j)) }
 ----
 
-After this extraction step, CN can use the (former) extracted resource to justify the access `+p[i]+`.
+After this extraction step, CN can use the (former) extracted resource to justify the access `+p[i]+`. Note that an `+extract+` statement's second argument can be any arithmetic expression, not just a single identifier like in this example.
 
-Following an `+extract+` statement, CN moreover remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function.
+Following an `+extract+` statement, CN remembers the extracted index and can automatically "`reverse`" the extraction when needed: after type checking the access `+p[i]+` CN must ensure the function’s postcondition holds, which needs the full array ownership again (including the extracted index `+i+`); remembering the index `+i+`, CN then automatically merges resources (1) and (2) again to obtain the required full array ownership, and completes the verification of the function.
 
-So far the specification only guarantees safe execution but does not specify the behaviour of `+read+`. To address this, let’s return to the iterated resources in the function specification. When we specify `+take a1 = each ...+` here, what is `+a1+`? In CN, the output of an iterated resource is a _map_ from indices to resource outputs. In this example, where index `+j+` has CN type `+i32+` and the iterated resource is `+Owned<int>+`, the output `+a1+` is a map from `+i32+` indices to `+i32+` values — CN type `+map<i32,i32>+`. (If the type of `+j+` was `+i64+` and the resource `+Owned<char>+`, `+a1+` would have type `+map<i64,u8>+`.)
+So far the specification only guarantees safe execution but does not
+specify the behaviour of `+read+`. To address this, let’s return to
+the iterated resources in the function specification. When we specify
+`+take A = each ...+` here, what is `+A+`? In CN, the output of an
+iterated resource is a _map_ from indices to resource outputs. In this
+example, where index `+j+` has CN type `+i32+` and the iterated
+resource is `+Owned<int>+`, the output `+A+` is a map from `+i32+`
+indices to `+i32+` values — CN type `+map<i32,i32>+`. If the type of
+`+j+` was `+i64+` and the resource `+Owned<char>+`, `+A+` would have
+type `+map<i64,u8>+`.
 
 We can use this to refine our specification with information about the functional behaviour of `+read+`.
 
 include_example(exercises/array_load2.c)
 
-We specify that `+read+` does not change the array — the outputs `+a1+` and `+a2+`, taken before and after running the function, are the same — and that the value returned is `+a1[i]+`, `+a1+` at index `+i+`.
+We specify that `+read+` does not change the array — the outputs of `+Owned+`,
+`+A+` and `+A_post+`, taken before and after running the function, are
+the same — and that the value returned is `+A[i]+`.
 
 === Exercises
 
 
 *Array read two.* Specify and verify the following function, `+array_read_two+`, which takes the base pointer `+p+` of an `+unsigned int+` array, the array length `+n+`, and two indices `+i+` and `+j+`. Assuming `+i+` and `+j+` are different, it returns the sum of the values at these two indices.
 
+// TODO: BCP: When we get around to renaming files in the examples directory, we should call this one array_swap or something else beginning with "array".
+
 include_example(exercises/add_two_array.c)
 
 ////
 TODO: BCP: In this one I got quite tangled up in different kinds of integers, then got tangled up in (I think) putting the extract declarations in the wrong place.  (I didn't save the not-working version, I'm afraid.)
+
+TODO: Sainati: I think it would be useful to have a int array version of this exercise as a worked example; I am not sure, for example, how one would express bounds requirements on the contents of an array in CN, as you would need to do here to ensure that p[i] + p[j] doesn’t overflow if p's contents are signed ints
 ////
 
 *Swap array.* Specify and verify `+swap_array+`, which swaps the values of two cells of an `+int+` array. Assume again that `+i+` and `+j+` are different, and describe the effect of `+swap_array+` on the array value using the CN map update expression `+a[i:v]+`, which denotes the same map as `+a+`, except with index `+i+` updated to `+v+`.
@@ -578,15 +758,17 @@ TODO: BCP: I wrote this, which seemed natural but did not work -- I still don't
 
 === Loops
 
-The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to *loop*, uniformly accessing all cells of an array, or sub-ranges of it.
+The array examples covered so far manipulate one or two individual cells of an array. Another typical pattern in code working over arrays is to *loop*, uniformly accessing all cells of an array or a sub-range of it.
 
 In order to verify code with loops, CN requires the user to supply loop invariants -- CN specifications of all owned resources and the constraints required to verify each iteration of the loop.
 
-
 Let's take a look at a simple first example. The following function, `+init_array+`, takes the base pointer `+p+` of a `+char+` array and the array length `+n+` and writes `+0+` to each array cell.
+
+// TODO: BCP: Rename to array_init.c
+
 include_example(exercises/init_array.c)
 
-If, for the moment, we focus just on proving safe execution of `+init_array+`, ignoring its functional behaviour, a specification might look as above: on entry `+init_array+` takes ownership of an iterated `+Owned<char>+` resource -- one `+Owned+` resource for each index `+i+` of type `+u32+` (so necessarily greater or equal to `+0+`) up to `+n+`; on exit `+init_array+` returns the ownership.
+If, for the moment, we focus just on proving safe execution of `+init_array+`, ignoring its functional behaviour, a specification might look as above: on entry, `+init_array+` takes ownership of an iterated `+Owned<char>+` resource -- one `+Owned+` resource for each index `+i+` of type `+u32+` (so necessarily greater or equal to `+0+`) up to `+n+`; on exit `+init_array+` returns the ownership.
 
 To verify this, we have to supply a loop invariant that specifies all resource ownership and the necessary constraints that hold before and after each iteration of the loop. Loop invariants are specified using the keyword `inv`, followed by CN specifications using the same syntax as in function pre- and postconditions. The variables in scope for loop invariants are all in-scope C variables, as well as CN variables introduced in the function precondition. *In loop invariants, the name of a C variable refers to its current value* (more on this shortly).
 
@@ -597,7 +779,7 @@ TODO: BCP: Concrete syntax: Why not write something like "unchanged {p,n}" or "u
 
 The main condition here is unsurprising: we specify ownership of an iterated resource for an array just like in the the pre- and postcondition.
 
-The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable, and so CN permits this as well.While in this example it is obvious that `+p+` and `+n+` do not change, CN currently requires the loop invariant to explicitly state this, using special notation `+{p} unchanged+` (and similarly for `+n+`).
+The second thing we need to do, however, is less straightforward. Recall that, as discussed at the start of the tutorial, function arguments in C are mutable. Although, in this example, it is obvious that `+p+` and `+n+` do not change, CN currently requires the loop invariant to explicitly state this, using special notation `+{p} unchanged+` (and similarly for `+n+`).
 
 **Note.** If we forget to specify `+unchanged+`, this can lead to confusing errors. In this example, for instance, CN would verify the loop against the loop invariant, but would be unable to prove a function postcondition seemingly directly implied by the loop invariant (lacking the information that the postcondition's `+p+` and `+n+` are the same as the loop invariant's). Future CN versions may handle loop invariants differently and treat variables as immutable by default.
 ////
@@ -607,19 +789,23 @@ TODO: BCP: This seems like a good idea!
 The final piece needed in the verification is an `+extract+` statement, as used in the previous examples: to separate the individual `+Owned<char>+` resource for index `+j+` out of the iterated `+Owned+` resource and make it available to the resource inference, we specify `+extract Owned<char>, j;+`.
 
 
-With the `+extract+` statements in place, CN accepts the function.
+With the `+inv+` and `+extract+` statements in place, CN accepts the function.
 
 === Second loop example
 
-However, on closer look, the specification of `+init_array+` is overly strong: it requires an iterated `+Owned+` resource for the array on entry. If, as the name suggests, the purpose of `+init_array+` is to initialise the array, then a precondition asserting only an iterated `+Block+` resource for the array should also be sufficient. The modified specification is then as follows.
+The specification of `+init_array+` is overly strong: it requires an iterated `+Owned+` resource for the array on entry. If, as the name suggests, the purpose of `+init_array+` is to initialise the array, then a precondition asserting only an iterated `+Block+` resource for the array should also be sufficient. The modified specification is then as follows.
 
 include_example(exercises/init_array2.c)
 
-This specification *should* hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `+Block+` to `+Owned+` "`state`", so that on function return the full array is initialised. (Recall that stores only require `+Block+` ownership of the written memory location, so ownership of not-necessarily-initialised memory.)
+This specification *should* hold: assuming ownership of an uninitialised array on entry, each iteration of the loop initialises one cell of the array, moving it from `+Block+` to `+Owned+` "`state`", so that on function return the full array is initialised. (Recall that stores only require `+Block+` ownership of the written memory location, i.e., ownership of not-necessarily-initialised memory.)
 
-To verify this modified example we again need a loop invariant. This time, the loop invariant is more involved, however: since each iteration of the loop initialises one more array cell, the loop invariant has to do precise book-keeping of the initialisation status of the array.
+To verify this modified example we again need a loop Invariant. But
+this time the loop invariant is more involved: since each iteration of
+the loop initialises one more array cell, the loop invariant has to do
+precise book-keeping of the initialisation status of the different
+sections of the array.
 
-To do so, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `+Owned+` resource, for all other array indices we have the (unchanged) `+Block+` ownership.
+To do this, we partition the array ownership into two parts: for each index of the array the loop has already visited, we have an `+Owned+` resource, for all other array indices we have the (unchanged) `+Block+` ownership.
 
 include_example(solutions/init_array2.c)
 
@@ -631,16 +817,18 @@ Let's go through this line-by-line:
 
 - As in the previous example, we assert `+p+` and `+n+` are unchanged.
 
-- Finally, unlike in the previous example, this loop invariant involves `+j+`. We therefore also need to know that `+j+` does not exceed the array length `+n+`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `+j=n+` holds. This, in turn, is needed to show that when the function returns, ownership of the iterated `+Owned+` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource.
+- Finally, unlike in the previous example, this loop invariant involves `+j+`. We therefore also need to know that `+j+` does not exceed the array length `+n+`. Otherwise CN would not be able to prove that, on completing the last loop iteration, `+j=n+` holds. This, in turn, is needed to show that, when the function returns, ownership of the iterated `+Owned+` resource --- as specified in the loop invariant --- is fully consumed by the function's post-condition and there is no left-over unused resource.
 
 As before, we also have to instruct CN to `+extract+` ownership of individual array cells out of the iterated resources:
 
-- to allow CN to extract the individual `+Block+` to be written we use `+extract Block<char>, j;+`;
+- to allow CN to extract the individual `+Block+` to be written, we use `+extract Block<char>, j;+`;
 
 - the store returns a matching `+Owned<char>+` resource for index `+j+`;
 
-- finally, we put `+extract Owned<char>, j;+` to allow CN to "`attach`" this resource to the iterated `+Owned+` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `+extract+` only for the "`reverse`" direction.
+- finally, we add `+extract Owned<char>, j;+` to allow CN to "`attach`" this resource to the iterated `+Owned+` resource. CN issues a warning, because nothing is, in fact, extracted: we are using `+extract+` only for the "`reverse`" direction.
 
+// TODO: BCP: That last bit is mysterious.
+// Dhruv: See long explanation and issue here: rems-project/cerberus#498
 
 === Exercises
 
@@ -648,7 +836,7 @@ As before, we also have to instruct CN to `+extract+` ownership of individual ar
 
 include_example(exercises/init_array_rev.c)
 
-
+// TODO: BCP: The transition to the next section is awkward.  Needs a sentence or two to signal that we're changing topics.  Some better visual indication would also be nice.
 
 ////
 ___________________________________________________________________________
@@ -679,17 +867,35 @@ not alias...
 include_example(exercises/slf_incr2_noalias.c)
 
 But what if they do alias?  The clunky solution is to write a whole
-different version of incr2 with a different embedded specification...
+different version of `+incr2+` with a different embedded specification...
 
 include_example(exercises/slf_incr2_alias.c)
 
-This is horrible.  Much better is to define a predicate to use
-in the pre- and postconditions that captures both cases together:
+This version does correctly state that the final values of `+p+` and `+q+` are,m respectively, `+3+` and `+1+` more than their original values.  But the way we got there -- by duplicating the whole function `+incr2+`, is horrible.
+
+// TODO: Sainati: I think it would be useful here to add an explanation for how CN's type checking works.
+// For example, in the definition of BothOwned here, how is CN able to prove that `+take pv = Owned<unsigned int>(p);+`
+// type checks, since all we know about `p` in the definition of the predicate is that it's a pointer?
+
+A better way is to define a *predicate* that captures both the aliased
+and the non-aliased cases together and use it in the pre- and
+postconditions:
+
+// TODO: Sainati: I think it would be useful here to add an explanation for how CN's type checking works. 
+// For example, in the definition of BothOwned here, how is CN able to prove that `+take pv = Owned<unsigned int>(p);+` 
+// type checks, since all we know about `p` in the definition of the predicate is that it's a pointer? 
 
 include_example(exercises/slf_incr2.c)
 
+// TODO: BCP: "BothOwned" is a pretty awkward name.
+// TODO: BCP: We haven't introduced CN records.  In particular, C programmers may be surprised that we don't have to pre-declare record types.
+// TODO: BCP: the annotation on incr2 needs some unpacking for readers!!
+// TODO: BCP: first use of the "split_case" annotation
+
 == Allocating and Deallocating Memory
 
+// TODO: BCP: Again, more text is needed to set up this discussion.
+
 At the moment, CN does not understand the `+malloc+` and `+free+`
 functions.  They are a bit tricky because they rely on a bit of
 polymorphism and a typecast between `+char*+` -- the result type of
@@ -700,7 +906,7 @@ However, for any given type, we can define a type-specific function
 that allocates heap storage with exactly that type.  The
 implementation of this function cannot be checked by CN, but we can
 give just the spec, together with a promise to link against an
-external C library providing the implementation:
+external C library providing a correct (but not verified!) implementation:
 
 include_example(exercises/malloc.h)
 
@@ -709,9 +915,11 @@ inside a CN file by marking it with the keyword `+trusted+` at the top
 of its CN specification.)
 
 Similarly:
+
 include_example(exercises/free.h)
 
 Now we can write code that allocates and frees memory:
+
 include_example(exercises/slf17_get_and_free.c)
 
 We can also define a "safer", ML-style version of `+malloc+` that
@@ -735,53 +943,61 @@ pointed to by its argument.
 
 include_example(exercises/slf_ref_greater.c)
 
-=== Side Note
+=== Side note
 
 Here is another syntax for external / unknown
 functions, together with an example of a loose specification:
 
 ////
-TODO: BCP: This is a bit random -- it's not clear people need to know about this alternate syntax, and it's awkwardly mixed with a semi-interesting example that's not relevant to this section.
+TODO: BCP: This is a bit random -- it's not clear people need to know about this alternate syntax, and it's awkwardly mixed with a semi-interesting example that's not relevant to this section.  Also awkwardly placed, right here.
 ////
 
 include_example(exercises/slf18_two_dice.c)
 
 == Lists
 
+// TODO: BCP: Better intro needed
+
 Now it's time to look at some more interesting heap structures.
 
 To begin with, here is a C definition for linked list cells, together
 with allocation and deallocation functions:
 
-include_example(exercises/list_c_types.h)
+// TODO: BCP: Here and in several other places, we should use the "take _ = ..." syntax when the owned value is not used.  And we should explain it the first time we use it.
+
+include_example(exercises/list/c_types.h)
+
+// TODO: BCP: Per discussion with Christopher, Cassia, and Daniel, the word "predicate" is quite confusing for newcomers (in logic, predicates do not return things!).  A more neutral word might make for significantly easier onboarding.
+// Dhruv: Or no keyword? rems-project/cerberus#304  How about traversal?
+// BCP: No keyword sounds even better. But "traversal" in the interim is not bad. Or maybe "extractor" or something like that?
 
 To write specifications for C functions that manipulate lists, we need
-to define a CN "predicate" that describes *mathematical* list
-structures, as one would do in ML, Haskell, or Coq.  (We call them
-"sequences" here to avoid overloading the word "list".)
+to define a CN "predicate" that describes specification-level list
+structures, as one would do in ML, Haskell, or Coq.  We use the
+datatype `+List+` for CN-level lists.
 
-Intuitively, the `+IntList+` predicate walks over a pointer structure
-in the C heap and extracts an `+Owned+` version of the mathematical
-list that it represents.
+Intuitively, the `+SLList_At+` predicate walks over a singly-linked
+pointer structure in the C heap and extracts an `+Owned+` version of
+the CN-level list that it represents.
 
-include_example(exercises/list_cn_types.h)
+include_example(exercises/list/cn_types.h)
 
-We can also write specification-level "functions" by ordinary
-functional programming (in slightly strange, unholy-union-of-C-and-ML
+We can also write *functions* on CN-level lists by ordinary functional
+programming (in a slightly strange, unholy-union-of-C-and-Rust
 syntax):
 
-include_example(exercises/list_hdtl.h)
+include_example(exercises/list/hdtl.h)
 
-We use the `+IntList+` predicate to specify functions returning the
+We use the `+SLList_At+` predicate to specify functions returning the
 empty list and the cons of a number and a list.
 
-include_example(exercises/list_constructors.h)
+include_example(exercises/list/constructors.h)
 
-Finally, we can collect all this stuff into a single header file and
+Finally, we can collect all this stuff into a single header file.  (We
 add the usual C `+#ifndef+` gorp to avoid complaints from the compiler
-if it happens to get included twice from the same source file later.
+if it happens to get included twice from the same source file later.)
 
-include_example(exercises/list.h)
+include_example(exercises/list/headers.h)
 
 ////
 TODO: BCP: The 'return != NULL' should not be needed, but to remove it
@@ -797,22 +1013,23 @@ verifying list-manipulating functions.  First, `+append+`.
 Here is its specification (in a separate file, because we'll want to
 use it multiple times below.)
 
-include_example(exercises/list_append.h)
+include_example(exercises/list/append.h)
 
 Here is a simple destructive `+append+` function.  Note the two uses
 of the `+unfold+` annotation in the body, which are needed to help the
-CN typechecker.
+CN typechecker. The `+unfold+` annotation is an instruction to CN to replace a call to a recursive (CN) function (in this case `+append+`)
+with its definition, and is necessary because CN is unable to automatically determine when and where to expand recursive definitions on its own.
 
 // TODO: BCP: Can someone add a more technical explanation of why they are needed and exactly what they do?
 
-include_example(exercises/append.c)
+include_example(exercises/list/append.c)
 
 === List copy
 
 Here is an allocating list copy function with a pleasantly light
 annotation burden.
 
-include_example(exercises/list_copy.c)
+include_example(exercises/list/copy.c)
 
 === Merge sort
 
@@ -823,7 +1040,11 @@ avoids allocating any new list cells in the splitting step by taking
 alternate cells from the original list and linking them together into
 two new lists of roughly equal lengths.
 
-include_example(exercises/mergesort.c)
+// TODO: BCP: We've heard from more than one reader that this example is particularly hard to digest without some additional help
+
+// TODO: BCP: Nit: Merge multiple requires and ensures clauses into one
+
+include_example(exercises/list/mergesort.c)
 
 === Exercises
 
@@ -831,48 +1052,60 @@ include_example(exercises/mergesort.c)
 `+IntList_append2+`.  (You will need some in the body as well as at
 the top.)
 
-include_example(exercises/append2.c)
+include_example(exercises/list/append2.c)
 
 Note that it would not make sense to do the usual
 functional-programming trick of copying xs but sharing ys.  (Why?)
 
 *Length*.  Add annotations as appropriate:
 
-include_example(exercises/list_length.c)
+include_example(exercises/list/length.c)
 
 *List deallocation*.  Fill in the body of the following procedure and
 add annotations as appropriate:
 
-include_example(exercises/list_free.c)
+include_example(exercises/list/free.c)
 
 *Length with an accumulator*.  Add annotations as appropriate:
 // TODO: BCP: Removing / forgetting the unfold in this one gives a truly
 // bizarre error message saying that the constraint "n == (n + length(L1))"
 // is unsatisfiable...
 
+// TODO: Sainati: when I went through the tutorial, the file provided for this exercise was already "complete" in that
+// it already had all the necessary annotations present for CN to verify it
+
 include_example(exercises/slf_length_acc.c)
 
 == Working with External Lemmas
 
-**TODO**: This section should also show what the proof of the lemmas
+// TODO: BCP: This section should also show what the proof of the lemmas
 looks like on the Coq side!
 
 // TODO: BCP: This needs to be filled in urgently!!
+// Dhruyv: There are some examples in the Cerberus repo tests? rems-project/cerberus@20d9d5c
+
+////
+TODO: BCP: 
+think about capitalization, etc., for lemma names
+  push_lemma should be Push_lemma, I guess?  Or lemma_push?
+  snoc_facts should be lemma_Snoc or something
+  others?
+////
 
 === List reverse
 
 The specification of list reversal in CN relies on the familiar
 recursive list reverse function, with a recursive helper.
 
-include_example(exercises/list_snoc.h)
-include_example(exercises/list_rev.h)
+include_example(exercises/list/snoc.h)
+include_example(exercises/list/rev.h)
 
 To reason about the C implementation of list reverse, we need to help
 the SMT solver by enriching its knowledge base with a couple of facts
 about lists.  The proofs of these facts require induction, so in CN we
 simply state them as lemmas and defer the proofs to Coq.
 
-include_example(exercises/list_rev_lemmas.h)
+include_example(exercises/list/rev_lemmas.h)
 
 Having stated these lemmas, we can now complete the specification and
 proof of `+IntList_rev+`.  Note the two places where `+apply+` is used
@@ -885,19 +1118,21 @@ general scope where a given set of lemmas might be needed, rather than
 specifying exactly where to use them.)
 ////
 
-include_example(exercises/list_rev.c)
+include_example(exercises/list/rev.c)
 
 For comparison, here is another way to write the program, using a
 while loop instead of recursion, with its specification and proof.
 
 // TODO: BCP: Why 0 instead of NULL??  (Is 0 better?)
 
-include_example(exercises/list_rev_alt.c)
+include_example(exercises/list/rev_alt.c)
 
 === Exercises
 
 **Sized stacks:** Fill in annotations where requested:
 
+// TODO: BCP: type_synonym has not been introduced yet
+
 include_example(exercises/slf_sized_stack.c)
 
 // ======================================================================
@@ -914,6 +1149,8 @@ include_example(exercises/slf_sized_stack.c)
 
 == CN Style
 
+// TODO: BCP: If we are agreed on the naming conventions suggested in /NAMING-CONVENTIONS.md, we could move that material here.
+
 This section gathers some advice on stylistic conventions and best
 practices in CN.
 
@@ -955,45 +1192,48 @@ include_example(exercises/const_example_lessgood.c)
 potential source of nasty bugs!
 
 
+// ======================================================================
+// ======================================================================
 // ======================================================================
 
 == Case Studies
 
 To close out the tutorial, let's look at some larger examples.
 
-=== Imperative Queues
+=== Case Study: Imperative Queues
 
 A queue is a linked list with O(1) operations for adding things to one
 end (the "back") and removing them from the other (the "front").  Here
 are the C type definitions:
 
-include_example(exercises/queue_c_types.h)
+include_example(exercises/queue/c_types.h)
 
 A queue consists of a pair of pointers, one pointing to the front
-element, which is the first in a linked list of `+int_queueCell+`s,
+element, which is the first in a linked list of `+queue_cell+`s,
 the other pointing directly to the last cell in this list.  If the
 queue is empty, both pointers are NULL.
 
-Abstractly, a queue just represents a list, so we can reuse the `+seq+`
+Abstractly, a queue just represents a list, so we can reuse the `+List+`
 type from the list examples earlier in the tutorial.
 
-include_example(exercises/queue_cn_types_1.h)
-////
-TODO: BCP: If we're going to call this IntQueuePtr (Dhruv's suggestion), then
-we have to rename other things above for consistency...
-////
+include_example(exercises/queue/cn_types_1.h)
 
-Given a pointer to an `+int_queue+` struct, this predicate grabs
-ownership of the struct, asserts that the `+front+` and `+back+` pointers
-must either both be NULL or both be non-NULL, and then hands off to an
-auxiliary predicate `+IntQueueFB+`.  (Conceptually, `+IntQueueFB+` is
-part of `+IntQueuePTR+`, but CN currently allows conditional
-expressions only at the beginning of predicate definitions, not after
-a `+take+`.)
+Given a pointer to a `+queue+` struct, this predicate grabs ownership
+of the struct, asserts that the `+front+` and `+back+` pointers must
+either both be NULL or both be non-NULL, and then hands off to an
+auxiliary predicate `+QueueFB+`.  Note that `+QueuePtr_At+` returns a
+`+List+` -- that is, the abstract view of a queue heap structure is
+simply the sequence of elements that it contains.  The difference
+between a queue and a singly or doubly linked list is simply one of
+concrete representation.
 
-`+IntQueueFB+` is where the interesting part starts:
+`+QueueFB+` is where the interesting part starts.  (Conceptually,
+`+QueueFB+` is part of `+QueuePTR+`, but CN currently allows
+conditional expressions only at the beginning of predicate
+definitions, not after a `+take+`, so we need to make a separate
+auxiliary predicate.)
 
-include_example(exercises/queue_cn_types_2.h)
+include_example(exercises/queue/cn_types_2.h)
 
 First, we case on whether the `+front+` of the queue is NULL.  If so,
 then the queue is empty and we return the empty sequence.
@@ -1001,7 +1241,7 @@ then the queue is empty and we return the empty sequence.
 If the queue is not empty, we need to walk down the linked list of
 elements and gather up all their values into a sequence.  But we must
 treat the last element of the queue specially, for two reasons.
-First, because the `+push+` operation is going to follow the `+back+`
+First, since the `+push+` operation is going to follow the `+back+`
 pointer directly to the last list cell without traversing all the
 others, we need to `+take+` that element now rather than waiting to
 get to it at the end of the recursion starting from the `+front+`.
@@ -1011,10 +1251,10 @@ the second to last cell (or the `+front+` pointer, if there is only
 one cell in the list), so we need to be careful not to `+take+` this
 cell twice.
 
-Accordingly, we begin by `+take+`ing the tail cell and passing it
-separately to the `+IntQueueAux+` predicate, which has the job of
+Accordingly, we begin by `+take+`-ing the tail cell and passing it
+separately to the `+QueueAux+` predicate, which has the job of
 walking down the cells from the front and gathering all the rest of
-them into a sequence.  We take the result from `+IntQueueAux+` and
+them into a sequence.  We take the result from `+QueueAux+` and
 `+snoc+` on the very last element.
 
 The `+assert (is_null(B.next))+` here gives the CN verifier a crucial
@@ -1024,38 +1264,38 @@ its `+next+` field will always be NULL.
 
 // TODO: BCP: How to help people guess that this is needed??
 
-Finally, the `+IntQueueAux+` predicate recurses down the list of
-cells.
+Finally, the `+QueueAux+` predicate recurses down the list of
+cells and returns a list of their contents.
 
-include_example(exercises/queue_cn_types_3.h)
+include_example(exercises/queue/cn_types_3.h)
 
 Its first argument (`+f+`) starts out at `+front+` and progresses
-through the list on recursive calls; its `+b+` argument is always a
+through the queue on recursive calls; its `+b+` argument is always a
 pointer to the very last cell.
 
 When `+f+` and `+b+` are equal, we have reached the last cell and
-there is nothing to do.  (We don't even have to build a singleton
-list: that's going to happen one level up, in `+IntQueueFB+`.)
+there is nothing to do.  We don't even have to build a singleton
+list: that's going to happen one level up, in `+QueueFB+`.
 
 Otherwise, we `+take+` the fields of the `+f+`, make a recurive
-call to `+IntQueueAux+` to process the rest of the cells, and cons the
+call to `+QueueAux+` to process the rest of the cells, and cons the
 `+first+` field of this cell onto the resulting sequence before
-returning it.  (Again, we need to help the CN verifier by explicitly
+returning it.  Again, we need to help the CN verifier by explicitly
 informing it of the invariant that we know, that `+C.next+` cannot be
-null if `+f+` and `+b+` are different.)
+null if `+f+` and `+b+` are different.
 
 Now we need a bit of boilerplate: just as with linked lists, we need
 to be able to allocate and deallocate queues and queue cells.  There
 are no interesting novelties here.
 
-include_example(exercises/queue_allocation.h)
+include_example(exercises/queue/allocation.h)
 
 // ======================================================================
 
 *Exercise*: The function for creating an empty queue just needs to set
 both of its fields to NULL.  See if you can fill in its specification.
 
-include_example(exercises/queue_empty.c)
+include_example(exercises/queue/empty.c)
 
 // ======================================================================
 
@@ -1064,12 +1304,12 @@ first.
 
 Here's the unannotated C code -- make sure you understand it.
 
-include_example(exercises/queue_push_orig.broken.c)
+include_example(exercises/queue/push_orig.broken.c)
 
 *Exercise*: Before reading on, see if you can write down a reasonable
 top-level specification for this operation.
 
-(One thing you might find odd about this code is that there's a
+One thing you might find odd about this code is that there's a
 `+return+` statement at the end of each branch of the conditional,
 rather than a single `+return+` at the bottom.  The reason for this is
 that, when CN analyzes a function body containing a conditional, it
@@ -1078,11 +1318,11 @@ the branches.  Then, if verification encounters an error related to
 this code -- e.g., "you didn't establish the `+ensures+` conditions at
 the point of returning -- the error message will be confusing because
 it will not be clear which branch of the conditional it is associated
-with.)
+with.
 
 Now, here is the annotated version of the `+push+` operation.
 
-include_example(exercises/queue_push.c)
+include_example(exercises/queue/push.c)
 
 The case where the queue starts out empty (`+q->back == 0+`) is easy.
 CN can work it out all by itself.
@@ -1093,7 +1333,10 @@ elements, so we should expect that validating `+push+` is going to
 require some reasoning about this sequence.  Here, in fact, is the
 lemma we need.
 
-include_example(exercises/queue_push_lemma.h)
+// TODO: BCP: Not sure I can explain what "pointer" means here, or why we don't need to declare more specific types for these arguments to the lemma.
+// Dhruv: See above comments about strong updates: in a requires/ensures, the types are given by the arguments in scope, but here we don't have that.
+
+include_example(exercises/queue/push_lemma.h)
 
 This says, in effect, that we have two choices for how to read out the
 values in some chain of queue cells of length at least 2, starting
@@ -1116,17 +1359,17 @@ as part of the rest (so that the new `+back+` cell can now be treated
 specially).
 
 One interesting technicality is worth noting: After the assignment
-`+q->back = c+` we can no longer prove `+IntQueueFB(q->front,
-oldback)+`, but we don't care, since we want to prove
-`+IntQueueFB(q->front, q->back)+`. However, crucially,
-`+IntQueueAux(q->front, oldback)+` is still true.
+`+q->back = c+`, we can no longer prove `+QueueFB(q->front,
+oldback)+`, but we don't care about this, since we want to prove
+`+QueueFB(q->front, q->back)+`. However, crucially,
+`+QueueAux(q->front, oldback)+` is still true.
 
 // ======================================================================
 
 Now let's look at the `+pop+` operation.  Here is the un-annotated
 version:
 
-include_example(exercises/queue_pop_orig.broken.c)
+include_example(exercises/queue/pop_orig.broken.c)
 
 *Exercise*: Again, before reading on, see if you can write down a
 plausible top-level specification.  (For extra credit, see how far you
@@ -1134,23 +1377,23 @@ can get with verifying it!)
 
 Here is the fully annotated `+pop+` code:
 
-include_example(exercises/queue_pop.c)
+include_example(exercises/queue/pop.c)
 
 There are three annotations to explain.  Let's consider them in order.
 
 First, the `+split_case+` on `+is_null(q->front)+` is needed to tell
 CN which of the branches of the `+if+` at the beginning of the
-`+IntQueueFB+` predicate it can "unpack".  (`+IntQueuePtr+` can be
-unpacked immediately because it is unconditional, but `+IntQueueFB+`
+`+QueueFB+` predicate it can "unpack".  (`+QueuePtr_At+` can be
+unpacked immediately because it is unconditional, but `+QueueFB+`
 cannot.)
 // TODO: BCP: the word "unpack" is mysterious here.
 
-The guard/condition for `+IntQueueFB+` is `+is_null(front)+`, which is
+The guard/condition for `+QueueFB+` is `+is_null(front)+`, which is
 why we need to do a `+split_case+` on this value. On one branch of the
-`+split_case+`, we have a contradiction: the fact that `+before ==
-Seq_Nil{}+` (from `+IntQueueFB+`) conflicts with `+before != Seq_Nil+`
+`+split_case+` we have a contradiction: the fact that `+before ==
+Nil{}+` (from `+QueueFB+`) conflicts with `+before != Nil+`
 from the precondition, so that case is immediate.  On the other
-branch, CN now knows that the queue is non-empty as required and type
+branch, CN now knows that the queue is non-empty, as required, and type
 checking proceeds.
 
 When `+h == q->back+`, we are in the case where the queue contains
@@ -1165,7 +1408,7 @@ the `+front+` field of the queue structure to point to the next cell.
 To push the verification through, we need a simple lemma about the
 `+snoc+` function:
 
-include_example(exercises/queue_pop_lemma.h)
+include_example(exercises/queue/pop_lemma.h)
 
 The crucial part of this lemma is the last three lines, which express
 a simple, general fact about `+snoc+`:
@@ -1198,17 +1441,16 @@ telltale clues in the error report that suggest what the problem was?
 
 * Remove `+assert (is_null(B.next));+` from `+InqQueueFB+`.
 * Remove `+assert (is_null(B.next));+` from `+InqQueueAux+`.
-* Remove one or both of occurrences of `+freeIntQueueCell(f)+` in
-  `+IntQueue_pop+`.
+* Remove one or both of occurrences of `+free_queue_cell(f)+` in
+  `+pop_queue+`.
 * Remove, in turn, each of the CN annotations in the bodies of
-  `+IntQueue_pop+` and `+IntQueue_push+`.
+  `+pop_queue+` and `+push_queue+`.
 
 *Exercise*: The conditional in the `+pop+` function tests whether or
 not `+f == b+` to find out whether we have reached the last element of
 the queue.  Another way to get the same information would be to test
 whether `+f->next == 0+`.  Can you verify this version?
-
-Note: I (BCP) have not worked out the details, so am not sure how hard
+*Note*: I (BCP) have not worked out the details, so am not sure how hard
 this is (or if it is even not possible, though I'd be surprised).
 Please let me know if you get it working!
 
@@ -1216,136 +1458,155 @@ Please let me know if you get it working!
 it might seem reasonable to move the identical assignments to `+x+` in both
 branches to above the `+if+`.  This doesn't "just work" because the
 ownership reasoning is different.  In the first case, ownership of
-`+h+` comes from `+IntQueueFB+` (because `+h == q->back+`). In the
-second case, it comes from `+IntQueueAux+` (because `+h !=
+`+h+` comes from `+QueueFB+` (because `+h == q->back+`). In the
+second case, it comes from `+QueueAux+` (because `+h !=
 q->back+`).
 
 Can you generalize the `+snoc_facts+` lemma to handle both cases?  You
 can get past the dereference with a `+split_case+` but formulating the
 lemma before the `+return+` will be a bit more complicated.
-
-Note: Again, this has not been shown to be possible, but Dhruv
+//
+*Note*: Again, this has not been shown to be possible, but Dhruv
 believes it should be!
 
-=== Doubly Linked Lists
+// ======================================================================
+// ======================================================================
+// ======================================================================
+=== Case Study: Doubly Linked Lists
+
+// TODO: BCP: The rest of the tutorial (from here to the end) needs to be checked for consistency of naming and capitalization conventions.
 
 A doubly linked list is a linked list where each node has a pointer
 to both the next node and the previous node. This allows for O(1)
-operations for adding or removing nodes anywhere in the list. Here is
-the C type definition:
+operations for adding or removing nodes anywhere in the list. 
 
-include_example(exercises/Dbl_Linked_List/c_types.h)
+Because of all the sharing in this data structure, the separation
+reasoning is a bit tricky.  We'll give you the core definitions and
+then invite you to help fill in the annotations for some of the
+functions that manipulate doubly linked lists.
 
-The idea behind the representation of this list is that we don't keep 
-track of the front or back, but rather we take any node in the list 
-and have a sequence to the left and to the right of that node. The `left` 
-and `right` are from the point of view of the node itself, so `left` 
-is kept in reverse order. Additionally, similarly to in the 
-`Imperative Queues` example, we can reuse the `+seq+` type.
+First, here is the C type definition:
 
-include_example(exercises/Dbl_Linked_List/cn_types.h)
+include_example(exercises/dll/c_types.h)
 
-The predicate for this datatype is a bit complicated. The idea is that 
-we first want to own the node that is passed in. Then, we want to 
-follow all of the `prev` pointers to own everything backwards from the 
-node. We want to do the same for the `next` pointers to own everything 
-forwards from the node. This is how we construct our `left` and `right`
-fields.
+The idea behind the representation of this list is that we don't keep
+track of the front or back, but rather we take any node in the list
+and have a sequence to the left and to the right of that node. The `left`
+and `right` are from the point of view of the node itself, so `left`
+is kept in reverse order. Additionally, similarly to in the
+`Imperative Queues` example, we can reuse the `+List+` type.
 
-include_example(exercises/Dbl_Linked_List/predicates.h)
+include_example(exercises/dll/cn_types.h)
 
-Note that `Dll_at` takes ownership of the node passed in, and then
-calls `Own_Backwards` and `Own_Forwards` which recursively take 
-ownership of the rest of the list and add their values to the `left` 
-and `right` sequences, respectively.
+The predicate for this datatype is a bit complicated. The idea is that
+we first own the node that is passed in. Then we follow all of the
+`prev` pointers to own everything backwards from the node, and finally
+all the `next` pointers to own everything forwards from the node, to
+construct the `left` and `right` fields.
 
-Additionally, you will notice that `Own_Forwards` and `Own_Backwards` 
-include `ptr_eq` assertions for the `prev` and `next` pointers. This 
-is to ensure that the nodes in the list are correctly 
-doubly linked. For example, the line 
-`assert (ptr_eq(n.prev, prev_pointer));` in `Own_Forwards` ensures 
-that the current node correctly points backward to the previous node in the 
-list. The line `assert(ptr_eq(prev_node.next, p));` ensures that the 
-previous node correctly points forward to the current node. The same can be 
-said for these assertions in `Own_Backwards`.
+// TODO: BCP: Maybe rethink the Own_Forwards / Backwards naming -- would something like Queue_At_Left and Queue_At_Right be clearer??
+include_example(exercises/dll/predicates.h)
 
-All three of these predicates stop once they reach a null pointer. In 
-this way, we can ensure that the only null pointers in the list are at 
-the beginning and end of the list.
+Note that `Dll_at` takes ownership of the node passed in, and then
+calls `Own_Backwards` and `Own_Forwards`, which recursively take
+ownership of the rest of the list.
 
-Before we move on to the functions that manipulate the doubly linked 
-list, we need to define a few "getter" functions that will allow us 
-to access the fields of our `Dll` datatype. This will make our 
-specifications much easier to write.
+Also, notice that `Own_Forwards` and `Own_Backwards` include `ptr_eq`
+assertions for the `prev` and `next` pointers. This is to ensure that
+the nodes in the list are correctly doubly linked. For example, the
+line `assert (ptr_eq(n.prev, prev_pointer));` in `Own_Forwards`
+ensures that the current node correctly points backward to the
+previous node in the list. The line `assert(ptr_eq(prev_node.next,
+p));` ensures that the previous node correctly points forward to the
+current node. 
 
-include_example(exercises/Dbl_Linked_List/getters.h)
+Before we move on to the functions that manipulate doubly linked
+lists, we need to define a few "getter" functions that will allow us
+to access the fields of our `Dll` datatype. This will make the
+specifications easier to write.
 
-We also must include some boilerplate code for allocation and 
-deallocation.
+include_example(exercises/dll/getters.h)
 
-include_example(exercises/Dbl_Linked_List/malloc_free.h)
+We also need some boilerplate for allocation and deallocation.
 
-And we compile all of these files into a single header file.
+include_example(exercises/dll/malloc_free.h)
 
-include_example(exercises/Dbl_Linked_List/headers.h)
+For convenience, we gather all of these files into a single header file.
 
-Lastly, an important note about this representation of a doubly linked list is that there is no higher level representation of the list (such as the `int_queue` structure in the `Imperative Queues` section). This makes it difficult to reason about adding and removing things from a list that may be empty at some times. If we have an empty list, we do not want any identifier of this list to disappear altogether. To work around this problem, we represent an empty list as a null pointer and require that every function that manipulates the list must return a pointer to somewhere in the list. This way, we can always have a pointer to the list, even if it is empty.
+include_example(exercises/dll/headers.h)
 
 // ======================================================================
 
-Now we can move on to an initialization function. Since an empty list is represented as a null pointer, we will look at initializing
-a singleton list (or in other words, a list with only one item).
+Now we can move on to an initialization function. Since an empty list
+is represented as a null pointer, we will look at initializing a
+singleton list (or in other words, a list with only one item).
 
-include_example(exercises/Dbl_Linked_List/singleton.c)
+include_example(exercises/dll/singleton.c)
 
 // ======================================================================
 
 The `add` and `remove` functions are where it gets a little tricker.
 Let's start with `add`. Here is the unannotated version:
 
-include_example(exercises/Dbl_Linked_List/add_orig.broken.c)
+include_example(exercises/dll/add_orig.broken.c)
 
-*Exercise*: Before reading on, see if you can figure out what specifications are needed.
+*Exercise*: Before reading on, see if you can figure out what
+specification is appropriate and what other are needed.
+// TODO: BCP: I rather doubt they are going to be able to come up with this specification on their own!  We need to set it up earlier with a simpler example (maybe in a whoile earlier section) showing how to use conditionals in specs.
 
 Now, here is the annotated version of the `add` operation:
 
-include_example(exercises/Dbl_Linked_List/add.c)
+include_example(exercises/dll/add.c)
 
-First, let's look at the pre and post conditions. The `requires` 
-clause is straightforward. We need to own the list centered around 
+First, let's look at the pre- and post-conditions. The `requires`
+clause is straightforward. We need to own the list centered around
 the node that `n` points to. `Before` is a `Dll`
-that is either empty, or it has a seq to the left,
-the current node that `n` points to, and a seq to the right.
+that is either empty, or it has a List to the left,
+the current node that `n` points to, and a List to the right.
 This corresponds to the state of the list when it is passed in.
 
-In the ensures clause, we again establish ownership of the list, but this time it is centered around the added node. This means that `After` is a `Dll` structure similar to `Before`, except that the node `curr` is 
-now the created node. The old `curr` is pushed into the
-left part of the new list. The ternary operator in the `ensures` clause is saying that if the list was empty
-coming in, it now is a singleton list. Otherwise, the left left part of the list now has the data from the old `curr` node, the new `curr` node is the added node,
-and the right part of the list is the same as before.
-
-Now, let's look at the annotations in the function body.
-CN can figure out the empty list case for itself, but it needs some help with the non-empty list case. The
-`split_case` on `is_null((\*n).prev)` tells CN to unpack the `Own_Backwards` predicate. Without this annotation,
-CN cannot reason that we didn't lose the left half of the list before we return, and will claim we are missing a resource for returning. The `split_case` on `is_null(n->next->next)` is similar, but for unpacking the `Own_Forwards` predicate. Note that we 
-have to go one more node forward to make sure that everything past `n->next` is still owned at the end of the function.
-
-
-Now let's look at the `remove` operation. Traditionally, a `remove` operation for a list returns the integer that was removed. However we also want all of our functions to return a pointer to the list. Because of this, we define a `+struct+` that includes an `int` and a `node`. 
-
-include_example(exercises/Dbl_Linked_List/node_and_int.h)
+In the ensures clause, we again establish ownership of the list, but
+this time it is centered around the added node. This means that
+`After` is a `Dll` structure similar to `Before`, except that the node
+`curr` is now the created node. The old `curr` is pushed into the left
+part of the new list. The conditional operator in the `ensures` clause
+is saying that if the list was empty coming in, it now is a singleton
+list. Otherwise, the left left part of the list now has the data from
+the old `curr` node, the new `curr` node is the added node, and the
+right part of the list is the same as before.
+
+Now, let's look at the annotations in the function body.  CN can
+figure out the empty list case for itself, but it needs some help with
+the non-empty list case. The `split_case` on `is_null(n->prev)`
+tells CN to unpack the `Own_Backwards` predicate. Without this
+annotation, CN cannot reason that we didn't lose the left half of the
+list before we return, and will claim we are missing a resource for
+returning. The `split_case` on `is_null(n->next->next)` is similar,
+but for unpacking the `Own_Forwards` predicate. Note that we have to
+go one more node forward to make sure that everything past `n->next`
+is still owned at the end of the function.
+
+Now let's look at the `remove` operation. Traditionally, a `remove`
+operation for a list returns the integer that was removed. However we
+also want all of our functions to return a pointer to the
+list. Because of this, we define a `+struct+` that includes an `int`
+and a `node`.
+
+include_example(exercises/dll/dllist_and_int.h)
 
 Now we can look at the code for the `remove` operation. Here is the un-annotated version:
 
-include_example(exercises/Dbl_Linked_List/remove_orig.broken.c)
+include_example(exercises/dll/remove_orig.broken.c)
 
-*Exercise*: Before reading on, see if you can figure out what specifications are needed.
+*Exercise*: Before reading on, see if you can figure out what
+specification is appropriate and what annotations are needed.
+// TODO: BCP: Again, unlikely the reader is going to be able to figure this out without help.  We need some hints.
 
 Now, here is the fully annotated version of the `remove` operation:
 
-include_example(exercises/Dbl_Linked_List/remove.c)
+include_example(exercises/dll/remove.c)
 
-First, let's look at the pre and post conditions. The `requires` clause says that we cannot remove a node from an empty list, so the pointer passed in must not be null. Then we take ownership of the list, and we
+First, let's look at the pre- and post-conditions. The `requires` clause says that we cannot remove a node from an empty list, so the pointer passed in must not be null. Then we take ownership of the list, and we
 assign the node of that list to the identifier `del`
 to make our spec more readable. So `Before` refers to the `Dll` when the function is called, and `del` refers to the node that will be deleted.
 
@@ -1354,47 +1615,125 @@ of the `node_and_int` struct as well as the `Dll` that
 the node is part of. Here, `After` refers to the `Dll`
 when the function returns. We ensure that the int that is returned is the value of the deleted node, as intended. Then we have a complicated nested ternary conditional that ensures that `After` is the same as `Before` except for the deleted node. Let's break down this conditional:
 
-- The first guard asks if both `del.prev` and `del.next` are null. In this case, we are removing the only node in the list, so the resulting list will be empty. The `else` branch of this conditional contains it's own conditional.
-
-- For the following conditional, the guard checks if 'del.prev' is NOT null. Note that in the code, this means that the returned node is `del.next`, regardless of whether or not `del.prev` is null. If this is the case, `After` is now centered around `del.next`, and the left part of the list is the same as before. Since `del.next` was previously the head of the right side, the right side loses its head in `After`. This is where we get `After == Dll{left: Left(Before), curr: Node(After), right: tl(Right(Before))}`. 
-
-- The final `else` branch is the case where `del.next` is null, but `del.prev` is not null. In this case, the returned node is `del.prev`. This branch follows the same logic as the one before it, except now we are taking the head of the left side rather than the right side. Now the right side is unchanged, and the left side is just the tail, as seen shown in
-`After == Dll{left: tl(Left(Before)), curr: Node(After), right: Right(Before)};`
-
-Now, let's look at the annotations in the function body. These are similar to in the `add` function. Both of these `split_case` annotations are needed to unpack the `Own_Forwards` and `Own_Backwards` predicates. Without these annotations, CN will not be able to reason that we didn't lose the left or right half of the list before we return, and will claim we are missing a resource for returning.
+- The first guard asks if both `del.prev` and `del.next` are null. In this case, we are removing the only node in the list, so the resulting list will be empty. The `else` branch of this conditional contains its own conditional.
+
+- For the following conditional, the guard checks if 'del.prev' is
+  _not_ null. This means that the returned node is `del.next`,
+  regardless of whether or not `del.prev` is null. If this is the
+  case, `After` is now centered around `del.next`, and the left part
+  of the list is the same as before. Since `del.next` was previously
+  the head of the right side, the right side loses its head in
+  `After`. This is where we get `After == Dll{left:
+  Left_Sublist(Before), curr: Node(After), right: Tl(Right(Before))}`.
+
+- The final `else` branch is the case where `del.next` is null, but
+`del.prev` is not null. In this case, the returned node is
+`del.prev`. This branch follows the same logic as the one before it,
+except now we are taking the head of the left side rather than the
+right side. Now the right side is unchanged, and the left side is just
+the tail, as seen shown in `After == Dll{left:
+Tl(Left_Sublist(Before)), curr: Node(After), right: Right(Before)};`
+
+The annotations in the function body are similar to in the `add`
+function. Both of these `split_case` annotations are needed to unpack
+the `Own_Forwards` and `Own_Backwards` predicates. Without them, CN
+will not be able to reason that we didn't lose the left or right half
+of the list before we return and will claim we are missing a resource
+for returning.
 
 // ======================================================================
 
-*Exercise*: There are many other functions that one might want to implement for a doubly linked list. For example, one might want to implement a function that appends one list to another, or a function that reverses a list. Try implementing these functions and writing their specifications.
-
-=== The Runway
-
-Suppose we have been tasked with writing a program that simulates a runway at an airport. This airport is very small, so it only has one runway that is used for both takeoffs and landings. We want to verify that the runway is always safe by implementing the following specifications into CN:
-
-1. The runway has two modes: departure mode and arrival mode. The two modes can never be active at the same time, and neither mode is active at the beginning of the day.
-
-2. There is always a waitlist of planes that need to land at the airport and planes that need to leave the airport at a given moment. These can be modeled with counters `W_A` for the number of planes waiting to arrive, and `W_D` for the number of planes waiting to depart. 
+*Exercise*: There are many other functions that one might want to
+ implement for a doubly linked list. For example, one might want to
+ implement a function that appends one list to another, or a function
+ that reverses a list. Try implementing a few of these functions and
+ writing their specifications.
 
-3. At any time, a plane is either waiting to arrive, waiting to depart, or on the runway. Once a plane has started arriving or departing, the corresponding counter (`W_A` or `W_D`) is decremented. There is no need to keep track of planes once they have arrived or departed. Additionally,  once a plane is waiting to arrive or depart, it continues waiting until it has arrived or departed.
-
-
-4. Let’s say it takes 5 minutes for a plane to arrive or depart. During these 5 minutes, no other plane may use the runway. We can keep track of how long a plane has been on the runway with the `Runway_Counter`. If the `Runway_Counter` is at 0, then there is currently no plane using the runway, and it is clear for another plane to begin arriving or departing. Once the `Runway_Counter` reaches 5, we can reset it at the next clock tick. One clock tick represents 1 minute.
-
-5.  If there is at least one plane waiting to depart and no cars waiting to arrive, then the runway is set to departure mode (and vice versa for arrivals).
-
-6.  If both modes of the runway are inactive and planes become ready to depart and arrive simultaneously, the runway will activate arrival mode first. If the runway is in arrival mode and there are planes waiting to depart, no more than 3 planes may arrive from that time point. When either no more planes are waiting to arrive or 3 planes have arrived, the runway switches to departure mode. If the runway is on arrival mode and no planes are waiting to depart, then the runway may stay in arrival mode until a plane is ready to depart, from which time the 3-plane limit is imposed (and vice versa for departures). Put simply, if any planes are waiting for a mode that is inactive, that mode will become active no more than 15 minutes later (5 minutes for each of 3 planes).
-
-To encode all this in CN, we first need a way to describe the state of the runway at a given time. We can use a *struct* that includes the following fields:
-
-- `ModeA` and `ModeD` to represent the arrival and departure modes, respectively. We can define constants for `ACTIVE` and `INACTIVE`, as described in the `Constants` section above.
-- `W_A` and `W_D` to represent the number of planes waiting to arrive and depart, respectively.
-- `Runway_Time` to represent the time (in minutes) that a plane has spent on the runway while arriving or departing.
-- `Plane_Counter` to represent the number of planes that have arrived or departed while planes are waiting for the other mode. This will help us keep track of the 3-plane limit as described in *(6)*.
+*Exercise*: For extra practice, try coming up with one or two
+variations on the Dll data structure itself (there are many!).
 
+// ======================================================================
+// ======================================================================
+// ======================================================================
+=== Case Study: Airport Simulation
+
+// TODO: BCP: I'm nervous about this case study -- it is not nearly as well debugged as the others, and it seems potentially quite confusing.  I propose deleting it, but if other like it we can try to whip it into better shape...
+
+Suppose we have been tasked with writing a program that simulates a
+runway at an airport. This airport is very small, so it only has one
+runway, which is used for both takeoffs and landings. We want to
+verify that the runway is always used safely, by checking the
+following informal specification:
+
+1. The runway has two modes: departure mode and arrival mode. The two
+   modes can never be active at the same time.  Neither mode is active
+   at the beginning of the day.
+// TODO: BCP: Would it be simpler to say it is in arrival mode at the beginning of the day?  What difference would that make?  (Saying there are two modes and then immediately introducing a third one is a bit confusing.)
+
+2. At any given moment, there is a waiting list of planes that need to
+   land at the airport and planes that need to leave the
+   airport. These are modeled with counters `W_A` for the number of
+   planes waiting to arrive, and `W_D` for the number of planes
+   waiting to depart.
+
+3. At any moment, a plane is either waiting to arrive, waiting to
+   depart, or on the runway. Once a plane has started arriving or
+   departing, the corresponding counter (`W_A` or `W_D`) is
+   decremented. There is no need to keep track of planes once they
+   have arrived or departed. Additionally, once a plane is waiting to
+   arrive or depart, it continues waiting until it has arrived or
+   departed.
+
+4. It takes 5 minutes for a plane to arrive or depart. During these 5
+   minutes, no other plane may use the runway. We can keep track of
+   how long a plane has been on the runway with the
+   `Runway_Counter`. If the `Runway_Counter` is at 0, then there is
+   currently no plane using the runway, and it is clear for another
+   plane to begin arriving or departing. Once the `Runway_Counter`
+   reaches 5, we can reset it at the next clock tick. One clock tick
+   represents 1 minute.
+
+5. If there is at least one plane waiting to depart and no cars
+   waiting to arrive, then the runway is set to departure mode (and
+   vice versa for arrivals).
+
+6. If both modes of the runway are inactive and planes become ready to
+   depart and arrive simultaneously, the runway will activate arrival
+   mode first. If the runway is in arrival mode and there are planes
+   waiting to depart, no more than 3 planes may arrive from that time
+   point. When either no more planes are waiting to arrive or 3 planes
+   have arrived, the runway switches to departure mode. If the runway
+   is on arrival mode and no planes are waiting to depart, then the
+   runway may stay in arrival mode until a plane is ready to depart,
+   from which time the 3-plane limit is imposed (and vice versa for
+   departures). Put simply, if any planes are waiting for a mode that
+   is inactive, that mode will become active no more than 15 minutes
+   later (5 minutes for each of 3 planes).
+
+To encode all this in CN, we first need a way to describe the state of
+the runway at a given time. We can use a *struct* that includes the
+following fields:
+
+- `ModeA` and `ModeD` to represent the arrival and departure modes,
+  respectively. We can define constants for `ACTIVE` and `INACTIVE`,
+  as described in the `Constants` section above.
+
+- `W_A` and `W_D` to represent the number of planes waiting to arrive
+  and depart, respectively.
+
+- `Runway_Time` to represent the time (in minutes) that a plane has
+  spent on the runway while arriving or departing.
+
+- `Plane_Counter` to represent the number of planes that have arrived
+  or departed while planes are waiting for the other mode. This will
+  help us keep track of the 3-plane limit as described in *(6)*.
 
 include_example(exercises/runway/state.h)
 
-Next, we need to specify what makes a state valid. We must define a rigorous specification in order to ensure that the runway is always safe and working as intended. Try thinking about what this might look like before looking at the code below.
+Next, we need to specify what makes a state valid. We must define a
+rigorous specification in order to ensure that the runway is always
+safe and working as intended. Try thinking about what this might look
+like before looking at the code below.
 
 include_example(exercises/runway/valid_state.h)
 
@@ -1422,11 +1761,18 @@ First, let's look at an initialization function and functions to update `Plane_C
 
 include_example(exercises/runway/funcs1.h)
 
-*Exercise*: Now try adding your own specifications to the following functions. Make sure that you specify a valid state as a pre and post condition for every function. If you get stuck, the solution is in the solutions folder.
+*Exercise*: Now try adding your own specifications to the following
+functions. Make sure that you specify a valid state as a pre- and
+post-condition for every function. If you get stuck, the solution is
+in the solutions folder.
 
 include_example(exercises/runway/funcs2.c)
 
-*Exercise*: For extra practice, try coming up with different specifications or variations for this exercise and implementing them yourself!
+// ======================================================================
+
+== Acknowledgment of Support and Disclaimer
+
+This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044, a European Research Council (ERC) Advanced Grant “ELVER” under the European Union’s Horizon 2020 research and innovation programme (grant agreement no. 789108), and additional funding from Google.  The opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the Air Force Research Laboratory (AFRL).
 
 // ======================================================================
 
@@ -1447,9 +1793,9 @@ Further topics:
     https://www.geeksforgeeks.org/data-structures/#most-popular-data-structures
   - Maybe add some explanation of -- or at least a pointer to --
     Dhruv's Iris-in-C examples:
-       queue_pop_lemma_stages.c
-       queue_push_induction.c
-       queue_pop_unified.c
+       pop_queue_lemma_stages.c
+       push_queue_induction.c
+       pop_queue_unified.c
 
 Further exercises:
   - Some exercises that get THEM to write predicates, datatype
@@ -1460,15 +1806,15 @@ Misc things to do:
 
   - naming issues
         - rename == to ptr_eq everywhere in specs
-        - rename list to seq in filenames.  or go more radical and rename seq to cnlist
-        - consider renaming IntList to just List (and int_list to just list,
+        - rename list to List in filenames.  or go more radical and rename List to cnlist
+        - consider renaming SLList_At to just List (and sllist to just list,
           etc.) everywhere (since we are only dealing with one kind of list
           in the tutorial, the extra pedantry is not getting us much; and
           this simplification would avoid trying to fix conventions that all
           CN code should use everywhere...)
-       - related: the name Seq_Cons is awkward for several reasons:
+       - related: the name Cons is awkward for several reasons:
            - long / verbose (nothing to do about that, I guess)
-           - Seq is capitalized, but it means seq
+           - Seq is capitalized, but it means List
            - most important part is buried in the middle
            - What are the established C conventions here??
 
@@ -1481,9 +1827,9 @@ Misc things to do:
     defining an "exit" function" with trivial pre- and postconditions
     (true / false).
 
-  - In queue.c, when I tried /*@ unfold IntQueueAux (F.front, F.back,
+  - In queue.c, when I tried /*@ unfold QueueAux (F.front, F.back,
     B.first); @*/ I was confused by "the specification function
-    `IntQueueAux' is not declared".  I guess this is, again, the
+    `QueueAux' is not declared".  I guess this is, again, the
     distinction between functions and predicates...?
 
   - In debugging the queue example, The fact that some of the
diff --git a/src/underconstruction/bst/README.md b/src/underconstruction/bst/README.md
new file mode 100644
index 00000000..3a203df5
--- /dev/null
+++ b/src/underconstruction/bst/README.md
@@ -0,0 +1,6 @@
+This example still needs some work, for an amusing reason: It gives a
+wrong version of the BST invariant, then specifies each function
+slightly incorrectly in an analogous way! 
+
+It would be good to fix the specs and then make an extended exercise
+out of it for the tutorial.
diff --git a/src/underconstruction/bst/c_types.h b/src/underconstruction/bst/c_types.h
new file mode 100644
index 00000000..196270b3
--- /dev/null
+++ b/src/underconstruction/bst/c_types.h
@@ -0,0 +1,21 @@
+// Defines structure of Binary Tree Nodes
+// Defines the specs for allocating and freeing the Nodes
+
+struct node {
+    int data;
+    struct node* left;
+    struct node* right;
+};
+
+extern struct node* malloc_node();
+/*@ spec malloc_node();
+    requires true;
+    ensures take R = Block<struct node>(return);
+            !ptr_eq(return, NULL);
+@*/ 
+
+extern void freenode (struct node *t);
+/*@ spec freenode(pointer t);
+    requires take R = Block<struct node>(t);
+    ensures true;
+@*/
diff --git a/src/underconstruction/bst/cn_getters.h b/src/underconstruction/bst/cn_getters.h
new file mode 100644
index 00000000..d0a84d31
--- /dev/null
+++ b/src/underconstruction/bst/cn_getters.h
@@ -0,0 +1,48 @@
+// Defines basic CN functions to extract a member of the Tree datatype
+
+/*@
+function (i32) Data_Of (datatype Tree sapling) 
+{
+  match sapling 
+  {
+    Leaf {} => 
+    {
+      default<i32>
+    }
+    Node {Left : _, Data : dat, Right: _} => 
+    {
+      dat
+    }
+  }
+}
+
+function (datatype Tree) get_lb (datatype Tree sapling) 
+{
+  match sapling 
+  {
+    Leaf {} => 
+    {
+      Leaf {}
+    }
+    Node {Left : left, Data : _ , Right: _} => 
+    {
+      left
+    }
+  }
+}
+
+function (datatype Tree) get_rb (datatype Tree sapling) 
+{
+  match sapling 
+  {
+    Leaf {} => 
+    {
+      Leaf {}
+    }
+    Node {Left : _, Data : _ , Right: right} => 
+    {
+      right
+    }
+  }
+}
+@*/
diff --git a/src/underconstruction/bst/cn_types.h b/src/underconstruction/bst/cn_types.h
new file mode 100644
index 00000000..024b73de
--- /dev/null
+++ b/src/underconstruction/bst/cn_types.h
@@ -0,0 +1,26 @@
+// FILL IN: This is where we define the Tree datatype and the
+// associated Tree_At predicate
+
+/*@
+datatype Tree {
+    Leaf {},
+    Node {datatype Tree Left, i32 Data, datatype Tree Right}
+} 
+
+predicate (datatype Tree) Tree_At (pointer t) 
+{
+    if (is_null(t))
+    {
+        return Leaf{};
+    }
+    else
+    {
+        take T = Owned<struct node>(t);
+        take L = Tree_At(T.left);
+        assert (L == Leaf{} || Data_Of(L) < T.data);
+        take R = Tree_At(T.right);
+        assert (R == Leaf{} || Data_Of(R) >= T.data);
+        return (Node {Left: L, Data: T.data, Right: R});
+    }
+}
+@*/
diff --git a/src/underconstruction/bst/constructors.h b/src/underconstruction/bst/constructors.h
new file mode 100644
index 00000000..cfc368a6
--- /dev/null
+++ b/src/underconstruction/bst/constructors.h
@@ -0,0 +1,53 @@
+// Constructors for trees
+
+struct node* node_nil()
+/*@ ensures take Ret = Tree_At(return);
+            Ret == Leaf{};
+ @*/
+{
+  return 0;
+}
+
+struct node* node_cons_left(int val, struct node* left_b)
+/*@ requires take L = Tree_At(left_b);
+             (L == Leaf{} || Data_Of(L) < val);
+    ensures take Ret = Tree_At(return);
+            Ret == Node{Left: L, Data: val, Right: Leaf{}};
+ @*/
+{
+  struct node *t = malloc_node();
+  t->data = val;
+  t->left = left_b;
+  t->right = 0;
+  return t;
+}
+
+struct node* node_cons_right(int val, struct node* right_b)
+/*@ requires take R = Tree_At(right_b);
+             (R == Leaf{} || Data_Of(R) >= val);
+    ensures take Ret = Tree_At(return);
+            Ret == Node{Left: Leaf{}, Data: val, Right: R};
+ @*/
+{
+  struct node *t = malloc_node();
+  t->data = val;
+  t->left = 0;
+  t->right = right_b;
+  return t;
+}
+
+struct node* node_cons_both(int val, struct node* left_b, struct node* right_b)
+/*@ requires take L = Tree_At(left_b);
+             take R = Tree_At(right_b);
+             (L == Leaf{} || Data_Of(L) < val);
+             (R == Leaf{} || Data_Of(R) >= val);
+    ensures take Ret = Tree_At(return);
+            Ret == Node{Left: L, Data: val, Right: R};
+@*/
+{
+  struct node *t = malloc_node();
+  t->data = val;
+  t->left = left_b;
+  t->right = right_b;
+  return t;
+}
diff --git a/src/underconstruction/bst/contains.c b/src/underconstruction/bst/contains.c
new file mode 100644
index 00000000..aee1293e
--- /dev/null
+++ b/src/underconstruction/bst/contains.c
@@ -0,0 +1,65 @@
+#include "./headers.h"
+// returns true (1u32) or false (u32), if value is an node in the binary Tree
+
+/* FILL IN CN FUNCTION SPEC DEFINTION HERE */
+/* --BEGIN-- */
+/*@
+function [rec] (u32) exists(datatype Tree sapling, i32 value)
+{
+    match sapling 
+    {
+        Leaf {} => 
+        {
+            0u32
+        }
+        Node {Left: l, Data: dat, Right: r} =>
+        {   
+            let lb_exist = exists(l, value);
+            let rb_exist = exists(r, value);  
+            ((value == dat)
+                ? 1u32
+                : ((value < dat) ? lb_exist  : rb_exist))
+        }
+    }
+}
+@*/
+/* --END-- */
+
+typedef enum { false, true } bool;
+
+bool node_containsValue (struct node* t, int value)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take t1 = Tree_At(t);
+    ensures  take t2 = Tree_At(t);
+                  t1 == t2;
+            return == exists(t1, value);
+@*/
+/* --END-- */
+{   
+    /* --BEGIN-- */
+    /*@ unfold exists(t1, value); @*/
+    /* --END-- */
+    if (t == 0)
+    {
+        return false;
+    }
+    else
+      {
+        if (t->data == value)
+        {
+            return true;
+        }
+        else
+        {
+            if (value < t->data)
+            {      
+                return node_containsValue(t->left, value);
+            }
+            else
+            {
+                return node_containsValue(t->right, value);
+            }
+        }
+    }
+}
diff --git a/src/underconstruction/bst/copy.c b/src/underconstruction/bst/copy.c
new file mode 100644
index 00000000..4b80c7a0
--- /dev/null
+++ b/src/underconstruction/bst/copy.c
@@ -0,0 +1,26 @@
+#include "./headers.h"
+#include "./constructors.h"
+// takes in binary tree, Returns copy of it
+
+struct node* node_copy (struct node* t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take T1 = Tree_At(t);
+    ensures  take T1_ = Tree_At(t);
+             take T2  = Tree_At(return);
+                  T1 == T1_;
+                  T1 == T2;
+@*/
+/* --END-- */
+{
+    if (t == 0)
+    {
+        return node_nil();
+    }
+    else
+    {
+        struct node* new_left = node_copy(t->left);
+        struct node* new_right = node_copy(t->right);
+        return node_cons_both(t->data, new_left, new_right);
+    }
+}
\ No newline at end of file
diff --git a/src/underconstruction/bst/create_node.c b/src/underconstruction/bst/create_node.c
new file mode 100644
index 00000000..075ba82e
--- /dev/null
+++ b/src/underconstruction/bst/create_node.c
@@ -0,0 +1,19 @@
+#include "./headers.h"
+// Initializes new node with value given as its argument
+
+struct node* node_create_node(int value)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ ensures take T = Tree_At(return);
+        T == Node {Left: Leaf{}, Data: value, Right: Leaf{}};
+        !is_null(return);
+        Data_Of(T) == value;
+@*/
+/* --END-- */
+{
+    struct node* node = malloc_node();
+    node->data = value;
+    node->left = 0;
+    node->right = 0;
+    return node;
+}
\ No newline at end of file
diff --git a/src/underconstruction/bst/depth.c b/src/underconstruction/bst/depth.c
new file mode 100644
index 00000000..2798cc0f
--- /dev/null
+++ b/src/underconstruction/bst/depth.c
@@ -0,0 +1,49 @@
+#include "./headers.h"
+// counts the furthest distance from the root to the leaf node
+
+/* FILL IN CN FUNCTION SPEC DEFINTION HERE */
+/* --BEGIN-- */
+/*@
+function [rec] (u32) depth (datatype Tree sapling)
+{
+    match sapling 
+    {
+        Leaf {} => 
+        {
+            0u32
+        }
+        Node {Left: l, Data: dat, Right: r} => 
+        {
+            let left_b = depth(l);
+            let right_b = depth(r);
+            ((left_b > right_b) ? (1u32 + left_b) : (1u32 + right_b))
+        }
+    }
+}
+@*/
+/* --END-- */
+
+unsigned int node_depth(struct node* t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take t1 = Tree_At(t);
+    ensures take t2 = Tree_At(t);
+                 t1 == t2;
+             return == depth(t1);
+@*/
+/* --END-- */
+{
+    /* --BEGIN-- */
+    /*@ unfold depth(t1); @*/
+    /* --END-- */
+    if (t == 0)
+    {
+        return 0;
+    }
+    else
+    {
+        unsigned int left_b = node_depth(t->left);
+        unsigned int right_b = node_depth(t->right);
+        return ((left_b > right_b) ? (1 + left_b) : (1 + right_b));
+    }   
+}
diff --git a/src/underconstruction/bst/free.c b/src/underconstruction/bst/free.c
new file mode 100644
index 00000000..84f3204c
--- /dev/null
+++ b/src/underconstruction/bst/free.c
@@ -0,0 +1,20 @@
+#include "./headers.h"
+// deallocates all the nodes in the binary tree
+
+void node_free_tree (struct node* t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@  requires take v1 = Tree_At(t); @*/
+/* --END-- */
+{
+    if (t == 0)
+    {
+        return;
+    } 
+    else
+    {
+        node_free_tree(t->right);
+        node_free_tree(t->left);
+        freenode(t);
+    }
+}
\ No newline at end of file
diff --git a/src/underconstruction/bst/getter.c b/src/underconstruction/bst/getter.c
new file mode 100644
index 00000000..f3983af8
--- /dev/null
+++ b/src/underconstruction/bst/getter.c
@@ -0,0 +1,63 @@
+#include "./headers.h"
+// Extracts the members of a given Tree node
+
+int get_Tree_Data (struct node *t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take v1 = Tree_At(t);
+    ensures  take v2 = Tree_At(t);
+                  v1 == v2;
+            return == (is_null(t) ? 0i32 : Data_Of(v2)); @*/
+/* --END-- */
+{
+    if (t)
+    {
+        return t->data;
+    }
+    else
+    {
+        return 0;
+    }
+}
+
+struct node* get_Tree_Left (struct node *t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take v1 = Owned<struct node>(t);
+             take v1_left = Owned<struct node>(v1.left);
+    ensures  take v2 = Owned<struct node>(t);
+             take v2_left = Owned<struct node>(v2.left);
+             v1 == v2 && v1_left == v2_left;
+    ptr_eq(return, ((is_null(t)) ? (t) : (v1.left))); @*/
+/* --END-- */
+{
+    if (t)
+    {
+        return t->left;
+    }
+    else
+    {
+        return 0;
+    }
+}
+
+struct node* get_Tree_Right (struct node *t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take v1 = Owned<struct node>(t);
+             take v1_right = Owned<struct node>(v1.right);
+    ensures  take v2 = Owned<struct node>(t);
+             take v2_right = Owned<struct node>(v2.right);
+             v1 == v2 && v1_right == v2_right;
+    ptr_eq(return, ((is_null(t)) ? (t) : (v1.right))); @*/
+/* --END-- */
+{
+    if (t)
+    {
+        return t->right;
+    }
+    else
+    {
+        return 0;
+    }
+}
\ No newline at end of file
diff --git a/src/underconstruction/bst/headers.h b/src/underconstruction/bst/headers.h
new file mode 100644
index 00000000..8538a522
--- /dev/null
+++ b/src/underconstruction/bst/headers.h
@@ -0,0 +1,10 @@
+// Header file for basic node definitions and functionality
+
+#ifndef _TREE_H
+#define _TREE_H
+
+#include "./c_types.h"
+#include "./cn_types.h"
+#include "./cn_getters.h"
+
+#endif //_TREE_H
diff --git a/src/underconstruction/bst/insert.c b/src/underconstruction/bst/insert.c
new file mode 100644
index 00000000..8b67415c
--- /dev/null
+++ b/src/underconstruction/bst/insert.c
@@ -0,0 +1,61 @@
+#include "./headers.h"
+#include "create_node.c"
+// inserts a new node into binary tree
+
+/* FILL IN CN FUNCTION SPEC HERE */
+/* --BEGIN-- */
+/*@ 
+function [rec] (datatype Tree) insert (datatype Tree sapling, i32 value)
+{
+    match sapling 
+    {
+        Leaf{} => 
+        {
+            Node{Left: Leaf{}, Data: value, Right: Leaf{}}
+        }
+        Node{Left: l, Data: dat, Right: r} => 
+        {
+
+            ((value < dat) ? Node {Left: insert(l, value), Data: dat, Right: r} :
+            Node {Left: l, Data: dat, Right: insert(r, value)})
+        }
+    }
+}
+@*/
+/* --END-- */
+
+struct node* node_insert(struct node* t, int value)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take T1 = Tree_At(t);
+    ensures take Ret = Tree_At(return);  
+                 Ret == insert(T1,value);
+                 T1 != Leaf{} implies Data_Of(Ret) == Data_Of(T1);
+                !is_null(return);  
+@*/
+/* --END-- */
+{
+    /* --BEGIN-- */
+    /*@ unfold insert(Leaf{}, value); @*/
+    /*@ unfold insert(T1, value); @*/
+    /* --END-- */
+    if (t == 0)
+    {
+        struct node* add = node_create_node(value);
+        return add;
+    }
+    else
+    {
+        if (value < t->data)
+        {
+            t->left = node_insert(t->left, value);
+            return t;
+            
+        }   
+        else
+        {
+            t->right = node_insert(t->right, value);
+            return t;
+        }
+    }
+}
diff --git a/src/underconstruction/bst/length.c b/src/underconstruction/bst/length.c
new file mode 100644
index 00000000..9b90b129
--- /dev/null
+++ b/src/underconstruction/bst/length.c
@@ -0,0 +1,49 @@
+#include "./headers.h"
+// Function which counts all the nodes in the tree
+
+/* FILL IN CN FUNCTION SPEC DEFINTION HERE */
+/* --BEGIN-- */
+/*@
+function [rec] (u32) length (datatype Tree sapling)
+{
+    match sapling 
+    {
+        Leaf {} => 
+        {
+            0u32
+        }
+        Node {Left: l, Data: dat, Right: r} => 
+        {
+            let left_b = length(l);
+            let right_b = length(r);
+            (1u32 + left_b + right_b)
+        }
+    }
+}
+@*/
+/* --END-- */
+
+unsigned int node_length(struct node* t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take t1 = Tree_At(t);
+    ensures take t2 = Tree_At(t);
+                 t1 == t2;
+             return == length(t1);
+@*/
+/* --END-- */
+{
+    /* --BEGIN-- */
+    /*@ unfold length(t1); @*/
+    /* --END-- */
+    if (t == 0)
+    {
+        return 0;
+    }
+    else
+    {
+        unsigned int left_b = node_length(t->left);
+        unsigned int right_b = node_length(t->right);
+        return (1 + left_b + right_b);
+    }   
+}
\ No newline at end of file
diff --git a/src/underconstruction/bst/search.c b/src/underconstruction/bst/search.c
new file mode 100644
index 00000000..1e8653ac
--- /dev/null
+++ b/src/underconstruction/bst/search.c
@@ -0,0 +1,63 @@
+#include "./headers.h"
+// Searches for a node with the given value in the binary Tree
+
+/* FILL IN CN FUNCTION SPEC DEFINTION HERE */
+/* --BEGIN-- */
+/*@
+function [rec] (datatype Tree) search(datatype Tree sapling, i32 value)
+{
+    match sapling 
+    {
+        Leaf {} => 
+        {
+            Leaf{}
+        }
+        Node {Left: l, Data: dat, Right: r} =>
+        {
+            ((value == dat) ? sapling :
+            ((value < dat) ? search(l, value) : search(r, value)))
+        }
+    }
+}
+@*/
+/* --END-- */
+
+struct node* node_search(struct node* t, int value)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take t1 = Tree_At(t);
+    ensures  take t2 = Tree_At(t);
+                  t1 == t2;
+                  let Ret = search(t1, value);
+                  (Ret == Leaf{} ? is_null(return) : Data_Of(Ret) == value);                
+@*/
+/* --END-- */
+{   
+    /* --BEGIN-- */
+    /*@ unfold search(t1, value); @*/
+    /* --END-- */
+    if (t == 0)
+    {
+        
+        return 0;
+    }
+    else
+    {
+        
+        if (t->data == value)
+        {
+            return t;
+        }
+        else
+        {
+            if (value < t->data)
+            {   
+                return node_search(t->left, value);
+            }
+            else
+            {
+                return node_search(t->right, value);
+            }
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/underconstruction/bst/sum.c b/src/underconstruction/bst/sum.c
new file mode 100644
index 00000000..70fb6393
--- /dev/null
+++ b/src/underconstruction/bst/sum.c
@@ -0,0 +1,51 @@
+#include "./headers.h"
+// Sums up the data values of the nodes of the binary tree
+
+/* FILL IN CN FUNCTION SPEC DEFINTION HERE */
+/* --BEGIN-- */
+/*@
+function [rec] (u32) sum(datatype Tree sapling)
+{
+    match sapling 
+    {
+        Leaf {} => 
+        {
+            0u32
+        }
+        Node {Left: l, Data: dat, Right: r} => 
+        {
+            let rt_val = (u32) dat;
+            let sum_lb = sum(l);
+            let sum_rb = sum(r);
+            (rt_val + sum_lb + sum_rb)
+        }
+    }
+}
+@*/
+/* --END-- */
+
+unsigned int node_sum(struct node* t)
+/* FILL IN HERE */
+/* --BEGIN-- */
+/*@ requires take t1 = Tree_At(t);
+    ensures  take t2 = Tree_At(t);
+                 t1 == t2;
+             return == sum(t1);
+@*/
+/* --END-- */
+{   
+    /* --BEGIN-- */
+    /*@ unfold sum(t1); @*/
+    /* --END-- */
+    if (t == 0)
+    {
+        return 0;
+    }
+    else
+    {
+        unsigned int sum_lb = node_sum(t->left);
+        unsigned int sum_rb = node_sum(t->right);
+        unsigned int root_val = t->data;
+        return (root_val + sum_lb + sum_rb);
+    }   
+}
\ No newline at end of file