--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Tue Jun 28 21:07:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Wed Jun 29 12:38:05 2022 +0100
@@ -852,13 +852,49 @@
 The reason why we take the trouble of defining 
 two separate list rewriting definitions $\frewrite$ and $\grewrite$
 is that sometimes $\grewrites$ is slightly too powerful
-that it renders certain equivalence to break after derivative:
-
-$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} \neq 
-	\rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing})} $
+for proving equivalence.
+For example, when proving the closed-form for the alternative regular expression,
+one of the rewriting steps would be:
+\begin{lemma}
+	$\sum (\rDistinct \; (\map \; (\_ \backslash x) \; (\rflts \; rs)) \; \varnothing) \sequal
+	 \sum (\rDistinct \; (\rflts \; (\map \; (\_ \backslash x) \; rs)) \; \varnothing)
+	 $
+\end{lemma}
+\noindent
+Proving this is by first showing 
+\begin{lemma}
+	$\map \; (\_ \backslash x) \;  (\rflts \; rs) \frewrites
+\rflts \; (\map \; (\_ \backslash x) \; rs)$
+\end{lemma}
+\noindent
+and then using lemma
+\begin{lemma}\label{frewritesSimpeq}
+	If $rs_1 \frewrites rs_2 $, then $\sum (\rDistinct \; rs_1 \; \varnothing) \sequal 
+	\sum (\rDistinct \;  rs_2 \;  {})$.
+\end{lemma}
+. But this trick will not work for $\grewrites$:
+\begin{center}
+$\map \; (\_ \backslash x) \; (\rDistinct \; rs \; rset) \grewrites \rDistinct \; (\map \;
+(\_ \backslash x) \; rs) \; (\map \; (\_ \backslash x) \; rset)$
+\end{center}
+\noindent
+does \emph{not} hold.
 
 
 
+
+%this is for closed form for alts section, talk about that later------------------------------
+\begin{comment}
+\begin{center}
+$\rsimp{(\rsimpalts \; (\map \; (\_ \backslash x) \; (\rdistinct{(\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs}))))}{\varnothing})))} = 
+\rsimp{(\rsimpalts \; (\rdistinct{(\map \; (\_ \backslash x) \; (\rflts \; (\map \; (\rsimp{} \; \circ \; (\lambda r. \rderssimp{r}{xs})))) ) }{\varnothing}))} $
+\end{center}
+	
+\noindent
+This is not possible to prove 
+
+\end{comment}
+%this is for closed form for alts section, talk about that later------------------------------
 And we define an "grewrite" relation that works on lists:
 \begin{center}
 \begin{tabular}{lcl}
@@ -1321,14 +1357,10 @@
 
 
 There are a few key steps, one of these steps is
-\[
-rsimp (rsimp\_ALTs (map (rder x) (rdistinct (rflts (map (rsimp \circ (\lambda r. rders\_simp r xs)) rs)) {})))
-= rsimp (rsimp\_ALTs (rdistinct (map (rder x) (rflts (map (rsimp \circ (\lambda r. rders\_simp r xs)) rs))) {}))
-\]
+
 
 
 One might want to prove this by something a simple statement like: 
-$map (rder x) (rdistinct rs rset) = rdistinct (map (rder x) rs) (rder x) ` rset)$.
 
 For this to hold we want the $\textit{distinct}$ function to pick up
 the elements before and after derivatives correctly: