--- a/Paper/Paper.thy	Mon Feb 14 23:10:44 2011 +0000
+++ b/Paper/Paper.thy	Tue Feb 15 08:08:04 2011 +0000
@@ -490,16 +490,16 @@
   is a set of terms. Given a set of equivalence
   classes @{text CS}, our initial equational system @{term "Init CS"} is thus 
   formally defined as
-
-  \begin{center}
-  \begin{tabular}{rcl}     
+  %
+  \begin{equation}\label{initcs}
+  \mbox{\begin{tabular}{rcl}     
   @{thm (lhs) Init_rhs_def} & @{text "\<equiv>"} & 
   @{text "if"}~@{term "[] \<in> X"}\\
   & & @{text "then"}~@{term "{Trn Y (CHAR c) | Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X} \<union> {Lam EMPTY}"}\\
   & & @{text "else"}~@{term "{Trn Y (CHAR c)| Y c. Y \<in> CS \<and> Y \<Turnstile>c\<Rightarrow> X}"}\\
   @{thm (lhs) Init_def}     & @{text "\<equiv>"} & @{thm (rhs) Init_def}
-  \end{tabular}
-  \end{center}
+  \end{tabular}}
+  \end{equation}
 
   
 
@@ -618,9 +618,10 @@
   in each @{const Iter}-step a single equation, and therefore 
   have a well-founded termination order by taking the cardinality 
   of the equational system @{text ES}. This enables us to prove
-  properties about our definition of @{const Solve} called with
-  our initial equational system @{term "Init (UNIV // \<approx>A)"} from ???
-  as follows:
+  properties about our definition of @{const Solve} when we ``call'' it with
+  the equivalence class @{text X} and the initial equational system 
+  @{term "Init (UNIV // \<approx>A)"} from
+  \eqref{initcs}:
 
 
   \begin{center}
@@ -635,30 +636,58 @@
   \end{center}
 
   \noindent
-  This principle states that given an invariant we can prove a property
-  @{text "P"} involving @{const Solve}. For this we have to first show that the
+  This principle states that given an invariant (which we will specify below) 
+  we can prove a property
+  @{text "P"} involving @{const Solve}. For this we have to discharge the following
+  proof obligations: first the
   initial equational system satisfies the invariant; second that the iteration
-  step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond};
+  step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond} holds;
   third that @{text "Iter"} decreases the termination order, and fourth that
-  once the condition does not hold for an invariant equational system @{text ES},
-  then the property must hold.
+  once the condition does not hold anymore then the property @{text P} must hold.
 
-  The property @{term P} we will show states that @{term "Solve X (Init (UNIV // \<approx>A))"}
+  The property @{term P} in our proof will state that @{term "Solve X (Init (UNIV // \<approx>A))"}
   returns with a single equation @{text "X = xrhs"}, for some @{text "xrhs"} and
-  that this equation satisfies also the invariant. The invariant is composed 
-  of several properties
+  that this equational system still satisfies the invariant. In order to get
+  the proof through, the invariant is composed of the following six properties:
 
   \begin{center}
-  \begin{tabular}{rcl@ {\hspace{10mm}}l}
-  @{text "invariant X ES"} & @{text "\<equiv>"} &
+  \begin{tabular}{@ {}rcl@ {\hspace{-13mm}}l @ {}}
+  @{text "invariant ES"} & @{text "\<equiv>"} &
       @{term "finite ES"} & @{text "(finiteness)"}\\
   & @{text "\<and>"} & @{thm (rhs) finite_rhs_def} & @{text "(finiteness rhs)"}\\
-  & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(validity)"}\\
-  & @{text "\<and>"} & @{thm (rhs) distinct_equas_def} & @{text "(distinctness)"}\\
+  & @{text "\<and>"} & @{text "\<forall>(X, rhs)\<in>ES. X = \<Union>\<calL> ` rhs"} & @{text "(soundness)"}\\
+  & @{text "\<and>"} & @{thm (rhs) distinct_equas_def}\\
+  &             &  & @{text "(distinctness)"}\\
   & @{text "\<and>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\   
+  & @{text "\<and>"} & @{thm (rhs) valid_eqs_def} & @{text "(validity)"}\\
   \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); \ldots
+
+  \begin{lemma}
+  @{thm[mode=IfThen] Init_ES_satisfies_invariant}
+  \end{lemma}
+
+  \begin{lemma}
+  @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
+  \end{lemma}
+
+  \begin{lemma}
+  @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
+  \end{lemma}
+
+  \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{theorem}
+  @{thm[mode=IfThen] Myhill_Nerode1}
+  \end{theorem}
 *}