equal
deleted
inserted
replaced
243 then obtain f::"nat \<Rightarrow> letter list" where b: "inj f" and c: "range f \<subseteq> A" |
243 then obtain f::"nat \<Rightarrow> letter list" where b: "inj f" and c: "range f \<subseteq> A" |
244 by (auto simp add: infinite_iff_countable_subset) |
244 by (auto simp add: infinite_iff_countable_subset) |
245 from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast |
245 from higman_idx obtain i j where d: "i < j" and e: "f i \<preceq> f j" by blast |
246 have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def) |
246 have "f i \<noteq> f j" using b d by (auto simp add: inj_on_def) |
247 moreover |
247 moreover |
248 have "f i \<in> A" sorry |
248 have "f i \<in> A" using c by auto |
249 moreover |
249 moreover |
250 have "f j \<in> A" sorry |
250 have "f j \<in> A" using c by auto |
251 ultimately have "\<not>(f i \<preceq> f j)" using a by simp |
251 ultimately have "\<not>(f i \<preceq> f j)" using a by simp |
252 with e show "False" by simp |
252 with e show "False" by simp |
253 qed |
253 qed |
254 |
254 |
255 definition |
255 definition |