Slightly improve the determinism proof section.
authorMatthijs Kooijman <matthijs@stdin.nl>
Wed, 9 Dec 2009 09:26:56 +0000 (10:26 +0100)
committerMatthijs Kooijman <matthijs@stdin.nl>
Wed, 9 Dec 2009 09:26:56 +0000 (10:26 +0100)
Chapters/Normalization.tex

index 5252c0f..8058a15 100644 (file)
       {\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}}
 
     Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In
-    other words, there is a set of transformations that can be applied
-    to transform \lam{A} to \lam{B}. \lam{=>} is used to mean
-    \emph{implies}.
+    other words, there is a set of transformations that can transform
+    \lam{A} to \lam{B}. \lam{=>} is used to mean \emph{implies}.
 
     For a transformation system holding the Church-Rosser property, it
     is easy to show that it is in fact deterministic. Showing that this