775 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
775 | Posix_STAR2: "[] \<in> STAR r \<rightarrow> Stars []" |
776 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r n \<rightarrow> Stars vs; flat v \<noteq> []; |
776 | Posix_UPNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> UPNTIMES r n \<rightarrow> Stars vs; flat v \<noteq> []; |
777 \<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 n))\<rbrakk> |
777 \<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 n))\<rbrakk> |
778 \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
778 \<Longrightarrow> (s1 @ s2) \<in> UPNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
779 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
779 | Posix_UPNTIMES2: "[] \<in> UPNTIMES r n \<rightarrow> Stars []" |
780 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; |
780 | Posix_NTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NTIMES r n \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
781 \<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 (NTIMES r n))\<rbrakk> |
781 \<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 (NTIMES r n))\<rbrakk> |
782 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
782 \<Longrightarrow> (s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
783 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
783 | Posix_NTIMES2: "[] \<in> NTIMES r 0 \<rightarrow> Stars []" |
784 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; |
784 | Posix_FROMNTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> FROMNTIMES r n \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
785 \<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 (FROMNTIMES r n))\<rbrakk> |
785 \<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 (FROMNTIMES r n))\<rbrakk> |
786 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
786 \<Longrightarrow> (s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> Stars (v # vs)" |
787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
787 | Posix_FROMNTIMES2: "s \<in> STAR r \<rightarrow> Stars vs \<Longrightarrow> s \<in> FROMNTIMES r 0 \<rightarrow> Stars vs" |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
788 | Posix_NMTIMES1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> NMTIMES r n m \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = []; |
789 \<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 m))\<rbrakk> |
789 \<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 m))\<rbrakk> |
1113 case (Posix_NTIMES2 r v2) |
1113 case (Posix_NTIMES2 r v2) |
1114 have "[] \<in> NTIMES r 0 \<rightarrow> v2" by fact |
1114 have "[] \<in> NTIMES r 0 \<rightarrow> v2" by fact |
1115 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
1115 then show "Stars [] = v2" by cases (auto simp add: Posix1) |
1116 next |
1116 next |
1117 case (Posix_NTIMES1 s1 r v s2 n vs v2) |
1117 case (Posix_NTIMES1 s1 r v s2 n vs v2) |
1118 have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2" |
1118 have "(s1 @ s2) \<in> NTIMES r (Suc n) \<rightarrow> v2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
1119 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NTIMES r n) \<rightarrow> Stars vs" |
1119 "s1 \<in> r \<rightarrow> v" "s2 \<in> (NTIMES r n) \<rightarrow> Stars vs" |
1120 "\<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 (NTIMES r n))" by fact+ |
1120 "\<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 (NTIMES r n))" by fact+ |
1121 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')" |
1121 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NTIMES r n) \<rightarrow> (Stars vs')" |
1122 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1122 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1123 using Posix1(1) apply fastforce |
1123 using Posix1(1) apply fastforce |
1124 apply (metis Posix1(1) Posix_NTIMES1.hyps(5) append_Nil append_Nil2) |
1124 by (metis Posix1(1) Posix_NTIMES1.hyps(6) append_Nil append_Nil2) |
1125 done |
|
1126 moreover |
1125 moreover |
1127 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1126 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1128 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1127 "\<And>v2. s2 \<in> NTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1129 ultimately show "Stars (v # vs) = v2" by auto |
1128 ultimately show "Stars (v # vs) = v2" by auto |
1130 next |
1129 next |
1136 apply(auto) |
1135 apply(auto) |
1137 done |
1136 done |
1138 next |
1137 next |
1139 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
1138 case (Posix_FROMNTIMES1 s1 r v s2 n vs v2) |
1140 have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" |
1139 have "(s1 @ s2) \<in> FROMNTIMES r (Suc n) \<rightarrow> v2" |
1141 "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs" |
1140 "s1 \<in> r \<rightarrow> v" "s2 \<in> (FROMNTIMES r n) \<rightarrow> Stars vs" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
1142 "\<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 (FROMNTIMES r n))" by fact+ |
1141 "\<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 (FROMNTIMES r n))" by fact+ |
1143 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r n) \<rightarrow> (Stars vs')" |
1142 then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (FROMNTIMES r n) \<rightarrow> (Stars vs')" |
1144 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1143 apply(cases) apply (auto simp add: append_eq_append_conv2) |
1145 using Posix1(1) apply fastforce |
1144 using Posix1(1) apply fastforce |
1146 by (metis Posix1(1) Posix_FROMNTIMES1.hyps(5) append_Nil2 self_append_conv2) |
1145 by (metis Posix1(1) Posix_FROMNTIMES1.hyps(6) append_Nil append_Nil2) |
1147 moreover |
1146 moreover |
1148 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1147 have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2" |
1149 "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1148 "\<And>v2. s2 \<in> FROMNTIMES r n \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+ |
1150 ultimately show "Stars (v # vs) = v2" by auto |
1149 ultimately show "Stars (v # vs) = v2" by auto |
1151 next |
1150 next |
1429 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1428 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1430 have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact |
1429 have "s \<in> der c (NTIMES r n) \<rightarrow> v" by fact |
1431 then consider |
1430 then consider |
1432 (cons) m v1 vs s1 s2 where |
1431 (cons) m v1 vs s1 s2 where |
1433 "n = Suc m" |
1432 "n = Suc m" |
1434 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1433 "v = Seq v1 (Stars vs)" "s = s1 @ s2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
1435 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r m) \<rightarrow> (Stars vs)" |
1434 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (NTIMES r m) \<rightarrow> (Stars vs)" |
1436 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" |
1435 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" |
1437 apply(case_tac n) |
1436 apply(case_tac n) |
1438 apply(simp) |
1437 apply(simp) |
1439 using Posix_elims(1) apply blast |
1438 using Posix_elims(1) apply blast |
1446 have "n = Suc m" by fact |
1445 have "n = Suc m" by fact |
1447 moreover |
1446 moreover |
1448 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1447 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1449 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1448 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1450 moreover |
1449 moreover |
|
1450 have "flat v = [] \<Longrightarrow> flat (Stars vs) = []" by fact |
|
1451 moreover |
1451 have "s2 \<in> NTIMES r m \<rightarrow> Stars vs" by fact |
1452 have "s2 \<in> NTIMES r m \<rightarrow> Stars vs" by fact |
1452 moreover |
1453 moreover |
1453 have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" by fact |
1454 have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (NTIMES r m))" by fact |
1454 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r m))" |
1455 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NTIMES r m))" |
1455 by (simp add: der_correctness Der_def) |
1456 by (simp add: der_correctness Der_def) |
1456 ultimately |
1457 ultimately |
1457 have "((c # s1) @ s2) \<in> NTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
1458 have "((c # s1) @ s2) \<in> NTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
1458 apply(rule_tac Posix.intros(10)) |
1459 apply(rule_tac Posix.intros(10)) |
1459 apply(simp_all) |
1460 apply(simp_all) |
1460 done |
1461 by (simp add: Posix1(2)) |
1461 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
1462 then show "(c # s) \<in> NTIMES r n \<rightarrow> injval (NTIMES r n) c v" using cons by(simp) |
1462 qed |
1463 qed |
1463 next |
1464 next |
1464 case (FROMNTIMES r n) |
1465 case (FROMNTIMES r n) |
1465 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1466 have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact |
1470 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1471 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1471 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)" |
1472 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r 0) \<rightarrow> (Stars vs)" |
1472 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))" |
1473 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r 0))" |
1473 | (cons) m v1 vs s1 s2 where |
1474 | (cons) m v1 vs s1 s2 where |
1474 "n = Suc m" |
1475 "n = Suc m" |
1475 "v = Seq v1 (Stars vs)" "s = s1 @ s2" |
1476 "v = Seq v1 (Stars vs)" "s = s1 @ s2" "flat v = [] \<Longrightarrow> flat (Stars vs) = []" |
1476 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
1477 "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (FROMNTIMES r m) \<rightarrow> (Stars vs)" |
1477 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" |
1478 "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" |
1478 apply(case_tac n) |
1479 apply(case_tac n) |
1479 apply(simp) |
1480 apply(simp) |
1480 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
1481 apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros) |
1492 moreover |
1493 moreover |
1493 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1494 have "s1 \<in> der c r \<rightarrow> v1" by fact |
1494 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1495 then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp |
1495 moreover |
1496 moreover |
1496 have "s2 \<in> FROMNTIMES r m \<rightarrow> Stars vs" by fact |
1497 have "s2 \<in> FROMNTIMES r m \<rightarrow> Stars vs" by fact |
|
1498 moreover |
|
1499 have "flat v = [] \<Longrightarrow> flat (Stars vs) = []" by fact |
1497 moreover |
1500 moreover |
1498 have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" by fact |
1501 have "\<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 (der c r) \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" by fact |
1499 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" |
1502 then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (FROMNTIMES r m))" |
1500 by (simp add: der_correctness Der_def) |
1503 by (simp add: der_correctness Der_def) |
1501 ultimately |
1504 ultimately |
1502 have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
1505 have "((c # s1) @ s2) \<in> FROMNTIMES r (Suc m) \<rightarrow> Stars (injval r c v1 # vs)" |
1503 apply(rule_tac Posix.intros(12)) |
1506 apply(rule_tac Posix.intros(12)) |
1504 apply(simp_all) |
1507 apply(simp_all) |
1505 done |
1508 by (simp add: Posix1(2)) |
1506 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
1509 then show "(c # s) \<in> FROMNTIMES r n \<rightarrow> injval (FROMNTIMES r n) c v" using cons by(simp) |
1507 next |
1510 next |
1508 case null |
1511 case null |
1509 then have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" |
1512 then have "((c # s1) @ s2) \<in> FROMNTIMES r 0 \<rightarrow> Stars (injval r c v1 # vs)" |
1510 apply(rule_tac Posix.intros) |
1513 apply(rule_tac Posix.intros) |