From ebdbf9eb5db4bdad3a07b58163efa1fa00dfbc39 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:34:44 +0100
Subject: Fix 525--538.

---
 sec/encoding.ltx | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'sec/encoding.ltx')

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}
-- 
cgit v1.2.3

