equal
deleted
inserted
replaced
2203 \end{tabular} |
2203 \end{tabular} |
2204 \end{center} |
2204 \end{center} |
2205 |
2205 |
2206 \noindent |
2206 \noindent |
2207 and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows |
2207 and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows |
2208 that @{term "SUBSEQ A"} is regular, provided @{text A} is. |
2208 that @{term "SUPSEQ A"} is regular, provided @{text A} is. |
2209 \end{proof} |
2209 \end{proof} |
2210 |
2210 |
2211 \noindent |
2211 \noindent |
2212 Now we can prove the main lemma w.r.t.~@{const "SUPSEQ"}, namely |
2212 Now we can prove the main lemma w.r.t.~@{const "SUPSEQ"}, namely |
2213 |
2213 |