--- a/ninems/ninems.tex	Thu Jul 04 23:20:00 2019 +0100
+++ b/ninems/ninems.tex	Thu Jul 04 23:27:32 2019 +0100
@@ -740,9 +740,8 @@
 subsequent copies can be pruned from the regular expression.
 
 A psuedocode version of our algorithm is given below:\\
-
-simp r \defn r if r = ONE bs or CHAR bs c or STAR bs r
-simp SEQ bs r_1 r_2 \defn \\
+\[simp r \dn r if r = ONE bs or CHAR bs c or STAR bs r
+simp SEQ bs r_1 r_2 \dn \\
 case (simp(r_1), simp(r_2) ) of (0, _) => 0
 (_,0) => 0
 (1, r) => fuse bs r
@@ -752,6 +751,7 @@
 case Nil => ZERO
 case r::Nil => fuse bs r
 case rs => ALT bs rs
+\]
 
 The simplification does a pattern matching on the regular expression. When it detected that
 the regular expression is an alternative or sequence, it will try to simplify its children regular expressions
@@ -761,15 +761,16 @@
  Function distinct  keeps the first occurring copy only and remove all later ones when detected duplicates.
  Function flatten opens up nested ALT. Its recursive definition is given below:
  \\
- flatten ALT bs rs :: rss = (map fuse( bs,_)  rs )@ flatten rss
+ \[flatten ALT bs rs :: rss = (map fuse( bs,_)  rs )@ flatten rss
  flatten ZERO :: rss = flatten rss
  flatten r::rss = r @ flatten rss if r is of any other shape
+ \]
  
  Here flatten behaves like the traditional functional programming flatten function,
  what it does is basically removing parentheses like changing $a+(b+c)$ into $a+b+c$.
 
 If we apply simplification after each derivative step, we get an optimized version of the algorithm:
-\\TODO definition of blexer_simp
+\\TODO definition of $blexer_simp$
 
 This algorithm effectively keeps the regular expression size small, for example,
 with this simplification our previous $(a + aa)^*$ example's 8000 nodes will be reduced to only 6 and stay constant, however long the input string is.
@@ -814,13 +815,13 @@
  Sulzmann and Lu used this to connect the bit-coded algorithm to the older algorithm by the following equation:\\
  inj r c v = decode retrieve (bder c (internalise r)) v
  Fahad and Christian also used this fact to prove  the correctness of bit-coded algorithm without simplificaiton.
- Our purpose of using this, however, is try to establish 
- retrieve r v = retrieve simp(r) v'.
+ Our purpose of using this, however, is try to establish \\
+$ retrieve \; r \; v \;=\; retrieve  \; simp(r) \; v'.$\\
  Although the r and v are different now,  we can still extract the bitsequence that gies the same parsing information.
  After establishing this, we might be able to finally bridge the gap of proving
- retrieve r \backslash s v = retrieve simp(r) \backslash s v'
+ $retrieve \; r  \; \backslash  \;s \; v = \;retrieve \; simp(r) \; \backslash \; s \; v'$
  and subsequently
- retrieve r \backslash s v = retrieve r \backslash{with simplification} s v'.
+ $retrieve \; r \; \backslash \; s \; v\; = \; retrieve \; r \; \backslash{with simplification}  \; s \; v'$.
  This proves that our simplified version of regular expression still contains all the bitcodes neeeded.
 
 The second task is to speed up the more aggressive simplification. Currently it is slower than a naive simplifiction(the naive version as implemented in ADU of course can explode in some cases).