equal
deleted
inserted
replaced
659 *} |
659 *} |
660 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast |
660 have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using l_za ls_zb by blast |
661 with eq_zab show ?thesis by simp |
661 with eq_zab show ?thesis by simp |
662 qed |
662 qed |
663 with h5 h6 show ?thesis |
663 with h5 h6 show ?thesis |
664 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
664 by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE) |
665 qed |
665 qed |
666 } |
666 } |
667 -- {* By instantiating the reasoning pattern just derived for both directions:*} |
667 -- {* By instantiating the reasoning pattern just derived for both directions:*} |
668 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
668 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
669 -- {* The thesis is proved as a trival consequence: *} |
669 -- {* The thesis is proved as a trival consequence: *} |
768 by (auto simp:str_eq_def str_eq_rel_def) |
768 by (auto simp:str_eq_def str_eq_rel_def) |
769 with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast |
769 with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast |
770 with z_decom show ?thesis by auto |
770 with z_decom show ?thesis by auto |
771 qed |
771 qed |
772 with h5 h6 show ?thesis |
772 with h5 h6 show ?thesis |
773 by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE) |
773 by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE) |
774 qed |
774 qed |
775 } |
775 } |
776 -- {* By instantiating the reasoning pattern just derived for both directions:*} |
776 -- {* By instantiating the reasoning pattern just derived for both directions:*} |
777 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
777 from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]] |
778 -- {* The thesis is proved as a trival consequence: *} |
778 -- {* The thesis is proved as a trival consequence: *} |