equal
deleted
inserted
replaced
115 by (case_tac z, simp_all) |
115 by (case_tac z, simp_all) |
116 |
116 |
117 lemma up_lemma2: |
117 lemma up_lemma2: |
118 "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom" |
118 "\<lbrakk>chain Y; Y j \<noteq> Ibottom\<rbrakk> \<Longrightarrow> Y (i + j) \<noteq> Ibottom" |
119 apply (erule contrapos_nn) |
119 apply (erule contrapos_nn) |
120 apply (drule_tac x="j" and y="i + j" in chain_mono3) |
120 apply (drule_tac i="j" and j="i + j" in chain_mono) |
121 apply (rule le_add2) |
121 apply (rule le_add2) |
122 apply (case_tac "Y j") |
122 apply (case_tac "Y j") |
123 apply assumption |
123 apply assumption |
124 apply simp |
124 apply simp |
125 done |
125 done |