--- a/Myhill_1.thy	Tue Feb 15 10:37:56 2011 +0000
+++ b/Myhill_1.thy	Tue Feb 15 12:01:29 2011 +0000
@@ -1148,10 +1148,15 @@
     unfolding Solve_def by (rule while_rule)
 qed
 
-lemma last_cl_exists_rexp:
-  assumes Inv_ES: "invariant {(X, xrhs)}"
-  shows "\<exists>r::rexp. L r = X" 
-proof-
+lemma every_eqcl_has_reg:
+  assumes finite_CS: "finite (UNIV // \<approx>A)"
+  and X_in_CS: "X \<in> (UNIV // \<approx>A)"
+  shows "\<exists>r::rexp. X = L r" 
+proof -
+  from finite_CS X_in_CS 
+  obtain xrhs where Inv_ES: "invariant {(X, xrhs)}"
+    using Solve by metis
+
   def A \<equiv> "Arden X xrhs"
   have "rhss xrhs \<subseteq> {X}" using Inv_ES 
     unfolding valid_eqs_def invariant_def rhss_def lhss_def
@@ -1172,19 +1177,7 @@
     by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
   then have "X = L {Lam r | r. Lam r \<in> A}" using eq by simp
   then have "X = L (\<Uplus>{r. Lam r \<in> A})" using fin by auto
-  then show "\<exists>r::rexp. L r = X" by blast
-qed
-
-lemma every_eqcl_has_reg: 
-  assumes finite_CS: "finite (UNIV // \<approx>A)"
-  and X_in_CS: "X \<in> (UNIV // \<approx>A)"
-  shows "\<exists>r::rexp. L r = X"
-proof -
-  from finite_CS X_in_CS 
-  obtain xrhs where "invariant {(X, xrhs)}"
-    using Solve by metis
-  then show "\<exists>r::rexp. L r = X"
-    using last_cl_exists_rexp by auto
+  then show "\<exists>r::rexp. X = L r" by blast
 qed
 
 lemma bchoice_finite_set: