From 51c4ee734de45dac80f73cab386164e1e8e4098e Mon Sep 17 00:00:00 2001
From: Matthijs Kooijman
Date: Wed, 9 Dec 2009 10:26:56 +0100
Subject: [PATCH] Slightly improve the determinism proof section.
---
Chapters/Normalization.tex | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 5252c0f..8058a15 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -2568,9 +2568,8 @@
{\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
--
2.20.1