equal
deleted
inserted
replaced
821 \begin{lemma}\label{every_eqcl_has_reg} |
821 \begin{lemma}\label{every_eqcl_has_reg} |
822 @{thm[mode=IfThen] every_eqcl_has_reg} |
822 @{thm[mode=IfThen] every_eqcl_has_reg} |
823 \end{lemma} |
823 \end{lemma} |
824 |
824 |
825 \begin{proof} |
825 \begin{proof} |
826 By the preceding Lemma, we know that there exists a @{text "rhs"} such |
826 By the preceding lemma, we know that there exists a @{text "rhs"} such |
827 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, |
827 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"}, |
828 and that the invariant holds for this equation. That means we |
828 and that the invariant holds for this equation. That means we |
829 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
829 know @{text "X = \<Union>\<calL> ` rhs"}. We further know that |
830 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the |
830 this is equal to \mbox{@{text "\<Union>\<calL> ` (Arden X rhs)"}} using the properties of the |
831 invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"}, |
831 invariant and Lem.~\ref{ardenable}. Using the validity property for the equation @{text "X = rhs"}, |
895 \noindent |
895 \noindent |
896 Much more interesting, however, are the inductive cases. They seem hard to be solved |
896 Much more interesting, however, are the inductive cases. They seem hard to be solved |
897 directly. The reader is invited to try. |
897 directly. The reader is invited to try. |
898 |
898 |
899 Our proof will rely on some |
899 Our proof will rely on some |
900 \emph{taggingfunctions} defined over strings. Given the inductive hypothesis, it will |
900 \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will |
901 be easy to prove that the \emph{range} of these tagging-functions is finite |
901 be easy to prove that the \emph{range} of these tagging-functions is finite |
902 (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}). |
902 (the range of a function @{text f} is defined as @{text "range f \<equiv> f ` UNIV"}). |
903 With this we will be able to infer that the tagging-functions, seen as relations, |
903 With this we will be able to infer that the tagging-functions, seen as relations, |
904 give rise to finitely many equivalence classes of @{const UNIV}. Finally we |
904 give rise to finitely many equivalence classes of @{const UNIV}. Finally we |
905 will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which |
905 will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which |
908 We formally define the notion of a \emph{tagging-relation} as follows. |
908 We formally define the notion of a \emph{tagging-relation} as follows. |
909 |
909 |
910 \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x} |
910 \begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x} |
911 and @{text y} are \emph{tag-related} provided |
911 and @{text y} are \emph{tag-related} provided |
912 \begin{center} |
912 \begin{center} |
913 @{text "x =tag= y \<equiv> tag x = tag y"} |
913 @{text "x =tag= y \<equiv> tag x = tag y"}. |
914 \end{center} |
914 \end{center} |
915 \end{definition} |
915 \end{definition} |
916 |
916 |
917 \noindent |
917 \noindent |
918 In order to establish finiteness of a set @{text A}, we shall use the following powerful |
918 In order to establish finiteness of a set @{text A}, we shall use the following powerful |