diff -r 580c7b84f900 -r 5b10d83b0834 ninems/ninems.tex
--- a/ninems/ninems.tex	Sat Jul 06 20:34:41 2019 +0100
+++ b/ninems/ninems.tex	Sat Jul 06 21:09:45 2019 +0100
@@ -518,7 +518,7 @@
 $r_{i-1}$, we chop off a character from $r_{i-1}$ to form $r_i$.
 This leaves a "hole" on $r_i$. In order to calculate a value for
 $r_{i-1}$, we need to locate where that hole is. We can find this location
-informtaion by comparing $r_{i-1}$ and $v_i$.
+informtation by comparing $r_{i-1}$ and $v_i$.
 For instance, if $r_{i-1}$ is of shape $r_a \cdot r_b$, and $v_i$
 is of shape $\textit{Left}(\textit{Seq}(v_a, v_b))$, we know immediately that 
 \[ (r_a \cdot r_b)\backslash c = (r_a\backslash c) \cdot r_b \,+\, r_b\backslash c\],
@@ -568,7 +568,7 @@
  in \[r_3 = ( \underline{(0+0+0 + 0 + 1 \cdot 1 \cdot 1) \cdot r^*} + (0+0+0  + 1 + 0)
   \cdot r^*) +((0+1+0  + 0 + 0) \cdot r^*+(0+0+0  + 1 + 0) \cdot r^* )
  \](underlined). Note that the leftmost location of term \[((0+0+0 + 0 + 1 \cdot 1 \cdot 1) \cdot r^* \]
- (which corresponds to the intial sub-match $abc$)
+ (which corresponds to the initial sub-match $abc$)
   allows $mkeps$ to choose  it as the first candidate that meets the requirement of being $nullable$
   because $mkeps$ is defined to always choose the left one when nullable.
   In the case of this example, $abc$ is preferred over $a$ or $ab$.
@@ -959,7 +959,7 @@
 as this basically comes down to proving actions like removing the additional $r$ in $r+r$  does not delete important POSIX information in a regular expression.
 The hardcore of this problem is to prove that
 bmkeps bders r = bmkeps bders simp r
-That is, if we do derivative on regular expression r and the simplified version for, they can still prove the same POSIX value if there is one . This is not as straghtforward as the previous proposition, as the two regular expression r and simp r  might become very different regular expressions after repeated application ofd simp and derivative.
+That is, if we do derivative on regular expression r and the simplified version for, they can still prove the same POSIX value if there is one . This is not as straightforward as the previous proposition, as the two regular expression r and simp r  might become very different regular expressions after repeated application ofd simp and derivative.
 The crucial point is to find the "gene" of a regular expression and how it is kept intact during simplification.
 To aid this, we are utilizing the helping function retrieve described by Sulzmann and Lu:
 \\definition of retrieve\\