# HG changeset patch
# User wu
# Date 1290080357 0
# Node ID e31b733ace44f4054380ea5d63c1999a585b2a1b
# Parent  0792821035b6c267e910660073ee61d91ee396cf
All cases of the Other direction finished

diff -r 0792821035b6 -r e31b733ace44 MyhillNerode.thy
--- a/MyhillNerode.thy	Wed Nov 10 11:59:29 2010 +0000
+++ b/MyhillNerode.thy	Thu Nov 18 11:39:17 2010 +0000
@@ -1,5 +1,5 @@
 theory MyhillNerode
-  imports "Main" 
+  imports "Main" "List_Prefix"
 begin
 
 text {* sequential composition of languages *}
@@ -281,8 +281,9 @@
 where
   "L1 Quo L2 \<equiv> { \<lbrakk>x\<rbrakk>L2 | x. x \<in> L1}" 
 
+
 lemma lang_eqs_union_of_eqcls: 
-  "Lang = (\<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)})"
+  "Lang = \<Union> {X. X \<in> (UNIV Quo Lang) \<and> (\<forall> x \<in> X. x \<in> Lang)}"
 proof
   show "Lang \<subseteq> \<Union>{X \<in> UNIV Quo Lang. \<forall>x\<in>X. x \<in> Lang}"
   proof
@@ -304,7 +305,6 @@
     by auto
 qed
 
-
 lemma empty_notin_CS: "{} \<notin> UNIV Quo Lang"
 apply (clarsimp simp:quot_def equiv_class_def)
 by (rule_tac x = x in exI, auto simp:equiv_str_def)
@@ -317,7 +317,7 @@
 definition 
   CT :: "string set \<Rightarrow> char \<Rightarrow> string set \<Rightarrow> bool" ("_-_\<rightarrow>_" [99,99]99)
 where
-  "X-c\<rightarrow>Y \<equiv> ( X; {[c]} \<subseteq> Y)"
+  "X-c\<rightarrow>Y \<equiv> ((X;{[c]}) \<subseteq> Y)"
 
 types t_equa_rhs = "(string set \<times> rexp) set"
 
@@ -345,7 +345,7 @@
   equation_rhs :: "(string set) set \<Rightarrow> string set \<Rightarrow> t_equa_rhs"
 where
   "equation_rhs CS X \<equiv> if (X = {[]}) then {({[]}, EMPTY)}
-    else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"
+                         else {(S, folds ALT NULL {CHAR c| c. S-c\<rightarrow>X} )| S. S \<in> CS} \<union> empty_rhs X"
 
 definition 
   equations :: "(string set) set \<Rightarrow> t_equas"
@@ -498,14 +498,14 @@
 qed
 
 text {* 
-  merge_rhs {(X1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = 
+  merge_rhs {(x1, r1), (x2, r2}, (x4, r4), \<dots>} {(x1, r1'), (x3, r3'), \<dots>} = 
      {(x1, ALT r1 r1'}, (x2, r2), (x3, r3'), (x4, r4), \<dots>} *}  
 definition 
   merge_rhs :: "t_equa_rhs \<Rightarrow> t_equa_rhs \<Rightarrow> t_equa_rhs"
 where
   "merge_rhs rhs rhs' \<equiv> {(X, r). (\<exists> r1 r2. ((X,r1) \<in> rhs \<and> (X, r2) \<in> rhs') \<and> r = ALT r1 r2)  \<or>
                                  (\<exists> r1. (X, r1) \<in> rhs \<and> (\<not> (\<exists> r2. (X, r2) \<in> rhs')) \<and> r = r1) \<or>
-                                 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"   
+                                 (\<exists> r2. (X, r2) \<in> rhs' \<and> (\<not> (\<exists> r1. (X, r1) \<in> rhs)) \<and> r = r2)    }"                                  
 
 
 text {* rhs_subst rhs X=xrhs r: substitude all occurence of X in rhs((X,r) \<in> rhs) with xrhs *}
@@ -631,8 +631,7 @@
 definition Inv :: "string set \<Rightarrow> t_equas \<Rightarrow> bool"
 where
   "Inv X ES \<equiv> finite ES \<and> (\<exists> rhs. (X, rhs) \<in> ES) \<and> distinct_equas ES \<and> 
-         (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs 
-              \<subseteq> insert {[]} (left_eq_cls ES))"
+            (\<forall> X xrhs. (X, xrhs) \<in> ES \<longrightarrow> ardenable (X, xrhs) \<and> X \<noteq> {} \<and> rhs_eq_cls xrhs \<subseteq> insert {[]} (left_eq_cls ES))"
 
 text {*
   TCon: Termination Condition of the equation-system decreasion.
@@ -644,14 +643,11 @@
 
 text {* 
   The following is a iteration principle, and is the main framework for the proof:
+   1: We can form the initial equation-system using "equations" defined above, and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";
+   2: We can decrease the number of the equation-system using ardens_lemma_revised and substitution ("equas_subst", defined above), 
+        and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"
+   and finally using property Inv and TCon to prove the myhill-nerode theorem
   
-   1: We can form the initial equation-system using "equations" defined above, 
-      and prove it has invariance Inv by lemma "init_ES_satisfy_Inv";
-   
-   2: We can decrease the number of the equation-system using ardens_lemma_revised 
-      and substitution ("equas_subst", defined above), 
-      and prove it holds the property "step" in "wf_iter" by lemma "iteration_step"
-      and finally using property Inv and TCon to prove the myhill-nerode theorem
 *}
 lemma wf_iter [rule_format]: 
   fixes f
@@ -806,8 +802,7 @@
   "(X, xrhs) \<in> equations CS \<Longrightarrow> no_EMPTY_rhs xrhs"
 apply (clarsimp simp add:equations_def equation_rhs_def)
 apply (simp add:no_EMPTY_rhs_def empty_rhs_def, auto)
-apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}",
-  drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+
+apply (subgoal_tac "finite {CHAR c |c. Xa-c\<rightarrow>X}", drule_tac x = "[]" in fold_alt_null_eqs, clarsimp, rule finite_charset_rS)+
 done
 
 lemma init_ES_satisfy_ardenable:
@@ -894,8 +889,7 @@
 lemma ardenable_prop:
   assumes not_lambda: "Y \<noteq> {[]}"
   and ardable: "ardenable (Y, yrhs)"
-  shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" 
-    (is "\<exists> yrhs'. ?P yrhs'")
+  shows "\<exists> yrhs'. Y = L yrhs' \<and> distinct_rhs yrhs' \<and> rhs_eq_cls yrhs' = rhs_eq_cls yrhs - {Y}" (is "\<exists> yrhs'. ?P yrhs'")
 proof (cases "(\<exists> reg. (Y, reg) \<in> yrhs)")
   case True
   thus ?thesis 
@@ -1312,59 +1306,26 @@
 
 text {* tests by Christian *}
 
-lemma temp_set_ext[no_atp]: "(\<And>x. (x:A) = (x:B)) \<Longrightarrow> (A = B)"
-by(auto intro:set_eqI)
-
-fun
-  MNRel
-where
-  "MNRel Lang (x, y) = (x \<equiv>Lang\<equiv> y)"
-
-lemma
-  "equiv UNIV (MNRel Lang)"
-unfolding equiv_def
-unfolding refl_on_def sym_def trans_def
-apply(auto simp add: mem_def equiv_str_def)
-done
-
-lemma
-  "(MNRel Lang)``{x} = \<lbrakk>x\<rbrakk>Lang"
-unfolding equiv_class_def Image_def mem_def
-by (simp)
-
-lemma tt: "\<lbrakk>A = B; C \<subseteq> B\<rbrakk> \<Longrightarrow> C \<subseteq> A" by simp 
-
-lemma
-  "UNIV//(MNRel (L1 \<union> L2)) \<subseteq> (UNIV//(MNRel L1)) \<union> (UNIV//(MNRel L2))"
-unfolding quotient_def
-unfolding UNION_eq_Union_image
-apply(rule tt)
-apply(rule Un_Union_image[symmetric])
-apply(simp)
-apply(rule UN_mono)
-apply(simp)
-apply(simp)
-unfolding Image_def
-unfolding mem_def
-unfolding MNRel.simps
-apply(simp)
-oops
-
-
-
-text {* Alternative definition for Quo *}
+(* Alternative definition for Quo *)
 definition 
   QUOT :: "string set \<Rightarrow> (string set) set"  
 where
   "QUOT Lang \<equiv> (\<Union>x. {\<lbrakk>x\<rbrakk>Lang})"
 
-lemma test_01:
-  "Lang \<subseteq> (\<Union> QUOT Lang)"
-unfolding QUOT_def equiv_class_def equiv_str_def
-by (blast)
+lemma test: 
+  "UNIV Quo Lang = QUOT Lang"
+by (auto simp add: quot_def QUOT_def)
 
+lemma test1:
+  assumes finite_CS: "finite (QUOT Lang)"
+  shows "reg Lang"
+using finite_CS
+unfolding test[symmetric]
+by (auto dest: myhill_nerode)
 
-(* by chunhan *)
+lemma cons_one: "x @ y \<in> {z} \<Longrightarrow> x @ y = z"
+by simp
+
 lemma quot_lambda: "QUOT {[]} = {{[]}, UNIV - {[]}}"
 proof 
   show "QUOT {[]} \<subseteq> {{[]}, UNIV - {[]}}"
@@ -1446,7 +1407,7 @@
             proof -
               have "xa = [c] \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = {[c]}" using in_eqiv
                 apply (simp add:equiv_str_def)
-                apply (rule temp_set_ext, rule iffI, simp)
+                apply (rule set_ext, rule iffI, simp)
                 apply (drule_tac x = "[]" in spec, auto)
                 done   
               thus "xa = [c] \<Longrightarrow> x = {[c]}" using in_eqiv by simp 
@@ -1455,7 +1416,7 @@
             proof -
               have "\<lbrakk>xa \<noteq> []; xa \<noteq> [c]\<rbrakk> \<Longrightarrow> {y. xa \<equiv>{[c]}\<equiv> y} = UNIV - {[],[c]}" 
                 apply (clarsimp simp add:equiv_str_def)
-                apply (rule temp_set_ext, rule iffI, simp)
+                apply (rule set_ext, rule iffI, simp)
                 apply (rule conjI)
                 apply (drule_tac x = "[c]" in spec, simp)
                 apply (drule_tac x = "[]" in spec, simp)
@@ -1481,13 +1442,13 @@
         moreover have "x = {[c]} \<Longrightarrow> x \<in> QUOT {[c]}"
           apply (simp add:QUOT_def equiv_class_def equiv_str_def)
           apply (rule_tac x = "[c]" in exI, simp)
-          apply (rule temp_set_ext, rule iffI, simp+)
+          apply (rule set_ext, rule iffI, simp+)
           by (drule_tac x = "[]" in spec, simp)
         moreover have "x = UNIV - {[],[c]} \<Longrightarrow> x \<in> QUOT {[c]}"
           using exist_another
           apply (clarsimp simp add:QUOT_def equiv_class_def equiv_str_def)        
           apply (rule_tac x = "[a]" in exI, simp)
-          apply (rule temp_set_ext, rule iffI, simp)
+          apply (rule set_ext, rule iffI, simp)
           apply (clarsimp simp:quot_single_aux, simp)
           apply (rule conjI)
           apply (drule_tac x = "[c]" in spec, simp)
@@ -1498,53 +1459,18 @@
   qed
 qed
 
-lemma quot_seq: 
-  assumes finite1: "finite (QUOT L\<^isub>1)"
-  and finite2: "finite (QUOT L\<^isub>2)"
-  shows "finite (QUOT (L\<^isub>1;L\<^isub>2))"
-apply (simp add:QUOT_def equiv_class_def equiv_str_def)
-sorry
- 
-
-lemma a:
-  "\<lbrakk>x \<equiv>L1\<equiv> y \<and> x \<equiv>L2\<equiv> y\<rbrakk> \<Longrightarrow> x \<equiv>(L1 \<union> L2)\<equiv> y"
-apply(simp add: equiv_str_def)
-done
-
-
-(*
-lemma quot_star:  
-  assumes finite1: "finite (QUOT L\<^isub>1)"
-  shows "finite (QUOT (L\<^isub>1\<star>))"
-sorry
-
-
-lemma other_direction:
-  "Lang = L (r::rexp) \<Longrightarrow> finite (QUOT Lang)"
-apply (induct arbitrary:Lang rule:rexp.induct)
-apply (simp add:QUOT_def equiv_class_def equiv_str_def)
-by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)  
-
-lemma test: 
-  "UNIV Quo Lang = QUOT Lang"
-by (auto simp add: quot_def QUOT_def)
-*)
-
-
-(* by chunhan *)
-
+lemma eq_class_imp_eq_str:
+  "\<lbrakk>x\<rbrakk>lang = \<lbrakk>y\<rbrakk>lang \<Longrightarrow> x \<equiv>lang\<equiv> y"
+by (auto simp:equiv_class_def equiv_str_def)
 
 lemma finite_tag_image: 
   "finite (range tag) \<Longrightarrow> finite (((op `) tag) ` S)"
 apply (rule_tac B = "Pow (tag ` UNIV)" in finite_subset)
 by (auto simp add:image_def Pow_def)
 
-term image
-term "(op `) tag"
-
 lemma str_inj_imps:
   assumes str_inj: "\<And> m n. tag m = tag (n::string) \<Longrightarrow> m \<equiv>lang\<equiv> n"
-  shows "inj_on (image tag) (QUOT lang)"
+  shows "inj_on ((op `) tag) (QUOT lang)"
 proof (clarsimp simp add:inj_on_def QUOT_def)
   fix x y
   assume eq_tag: "tag ` \<lbrakk>x\<rbrakk>lang = tag ` \<lbrakk>y\<rbrakk>lang"
@@ -1563,24 +1489,17 @@
   qed
 qed
 
-definition 
-  tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
+definition tag_str_ALT :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
 where
   "tag_str_ALT L\<^isub>1 L\<^isub>2 x \<equiv> (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)"
 
-lemma
-  "{(\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2) | x. True} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"
-unfolding QUOT_def
-by (auto)
-
 lemma tag_str_alt_range_finite:
   assumes finite1: "finite (QUOT L\<^isub>1)"
   and finite2: "finite (QUOT L\<^isub>2)"
   shows "finite (range (tag_str_ALT L\<^isub>1 L\<^isub>2))"
 proof -
   have "{y. \<exists>x. y = (\<lbrakk>x\<rbrakk>L\<^isub>1, \<lbrakk>x\<rbrakk>L\<^isub>2)} \<subseteq> (QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"
-    unfolding QUOT_def
-    by auto
+    by (auto simp:QUOT_def)
   thus ?thesis using finite1 finite2
     by (auto simp: image_def tag_str_ALT_def UNION_def 
             intro: finite_subset[where B = "(QUOT L\<^isub>1) \<times> (QUOT L\<^isub>2)"])
@@ -1595,111 +1514,16 @@
   assumes finite1: "finite (QUOT L\<^isub>1)"
   and finite2: "finite (QUOT L\<^isub>2)"
   shows "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
-proof -
-  have "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+proof (rule_tac f = "(op `) (tag_str_ALT L\<^isub>1 L\<^isub>2)" in finite_imageD)
+  show "finite (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2) ` QUOT (L\<^isub>1 \<union> L\<^isub>2))"
     using finite_tag_image tag_str_alt_range_finite finite1 finite2
     by auto
-  moreover 
-  have "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
+next
+  show "inj_on (op ` (tag_str_ALT L\<^isub>1 L\<^isub>2)) (QUOT (L\<^isub>1 \<union> L\<^isub>2))"
     apply (rule_tac str_inj_imps)
     by (erule_tac tag_str_alt_inj)
-  ultimately 
-  show "finite (QUOT (L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
 qed
 
-
-(*by cu *)
-
-
-definition
-  str_eq ("_ \<approx>_ _")
-where
-  "x \<approx>Lang y \<equiv> (\<forall>z. x @ z \<in> Lang \<longleftrightarrow> y @ z \<in> Lang)"
-
-definition
-  str_eq_rel ("\<approx>_")
-where
-  "\<approx>Lang \<equiv> {(x, y). x \<approx>Lang y}"
-
-lemma [simp]:
-  "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
-by simp
-
-lemma inj_image_lang:
-  fixes f::"string \<Rightarrow> 'a"
-  assumes str_inj: "\<And>x y. f x = f y \<Longrightarrow> x \<approx>Lang y"
-  shows "inj_on (image f) (UNIV // (\<approx>Lang))"
-proof - 
-  { fix x y::string
-    assume eq_tag: "f ` {z. x \<approx>Lang z} = f ` {z. y \<approx>Lang z}"
-    moreover
-    have "{z. x \<approx>Lang z} \<noteq> {}" unfolding str_eq_def by auto
-    ultimately obtain a b where "x \<approx>Lang a" "y \<approx>Lang b" "f a = f b" by blast
-    then have "x \<approx>Lang a" "y \<approx>Lang b" "a \<approx>Lang b" using str_inj by auto
-    then have "x \<approx>Lang y" unfolding str_eq_def by simp 
-    then have "{z. x \<approx>Lang z} = {z. y \<approx>Lang z}" unfolding str_eq_def by simp
-  }
-  then have "\<forall>x\<in>UNIV // \<approx>Lang. \<forall>y\<in>UNIV // \<approx>Lang. f ` x = f ` y \<longrightarrow> x = y"
-    unfolding quotient_def Image_def str_eq_rel_def by simp
-  then show "inj_on (image f) (UNIV // (\<approx>Lang))"
-    unfolding inj_on_def by simp
-qed
-
-
-lemma finite_range_image: 
-  assumes fin: "finite (range f)"
-  shows "finite ((image f) ` X)"
-proof -
-  from fin have "finite (Pow (f ` UNIV))" by auto
-  moreover
-  have "(image f) ` X \<subseteq> Pow (f ` UNIV)" by auto
-  ultimately show "finite ((image f) ` X)" using finite_subset by auto
-qed
-
-definition 
-  tag1 :: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set)"
-where
-  "tag1 L\<^isub>1 L\<^isub>2 \<equiv> \<lambda>x. ((\<approx>L\<^isub>1) `` {x}, (\<approx>L\<^isub>2) `` {x})"
-
-lemma tag1_range_finite:
-  assumes finite1: "finite (UNIV // \<approx>L\<^isub>1)"
-  and finite2: "finite (UNIV // \<approx>L\<^isub>2)"
-  shows "finite (range (tag1 L\<^isub>1 L\<^isub>2))"
-proof -
-  have "finite (UNIV // \<approx>L\<^isub>1 \<times> UNIV // \<approx>L\<^isub>2)" using finite1 finite2 by auto
-  moreover
-  have "range (tag1 L\<^isub>1 L\<^isub>2) \<subseteq> (UNIV // \<approx>L\<^isub>1) \<times> (UNIV // \<approx>L\<^isub>2)"
-    unfolding tag1_def quotient_def by auto
-  ultimately show "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 
-    using finite_subset by blast
-qed
-
-lemma tag1_inj:
-  "tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y"
-unfolding tag1_def Image_def str_eq_rel_def str_eq_def
-by auto
-
-lemma quot_alt_cu:
-  fixes L\<^isub>1 L\<^isub>2::"string set"
-  assumes fin1: "finite (UNIV // \<approx>L\<^isub>1)"
-  and fin2: "finite (UNIV // \<approx>L\<^isub>2)"
-  shows "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))"
-proof -
-  have "finite (range (tag1 L\<^isub>1 L\<^isub>2))" 
-    using fin1 fin2 tag1_range_finite by simp
-  then have "finite (image (tag1 L\<^isub>1 L\<^isub>2) ` (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2)))" 
-    using finite_range_image by blast
-  moreover 
-  have "\<And>x y. tag1 L\<^isub>1 L\<^isub>2 x = tag1 L\<^isub>1 L\<^isub>2 y \<Longrightarrow> x \<approx>(L\<^isub>1 \<union> L\<^isub>2) y" 
-    using tag1_inj by simp
-  then have "inj_on (image (tag1 L\<^isub>1 L\<^isub>2)) (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" 
-    using inj_image_lang by blast
-  ultimately 
-  show "finite (UNIV // \<approx>(L\<^isub>1 \<union> L\<^isub>2))" by (rule finite_imageD)
-qed
-
-(* by chunhan *)
-
 (* list_diff:: list substract, once different return tailer *)
 fun list_diff :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "-" 51)
 where
@@ -1707,76 +1531,108 @@
   "list_diff (x#xs) [] = x#xs" |
   "list_diff (x#xs) (y#ys) = (if x = y then list_diff xs ys else (x#xs))"
 
-definition tag_str_SEQ:: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set) set"
+lemma [simp]: "(x @ y) - x = y"
+apply (induct x)
+by (case_tac y, simp+)
+
+lemma [simp]: "x - x = []"
+by (induct x, auto)
+
+lemma [simp]: "x = xa @ y \<Longrightarrow> x - xa = y "
+by (induct x, auto)
+
+lemma [simp]: "x - [] = x"
+by (induct x, auto)
+
+lemma [simp]: "xa \<le> x \<Longrightarrow> (x @ y) - xa = (x - xa) @ y"
+by (auto elim:prefixE)
+
+definition tag_str_SEQ:: "string set \<Rightarrow> string set \<Rightarrow> string \<Rightarrow> (string set \<times> string set set)"
 where
-  "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> if (\<exists> y. y \<le> x \<and> y \<in> L\<^isub>1)
-                         then {(\<lbrakk>(x - y)\<rbrakk>L\<^isub>2) | y.  y \<le> x \<and> y \<in> L\<^isub>1}
-                         else { \<lbrakk>x\<rbrakk>L\<^isub>1 }"
+  "tag_str_SEQ L\<^isub>1 L\<^isub>2 x \<equiv> if (\<exists> xa \<le> x. xa \<in> L\<^isub>1)
+                         then (\<lbrakk>x\<rbrakk>L\<^isub>1, {\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 | xa.  xa \<le> x \<and> xa \<in> L\<^isub>1})
+                         else (\<lbrakk>x\<rbrakk>L\<^isub>1, {})"
+
+lemma tag_seq_eq_E:
+  "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y \<Longrightarrow>
+   ((\<exists> xa \<le> x. xa \<in> L\<^isub>1) \<and> \<lbrakk>x\<rbrakk>L\<^isub>1 = \<lbrakk>y\<rbrakk>L\<^isub>1 \<and> 
+    {\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 | xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = {\<lbrakk>(y - ya)\<rbrakk>L\<^isub>2 | ya. ya \<le> y \<and> ya \<in> L\<^isub>1} ) \<or>
+   ((\<forall> xa \<le> x. xa \<notin> L\<^isub>1) \<and> \<lbrakk>x\<rbrakk>L\<^isub>1 = \<lbrakk>y\<rbrakk>L\<^isub>1)"
+by (simp add:tag_str_SEQ_def split:if_splits, blast)
 
 lemma tag_str_seq_range_finite:
   assumes finite1: "finite (QUOT L\<^isub>1)"
   and finite2: "finite (QUOT L\<^isub>2)"
   shows "finite (range (tag_str_SEQ L\<^isub>1 L\<^isub>2))"
 proof -
-  have "(range (tag_str_SEQ L\<^isub>1 L\<^isub>2)) \<subseteq> Pow ((QUOT L\<^isub>1) \<union> (QUOT L\<^isub>2))"
+  have "(range (tag_str_SEQ L\<^isub>1 L\<^isub>2)) \<subseteq> (QUOT L\<^isub>1) \<times> (Pow (QUOT L\<^isub>2))"
     by (auto simp:image_def tag_str_SEQ_def QUOT_def)
   thus ?thesis using finite1 finite2 
-    by (rule_tac B = "Pow ((QUOT L\<^isub>1) \<union> (QUOT L\<^isub>2))" in finite_subset, auto)
+    by (rule_tac B = "(QUOT L\<^isub>1) \<times> (Pow (QUOT L\<^isub>2))" in finite_subset, auto)
 qed
   
+lemma app_in_seq_decom[rule_format]:
+  "\<forall> x. x @ z \<in> L\<^isub>1 ; L\<^isub>2 \<longrightarrow> (\<exists> xa \<le> x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2) \<or> 
+                            (\<exists> za \<le> z. (x @ za) \<in> L\<^isub>1 \<and> (z - za) \<in> L\<^isub>2)"
+apply (induct z)
+apply (simp, rule allI, rule impI, rule disjI1)
+apply (clarsimp simp add:lang_seq_def)
+apply (rule_tac x = s1 in exI, simp)
+apply (rule allI | rule impI)+
+apply (drule_tac x = "x @ [a]" in spec, simp)
+apply (erule exE | erule conjE | erule disjE)+
+apply (rule disjI2, rule_tac x = "[a]" in exI, simp)
+apply (rule disjI1, rule_tac x = xa in exI, simp) 
+apply (erule exE | erule conjE)+
+apply (rule disjI2, rule_tac x = "a # za" in exI, simp)
+done
+
 lemma tag_str_seq_inj:
   assumes tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
   shows "(x::string) \<equiv>(L\<^isub>1 ; L\<^isub>2)\<equiv> y"
-proof (cases "\<exists> xa. xa \<le> x \<and> xa \<in> L\<^isub>1")
-  have equiv_str_sym: "\<And> x y lang. (x::string) \<equiv>lang\<equiv> y \<Longrightarrow> y \<equiv>lang\<equiv> x"
-    by (auto simp:equiv_str_def)
-  have set_equ_D: "\<And> A a B b. \<lbrakk>A = B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> a b. a \<in> A \<and> b \<in> B \<and> a = b " by auto
-  have eqset_equ_D: "\<And> x y lang. {y. x \<equiv>lang\<equiv> y} = {ya. y \<equiv>lang\<equiv> ya} \<Longrightarrow> x \<equiv>lang\<equiv> y"
-    by (drule set_equ_D, auto simp:equiv_str_def)
-  assume  x_left_l1: "\<exists>xa\<le>x. xa \<in> L\<^isub>1"
-  show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
-  proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1")
-    assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1"
-    with tag_eq x_left_l1
-    show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
-      apply (simp add:tag_str_SEQ_def)
-      apply (drule set_equ_D)
-      apply (auto simp:equiv_class_def equiv_str_def)[1]
-      apply (clarsimp simp:equiv_str_def)
-      apply (rule iffI)
-      apply  
-      apply (
+proof -
+  have aux: "\<And> x y z. \<lbrakk>tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y; x @ z \<in> L\<^isub>1 ; L\<^isub>2\<rbrakk> 
+                       \<Longrightarrow> y @ z \<in> L\<^isub>1 ; L\<^isub>2"
+  proof (drule app_in_seq_decom, erule disjE)
+    fix x y z
+    assume tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
+      and x_gets_l2: "\<exists>xa\<le>x. xa \<in> L\<^isub>1 \<and> (x - xa) @ z \<in> L\<^isub>2"
+    from x_gets_l2 have "\<exists> xa \<le> x. xa \<in> L\<^isub>1" by blast
+    hence xy_l2:"{\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 | xa. xa \<le> x \<and> xa \<in> L\<^isub>1} = {\<lbrakk>(y - ya)\<rbrakk>L\<^isub>2 | ya. ya \<le> y \<and> ya \<in> L\<^isub>1}"
+      using tag_eq tag_seq_eq_E by blast
+    from x_gets_l2 obtain xa where xa_le_x: "xa \<le> x"
+                               and xa_in_l1: "xa \<in> L\<^isub>1"
+                               and rest_in_l2: "(x - xa) @ z \<in> L\<^isub>2" by blast
+    hence "\<exists> ya. \<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 = \<lbrakk>(y - ya)\<rbrakk>L\<^isub>2 \<and> ya \<le> y \<and> ya \<in> L\<^isub>1" using xy_l2 by auto
+    then obtain ya where ya_le_x: "ya \<le> y"
+                     and ya_in_l1: "ya \<in> L\<^isub>1"
+                     and rest_eq: "\<lbrakk>(x - xa)\<rbrakk>L\<^isub>2 = \<lbrakk>(y - ya)\<rbrakk>L\<^isub>2" by blast
+    from rest_eq rest_in_l2 have "(y - ya) @ z \<in> L\<^isub>2" 
+      by (auto simp:equiv_class_def equiv_str_def)
+    hence "ya @ ((y - ya) @ z) \<in> L\<^isub>1 ; L\<^isub>2" using ya_in_l1
+      by (auto simp:lang_seq_def)
+    thus "y @ z \<in> L\<^isub>1 ; L\<^isub>2" using ya_le_x 
+      by (erule_tac prefixE, simp)
   next
-    assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)"
-    show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
-      sorry
+    fix x y z
+    assume tag_eq: "tag_str_SEQ L\<^isub>1 L\<^isub>2 x = tag_str_SEQ L\<^isub>1 L\<^isub>2 y"
+      and x_gets_l1: "\<exists>za\<le>z. x @ za \<in> L\<^isub>1 \<and> z - za \<in> L\<^isub>2"
+    from tag_eq tag_seq_eq_E have x_y_eq: "\<lbrakk>x\<rbrakk>L\<^isub>1 = \<lbrakk>y\<rbrakk>L\<^isub>1" by blast
+    from x_gets_l1 obtain za where za_le_z: "za \<le> z"
+                               and x_za_in_l1: "(x @ za) \<in> L\<^isub>1"
+                               and rest_in_l2: "z - za \<in> L\<^isub>2" by blast
+    from x_y_eq x_za_in_l1 have y_za_in_l1: "y @ za \<in> L\<^isub>1"
+      by (auto simp:equiv_class_def equiv_str_def)
+    hence "(y @ za) @ (z - za) \<in> L\<^isub>1 ; L\<^isub>2" using rest_in_l2
+      apply (simp add:lang_seq_def)
+      by (rule_tac x = "y @ za" in exI, rule_tac x = "z - za" in exI, simp)
+    thus "y @ z \<in> L\<^isub>1 ; L\<^isub>2" using za_le_z
+      by (erule_tac prefixE, simp)
   qed
-next
-  assume x_in_l1: "\<not> (\<exists>xa\<le>x. xa \<in> L\<^isub>1)"
-  show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
-  proof (cases "\<exists> ya. ya \<le> y \<and> ya \<in> L\<^isub>1")
-    assume y_left_l1: "\<exists>ya\<le>y. ya \<in> L\<^isub>1"
-    show "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
-      sorry
-  next
-    assume y_in_l1: "\<not> (\<exists>ya\<le>y. ya \<in> L\<^isub>1)"
-    with tag_eq x_in_l1
-    have "\<lbrakk>x\<rbrakk>(L\<^isub>1;L\<^isub>2) = \<lbrakk>y\<rbrakk>(L\<^isub>1;L\<^isub>2)"
-      sorry
-    thus "x \<equiv>L\<^isub>1 ; L\<^isub>2\<equiv> y"
-      by (auto simp:equiv_class_def equiv_str_def)
-  qed
+  show ?thesis using tag_eq
+    apply (simp add:equiv_str_def)
+    by (auto intro:aux)
 qed
-  
-apply (simp add:tag_str_SEQ_def split:if_splits)
-prefer 4
-apply (clarsimp simp add:equiv_str_def)
-apply (rule iffI)
-apply (simp add:lang_seq_def equiv_class_def equiv_str_def)
-apply blast
-apply (
-sorry
-
 
 lemma quot_seq: 
   assumes finite1: "finite (QUOT L\<^isub>1)"
@@ -1792,9 +1648,20 @@
     by (erule_tac tag_str_seq_inj)
 qed
 
-definition tag_str_STAR:: "string set \<Rightarrow> string \<Rightarrow> (string set) set"
+(****************** the STAR case ************************)
+
+lemma app_eq_elim[rule_format]:
+  "\<And> a. \<forall> b x y. a @ b = x @ y \<longrightarrow> (\<exists> aa ab. a = aa @ ab \<and> x = aa \<and> y = ab @ b) \<or>
+                                   (\<exists> ba bb. b = ba @ bb \<and> x = a @ ba \<and> y = bb \<and> ba \<noteq> [])"
+  apply (induct_tac a rule:List.induct, simp)
+  apply (rule allI | rule impI)+
+  by (case_tac x, auto)
+
+definition tag_str_STAR:: "string set \<Rightarrow> string \<Rightarrow> string set set"
 where
-  "tag_str_STAR L\<^isub>1 x = {\<lbrakk>y\<rbrakk>L\<^isub>1 | y. y \<le> x}"
+  "tag_str_STAR L\<^isub>1 x \<equiv> if (x = []) 
+                       then {}
+                       else {\<lbrakk>x\<^isub>2\<rbrakk>L\<^isub>1 | x\<^isub>1 x\<^isub>2. x =  x\<^isub>1 @ x\<^isub>2 \<and> x\<^isub>1 \<in> L\<^isub>1\<star> \<and> x\<^isub>2 \<noteq> []}"
 
 lemma tag_str_star_range_finite:
   assumes finite1: "finite (QUOT L\<^isub>1)"
@@ -1806,52 +1673,126 @@
     by (rule_tac B = "Pow (QUOT L\<^isub>1)" in finite_subset, auto)
 qed
 
+lemma star_prop[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall> y. y \<in> lang\<star> \<longrightarrow> x @ y \<in> lang\<star>"
+by (erule Star.induct, auto)
+
+lemma star_prop2: "y \<in> lang \<Longrightarrow> y \<in> lang\<star>"
+by (drule step[of y lang "[]"], auto simp:start)
+
+lemma star_prop3[rule_format]: "x \<in> lang\<star> \<Longrightarrow> \<forall>y . y \<in> lang \<longrightarrow> x @ y \<in> lang\<star>"
+by (erule Star.induct, auto intro:star_prop2)
+
+lemma postfix_prop: "y >>= (x @ y) \<Longrightarrow> x = []"
+by (erule postfixE, induct x arbitrary:y, auto)
+
+lemma inj_aux:
+  "\<lbrakk>(m @ z) \<in> L\<^isub>1\<star>; m \<equiv>L\<^isub>1\<equiv> yb; xa @ m = x; xa \<in> L\<^isub>1\<star>; m \<noteq> [];
+    \<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= m\<rbrakk> 
+  \<Longrightarrow> (yb @ z) \<in> L\<^isub>1\<star>"
+proof- 
+  have "\<And>s. s \<in> L\<^isub>1\<star> \<Longrightarrow> \<forall> m z yb. (s = m @ z \<and> m \<equiv>L\<^isub>1\<equiv> yb \<and> x = xa @ m \<and> xa \<in> L\<^isub>1\<star> \<and> m \<noteq> [] \<and>  
+    (\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= m) \<longrightarrow> (yb @ z) \<in> L\<^isub>1\<star>)"    
+    apply (erule Star.induct, simp)
+    apply (rule allI | rule impI | erule conjE)+
+    apply (drule app_eq_elim)
+    apply (erule disjE | erule exE | erule conjE)+
+    apply simp
+    apply (simp (no_asm) only:append_assoc[THEN sym])
+    apply (rule step) 
+    apply (simp add:equiv_str_def)
+    apply simp
+
+    apply (erule exE | erule conjE)+    
+    apply (rotate_tac 3)
+    apply (frule_tac x = "xa @ s1" in spec)
+    apply (rotate_tac 12)
+    apply (drule_tac x = ba in spec)
+    apply (erule impE)
+    apply ( simp add:star_prop3)
+    apply (simp)
+    apply (drule postfix_prop)
+    apply simp
+    done
+  thus "\<lbrakk>(m @ z) \<in> L\<^isub>1\<star>; m \<equiv>L\<^isub>1\<equiv> yb; xa @ m = x; xa \<in> L\<^isub>1\<star>; m \<noteq> [];
+         \<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= m\<rbrakk> 
+        \<Longrightarrow> (yb @ z) \<in> L\<^isub>1\<star>" by blast
+qed
+
+
+lemma min_postfix_exists[rule_format]:
+  "finite A \<Longrightarrow> A \<noteq> {} \<and> (\<forall> a \<in> A. \<forall> b \<in> A. ((b >>= a) \<or> (a >>= b))) 
+                \<longrightarrow> (\<exists> min. (min \<in> A \<and> (\<forall> a \<in> A. a >>= min)))"
+apply (erule finite.induct)
+apply simp
+apply simp
+apply (case_tac "A = {}")
+apply simp
+apply clarsimp
+apply (case_tac "a >>= min")
+apply (rule_tac x = min in exI, simp)
+apply (rule_tac x = a in exI, simp)
+apply clarify
+apply (rotate_tac 5)
+apply (erule_tac x = aa in ballE) defer apply simp
+apply (erule_tac ys = min in postfix_trans)
+apply (erule_tac x = min in ballE) 
+by simp+
+
 lemma tag_str_star_inj:
   "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 (y::string) \<Longrightarrow> x \<equiv>L\<^isub>1\<star>\<equiv> y"
 proof -
-  have "\<forall> x lang. (x = []) = (tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang})"
-  proof (rule_tac allI, rule_tac allI, rule_tac iffI)
-    fix x lang
-    show "x = [] \<Longrightarrow> tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang}" 
-      by (simp add:tag_str_STAR_def)
-  next    
-    fix x lang
-    show "tag_str_STAR lang x = {\<lbrakk>[]\<rbrakk>lang} \<Longrightarrow> x = []"
-      apply (simp add:tag_str_STAR_def)
-      apply (drule equalityD1)
-      apply (case_tac x)
-      apply simp
-      thm in_mono
-      apply (drule_tac x = "\<lbrakk>[a]\<rbrakk>lang" in in_mono)
-      apply simp
-      apply auto
-      
-      apply (erule subsetCE)
-      
-      apply (case_tac y)
-      
-      sorry
-  next
+  have aux: "\<And> x y z. \<lbrakk>tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y; x @ z \<in> L\<^isub>1\<star>\<rbrakk> \<Longrightarrow> y @ z \<in> L\<^isub>1\<star>"
+  proof-
+    fix x y z
+    assume tag_eq: "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y"
+      and x_z: "x @ z \<in> L\<^isub>1\<star>"
+    show "y @ z \<in> L\<^isub>1\<star>"
+    proof (cases "x = []")
+      case True
+      with tag_eq have "y = []" by (simp add:tag_str_STAR_def split:if_splits, blast)
+      thus ?thesis using x_z True by simp
+    next
+      case False
+      hence not_empty: "{xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>} \<noteq> {}" using x_z
+        by (simp, rule_tac x = x in exI, rule_tac x = "[]" in exI, simp add:start)
+      have finite_set: "finite {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}"
+        apply (rule_tac B = "{xb. \<exists> xa. x = xa @ xb}" in finite_subset)
+        apply auto
+        apply (induct x, simp)
+        apply (subgoal_tac "{xb. \<exists>xa. a # x = xa @ xb} = insert (a # x) {xb. \<exists>xa. x = xa @ xb}")
+        apply auto
+        by (case_tac xaa, simp+)
+      have comparable: "\<forall> a \<in> {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}. 
+                        \<forall> b \<in> {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>}.
+                          ((b >>= a) \<or> (a >>= b))"
+        by (auto simp:postfix_def, drule app_eq_elim, blast)
+      hence "\<exists> min. min \<in> {xb. \<exists> xa. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star>} 
+                \<and> (\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= min)"
+        using finite_set not_empty comparable
+        apply (drule_tac min_postfix_exists, simp)
+        by (erule exE, rule_tac x = min in exI, auto)
+      then obtain min xa where x_decom: "x = xa @ min \<and> xa \<in> L\<^isub>1\<star>"
+        and min_not_empty: "min \<noteq> []"
+        and min_z_in_star: "min @ z \<in> L\<^isub>1\<star>"
+        and is_min: "\<forall> xa xb. x = xa @ xb \<and> xa \<in> L\<^isub>1\<star> \<and> xb \<noteq> [] \<and> xb @ z \<in> L\<^isub>1\<star> \<longrightarrow> xb >>= min"  by blast
+      from x_decom min_not_empty have "\<lbrakk>min\<rbrakk>L\<^isub>1 \<in> tag_str_STAR L\<^isub>1 x"  by (auto simp:tag_str_STAR_def)
+      hence "\<exists> yb. \<lbrakk>yb\<rbrakk>L\<^isub>1 \<in> tag_str_STAR L\<^isub>1 y \<and> \<lbrakk>min\<rbrakk>L\<^isub>1 = \<lbrakk>yb\<rbrakk>L\<^isub>1" using tag_eq by auto
+      hence "\<exists> ya yb. y = ya @ yb \<and> ya \<in> L\<^isub>1\<star> \<and> min \<equiv>L\<^isub>1\<equiv> yb \<and> yb \<noteq> [] " 
+        by (simp add:tag_str_STAR_def equiv_class_def equiv_str_def split:if_splits, blast)        
+      then obtain ya yb where y_decom: "y = ya @ yb"
+                          and ya_in_star: "ya \<in> L\<^isub>1\<star>"
+                          and yb_not_empty: "yb \<noteq> []"
+                          and min_yb_eq: "min \<equiv>L\<^isub>1\<equiv> yb"  by blast
+      from min_z_in_star min_yb_eq min_not_empty is_min x_decom
+      have "yb @ z \<in> L\<^isub>1\<star>"
+        by (rule_tac x = x and xa = xa in inj_aux, simp+)
+      thus ?thesis using ya_in_star y_decom
+        by (auto dest:star_prop)        
+    qed
   qed
-    apply (simp add:tag_str_STAR_def equiv_class_def equiv_str_def)
-    apply (rule iffI)
-    
-    apply (auto simp:tag_str_STAR_def equiv_class_def equiv_str_def)
-  have "\<And> x y z xstr. xstr \<in> L\<^isub>1\<star> \<Longrightarrow> 
-                      xstr = x @ z \<and> tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y \<longrightarrow> y @ z \<in> L\<^isub>1\<star> "
-  proof (erule Star.induct)
-    fix x y z xstr
-    show "[] = x @ z \<and> tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 y \<longrightarrow> y @ z \<in> L\<^isub>1\<star>"
-    apply (clarsimp simp add:tag_str_STAR_def equiv_str_def equiv_class_def)
-    apply (blast)
-apply (simp add:tag_str_STAR_def equiv_class_def QUOT_def)
-apply (simp add:equiv_str_def)
-apply (rule allI, rule_tac iffI)
-apply (erule_tac star.induct)
-apply blast
-
-sorry
-
+  show "tag_str_STAR L\<^isub>1 x = tag_str_STAR L\<^isub>1 (y::string) \<Longrightarrow> x \<equiv>L\<^isub>1\<star>\<equiv> y"
+    by (auto intro:aux simp:equiv_str_def)
+qed
 
 lemma quot_star:  
   assumes finite1: "finite (QUOT L\<^isub>1)"
@@ -1872,7 +1813,4 @@
 apply (simp add:QUOT_def equiv_class_def equiv_str_def)
 by (simp_all add:quot_lambda quot_single quot_seq quot_alt quot_star)  
 
-
-
-
-end
\ No newline at end of file
+end