Fix 525--538.

1 files changed, 8 insertions, 6 deletions

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index becab5e..f2ace28 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -210,20 +210,22 @@ We also add \(\mathsf{match}\) on lists. We need this to determine
 whether a path is addressing the root entry or one of its inductive
 components.
 
-We now return to our examples. After some beta reduction we recover
-the following value for \systemtinline{balanced}:
+We now return to our examples. After simplifying using the equational
+theory we recover
+the below value for \systemtinline{balanced}. In each branch we
+increase the recursive depth by one and create a new heap.
 \begin{listing}[H]
 \begin{systemt}
 let balanced n f = primrec n with
-  Zero => (Suc (max (fun (d, h) => d) []), fun xs =>
+  Zero => (Suc Zero, fun xs =>
     match xs with
       []      => Leaf f
     | x :: xs => snd (index [] x) xs)
 | Suc (depth, heap) =>
-    (Suc (max (fun (d, h) => d) [(depth, heap), (depth, hep)]), fun xs =>
+    (Suc depth, fun xs =>
       match xs with
-        []      => Branch (0, 1)
-      | x :: xs => snd (index [(depth, heap), (depth, heap)] x) xs)
+        []      => Branch (0, 0)
+      | x :: xs => snd (index [(depth, heap)] x) xs)
 \end{systemt}
 \vspace{-\baselineskip}
 \end{listing}