892   qed         

   892   qed        

   893 next    

   894   case (Posix_FROMNTIMES3 s1 r v s2 vs v3)

   895       have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+

   896   then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))

   897   have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact

   898   have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact

   899   have cond: "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact

   900   have cond2: "flat v \<noteq> []" by fact

   901   have "v3 \<in> LV (FROMNTIMES r 0) (s1 @ s2)" by fact

   902   then consider 

   903     (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 

   904     "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"

   905     "flat (Stars (v3a # vs3)) = s1 @ s2"

   906   | (Empty) "v3 = Stars []" 

   907   unfolding LV_def  

   908   apply(auto)

   909   apply(erule Prf.cases)

   910   apply(auto)

   911   apply(case_tac vs)

   912   apply(auto intro: Prf.intros)

   913   done

   914   then show "Stars (v # vs) :\<sqsubseteq>val v3" 

   915     proof (cases)

   916       case (NonEmpty v3a vs3)

   917       have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 

   918       with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)

   919         unfolding prefix_list_def

   920         by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) 

   921       then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)

   922         by (simp add: sprefix_list_def append_eq_conv_conj)

   923       then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 

   924         using PosOrd_spreI as1(1) NonEmpty(4) by blast

   925       then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" 

   926         using NonEmpty(2,3) by (auto simp add: LV_def)

   927       then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast

   928       then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 

   929          unfolding PosOrd_ex_eq_def by auto     

   930       then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1

   931         unfolding  PosOrd_ex_eq_def

   932         using PosOrd_StarsI PosOrd_StarsI2 by auto 

   933       then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast

   934     next 

   935       case Empty

   936       have "v3 = Stars []" by fact

   937       then show "Stars (v # vs) :\<sqsubseteq>val v3"

   938       unfolding PosOrd_ex_eq_def using cond2

   939       by (simp add: PosOrd_shorterI)

   940     qed