diff --git a/frap_book.tex b/frap_book.tex index 279c6f1..11b4861 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -3154,7 +3154,7 @@ More precisely, the limit on how many times we can run garbage collection in a r The type-safety proof is fairly straightforward to update. We prove progress by \emph{ignoring} the garbage-collection rule, since the existing rules were already enough to find a step for every nonvalue. -A bit more work is needed to update the proof of preservation; its case for the existing rules follows the same way as before, while we must prove a few lemmas on the way to handling the new rule. +A bit more work is needed to update the proof of preservation; its cases for the existing rules follow the same way as before, while we must prove a few lemmas on the way to handling the new rule. \begin{lemma}[Transitivity for reachability] If $\freeloc{e_1} \subseteq \freeloc{e_2}$, then $\reach{h}{e_1} \subseteq \reach{h}{e_2}$.