--- a/Paper/Paper.thy	Mon Feb 14 11:12:01 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 14 23:10:44 2011 +0000
@@ -149,7 +149,7 @@
   requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98} 
   dismisses for this the option of using identities, because it leads according to 
   him to ``messy proofs''. He
-  opts for a variant of \eqref{disjointunion} using bitlists, but writes 
+  opts for a variant of \eqref{disjointunion} using bit lists, but writes 
 
   \begin{quote}
   \it%
@@ -482,7 +482,7 @@
 
   \noindent
   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 
+  to obtain this equation: it only holds with the marker, since none of 
   the other terms contain the empty string. 
 
   Our representation for the equations in Isabelle/HOL are pairs,
@@ -592,7 +592,7 @@
   expression. Therefore we define the iteration step so that it chooses an
   equation with an equivalence class that is not @{text X}. This allows us to 
   control, which equation will be the last. We use Hilbert's choice operator, 
-  written @{text SOME}, to chose an equation to be eliminated in @{text ES}.
+  written @{text SOME}, to choose an equation to be eliminated in @{text ES}.
   
   \begin{center}
   \begin{tabular}{rc@ {\hspace{4mm}}r@ {\hspace{1mm}}l}
@@ -603,22 +603,62 @@
   \end{center}
 
   \noindent
-  The last definition applies @{term Iter} over and over again a condition 
+  The last definition we need applies @{term Iter} over and over again until a condition 
   @{text COND} is \emph{not} satisfied anymore. The condition states that there
-  are more than one equation in the equational system @{text ES}. The 
-  iteration is defined in terms of HOL's @{text while}-operator as follows:
+  are more than one equation left in the equational system @{text ES}. For this
+  we use Isabelle/HOL's @{text while}-operator as follows:
   
   \begin{center}
   @{thm Solve_def}
   \end{center}
 
   \noindent
-  We are not concerned here with the definition of this operator in this paper
-  (see \cite{BerghoferNipkow00}).
+  We are not concerned here with the definition of this operator
+  (see \cite{BerghoferNipkow00}), but note that we eliminate
+  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:
+
 
   \begin{center}
-  @{thm while_rule}
+  \begin{tabular}{l}
+  @{term "invariant (Init (UNIV // \<approx>A))"} \\
+  @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> invariant (Iter X ES)"}\\
+  @{term "\<forall>ES. invariant ES \<and> Cond ES \<longrightarrow> card (Iter X ES) < card ES"}\\
+  @{term "\<forall>ES. invariant ES \<and> \<not> Cond ES \<longrightarrow> P ES"}\\
+  \hline
+  \multicolumn{1}{c}{@{term "P (Solve X (Init (UNIV // \<approx>A)))"}}
+  \end{tabular}
   \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
+  initial equational system satisfies the invariant; second that the iteration
+  step @{text "Iter"} preserves the the invariant as long as the condition @{term Cond};
+  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.
+
+  The property @{term P} we will show states 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
+
+  \begin{center}
+  \begin{tabular}{rcl@ {\hspace{10mm}}l}
+  @{text "invariant X 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>"} & @{thm (rhs) ardenable_def} & @{text "(ardenable)"}\\   
+  \end{tabular}
+  \end{center}
+ 
 *}