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