283   moreover

   283   moreover

   284   have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" 

   284   have "\<forall>x \<in> B. \<forall>y \<in> B. x \<noteq> y \<longrightarrow> \<not> (x \<approx>A y)" 

   285     apply(auto simp add: B_def A_def)

   285     apply(auto simp add: B_def A_def)

   286     apply(auto simp add: str_eq_def)

   286     apply(auto simp add: str_eq_def)

   287     apply(drule_tac x="CHR ''b'' ^^^ aa" in spec)

   287     apply(drule_tac x="CHR ''b'' ^^^ aa" in spec)

   289     apply(auto)

   288     apply(auto)

   290     apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)

   289     apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)

   291     apply(simp add: length_test_def)

   290     apply(simp add: length_test_def)

   292     done

   291     done

   293   ultimately 

   292   ultimately