\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[english]{babel}
\usepackage{listings}
 \usepackage{amsthm}
 \usepackage{hyperref}
 \usepackage[margin=1in]{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{BIG lemma} \begin{equation}\label{bg} \textit{ bsimp}( \textit{ ALTS}(
	bs, \textit{ ALTS}( bs_1, as_1),\textit{ ALTS}( bs2, as_2)))) =
	\textit{ bsimp}(\textit{ALTS}( bs, \textit{ map} \; ( \textit{fuse} \;
	bs_1) \; as_1 ++  \textit{ map} \; (\textit{fuse} \;  bs_2) \; as_2))
\end{equation}	We want to show the $ \textit{ LHS}$ of \eqref{bg} is equal to
the $ \textit{ RHS}$ of \eqref{bg}.  We can first write it in a shorter and
more readable form. And that is \begin{equation}\label{sm} s (A ( bs, A ( bs_1,
as_1), A ( bs_2, as_2)))=s(A(bs, (bs_1 \rightarrow as_1) @ (bs_2 \rightarrow
as_2))) \end{equation} Where $s$ means $\textit{bsimp}$ and $A$ stands for
$\textit{ALTS}$. The right arrow denotes the $\textit{map \; fuse}$ operation.
We want to transform both sides into function application of $\textit{bsimp}$
with its arguments involving regexes of the form $s(as_1)$ and $s(as_2)$, which
can then be expanded by a case-by-case analysis. Each case can then be shown
with ease.  We have the following:\\ $\textit{LHS}=\textit{s}(A(bs, A(bs_1,
as_1),A(bs_2, as_2)))=s(A(bs, s(A(bs_1,as_1)), s(A(bs_2,as_2)))).$ \\This is by
a previous lemma. We get "free" $\textit{bsimp}$ on the inner 2
$\textit{ALTS}$s out of nowhere.  And by application of the inner
$\textit{bsimp}$ in the above expression, we have that\\ $s(A(bs,
s(A(bs_1,as_1)), s(A(bs_2,as_2)))) = s(A(bs, Li(A(bs_1,
\textit{flts}(s(as_1)))),Li(A(bs_2, \textit{flts}(s(as_2))) ) )).$\\ Now we
have successfully added $s$ to $as_1$ and $as_2$.  Let us transform the
$\textit{RHS}$ of equation \eqref{bg}.  \\ $\textit{RHS}=s(s(A(bs, (bs_1
\rightarrow as_1)@(bs_2 \rightarrow as_2))))=s(Li(A(bs,
\textit{flts}(s(as_1'@as_2'))))).$ \\where the $as_i'$ corresponds to $bs_i
\rightarrow as_i$.  \\The right hand side of the above equation can again be
transformed into $s(Li(A(bs, \textit{flts}(s(as_1')@s(as_2'))))).$ \\You might
want to have a lemma for $s(as_1'@as_2')= s(as_1')@s(as_2')$, which is
basically a linearity property of the $\textit{map}$ function.  The above
expression can then again be transformed into $s(Li(A(bs,
\textit{flts}(s(as_1'))@\textit{flts}(s(as_2')))).$ You might again want to
have a lemma for this linearity property of $\textit{flats}.$\\
%The above can be then again transformed into $\$
We now want to equate $s(Li(A(bs,
\textit{flts}(s(as_1'))@\textit{flts}(s(as_2'))))$ with $s(A(bs, Li(A(bs_1,
\textit{flts}(s(as_1)))),Li(A(bs_2, \textit{flts}(s(as_2))) ) ))$ \\ We just
need to equate the contents inside $\textit{bsimp}$, namely we want to prove\\
$Li(A(bs, \textit{flts}(s(as_1'))@\textit{flts}(s(as_2'))))$ with $A(bs,
Li(A(bs_1, \textit{flts}(s(as_1)))),Li(A(bs_2, \textit{flts}(s(as_2))) ) ).$ \\
This shouldn't be surprising, we have added redundant $\textit{bsimp}$, now we
are just removing it.  This is where we need a case-by-case analysis.  We need
to assume the conditions when $s(as_i')$ is empty list, single element list and
list with 2 or more elements.  They are all trivial and therefore ommitted.

\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.