regexp: comparison Paper/Paper.thy

equal deleted inserted replaced

-:990c12ab1562
+:ea2e5acbfe4a
 \begin{equation}\label{inv2}
 @{text "X\<^isub>1 = \<calL>(Y\<^isub>1\<^isub>1, CHAR c\<^isub>1\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>1\<^isub>p, CHAR c\<^isub>1\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}.
 \end{equation}
 \noindent
-The reason for adding the @{text \<lambda>}-marker to our initial equational system is
+holds. The reason for adding the @{text \<lambda>}-marker to our initial equational system is
 to obtain this equation: it only holds with the marker, since none of
 the other terms contain the empty string. The point of the initial equational system is
 that solving it means we will be able to extract a regular expression for every equivalence class.
 Our representation for the equations in Isabelle/HOL are pairs,
 \end{tabular}
 \end{center}
 \noindent
 The first two ensure that the equational system is always finite (number of equations
-and number of terms in each equation); the second makes sure the `meaning' of the
+and number of terms in each equation); the third makes sure the `meaning' of the
 equations is preserved under our transformations. The other properties are a bit more
 technical, but are needed to get our proof through. Distinctness states that every
 equation in the system is distinct. @{text Ardenable} ensures that we can always
 apply the @{text Arden} operation.
 The last property states that every @{text rhs} can only contain equivalence classes
 section {* Myhill-Nerode, Second Part *}
 text {*
 We will prove in this section the second part of the Myhill-Nerode
-theorem. It can be formulated in our setting as follows.
+theorem. It can be formulated in our setting as follows:
 \begin{theorem}
 Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
 \end{theorem}

changeset 160	ea2e5acbfe4a
parent 159	990c12ab1562
child 162	e93760534354