--- thys/Re1.thy	
+++ thys/Re1.thy	
@@ -168,6 +168,33 @@
 done
 *)
 
+
+
+
+lemma POSIX_ALT2:
+  assumes "POSIX (Left v1) (ALT r1 r2)"
+  shows "POSIX v1 r1"
+using assms
+unfolding POSIX_def
+apply(auto)
+apply(drule_tac x="Left v'" in spec)
+apply(simp)
+apply(drule mp)
+apply(rule Prf.intros)
+apply(auto)
+apply(erule ValOrd.cases)
+apply(simp_all)
+done
+
+lemma POSIX2_ALT:
+  assumes "POSIX2 (Left v1) (ALT r1 r2)"
+  shows "POSIX2 v1 r1"
+using assms
+unfolding POSIX2_def
+apply(auto)
+
+done
+
 lemma POSIX_ALT:
   assumes "POSIX (Left v1) (ALT r1 r2)"
   shows "POSIX v1 r1"