From 6190f3493820604de279fe31c8bccab631e08245 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Sun, 3 Jun 2018 22:31:29 +0200
Subject: Minor textual enhancements

---
 expr.tex | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/expr.tex b/expr.tex
index ddaf3a1..9e1ed34 100644
--- a/expr.tex
+++ b/expr.tex
@@ -127,7 +127,6 @@ Since the program is reversed for use in \textsf{pn\_eval}, we can rewrite the p
 Suppose the original expression was \textsf{e = eadd e1 e2},
 	we now consider \textsf{pn\_eval v env ((rev (rpn v e1) ++ rev (rpn v e2)) ++ rest)}
 	in the evaluation of \textsf{rpnadd}.
-
 Due to associativity of \textsf{++}, we can reanalyse this as
 	\textsf{pn\_eval v env (rev (rpn v e1) ++ (rev (rpn v e2) ++ rest))},
 	which allows for application of the induction hypothesis with \textsf{rev (rpn v e2) ++ rest} as the \enquote{rest of the program}, i.e., the \textsf{rest}.
@@ -146,13 +145,13 @@ The proof of the lemma now follows by applying the assertion of the induction st
 
 \coq{83}{85}
 
-We now return to the proof of the correctness theorem, repeated here:
+We now return to the proof of the correctness theorem:
 
-\coq{87}{88}
+\coq{87}{89}
 
 We outsource this proof to our proof on \textsf{pn\_eval} using \textsf{rest = result = []}.
 
-\coq{89}{93}
+\coq{90}{93}
 
 The result of the call to \textsf{pn\_eval} from \textsf{rpn\_eval} is now known,
 	and we can simplify the \textsf{rpn\_eval} call further to the point of reflexivity.
-- 
cgit v1.2.3