diff -r 1ab693d6342f -r 35b80e37dfe7 ChengsongTanPhdThesis/Chapters/Chapter1.tex
--- a/ChengsongTanPhdThesis/Chapters/Chapter1.tex	Tue May 03 13:11:41 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter1.tex	Fri May 06 13:22:20 2022 +0100
@@ -13,18 +13,30 @@
 \newcommand{\file}[1]{\texttt{\bfseries#1}}
 \newcommand{\option}[1]{\texttt{\itshape#1}}
 
-\newcommand{\bderssimp}[2]{{#1} \backslash_{bsimp} {#2}}
+%\newcommand{\sflataux}[1]{\textit{sflat}\_\textit{aux} \, #1}
+\newcommand\sflat[1]{\llparenthesis #1 \rrparenthesis }
+\newcommand{\ASEQ}[3]{\textit{ASEQ}_{#1} \, #2 \, #3}
+\newcommand{\bderssimp}[2]{#1 \backslash_{bsimp} #2}
+\newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2}
+\newcommand{\bsimp}[1]{\textit{bsimp}(#1)}
+\newcommand{\rsimp}[1]{\textit{rsimp}(#1)}
+\newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'}
 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
 \newcommand{\ZERO}{\mbox{\bf 0}}
 \newcommand{\ONE}{\mbox{\bf 1}}
+\newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2}
+
+\newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}}
+
 \def\lexer{\mathit{lexer}}
 \def\mkeps{\mathit{mkeps}}
 
 \def\AZERO{\textit{AZERO}}
 \def\AONE{\textit{AONE}}
 \def\ACHAR{\textit{ACHAR}}
-\def\ASEQ{\textit{ASEQ}}
-\def\AALTS{\textit{AALTS}}
+
+
+\def\ALTS{\textit{ALTS}}
 \def\ASTAR{\textit{ASTAR}}
 \def\DFA{\textit{DFA}}
 \def\bmkeps{\textit{bmkeps}}
@@ -33,7 +45,7 @@
 \def\flex{\textit{flex}}
 \def\inj{\mathit{inj}}
 \def\Empty{\mathit{Empty}}
-\def\Left{\mathit{Left}}
+\def\Left{\mathit{Left}}xc
 \def\Right{\mathit{Right}}
 \def\Stars{\mathit{Stars}}
 \def\Char{\mathit{Char}}
@@ -46,22 +58,33 @@
 %\def\bderssimp{\mathit{bders}\_\mathit{simp}}
 \def\distinctWith{\textit{distinctWith}}
 
+\def\rexp{\mathbf{rexp}}
 \def\simp{\mathit{simp}}
 \def\simpALTs{\mathit{simp}\_\mathit{ALTs}}
 \def\map{\mathit{map}}
 \def\distinct{\mathit{distinct}}
 \def\blexersimp{\mathit{blexer}\_\mathit{simp}}
 \def\map{\textit{map}}
-\def\vsuf{\textit{vsuf}}
-\def\sflataux{\textit{sflat}\_\textit{aux}}
+%\def\vsuf{\textit{vsuf}}
+%\def\sflataux{\textit{sflat}\_\textit{aux}}
 \def\rrexp{\textit{rrexp}}
-\def\rsize{\textit{rsize}}
-\def\asize{\textit{asize}}
-\def\rerase{\textit{rerase}}
+\newcommand\rnullable[1]{\textit{rnullable}(#1)}
+\newcommand\rsize[1]{\llbracket #1 \rrbracket_r}
+\newcommand\asize[1]{\llbracket #1 \rrbracket}
+\newcommand\rerase[1]{ (#1)\downarrow_r}
+
 \def\erase{\textit{erase}}
 \def\STAR{\textit{STAR}}
 \def\flts{\textit{flts}}
 
+
+\def\RZERO{\mathbf{0}_r }
+\def\RONE{\mathbf{1}_r}
+\newcommand\RCHAR[1]{\mathbf{#1}_r}
+\newcommand\RSEQ[2]{#1 \cdot #2}
+\newcommand\RALTS[1]{\oplus #1}
+\newcommand\RSTAR[1]{#1^*}
+\newcommand\vsuf[2]{\textit{vsuf} \;#1\;#2}
 %----------------------------------------------------------------------------------------
 %This part is about regular expressions, Brzozowski derivatives,
 %and a bit-coded lexing algorithm with proven correctness and time bounds.