1 files changed, 34 insertions, 0 deletions
diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index d68ff72..4afc43f 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -149,6 +149,40 @@ index of the given child.
   \end{itemize}
 }
 
+After some beta reduction we recover the following definition for \systemtinline{balanced}:
+\begin{listing}[H]
+\begin{systemt}
+let balanced n f = primrec n with
+  Zero              => (1, fun xs =>
+    match xs with
+      []      => Leaf f
+    | x :: xs => arb)
+| Suc (depth, heap) => (1 + max [depth, depth], fun xs =>
+    match xs with
+      []      => Branch (0, 1)
+    | x :: xs => match x with
+        0 => heap xs
+      | 1 => heap xs)
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
+And here is the updated definition of \systemtinline{compose}:
+\begin{listing}[H]
+\begin{systemt}
+let compose (depth, heap) =
+  let go = primrec depth with
+    Zero   => arb
+  | Suc ih => fun index =>
+    let x = map (heap index) (fun x => ih (snoc xs x)) in
+    match x with
+      Leaf f        => f
+    | Branch (f, g) => fun x => f (g x)
+  in go []
+\end{systemt}
+\vspace{-\baselineskip}
+\end{listing}
+
 \TODO{
   \begin{itemize}
     \item state that we encode lists using their eliminators