From ed64e05e38bf42705e132b99af21730765860e62 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Mon, 4 Mar 2019 11:26:06 -0500
Subject: [PATCH] Closes #27

---
 frap_book.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/frap_book.tex b/frap_book.tex
index e89e48c..5412798 100644
--- a/frap_book.tex
+++ b/frap_book.tex
@@ -810,7 +810,7 @@ In that sense, with this translation, we make progress toward efficient implemen
 \newcommand{\compile}[1]{{\left \lfloor #1 \right \rfloor}}
 
 Throughout this book, we will use notation $\compile{\ldots}$ for compilation, where the floor-based notation suggests \emph{moving downward} to a lower abstraction level.
-Here is the compiler that concerns us now, where we write $\concat{s_1}{s_2}$ for concatenation of two stacks $s_1$ and $s_2$.
+Here is the compiler that concerns us now, where we write $\concat{\overline{i_1}}{\overline{i_2}}$ for concatenation of two instruction sequences $\overline{i_1}$ and $\overline{i_2}$.
 \encoding
 \begin{eqnarray*}
   \compile{n} &=& \mathsf{PushConst}(n) \\
@@ -843,7 +843,7 @@ e \arrow{r}{\compile{\ldots}} \arrow{dr}{\denote{\ldots}} & \compile{e} \arrow{d
 As usual, we leave proof details for the associated Coq code, but the key insight of the proof is to strengthen the induction hypothesis via a lemma.
 
 \begin{lemma}
-  $\denote{\concat{\compile{e}}{\overline{i}}}(v, s) = \denote{\overline{i}}(v, \concat{\denote{e}v}{s})$.
+  $\denote{\concat{\compile{e}}{\overline{i}}}(v, s) = \denote{\overline{i}}(v, \push{\denote{e}v}{s})$.
 \end{lemma}
 
 We strengthen the statement by considering both an arbitrary initial stack $s$ and a sequence of extra instructions $\overline{i}$ to be run after $e$.