projects
/
matthijs
/
master-project
/
report.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
23487a1
)
Slightly improve the determinism proof section.
author
Matthijs Kooijman
<matthijs@stdin.nl>
Wed, 9 Dec 2009 09:26:56 +0000
(10:26 +0100)
committer
Matthijs Kooijman
<matthijs@stdin.nl>
Wed, 9 Dec 2009 09:26:56 +0000
(10:26 +0100)
Chapters/Normalization.tex
patch
|
blob
|
history
diff --git
a/Chapters/Normalization.tex
b/Chapters/Normalization.tex
index 5252c0fe71bca473d5ff2deb71482a7bbeed2d2a..8058a1596c8683fb7da8ea5af9501ca78d555a3d 100644
(file)
--- 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
{\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
For a transformation system holding the Church-Rosser property, it
is easy to show that it is in fact deterministic. Showing that this