From: Matthijs Kooijman Date: Wed, 9 Dec 2009 09:26:56 +0000 (+0100) Subject: Slightly improve the determinism proof section. X-Git-Tag: final-thesis~10 X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=commitdiff_plain;h=51c4ee734de45dac80f73cab386164e1e8e4098e;hp=23487a1fa3e35868cd9d838eb3c59d02ed5ebdac Slightly improve the determinism proof section. --- 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