diff -r fa92124d1fb7 -r b306628a0eab ChengsongTanPhdThesis/Chapters/Introduction.tex
--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Fri Sep 02 19:35:55 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Sat Sep 03 00:14:20 2022 +0100
@@ -20,7 +20,7 @@
 \newcommand\sflat[1]{\llparenthesis #1 \rrparenthesis }
 \newcommand{\ASEQ}[3]{\textit{ASEQ}_{#1} \, #2 \, #3}
 \newcommand{\bderssimp}[2]{#1 \backslash_{bsimps} #2}
-\newcommand{\rderssimp}[2]{#1 \backslash_{rsimp} #2}
+\newcommand{\rderssimp}[2]{#1 \backslash_{rsimps} #2}
 \def\derssimp{\textit{ders}\_\textit{simp}}
 \def\rders{\textit{rders}}
 \newcommand{\bders}[2]{#1 \backslash #2}
@@ -137,6 +137,9 @@
 \def\rflts{\textit{rflts}}
 \def\rrewrite{\textit{rrewrite}}
 \def\bsimpalts{\textit{bsimp}_{ALTS}}
+\def\bsimpaseq{\textit{bsimp}_{ASEQ}}
+\def\rsimlalts{\textit{rsimp}_{ALTs}}
+\def\rsimpseq{\textit{rsimp}_{SEQ}}
 
 \def\erase{\textit{erase}}
 \def\STAR{\textit{STAR}}