X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=d564d231405a00ab7f31622ef525b15f987c2218;hp=b058b63a2a3debae92f4fe435fe1f31799555c40;hb=d92aa4307ca45f07c6ae50056e08ffc874839756;hpb=8638abef4686335ede35793b43f3e25930822544

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index b058b63..d564d23 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -1590,7 +1590,7 @@
 
       \subsubsection[sec:transformation:caseremoval]{Case removal}
         This transform removes any case expression with a single alternative and
-        only wild binders.\refdef{wild binder}
+        only wild binders.\refdef{wild binders}
 
         These "useless" case expressions are usually leftovers from case simplification
         on extractor case (see the previous example).
@@ -2240,11 +2240,13 @@
     developed in the final part of the research, leaving no more time
     for verifying these properties. In fact, it is likely that the
     current transformation system still violates some of these
-    properties in some cases and should be improved (or extra conditions
-    on the input hardware descriptions should be formulated).
+    properties in some cases (see
+    \in{section}[sec:normalization:non-determinism] and
+    \in{section}[sec:normalization:stateproblems]) and should be improved (or
+    extra conditions on the input hardware descriptions should be formulated).
 
     This is most likely the case with the completeness and determinism
-    properties, perhaps als the termination property. The soundness
+    properties, perhaps also the termination property. The soundness
     property probably holds, since it is easier to manually verify (each
     transformation can be reviewed separately).
 
@@ -2441,7 +2443,7 @@
       each node in the normal set is also in the intended normal set.
       Reasoning about our intended normal set is easier, since we know
       how to generate it from its definition. \refdef{intended normal
-      form definition}.
+      form definition}
 
       Fortunately, we can also prove the complement (which is
       equivalent, since $A \subseteq B \Leftrightarrow \overline{B}