1 \documentclass{article}

     2 \usepackage[utf8]{inputenc}

     3 \usepackage[english]{babel}

     4 \usepackage{listings}

     5  \usepackage{amsthm}

     6  \usepackage{hyperref}

     7  \usepackage[margin=1in]{geometry}

     8 \usepackage{pmboxdraw}

     9 

    10 \theoremstyle{theorem}

    11 \newtheorem{theorem}{Theorem}

    12 

    13 \theoremstyle{lemma}

    14 \newtheorem{lemma}{Lemma}

    15 \usepackage{amsmath}

    16 \newcommand{\lemmaautorefname}{Lemma}

    17 

    18 \theoremstyle{definition}

    19  \newtheorem{definition}{Definition}

    20 \begin{document}

    21 

    22 \section{BIG lemma} \begin{equation}\label{bg} \textit{ bsimp}( \textit{ ALTS}(

    23 	bs, \textit{ ALTS}( bs_1, as_1),\textit{ ALTS}( bs2, as_2)))) =

    24 	\textit{ bsimp}(\textit{ALTS}( bs, \textit{ map} \; ( \textit{fuse} \;

    25 	bs_1) \; as_1 ++  \textit{ map} \; (\textit{fuse} \;  bs_2) \; as_2))

    26 \end{equation}	We want to show the $ \textit{ LHS}$ of \eqref{bg} is equal to

    27 the $ \textit{ RHS}$ of \eqref{bg}.  We can first write it in a shorter and

    28 more readable form. And that is \begin{equation}\label{sm} s (A ( bs, A ( bs_1,

    29 as_1), A ( bs_2, as_2)))=s(A(bs, (bs_1 \rightarrow as_1) @ (bs_2 \rightarrow

    30 as_2))) \end{equation} Where $s$ means $\textit{bsimp}$ and $A$ stands for

    31 $\textit{ALTS}$. The right arrow denotes the $\textit{map \; fuse}$ operation.

    32 We want to transform both sides into function application of $\textit{bsimp}$

    33 with its arguments involving regexes of the form $s(as_1)$ and $s(as_2)$, which

    34 can then be expanded by a case-by-case analysis. Each case can then be shown

    35 with ease.  We have the following:\\ $\textit{LHS}=\textit{s}(A(bs, A(bs_1,

    36 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

    37 a previous lemma. We get "free" $\textit{bsimp}$ on the inner 2

    38 $\textit{ALTS}$s out of nowhere.  And by application of the inner

    39 $\textit{bsimp}$ in the above expression, we have that\\ $s(A(bs,

    40 s(A(bs_1,as_1)), s(A(bs_2,as_2)))) = s(A(bs, Li(A(bs_1,

    41 \textit{flts}(s(as_1)))),Li(A(bs_2, \textit{flts}(s(as_2))) ) )).$\\ Now we

    42 have successfully added $s$ to $as_1$ and $as_2$.  Let us transform the

    43 $\textit{RHS}$ of equation \eqref{bg}.  \\ $\textit{RHS}=s(s(A(bs, (bs_1

    44 \rightarrow as_1)@(bs_2 \rightarrow as_2))))=s(Li(A(bs,

    45 \textit{flts}(s(as_1'@as_2'))))).$ \\where the $as_i'$ corresponds to $bs_i

    46 \rightarrow as_i$.  \\The right hand side of the above equation can again be

    47 transformed into $s(Li(A(bs, \textit{flts}(s(as_1')@s(as_2'))))).$ \\You might

    48 want to have a lemma for $s(as_1'@as_2')= s(as_1')@s(as_2')$, which is

    49 basically a linearity property of the $\textit{map}$ function.  The above

    50 expression can then again be transformed into $s(Li(A(bs,

    51 \textit{flts}(s(as_1'))@\textit{flts}(s(as_2')))).$ You might again want to

    52 have a lemma for this linearity property of $\textit{flats}.$\\

    53 %The above can be then again transformed into $\$

    54 We now want to equate $s(Li(A(bs,

    55 \textit{flts}(s(as_1'))@\textit{flts}(s(as_2'))))$ with $s(A(bs, Li(A(bs_1,

    56 \textit{flts}(s(as_1)))),Li(A(bs_2, \textit{flts}(s(as_2))) ) ))$ \\ We just

    57 need to equate the contents inside $\textit{bsimp}$, namely we want to prove\\

    58 $Li(A(bs, \textit{flts}(s(as_1'))@\textit{flts}(s(as_2'))))$ with $A(bs,

    59 Li(A(bs_1, \textit{flts}(s(as_1)))),Li(A(bs_2, \textit{flts}(s(as_2))) ) ).$ \\

    60 This shouldn't be surprising, we have added redundant $\textit{bsimp}$, now we

    61 are just removing it.  This is where we need a case-by-case analysis.  We need

    62 to assume the conditions when $s(as_i')$ is empty list, single element list and

    63 list with 2 or more elements.  They are all trivial and therefore ommitted.

    64 

    65 \end{document}

    66 

    67 %The second part might still need some more development.

    68 %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).\\

    69 %By first part of proof, we have ders(ar, s1) $\sim_{m\epsilon}$ ders\_simp(ar, s1)

    70 %.....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))

    71 %So this path stuck here.