397         obtain za zb where eq_zab: "z = za @ zb" 

   397         obtain za zb where eq_zab: "z = za @ zb" 

   398           and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"

   398           and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"

   399         proof -

   399         proof -

   400           from h1 have "(x - xa_max) @ z \<noteq> []" 

   400           from h1 have "(x - xa_max) @ z \<noteq> []" 

   401             by (auto simp:strict_prefix_def elim:prefixE)

   401             by (auto simp:strict_prefix_def elim:prefixE)

   403           obtain a b where a_in: "a \<in> L\<^isub>1" 

   403           obtain a b where a_in: "a \<in> L\<^isub>1" 

   404             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 

   404             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 

   405             and ab_max: "(x - xa_max) @ z = a @ b" by blast

   405             and ab_max: "(x - xa_max) @ z = a @ b" by blast

   406           let ?za = "a - (x - xa_max)" and ?zb = "b"

   406           let ?za = "a - (x - xa_max)" and ?zb = "b"

   407           have pfx: "(x - xa_max) \<le> a" (is "?P1") 

   407           have pfx: "(x - xa_max) \<le> a" (is "?P1")