diff -r 42268a284ea6 -r 424bdcd01016 thys/PositionsExt.thy
--- a/thys/PositionsExt.thy	Sun Oct 08 14:21:24 2017 +0100
+++ b/thys/PositionsExt.thy	Tue Oct 10 10:40:44 2017 +0100
@@ -940,10 +940,123 @@
     qed      
 next
   case (Posix_NMTIMES2 vs r n m v2) 
-  then show "Stars vs :\<sqsubseteq>val v2" sorry
+  then show "Stars vs :\<sqsubseteq>val v2" 
+    apply(auto simp add: LV_def)
+    apply(erule Prf_elims)
+     apply(simp)
+     apply(rule PosOrd_eq_Stars_zipI) 
+       apply(auto)
+     apply (meson in_set_zipE)
+    by (metis Posix1(2) flats_empty)
 next
-  case (Posix_NMTIMES1 s1 r v s2 n m vs v2) 
-  then show "Stars (v # vs) :\<sqsubseteq>val v2" sorry      
+  case (Posix_NMTIMES1 s1 r v s2 n m vs v3) 
+  have "s1 \<in> r \<rightarrow> v" "s2 \<in> NMTIMES r (n - 1) (m - 1) \<rightarrow> Stars vs" by fact+
+  then have as1: "s1 = flat v" "s2 = flats 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 (NMTIMES r (n - 1) (m - 1)) 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 (NMTIMES r (n - 1) (m - 1)))" by fact
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (NMTIMES r n m) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : NMTIMES r (n - 1) (m - 1)"
+    "flats (v3a # vs3) = s1 @ s2"
+  | (Empty) "v3 = Stars []" 
+  unfolding LV_def  
+  apply(auto)
+  apply(erule Prf.cases)
+             apply(auto)  
+  apply(case_tac n)
+    apply(auto intro: Prf.intros)
+   apply(case_tac vs1)
+    apply(auto intro: Prf.intros)
+   apply (simp add: as1(1) cond2 flats_empty)
+   apply (simp add: Prf.intros(11))
+  apply(case_tac n)
+   apply(simp)
+  using Posix_NMTIMES1.hyps(6) apply blast
+  apply(simp)
+  apply(case_tac vs)
+   apply(auto)
+  by (simp add: Prf.intros(12))
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flats (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) flat_Stars)
+      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 (NMTIMES r (n - 1) (m - 1)) 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_NMTIMES3 s1 r v s2 m vs v3) 
+  have "s1 \<in> r \<rightarrow> v" "s2 \<in> UPNTIMES r (m - 1) \<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 (UPNTIMES r (m - 1)) 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 (UPNTIMES r (m - 1)))" by fact
+  have cond2: "flat v \<noteq> []" by fact
+  have "v3 \<in> LV (NMTIMES r 0 m) (s1 @ s2)" by fact
+  then consider 
+    (NonEmpty) v3a vs3 where "v3 = Stars (v3a # vs3)" 
+    "\<Turnstile> v3a : r" "\<Turnstile> Stars vs3 : UPNTIMES r (m - 1)" 
+    "flats (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)
+  by (simp add: Prf.intros(7) as1(1) cond2)
+  then show "Stars (v # vs) :\<sqsubseteq>val v3" 
+    proof (cases)
+      case (NonEmpty v3a vs3)
+      have "flats (v3a # vs3) = s1 @ s2" using NonEmpty(4) . 
+      with cond have "flat v3a \<sqsubseteq>pre s1" using NonEmpty(2,3)
+        unfolding prefix_list_def
+        apply(simp)
+        apply(simp add: append_eq_append_conv2)
+        apply(auto)
+        by (metis L_flat_Prf1 One_nat_def cond flat_Stars)
+      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 (UPNTIMES r (m - 1)) 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          
 qed