equal
deleted
inserted
replaced
207 lemma above_decreases: |
207 lemma above_decreases: |
208 "system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j) |
208 "system \<in> (\<Union>j. {s. above i s = x} Int {s. j \<in> above i s} Int Highest j) |
209 leadsTo {s. above i s < x}" |
209 leadsTo {s. above i s < x}" |
210 apply (rule leadsTo_UN) |
210 apply (rule leadsTo_UN) |
211 apply (rule single_leadsTo_I, clarify) |
211 apply (rule single_leadsTo_I, clarify) |
212 apply (rule_tac x = "above i x" in above_decreases_lemma) |
212 apply (rule_tac x = "above i xa" in above_decreases_lemma) |
213 apply (simp_all (no_asm_use) add: Highest_iff_above0) |
213 apply (simp_all (no_asm_use) add: Highest_iff_above0) |
214 apply blast+ |
214 apply blast+ |
215 done |
215 done |
216 |
216 |
217 (** Just a massage of conditions to have the desired form ***) |
217 (** Just a massage of conditions to have the desired form ***) |