Fix 593--599.

1 files changed, 1 insertions, 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.