--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/big_lemma.tex	Mon Jul 22 22:30:47 2019 +0100
@@ -0,0 +1,71 @@
+\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.