\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{listings}
 \usepackage{amsthm}
 \usepackage{hyperref}
 \usepackage[margin=0.5in]{geometry}
\usepackage{pmboxdraw}

\theoremstyle{theorem}
\newtheorem{theorem}{Theorem}

\theoremstyle{lemma}
\newtheorem{lemma}{Lemma}
\usepackage{amsmath}
\newcommand{\lemmaautorefname}{Lemma}

\theoremstyle{definition}
 \newtheorem{definition}{Definition}
\begin{document}


\section{Main Result}

Want to prove 
\begin{equation}\label{cen}
\textit{bsimp}(\textit{bder}(c,a)) = \textit{bsimp}(\textit{bder}(c,\textit{bsimp}(a))).
\end{equation}
For simplicity, we use $s$ to denote $\textit{bsimp}$ and use $a \backslash c$ or $d \; c \; a $ to denote $\textit{bder}(c,a)$, then we can write the equation we want to prove in the following manner:
\begin{center}
$s \; d \; c \; a= s \; d \; c \; s \; a$
\end{center}
Specifically, we are interested in the case where $a = a_1+a_2$. The inductive hypothesis is that

\begin{center}
$s \; d \; c \; a_1= s \; d \; c \; s \; a_1 \;  \textbf{and}  \; s \; d \; c \; a_2= s \; d \; c \; s \; a_2.$
\end{center}
\noindent
We want to prove that the $\textit{LHS}$ of \eqref{cen} is equal to the $\textit{RHS}$ of \eqref{cen}.
For better readability the bits are ommitted as they don't inhibit the proof process but just adds to the
nuisance of writing.
$\textit{LHS}$ can be manipulated successively as follows:
\begin{center}
		\begin{tabular}{@{}rrl@{}}
			%\multicolumn{3}{@{}l}{}\medskip\\
			$\textit{LHS}$ & $=$  & $s \; (a_1+a_2) \backslash c$\\
			& $=$ & $s \; (a_1 \backslash c + a_2 \backslash c)$   \\
			& $\overset{\autoref{lma1}}{=}$ & $s(s(a_1 \backslash c) + s(a_2 \backslash c))$         \\
			& $\overset{\autoref{lma2}}{=}$ & $s(s(a_1) \backslash c + s(a_2) \backslash c).$\\
		\end{tabular}
\end{center}
$\textit{RHS}$ can be manipulated this way:
\begin{center}
		\begin{tabular}{@{}rrl@{}}
			%\multicolumn{3}{@{}l}{}\medskip\\
			$\textit{RHS}$ & $=$  & $s \; [(s(a_1+a_2)] \backslash c$\\
		\end{tabular}
\end{center}
If we refer to $s(a_1+a_2)$ as $core$, then we have
\begin{center}
		\begin{tabular}{@{}rrl@{}}
			%\multicolumn{3}{@{}l}{}\medskip\\
			$\textit{RHS}$ & $=$  & $s \; (core \backslash c)$\\
		\end{tabular}
\end{center}
and then
\begin{center}
		\begin{tabular}{@{}rrl@{}}
			%\multicolumn{3}{@{}l}{}\medskip\\
			$\textit{core}$ & $=$  & $s \; \textit{ALTS}(bs, a_1+a_2)$\\
			& $\overset{\mathit{bsimp \; def}}{=}$ & $Li(ALTS(bs, dB(flats(s(a_1)+s(a_2))))$\\	
		\end{tabular}
\end{center}
Here we use $Li$ to refer to the operation that opens up the $\textit{ALTS}$ when it has 1
element, returns 0 when it has 0 elements or does nothing when 
there are 2 or more elements in the list $rs$ in $\textit{ALTS}(bs, rs)$(in scala code corresponds to the case clauses).

Now in order to establish that $LHS = RHS$, we need to
 prove the transformed results we got above
for $LHS$ and $RHS$ are equal to each other.
That is,
\begin{center}
		\begin{tabular}{@{}rrl@{}}
			%\multicolumn{3}{@{}l}{}\medskip\\
			$s(s(a_1) \backslash c + s(a_2) \backslash c)$ & $=$  &  $Li(ALTS(bs, dB(flats(s(a_1)+s(a_2))))$\\	
		\end{tabular}
\end{center}
We shall call the two sides of the above equation $LHS'$ and $RHS'$.
To prove this equality we just need to consider what $s(a_1)$ and $s(a_2)$ look like.
There are three interesting possibility for each, namely 
$s(a_i)$ is an alt, a star or a sequence. Combined that is
9 possibilities. We just need to investigate each of these 9 possibilities.
Here we only one of the 9 cases. The others are handled in a similar 
fashion.

When $s(a_1) = ALTS(bs_1, as_1)$ and $s(a_2) = ALTS(bs_2, as_2)$,
\begin{center}
			$\textit{LHS'}$ \\
			 $=$   \\
			  $s(ALTS(bs, ALTS(bs_1, as_1) \backslash c
			+ ALTS(bs_2, as_2) \backslash c))$\\
			$=$ \\
			 $s(ALTS(bs, ALTS(bs_1, as_1.map \backslash c )+ ALTS(bs_2,as_2.map \backslash c) )  )$\\
			 			$\overset{\autoref{lma3}}{=}$ \\
			 $s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
\end{center} 

And then we deal with $RHS'$:
$RHS'$\\
			 			$\overset{\autoref{lma4}}{=}$ \\
			 $s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))++ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
and this completes the proof.

\begin{lemma}{doing simplification in advance to subparts}\label{lma1}\\
We have that for any annotated regular expressions $a_1 \; a_2$ and bitcode $bs$,\\
$\textit{bsimp}(\textit{ALTS}(bs, a_1, a_2)) =
 \textit{bsimp}(\textit{ALTS}(bs, \textit{bsimp}(a_1), \textit{bsimp}(a_2))) $
\end{lemma}

\begin{lemma}{combination of lemma 1 and inductive hypothesis(from now on use simple notation)}\label{lma2}\\
We have that for any annotated regular expressions $a_1 \; a_2$ and bitcode $bs$,
$s(s(a_1 \backslash c) + s(a_2 \backslash c)) = 
s(s(a_1) \backslash c + s(a_2) \backslash c)$
\end{lemma}


%\begin{theorem}See~\cref{lma1}.\end{theorem}
%\begin{lemma}\label{lma1}\lipsum[2]\end{lemma}

\begin{lemma}{Spilling out ALTS does not affect simplification result}\label{lma3}\\
$s(ALTS(bs, ALTS(bs_1, as_1.map \backslash c )+ ALTS(bs_2,as_2.map \backslash c) )  )$\\
			 			$\overset{\autoref{lma3}}{=}$ \\
			 $s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
\end{lemma}

\begin{lemma}{deleting duplicates does not affect simplification result}\label{lma4}\\
$s(ALTS(bs,  (as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  )$\\
$=$\\
$s(ALTS(bs,  dB((as_1.map \backslash c ).map(fuse(bs_1))+ (as_2.map \backslash c).map(fuse(bs_2)) )  ))$
\end{lemma}

\begin{lemma}{mkepsBC invariant manipulation of bits and notation}\label{lma7}\\
ALTS(bs, ALTS(bs1, rs1), ALTS(bs2, rs2)) $\sim_{m\epsilon}$ ALTS(bs, rs1.map(fuse(bs1, \_)) ++ rs2.map(fuse(bs2, \_)) ). \\
We also use $bs2>>rs2 $ as a shorthand notation for rs2.map(fuse(bs2,\_)).
\end{lemma}



\begin{lemma}{What does dB do to two already simplified ALTS}\label{lma5}\\
$d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) = d Co(ALTS(bs, bs1>>rs1 ++ ((bs2>>rs2)--rs1)        )) $ 
\end{lemma}
\begin{proof}
We prove that $ dB(bs1>>rs1 ++ bs2>>rs2) = bs1>>rs1 ++ ((bs2>>rs2)--rs1)$.


\end{proof}

\begin{lemma}{after opening two previously simplified alts up into terms, length must exceed 2}\label{lma6}\\
If sr1, sr2 are of the form ALTS(bs1, rs1), ALTS(bs2, rs2) respectively, then we have that 
$Co(bs, (bs1>>rs1) ++ (bs2>>rs2)--rs1) = ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)$
\end{lemma}
\begin{proof}
 $Co(bs, rs) \sim_{m\epsilon} ALTS(bs, rs)$ if $rs$ is a list of length greater than or equal to 2.
 As suggested by the title of this lemma, ALTS(bs1, rs1) is a result of simplification, which means that rs1 must be composed of at least 2 distinct regular terms. This alone says that $bs1>>rs1 ++ (bs2>>rs2)--rs1$ is a list of length greater than or equal to 2, as the second operand of the concatenation operator $(bs2>>rs2) -- rs1$ can only contribute a non-negative value to the overall length of the list 
 $bs1>>rs1 ++ (bs2>>rs2)--rs1$.
\end{proof}


\begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS+ some deletion after derivatives)}\label{lma8}\\
$d ALTS(bs, bs1>>rs1 ++ bs2>>rs2) \sim_{m\epsilon} d ALTS(bs, bs1>>rs1 ++ ((bs2>>rs2)--rs1)        ) $ 
\end{lemma}
\begin{proof}
Let's call $bs1>>rs1$ $rs1'$ and  $bs2>>rs2$ $rs2'$. Then we need to prove $d ALTS(bs, rs1' ++rs2') \sim_{m\epsilon} d ALTS(bs, rs1'++(rs2' -- rs1') )   $.\\
We might as well omit the prime in each rs for simplicty of notation and prove $d ALTS(bs, rs1++rs2) \sim_{m\epsilon} d ALTS(bs, rs1++(rs2 -- rs1) )   $.\\
We know that the result of derivative is nullable, so there must exist an r in rs1++rs2 s.t. r is nullable.\\
If $r \in rs1$, then equivalence holds. If $r \in rs2 \wedge  r \notin rs1$, equivalence holds as well. This completes the proof.
\end{proof}

\begin{lemma}{nullability relation between a regex and its simplified version}\label{lma9}\\
$r\ nullable \iff sr\ nullable $ 
\end{lemma}

\begin{lemma}{concatenation + simp invariance of mkepsBC}\label{lma10}\\
$mkepsBC r1 \cdot sr2 = mkepsBC r1 \cdot r2$ if both r1 and r2 are nullable.
\end{lemma}


\begin{theorem}{Correctness Result}

\begin{itemize}

\item{}
When s is a string in the language L(ar), \\
ders\_simp(ar, s)  $\sim_{m\epsilon}$ ders(ar, s), \\
\item{}
when s is not a string of the language L(ar)
ders\_simp(ar, s) is not nullable
\end{itemize}
\end{theorem}

\begin{proof}{Split into 2 parts.}
\begin{itemize}
\item


When we have an annotated regular expression ar and a string s that matches ar, by the correctness of the algorithm ders, we have that ders(ar, s) is nullable, and that mkepsBC will extract the desired bits for decoding the correct value v for the matching, and v is a POSIX value. Now we prove that mkepsBC(ders\_simp(ar, s)) yields the same bitsequence.
\\
We first open up the ders\_simp function into nested alternating sequences of ders and simp.
Assume that s = $c_1...c_n$($n \geq 1$ ) where each of the $c_i$ are characters. 
Then $ders\_simp(ar, s)$ = $s(d_{c_n}(...s(d_{c_1}(r))...))$ = $sdsd......sdr$. If we can prove that
$sdr \sim_{m\epsilon} dsr$ holds for any regular expression and any character, then we are done. This is because then we can push ders operation inside and move simp operation outside and have that $sdsd...sdr \sim_{m\epsilon} ssddsdsd...sdr \sim_{m\epsilon} ... \sim_{m\epsilon} s....sd....dr$.
 Using \autoref{lma1} we have that $s...sd....dr = sd...dr$. 
By \autoref{lma2}, we have $RHS \sim_{m\epsilon} d...dr$.\\
Notice that we don't actually need \autoref{lma1} here. That is because by \autoref{lma2}, we can have that $s...sd....dr \sim_{m\epsilon} sd...dr$. The equality above can be replaced by mkepsBC
 equivalence without affecting the validity of the whole proof since all we want is mkepsBC equivalence, not equality.

Now we proceed to prove that $sdr \sim_{m\epsilon} dsr$. This can be reduced to proving $dr \sim_{m\epsilon} dsr$ as we know that $dr \sim_{m\epsilon} sdr$ by \autoref{lma2}.\\

we use an induction proof. Base cases are omitted. Here are the 3 inductive cases.
\begin{itemize}

\item{$r_1+r_2$}\\
The most difficult case is when $sr1$ and $sr2$ are both ALTS, so that they will be opened up in the flats function and some terms in sr2 might be deleted. Or otherwise we can use the argument that $d(r_1+r_2) = dr_1 + dr_2  \sim_{m\epsilon} dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$,
 the last equivalence being established by \autoref{lma3}.
When $s(r_1), s(r_2)$ are both ALTS, we have to be more careful for the last equivalence step, namelly, $dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$. \\
We have that $LHS = dsr_1 + dsr_2 = d(sr_1 +sr_2)$. Since $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have  $  d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ by \autoref{lma4}.
On the other hand, $RHS = ds(ALTS(bs, r1, r2)) = d Co(bs, dB(flats(s(r1), s(r2)) ) ) = d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2))$ by definition of bsimp and flats.\\  
$d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2)) = d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1))) $ by \autoref{lma5}.\\ $d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1)        )) = d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1))$ by \autoref{lma6}. \\
 Using \autoref{lma8}, we have  $d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2)) \sim_{m\epsilon}  RHS$.\\
 %only the last part we don't have an equality here. We use mkeps equivalence instead because these two regexes are indeed different syntactically. However, they have even more in common than just mkeps equal. We might later augment this proof so that this equivalence relation is changed to something like regular expression equivalence.
 This completes the proof.
\item{$r*$}\\
$s(r*) = r*$. Our goal is trivially achieved.
\item{$r1 \cdot r2$}\\
When r1 is nullable, $ds r1r2 = dsr1 \cdot sr2 + dsr2  \sim_{m\epsilon}  dr1 \cdot sr2 + dr2 = dr1 \cdot r2 + dr2 $. The last step uses \autoref{lma10}. 
When r1 is not nullable, $ds r1r2 = dsr1 \cdot sr2  \sim_{m\epsilon}  dr1 \cdot sr2  \sim_{m\epsilon}  dr1 \cdot r2 $

\end{itemize}
\item
Proof of second part of the theorem: use a similar structure of argument as in the first part.

\item
This proof has a major flaw: it assumes all dr is nullable along the path of deriving r by s. But it could be the case that $s\in L(r)$ but $ \exists s' \in Pref(s) \ s.t.\ ders(s', r)$ is not nullable (or equivalently, $s'\notin L(r)$). One remedy for this is to replace the mkepsBC equivalence relation into some other transitive relation that entails mkepsBC equivalence.
\end{itemize}
\end{proof}

\begin{theorem}{
This is a very strong claim that has yet to be more carefully examined and proved. However, experiments suggest a very good hope for this.}\\
Define pushbits as the following:\\  
\begin{verbatim}
def pushbits(r: ARexp): ARexp = r match {
    case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
    case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
    case r => r
  }
  \end{verbatim}
Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\
Unfortunately this does not hold. A counterexample is\\
\begin{verbatim}
baa
original regex
STA
 └-ALT
    └-STA List(Z)
    |  └-a
    └-ALT List(S)
       └-b List(Z)
       └-a List(S)
regex after ders simp
ALT List(S, S, Z, C(b))
 └-SEQ
 |  └-STA List(S, Z, S, C(a), S, C(a))
 |  |  └-a
 |  └-STA
 |     └-ALT
 |        └-STA List(Z)
 |        |  └-a
 |        └-ALT List(S)
 |           └-b List(Z)
 |           └-a List(S)
 └-SEQ List(S, Z, S, C(a), Z)
    └-ALT List(S)
    |  └-STA List(Z, S, C(a))
    |  |  └-a
    |  └-ONE List(S, S, C(a))
    └-STA
       └-ALT
          └-STA List(Z)
          |  └-a
          └-ALT List(S)
             └-b List(Z)
             └-a List(S)
regex after ders
ALT
 └-SEQ
 |  └-ALT List(S)
 |  |  └-SEQ List(Z)
 |  |  |  └-ZERO
 |  |  |  └-STA
 |  |  |     └-a
 |  |  └-ALT List(S)
 |  |     └-ZERO
 |  |     └-ZERO
 |  └-STA
 |     └-ALT
 |        └-STA List(Z)
 |        |  └-a
 |        └-ALT List(S)
 |           └-b List(Z)
 |           └-a List(S)
 └-ALT List(S, S, Z, C(b))
    └-SEQ
    |  └-ALT List(S)
    |  |  └-ALT List(Z)
    |  |  |  └-SEQ
    |  |  |  |  └-ZERO
    |  |  |  |  └-STA
    |  |  |  |     └-a
    |  |  |  └-SEQ List(S, C(a))
    |  |  |     └-ONE List(S, C(a))
    |  |  |     └-STA
    |  |  |        └-a
    |  |  └-ALT List(S)
    |  |     └-ZERO
    |  |     └-ZERO
    |  └-STA
    |     └-ALT
    |        └-STA List(Z)
    |        |  └-a
    |        └-ALT List(S)
    |           └-b List(Z)
    |           └-a List(S)
    └-SEQ List(S, Z, S, C(a), Z)
       └-ALT List(S)
       |  └-SEQ List(Z)
       |  |  └-ONE List(S, C(a))
       |  |  └-STA
       |  |     └-a
       |  └-ALT List(S)
       |     └-ZERO
       |     └-ONE List(S, C(a))
       └-STA
          └-ALT
             └-STA List(Z)
             |  └-a
             └-ALT List(S)
                └-b List(Z)
                └-a List(S)
regex after ders and then a single simp
ALT
 └-SEQ List(S, S, Z, C(b))
 |  └-STA List(S, Z, S, C(a), S, C(a))
 |  |  └-a
 |  └-STA
 |     └-ALT
 |        └-STA List(Z)
 |        |  └-a
 |        └-ALT List(S)
 |           └-b List(Z)
 |           └-a List(S)
 └-SEQ List(S, S, Z, C(b), S, Z, S, C(a), Z)
    └-ALT List(S)
    |  └-STA List(Z, S, C(a))
    |  |  └-a
    |  └-ONE List(S, S, C(a))
    └-STA
       └-ALT
          └-STA List(Z)
          |  └-a
          └-ALT List(S)
             └-b List(Z)
             └-a List(S)
\end{verbatim}
\end{theorem}

\end{document}

%The second part might still need some more development.
%When s is not in the set L(ar), we have that s = s1@s2 s.t. s1 $\in$ L(ar), and any longer string that is a prefix of s does not belong to L(ar).\\
%By first part of proof, we have ders(ar, s1) $\sim_{m\epsilon}$ ders\_simp(ar, s1)
%.....somehow show that by correctness, der(c, ders\_simp(ar, s1)) must be not nullable. But this will need that L(ders(ar, s1)) == L(ders\_simp(ar, s1)). By part 1 of proof we only have that for any string s1c s.t. s1c $\in$ L(ar) (which is equivalent to s $\in$ L(ders(ar, s1))), s is also in L(ders\_simp(ar, s1)). That is an inclusion, not an equality. c not in L(ders(ar, s1)) does not imply c not in L(ders\_simp(ar, s1))
%So this path stuck here.