equal
deleted
inserted
replaced
90 \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m); |
90 \<forall>m \<in> lessThan n. F \<in> {m} LeadsTo (greaterThan m); |
91 n \<in> common |] |
91 n \<in> common |] |
92 ==> F \<in> (atMost n) LeadsTo common" |
92 ==> F \<in> (atMost n) LeadsTo common" |
93 apply (rule LeadsTo_weaken_R) |
93 apply (rule LeadsTo_weaken_R) |
94 apply (rule_tac f = id and l = n in GreaterThan_bounded_induct) |
94 apply (rule_tac f = id and l = n in GreaterThan_bounded_induct) |
95 apply (simp_all (no_asm_simp)) |
95 apply (simp_all (no_asm_simp) del: Int_insert_right_if1) |
96 apply (rule_tac [2] subset_refl) |
96 apply (rule_tac [2] subset_refl) |
97 apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) |
97 apply (blast dest: PSP_Stable2 intro: common_stable LeadsTo_weaken_R) |
98 done |
98 done |
99 |
99 |
100 (*The "\<forall>m \<in> -common" form echoes CMT6.*) |
100 (*The "\<forall>m \<in> -common" form echoes CMT6.*) |