equal
deleted
inserted
replaced
2152 Higman's Lemma, which is already proved in the Isabelle/HOL library |
2152 Higman's Lemma, which is already proved in the Isabelle/HOL library |
2153 \cite{Berghofer03}.\footnote{Unfortunately, Berghofer's formalisation of Higman's Lemma |
2153 \cite{Berghofer03}.\footnote{Unfortunately, Berghofer's formalisation of Higman's Lemma |
2154 is restricted to 2-letter alphabets, |
2154 is restricted to 2-letter alphabets, |
2155 which means also our formalisation of Theorem~\ref{subseqreg} is `tainted' with |
2155 which means also our formalisation of Theorem~\ref{subseqreg} is `tainted' with |
2156 this constraint. However our methodology is applicable to any alphabet of finite size.} |
2156 this constraint. However our methodology is applicable to any alphabet of finite size.} |
2157 Higman's Lemma allows us to infer that every set @{text A} of antichains, satisfying |
2157 Higman's Lemma allows us to infer that every language @{text A} of antichains, satisfying |
2158 |
2158 |
2159 \begin{equation}\label{higman} |
2159 \begin{equation}\label{higman} |
2160 @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"} |
2160 @{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"} |
2161 \end{equation} |
2161 \end{equation} |
2162 |
2162 |