From e1b285483a778cfa0d1336d60c618af3c62e0c56 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:30:16 +0100
Subject: Fix 508--513.

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

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index cd59b67..fd71af8 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -153,8 +153,8 @@ write the fold operation, so we cannot use eliminator encodings. Thus
 the only suitable encoding strategy is a heap encoding.
 
 Unlike the description of the heap encoding in
-\cref{M-subsec:heap-encoding} we do not use the same type for indices
-and pointers. We use \(\mathsf{List}~\nat\) as the index type,
+\cref{M-subsec:encoding-strategies} we do not use the same type for
+indices and pointers. We use \(\mathsf{List}~\nat\) as the index type,
 representing a path through the term. We use the empty list to
 indicate the root of the inductive value. Otherwise, the head of the
 list selects which child to recurse into and its tail is the path
@@ -181,16 +181,23 @@ the \roll*{} operation as we do not need to fixup the entire heap.
 
 More formally, we encode the type \(\mu X. A\) as \(\nat \times
 (\mathsf{List}~\nat \to \sub{A}{X/\nat})\). We present the encoding of
-\roll*{} and \foldkw{} in \cref{fig:phase-2-encode}. We add three new
+\roll*{} and \foldkw{} in \cref{fig:phase-2-encode}. We add two new
 operators for working with lists:
 \begin{description}
   \item[\(\mathsf{max}\)] for calculating the maximum from a list,
-    given a function converting values to naturals;
-  \item[\(\mathsf{snoc}\)] for appending a single item to the tail of
-    a list;
+    given a function converting values to naturals; and
   \item[\(\mathsf{match}\)] for pattern matching on a list as either
     \(\mathsf{nil}\) or \(\mathsf{cons}\)
 \end{description}
+These operators satisfy the following equations:
+\begin{align*}
+  \mathsf{max}~f~\mathsf{nil} &= 0 &
+  \domatch{\mathsf{nil}}{\mathsf{nil}. f; \mathsf{cons}~x~y. g} &= f \\
+  \mathsf{max}~f~(\mathsf{cons}~t~u) &= f~t \sqcup u &
+  \domatch{\mathsf{cons}~t~u}{\mathsf{nil}. f; \mathsf{cons}~x~y. g}
+    &= \sub{g}{x/t, y/u}
+\end{align*}
+
 Computing the maximum value from a list is necessary to correctly
 determine the recursive depth to use when folding over an inductive
 value. It is also the primary reason why infinite inductive types are
-- 
cgit v1.2.3