8
+ − 1 \documentclass{article}
+ − 2 \usepackage[utf8]{inputenc}
+ − 3 \usepackage[english]{babel}
+ − 4 \usepackage{listings}
+ − 5 \usepackage{amsthm}
9
+ − 6 \usepackage{hyperref}
8
+ − 7 \usepackage[margin=0.5in]{geometry}
10
+ − 8 \usepackage{pmboxdraw}
+ − 9
8
+ − 10 \theoremstyle{theorem}
+ − 11 \newtheorem{theorem}{Theorem}
+ − 12
+ − 13 \theoremstyle{lemma}
+ − 14 \newtheorem{lemma}{Lemma}
+ − 15
9
+ − 16 \newcommand{\lemmaautorefname}{Lemma}
+ − 17
8
+ − 18 \theoremstyle{definition}
+ − 19 \newtheorem{definition}{Definition}
+ − 20 \begin{document}
+ − 21 This is a sketch proof for the correctness of the algorithm ders\_simp.
+ − 22 \section{Function Definitions}
+ − 23
+ − 24 \begin{definition}{Bits}
+ − 25 \begin{verbatim}
+ − 26 abstract class Bit
+ − 27 case object Z extends Bit
+ − 28 case object S extends Bit
+ − 29 case class C(c: Char) extends Bit
+ − 30
+ − 31 type Bits = List[Bit]
+ − 32 \end{verbatim}
+ − 33 \end{definition}
+ − 34
+ − 35 \begin{definition}{Annotated Regular Expressions}
+ − 36 \begin{verbatim}
+ − 37 abstract class ARexp
+ − 38 case object AZERO extends ARexp
+ − 39 case class AONE(bs: Bits) extends ARexp
+ − 40 case class ACHAR(bs: Bits, f: Char) extends ARexp
+ − 41 case class AALTS(bs: Bits, rs: List[ARexp]) extends ARexp
+ − 42 case class ASEQ(bs: Bits, r1: ARexp, r2: ARexp) extends ARexp
+ − 43 case class ASTAR(bs: Bits, r: ARexp) extends ARexp
+ − 44 \end{verbatim}
+ − 45 \end{definition}
+ − 46
+ − 47 \begin{definition}{bnullable}
+ − 48 \begin{verbatim}
+ − 49 def bnullable (r: ARexp) : Boolean = r match {
+ − 50 case AZERO => false
+ − 51 case AONE(_) => true
+ − 52 case ACHAR(_,_) => false
+ − 53 case AALTS(_, rs) => rs.exists(bnullable)
+ − 54 case ASEQ(_, r1, r2) => bnullable(r1) && bnullable(r2)
+ − 55 case ASTAR(_, _) => true
+ − 56 }
+ − 57 \end{verbatim}
+ − 58 \end{definition}
+ − 59
+ − 60 \begin{definition}{ders\_simp}
+ − 61 \begin{verbatim}
+ − 62 def ders_simp(r: ARexp, s: List[Char]): ARexp = {
+ − 63 s match {
+ − 64 case Nil => r
+ − 65 case c::cs => ders_simp(bsimp(bder(c, r)), cs)
+ − 66 }
+ − 67 }\end{verbatim}
+ − 68 \end{definition}
+ − 69
+ − 70 \begin{definition}{bder}
+ − 71 \begin{verbatim}
+ − 72 def bder(c: Char, r: ARexp) : ARexp = r match {
+ − 73 case AZERO => AZERO
+ − 74 case AONE(_) => AZERO
+ − 75 case ACHAR(bs, f) => if (c == f) AONE(bs:::List(C(c))) else AZERO
+ − 76 case AALTS(bs, rs) => AALTS(bs, rs.map(bder(c, _)))
+ − 77 case ASEQ(bs, r1, r2) => {
+ − 78 if (bnullable(r1)) AALT(bs, ASEQ(Nil, bder(c, r1), r2), fuse(mkepsBC(r1), bder(c, r2)))
+ − 79 else ASEQ(bs, bder(c, r1), r2)
+ − 80 }
+ − 81 case ASTAR(bs, r) => ASEQ(bs, fuse(List(S), bder(c, r)), ASTAR(Nil, r))
+ − 82 }
+ − 83 \end{verbatim}
+ − 84 \end{definition}
+ − 85
+ − 86 \begin{definition}{bsimp}
+ − 87 \begin{verbatim}
+ − 88 def bsimp(r: ARexp): ARexp = r match {
+ − 89 case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(r2)) match {
+ − 90 case (AZERO, _) => AZERO
+ − 91 case (_, AZERO) => AZERO
+ − 92 case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
+ − 93 case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
+ − 94 }
+ − 95 case AALTS(bs1, rs) => {
+ − 96 val rs_simp = rs.map(bsimp)
+ − 97 val flat_res = flats(rs_simp)
+ − 98 val dist_res = distinctBy(flat_res, erase)
+ − 99 dist_res match {
+ − 100 case Nil => AZERO
+ − 101 case s :: Nil => fuse(bs1, s)
+ − 102 case rs => AALTS(bs1, rs)
+ − 103 }
+ − 104 }
+ − 105 //case ASTAR(bs, r) => ASTAR(bs, bsimp(r))
+ − 106 case r => r
+ − 107 }
+ − 108 \end{verbatim}
+ − 109 \end{definition}
+ − 110
+ − 111 \begin{definition}{sub-parts of bsimp}
+ − 112 \begin{itemize}
+ − 113 \item{flats}\\
+ − 114 flattens the list.
+ − 115 \item{dB}\\
+ − 116 means distinctBy
+ − 117 \item{Co}\\
9
+ − 118 The last matching clause of the function bsimp, with a slight modification to suit later reasoning.
+ − 119 \begin{verbatim}
+ − 120 def Co(bs1, rs): ARexp = {
+ − 121 rs match {
8
+ − 122 case Nil => AZERO
+ − 123 case s :: Nil => fuse(bs1, s)
+ − 124 case rs => AALTS(bs1, rs)
+ − 125 }
9
+ − 126 \end{verbatim}
8
+ − 127 \end{itemize}
+ − 128 \end{definition}
+ − 129
+ − 130 \begin{definition}{fuse}
+ − 131 \begin{verbatim}
+ − 132 def fuse(bs: Bits, r: ARexp) : ARexp = r match {
+ − 133 case AZERO => AZERO
+ − 134 case AONE(cs) => AONE(bs ++ cs)
+ − 135 case ACHAR(cs, f) => ACHAR(bs ++ cs, f)
+ − 136 case AALTS(cs, rs) => AALTS(bs ++ cs, rs)
+ − 137 case ASEQ(cs, r1, r2) => ASEQ(bs ++ cs, r1, r2)
+ − 138 case ASTAR(cs, r) => ASTAR(bs ++ cs, r)
+ − 139 }
+ − 140 \end{verbatim}
+ − 141 \end{definition}
+ − 142
+ − 143
+ − 144 \begin{definition}{mkepsBC}
+ − 145 \begin{verbatim}
+ − 146 def mkepsBC(r: ARexp) : Bits = r match {
+ − 147 case AONE(bs) => bs
+ − 148 case AALTS(bs, rs) => {
+ − 149 val n = rs.indexWhere(bnullable)
+ − 150 bs ++ mkepsBC(rs(n))
+ − 151 }
+ − 152 case ASEQ(bs, r1, r2) => bs ++ mkepsBC(r1) ++ mkepsBC(r2)
+ − 153 case ASTAR(bs, r) => bs ++ List(Z)
+ − 154 }
+ − 155 \end{verbatim}
+ − 156 \end{definition}
+ − 157
+ − 158 \begin{definition}{mkepsBC equicalence}
+ − 159 \\
+ − 160 Given 2 nullable annotated regular expressions r1, r2, if mkepsBC(r1) == mkepsBC(r2)
+ − 161 then r1 and r2 are mkepsBC equivalent, denoted as r1 $\sim_{m\epsilon}$ r2
+ − 162 \end{definition}
+ − 163
+ − 164 \begin{definition}{shorthand notation for ders}
+ − 165 \\For the sake of reducing verbosity, we sometimes use the shorthand notation
+ − 166 $d_{c}(r)$ for the function application bder(c, r) and $s(r)$(s here stands for simplification) for the function application bsimp(r) .
+ − 167 \\We omit the subscript when it is clear from context what that character is and write $d(r)$ instead of $d_{c}(r)$.
+ − 168 \\And we omit the parentheses when no confusion can be caused. For example ders\_simp(c, r) can be written as $s(d_{c}(r))$ or even $s d r$ as we know the derivative operation is w.r.t the character c. Here the s and d are more like operators that take an annotated regular expression as an input and return an annotated regular expression as an output
+ − 169
+ − 170 \end{definition}
+ − 171
+ − 172
+ − 173
+ − 174 \begin{definition}{distinctBy operation expressed in a different way--how it transforms the list}\\
+ − 175 Given two lists rs1 and rs2, we define the operation $--$:\\
+ − 176 $rs1 -- rs2 := [r \in rs1 | r \notin rs2]$
9
+ − 177 Note that the order each term appears in $rs_1 -- rs_2$ is preserved as in the original list.
8
+ − 178 \end{definition}
+ − 179
+ − 180
+ − 181 \section{Main Result}
9
+ − 182
+ − 183 \begin{lemma}{simplification function does not simplify an already simplified regex}\label{lma1}\\
8
+ − 184 bsimp(r) == bsimp(bsimp(r)) holds for any annotated regular expression r.
+ − 185 \end{lemma}
+ − 186
9
+ − 187 \begin{lemma}{simp and mkeps}\label{lma2}\\
8
+ − 188 When r is nullable, we have that
+ − 189 mkeps(bsimp(r)) == mkeps(r)
+ − 190 \end{lemma}
+ − 191
9
+ − 192
+ − 193 %\begin{theorem}See~\cref{lma1}.\end{theorem}
+ − 194 %\begin{lemma}\label{lma1}\lipsum[2]\end{lemma}
+ − 195
+ − 196 \begin{lemma}{mkeps equivalence w.r.t some syntactically different regular expressions(1 ALTS)}\label{lma3}\\
+ − 197 When one of the 2 regular expressions $s(r_1)$ and $s(r_2)$ is of the form ALTS(bs1, rs1), we have that $ds(ALTS(bs, r1, r2)) \sim_{m\epsilon} d(ALTS(bs, sr_1, sr_2))$
8
+ − 198 \end{lemma}
+ − 199 \begin{proof}
9
+ − 200 By opening up one of the alts and show no additional changes are made.\\
+ − 201 Details: $ds(ALTS(bs, r1, r2)) = d Co( bs, dB(flats(sr1, sr2)) )$
8
+ − 202 \end{proof}
+ − 203
9
+ − 204
+ − 205 \begin{lemma}{mkepsBC invariant manipulation of bits and notation}\label{lma7}\\
+ − 206 ALTS(bs, ALTS(bs1, rs1), ALTS(bs2, rs2)) $\sim_{m\epsilon}$ ALTS(bs, rs1.map(fuse(bs1, \_)) ++ rs2.map(fuse(bs2, \_)) ). \\
+ − 207 We also use $bs2>>rs2 $ as a shorthand notation for rs2.map(fuse(bs2,\_)).
+ − 208 \end{lemma}
+ − 209
+ − 210 \begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS)}\label{lma4}\\
8
+ − 211 $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have $ d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$
+ − 212 \end{lemma}
+ − 213 \begin{proof}
+ − 214 We are just fusing bits inside here, there is no other structural change.
+ − 215 \end{proof}
+ − 216
9
+ − 217 \begin{lemma}{What does dB do to two already simplified ALTS}\label{lma5}\\
+ − 218 $d Co(ALTS(bs, dB(bs1>>rs1 ++ bs2>>rs2))) = d Co(ALTS(bs, bs1>>rs1 ++ ((bs2>>rs2)--rs1) )) $
8
+ − 219 \end{lemma}
+ − 220 \begin{proof}
9
+ − 221 We prove that $ dB(bs1>>rs1 ++ bs2>>rs2) = bs1>>rs1 ++ ((bs2>>rs2)--rs1)$.
+ − 222
+ − 223
8
+ − 224 \end{proof}
+ − 225
9
+ − 226 \begin{lemma}{after opening two previously simplified alts up into terms, length must exceed 2}\label{lma6}\\
+ − 227 If sr1, sr2 are of the form ALTS(bs1, rs1), ALTS(bs2, rs2) respectively, then we have that
+ − 228 $Co(bs, (bs1>>rs1) ++ (bs2>>rs2)--rs1) = ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)$
8
+ − 229 \end{lemma}
+ − 230 \begin{proof}
9
+ − 231 $Co(bs, rs) \sim_{m\epsilon} ALTS(bs, rs)$ if $rs$ is a list of length greater than or equal to 2.
+ − 232 As suggested by the title of this lemma, ALTS(bs1, rs1) is a result of simplification, which means that rs1 must be composed of at least 2 distinct regular terms. This alone says that $bs1>>rs1 ++ (bs2>>rs2)--rs1$ is a list of length greater than or equal to 2, as the second operand of the concatenation operator $(bs2>>rs2) -- rs1$ can only contribute a non-negative value to the overall length of the list
+ − 233 $bs1>>rs1 ++ (bs2>>rs2)--rs1$.
8
+ − 234 \end{proof}
+ − 235
+ − 236
9
+ − 237 \begin{lemma}{mkepsBC equivalence w.r.t syntactically different regular expressions(2 ALTS+ some deletion after derivatives)}\label{lma8}\\
+ − 238 $d ALTS(bs, bs1>>rs1 ++ bs2>>rs2) \sim_{m\epsilon} d ALTS(bs, bs1>>rs1 ++ ((bs2>>rs2)--rs1) ) $
+ − 239 \end{lemma}
+ − 240 \begin{proof}
+ − 241 Let's call $bs1>>rs1$ $rs1'$ and $bs2>>rs2$ $rs2'$. Then we need to prove $d ALTS(bs, rs1' ++rs2') \sim_{m\epsilon} d ALTS(bs, rs1'++(rs2' -- rs1') ) $.\\
+ − 242 We might as well omit the prime in each rs for simplicty of notation and prove $d ALTS(bs, rs1++rs2) \sim_{m\epsilon} d ALTS(bs, rs1++(rs2 -- rs1) ) $.\\
+ − 243 We know that the result of derivative is nullable, so there must exist an r in rs1++rs2 s.t. r is nullable.\\
+ − 244 If $r \in rs1$, then equivalence holds. If $r \in rs2 \wedge r \notin rs1$, equivalence holds as well. This completes the proof.
+ − 245 \end{proof}
8
+ − 246
10
+ − 247 \begin{lemma}{nullability relation between a regex and its simplified version}\label{lma9}\\
+ − 248 $r\ nullable \iff sr\ nullable $
+ − 249 \end{lemma}
+ − 250
+ − 251 \begin{lemma}{concatenation + simp invariance of mkepsBC}\label{lma10}\\
+ − 252 $mkepsBC r1 \cdot sr2 = mkepsBC r1 \cdot r2$ if both r1 and r2 are nullable.
+ − 253 \end{lemma}
8
+ − 254
+ − 255
+ − 256 \begin{theorem}{Correctness Result}
+ − 257
+ − 258 \begin{itemize}
+ − 259
+ − 260 \item{}
+ − 261 When s is a string in the language L(ar), \\
+ − 262 ders\_simp(ar, s) $\sim_{m\epsilon}$ ders(ar, s), \\
+ − 263 \item{}
+ − 264 when s is not a string of the language L(ar)
+ − 265 ders\_simp(ar, s) is not nullable
+ − 266 \end{itemize}
+ − 267 \end{theorem}
+ − 268
+ − 269 \begin{proof}{Split into 2 parts.}
+ − 270 \begin{itemize}
+ − 271 \item
+ − 272
9
+ − 273
8
+ − 274 When we have an annotated regular expression ar and a string s that matches ar, by the correctness of the algorithm ders, we have that ders(ar, s) is nullable, and that mkepsBC will extract the desired bits for decoding the correct value v for the matching, and v is a POSIX value. Now we prove that mkepsBC(ders\_simp(ar, s)) yields the same bitsequence.
+ − 275 \\
+ − 276 We first open up the ders\_simp function into nested alternating sequences of ders and simp.
+ − 277 Assume that s = $c_1...c_n$($n \geq 1$ ) where each of the $c_i$ are characters.
+ − 278 Then $ders\_simp(ar, s)$ = $s(d_{c_n}(...s(d_{c_1}(r))...))$ = $sdsd......sdr$. If we can prove that
9
+ − 279 $sdr \sim_{m\epsilon} dsr$ holds for any regular expression and any character, then we are done. This is because then we can push ders operation inside and move simp operation outside and have that $sdsd...sdr \sim_{m\epsilon} ssddsdsd...sdr \sim_{m\epsilon} ... \sim_{m\epsilon} s....sd....dr$.
+ − 280 Using \autoref{lma1} we have that $s...sd....dr = sd...dr$.
+ − 281 By \autoref{lma2}, we have $RHS \sim_{m\epsilon} d...dr$.\\
+ − 282 Notice that we don't actually need \autoref{lma1} here. That is because by \autoref{lma2}, we can have that $s...sd....dr \sim_{m\epsilon} sd...dr$. The equality above can be replaced by mkepsBC
+ − 283 equivalence without affecting the validity of the whole proof since all we want is mkepsBC equivalence, not equality.
+ − 284
+ − 285 Now we proceed to prove that $sdr \sim_{m\epsilon} dsr$. This can be reduced to proving $dr \sim_{m\epsilon} dsr$ as we know that $dr \sim_{m\epsilon} sdr$ by \autoref{lma2}.\\
8
+ − 286
+ − 287 we use an induction proof. Base cases are omitted. Here are the 3 inductive cases.
+ − 288 \begin{itemize}
+ − 289
10
+ − 290 \item{$r_1+r_2$}\\
8
+ − 291 The most difficult case is when $sr1$ and $sr2$ are both ALTS, so that they will be opened up in the flats function and some terms in sr2 might be deleted. Or otherwise we can use the argument that $d(r_1+r_2) = dr_1 + dr_2 \sim_{m\epsilon} dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$,
9
+ − 292 the last equivalence being established by \autoref{lma3}.
8
+ − 293 When $s(r_1), s(r_2)$ are both ALTS, we have to be more careful for the last equivalence step, namelly, $dsr_1 + dsr_2 \sim_{m\epsilon} ds(r_1+r_2)$. \\
9
+ − 294 We have that $LHS = dsr_1 + dsr_2 = d(sr_1 +sr_2)$. Since $sr_1 = ALTS(bs1, rs1)$ and $sr_2 = ALTS(bs2, rs2)$ we have $ d(sr_1 +sr_2 ) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2))$ by \autoref{lma4}.
+ − 295 On the other hand, $RHS = ds(ALTS(bs, r1, r2)) = d Co(bs, dB(flats(s(r1), s(r2)) ) ) = d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2))$ by definition of bsimp and flats.\\
+ − 296 $d Co(bs, dB(bs1>>rs1 ++ bs2>>rs2)) = d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1))) $ by \autoref{lma5}.\\ $d Co(bs, (bs1>>rs1 ++ ((bs2>>rs2)--rs1) )) = d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1))$ by \autoref{lma6}. \\
+ − 297 Using \autoref{lma8}, we have $d(ALTS(bs, bs1>>rs1 ++ (bs2>>rs2)--rs1)) \sim_{m\epsilon} d(ALTS(bs, bs1>>rs1 ++ bs2>>rs2)) \sim_{m\epsilon} RHS$.\\
+ − 298 %only the last part we don't have an equality here. We use mkeps equivalence instead because these two regexes are indeed different syntactically. However, they have even more in common than just mkeps equal. We might later augment this proof so that this equivalence relation is changed to something like regular expression equivalence.
8
+ − 299 This completes the proof.
+ − 300 \item{$r*$}\\
10
+ − 301 $s(r*) = r*$. Our goal is trivially achieved.
+ − 302 \item{$r1 \cdot r2$}\\
+ − 303 When r1 is nullable, $ds r1r2 = dsr1 \cdot sr2 + dsr2 \sim_{m\epsilon} dr1 \cdot sr2 + dr2 = dr1 \cdot r2 + dr2 $. The last step uses \autoref{lma10}.
+ − 304 When r1 is not nullable, $ds r1r2 = dsr1 \cdot sr2 \sim_{m\epsilon} dr1 \cdot sr2 \sim_{m\epsilon} dr1 \cdot r2 $
8
+ − 305
+ − 306 \end{itemize}
+ − 307 \item
+ − 308 Proof of second part of the theorem: use a similar structure of argument as in the first part.
10
+ − 309
+ − 310 \item
+ − 311 This proof has a major flaw: it assumes all dr is nullable along the path of deriving r by s. But it could be the case that $s\in L(r)$ but $ \exists s' \in Pref(s) \ s.t.\ ders(s', r)$ is not nullable (or equivalently, $s'\notin L(r)$). One remedy for this is to replace the mkepsBC equivalence relation into some other transitive relation that entails mkepsBC equivalence.
8
+ − 312 \end{itemize}
+ − 313 \end{proof}
+ − 314
10
+ − 315 \begin{theorem}{
+ − 316 This is a very strong claim that has yet to be more carefully examined and proved. However, experiments suggest a very good hope for this.}\\
+ − 317 Define pushbits as the following:\\
+ − 318 $pushbits(r) = if( r == ALTS(bs, rs) )\ then\ ALTS(Nil, rs.map(fuse(bs,\_))) \ else\ r$.\\
+ − 319 Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\
+ − 320 Unfortunately this does not hold. A counterexample is\\
+ − 321 \begin{verbatim}
+ − 322 r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),c), ACHAR(List(S),b))),ASEQ(List(),ASTAR(List(),ACHAR(List(),a)),AALTS(List(),List(ACHAR(List(Z),a), ACHAR(List(S),a))))))
+ − 323 regex after ders simp
+ − 324
+ − 325 SEQ
+ − 326 └-ALT List(S, S, C(b))
+ − 327 | └-SEQ
+ − 328 | | └-STA List(S, C(a), S, C(a))
+ − 329 | | | └-a
+ − 330 | | └-a List(Z)
+ − 331 | └-ONE List(S, C(a), Z, Z, C(a))
+ − 332 └-STA
+ − 333 └-SEQ
+ − 334 └-ALT
+ − 335 | └-c List(Z)
+ − 336 | └-b List(S)
+ − 337 └-SEQ
+ − 338 └-STA
+ − 339 | └-a
+ − 340 └-ALT
+ − 341 └-a List(Z)
+ − 342 └-a List(S)
+ − 343 regex after ders and then a single simp
+ − 344 SEQ
+ − 345 └-ALT List(S)
+ − 346 | └-SEQ List(S, C(b))
+ − 347 | | └-STA List(S, C(a), S, C(a))
+ − 348 | | | └-a
+ − 349 | | └-a List(Z)
+ − 350 | └-ONE List(S, C(b), S, C(a), Z, Z, C(a))
+ − 351 └-STA
+ − 352 └-SEQ
+ − 353 └-ALT
+ − 354 | └-c List(Z)
+ − 355 | └-b List(S)
+ − 356 └-SEQ
+ − 357 └-STA
+ − 358 | └-a
+ − 359 └-ALT
+ − 360 └-a List(Z)
+ − 361 └-a List(S)
+ − 362 \end{verbatim}
+ − 363 \end{theorem}
+ − 364
8
+ − 365 \end{document}
+ − 366
+ − 367 %The second part might still need some more development.
+ − 368 %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).\\
+ − 369 %By first part of proof, we have ders(ar, s1) $\sim_{m\epsilon}$ ders\_simp(ar, s1)
+ − 370 %.....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))
+ − 371 %So this path stuck here.