--- a/Paper/Paper.thy	Tue Feb 15 08:08:04 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 15 10:37:56 2011 +0000
@@ -667,10 +667,21 @@
   The first two ensure that the equational system is always finite (number of equations
   and number of terms in each equation); \ldots
 
+  It is straightforward to prove that the inital equational system satisfies the
+  invariant.
+
   \begin{lemma}
   @{thm[mode=IfThen] Init_ES_satisfies_invariant}
   \end{lemma}
 
+  \begin{proof}
+  Finiteness is given by the assumption and the way how we set up the 
+  initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
+  follows from the fact that the equivalence classes are disjoint. The ardenable
+  property also follows from the setup of the equational system as does 
+  validity.\qed
+  \end{proof}
+
   \begin{lemma}
   @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
   \end{lemma}
@@ -679,15 +690,54 @@
   @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
   \end{lemma}
 
+  \begin{proof}
+  By assumption we know that @{text "ES"} is finite and has more than one element.
+  Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with 
+  @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distictness property we can infer
+  that @{term "Y \<noteq> X"}. We further know that @{text "Remove ES Y yrhs"}
+  removes the equation @{text "Y = yrhs"} from the system, and therefore 
+  the cardinality of @{const Iter} strictly decreases.\qed
+  \end{proof}
+
   \begin{lemma}
   If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
   a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
   and @{term "invariant {(X, rhs)}"}.
   \end{lemma}
 
+  \begin{lemma}\label{every_eqcl_has_reg}
+  @{thm[mode=IfThen] every_eqcl_has_reg}
+  \end{lemma}
+
+  \begin{proof}
+  By the preceeding Lemma, we know that there exists a @{text "rhs"} such
+  that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
+  and that the invariant holds for this equation. That means we 
+  know @{text "X = \<Union>\<calL> ` rhs"}. We further know that
+  this is equal to @{text "\<Union>\<calL> ` (Arden X rhs)"} using ???.
+
+  \end{proof}
+
   \begin{theorem}
   @{thm[mode=IfThen] Myhill_Nerode1}
   \end{theorem}
+
+  \begin{proof}
+  By Lem.~\ref{every_eqcl_has_reg} we know that there exists a regular language for
+  every equivalence class in @{term "UNIV // \<approx>A"}. Since @{text "finals A"} is
+  a subset of  @{term "UNIV // \<approx>A"}, we also know that for every equvalence class
+  in @{term "finals A"} there exists a regular language. Moreover by assumption 
+  we know that @{term "finals A"} must be finite, therefore there must be a finite
+  set of regular expressions @{text "rs"} such that
+
+  \begin{center}
+  @{term "\<Union>(finals A) = L (\<Uplus>rs)"}
+  \end{center}
+
+  \noindent
+  Since the left-hand side is equal to @{text A}, we can use @{term "\<Uplus>rs"} 
+  as the regular expression that solves the goal.\qed
+  \end{proof}
 *}