Theory Erdos_Milner

theory Erdos_Milner
  imports Partitions


subsection ‹Erdős-Milner theorem›

text ‹P. Erdős and E. C. Milner, A Theorem in the Partition Calculus.
Canadian Math. Bull. 15:4 (1972), 501-505.
Corrigendum, Canadian Math. Bull. 17:2 (1974), 305.›

text ‹The paper defines strong types as satisfying the criteria below.
      It remarks that ordinals satisfy those criteria. Here is a (too complicated) proof.›
proposition strong_ordertype_eq:
  assumes D: "D  elts β" and "Ord β"
  obtains L where "(List.set L) = D" "X. X  List.set L  indecomposable (tp X)"
    and "M. M  D; X. X  List.set L  tp (M  X)  tp X  tp M = tp D"
proof -
  define φ where "φ  inv_into D (ordermap D VWF)"
  then have bij_φ: "bij_betw φ (elts (tp D)) D"
    using D bij_betw_inv_into down ordermap_bij by blast
  have φ_cancel_left: "d. d  D  φ (ordermap D VWF d) = d"
    by (metis D φ_def bij_betw_inv_into_left down ordermap_bij total_on_VWF wf_VWF)
  have φ_cancel_right: "γ. γ  elts (tp D)  ordermap D VWF (φ γ) = γ"
    by (metis φ_def f_inv_into_f ordermap_surj subsetD)
  have "small D" "D  ON"
    using assms down elts_subset_ON [of β] by auto
  then have φ_less_iff: "γ δ. γ  elts (tp D); δ  elts (tp D)  φ γ < φ δ  γ < δ"
    by (metis φ_def inv_ordermap_VWF_mono_iff inv_ordermap_mono_eq less_V_def)
  obtain αs where "List.set αs  ON" and "ω_dec αs" and tpD_eq: "tp D = ω_sum αs"
    using Ord_ordertype ω_nf_exists by blast                ― ‹Cantor normal form of the ordertype›
  have ord [simp]: "Ord (αs ! k)" "Ord (ω_sum (take k αs))" if "k < length αs" for k
    using that list.set αs  ON
    by (auto simp: dual_order.trans set_take_subset elim: ON_imp_Ord)
  define E where "E  λk. lift (ω_sum (take k αs)) (ω(αs!k))"
  define L where "L  map (λk. φ ` (elts (E k))) [0..<length αs]"
  have lengthL [simp]: "length L = length αs"
    by (simp add: L_def)
  have in_elts_E_less: "elts (E k')  elts (E k)" if "k'<k" "k < length αs" for k k'
    ― ‹The ordinals have been partitioned into disjoint intervals›
  proof -
    have ordω: "Ord (ω  αs ! k')"
      using that by auto
    from that id_take_nth_drop [of k' "take k αs"]
    obtain l where "take k αs = take k' αs @ (αs!k') # l"
      by (simp add: min_def)
    then show ?thesis
      using that unfolding E_def lift_def less_sets_def
      by (auto dest!: OrdmemD [OF ordω] intro: less_le_trans)
  have elts_E: "elts (E k)  elts (ω_sum αs)"
    if "k < length αs" for k
  proof -
    have "ω  (αs!k)  ω_sum (drop k αs)"
      by (metis that Cons_nth_drop_Suc ω_sum_Cons add_le_cancel_left0)
    then have "(+) (ω_sum (take k αs)) ` elts (ω  (αs!k))  elts (ω_sum (take k αs) + ω_sum (drop k αs))"
      by blast
    also have " = elts (ω_sum αs)"
      using ω_sum_take_drop by auto
    finally show ?thesis
      by (simp add: lift_def E_def)
  have ω_sum_in_tpD: "ω_sum (take k αs) + γ  elts (tp D)"
    if "γ  elts (ω  αs!k)" "k < length αs" for γ k
    using elts_E lift_def that tpD_eq by (auto simp: E_def)
  have Ord_φ: "Ord (φ (ω_sum (take k αs) + γ))"
    if "γ  elts (ω  αs!k)" "k < length αs" for γ k
    using ω_sum_in_tpD D  ON bij_φ bij_betw_imp_surj_on that by fastforce
  define π where "π  λk. ((λy. odiff y (ω_sum (take k αs)))  ordermap D VWF)"
      ― ‹mapping the segments of @{term D} into some power of @{term ω}
  have bij_π: "bij_betw (π k) (φ ` elts (E k)) (elts (ω  (αs!k)))"
    if "k < length αs" for k
    using that by (auto simp: bij_betw_def π_def E_def inj_on_def lift_def image_comp ω_sum_in_tpD φ_cancel_right that)
  have π_iff: "π k x < π k y  (x,y)  VWF"
    if "x  φ ` elts (E k)" "y  φ ` elts (E k)" "k < length αs" for k x y
    using that
    by (auto simp: π_def E_def lift_def ω_sum_in_tpD φ_cancel_right Ord_φ φ_less_iff)
  have tp_E_eq [simp]: "tp (φ ` elts (E k)) = ω(αs!k)"
    if k: "k < length αs" for k
    by (metis Ord_ω Ord_oexp π_iff bij_π ord(1) ordertype_VWF_eq_iff replacement small_elts that)
  have tp_L_eq [simp]: "tp (L!k) = ω(αs!k)" if "k < length αs" for k
    by (simp add: L_def that)
  have UL_eq_D: " (list.set L) = D"
  proof (rule antisym)
    show " (list.set L)  D"
      by (force simp: L_def tpD_eq bij_betw_apply [OF bij_φ] dest: elts_E)
    show "D   (list.set L)"
      fix δ
      assume "δ  D"
      then have "ordermap D VWF δ  elts (ω_sum αs)"
        by (metis small D ordermap_in_ordertype tpD_eq)
      then show "δ   (list.set L)"
        using δ  D φ_cancel_left in_elts_ω_sum
        by (fastforce simp: L_def E_def image_iff lift_def)
  show thesis
    show "indecomposable (tp X)" if "X  list.set L" for X
      using that by (auto simp: L_def indecomposable_ω_power)
    fix M
    assume "M  D" and *: "X. X  list.set L  tp X  tp (M  X)"
    show "tp M = tp D"
    proof (rule antisym)
      show "tp M  tp D"
        by (simp add: M  D small D ordertype_VWF_mono)
      define σ where "σ  λX. inv_into (M  X) (ordermap (M  X) VWF)"
                              ― ‹The bijection from an @{term ω}-power into the appropriate segment of @{term M}
      have bij_σ: "bij_betw (σ X) (elts (tp (M  X))) (M  X)" for X
        unfolding σ_def
        by (meson M  D small D bij_betw_inv_into inf_le1 ordermap_bij smaller_than_small total_on_VWF wf_VWF)
      have Ord_σ: "Ord (σ X α)" if "α  elts (tp (M  X))" for α X
        using D  ON M  D bij_betw_apply [OF bij_σ] that by blast
      have σ_cancel_right: "γ X. γ  elts (tp (M  X))  ordermap (M  X) VWF (σ X γ) = γ"
        by (metis σ_def f_inv_into_f ordermap_surj subsetD)
      have smM: "small (M  X)" for X
        by (meson M  D small D inf_le1 subset_iff_less_eq_V)
      have "k < length αs. γ  elts (E k)" if γ: "γ  elts (tp D)" for γ
      proof -
        obtain X where "X  set L" and X: "φ γ  X"
          by (metis UL_eq_D γ Union_iff φ_def in_mono inv_into_into ordermap_surj)
        then have "k < length αs. γ  elts (E k)  X = φ ` elts (E k)"
          apply (clarsimp simp: L_def)
          by (metis γ φ_cancel_right elts_E in_mono tpD_eq)
        then show ?thesis
          by blast
      then obtain K where K: "γ. γ  elts (tp D)  K γ < length αs  γ  elts (E (K γ))"
        by metis  ― ‹The index from @{term "tp D"} to the appropriate segment number›
      define ψ where "ψ  λd. σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d)"
      show "tp D  tp M"
      proof (rule ordertype_inc_le)
        show "small D" "small M"
          using M  D small D subset_iff_less_eq_V by auto
        fix d' d
        assume xy: "d'  D" "d  D" and "(d',d)  VWF"
        then have "d' < d"
          using ON_imp_Ord D  ON by auto
        let ?γ' = "ordermap D VWF d'"
        let  = "ordermap D VWF d"
        have len': "K ?γ' < length αs" and elts': "?γ'  elts (E (K ?γ'))"
          and len: "K  < length αs" and elts: "  elts (E (K ))"
          using K d'  D d  D by (auto simp: small D ordermap_in_ordertype)
        have Ord_σL: "Ord (σ (L!k) (π k d))" if "d  φ ` elts (E k)" "k < length αs" for k d
          by (metis (mono_tags) "*" Ord_σ bij_π bij_betw_apply lengthL nth_mem that tp_L_eq vsubsetD)
        have "?γ' < "
          by (simp add: (d', d)  VWF small D ordermap_mono_less xy)
        then have "K ?γ'  K "
          using elts' elts in_elts_E_less by (meson leI len' less_asym less_sets_def)
        then consider (less) "K ?γ' < K " | (equal) "K ?γ' = K "
          by linarith
        then have "σ (L ! K ?γ') (π (K ?γ') d') < σ (L ! K ) (π (K ) d)"
        proof cases
          case less
          obtain : "σ (L ! K ?γ') (π (K ?γ') d')  M  L ! K ?γ'" "σ (L ! K ) (π (K ) d)  M  L ! K "
            using elts' elts len' len * [THEN vsubsetD]
            by (metis lengthL φ_cancel_left bij_π bij_σ bij_betw_imp_surj_on imageI nth_mem tp_L_eq xy)
          then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d'))  elts (E (K ?γ'))" "ordermap D VWF (σ (L ! K ) (π (K ) d))  elts (E (K ))"
            using len' len elts_E tpD_eq
            by (fastforce simp: L_def φ_cancel_right)+
          then have "ordermap D VWF (σ (L ! K ?γ') (π (K ?γ') d')) < ordermap D VWF (σ (L ! K ) (π (K ) d))"
            using in_elts_E_less len less by (meson less_sets_def)
          moreover have "σ (L ! K ?γ') (π (K ?γ') d')  D" "σ (L ! K ) (π (K ) d)  D"
            using M  D  by auto
          ultimately show ?thesis
            by (metis small D φ_cancel_left φ_less_iff ordermap_in_ordertype)
          case equal
          have σ_less: "X γ δ. γ < δ; γ  elts (tp (M  X)); δ  elts (tp (M  X))
                           σ X γ < σ X δ"
            by (metis D  ON M  D σ_def dual_order.trans inv_ordermap_VWF_strict_mono_iff le_infI1 smM)
          have "π (K ) d' < π (K ) d"
            by (metis equal (d', d)  VWF φ_cancel_left π_iff elts elts' imageI len xy)
          then show ?thesis
            unfolding equal
            by (metis * [THEN vsubsetD] lengthL φ_cancel_left σ_less bij_π 
                 bij_betw_imp_surj_on elts elts' image_eqI len local.equal nth_mem tp_L_eq xy)
        moreover have "Ord (σ (L ! K ?γ') (π (K ?γ') d'))" "Ord (σ (L ! K ) (π (K ) d))"
          using Ord_σL φ_cancel_left elts len elts' len' xy by fastforce+
        ultimately show "(ψ d', ψ d)  VWF"
          by (simp add: ψ_def)
        show "ψ ` D  M"
        proof (clarsimp simp: ψ_def)
          fix d
          assume "d  D"
          let  = "ordermap D VWF d"
          have len: "K  < length αs" and elts: "  elts (E (K ))"
            using K d  D by (auto simp: small D ordermap_in_ordertype)
          have "π (K ) d  elts (tp (L! (K )))"
            using bij_π [OF len] d  D
            by (metis φ_cancel_left bij_betw_apply elts imageI len tp_L_eq)
          then show "σ (L ! K (ordermap D VWF d)) (π (K (ordermap D VWF d)) d)  M"
            by (metis "*" lengthL Int_iff bij_σ bij_betw_apply len nth_mem vsubsetD) 
      qed auto
  qed (simp add: UL_eq_D)

text ‹The ``remark'' of Erdős and E. C. Milner, Canad. Math. Bull. Vol. 17 (2), 1974›

proposition indecomposable_imp_Ex_less_sets:
  assumes indec: "indecomposable α" and "α  ω" 
    and A: "tp A = α" "small A" "A  ON"
    and "x  A" and A1: "tp A1 = α" "A1  A"
  obtains A2 where "tp A2 = α" "A2  A1" "{x}  A2"
proof -
  have "Ord α"
    using indec indecomposable_imp_Ord by blast
  have "Limit α"
    by (meson ω_gt1 assms indec indecomposable_imp_Limit less_le_trans)
  define φ where "φ  inv_into A (ordermap A VWF)"
  then have bij_φ: "bij_betw φ (elts α) A"
    using A bij_betw_inv_into down ordermap_bij by blast
  have bij_om: "bij_betw (ordermap A VWF) A (elts α)"
    using A down ordermap_bij by blast
  define γ where "γ  ordermap A VWF x"
  have γ: "γ  elts α"
    unfolding γ_def using A x  A down by auto
  then have "Ord γ"
    using Ord_in_Ord Ord α by blast
  define B where "B  φ ` (elts (succ γ))"
  have B: "{y  A. ordermap A VWF y  ordermap A VWF x}  B"
    apply (clarsimp simp add: B_def γ_def image_iff φ_def)
    by (metis Ord_linear Ord_ordermap OrdmemD bij_betw_inv_into_left bij_om leD)
  show thesis
    have "small A1"
      by (meson small A A1 smaller_than_small)
    then have "tp (A1 - B)  tp A1"
      by (simp add: ordertype_VWF_mono)
    moreover have "tp (A1 - B)  α"
    proof -
      have "¬ (α  tp B)"
        unfolding B_def
      proof (subst ordertype_VWF_inc_eq)
        show "elts (succ  γ)  ON"
          by (auto simp: γ_def ordertype_VWF_inc_eq intro: Ord_in_Ord)
        have sub: "elts (succ  γ)  elts α"
          using Ord_trans γ Ord α by auto
        then show "φ ` elts (succ  γ)  ON"
          using A  ON bij_φ bij_betw_imp_surj_on by blast
        have "succ γ  elts α"
          using γ Limit_def Limit α by blast
        with A sub show "φ u < φ v"
          if "u  elts (succ  γ)" and "v  elts (succ  γ)" and "u < v" for u v
          by (metis φ_def inv_ordermap_VWF_strict_mono_iff subsetD that)
        show "¬ α  tp (elts (succ  γ))"
          by (metis Limit_def Ord_succ γ Limit α Ord γ mem_not_refl ordertype_eq_Ord vsubsetD)
      qed auto
      then show ?thesis
        using indecomposable_ordertype_ge [OF indec, of A1 B] small A1 A1 by (auto simp: B_def)
    ultimately show "tp (A1 - B) = α"
      using A1 by blast
    have "{x}  (A - B)"
      using assms B 
      apply (clarsimp simp: less_sets_def φ_def subset_iff)
      by (metis Ord_not_le VWF_iff_Ord_less less_V_def order_refl ordermap_mono_less trans_VWF wf_VWF)
    with A1  A show "{x}  (A1 - B)" by auto
  qed auto

text ‹the main theorem, from which they derive the headline result›
theorem Erdos_Milner_aux:
  assumes part: "partn_lst_VWF α [k, γ] 2"
    and indec: "indecomposable α" and "k > 1" "Ord γ" and β: "β  elts ω1"
  shows "partn_lst_VWF (α*β) [ord_of_nat (2*k), min γ (ω*β)] 2"
proof (cases "α1  β=0")
  case True
  have "Ord α"
    using indec indecomposable_def by blast
  show ?thesis
  proof (cases "β=0")
    case True then show ?thesis
      by (simp add: partn_lst_triv0 [where i=1])
    case False
    then consider (0) "α=0" | (1) "α=1"
      by (metis Ord_0 OrdmemD True Ord α mem_0_Ord one_V_def order.antisym succ_le_iff)
    then show ?thesis
    proof cases
      case 0
      with part show ?thesis
        by (force simp add: partn_lst_def nsets_empty_iff less_Suc_eq)
      case 1
      then obtain "Ord β"
        by (meson ON_imp_Ord Ord_ω1 True β elts_subset_ON)
      then obtain i where "i < Suc (Suc 0)" "[ord_of_nat k, γ] ! i  α"
        using partn_lst_VWF_nontriv [OF part] 1 by auto
      then have "γ  1"
        using α=1 k > 1 by (fastforce simp: less_Suc_eq)
      then have "min γ (ω*β)  1"
        by (metis Ord_1 Ord_ω Ord_linear_le Ord_mult Ord β min_def order_trans)
      then show ?thesis
        using False by (auto simp: True Ord β β0 α=1 intro!: partn_lst_triv1 [where i=1])
  case False
  then have "α  ω"
    by (meson Ord_1 Ord_not_less indec indecomposable_def indecomposable_imp_Limit omega_le_Limit)
  have "0  elts β" "β  0"
    using False Ord_ω1 Ord_in_Ord β mem_0_Ord by blast+
  show ?thesis
    unfolding partn_lst_def
  proof clarsimp
    fix f
    assume "f  [elts (α*β)]⇗2 {..<Suc (Suc 0)}"
    then have f: "f  [elts (α*β)]⇗2 {..<2::nat}"
      by (simp add: eval_nat_numeral)
    obtain ord [iff]: "Ord α" "Ord β" "Ord (α*β)"
      using Ord_ω1 Ord_in_Ord β indec indecomposable_imp_Ord Ord_mult by blast
    have *: False
      if i [rule_format]: "H. tp H = ord_of_nat (2*k)  H  elts (α*β)  ¬ f ` [H]⇗2 {0}"
        and ii [rule_format]: "H. tp H = γ  H  elts (α*β)  ¬ f ` [H]⇗2 {1}"
        and iii [rule_format]: "H. tp H = (ω*β)  H  elts (α*β)  ¬ f ` [H]⇗2 {1}"
    proof -
      have Ak0: "X  [A]⇗k. f ` [X]⇗2 {0}" ―‹remark (8) about @{term"A  S"}
        if A_αβ: "A  elts (α*β)" and ot: "tp A  α" for A
      proof -
        let ?g = "inv_into A (ordermap A VWF)"
        have "small A"
          using down that by auto
        then have inj_g: "inj_on ?g (elts α)"
          by (meson inj_on_inv_into less_eq_V_def ordermap_surj ot subset_trans)
        have om_A_less: "x y. x  A; y  A; x < y  ordermap A VWF x < ordermap A VWF y"
          using ord
          by (meson A_αβ Ord_in_Ord VWF_iff_Ord_less small A in_mono ordermap_mono_less trans_VWF wf_VWF)
        have α_sub: "elts α  ordermap A VWF ` A"
          by (metis small A elts_of_set less_eq_V_def ordertype_def ot replacement)
        have g: "?g  elts α  elts (α*β)"
          by (meson A_αβ Pi_I' α_sub inv_into_into subset_eq)
        then have fg: "f  (λX. ?g ` X)  [elts α]⇗2 {..<2}"
          by (rule nsets_compose_image_funcset [OF f _ inj_g])
        obtain i H where "i < 2" "H  elts α"
          and ot_eq: "tp H = [k,γ]!i" "(f  (λX. ?g ` X)) ` (nsets H 2)  {i}"
          using ii partn_lst_E [OF part fg] by (auto simp: eval_nat_numeral)
        then consider (0) "i=0" | (1) "i=1"
          by linarith
        then show ?thesis
        proof cases
          case 0
          then have "f ` [inv_into A (ordermap A VWF) ` H]⇗2 {0}"
            using ot_eq H  elts α α_sub by (auto simp: nsets_def [of _ k] inj_on_inv_into elim!: nset_image_obtains)
          moreover have "finite H  card H = k"
            using 0 ot_eq H  elts α down by (simp add: finite_ordertype_eq_card)
          then have "inv_into A (ordermap A VWF) ` H  [A]⇗k⇖"
            using H  elts α α_sub by (auto simp: nsets_def [of _ k] card_image inj_on_inv_into inv_into_into)
          ultimately show ?thesis
            by blast
          case 1
          have gH: "?g ` H  elts (α*β)"
            by (metis A_αβ α_sub H  elts α image_subsetI inv_into_into subset_eq)
          have g_less: "?g x < ?g y" if "x < y" "x  elts α" "y  elts α" for x y
            using Pi_mem [OF g] ord that
            by (meson A_αβ Ord_in_Ord Ord_not_le small A dual_order.trans elts_subset_ON inv_ordermap_VWF_mono_le ot vsubsetD)
          have [simp]: "tp (?g ` H) = tp H"
            by (meson H  elts α ord down dual_order.trans elts_subset_ON gH g_less ordertype_VWF_inc_eq subsetD)
          show ?thesis
            using ii [of "?g ` H"] subset_inj_on [OF inj_g H  elts α] ot_eq 1 
            by (auto simp: gH elim!: nset_image_obtains)
      define K where "K  λi x. {y  elts (α*β). x  y  f{x,y} = i}"
      have small_K: "small (K i x)" for i x
        by (simp add: K_def)
      define KI where "KI  λi X. (xX. K i x)"
      have KI_disj_self: "X  KI i X = {}" for i X
        by (auto simp: KI_def K_def)
      define M where "M  λD 𝔄 x. {ν::V. ν  D  tp (K 1 x  𝔄 ν)  α}"
      have M_sub_D: "M D 𝔄 x  D" for D 𝔄 x
        by (auto simp: M_def)
      have small_M [simp]: "small (M D 𝔄 x)" if "small D" for D 𝔄 x
        by (simp add: M_def that)
      have 9: "tp {x  A. tp (M D 𝔄 x)  tp D}  α" (is "ordertype ?AD _  α")
        if inD: "indecomposable (tp D)" and D: "D  elts β" and A: "A  elts (α*β)" and tpA: "tp A = α"
          and 𝔄: "𝔄  D  {X. X  elts (α*β)  tp X = α}"  for D A 𝔄
          ―‹remark (9), assuming an indecomposable order type›
      proof (rule ccontr)
        define A' where "A'  {x  A. ¬ tp (M D 𝔄 x)  tp D}"
        have small [iff]: "small A" "small D"
          using A D down by (auto simp: M_def)
        have small_𝔄: "small (𝔄 δ)" if "δ  D" for δ
          using that 𝔄 by (auto simp: Pi_iff subset_iff_less_eq_V)
        assume not_α_le: "¬ α  tp {x  A. tp (M D 𝔄 x)  tp D}"
        obtain "small A" "small A'" "A'  A" and A'_sub: "A'  elts (α*β)"
          using A'_def A down by auto
        moreover have "A' = A - ?AD"
          by (force simp: A'_def)
        ultimately have A'_ge: "tp A'  α"
          by (metis (no_types, lifting) dual_order.refl indec indecomposable_ordertype_eq mem_Collect_eq subsetI tpA)
        obtain X where "X  A'" "finite X" "card X = k" and fX0: "f ` [X]⇗2 {0}"
          using Ak0 [OF A'_sub A'_ge] by (auto simp: nsets_def [of _ k])
        then have : "¬ tp (M D 𝔄 x)  tp D" if "x  X" for x
          using that by (auto simp: A'_def)
        obtain x where "x  X"
          using card X = k k>1 by fastforce
        have "¬ D  ( xX. M D 𝔄 x)"
          assume not: "D  (xX. M D 𝔄 x)"
          have "XM D 𝔄 ` X. tp D  tp X"
          proof (rule indecomposable_ordertype_finite_ge [OF inD])
            show "M D 𝔄 ` X  {}"
              using A'_def A'_ge not not_α_le by auto
            show "small ( (M D 𝔄 ` X))"
              using finite X by (simp add: finite_imp_small)
          qed (use finite X not in auto)
          then show False
            by (simp add: )
        then obtain ν where "ν  D" and ν: "ν  ( xX. M D 𝔄 x)"
          by blast
        define 𝒜 where "𝒜  {KI 0 X  𝔄 ν, xX. K 1 x  𝔄 ν, X  𝔄 ν}"
        have αβ: "X  elts (α*β)" "𝔄 ν  elts (α*β)"
          using A'_sub X  A' 𝔄 ν  D by auto
        then have "KI 0 X  (xX. K 1 x)  X = elts (α*β)"
          using x  X f by (force simp: K_def KI_def Pi_iff less_2_cases_iff)
        with αβ have 𝔄ν_𝒜: "finite 𝒜" "𝔄 ν  𝒜"
          by (auto simp: 𝒜_def)
        then have "¬ tp (K 1 x  𝔄 ν)  α" if "x  X" for x
          using that ν  D ν k > 1 card X = k by (fastforce simp: M_def)
        moreover have sm_K1: "small (xX. K 1 x  𝔄 ν)"
          by (meson Finite_V Int_lower2 ν  D finite X small_𝔄 small_UN smaller_than_small)
        ultimately have not1: "¬ tp (xX. K 1 x  𝔄 ν)  α"
          using finite X x  X indecomposable_ordertype_finite_ge [OF indec, of "(λx. K 1 x  𝔄 ν) ` X"] by blast
        moreover have "¬ tp (X  𝔄 ν)  α"
          using finite X α  ω
          by (meson finite_Int mem_not_refl ordertype_VWF_ω vsubsetD)
        moreover have "α  tp (𝔄 ν)"
          using 𝔄 ν  D small_𝔄 by fastforce+
        moreover have "small ( 𝒜)"
          using ν  D small_𝔄 by (fastforce simp: 𝒜_def intro: smaller_than_small sm_K1)
        ultimately have K0𝔄_ge: "tp (KI 0 X  𝔄 ν)  α"
          using indecomposable_ordertype_finite_ge [OF indec 𝔄ν_𝒜] by (auto simp: 𝒜_def)
        have 𝔄ν: "𝔄 ν  elts (α*β)" "tp (𝔄 ν) = α"
          using ν  D 𝔄 by blast+
        then obtain Y where Ysub: "Y  KI 0 X  𝔄 ν" and "finite Y" "card Y = k" and fY0: "f ` [Y]⇗2 {0}"
          using Ak0 [OF _ K0𝔄_ge] by (auto simp: nsets_def [of _ k])
        have : "X  Y = {}"
          using Ysub KI_disj_self by blast
        then have "card (X  Y) = 2*k"
          by (simp add: card X = k card Y = k finite X finite Y card_Un_disjoint)
        moreover have "X  Y  elts (α*β)"
          using A'_sub X  A' 𝔄ν(1) Y  KI 0 X  𝔄 ν by auto
        moreover have "f ` [X  Y]⇗2 {0}"
          using fX0 fY0 Ysub by (auto simp:  nsets_disjoint_2 image_Un image_UN KI_def K_def)
        ultimately show False
          using i finite X finite Y ordertype_VWF_finite_nat by auto
      have IX: "tp {x  A. tp (M D 𝔄 x)  tp D}  α"
        if D: "D  elts β" and A: "A  elts (α*β)" and tpA: "tp A = α"
          and 𝔄: "𝔄  D  {X. X  elts (α*β)  tp X = α}" for D A 𝔄
          ―‹remark (9) for any order type›
      proof -
        obtain L where UL: "(List.set L)  D"
          and indL: "X. X  List.set L  indecomposable (tp X)"
          and eqL: "M. M  D; X. X  List.set L  tp (M  X)  tp X  tp M = tp D"
          using ord by (metis strong_ordertype_eq D order_refl)
        obtain A'' where A'': "A''  A" "tp A''  α"
          and "x X. x  A''; X  List.set L  tp (M D 𝔄 x  X)  tp X"
          using UL indL
        proof (induction L arbitrary: thesis)
          case (Cons X L)
          then obtain A'' where A'': "A''  A" "tp A''  α" and "X  D"
            and ge_X: "x X. x  A''; X  List.set L  tp (M D 𝔄 x  X)  tp X" by auto
          then have tp_A'': "tp A'' = α"
            by (metis A antisym down ordertype_VWF_mono tpA)
          have ge_α: "tp {x  A''. tp (M X 𝔄 x)  tp X}  α"
            by (rule 9) (use A A'' tp_A'' Cons.prems D  elts β X  D 𝔄 in auto)
          let ?A = "{x  A''. tp (M D 𝔄 x  X)  tp X}"
          have M_eq: "M D 𝔄 x  X = M X 𝔄 x" if "x  A''" for x
            using that X  D by (auto simp: M_def)
          show thesis
          proof (rule Cons.prems)
            show "α  tp ?A"
              using ge_α by (simp add: M_eq cong: conj_cong)
            show "tp Y  tp (M D 𝔄 x  Y)" if "x  ?A" "Y  list.set (X # L)" for x Y
              using that ge_X by force
          qed (use A'' in auto)
        qed (use tpA in auto)
        then have tp_M_ge: "tp (M D 𝔄 x)  tp D" if "x  A''" for x
          using eqL that by (auto simp: M_def)
        have "α  tp A''"
          by (simp add: A'')
        also have "  tp {x  A''. tp (M D 𝔄 x)  tp D}"
          by (metis (mono_tags, lifting) tp_M_ge eq_iff mem_Collect_eq subsetI)
        also have "  tp {x  A. tp D  tp (M D 𝔄 x)}"
          by (rule ordertype_mono) (use A'' A down in auto)
        finally show ?thesis .
      have IX': "tp {x  A'. tp (K 1 x  A)  α}  α"
        if A: "A  elts (α*β)" "tp A = α" and A': "A'  elts (α*β)" "tp A' = α" for A A'
      proof -
        have : "α  tp (K 1 t  A)" if "1  tp {ν. ν = 0  α  tp (K 1 t  A)}" for t
          using that
          by (metis Collect_empty_eq less_eq_V_0_iff ordertype_empty zero_neq_one)
        have "tp {x  A'. 1  tp {ν. ν = 0  α  tp (K 1 x  A)}}
             tp {x  A'. α  tp (K 1 x  A)}"
          by (rule ordertype_mono) (use "" A' in auto simp: down)
        then show ?thesis
          using IX [of "{0}" A' "λx. A"] that 0  elts β by (force simp: M_def)

      have 10: "x0  A. g  elts β  elts β. strict_mono_on (elts β) g  (ν  F. g ν = ν)
                                       (ν  elts β. tp (K 1 x0  𝔄 (g ν))  α)"
        if F: "finite F" "F  elts β"
          and A: "A  elts (α*β)" "tp A = α"
          and 𝔄: "𝔄  elts β  {X. X  elts (α*β)  tp X = α}"
        for F A 𝔄
      proof -
        define p where "p  card F"
        have "β  F"
          using that by auto
        then obtain ι :: "nat  V" where bijι: "bij_betw ι {..p} (insert β F)" and monι: "strict_mono_on {..p} ι"
          using ZFC_Cardinals.ex_bij_betw_strict_mono_card [of "insert β F"] elts_subset_ON Ord β F
          by (simp add: p_def lessThan_Suc_atMost) blast
        have less_ι_I: "ι k < ι l" if "k < l" "l  p" for k l
          using monι that by (auto simp: strict_mono_on_def)
        then have less_ι_D: "k < l" if "ι k < ι l" "k  p" for k l
          by (metis less_asym linorder_neqE_nat that)
        have Ord_ι: "Ord (ι k)" if "k  p" for k
          by (metis (no_types, lifting) ON_imp_Ord atMost_iff insert_subset mem_Collect_eq order_trans  F  elts β bijι bij_betwE elts_subset_ON Ord β that)
        have le_ι0 [simp]: "j. j  p  ι 0  ι j"
          by (metis eq_refl leI le_0_eq less_ι_I less_imp_le)
        have le_ι: "ι i  ι (j - Suc 0)" if "i < j" "j  p" for i j
        proof (cases i)
          case 0 then show ?thesis
            using le_ι0 that by auto
          case (Suc i') then show ?thesis
            by (metis (no_types, opaque_lifting) Suc_pred le_less less_Suc_eq less_Suc_eq_0_disj less_ι_I not_less_eq that)

        have [simp]: "ι p = β"
        proof -
          obtain k where k: "ι k = β" "k  p"
            by (meson atMost_iff bijι bij_betw_iff_bijections insertI1)
          then have "k = p  k < p"
            by linarith
          then show ?thesis
            using bijι ord k that(2)
            by (metis OrdmemD atMost_iff bij_betw_iff_bijections insert_iff leD less_ι_D order_refl subsetD)

        have F_imp_Ex: "k < p. ξ = ι k" if "ξ  F" for ξ
        proof -
          obtain k where k: "k  p" "ξ = ι k"
            by (metis ξ  F atMost_iff bijι bij_betw_def imageE insert_iff)
          then show ?thesis
            using β  F ι p = β le_imp_less_or_eq that by blast
        have F_imp_ge: "ξ  ι 0" if "ξ  F" for ξ
          using F_imp_Ex [OF that] by (metis dual_order.order_iff_strict le0 less_ι_I)
        define D where "D  λk. (if k=0 then {..<ι 0} else {ι (k-1)<..<ι k})  elts β"
        have : "D k  elts β" for k
          by (auto simp: D_def)
        then have small_D [simp]: "small (D k)" for k
          by (meson down)
        have M_Int_D: "M (elts β) 𝔄 x  D k = M (D k) 𝔄 x" if "k  p" for x k
          using  by (auto simp: M_def)
        have ι_le_if_D: "ι k  μ" if "μ  D (Suc k)" for μ k
          using that by (simp add: D_def order.order_iff_strict)
        have mono_D: "D i  D j" if "i < j" "j  p" for i j
        proof (cases j)
          case (Suc j')
          with that show ?thesis
            apply (simp add: less_sets_def D_def Ball_def)
            by (metis One_nat_def diff_Suc_1 le_ι less_le_trans less_trans)
        qed (use that in auto)
        then have disjnt_DD: "disjnt (D i) (D j)" if "i  j" "i  p" "j  p" for i j
          by (meson disjnt_sym less_linear less_sets_imp_disjnt that)
        have UN_D_eq: "(l  k. D l) = {..<ι k}  (elts β - F)" if "k  p" for k
          using that
        proof (induction k)
          case 0
          then show ?case
            by (auto simp: D_def F_imp_ge leD)
          case (Suc k)
          have "D (Suc k)  {..<ι k}  (elts β - F) = {..<ι (Suc k)}  (elts β - F)"
            (is "?lhs = ?rhs")
            show "?lhs  ?rhs"
              using Suc.prems
              by (auto simp: D_def if_split_mem2 intro: less_ι_I less_trans dest!: less_ι_D F_imp_Ex)
            have "x. x < ι (Suc k); x  elts β; x  F; ι k  x  ι k < x"
              using Suc.prems F  elts β bijι le_imp_less_or_eq
              by (fastforce simp: bij_betw_iff_bijections)
            then show "?rhs  ?lhs"
              using Suc.prems by (auto simp: D_def Ord_not_less Ord_in_Ord [OF Ord β] Ord_ι if_split_mem2)
          show ?case
            using Suc by (simp add: atMost_Suc)
        have β_decomp: "elts β = F  (k  p. D k)"
          using F  elts β OrdmemD [OF Ord β] by (auto simp: UN_D_eq)
        define βidx where "βidx  λν. @k. ν  D k  k  p"
        have βidx: "ν  D (βidx ν)  βidx ν  p" if "ν  elts β - F" for ν
          using that by (force simp: βidx_def β_decomp intro: someI_ex del: conjI)
        have any_imp_βidx: "k = βidx ν" if "ν  D k" "k  p" for k ν
        proof (rule ccontr)
          assume non: "k  βidx ν"
          have "ν  F"
            using that UN_D_eq by auto
          then show False
            using disjnt_DD [OF non] by (metis  Diff_iff βidx disjnt_iff subsetD that)
        have "A'. A'  A  tp A' = α  (x  A'. F  M (elts β) 𝔄 x)"
          using F
        proof induction
          case (insert ν F)
          then obtain A' where "A'  A" and A': "A'  elts (α*β)" "tp A' = α" and FN: "x. x  A'  F  M (elts β) 𝔄 x"
            using A(1) by auto
          define A'' where "A''  {x  A'. α  tp (K 1 x  𝔄 ν)}"
          have "ν  elts β" "F  elts β"
            using insert by auto
          note ordertype_eq_Ord [OF Ord β, simp]
          show ?case
          proof (intro exI conjI)
            show "A''  A"
              using A'  A by (auto simp: A''_def)
            show "tp A'' = α"
            proof (rule antisym)
              show "tp A''  α"
                using A''  A down ordertype_VWF_mono A by blast
              have "𝔄 ν  elts (α*β)" "tp (𝔄 ν) = α"
                using 𝔄 ν  elts β by auto
              then show "α  tp A''"
                using IX' [OF _ _ A'] by (simp add: A''_def)
            show "xA''. insert ν F  M (elts β) 𝔄 x"
              using A''_def FN M_def ν  elts β by blast
        qed (use A in auto)
        then obtain A' where A': "A'  A" "tp A' = α" and FN: "x. x  A'  F  M (elts β) 𝔄 x"
          by metis
        have False
          if *: "x0 g. x0  A; g  elts β  elts β; strict_mono_on (elts β) g
                    (νF. g ν  ν)  (νelts β. tp (K 1 x0  𝔄 (g ν)) < α)"
        proof -
          { fix x       ― ‹construction of the monotone map @{term g} mentioned above›
            assume "x  A'"
            with A' have "x  A" by blast
            have "k. k  p  tp (M (D k) 𝔄 x) < tp (D k)" (is "?P")
            proof (rule ccontr)
              assume "¬ ?P"
              then have le: "tp (D k)  tp (M (D k) 𝔄 x)" if "k  p" for k
                by (meson Ord_linear2 Ord_ordertype that)
              have "fD k  M (D k) 𝔄 x. inj_on f (D k)  (strict_mono_on (D k) f)"
                if "k  p" for k
                using le [OF that] that VWF_iff_Ord_less
                apply (clarsimp simp: ordertype_le_ordertype strict_mono_on_def)
                by (metis (full_types)  M_sub_D Ord_in_Ord PiE VWF_iff_Ord_less ord(2) subsetD)
              then obtain h where fun_h: "k. k  p  h k  D k  M (D k) 𝔄 x"
                and inj_h: "k. k  p  inj_on (h k) (D k)"
                and mono_h: "k x y. k  p  strict_mono_on (D k) (h k)"
                by metis
              then have fun_hD: "k. k  p  h k  D k  D k"
                by (auto simp: M_def)
              have h_increasing: "ν  h k ν"
                if "k  p" "ν  D k" for k ν 
                by (meson  Ord_mono_imp_increasing ord dual_order.trans elts_subset_ON fun_hD mono_h that)
              define g where "g  λν. if ν  F then ν else h (βidx ν) ν"
              have [simp]: "g ν = ν" if "ν  F" for ν
                using that by (auto simp: g_def)
              have fun_g: "g  elts β  elts β"
              proof (rule Pi_I)
                fix x assume "x  elts β"
                then have "x  D (βidx x)" "βidx x  p" if "x  F"
                  using that by (auto simp: βidx)
                then show "g x  elts β"
                  by (metis fun_h  M_sub_D x  elts β PiE g_def subsetD)
              have h_in_D: "h (βidx ν) ν  D (βidx ν)" if "ν  F" "ν  elts β" for ν
                using βidx fun_hD that by fastforce
              have 1: "ι k < h (βidx ν) ν"
                if "k < p" and ν: "ν  F" "ν  elts β" and "ι k < ν" for k ν
                by (meson that h_in_D [OF ν] βidx DiffI h_increasing order_less_le_trans)
              moreover have 2: "h (βidx μ) μ < ι k"
                if μ: "μ  F" "μ  elts β" and "k < p" "μ < ι k" for μ k
              proof -
                have "βidx μ  k"
                proof (rule ccontr)
                  assume "¬ βidx μ  k"
                  then have "k < βidx μ"
                    by linarith
                  then show False
                    using ι_le_if_D βidx that by (metis Diff_iff Suc_pred le0 leD le_ι le_less_trans)
                then show ?thesis
                  using that h_in_D [OF μ]
                  by (smt (verit, best) Int_lower1 UN_D_eq UN_I atMost_iff lessThan_iff less_imp_le subset_eq)
              moreover have "h (βidx μ) μ < h (βidx ν) ν"
                if μ: "μ  F" "μ  elts β" and ν: "ν  F" "ν  elts β" and "μ < ν" for μ ν
              proof -
                have le: "βidx μ  βidx ν" if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)"
                  by (metis 2 DiffI βidx μ ν μ < ν order.strict_trans h_increasing leI le_ι order_less_asym order_less_le_trans that)
                have "h 0 μ < h 0 ν" if "βidx μ = 0" "βidx ν = 0"
                  using that mono_h unfolding strict_mono_on_def
                  by (metis Diff_iff βidx μ ν μ < ν)
                moreover have "h 0 μ < h (βidx ν) ν"
                  if "0 < βidx ν" "h 0 μ < ι 0" and "ι (βidx ν - Suc 0) < h (βidx ν) ν"
                  by (meson DiffI βidx ν le_ι le_less_trans less_le_not_le that)
                moreover have "βidx ν  0"
                  if "0 < βidx μ" "h 0 ν < ι 0" "ι (βidx μ - Suc 0) < h (βidx μ) μ"
                  using le le_0_eq that by fastforce
                moreover have "h (βidx μ) μ < h (βidx ν) ν"
                  if "ι (βidx μ - Suc 0) < h (βidx μ) μ" "h (βidx ν) ν < ι (βidx ν)"
                    "h (βidx μ) μ < ι (βidx μ)" "ι (βidx ν - Suc 0) < h (βidx ν) ν"
                  using mono_h unfolding strict_mono_on_def
                  by (metis le Diff_iff βidx μ ν μ < ν le_ι le_less le_less_trans that)
                ultimately show  ?thesis
                  using h_in_D [OF μ] h_in_D [OF ν] by (simp add: D_def split: if_split_asm)
              ultimately have sm_g: "strict_mono_on (elts β) g"
                by (auto simp: g_def strict_mono_on_def dest!: F_imp_Ex)
              have False if "ν  elts β" and ν: "tp (K 1 x  𝔄 (g ν)) < α" for ν
              proof -
                have "F  M (elts β) 𝔄 x"
                  by (meson FN x  A')
                then have False if "tp (K (Suc 0) x  𝔄 ν) < α" "ν  F"
                  using that by (auto simp: M_def)
                moreover have False if "tp (K (Suc 0) x  𝔄 (g ν)) < α" "ν  D k" "k  p" "ν  F" for k
                proof -
                  have "h (βidx ν) ν  M (D (βidx ν)) 𝔄 x"
                    using fun_h βidx ν  elts β ν  F by auto
                  then show False
                    using that by (simp add: M_def g_def leD)
                ultimately show False
                  using ν  elts β ν by (force simp: β_decomp)
              then show False
                using * [OF x  A fun_g sm_g] by auto
            then have "l. l  p  tp (M (elts β) 𝔄 x  D l) < tp (D l)"
              using M_Int_D by auto
          then obtain l where lp: "x. x  A' l x  p"
            and lless: "x. x  A' tp (M (elts β) 𝔄 x  D (l x)) < tp (D (l x))"
            by metis
          obtain A'' L where "A''  A'" and A'': "A''  elts (α*β)" "tp A'' = α" and lL: "x. x  A''  l x = L"
          proof -
            have eq: "A' = (ip. {x  A'. l x = i})"
              using lp by auto
            have "X(λi. {x  A'. l x = i}) ` {..p}. α  tp X"
            proof (rule indecomposable_ordertype_finite_ge [OF indec])
              show "small (ip. {x  A'. l x = i})"
                by (metis A'(1) A(1) eq down smaller_than_small)
            qed (use A' eq in auto)
            then show thesis
              fix A''
              assume A'': "A''  (λi. {x  A'. l x = i}) ` {..p}" and "α  tp A''"
              then obtain L where L: "x. x  A''  l x = L"
                by auto
              have "A''  A'"
                using A'' by force
              then have "tp A''  tp A'"
                by (meson A' A down order_trans ordertype_VWF_mono)
              with α  tp A'' have "tp A'' = α"
                using A'(2) by auto
              moreover have "A''  elts (α*β)"
                using A' A A''  A' by auto
              ultimately show thesis
                using L that [OF A''  A'] by blast
          have 𝔄D: "𝔄  D L  {X. X  elts (α*β)  tp X = α}"
            using 𝔄  by blast
          have α: "α  tp {x  A''. tp (D L)  tp (M (D L) 𝔄 x)}"
            using IX [OF  A'' 𝔄D] by simp
          have "M (elts β) 𝔄 x  D L = M (D L) 𝔄 x" for x
            using  by (auto simp: M_def)
          then have "tp (M (D L) 𝔄 x) < tp (D L)" if "x  A''" for x
            using lless that A''  A' lL by force
          then have [simp]: "{x  A''. tp (D L)  tp (M (D L) 𝔄 x)} = {}"
            using leD by blast
          show False
            using α α  ω by simp
        then show ?thesis
          by (meson Ord_linear2 Ord_ordertype Ord α)
      let ?U = "UNIV :: nat set"
      define μ where "μ  fst  from_nat_into (elts β × ?U)"
      define q where "q  to_nat_on (elts β × ?U)"
      have co_βU: "countable (elts β × ?U)"
        by (simp add: β less_ω1_imp_countable)
      moreover have "elts β × ?U  {}"
        using 0  elts β by blast
      ultimately have "range (from_nat_into (elts β × ?U)) = (elts β × ?U)"
        by (metis range_from_nat_into)
      then have μ_in_β [simp]: "μ i  elts β" for i
        by (metis SigmaE μ_def comp_apply fst_conv range_eqI)

      then have Ord_μ [simp]: "Ord (μ i)" for i
        using Ord_in_Ord by blast

      have inf_βU: "infinite (elts β × ?U)"
        using 0  elts β finite_cartesian_productD2 by auto

      have 11 [simp]: "μ (q (ν,n)) = ν" if "ν  elts β" for ν n
        by (simp add: μ_def q_def that co_βU)
      have range_μ [simp]: "range μ = elts β"
        by (auto simp: image_iff) (metis 11)
      have [simp]: "KI i {} = UNIV" "KI i (insert a X) = K i a  KI i X" for i a X
        by (auto simp: KI_def)
      define Φ where "Φ  λn::nat. λ𝔄 x. (ν  elts β. 𝔄 ν  elts (α*β)  tp (𝔄 ν) = α)
                                         x ` {..<n}  elts (α*β)
                                         (ν  elts β. 𝔄 ν)  KI 1 (x ` {..<n}) 
                                         strict_mono_sets (elts β) 𝔄"
      define Ψ where "Ψ  λn::nat. λg 𝔄 𝔄' xn. g  elts β  elts β  strict_mono_on (elts β) g
                   (in. g (μ i) = μ i)
                   (ν  elts β. 𝔄' ν  K 1 xn  𝔄 (g ν))
                   {xn}  (𝔄' (μ n))  xn  𝔄 (μ n)"
      let ?𝔄0 = "λν. plus (α * ν) ` elts α"
      have base: "Φ 0 ?𝔄0 x" for x
        by (auto simp: Φ_def add_mult_less add_mult_less_add_mult ordertype_image_plus strict_mono_sets_def less_sets_def)
      have step: "Ex (λ(g,𝔄',xn). Ψ n g 𝔄 𝔄' xn  Φ (Suc n) 𝔄' (x(n:=xn)))" if "Φ n 𝔄 x" for n 𝔄 x
      proof -
        have 𝔄: "ν. ν  elts β  𝔄 ν  elts (α*β)  tp (𝔄 ν) = α"
          and x: "x ` {..<n}  elts (α*β)"
          and sub: " (𝔄 ` elts β)  KI (Suc 0) (x ` {..<n})"
          and sm: "strict_mono_sets (elts β) 𝔄"
          and μβ: "μ ` {..n}  elts β" and 𝔄sub: "𝔄 (μ n)  elts (α*β)"
          and 𝔄fun: "𝔄  elts β  {X. X  elts (α*β)  tp X = α}"
          using that by (auto simp: Φ_def)
        then obtain xn g where xn: "xn  𝔄 (μ n)" and g: "g  elts β  elts β"
          and sm_g: "strict_mono_on (elts β) g" and g_μ: "ν  μ`{..n}. g ν = ν"
          and g_α: "ν  elts β. α  tp (K 1 xn  𝔄 (g ν))"
          using 10 [OF _ μβ 𝔄sub _ 𝔄fun] by (auto simp: 𝔄)
        have tp1: "tp (K 1 xn  𝔄 (g ν)) = α" if "ν  elts β" for ν
          by (metis antisym Int_lower2 PiE 𝔄 down g g_α ordertype_VWF_mono that)
        have tp2: "tp (𝔄 (μ n)) = α"
          by (auto simp: 𝔄)
        obtain "small (𝔄 (μ n))" "𝔄 (μ n)  ON"
          by (meson 𝔄sub ord down elts_subset_ON subset_trans)
        then obtain A2 where A2: "tp A2 = α" "A2  K 1 xn  𝔄 (μ n)" "{xn}  A2"
          using indecomposable_imp_Ex_less_sets [OF indec α  ω tp2]
          by (metis μ_in_β atMost_iff image_eqI inf_le2 le_refl xn tp1 g_μ)
        then have A2_sub: "A2  𝔄 (μ n)" by simp
        let ?𝔄 = "λν. if ν = μ n then A2 else K 1 xn  𝔄 (g ν)"
        have [simp]: "({..<Suc n}  {x. x  n}) = ({..<n})"
          by auto
        have "K (Suc 0) xn  (xelts β  {ν. ν  μ n}. 𝔄 (g x))  KI (Suc 0) (x ` {..<n})"
          using sub g by (auto simp: KI_def)
        moreover have "A2  KI (Suc 0) (x ` {..<n})" "A2  elts (α*β)" "xn  elts (α*β)"
          using 𝔄sub sub A2 xn by fastforce+
        moreover have "strict_mono_sets (elts β) ?𝔄"
          using sm sm_g g g_μ A2_sub
          unfolding strict_mono_sets_def strict_mono_on_def less_sets_def Pi_iff subset_iff Ball_def Bex_def image_iff
          by (simp (no_asm_use) add: if_split_mem2) (smt order_refl)
        ultimately have "Φ (Suc n) ?𝔄 (x(n := xn))"
          using tp1 x A2 by (auto simp: Φ_def K_def)
        with A2 show ?thesis
          by (rule_tac x="(g,?𝔄,xn)" in exI) (simp add: Ψ_def g sm_g g_μ xn)
      define G where "G  λn 𝔄 x. @(g,𝔄',x'). xn. Ψ n g 𝔄 𝔄' xn  x' = (x(n:=xn))  Φ (Suc n) 𝔄' x'"
      have : "(λ(g,𝔄',x'). Φ (Suc n) 𝔄' x') (G n 𝔄 x)"
        and : "(λ(g,𝔄',x'). Ψ n g 𝔄 𝔄' (x' n)) (G n 𝔄 x)"  if "Φ n 𝔄 x" for n 𝔄 x
        using step [OF that] by (force simp: G_def dest: some_eq_imp)+
      define H where "H  rec_nat (id,?𝔄0,undefined) (λn (g0,𝔄,x0). G n 𝔄 x0)"
      have "(λ(g,𝔄,x). Φ n 𝔄 x) (H n)" for n
        unfolding H_def by (induction n) (use  base in fastforce)+
      then have H_imp_Φ: "Φ n 𝔄 x" if "H n = (g,𝔄,x)" for g 𝔄 x n
        by (metis case_prodD that)
      then have H_imp_Ψ: "(λ(g,𝔄',x'). let (g0,𝔄,x) = H n in Ψ n g 𝔄 𝔄' (x' n)) (H (Suc n))" for n
        using  by (fastforce simp: H_def split: prod.split)
      define g where "g  λn. (λ(g,𝔄,x). g) (H (Suc n))"
      have g: "g n  elts β  elts β" and sm_g: "strict_mono_on (elts β) (g n)"
        and 13: "i. in  g n (μ i) = μ i" for n
        using H_imp_Ψ [of n] by (auto simp: g_def Ψ_def)
      define 𝔄 where "𝔄  λn. (λ(g,𝔄,x). 𝔄) (H n)"
      define x where "x  λn. (λ(g,𝔄,x). x n) (H (Suc n))"
      have 14: "𝔄 (Suc n) ν  K 1 (x n)  𝔄 n (g n ν)" if "ν  elts β" for ν n
        using H_imp_Ψ [of n] that by (force simp: Ψ_def 𝔄_def x_def g_def)
      then have x14: "𝔄 (Suc n) ν  𝔄 n (g n ν)" if "ν  elts β" for ν n
        using that by blast
      have 15: "x n  𝔄 n (μ n)" and 16: "{x n}  (𝔄 (Suc n) (μ n))" for n
        using H_imp_Ψ [of n] by (force simp: Ψ_def 𝔄_def x_def)+
      have 𝔄_αβ: "𝔄 n ν  elts (α*β)" if "ν  elts β" for ν n
        using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split)
      have 12: "strict_mono_sets (elts β) (𝔄 n)" for n
        using H_imp_Φ [of n] that by (auto simp: Φ_def 𝔄_def split: prod.split)
      let ?Z = "range x"
      have S_dec: " (𝔄 (m+k) ` elts β)   (𝔄 m ` elts β)" for k m
        by (induction k) (use 14 g in fastforce+)
      have "x n  K 1 (x m)" if "m<n" for m n
      proof -
        have "x n  (ν  elts β. 𝔄 n ν)"
          by (meson "15" UN_I μ_in_β)
        also have "  (ν  elts β. 𝔄 (Suc m) ν)"
          using S_dec [of "Suc m"] less_iff_Suc_add that by auto
        also have "  K 1 (x m)"
          using 14 by auto
        finally show ?thesis .
      then have "f{x m, x n} = 1" if "m<n" for m n
        using that by (auto simp: K_def)
      then have Z_K1: "f ` [?Z]⇗2 {1}"
        by (clarsimp simp: nsets_2_eq) (metis insert_commute less_linear)
      moreover have Z_sub: "?Z  elts (α*β)"
        using "15" 𝔄_αβ μ_in_β by blast
      moreover have "tp ?Z  ω * β"
      proof -
        define 𝔤 where "𝔤  λi j x. wfrec (measure (λk. j-k)) (λ𝔤 k. if k<j then g k (𝔤 (Suc k)) else x) i"
        have 𝔤: "𝔤 i j x = (if i<j then g i (𝔤 (Suc i) j x) else x)" for i j x
          by (simp add: 𝔤_def wfrec cut_apply)
        have 17: "𝔤 k j (μ i) = μ i" if "i  k" for i j k
          using wf_measure [of "λk. j-k"] that
          by (induction k rule: wf_induct_rule) (simp add: "13" 𝔤 le_imp_less_Suc)
        have 𝔤_in_β: "𝔤 i j ν   elts β" if "ν  elts β" for i j ν
          using wf_measure [of "λk. j-k"] that
        proof (induction i rule: wf_induct_rule)
          case (less i)
          with g show ?case by (force simp: 𝔤 [of i])
        then have 𝔤_fun: "𝔤 i j  elts β  elts β" for i j
          by simp
        have sm_𝔤: "strict_mono_on (elts β) (𝔤 i j)" for i j
          using wf_measure [of "λk. j-k"]
        proof (induction i rule: wf_induct_rule)
          case (less i)
          with sm_g show ?case
            by (auto simp: 𝔤 [of i] strict_mono_on_def 𝔤_in_β)
        have *: "𝔄 j (μ j)  𝔄 i (𝔤 i j (μ j))" if "i < j" for i j
          using wf_measure [of "λk. j-k"] that
        proof (induction i rule: wf_induct_rule)
          case (less i)
          then have "j - Suc i < j - i"
            by (metis (no_types) Suc_diff_Suc lessI)
          with less 𝔤_in_β show ?case
            by (simp add: 𝔤 [of i]) (metis 17 Suc_lessI μ_in_β order_refl order_trans x14)
        have le_iff: "𝔤 i j (μ j)  μ i  μ j  μ i" for i j
          using sm_𝔤 unfolding strict_mono_on_def
          by (metis "17" Ord_in_Ord Ord_linear2 μ_in_β leD le_refl less_V_def Ord β)
        then have less_iff: "𝔤 i j (μ j) < μ i  μ j < μ i" for i j
          by (metis (no_types, lifting) "17" μ_in_β less_V_def order_refl sm_𝔤 strict_mono_on_def)
        have eq_iff: "𝔤 i j (μ j) = μ i  μ j = μ i" for i j
          by (metis eq_refl le_iff less_iff less_le)
        have μ_if_ne: "μ m < μ n" if mn: "𝔄 m (μ m)  𝔄 n (μ n)" "m  n" for m n
        proof -
          have xmn: "x m < x n"
            using "15" less_setsD that(1) by blast
          have Ord𝔤: "Ord (𝔤 n m (μ m))"
            using Ord_in_Ord 𝔤_in_β μ_in_β ord(2) by presburger
          have "¬ 𝔄 m (μ m)  𝔄 n (μ n)" if "μ n = μ m"
            using  "*" "15" eq_iff that unfolding less_sets_def
            by (metis in_mono less_irrefl not_less_iff_gr_or_eq)
          have "𝔄 n (μ n)  𝔄 m (𝔤 m n (μ n))  𝔄 m (μ m)  𝔄 n (𝔤 n m (μ m))"
            using * mn
            by (meson antisym_conv3)
          then have False if "μ n < μ m"
            using strict_mono_setsD [OF 12] 15 xmn 𝔤_in_β μ_in_β that
            by (smt (verit, best) Ord𝔤 Ord_μ Ord_linear2 leD le_iff less_asym less_iff less_setsD subset_iff)
          ultimately show "μ m < μ n"
            by (meson that(1) Ord_μ Ord_linear_lt)
        have 18: "𝔄 m (μ m)  𝔄 n (μ n)  μ m < μ n" for m n
        proof (cases n m rule: linorder_cases)
          case less
          show ?thesis
          proof (intro iffI)
            assume "μ m < μ n"
            then have "𝔄 n (𝔤 n m (μ m))  𝔄 n (μ n)"
              by (metis "12" 𝔤_in_β μ_in_β eq_iff le_iff less_V_def strict_mono_sets_def)
            then show "𝔄 m (μ m)  𝔄 n (μ n)"
              by (meson "*" less less_sets_weaken1)
          qed (use μ_if_ne less in blast)
          case equal
          with 15 show ?thesis by auto
          case greater
          show ?thesis
          proof (intro iffI)
            assume "μ m < μ n"
            then have "𝔄 m (μ m)  (𝔄 m (𝔤 m n (μ n)))"
              by (meson 12 Ord_in_Ord Ord_linear2 𝔤_in_β μ_in_β le_iff leD ord(2) strict_mono_sets_def)
            then show "𝔄 m (μ m)  𝔄 n (μ n)"
              by (meson "*" greater less_sets_weaken2)
          qed (use μ_if_ne greater in blast)
        have 𝔄_increasing_μ: "𝔄 n (μ n)  𝔄 m (μ m)" if "m  n" "μ m = μ n" for m n
          by (metis "*" "17" dual_order.order_iff_strict that)
        moreover have INF: "infinite {n. n  m  μ m = μ n}" for m
        proof -
          have "infinite (range (λn. q (μ m, n)))"
            unfolding q_def
            using to_nat_on_infinite [OF co_βU inf_βU] finite_image_iff
            by (simp add: finite_image_iff inj_on_def)
          moreover have "(range (λn. q (μ m, n)))  {n. μ m = μ n}"
            using 11 [of "μ m"] by auto
          ultimately have "infinite {n. μ m = μ n}"
            using finite_subset by auto
          then have "infinite ({n. μ m = μ n} - {..<m})"
            by simp
          then show ?thesis
            by (auto simp: finite_nat_set_iff_bounded Bex_def not_less)
        let ?eqv = "λm. {n. m  n  μ m = μ n}"
        have sm_x: "strict_mono_on (?eqv m) x" for m
        proof (clarsimp simp: strict_mono_on_def)
          fix n p
          assume "m  n" "μ p = μ n" "μ m = μ n" "n < p"
          with 16 [of n] show "x n < x p"
            by (metis "*" "15" "17" Suc_lessI insert_absorb insert_subset le_SucI less_sets_singleton1)
        then have inj_x: "inj_on x (?eqv m)" for m
          using strict_mono_on_imp_inj_on by blast
        define ZA where "ZA  λm. ?Z  𝔄 m (μ m)"
        have small_ZA [simp]: "small (ZA m)" for m
          by (metis ZA_def inf_le1 small_image_nat smaller_than_small)
        have 19: "tp (ZA m)  ω" for m
        proof -
          have "x ` {n. m  n  μ m = μ n}  ZA m"
            unfolding ZA_def using "15" 𝔄_increasing_μ by blast
          then have "infinite (ZA m)"
            using INF [of m] finite_image_iff [OF inj_x] by (meson finite_subset)
          then show ?thesis
            by (simp add: ordertype_infinite_ge_ω)
        have "f  elts ω  ZA m. strict_mono_on (elts ω) f" for m
        proof -
          obtain Z where "Z  ZA m" "tp Z = ω"
            by (meson 19 Ord_ω le_ordertype_obtains_subset small_ZA)
          moreover have "ZA m  ON"
            using Ord_in_Ord 𝔄_αβ μ_in_β unfolding ZA_def by blast
          ultimately show ?thesis
            by (metis strict_mono_on_ordertype Pi_mono small_ZA smaller_than_small subset_iff)
        then obtain φ where φ: "m. φ m  elts ω  ZA m"
          and sm_φ: "m. strict_mono_on (elts ω) (φ m)"
          by metis
        have "Ex(λ(m,ν). ν  elts β  γ = ω * ν + ord_of_nat m)" if "γ  elts (ω * β)" for γ
          using that by (auto simp: mult [of ω β] lift_def elts_ω)
        then obtain split where split: "γ. γ