78
+ − 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.