equal
deleted
inserted
replaced
159 with assms have "Max js \<in> js" |
159 with assms have "Max js \<in> js" |
160 by auto |
160 by auto |
161 with assms have "Max js < i" |
161 with assms have "Max js < i" |
162 by (auto simp add: iseq_def) |
162 by (auto simp add: iseq_def) |
163 with fin assms have "\<forall>j\<in>js. j < i" |
163 with fin assms have "\<forall>j\<in>js. j < i" |
164 by (simp add: Max_less_iff) |
164 by simp |
165 with assms show ?thesis |
165 with assms show ?thesis |
166 by (simp add: iseq_def) |
166 by (simp add: iseq_def) |
167 qed |
167 qed |
168 |
168 |
169 lemma iseq_mono: "is \<in> iseq xs i \<Longrightarrow> i \<le> j \<Longrightarrow> is \<in> iseq xs j" |
169 lemma iseq_mono: "is \<in> iseq xs i \<Longrightarrow> i \<le> j \<Longrightarrow> is \<in> iseq xs j" |