diff -r a3134f7de065 -r 42268a284ea6 thys/PositionsExt.thy
--- a/thys/PositionsExt.thy	Sat Oct 07 22:16:16 2017 +0100
+++ b/thys/PositionsExt.thy	Sun Oct 08 14:21:24 2017 +0100
@@ -889,7 +889,55 @@
       then show "Stars (v # vs) :\<sqsubseteq>val v3"
       unfolding PosOrd_ex_eq_def using cond2
       by (simp add: PosOrd_shorterI)
-  qed         
+  qed        
+next    
+  case (Posix_FROMNTIMES3 s1 r v s2 vs v3)
+      have "s1 \<in> r \<rightarrow> v" "s2 \<in> STAR r \<rightarrow> Stars vs" by fact+
+  then have as1: "s1 = flat v" "s2 = flat (Stars vs)" by (auto dest: Posix1(2))
+  have IH1: "\<And>v3. v3 \<in> LV r s1 \<Longrightarrow> v :\<sqsubseteq>val v3" by fact
+  have IH2: "\<And>v3. v3 \<in> LV (STAR r) s2 \<Longrightarrow> Stars vs :\<sqsubseteq>val v3" by fact
+  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
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (FROMNTIMES r 0) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : STAR r"
+    "flat (Stars (v3a # vs3)) = s1 @ s2"
+  | (Empty) "v3 = Stars []" 
+  unfolding LV_def  
+  apply(auto)
+  apply(erule Prf.cases)
+  apply(auto)
+  apply(case_tac vs)
+  apply(auto intro: Prf.intros)
+  done
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flat (Stars (v3a # vs3)) = s1 @ s2" using NonEmpty(4) . 
+      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+        unfolding prefix_list_def
+        by (smt L_flat_Prf1 append_Nil2 append_eq_append_conv2 flat.simps(7)) 
+      then have "flat v3a \<sqsubset>spre s1 \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" using NonEmpty(4)
+        by (simp add: sprefix_list_def append_eq_conv_conj)
+      then have q2: "v :\<sqsubset>val v3a \<or> (flat v3a = s1 \<and> flat (Stars vs3) = s2)" 
+        using PosOrd_spreI as1(1) NonEmpty(4) by blast
+      then have "v :\<sqsubset>val v3a \<or> (v3a \<in> LV r s1 \<and> Stars vs3 \<in> LV (STAR r) s2)" 
+        using NonEmpty(2,3) by (auto simp add: LV_def)
+      then have "v :\<sqsubset>val v3a \<or> (v :\<sqsubseteq>val v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" using IH1 IH2 by blast
+      then have "v :\<sqsubset>val v3a \<or> (v = v3a \<and> Stars vs :\<sqsubseteq>val Stars vs3)" 
+         unfolding PosOrd_ex_eq_def by auto     
+      then have "Stars (v # vs) :\<sqsubseteq>val Stars (v3a # vs3)" using NonEmpty(4) q2 as1
+        unfolding  PosOrd_ex_eq_def
+        using PosOrd_StarsI PosOrd_StarsI2 by auto 
+      then show "Stars (v # vs) :\<sqsubseteq>val v3" unfolding NonEmpty by blast
+    next 
+      case Empty
+      have "v3 = Stars []" by fact
+      then show "Stars (v # vs) :\<sqsubseteq>val v3"
+      unfolding PosOrd_ex_eq_def using cond2
+      by (simp add: PosOrd_shorterI)
+    qed      
 next
   case (Posix_NMTIMES2 vs r n m v2) 
   then show "Stars vs :\<sqsubseteq>val v2" sorry