From 46b287960d05135616ef4a10906289fbb4a5692a Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 13:41:56 +0100
Subject: Fix 593--599.

---
 sec/encoding.ltx | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/sec/encoding.ltx b/sec/encoding.ltx
index 9ffe418..19f2a73 100644
--- a/sec/encoding.ltx
+++ b/sec/encoding.ltx
@@ -320,12 +320,7 @@ lookup the index in the old list.
 
 We encode \(\mathsf{max}~f~t\) by primitive recursion on the length of
 the list \(t\).
-\[\doprimrec{t.0}{\zero}{x}{(x.1 - f~x.0) + f~x.0}\]
-We compute the binary maximum by performing a truncated subtraction
-followed by an addition. These both have standard
-encodings~\cref{add+sub}. Note that we use the inductive hypothesis on
-the left of the subtraction so that a naive partial evaluator can
-reduce the maximum of a singleton list to a single value.
+\[\doprimrec{t.0}{\zero}{x}{f~x.0 \sqcup x.1}\]
 
 The final operator to encode is pattern matching. We achieve this by
 inspecting the length of the list to match.
-- 
cgit v1.2.3