# HG changeset patch
# User Chengsong
# Date 1652748270 -3600
# Node ID 84938708781d4db1e96b231b364bb8aeb2602ca5
# Parent  036600af4c30b88727aae1a1966f8c4fdda0cba6
a bit

diff -r 036600af4c30 -r 84938708781d ChengsongTanPhdThesis/Chapters/Chapter2.tex
--- a/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Tue May 17 00:54:29 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Tue May 17 01:44:30 2022 +0100
@@ -215,10 +215,40 @@
 but this time we will have stronger equalities established.
 \subsection{"hrewrite" relation}
 List of 1-step rewrite rules for regular expressions simplification without bitcodes:
-\
+\begin{center}
+\begin{tabular}{lcl}
+$r_1 \cdot \ZERO$ & $\rightarrow$ & $\ZERO$
+\end{tabular}
+\end{center}
+
+And we define an "grewrite" relation that works on lists:
+\begin{center}
+\begin{tabular}{lcl}
+$ \ZERO :: rs$ & $\rightarrow_g$ & $rs$
+\end{tabular}
+\end{center}
 
 
 
+With these relations we prove
+\begin{lemma}
+$rs \rightarrow rs'  \implies \RALTS{rs} \rightarrow \RALTS{rs'}$
+\end{lemma}
+which enables us to prove "closed forms" equalities such as
+\begin{lemma}
+$\sflat{(r_1 \cdot r_2) \backslash s} = \RALTS{ (r_1 \backslash s) \cdot r_2 :: (\map (r_2 \backslash \_) (\vsuf{s}{r_1}))}$
+\end{lemma}
+
+But the most involved part of the above lemma is proving the following:
+\begin{lemma}
+$\bsimp{\RALTS{rs @ \RALTS{rs_1} @ rs'}} = \bsimp{\RALTS{rs @rs_1 @ rs'}} $ 
+\end{lemma}
+which is needed in proving things like 
+\begin{lemma}
+$r \rightarrow_f r'  \implies \rsimp{r} \rightarrow \rsimp{r'}$
+\end{lemma}
+.
+Fortunately this is provable by induction on the list $rs$
 
 %----------------------------------------------------------------------------------------
 %	SECTION ??