ChengsongTanPhdThesis/Chapters/Further.tex
author Christian Urban <christian.urban@kcl.ac.uk>
Sat, 10 Sep 2022 15:04:35 +0100
changeset 598 2c9a3aba8ebc
parent 532 cc54ce075db5
permissions -rwxr-xr-x
simplified the n-times case in decode_aux

% Chapter Template

\chapter{Further Improvements} % Main chapter title

\label{Further} %In Chapter 5\ref{Chapter5} we discuss stronger simplifications to improve the finite bound
%in Chapter 4 to a polynomial one, and demonstrate how one can extend the
%algorithm to include constructs such as bounded repetitions and negations.
 
%----------------------------------------------------------------------------------------
%	SECTION strongsimp
%----------------------------------------------------------------------------------------
\section{Zippers}
%TODO: search for isabelle proofs of algorithms that check equivalence 

Unfortunately using zippers causes a similar effect like the "break up" rule
and does not preserve the $\POSIX$ property.