Theory Omega_Omega

section ‹An ordinal partition theorem by Jean A. Larson›

text ‹Jean A. Larson,
     A short proof of a partition theorem for the ordinal $\omega^\omega$.
     \emph{Annals of Mathematical Logic}, 6:129--145, 1973.›

theory Omega_Omega
  imports "HOL-Library.Product_Lexorder" Erdos_Milner

begin

abbreviation "list_of ≡ sorted_list_of_set"

subsection ‹Cantor normal form for ordinals below @{term "ω↑ω"}›

text ‹Unlike @{term Cantor_sum}, there is no list of ordinal exponents,
which are instead taken as consecutive. We obtain an order-isomorphism between @{term "ω↑ω"}
and increasing lists of natural numbers (ordered lexicographically).›

fun omega_sum_aux  where
  Nil: "omega_sum_aux 0 _ = 0"
| Suc: "omega_sum_aux (Suc n) [] = 0"
| Cons: "omega_sum_aux (Suc n) (m#ms) = (ω↑n) * (ord_of_nat m) + omega_sum_aux n ms"

abbreviation omega_sum where "omega_sum ms ≡ omega_sum_aux (length ms) ms"

text ‹A normal expansion has no leading zeroes›
inductive normal:: "nat list ⇒ bool" where
  normal_Nil[iff]: "normal []"
| normal_Cons:     "m > 0 ⟹ normal (m#ms)"

inductive_simps normal_Cons_iff [simp]: "normal (m#ms)"

lemma omega_sum_0_iff [simp]: "normal ns ⟹ omega_sum ns = 0 ⟷ ns = []"
  by (induction ns rule: normal.induct) auto

lemma Ord_omega_sum_aux [simp]: "Ord (omega_sum_aux k ms)"
  by (induction rule: omega_sum_aux.induct) auto

lemma Ord_omega_sum: "Ord (omega_sum ms)"
  by simp

lemma omega_sum_less_ωω [intro]: "omega_sum ms < ω↑ω"
proof (induction ms)
  case (Cons m ms)
  have "ω ↑ (length ms) * ord_of_nat m ∈ elts (ω ↑ Suc (length ms))"
    using Ord_mem_iff_lt by auto
  then have "ω↑(length ms) * ord_of_nat m ∈ elts (ω↑ω)"
    using Ord_ord_of_nat oexp_mono_le omega_nonzero ord_of_nat_le_omega by blast
  with Cons show ?case
    by (auto simp: mult_succ OrdmemD oexp_less indecomposableD indecomposable_ω_power)
qed (auto simp: zero_less_Limit)

lemma omega_sum_aux_less: "omega_sum_aux k ms < ω ↑ k"
proof (induction rule: omega_sum_aux.induct)
  case (3 n m ms)
  have " ω↑n * ord_of_nat m + ω↑n < ω↑n * ω"
    by (metis Ord_ord_of_nat ω_power_succ_gtr mult_succ oexp_succ ord_of_nat.simps(2))
  with 3 show ?case
    using dual_order.strict_trans by force
qed auto

lemma omega_sum_less: "omega_sum ms < ω ↑ (length ms)"
  by (rule omega_sum_aux_less)

lemma omega_sum_ge: "m ≠ 0 ⟹ ω ↑ (length ms) ≤ omega_sum (m#ms)"
  apply clarsimp
  by (metis Ord_ord_of_nat add_le_cancel_left0 le_mult Nat.neq0_conv ord_of_eq_0_iff vsubsetD)

lemma omega_sum_length_less:
  assumes "normal ns" "length ms < length ns"
  shows "omega_sum ms < omega_sum ns"
  using assms
proof (induction rule: normal.induct)
  case (normal_Cons n ns')
  have "ω ↑ length ms ≤ ω ↑ length ns'"
    using normal_Cons oexp_mono_le by auto
  then show ?case
    by (metis gr_implies_not_zero less_le_trans normal_Cons.hyps omega_sum_aux_less omega_sum_ge)
qed auto

lemma omega_sum_length_leD:
  assumes "omega_sum ms ≤ omega_sum ns" "normal ms"
  shows "length ms ≤ length ns"
  by (meson assms leD leI omega_sum_length_less)

lemma omega_sum_less_eqlen_iff_cases [simp]:
  assumes "length ms = length ns"
   shows "omega_sum (m#ms) < omega_sum (n#ns) ⟷ m<n ∨ m=n ∧ omega_sum ms < omega_sum ns"
  using omega_sum_less [of ms] omega_sum_less [of ns]
  by (metis Kirby.add_less_cancel_left Omega_Omega.Cons Ord_ω Ord_oexp Ord_omega_sum Ord_ord_of_nat assms length_Cons linorder_neqE_nat mult_nat_less_add_less order_less_asym)

lemma omega_sum_less_iff_cases:
  assumes "m > 0" "n > 0"
  shows "omega_sum (m#ms) < omega_sum (n#ns)
          ⟷ length ms < length ns
            ∨ length ms = length ns ∧ m<n
            ∨ length ms = length ns ∧ m=n ∧ omega_sum ms < omega_sum ns"
  by (smt (verit) assms length_Cons less_eq_Suc_le less_le_not_le nat_less_le normal_Cons not_le 
      omega_sum_length_less omega_sum_less_eqlen_iff_cases)

lemma omega_sum_less_iff:
  "((length ms, omega_sum ms), (length ns, omega_sum ns)) ∈ less_than <*lex*> VWF
   ⟷ (ms,ns) ∈ lenlex less_than"
proof (induction ms arbitrary: ns)
  case (Cons m ms)
  then show ?case
  proof (induction ns)
    case (Cons n ns')
    show ?case
      using Cons.prems Cons_lenlex_iff omega_sum_less_eqlen_iff_cases by fastforce
  qed auto
qed auto

lemma eq_omega_sum_less_iff:
  assumes "length ms = length ns"
  shows "(omega_sum ms, omega_sum ns) ∈ VWF ⟷ (ms,ns) ∈ lenlex less_than"
  by (metis assms in_lex_prod less_not_refl less_than_iff omega_sum_less_iff)

lemma eq_omega_sum_eq_iff:
  assumes "length ms = length ns"
  shows "omega_sum ms = omega_sum ns ⟷ ms=ns"
proof
  assume "omega_sum ms = omega_sum ns"
  then have "(omega_sum ms, omega_sum ns) ∉ VWF" "(omega_sum ns, omega_sum ms) ∉ VWF"
    by auto
  then obtain "(ms,ns) ∉ lenlex less_than" "(ns,ms) ∉ lenlex less_than"
    using assms eq_omega_sum_less_iff by metis
  moreover have "total (lenlex less_than)"
    by (simp add: total_lenlex total_less_than)
  ultimately show "ms=ns"
    by (meson UNIV_I total_on_def)
qed auto

lemma inj_omega_sum: "inj_on omega_sum {l. length l = n}"
  unfolding inj_on_def using eq_omega_sum_eq_iff by fastforce

lemma Ex_omega_sum: "γ ∈ elts (ω↑n) ⟹ ∃ns. γ = omega_sum ns ∧ length ns = n"
proof (induction n arbitrary: γ)
  case 0
  then show ?case
    by (rule_tac x="[]" in exI) auto
next
  case (Suc n)
  then obtain k::nat where k: "γ ∈ elts (ω ↑ n * k)"
       and kmin: "⋀k'. k'<k ⟹ γ ∉ elts (ω ↑ n * k')"
    by (metis Ord_ord_of_nat elts_mult_ωE oexp_succ ord_of_nat.simps(2))
  show ?case
  proof (cases k)
    case (Suc k')
    then obtain δ where δ: "γ = (ω ↑ n * k') + δ"
      by (metis lessI mult_succ ord_of_nat.simps(2) k kmin mem_plus_V_E)
    then have δin: "δ ∈ elts (ω ↑ n)"
      using Suc k mult_succ by auto
    then obtain ns where ns: "δ = omega_sum ns" and len: "length ns = n"
      using Suc.IH by auto
    moreover have "omega_sum ns < ω↑n"
      using OrdmemD ns δin by auto
    ultimately show ?thesis
      by (rule_tac x="k'#ns" in exI) (simp add: δ)
  qed (use k in auto)
qed

lemma omega_sum_drop [simp]: "omega_sum (dropWhile (λn. n=0) ns) = omega_sum ns"
  by (induction ns) auto

lemma normal_drop [simp]: "normal (dropWhile (λn. n=0) ns)"
  by (induction ns) auto

lemma omega_sum_ωω:
  assumes "γ ∈ elts (ω↑ω)"
  obtains ns where "γ = omega_sum ns" "normal ns"
proof -
  obtain ms where "γ = omega_sum ms"
    using assms Ex_omega_sum by (auto simp: oexp_Limit elts_ω)
  then show thesis
    by (metis normal_drop omega_sum_drop that)
qed

definition Cantor_ωω :: "V ⇒ nat list"
  where "Cantor_ωω ≡ λx. SOME ns. x = omega_sum ns ∧ normal ns"

lemma
  assumes "γ ∈ elts (ω↑ω)"
  shows Cantor_ωω: "omega_sum (Cantor_ωω γ) = γ"
    and normal_Cantor_ωω: "normal (Cantor_ωω γ)"
  by (metis (mono_tags, lifting) Cantor_ωω_def assms omega_sum_ωω someI)+


subsection ‹Larson's set $W(n)$›

definition WW :: "nat list set"
  where "WW ≡ {l. strict_sorted l}"

fun into_WW :: "nat ⇒ nat list ⇒ nat list" where
  "into_WW k [] = []"
| "into_WW k (n#ns) = (k+n) # into_WW (Suc (k+n)) ns"

fun from_WW :: "nat ⇒ nat list ⇒ nat list" where
  "from_WW k [] = []"
| "from_WW k (n#ns) = (n - k) # from_WW (Suc n) ns"

lemma from_into_WW [simp]: "from_WW k (into_WW k ns) = ns"
  by (induction ns arbitrary: k) auto

lemma inj_into_WW: "inj (into_WW k)"
  by (metis from_into_WW injI)

lemma into_from_WW_aux:
  "⟦strict_sorted ns; ∀n∈list.set ns. k ≤ n⟧ ⟹ into_WW k (from_WW k ns) = ns"
  by (induction ns arbitrary: k) (auto simp: Suc_leI)

lemma into_from_WW [simp]: "strict_sorted ns ⟹ into_WW 0 (from_WW 0 ns) = ns"
  by (simp add: into_from_WW_aux)

lemma into_WW_imp_ge: "y ∈ List.set (into_WW x ns) ⟹ x ≤ y"
  by (induction ns arbitrary: x) fastforce+

lemma strict_sorted_into_WW: "strict_sorted (into_WW x ns)"
  by (induction ns arbitrary: x) (auto simp: dest: into_WW_imp_ge)

lemma length_into_WW: "length (into_WW x ns) = length ns"
  by (induction ns arbitrary: x) auto

lemma WW_eq_range_into: "WW = range (into_WW 0)"
proof -
  have "⋀ns. strict_sorted ns ⟹ ns ∈ range (into_WW 0)"
    by (metis into_from_WW rangeI)
  then show ?thesis by (auto simp: WW_def strict_sorted_into_WW)
qed

lemma into_WW_lenlex_iff: "(into_WW k ms, into_WW k ns) ∈ lenlex less_than ⟷ (ms, ns) ∈ lenlex less_than"
proof (induction ms arbitrary: ns k)
  case Nil
  then show ?case
    by simp (metis length_0_conv length_into_WW)
next
  case (Cons m ms)
  then show ?case
    by (induction ns) (auto simp: Cons_lenlex_iff length_into_WW)
qed

lemma wf_llt [simp]: "wf (lenlex less_than)" and trans_llt [simp]: "trans (lenlex less_than)"
  by blast+

lemma total_llt [simp]: "total_on A (lenlex less_than)"
  by (meson UNIV_I total_lenlex total_less_than total_on_def)

lemma omega_sum_1_less:
  assumes "(ms,ns) ∈ lenlex less_than" shows "omega_sum (1#ms) < omega_sum (1#ns)"
proof -
  have "omega_sum (1#ms) < omega_sum (1#ns)" if "length ms < length ns"
    using omega_sum_less_iff_cases that zero_less_one by blast
  then show ?thesis
    using assms by (auto simp: mult_succ simp flip: omega_sum_less_iff)
qed

lemma ordertype_WW_1: "ordertype WW (lenlex less_than) ≤ ordertype UNIV (lenlex less_than)"
  by (rule ordertype_mono) auto

lemma ordertype_WW_2: "ordertype UNIV (lenlex less_than) ≤ ω↑ω"
proof (rule ordertype_inc_le_Ord)
  show "range (λms. omega_sum (1#ms)) ⊆ elts (ω↑ω)"
    by (meson Ord_ω Ord_mem_iff_lt Ord_oexp Ord_omega_sum image_subset_iff omega_sum_less_ωω)
qed (use omega_sum_1_less in auto)

lemma ordertype_WW_3: "ω↑ω ≤ ordertype WW (lenlex less_than)"
proof -
  define π where "π ≡ into_WW 0 ∘ Cantor_ωω"
  have ωω: "ω↑ω = tp (elts (ω↑ω))"
    by simp
  also have "… ≤ ordertype WW (lenlex less_than)"
  proof (rule ordertype_inc_le)
    fix α β
    assume α: "α ∈ elts (ω↑ω)" and β: "β ∈ elts (ω↑ω)" and "(α, β) ∈ VWF"
    then obtain *: "Ord α" "Ord β" "α<β"
      by (metis Ord_in_Ord Ord_ordertype VWF_iff_Ord_less ωω)
    then have "length (Cantor_ωω α) ≤ length (Cantor_ωω β)"
      using α β by (simp add: Cantor_ωω normal_Cantor_ωω omega_sum_length_leD)
    with α β * have "(Cantor_ωω α, Cantor_ωω β) ∈ lenlex less_than"
      by (auto simp: Cantor_ωω simp flip: omega_sum_less_iff)
    then show "(π α, π β) ∈ lenlex less_than"
      by (simp add: π_def into_WW_lenlex_iff)
  qed (auto simp: π_def WW_def strict_sorted_into_WW)
  finally show "ω↑ω ≤ ordertype WW (lenlex less_than)" .
qed

lemma ordertype_WW: "ordertype WW (lenlex less_than) = ω↑ω"
  and ordertype_UNIV_ωω: "ordertype UNIV (lenlex less_than) = ω↑ω"
  using ordertype_WW_1 ordertype_WW_2 ordertype_WW_3 by auto


lemma ordertype_ωω:
  fixes F :: "nat ⇒ nat list set"
  assumes "⋀j::nat. ordertype (F j) (lenlex less_than) = ω↑j"
  shows "ordertype (⋃j. F j) (lenlex less_than) = ω↑ω"
proof (rule antisym)
  show "ordertype (⋃ (range F)) (lenlex less_than) ≤ ω ↑ ω"
    by (metis ordertype_UNIV_ωω ordertype_mono small top_greatest trans_llt wf_llt)
  have "⋀n. ω ↑ ord_of_nat n ≤ ordertype (⋃ (range F)) (lenlex less_than)"
    by (metis TC_small Union_upper assms ordertype_mono rangeI trans_llt wf_llt)
  then show "ω ↑ ω ≤ ordertype (⋃ (range F)) (lenlex less_than)"
    by (auto simp: oexp_ω_Limit ZFC_in_HOL.SUP_le_iff elts_ω)
qed



definition WW_seg :: "nat ⇒ nat list set"
  where "WW_seg n ≡ {l ∈ WW. length l = n}"

lemma WW_seg_subset_WW: "WW_seg n ⊆ WW"
  by (auto simp: WW_seg_def)

lemma WW_eq_UN_WW_seg: "WW = (⋃ n. WW_seg n)"
  by (auto simp: WW_seg_def)

lemma ordertype_list_seg: "ordertype {l. length l = n} (lenlex less_than) = ω↑n"
proof -
  have "bij_betw omega_sum {l. length l = n} (elts (ω↑n))"
    unfolding WW_seg_def bij_betw_def
    by (auto simp: inj_omega_sum Ord_mem_iff_lt omega_sum_less dest: Ex_omega_sum)
  then show ?thesis
    by (force simp: ordertype_eq_iff simp flip: eq_omega_sum_less_iff)
qed

lemma ordertype_WW_seg: "ordertype (WW_seg n) (lenlex less_than) = ω↑n"
  (is "ordertype ?W ?R = ω↑n")
proof -
  have "ordertype {l. length l = n} ?R = ordertype ?W ?R"
  proof (subst ordertype_eq_ordertype)
    show "∃f. bij_betw f {l. length l = n} ?W ∧ (∀x∈{l. length l = n}. ∀y∈{l. length l = n}. ((f x, f y) ∈ lenlex less_than) = ((x, y) ∈ lenlex less_than))"
    proof (intro exI conjI)
      have "inj_on (into_WW 0) {l. length l = n}"
        by (metis from_into_WW inj_onI)
      then show "bij_betw (into_WW 0) {l. length l = n} ?W"
        by (auto simp: bij_betw_def WW_seg_def WW_eq_range_into length_into_WW)
    qed (simp add: into_WW_lenlex_iff)
  qed auto
  then show ?thesis
    using ordertype_list_seg by auto
qed


subsection ‹Definitions required for the lemmas›

subsubsection ‹Larson's "$<$"-relation on ordered lists›

instantiation list :: (ord)ord
begin

definition "xs < ys ≡ xs ≠ [] ∧ ys ≠ [] ⟶ last xs < hd ys" for xs ys :: "'a list"
definition "xs ≤ ys ≡ xs < ys ∨ xs = ys" for xs ys :: "'a list"

instance
  by standard

end

lemma less_Nil [simp]: "xs < []" "[] < xs"
  by (auto simp: less_list_def)

lemma less_sets_imp_list_less:
  assumes "list.set xs ≪ list.set ys"
  shows "xs < ys"
  by (metis assms last_in_set less_list_def less_sets_def list.set_sel(1))

lemma less_sets_imp_sorted_list_of_set:
  assumes "A ≪ B" "finite A" "finite B"
  shows "list_of A < list_of B"
  by (simp add: assms less_sets_imp_list_less)

lemma sorted_list_of_set_imp_less_sets:
  assumes "xs < ys" "sorted xs" "sorted ys"
  shows "list.set xs ≪ list.set ys"
  using assms sorted_hd_le sorted_le_last
  by (force simp: less_list_def less_sets_def intro: order.trans)

lemma less_list_iff_less_sets:
  assumes "sorted xs" "sorted ys"
  shows "xs < ys ⟷ list.set xs ≪ list.set ys"
  using assms sorted_hd_le sorted_le_last
  by (force simp: less_list_def less_sets_def intro: order.trans)

lemma strict_sorted_append_iff:
  "strict_sorted (xs @ ys) ⟷ xs < ys ∧ strict_sorted xs ∧ strict_sorted ys"
  by (metis less_list_iff_less_sets less_setsD sorted_wrt_append strict_sorted_imp_less_sets strict_sorted_imp_sorted)

lemma singleton_less_list_iff: "sorted xs ⟹ [n] < xs ⟷ {..n} ∩ list.set xs = {}"
  apply (simp add: less_list_def disjoint_iff)
  by (metis empty_iff less_le_trans list.set(1) list.set_sel(1) not_le sorted_hd_le)

lemma less_hd_imp_less: "xs < [hd ys] ⟹ xs < ys"
  by (simp add: less_list_def)

lemma strict_sorted_concat_I:
  assumes "⋀x. x ∈ list.set xs ⟹ strict_sorted x"
          "⋀n. Suc n < length xs ⟹ xs!n < xs!Suc n"
          "xs ∈ lists (- {[]})"
  shows "strict_sorted (concat xs)"
  using assms
proof (induction xs)
  case (Cons x xs)
  then have "x < concat xs"
    apply (simp add: less_list_def)
    by (metis Compl_iff hd_concat insertI1 length_greater_0_conv length_pos_if_in_set list.sel(1) lists.cases nth_Cons_0)
  with Cons show ?case
    by (force simp: strict_sorted_append_iff)
qed auto


subsection ‹Nash Williams for lists›

subsubsection ‹Thin sets of lists›

inductive initial_segment :: "'a list ⇒ 'a list ⇒ bool"
  where "initial_segment xs (xs@ys)"

definition thin :: "'a list set ⇒ bool"
  where "thin A ≡ ¬ (∃x y. x ∈ A ∧ y ∈ A ∧ x ≠ y ∧ initial_segment x y)"

lemma initial_segment_ne:
  assumes "initial_segment xs ys" "xs ≠ []"
  shows "ys ≠ [] ∧ hd ys = hd xs"
  using assms by (auto elim!: initial_segment.cases)

lemma take_initial_segment:
  assumes "initial_segment xs ys" "k ≤ length xs"
  shows "take k xs = take k ys"
  by (metis append_eq_conv_conj assms initial_segment.cases min_def take_take)

lemma initial_segment_length_eq:
  assumes "initial_segment xs ys" "length xs = length ys"
  shows "xs = ys"
  using assms initial_segment.cases by fastforce

lemma initial_segment_Nil [simp]: "initial_segment [] ys"
  by (simp add: initial_segment.simps)

lemma initial_segment_Cons [simp]: "initial_segment (x#xs) (y#ys) ⟷ x=y ∧ initial_segment xs ys"
  by (metis append_Cons initial_segment.simps list.inject)

lemma init_segment_iff_initial_segment:
  assumes "strict_sorted xs" "strict_sorted ys"
  shows "init_segment (list.set xs) (list.set ys) ⟷ initial_segment xs ys" (is "?lhs = ?rhs")
proof
  assume ?lhs
  then obtain S' where S': "list.set ys = list.set xs ∪ S'" "list.set xs ≪ S'"
    by (auto simp: init_segment_def)
  then have "finite S'"
    by (metis List.finite_set finite_Un)
  have "ys = xs @ list_of S'"
    using S' ‹strict_sorted xs›
  proof (induction xs)
    case Nil
    with ‹strict_sorted ys› show ?case
      by auto
  next
    case (Cons a xs)
    with ‹finite S'› have "ys = a # xs @ list_of S'"
      by (metis List.finite_set append_Cons assms(2) sorted_list_of_set_Un sorted_list_of_set_set_of)
    then show ?case
      by (auto simp: Cons)
  qed
  then show ?rhs
    using initial_segment.intros by blast
next
  assume ?rhs
  then show ?lhs
  proof cases
    case (1 ys)
    with assms show ?thesis
      by (simp add: init_segment_Un strict_sorted_imp_less_sets)
  qed
qed

theorem Nash_Williams_WW:
  fixes h :: "nat list ⇒ nat"
  assumes "infinite M" and h: "h ` {l ∈ A. List.set l ⊆ M} ⊆ {..<2}" and "thin A" "A ⊆ WW"
  obtains i N where "i < 2" "infinite N" "N ⊆ M" "h ` {l ∈ A. List.set l ⊆ N} ⊆ {i}"
proof -
  define AM where "AM ≡ {l ∈ A. List.set l ⊆ M}"
  have "thin_set (list.set ` A)"
    using ‹thin A› ‹A ⊆ WW› unfolding thin_def thin_set_def WW_def
    by (auto simp: subset_iff init_segment_iff_initial_segment)
  then have "thin_set (list.set ` AM)"
    by (simp add: AM_def image_subset_iff thin_set_def)
  then have "Ramsey (list.set ` AM) 2"
    using Nash_Williams_2 by metis
  moreover have "(h ∘ list_of) ∈ list.set ` AM → {..<2}"
    unfolding AM_def
  proof clarsimp
    fix l
    assume "l ∈ A" "list.set l ⊆ M"
    then have "strict_sorted l"
      using WW_def ‹A ⊆ WW› by blast
    then show "h (list_of (list.set l)) < 2"
      using h ‹l ∈ A› ‹list.set l ⊆ M› by auto
  qed
  ultimately obtain N i where N: "N ⊆ M" "infinite N" "i<2" 
              and "list.set ` AM ∩ Pow N ⊆ (h ∘ list_of) -` {i}"
    unfolding Ramsey_eq by (metis ‹infinite M›)
  then have N_disjoint: "(h ∘ list_of) -` {1-i} ∩ (list.set ` AM) ∩ Pow N = {}"
    unfolding subset_vimage_iff less_2_cases_iff by force
  have "h ` {l ∈ A. list.set l ⊆ N} ⊆ {i}"
  proof clarify
    fix l
    assume "l ∈ A" and "list.set l ⊆ N"
    then have "h l < 2"
      using h ‹N ⊆ M› by force
    with ‹i<2› have "h l ≠ Suc 0 - i ⟹ h l = i"
      by (auto simp: eval_nat_numeral less_Suc_eq)
    moreover have "strict_sorted l"
      using ‹A ⊆ WW› ‹l ∈ A› unfolding WW_def by blast
    moreover have "h (list_of (list.set l)) = 1 - i ⟶ ¬ (list.set l ⊆ N)"
      using N_disjoint ‹N ⊆ M› ‹l ∈ A› by (auto simp: AM_def)
    ultimately show "h l = i"
      using N ‹N ⊆ M› ‹l ∈ A› ‹list.set l ⊆ N›
      by (auto simp: vimage_def set_eq_iff AM_def WW_def subset_iff)
  qed
  then show thesis
    using that ‹i<2› N by auto
qed

subsection ‹Specialised functions on lists›

lemma mem_lists_non_Nil: "xss ∈ lists (- {[]}) ⟷ (∀x ∈ list.set xss. x ≠ [])"
  by auto

fun acc_lengths :: "nat ⇒ 'a list list ⇒ nat list"
  where "acc_lengths acc [] = []"
      | "acc_lengths acc (l#ls) = (acc + length l) # acc_lengths (acc + length l) ls"

lemma length_acc_lengths [simp]: "length (acc_lengths acc ls) = length ls"
  by (induction ls arbitrary: acc) auto

lemma acc_lengths_eq_Nil_iff [simp]: "acc_lengths acc ls = [] ⟷ ls = []"
  by (metis length_0_conv length_acc_lengths)

lemma set_acc_lengths:
  assumes "ls ∈ lists (- {[]})" shows "list.set (acc_lengths acc ls) ⊆ {acc<..}"
  using assms by (induction ls rule: acc_lengths.induct) fastforce+

text ‹Useful because @{text acc_lengths.simps} will sometimes be deleted from the simpset.›
lemma hd_acc_lengths [simp]: "hd (acc_lengths acc (l#ls)) = acc + length l"
  by simp

lemma last_acc_lengths [simp]:
  "ls ≠ [] ⟹ last (acc_lengths acc ls) = acc + sum_list (map length ls)"
by (induction acc ls rule: acc_lengths.induct) auto

lemma nth_acc_lengths [simp]:
  "⟦ls ≠ []; k < length ls⟧ ⟹ acc_lengths acc ls ! k = acc + sum_list (map length (take (Suc k) ls))"
  by (induction acc ls arbitrary: k rule: acc_lengths.induct) (fastforce simp: less_Suc_eq nth_Cons')+

lemma acc_lengths_plus: "acc_lengths (m+n) as = map ((+)m) (acc_lengths n as)"
  by (induction n as arbitrary: m rule: acc_lengths.induct) (auto simp: add.assoc)

lemma acc_lengths_shift: "NO_MATCH 0 acc ⟹ acc_lengths acc as = map ((+)acc) (acc_lengths 0 as)"
  by (metis acc_lengths_plus add.comm_neutral)

lemma length_concat_acc_lengths:
  "ls ≠ [] ⟹ k + length (concat ls) ∈ list.set (acc_lengths k ls)"
  by (metis acc_lengths_eq_Nil_iff last_acc_lengths last_in_set length_concat)

lemma strict_sorted_acc_lengths:
  assumes "ls ∈ lists (- {[]})" shows "strict_sorted (acc_lengths acc ls)"
  using assms
proof (induction ls rule: acc_lengths.induct)
  case (2 acc l ls)
  then have "strict_sorted (acc_lengths (acc + length l) ls)"
    by auto
  then show ?case
    using set_acc_lengths "2.prems" by auto
qed auto

lemma acc_lengths_append:
  "acc_lengths acc (xs @ ys)
   = acc_lengths acc xs @ acc_lengths (acc + sum_list (map length xs)) ys"
by (induction acc xs rule: acc_lengths.induct) (auto simp: add.assoc)


lemma length_concat_ge:
  assumes "as ∈ lists (- {[]})"
  shows "length (concat as) ≥ length as"
  using assms
proof (induction as)
  case (Cons a as)
  then have "length a ≥ Suc 0" "⋀l. l ∈ list.set as ⟹ length l ≥ Suc 0"
    by (auto simp: Suc_leI)
  then show ?case
    using Cons.IH by force
qed auto


fun interact :: "'a list list ⇒ 'a list list ⇒ 'a list"
  where
  "interact [] ys = concat ys"
| "interact xs [] = concat xs"
| "interact (x#xs) (y#ys) = x @ y @ interact xs ys"

lemma (in monoid_add) length_interact:
  "length (interact xs ys) = sum_list (map length xs) + sum_list (map length ys)"
  by (induction rule: interact.induct) (auto simp: length_concat)

lemma length_interact_ge:
  assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})"
  shows "length (interact xs ys) ≥ length xs + length ys"
  by (metis add_mono assms length_concat length_concat_ge length_interact)

lemma set_interact [simp]:
  shows "list.set (interact xs ys) = list.set (concat xs) ∪ list.set (concat ys)"
by (induction rule: interact.induct) auto

lemma interact_eq_Nil_iff [simp]:
  assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})"
  shows "interact xs ys = [] ⟷ xs=[] ∧ ys=[]"
  using length_interact_ge [OF assms]  by fastforce

lemma interact_sing [simp]: "interact [x] ys = x @ concat ys"
  by (metis (no_types) concat.simps(2) interact.simps neq_Nil_conv)

lemma hd_interact: "⟦xs ≠ []; hd xs ≠ []⟧ ⟹ hd (interact xs ys) = hd (hd xs)"
  by (smt (verit, best) hd_append2 hd_concat interact.elims list.sel(1))

lemma acc_lengths_concat_injective:
  assumes "concat as' = concat as" "acc_lengths n as' = acc_lengths n as"
  shows "as' = as"
  using assms
proof (induction as arbitrary: n as')
  case Nil
  then show ?case
    by (metis acc_lengths_eq_Nil_iff)
next
  case (Cons a as)
  then obtain a' bs where "as' = a'#bs"
    by (metis Suc_length_conv length_acc_lengths)
  with Cons show ?case
    by simp
qed

lemma acc_lengths_interact_injective:
  assumes "interact as' bs' = interact as bs" "acc_lengths a as' = acc_lengths a as" "acc_lengths b bs' = acc_lengths b bs"
  shows "as' = as ∧ bs' = bs"
  using assms
proof (induction as bs arbitrary: a b as' bs' rule: interact.induct)
  case (1 cs) then show ?case
    by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(1))
next
  case (2 c cs)
  then show ?case
    by (metis acc_lengths_concat_injective acc_lengths_eq_Nil_iff interact.simps(2) list.exhaust)
next
  case (3 x xs y ys) 
  then obtain a' us b' vs where "as' = a'#us" "bs' = b'#vs"
    by (metis length_Suc_conv length_acc_lengths)
  with 3 show ?case
    by auto
qed


lemma strict_sorted_interact_I:
  assumes "length ys ≤ length xs" "length xs ≤ Suc (length ys)"
    "⋀x. x ∈ list.set xs ⟹ strict_sorted x"
    "⋀y. y ∈ list.set ys ⟹ strict_sorted y"
    "⋀n. n < length ys ⟹ xs!n < ys!n"
    "⋀n. Suc n < length xs ⟹ ys!n < xs!Suc n"
  assumes "xs ∈ lists (- {[]})" "ys ∈ lists (- {[]})"
  shows "strict_sorted (interact xs ys)"
  using assms
proof (induction rule: interact.induct)
  case (3 x xs y ys)
  then have "x < y"
    by force
  moreover have "strict_sorted (interact xs ys)"
    using 3 by simp (metis Suc_less_eq nth_Cons_Suc)
  moreover have "y < interact xs ys"
    using 3 apply (simp add: less_list_def)
    by (metis hd_interact le_zero_eq length_greater_0_conv list.sel(1) list.set_sel(1) list.size(3) lists.simps mem_lists_non_Nil nth_Cons_0)
  ultimately show ?case
    using 3 by (simp add: strict_sorted_append_iff less_list_def)
qed auto


subsection ‹Forms and interactions›

subsubsection ‹Forms›

inductive Form_Body :: "[nat, nat, nat list, nat list, nat list] ⇒ bool"
  where "Form_Body ka kb xs ys zs"
  if "length xs < length ys" "xs = concat (a#as)" "ys = concat (b#bs)"
          "a#as ∈ lists (- {[]})" "b#bs ∈ lists (- {[]})"
          "length (a#as) = ka" "length (b#bs) = kb"
          "c = acc_lengths 0 (a#as)"
          "d = acc_lengths 0 (b#bs)"
          "zs = concat [c, a, d, b] @ interact as bs"
          "strict_sorted zs"


inductive Form :: "[nat, nat list set] ⇒ bool"
  where "Form 0 {xs,ys}" if "length xs = length ys" "xs ≠ ys"
      | "Form (2*k-1) {xs,ys}" if "Form_Body k k xs ys zs" "k > 0"
      | "Form (2*k)   {xs,ys}" if "Form_Body (Suc k) k xs ys zs" "k > 0"

inductive_cases Form_0_cases_raw: "Form 0 u"

lemma Form_elim_upair:
  assumes "Form l U"
  obtains xs ys where "xs ≠ ys" "U = {xs,ys}" "length xs ≤ length ys"
  using assms
  by (smt (verit, best) Form.simps Form_Body.cases less_or_eq_imp_le nat_neq_iff)


lemma assumes "Form_Body ka kb xs ys zs"
  shows Form_Body_WW: "zs ∈ WW" 
    and Form_Body_nonempty: "length zs > 0" 
    and Form_Body_length: "length xs < length ys"
  using Form_Body.cases [OF assms] by (fastforce simp: WW_def)+

lemma form_cases:
  fixes l::nat
  obtains (zero) "l = 0" | (nz) ka kb where "l = ka+kb - 1" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
proof -
  have "l = 0 ∨ (∃ka kb. l = ka+kb - 1 ∧ 0 < kb ∧ kb ≤ ka ∧ ka ≤ Suc kb)"
    by presburger
  then show thesis
    using nz zero by blast
qed

subsubsection ‹Interactions›

lemma interact:
  assumes "Form l U" "l>0"
  obtains ka kb xs ys zs where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys zs" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
  using assms
  unfolding Form.simps
  by (smt (verit, best) add_Suc diff_Suc_1 lessI mult_2 nat_less_le order_refl)


definition inter_scheme :: "nat ⇒ nat list set ⇒ nat list"
  where "inter_scheme l U ≡ 
          SOME zs. ∃k xs ys. U = {xs,ys} ∧ 
            (l = 2*k-1 ∧ Form_Body k k xs ys zs ∨ l = 2*k ∧ Form_Body (Suc k) k xs ys zs)"


lemma inter_scheme:
  assumes "Form l U" "l>0"
  obtains ka kb xs ys where "l = ka+kb - 1" "U = {xs,ys}" "Form_Body ka kb xs ys (inter_scheme l U)" "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
  using interact [OF ‹Form l U›]
proof cases
  case (2 ka kb xs ys zs)
  then have §: "⋀ka kb zs. ¬ Form_Body ka kb ys xs zs"
    using Form_Body_length less_asym' by blast
  have "Form_Body ka kb xs ys (inter_scheme l U)"
  proof (cases "ka = kb")
    case True 
    with 2 have l: "∀k. l ≠ k * 2"
      by presburger
    have [simp]: "⋀k. kb + kb - Suc 0 = k * 2 - Suc 0 ⟷ k=kb"
      by auto
    show ?thesis
      unfolding inter_scheme_def using 2 l True
      by (auto simp: § ‹l > 0› Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex)
  next
    case False
    with 2 have l: "∀k. l ≠ k * 2 - Suc 0" and [simp]: "ka = Suc kb"
      by presburger+
    have [simp]: "⋀k. kb + kb = k * 2 ⟷ k=kb"
      by auto
    show ?thesis
      unfolding inter_scheme_def using 2 l False
      by (auto simp: § ‹l > 0› Set.doubleton_eq_iff conj_disj_distribR ex_disj_distrib algebra_simps some_eq_ex)
  qed
  then show ?thesis
    by (simp add: 2 that)
qed (use ‹l > 0› in auto)

lemma inter_scheme_strict_sorted:
  assumes "Form l U" "l>0"
  shows "strict_sorted (inter_scheme l U)"
  using Form_Body.simps assms inter_scheme by fastforce

lemma inter_scheme_simple:
  assumes "Form l U" "l>0"
  shows "inter_scheme l U ∈ WW ∧ length (inter_scheme l U) > 0"
  using inter_scheme [OF assms] by (meson Form_Body_WW Form_Body_nonempty)

subsubsection ‹Injectivity of interactions›

proposition inter_scheme_injective:
  assumes "Form l U" "Form l U'" "l > 0" and eq: "inter_scheme l U' = inter_scheme l U"
  shows "U' = U"
proof -
  obtain ka kb xs ys 
    where l: "l = ka+kb - 1" and U: "U = {xs,ys}" 
      and FB: "Form_Body ka kb xs ys (inter_scheme l U)" 
      and kb: "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
    using assms inter_scheme by blast
  then obtain a as b bs c d
    where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)"
      and len: "length (a#as) = ka" "length (b#bs) = kb"
      and c: "c = acc_lengths 0 (a#as)"
      and d: "d = acc_lengths 0 (b#bs)"
      and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs"
    by (auto simp: Form_Body.simps)
  obtain ka' kb' xs' ys' 
    where l': "l = ka'+kb' - 1" and U': "U' = {xs',ys'}" 
      and FB': "Form_Body ka' kb' xs' ys' (inter_scheme l U')" 
      and kb': "0 < kb'" "kb' ≤ ka'" "ka' ≤ Suc kb'"
    using assms inter_scheme by blast
  then obtain a' as' b' bs' c' d'
    where xs': "xs' = concat (a'#as')" and ys': "ys' = concat (b'#bs')"
      and len': "length (a'#as') = ka'" "length (b'#bs') = kb'"
      and c': "c' = acc_lengths 0 (a'#as')"
      and d': "d' = acc_lengths 0 (b'#bs')"
      and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'"
    using Form_Body.simps by auto
  have [simp]: "ka' = ka ∧ kb' = kb"
    using ‹l > 0› l l' kb kb' le_SucE le_antisym mult_2 by linarith 
  have [simp]: "length c = length c'" "length d = length d'"
    using c c' d d' len' len by auto
  have c_off: "c' = c" "a' @ d' @ b' @ interact as' bs' = a @ d @ b @ interact as bs"
    using eq by (auto simp: Ueq Ueq')
  then have len_a: "length a' = length a"
    by (metis acc_lengths.simps(2) add.left_neutral c c' nth_Cons_0)
  with c_off have §: "a' = a" "d' = d" "b' @ interact as' bs' = b @ interact as bs"
    by auto
  then have "length (interact as' bs') = length (interact as bs)"
    by (metis acc_lengths.simps(2) add_left_cancel append_eq_append_conv d d' list.inject)
  with § have "b' = b" "interact as' bs' = interact as bs"
    by auto
  moreover have "acc_lengths 0 as' = acc_lengths 0 as"
    using ‹a' = a› ‹c' = c› by (simp add: c' c acc_lengths_shift)
  moreover have "acc_lengths 0 bs' = acc_lengths 0 bs"
    using ‹b' = b› ‹d' = d› by (simp add: d' d acc_lengths_shift)
  ultimately have "as' = as ∧ bs' = bs"
    using acc_lengths_interact_injective by blast
  then show ?thesis
    by (simp add: ‹a' = a› U U' ‹b' = b› xs xs' ys ys')
qed


lemma strict_sorted_interact_imp_concat:
    "strict_sorted (interact as bs) ⟹ strict_sorted (concat as) ∧ strict_sorted (concat bs)"
proof (induction as bs rule: interact.induct)
  case (3 x xs y ys)
  have "x < concat xs"
    using "3.prems"
    by (smt (verit, del_insts) Un_iff hd_in_set interact.simps(3) last_in_set less_list_def set_append set_interact sorted_wrt_append)
  moreover have "y < concat ys"
    using 3 sorted_wrt_append strict_sorted_append_iff by fastforce 
  ultimately show ?case
    using 3 by (auto simp add: strict_sorted_append_iff)
qed auto


lemma strict_sorted_interact_hd:
  "⟦strict_sorted (interact cs ds); cs ≠ []; ds ≠ []; hd cs ≠ []; hd ds ≠ []⟧
       ⟹ hd (hd cs) < hd (hd ds)"
  by (metis append_is_Nil_conv hd_append2 hd_in_set interact.simps(3) list.exhaust_sel sorted_wrt_append)


text ‹the lengths of the two lists can differ by one›
proposition interaction_scheme_unique_aux:
  assumes "concat as = concat as'" and ys': "concat bs = concat bs'"
    and "as ∈ lists (- {[]})" "bs ∈ lists (- {[]})"
    and "strict_sorted (interact as bs)"
    and "length bs ≤ length as" "length as ≤ Suc (length bs)"
    and "as' ∈ lists (- {[]})" "bs' ∈ lists (- {[]})"
    and "strict_sorted (interact as' bs')"
    and "length bs' ≤ length as'" "length as' ≤ Suc (length bs')"
    and "length as = length as'" "length bs = length bs'"
  shows "as = as' ∧ bs = bs'"
  using assms
proof (induction "length as" arbitrary: as bs as' bs')
  case 0 then show ?case
    by auto
next
  case SUC: (Suc k)
  show ?case
  proof (cases k)
    case 0
    with SUC obtain a a' where aa': "as = [a]" "as' = [a']"
      by (metis Suc_length_conv length_0_conv)
    show ?thesis
    proof
      show "as = as'"
        using aa' ‹concat as = concat as'› by force
      with SUC 0 show "bs = bs'"
        by (metis Suc_leI append_Nil2 concat.simps impossible_Cons le_antisym length_greater_0_conv list.exhaust)
    qed
  next
    case (Suc k')
    then obtain a cs b ds where eq: "as = a#cs" "bs = b#ds"
      using SUC
      by (metis le0 list.exhaust list.size(3) not_less_eq_eq)
    have "length as' ≠ 0"
      using SUC by force
    then obtain a' cs' b' ds' where eq': "as' = a'#cs'" "bs' = b'#ds'"
      by (metis ‹length bs = length bs'› eq(2) length_0_conv list.exhaust)
    obtain k: "k = length cs" "k ≤ Suc (length ds)"
      using eq SUC by auto
    case (Suc k')
    obtain [simp]: "b ≠ []" "b' ≠ []" "a ≠ []" "a' ≠ []"
      using SUC by (simp add: eq eq')
    then have "hd b' = hd b"
      using SUC by (metis concat.simps(2) eq'(2) eq(2) hd_append2)
    have ss_ab: "strict_sorted (concat as)" "strict_sorted (concat bs)"
      using strict_sorted_interact_imp_concat SUC.prems(5) by blast+
    have sw_ab: "strict_sorted (a @ b @ interact cs ds)"
      by (metis SUC.prems(5) eq interact.simps(3))
    then obtain "a < b" "strict_sorted a" "strict_sorted b"
      by (metis append_assoc strict_sorted_append_iff)
    have b_cs: "strict_sorted (concat (b # cs))"
      by (metis append.simps(1) concat.simps(2) interact.simps(3) strict_sorted_interact_imp_concat sw_ab)
    then have "b < concat cs"
      using strict_sorted_append_iff by auto
    have "strict_sorted (a @ concat cs)"
      using eq(1) ss_ab(1) by force
    have "list.set a = list.set (concat as) ∩ {..< hd b}"
    proof -
      have "x ∈ list.set a"
        if "x < hd b" and "l ∈ list.set cs" and "x ∈ list.set l" for x l
        using b_cs sorted_hd_le strict_sorted_imp_sorted that by fastforce
      then show ?thesis
        using ‹b ≠ []› sw_ab by (force simp: strict_sorted_append_iff sorted_wrt_append eq)
    qed
    moreover
    have ss_ab': "strict_sorted (concat as')" "strict_sorted (concat bs')"
      using strict_sorted_interact_imp_concat SUC.prems(10) by blast+
    have sw_ab': "strict_sorted (a' @ b' @ interact cs' ds')"
      by (metis SUC.prems(10) eq' interact.simps(3))
    then obtain "a' < b'" "strict_sorted a'" "strict_sorted b'"
      by (metis append_assoc strict_sorted_append_iff)
    have b_cs': "strict_sorted (concat (b' # cs'))"
      by (metis (no_types) SUC.prems(10) append_Nil eq' interact.simps(3) strict_sorted_append_iff strict_sorted_interact_imp_concat)
    then have "b' < concat cs'"
      by (simp add: strict_sorted_append_iff)
    then have "hd b' ∉ list.set (concat cs')"
      by (metis Un_iff ‹b' ≠ []› list.set_sel(1) not_less_iff_gr_or_eq set_interact sorted_wrt_append sw_ab')
    have "strict_sorted (a' @ concat cs')"
      using eq'(1) ss_ab'(1) by force
    then have b_cs': "strict_sorted (b' @ concat cs')"
      using ‹b' < concat cs'› eq'(2) ss_ab'(2) strict_sorted_append_iff by auto
    have "list.set a' = list.set (concat as') ∩ {..< hd b'}"
    proof -
      have "x ∈ list.set a'"
        if "x < hd b'" and "l ∈ list.set cs'" and "x ∈ list.set l" for x l
        using b_cs' sorted_hd_le strict_sorted_imp_sorted that by fastforce
      then show ?thesis
        using ‹b' ≠ []› sw_ab' by (force simp: strict_sorted_append_iff sorted_wrt_append eq')
    qed
    ultimately have "a=a'"
      by (simp add: SUC.prems(1) ‹hd b' = hd b› ‹strict_sorted a'› ‹strict_sorted a› strict_sorted_equal)
    moreover
    have ccat_cs_cs': "concat cs = concat cs'"
      using SUC.prems(1) ‹a = a'› eq'(1) eq(1) by fastforce
    have "b=b'"
    proof (cases "ds = [] ∨ ds' = []")
      case True
      then show ?thesis
        using SUC eq'(2) eq(2) by fastforce
    next
      case False
      then have "ds ≠ []" "ds' ≠ []" "sorted (concat ds)" "sorted (concat ds')"
        using eq(2) ss_ab(2) eq'(2) ss_ab'(2) strict_sorted_append_iff strict_sorted_imp_sorted by auto
      have "strict_sorted b" "strict_sorted b'"
        using b_cs b_cs' sorted_wrt_append by auto
      moreover
      have "cs ≠ []"
        using k local.Suc by auto
      then obtain "hd cs ≠ []" "hd ds ≠ []"
        using SUC.prems(3) SUC.prems(4) eq list.set_sel(1)
        by (simp add: ‹ds ≠ []› mem_lists_non_Nil)
      then have "concat cs ≠ []"
        using ‹cs ≠ []› hd_in_set by auto
      have "hd (concat cs) < hd (concat ds)"
        using strict_sorted_interact_hd
        by (metis ‹cs ≠ []› ‹ds ≠ []› ‹hd cs ≠ []› ‹hd ds ≠ []› hd_concat sorted_wrt_append sw_ab)

      have "list.set b = list.set (concat bs) ∩ {..< hd (concat cs)}"
      proof -
        have 1: "x ∈ list.set b"
          if "x < hd (concat cs)" and "l ∈ list.set ds" and "x ∈ list.set l" for x l
          using ‹hd (concat cs) < hd (concat ds)› ‹sorted (concat ds)› sorted_hd_le that by fastforce
        have 2: "l < hd (concat cs)" if "l ∈ list.set b" for l
          by (metis ‹concat cs ≠ []› b_cs concat.simps(2) list.set_sel(1) sorted_wrt_append that)
        show ?thesis
          using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq)
      qed
      moreover
      have "cs' ≠ []"
        using k Suc ‹concat cs ≠ []› ccat_cs_cs' by auto
      then obtain "hd cs' ≠ []" "hd ds' ≠ []"
        using SUC.prems(8,9) ‹ds' ≠ []› eq'(1) eq'(2) list.set_sel(1) by auto
      then have "concat cs' ≠ []"
        using ‹cs' ≠ []› hd_in_set by auto
      have "hd (concat cs') < hd (concat ds')"
        using strict_sorted_interact_hd
        by (metis ‹cs' ≠ []› ‹ds' ≠ []› ‹hd cs' ≠ []› ‹hd ds' ≠ []› hd_concat sorted_wrt_append sw_ab')
      have "list.set b' = list.set (concat bs') ∩ {..< hd (concat cs')}"
      proof -
        have 1: "x ∈ list.set b'"
          if "x < hd (concat cs')" and "l ∈ list.set ds'" and "x ∈ list.set l" for x l
          using ‹hd (concat cs') < hd (concat ds')› ‹sorted (concat ds')› sorted_hd_le that by fastforce
        have 2: "l < hd (concat cs')" if "l ∈ list.set b'" for l
          by (metis ‹concat cs' ≠ []› b_cs' list.set_sel(1) sorted_wrt_append that)
        show ?thesis
          using 1 2 by (auto simp: strict_sorted_append_iff sorted_wrt_append eq')
      qed
      ultimately show "b = b'"
        by (simp add: SUC.prems(2) ccat_cs_cs' strict_sorted_equal)
    qed
    moreover
    have "cs = cs' ∧ ds = ds'"
    proof (rule SUC.hyps)
      show "k = length cs"
        using eq SUC.hyps(2) by auto[1]
      show "concat ds = concat ds'"
        using SUC.prems(2) ‹b = b'› eq'(2) eq(2) by auto
      show "strict_sorted (interact cs ds)"
        using eq SUC.prems(5) strict_sorted_append_iff by auto
      show "length ds ≤ length cs" "length cs ≤ Suc (length ds)"
        using eq SUC k by auto
      show "strict_sorted (interact cs' ds')"
        using eq' SUC.prems(10) strict_sorted_append_iff by auto
      show "length cs = length cs'"
        using SUC eq'(1) k(1) by force
    qed (use ccat_cs_cs' eq eq' SUC.prems in auto)
    ultimately show ?thesis
      by (simp add: ‹a = a'› ‹b = b'› eq eq')
  qed
qed


proposition Form_Body_unique:
  assumes "Form_Body ka kb xs ys zs" "Form_Body ka kb xs ys zs'" and "kb ≤ ka" "ka ≤ Suc kb"
  shows "zs' = zs"
proof -
  obtain a as b bs c d
      where xs: "xs = concat (a#as)" and ys: "ys = concat (b#bs)"
        and ne: "a#as ∈ lists (- {[]})" "b#bs ∈ lists (- {[]})"
        and len: "length (a#as) = ka" "length (b#bs) = kb"
        and c: "c = acc_lengths 0 (a#as)"
        and d: "d = acc_lengths 0 (b#bs)"
        and Ueq: "zs = concat [c, a, d, b] @ interact as bs"
        and ss_zs: "strict_sorted zs"
    using Form_Body.cases [OF assms(1)] by (metis (no_types))
  obtain a' as' b' bs' c' d'
      where xs': "xs = concat (a'#as')" and ys': "ys = concat (b'#bs')"
        and ne': "a'#as' ∈ lists (- {[]})" "b'#bs' ∈ lists (- {[]})"
        and len': "length (a'#as') = ka" "length (b'#bs') = kb"
        and c': "c' = acc_lengths 0 (a'#as')"
        and d': "d' = acc_lengths 0 (b'#bs')"
        and Ueq': "zs' = concat [c', a', d', b'] @ interact as' bs'"
        and ss_zs': "strict_sorted zs'"
    using Form_Body.cases [OF assms(2)] by (metis (no_types))
  have [simp]: "length c = length c'" "length d = length d'"
    using c c' d d' len' len by auto
  note acc_lengths.simps [simp del]
  have "a < b"
    using ss_zs by (auto simp: Ueq strict_sorted_append_iff less_list_def c d)
  have "a' < b'"
    using ss_zs' by (auto simp: Ueq' strict_sorted_append_iff less_list_def c' d')
  have "a#as = a'#as' ∧ b#bs = b'#bs'"
  proof (rule interaction_scheme_unique_aux)
    show "strict_sorted (interact (a # as) (b # bs))"
      using ss_zs ‹a < b› by (auto simp: Ueq strict_sorted_append_iff less_list_def d)
    show "strict_sorted (interact (a' # as') (b' # bs'))"
      using ss_zs' ‹a' < b'› by (auto simp: Ueq' strict_sorted_append_iff less_list_def d')
    show "length (b # bs) ≤ length (a # as)" "length (b' # bs') ≤ length (a' # as')"
      using ‹kb ≤ ka› len len' by auto
    show "length (a # as) ≤ Suc (length (b # bs))"
      using ‹ka ≤ Suc kb› len by linarith
    then show "length (a' # as') ≤ Suc (length (b' # bs'))"
      using len len' by fastforce
  qed (use len len' xs xs' ys ys' ne ne' in fastforce)+
  then show ?thesis
    using Ueq Ueq' c c' d d' by blast
qed


lemma Form_Body_imp_inter_scheme:
  assumes FB: "Form_Body ka kb xs ys zs" and "0 < kb" "kb ≤ ka" "ka ≤ Suc kb"
  shows "zs = inter_scheme ((ka+kb) - Suc 0) {xs,ys}"
proof -
  have "length xs < length ys"
    by (meson Form_Body_length assms(1))
  have [simp]: "a + a = b + b ⟷ a=b"  "a + a - Suc 0 = b + b - Suc 0 ⟷ a=b" for a b::nat
    by auto
  show ?thesis
  proof (cases "ka = kb")
    case True
    show ?thesis
      unfolding inter_scheme_def
      apply (rule some_equality [symmetric], metis One_nat_def True FB mult_2)
      using assms ‹length xs < length ys›
      by (auto simp: True mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger)
  next
    case False
    then have eq: "ka = Suc kb"
      using assms by linarith
    show ?thesis
      unfolding inter_scheme_def
      apply (rule some_equality [symmetric], use assms False mult_2 one_is_add eq in fastforce)
      using assms ‹length xs < length ys›
      by (auto simp: eq mult_2 Set.doubleton_eq_iff Form_Body_unique dest: Form_Body_length, presburger)
  qed
qed


subsection ‹For Lemma 3.8 AND PROBABLY 3.7›

definition grab :: "nat set ⇒ nat ⇒ nat set × nat set"
  where "grab N n ≡ (N ∩ enumerate N ` {..<n}, N ∩ {enumerate N n..})"

lemma grab_0 [simp]: "grab N 0 = ({}, N)"
  by (fastforce simp: grab_def enumerate_0 Least_le)

lemma less_sets_grab:
  "infinite N ⟹ fst (grab N n) ≪ snd (grab N n)"
  by (auto simp: grab_def less_sets_def intro: enumerate_mono less_le_trans)

lemma finite_grab [iff]: "finite (fst (grab N n))"
  by (simp add: grab_def)

lemma card_grab [simp]:
  assumes "infinite N" shows "card (fst (grab N n)) = n"
proof -
  have "N ∩ enumerate N ` {..<n} = enumerate N ` {..<n}"
    using assms by (auto simp: enumerate_in_set)
  with assms show ?thesis
    by (simp add: card_image grab_def strict_mono_enum strict_mono_imp_inj_on)
qed

lemma fst_grab_subset: "fst (grab N n) ⊆ N"
  using grab_def range_enum by fastforce

lemma snd_grab_subset: "snd (grab N n) ⊆ N"
  by (auto simp: grab_def)

lemma grab_Un_eq:
  assumes "infinite N" shows "fst (grab N n) ∪ snd (grab N n) = N"
proof
  show "N ⊆ fst (grab N n) ∪ snd (grab N n)"
    unfolding grab_def
    using assms enumerate_Ex le_less_linear strict_mono_enum strict_mono_less by fastforce
qed (simp add: grab_def)

lemma finite_grab_iff [simp]: "finite (snd (grab N n)) ⟷ finite N"
  by (metis finite_grab grab_Un_eq infinite_Un infinite_super snd_grab_subset)

lemma grab_eqD:
    "⟦grab N n = (A,M); infinite N⟧
    ⟹ A ≪ M ∧ finite A ∧ card A = n ∧ infinite M ∧ A ⊆ N ∧ M ⊆ N"
  using card_grab grab_def less_sets_grab finite_grab_iff by auto

lemma less_sets_fst_grab: "A ≪ N ⟹ A ≪ fst (grab N n)"
  by (simp add: fst_grab_subset less_sets_weaken2)

text‹Possibly redundant, given @{term grab}›
definition nxt where "nxt ≡ λN. λn::nat. N ∩ {n<..}"

lemma infinite_nxtN: "infinite N ⟹ infinite (nxt N n)"
  by (simp add: infinite_nat_greaterThan nxt_def)

lemma nxt_subset: "nxt N n ⊆ N"
  unfolding nxt_def by blast

lemma nxt_subset_greaterThan: "m ≤ n ⟹ nxt N n ⊆ {m<..}"
  by (auto simp: nxt_def)

lemma nxt_subset_atLeast: "m ≤ n ⟹ nxt N n ⊆ {m..}"
  by (auto simp: nxt_def)

lemma enum_nxt_ge: "infinite N ⟹ a ≤ enum (nxt N a) n"
  by (simp add: atLeast_le_enum infinite_nxtN nxt_subset_atLeast)

lemma inj_enum_nxt: "infinite N ⟹ inj_on (enum (nxt N a)) A"
  by (simp add: infinite_nxtN strict_mono_enum strict_mono_imp_inj_on)


subsection ‹Larson's Lemma 3.11›

text ‹Again from Jean A. Larson,
     A short proof of a partition theorem for the ordinal $\omega^\omega$.
     \emph{Annals of Mathematical Logic}, 6:129--145, 1973.›

lemma lemma_3_11:
  assumes "l > 0"
  shows "thin (inter_scheme l ` {U. Form l U})"
  using form_cases [of l]
proof cases
  case zero
  then show ?thesis
    using assms by auto
next
  case (nz ka kb)
  note acc_lengths.simps [simp del]
  show ?thesis
    unfolding thin_def
  proof clarify
    fix U U'
    assume ne: "inter_scheme l U ≠ inter_scheme l U'" and init: "initial_segment (inter_scheme l U) (inter_scheme l U')"
    assume "Form l U"
    then obtain kp kq xs ys where "l = kp+kq - 1" "U = {xs,ys}" 
            and U: "Form_Body kp kq xs ys (inter_scheme l U)" and "0 < kq" "kq ≤ kp" "kp ≤ Suc kq"
      using assms inter_scheme by blast
    then have "kp = ka ∧ kq = kb"
      using nz by linarith
    then obtain a as b bs c d
      where len: "length (a#as) = ka" "length (b#bs) = kb"
        and c: "c = acc_lengths 0 (a#as)"
        and d: "d = acc_lengths 0 (b#bs)"
        and Ueq: "inter_scheme l U = concat [c, a, d, b] @ interact as bs"
      using U by (auto simp: Form_Body.simps)
    assume "Form l U'"
    then obtain kp' kq' xs' ys'  where "l = kp'+kq' - 1" "U' = {xs',ys'}" 
            and U': "Form_Body kp' kq' xs' ys' (inter_scheme l U')" and "0 < kq'" "kq' ≤ kp'" "kp' ≤ Suc kq'"
      using assms inter_scheme by blast
    then have "kp' = ka ∧ kq' = kb"
      using nz by linarith
    then obtain a' as' b' bs' c' d'
      where len': "length (a'#as') = ka" "length (b'#bs') = kb"
        and c': "c' = acc_lengths 0 (a'#as')"
        and d': "d' = acc_lengths 0 (b'#bs')"
        and Ueq': "inter_scheme l U' = concat [c', a', d', b'] @ interact as' bs'"
      using U' by (auto simp: Form_Body.simps)
    have [simp]: "length bs' = length bs" "length as' = length as"
      using len len' by auto
    have "inter_scheme l U ≠ []" "inter_scheme l U' ≠ []"
      using Form_Body_nonempty U U' by auto
    define u1 where "u1 ≡ hd (inter_scheme l U)"
    have u1_eq': "u1 = hd (inter_scheme l U')"
      using ‹inter_scheme l U ≠ []› init u1_def initial_segment_ne by fastforce
    have au1: "u1 = length a"
      by (simp add: u1_def Ueq c)
    have au1': "u1 = length a'"
      by (simp add: u1_eq' Ueq' c')
    have len_eqk: "length c' = ka" "length d' = kb" "length c' = ka" "length d' = kb"
      using c d len c' d' len' by auto
    have take: "take (ka + u1 + kb) (c @ a @ d @ l) = c @ a @ d"
               "take (ka + u1 + kb) (c' @ a' @ d' @ l) = c' @ a' @ d'" for l
      using c d c' d' len by (simp_all flip: au1 au1')
    have leU: "ka + u1 + kb ≤ length (inter_scheme l U)"
      using c d len by (simp add: au1 Ueq)
    then have "take (ka + u1 + kb) (inter_scheme l U) = take (ka + u1 + kb) (inter_scheme l U')"
      using take_initial_segment init by blast
    then have §: "c @ a @ d = c' @ a' @ d'"
      by (metis Ueq Ueq' append.assoc concat.simps(2) take)
    have "length (inter_scheme l U) = ka + (c @ a @ d)!(ka-1) + kb + last d"
      by (simp add: Ueq c d length_interact nth_append flip: len)
    moreover have "length (inter_scheme l U') = ka + (c' @ a' @ d')!(ka-1) + kb + last d'"
      by (simp add: Ueq' c' d' length_interact nth_append flip: len')
    moreover have "last d = last d'"
      using "§" c d d' len'(1) len_eqk(1) by auto
    ultimately have "length (inter_scheme l U) = length (inter_scheme l U')"
      by (simp add: §)
    then show False
      using init initial_segment_length_eq ne by blast
  qed
qed


subsection ‹Larson's Lemma 3.6›

proposition lemma_3_6:
  fixes g :: "nat list set ⇒ nat"
  assumes g: "g ∈ [WW]⇗2⇖ → {0,1}"
  obtains N j where "infinite N"
    and "⋀k u. ⟦k > 0; u ∈ [WW]⇗2⇖; Form k u; [enum N k] < inter_scheme k u; List.set (inter_scheme k u) ⊆ N⟧ ⟹ g u = j k"
proof -
  define Φ where "Φ ≡ λm::nat. λM. infinite M ∧ m < Inf M"
  define Ψ where "Ψ ≡ λl m n::nat. λM N j. n > m ∧ N ⊆ M ∧ n ∈ M 
                     ∧ (∀U. Form l U ∧ U ⊆ WW ∧ [n] < inter_scheme l U ∧ list.set (inter_scheme l U) ⊆ N ⟶ g U = j)"
  have *: "∃n N j. Φ n N ∧ Ψ l m n M N j" if "l > 0" "Φ m M" for l m::nat and M :: "nat set"
  proof -
    define FF where "FF ≡ {U ∈ [WW]⇗2⇖. Form l U}"
    define h where "h ≡ λzs. g (inv_into FF (inter_scheme l) zs)"
    have "thin (inter_scheme l ` FF)"
      using ‹l > 0› lemma_3_11 by (simp add: thin_def FF_def)
    moreover
    have "inter_scheme l ` FF ⊆ WW"
      using inter_scheme_simple ‹0 < l› FF_def by blast
    moreover
    have "h ` {xs ∈ inter_scheme l ` FF. List.set xs ⊆ M} ⊆ {..<2}"
      using g inv_into_into[of concl: "FF" "inter_scheme l"]
      by (force simp: h_def FF_def Pi_iff)
    ultimately
    obtain j N where "j < 2" "infinite N" "N ⊆ M" and hj: "h ` {xs ∈ inter_scheme l ` FF. List.set xs ⊆ N} ⊆ {j}"
      using ‹Φ m M› unfolding Φ_def by (blast intro: Nash_Williams_WW [of M])
    let ?n = "Inf N"
    have "?n > m"
      using ‹Φ m M› ‹infinite N› unfolding Φ_def Inf_nat_def infinite_nat_iff_unbounded
      by (metis LeastI_ex ‹N ⊆ M› le_less_trans not_less not_less_Least subsetD)
    have "g U = j" if "Form l U" "U ⊆ WW" "[?n] < inter_scheme l U" "list.set (inter_scheme l U) ⊆ N - {?n}" for U
    proof -
      obtain xs ys where xys: "xs ≠ ys" "U = {xs,ys}"
        using Form_elim_upair ‹Form l U› by blast
      moreover have "inj_on (inter_scheme l) FF"
        using ‹0 < l› inj_on_def inter_scheme_injective FF_def by blast
      moreover 
      have "g (inv_into FF (inter_scheme l) (inter_scheme l U)) = j"
        using hj that xys subset_Diff_insert by (fastforce simp: h_def FF_def image_iff)
      ultimately show ?thesis
        using that FF_def by auto
    qed
    moreover have "?n < Inf (N - {?n})"
      by (metis Diff_iff Inf_nat_def Inf_nat_def1 ‹infinite N› finite.emptyI infinite_remove linorder_neqE_nat not_less_Least singletonI)
    moreover have "?n ∈ M"
      by (metis Inf_nat_def1 ‹N ⊆ M› ‹infinite N› finite.emptyI subsetD)
    ultimately have "Φ ?n (N - {?n}) ∧ Ψ l m ?n M (N - {?n}) j"
      using ‹Φ m M› ‹infinite N› ‹N ⊆ M› ‹?n > m› by (auto simp: Φ_def Ψ_def)
    then show ?thesis
      by blast
  qed
  have base: "Φ 0 {0<..}"
    unfolding Φ_def by (metis infinite_Ioi Inf_nat_def1 greaterThan_iff greaterThan_non_empty)
  have step: "Ex (λ(n,N,j). Φ n N ∧ Ψ l m n M N j)" if "Φ m M" "l > 0" for m M l
    using * [of l m M] that by (auto simp: Φ_def)
  define G where "G ≡ λl m M. @(n,N,j). Φ n N ∧ Ψ (Suc l) m n M N j"
  have GΦ: "(λ(n,N,j). Φ n N) (G l m M)" and GΨ: "(λ(n,N,j). Ψ (Suc l) m n M N j) (G l m M)"
    if "Φ m M" for l m M
    using step [OF that, of "Suc l"] by (force simp: G_def dest: some_eq_imp)+
  have G_increasing: "(λ(n,N,j). n > m ∧ N ⊆ M ∧ n ∈ M) (G l m M)"  if "Φ m M" for l m M
    using GΨ [OF that, of l] that by (simp add: Ψ_def split: prod.split_asm)
  define H where "H ≡ rec_nat (0,{0<..},0) (λl (m,M,j). G l m M)"
  have H_simps: "H 0 = (0,{0<..},0)" "⋀l. H (Suc l) = (case H l of (m,M,j) ⇒ G l m M)"
    by (simp_all add: H_def)
  have HΦ: "(λ(n,N,j). Φ n N) (H l)" for l
    by (induction l) (use base GΦ in ‹auto simp: H_simps split: prod.split_asm›)
  define ν where "ν ≡ (λl. case H l of (n,M,j) ⇒ n)"
  have H_inc: "ν l ≥ l" for l
  proof (induction l)
    case (Suc l)
    then show ?case
      using HΦ [of l] G_increasing [of "ν l"]
      apply (clarsimp simp: H_simps ν_def split: prod.split)
      by (metis (no_types, lifting) case_prodD leD le_less_trans not_less_eq_eq)
  qed auto
  let ?N = "range ν"
  define j where "j ≡ λl. case H l of (n,M,j) ⇒ j"
  have H_increasing_Suc: "(case H k of (n, N, j') ⇒ N) ⊇ (case H (Suc k) of (n, N, j') ⇒ insert n N)" for k
    using HΦ [of k]
    by (force simp: H_simps split: prod.split dest: G_increasing [where l=k])
  have H_increasing_superset: "(case H k of (n, N, j') ⇒ N) ⊇ (case H (n+k) of (n, N, j') ⇒ N)" for k n
  proof (induction n)
    case (Suc n)
    then show ?case
      using H_increasing_Suc [of "n+k"] by (auto split: prod.split_asm)
  qed auto
  then have H_increasing_less: "(case H k of (n, N, j') ⇒ N) ⊇ (case H l of (n, N, j') ⇒ insert n N)"
    if "k<l" for k l
    by (smt (verit, best) H_increasing_Suc add.commute less_natE order_trans that)
  have "ν k < ν (Suc k)" for k
    using HΦ [of k] unfolding ν_def
    by (auto simp: H_simps split: prod.split dest: G_increasing [where l=k])
  then have strict_mono_ν: "strict_mono ν"
    by (simp add: strict_mono_Suc_iff)
  then have enum_N: "enum ?N = ν"
    by (metis enum_works nat_infinite_iff range_strict_mono_ext)
  have **: "?N ∩ {n<..} ⊆ N'" if H: "H k = (n, N', j)" for n N' k j
  proof clarify
    fix l
    assume "n < ν l"
    then have False if "l ≤ k"
      using that strict_monoD [OF strict_mono_ν, of l k ] H by (force simp: ν_def)
    then have "k < l" using not_less by blast
    then obtain M j where Mj: "H l = (ν l,M,j)"
      unfolding ν_def
      by (metis (mono_tags, lifting) case_prod_conv old.prod.exhaust)
    then show "ν l ∈ N'"
      using that H_increasing_less [OF ‹k<l›] Mj by auto
  qed
  show thesis
  proof
    show "infinite (?N::nat set)"
      using H_inc infinite_nat_iff_unbounded_le by auto
  next
    fix l U
    assume "0 < l" and U: "U ∈ [WW]⇗2⇖"
      and interU: "[enum ?N l] < inter_scheme l U" "Form l U"
      and sub: "list.set (inter_scheme l U) ⊆ ?N"
    obtain k where k: "l = Suc k"
      using ‹0 < l› gr0_conv_Suc by blast
    have "g U = v" if "H k = (m, M, j0)" and "G k m M = (n, N', v)"
      for m M j0 n N' v
    proof -
      have n: "ν (Suc k) = n"
        using that by (simp add: ν_def H_simps)
      have "{..enum (range ν) l} ∩ list.set (inter_scheme l U) = {}"
        using inter_scheme_strict_sorted ‹0 < l› interU singleton_less_list_iff strict_sorted_iff by blast
      then have "list.set (inter_scheme (Suc k) U) ⊆ N'"
        using that sub ** [of "Suc k" n N' v] Suc_le_eq not_less_eq_eq
        by (fastforce simp:  k n enum_N H_simps)
      then show ?thesis
        using that interU U GΨ [of m M k] HΦ [of k]
        by (auto simp: Ψ_def k enum_N H_simps n nsets_def)
    qed
    with U show "g U = j l"
      by (auto simp: k j_def H_simps split: prod.split)
  qed
qed


subsection ‹Larson's Lemma 3.7›

subsubsection ‹Preliminaries›

text ‹Analogous to @{thm [source] ordered_nsets_2_eq}, but without type classes›
lemma total_order_nsets_2_eq:
  assumes tot: "total_on A r" and irr: "irrefl r"
  shows "nsets A 2 = {{x,y} | x y. x ∈ A ∧ y ∈ A ∧ (x,y) ∈ r}"
     (is "_ = ?rhs")
proof
  show "nsets A 2 ⊆ ?rhs"
    using tot
    unfolding numeral_nat total_on_def nsets_def
    by (fastforce simp: card_Suc_eq Set.doubleton_eq_iff not_less)
  show "?rhs ⊆ nsets A 2"
    using irr unfolding numeral_nat by (force simp: nsets_def card_Suc_eq irrefl_def)
qed

lemma lenlex_nsets_2_eq: "nsets A 2 = {{x,y} | x y. x ∈ A ∧ y ∈ A ∧ (x,y) ∈ lenlex less_than}"
  using total_order_nsets_2_eq by (simp add: total_order_nsets_2_eq irrefl_def)

lemma sum_sorted_list_of_set_map: "finite I ⟹ sum_list (map f (list_of I)) = sum f I"
proof (induction "card I" arbitrary: I)
  case (Suc n I)
  then have [simp]: "I ≠ {}"
    by auto
  have "sum_list (map f (list_of (I - {Min I}))) = sum f (I - {Min I})"
    using Suc by auto
  then show ?case
    using Suc.prems sum.remove [of I "Min I" f]
    by (simp add: sorted_list_of_set_nonempty Suc)
qed auto


lemma sorted_list_of_set_UN_eq_concat:
  assumes I: "strict_mono_sets I f" "finite I" and fin: "⋀i. finite (f i)"
  shows "list_of (⋃i ∈ I. f i) = concat (map (list_of ∘ f) (list_of I))"
  using I
proof (induction "card I" arbitrary: I)
  case (Suc n I)
  then have "I ≠ {}" and Iexp: "I = insert (Min I) (I - {Min I})"
    using Min_in Suc.hyps(2) Suc.prems(2) by fastforce+
  have IH: "list_of (⋃ (f ` (I - {Min I}))) = concat (map (list_of ∘ f) (list_of (I - {Min I})))"
    using Suc unfolding strict_mono_sets_def
    by (metis DiffE Iexp card_Diff_singleton diff_Suc_1 finite_Diff insertI1)
  have "list_of (⋃ (f ` I)) = list_of (⋃ (f ` (insert (Min I) (I - {Min I}))))"
    using Iexp by auto
  also have "… = list_of (f (Min I) ∪ ⋃ (f ` (I - {Min I})))"
    by (metis Union_image_insert)
  also have "… = list_of (f (Min I)) @ list_of (⋃ (f ` (I - {Min I})))"
  proof (rule sorted_list_of_set_Un)
    show "f (Min I) ≪ ⋃ (f ` (I - {Min I}))"
      using Suc.prems ‹I ≠ {}› strict_mono_less_sets_Min by blast
    show "finite (⋃ (f ` (I - {Min I})))"
      by (simp add: ‹finite I› fin)
  qed (use fin in auto)
  also have "… = list_of (f (Min I)) @ concat (map (list_of ∘ f) (list_of (I - {Min I})))"
    using IH by metis
  also have "… = concat (map (list_of ∘ f) (list_of I))"
    by (simp add: Suc.prems(2) ‹I ≠ {}› sorted_list_of_set_nonempty)
  finally show ?case .
qed auto

subsubsection ‹Lemma 3.7 of Jean A. Larson, ibid.›

proposition lemma_3_7:
  assumes "infinite N" "l > 0"
  obtains M where "M ∈ [WW]⇗m⇖"
                  "⋀U. U ∈ [M]⇗2⇖ ⟹ Form l U ∧ List.set (inter_scheme l U) ⊆ N"
proof (cases "m < 2")
  case True
  obtain w where w: "w ∈ WW"
    using WW_def strict_sorted_into_WW by auto
  define M where "M ≡ if m=0 then {} else {w}"
  have M: "M ∈ [WW]⇗m⇖"
    using True by (auto simp: M_def nsets_def w)
  have [simp]: "[M]⇗2⇖ = {}"
    using True by (auto simp: M_def nsets_def w dest: subset_singletonD)
  show ?thesis
    using M that by fastforce
next
  case False
  then have "m ≥ 2"
    by auto
  have nonz: "(enum N ∘ Suc) i > 0" for i
    using assms(1) le_enumerate less_le_trans by fastforce
  note infinite_nxt_N = infinite_nxtN [OF ‹infinite N›, iff]
  note ‹infinite N› [ iff]
  have [simp]: "{n<..<Suc n} = {}" "{..<1::nat} = {0}" for n
    by auto
  note One_nat_def [simp del]

  define DF_Suc where "DF_Suc ≡ λk D. enum (nxt N (enum (nxt N (Max D)) (Inf D - 1))) ` {..<Suc k}"
  define DF where "DF ≡ λk n. (DF_Suc k ^^ n) ((enum N ∘ Suc) ` {..<Suc k})"
  have DF_simps: "DF k 0 = (enum N ∘ Suc) ` {..<Suc k}" "DF k (Suc i) = DF_Suc k (DF k i)" for i k
    by (auto simp: DF_def)

  have card_DF: "card (DF k i) = Suc k" for i k
  proof (induction i)
    case 0
    have "inj_on (enum N ∘ Suc) {..<Suc k}"
      by (simp add: assms(1) strict_mono_def strict_mono_imp_inj_on)
    with 0 show ?case
      using card_image DF_simps by fastforce
  next
    case (Suc i)
    then show ?case
      by (simp add: ‹infinite N› DF_simps DF_Suc_def card_image infinite_nxtN strict_mono_enum strict_mono_imp_inj_on)
  qed
  have DF_ne: "DF k i ≠ {}" for i k
    by (metis card_DF card_lessThan lessThan_empty_iff nat.simps(3))

  have finite_DF: "finite (DF k i)" for i k
    by (induction i) (auto simp: DF_simps DF_Suc_def)
  have DF_Suc: "DF k i ≪ DF k (Suc i)" for i k
    unfolding less_sets_def
    by (force simp: finite_DF DF_simps DF_Suc_def
        intro!: greaterThan_less_enum nxt_subset_greaterThan atLeast_le_enum nxt_subset_atLeast infinite_nxtN [OF ‹infinite N›])
  have DF_DF: "DF k i ≪ DF k j" if "i<j" for i j k
    by (meson DF_Suc DF_ne UNIV_I less_sets_imp_strict_mono_sets strict_mono_setsD that)
  then have sm_DF: "strict_mono_sets UNIV (DF k)" for k
    by (simp add: strict_mono_sets_def)

  have DF_gt0: "0 < Inf (DF k i)" for i k
  proof (cases i)
    case 0
    then show ?thesis
      by (metis DF_ne DF_simps(1) Inf_nat_def1 imageE nonz)
  next
    case (Suc n)
    then show ?thesis
      by (metis DF_Suc DF_ne Inf_nat_def1 gr0I gr_implies_not0 less_sets_def)
  qed
  have DF_N: "DF k i ⊆ N" for i k
  proof (induction i)
    case 0
    then show ?case
      using ‹infinite N› range_enum by (auto simp: DF_simps)
  next
    case (Suc i)
    then show ?case
      unfolding DF_simps DF_Suc_def image_subset_iff
      by (metis IntE ‹infinite N› enumerate_in_set infinite_nxtN nxt_def)
  qed

  have sm_enum_DF: "strict_mono_on {..k} (enum (DF k i))" for k i
    by (metis card_DF enum_works_finite finite_DF lessThan_Suc_atMost)

  define AF where "AF ≡ λk i. enum (nxt N (Max (DF k i))) ` {..<Inf (DF k i)}"
  have AF_ne: "AF k i ≠ {}" for i k
    by (auto simp: AF_def lessThan_empty_iff DF_gt0)
  have finite_AF [simp]: "finite (AF k i)" for i k
    by (simp add: AF_def)
  have card_AF: "card (AF k i) = ⨅ (DF k i)" for k i
    by (simp add: AF_def card_image inj_enum_nxt)

  have DF_AF: "DF k i ≪ AF k i" for i k
    unfolding less_sets_def AF_def
    by (simp add: finite_DF greaterThan_less_enum nxt_subset_greaterThan)

  have E: "⟦x ≤ y; infinite M⟧ ⟹ enum M x < enum (nxt N (enum M y)) z" for x y z M
    by (metis infinite_nxt_N dual_order.eq_iff enumerate_mono greaterThan_less_enum nat_less_le nxt_subset_greaterThan)

  have AF_DF_Suc: "AF k i ≪ DF k (Suc i)" for i k
    by (auto simp: DF_simps DF_Suc_def less_sets_def AF_def E)

  have AF_DF: "AF k p ≪ DF k q" if "p<q" for k p q
    by (metis AF_DF_Suc DF_ne Suc_lessI UNIV_I less_sets_trans sm_DF strict_mono_sets_def that)

  have AF_Suc: "AF k i ≪ AF k (Suc i)" for i k
    using AF_DF_Suc DF_AF DF_ne less_sets_trans by blast
  then have sm_AF: "strict_mono_sets UNIV (AF k)" for k
    by (simp add: AF_ne less_sets_imp_strict_mono_sets)

  define del where "del ≡ λk i j. enum (DF k i) j - enum (DF k i) (j - 1)"

  define QF where "QF k ≡ wfrec pair_less (λf (j,i).
       if j=0 then AF k i
       else let r = (if i=0 then f (j-1,m-1) else f (j,i-1)) in
                enum (nxt N (Suc (Max r))) ` {..< del k (if j=k then m - Suc i else i) j})"
    for k
  note cut_apply [simp]

  have finite_QF [simp]: "finite (QF k p)" for p k
    using wf_pair_less
  proof (induction p rule: wf_induct_rule)
    case (less p)
    then show ?case
      by (simp add: def_wfrec [OF QF_def, of k p] split: prod.split)
  qed

  have del_gt_0: "⟦j < Suc k; 0 < j⟧ ⟹ 0 < del k i j" for i j k
    by (simp add: card_DF del_def finite_DF)

  have QF_ne [simp]: "QF k (j,i) ≠ {}" if j: "j < Suc k" for j i k
    using wf_pair_less j
  proof (induction "(j,i)" rule: wf_induct_rule)
    case less
    then show ?case
      by (auto simp: def_wfrec [OF QF_def, of k "(j,i)"] AF_ne lessThan_empty_iff del_gt_0)
  qed

  have QF_0 [simp]: "QF k (0,i) = AF k i" for i k
    by (simp add: def_wfrec [OF QF_def])

  have QF_Suc: "QF k (Suc j,0) = enum (nxt N (Suc (Max (QF k (j, m - 1))))) `
                       {..< del k (if Suc j = k then m - 1 else 0) (Suc j)}" for j k
    apply (simp add: def_wfrec [OF QF_def, of k "(Suc j,0)"] One_nat_def)
    apply (simp add: pair_less_def cut_def)
    done

  have QF_Suc_Suc: "QF k (Suc j, Suc i)
                  = enum (nxt N (Suc (Max (QF k (Suc j, i))))) ` {..< del k (if Suc j = k then m - Suc(Suc i) else Suc i) (Suc j)}"
    for i j k
    by (simp add: def_wfrec [OF QF_def, of k "(Suc j,Suc i)"])

  have less_QF1: "QF k (j, m - 1) ≪ QF k (Suc j,0)" for j k
    by (auto simp: def_wfrec [OF QF_def, of k "(Suc j,0)"] pair_lessI1 enum_nxt_ge
        intro!: less_sets_weaken2 [OF less_sets_Suc_Max])

  have less_QF2: "QF k (j,i) ≪ QF k (j, Suc i)" for j i k
    by (auto simp: def_wfrec [OF QF_def, of k "(j, Suc i)"] pair_lessI2 enum_nxt_ge
        intro: less_sets_weaken2 [OF less_sets_Suc_Max] strict_mono_setsD [OF sm_AF])

  have less_QF_same: "QF k (j,i') ≪ QF k (j,i)"
    if "i' < i" "j ≤ k" for i' i j k
  proof (rule strict_mono_setsD [OF less_sets_imp_strict_mono_sets])
    show "QF k (j, i) ≪ QF k (j, Suc i)" for i
      by (simp add: less_QF2)
    show "QF k (j, i) ≠ {}" if "0 < i" for i
      using that by (simp add: ‹j ≤ k› le_imp_less_Suc)
  qed (use that in auto)

  have less_QF_step: "QF k (j-1, i') ≪ QF k (j,i)"
    if "0 < j" "j ≤ k" "i' < m" for j i' i k
  proof -
    have less_QF1': "QF k (j - 1, m-1) ≪ QF k (j,0)" if "j > 0" for j
      by (metis less_QF1 that Suc_pred One_nat_def)
    have "QF k (j-1, i') ≪ QF k (j,0)"
    proof (cases "i' = m - 1")
      case True
      then show ?thesis
        using less_QF1' ‹0 < j› by blast
    next
      case False
      show ?thesis
        using False that less_sets_trans [OF less_QF_same less_QF1' QF_ne] by auto
    qed
    then show ?thesis
      by (metis QF_ne less_QF_same less_Suc_eq_le less_sets_trans ‹j ≤ k› zero_less_iff_neq_zero)
  qed

  have less_QF: "QF k (j',i') ≪ QF k (j,i)"
    if j: "j' < j" "j ≤ k" and i: "i' < m" "i < m" for j' j i' i k
    using j
  proof (induction "j-j'" arbitrary: j)
    case (Suc d)
    show ?case
    proof (cases "j' < j - 1")
      case True
      then have "QF k (j', i') ≪ QF k (j - 1, i)"
        using Suc.hyps Suc.prems(2) by force
      then show ?thesis
        by (rule less_sets_trans [OF _ less_QF_step QF_ne]) (use Suc i in auto)
    next
      case False
      then have "j' = j - 1"
        using ‹j' < j› by linarith
      then show ?thesis
        using Suc.hyps ‹j ≤ k› less_QF_step i by auto
    qed
  qed auto

  have sm_QF: "strict_mono_sets ({..k} × {..<m}) (QF k)" for k
    unfolding strict_mono_sets_def
  proof (intro strip)
    fix p q
    assume p: "p ∈ {..k} × {..<m}" and q: "q ∈ {..k} × {..<m}" and "p < q"
    then obtain j' i' j i where §: "p = (j',i')" "q = (j,i)" "i' < m" "i < m" "j' ≤ k" "j ≤ k"
      using surj_pair [of p] surj_pair [of q] by blast
    with ‹p < q› have "j' < j ∨ j' = j ∧ i' < i"
      by auto
    then show "QF k p ≪ QF k q"
      using § less_QF less_QF_same by presburger
  qed
  then have sm_QF1: "strict_mono_sets {..<ka} (λj. QF k (j,i))"
    if "i<m" "Suc k ≥ ka" "ka ≥ k" for ka k i
  proof -
    have "{..<ka} ⊆ {..k}"
      by (metis lessThan_Suc_atMost lessThan_subset_iff ‹Suc k ≥ ka›)
    then show ?thesis
      by (simp add: less_QF strict_mono_sets_def subset_iff that)
  qed

  have disjoint_QF: "i'=i ∧ j'=j" if "¬ disjnt (QF k (j', i')) (QF k (j,i))" "j' ≤ k" "j ≤ k" "i' < m" "i < m" for i' i j' j k
    using that strict_mono_sets_imp_disjoint [OF sm_QF]
    by (force simp: pairwise_def)

  have card_QF: "card (QF k (j,i)) = (if j=0 then ⨅ (DF k i) else del k (if j = k then m - Suc i else i) j)"
    for i k j
  proof (cases j)
    case 0
    then show ?thesis
      by (simp add: AF_def card_image inj_enum_nxt)
  next
    case (Suc j')
    show ?thesis
      by (cases i; simp add: Suc One_nat_def QF_Suc QF_Suc_Suc card_image inj_enum_nxt)
  qed
  have AF_non_Nil: "list_of (AF k i) ≠ []" for k i
    by (simp add: AF_ne)
  have QF_non_Nil: "list_of (QF k (j,i)) ≠ []" if "j < Suc k" for i j k
    by (simp add: that)

  have AF_subset_N: "AF k i ⊆ N" for i k
    unfolding AF_def image_subset_iff
    using nxt_subset enumerate_in_set infinite_nxtN ‹infinite N› by blast

  have QF_subset_N: "QF k (j,i) ⊆ N" for i j k
  proof (induction j)
    case (Suc j)
    show ?case
      by (cases i) (use nxt_subset enumerate_in_set in ‹(force simp: QF_Suc QF_Suc_Suc)+›)
  qed (use AF_subset_N in auto)

  obtain ka k where "k>0" and kka: "k ≤ ka" "ka ≤ Suc k" "l = ((ka+k) - 1)"
    by (metis One_nat_def assms(2) diff_add_inverse form_cases le0 le_refl)
  then have "ka > 0"
    using dual_order.strict_trans1 by blast
  have ka_k_or_Suc: "ka = k ∨ ka = Suc k"
    using kka by linarith
  have lessThan_k: "{..<k} = insert 0 {0<..<k}" if "k>0" for k::nat
    using that by auto
  then have sorted_list_of_set_k: "list_of {..<k} = 0 # list_of {0<..<k}" if "k>0" for k::nat
    using sorted_list_of_set_insert_remove_cons [of concl: 0 "{0<..<k}"] that by simp

  define RF where "RF ≡ λj i. if j = k then QF k (j, m - Suc i) else QF k (j,i)"
  have RF_subset_N: "RF j i ⊆ N" if "i<m" for i j
    using that QF_subset_N by (simp add: RF_def)
  have finite_RF [simp]: "finite (RF k p)" for p k
    by (simp add: RF_def)
  have RF_0: "RF 0 i = AF k i" for i
    using RF_def ‹0 < k› by auto
  have disjoint_RF: "i'=i ∧ j'=j" if "¬ disjnt (RF j' i') (RF j i)" "j' ≤ k" "j ≤ k" "i' < m" "i < m" for i' i j' j
    using disjoint_QF that
    by (auto simp: RF_def split: if_split_asm dest: disjoint_QF)

  have sum_card_RF [simp]: "(∑j≤n. card (RF j i)) = enum (DF k i) n" if "n ≤ k" "i < m" for i n
    using that
  proof (induction n)
    case 0
    then show ?case
      using DF_ne [of k i] finite_DF [of k i] ‹k>0›
      by (simp add: RF_def AF_def card_image inj_enum_nxt enum_0_eq_Inf_finite)
  next
    case (Suc n)
    then have "enum (DF k i) 0 ≤ enum (DF k i) n ∧ enum (DF k i) n ≤ enum (DF k i) (Suc n)"
      using sm_enum_DF [of k i]
      by (metis card_DF finite_DF finite_enumerate_mono_iff le_imp_less_Suc less_nat_zero_code linorder_not_le nless_le)
    with Suc show ?case
      by (auto simp: RF_def card_QF del_def)
  qed
  have DF_in_N: "enum (DF k i) j ∈ N" if "j ≤ k" for i j
    by (metis DF_N card_DF finite_DF finite_enumerate_in_set le_imp_less_Suc subsetD that)
  have Inf_DF_N: "⨅(DF k p) ∈ N" for k p
    using DF_N DF_ne Inf_nat_def1 by blast
  have RF_in_N: "(∑j≤n. card (RF j i)) ∈ N" if "n ≤ k" "i < m" for i n
    by (auto simp: DF_in_N that)

  have "ka - 1 ≤ k"
    using kka(2) by linarith
  then have sum_card_RF' [simp]:
    "(∑j<ka. card (RF j i)) = enum (DF k i) (ka - 1)" if "i < m" for i
    using sum_card_RF [of "ka - 1" i]
    by (metis Suc_diff_1 ‹0 < ka› lessThan_Suc_atMost that)

  have enum_DF_le_iff [simp]:
    "enum (DF k i) j ≤ enum (DF k i') j ⟷ i ≤ i'" (is "?lhs = _")
    if "j ≤ k" for i' i j k
  proof
    show "i ≤ i'" if ?lhs
    proof -
      have "enum (DF k i) j ∈ DF k i"
        by (simp add: card_DF finite_enumerate_in_set finite_DF le_imp_less_Suc ‹j ≤ k›)
      moreover have "enum (DF k i') j ∈ DF k i'"
        by (simp add: ‹j ≤ k› card_DF finite_enumerate_in_set finite_DF le_imp_less_Suc that)
      ultimately have "enum (DF k i') j < enum (DF k i) j" if "i' < i"
        using sm_DF [of k] by (meson UNIV_I less_sets_def strict_mono_setsD that)
      then show ?thesis
        using not_less that by blast
    qed
    show ?lhs if "i ≤ i'"
      by (metis DF_DF ‹j ≤ k› card_DF finite_DF finite_enumerate_in_set le_eq_less_or_eq 
                less_Suc_eq_le less_sets_def that)
  qed
  then have enum_DF_eq_iff[simp]:
    "enum (DF k i) j = enum (DF k i') j ⟷ i = i'" if "j ≤ k" for i' i j k
    by (metis le_antisym order_refl that)
  have enum_DF_less_iff [simp]:
    "enum (DF k i) j < enum (DF k i') j ⟷ i < i'" if "j ≤ k" for i' i j k
    by (meson enum_DF_le_iff not_less that)

  have card_AF_sum: "card (AF k i) + (∑j∈{0<..<ka}. card (RF j i)) = enum (DF k i) (ka-1)"
    if "i < m" for i
    using that ‹k > 0›  ‹k ≤ ka› ‹ka ≤ Suc k›
    by (simp add: lessThan_k RF_0 flip: sum_card_RF')

  have sorted_list_of_set_iff [simp]: "list_of {0<..<k} = [] ⟷ k = 1" if "k>0" for k::nat
    using atLeastSucLessThan_greaterThanLessThan that by fastforce
  show thesis ―‹proof of main result›
  proof
    have inj: "inj_on (λi. list_of (⋃j<ka. RF j i)) {..<m}"
    proof (clarsimp simp: inj_on_def)
      fix x y
      assume "x < m" "y < m" "list_of (⋃j<ka. RF j x) = list_of (⋃j<ka. RF j y)"
      then have eq: "(⋃j<ka. RF j x) = (⋃j<ka. RF j y)"
        by (simp add: sorted_list_of_set_inject)
      show "x = y"
      proof -
        obtain n where n: "n ∈ RF 0 x"
          using AF_ne QF_0 ‹0 < k› Inf_nat_def1 ‹k ≤ ka› by (force simp: RF_def)
        with eq ‹ka > 0› obtain j' where "j' < ka" "n ∈ RF j' y"
          by blast
        then show ?thesis
          using disjoint_QF [of k 0 x j'] n ‹x < m› ‹y < m› ‹ka ≤ Suc k› ‹0 < k›
          by (force simp: RF_def disjnt_iff simp del: QF_0 split: if_split_asm)
      qed
    qed

    define M where "M ≡ (λi. list_of (⋃j<ka. RF j i)) ` {..<m}"
    have "finite M"
      unfolding M_def by blast
    moreover have "card M = m"
      by (simp add: M_def ‹k ≤ ka› card_image inj)
    moreover have "M ⊆ WW"
      by (force simp: M_def WW_def)
    ultimately show "M ∈ [WW]⇗m⇖"
      by (simp add: nsets_def)

    have sm_RF: "strict_mono_sets {..<ka} (λj. RF j i)" if "i<m" for i
      using sm_QF1 that kka
      by (simp add: less_QF RF_def strict_mono_sets_def)

    have RF_non_Nil: "list_of (RF j i) ≠ []" if "j < Suc k" for i j
      using that by (simp add: RF_def)

    have less_RF_same: "RF j i' ≪ RF j i"
      if "i' < i" "j < k" for i' i j
      using that by (simp add: less_QF_same RF_def)

    have less_RF_same_k: "RF k i' ≪ RF k i" ―‹reversed version for @{term k}›
      if "i < i'" "i' < m" for i' i
      using that by (simp add: less_QF_same RF_def)

    show "Form l U ∧ list.set (inter_scheme l U) ⊆ N" if "U ∈ [M]⇗2⇖" for U
    proof -
      from that obtain x y where "U = {x,y}" "x ∈ M" "y ∈ M" and xy: "(x,y) ∈ lenlex less_than"
        by (auto simp: lenlex_nsets_2_eq)
      let ?R = "λp. list_of ∘ (λj. RF j p)"
      obtain p q where x: "x = list_of (⋃j<ka. RF j p)"
        and y: "y = list_of (⋃j<ka. RF j q)" and "p < m" "q < m"
        using ‹x ∈ M› ‹y ∈ M› by (auto simp: M_def)
      then have pq: "p<q" "length x < length y"
        using xy ‹k ≤ ka› ‹ka ≤ Suc k› lexl_not_refl [OF irrefl_less_than]
        by (auto simp: lenlex_def sm_RF sorted_list_of_set_UN_lessThan length_concat sum_sorted_list_of_set_map)
      have xc: "x = concat (map (?R p) (list_of {..<ka}))"
        by (simp add: x sorted_list_of_set_UN_eq_concat ‹k ≤ ka› ‹ka ≤ Suc k› ‹p < m› sm_RF)
      have yc: "y = concat (map (?R q) (list_of {..<ka}))"
        by (simp add: y sorted_list_of_set_UN_eq_concat ‹k ≤ ka› ‹ka ≤ Suc k› ‹q < m› sm_RF)
      have enum_DF_AF: "enum (DF k p) (ka - 1) < hd (list_of (AF k p))" for p
      proof (rule less_setsD [OF DF_AF])
        show "enum (DF k p) (ka - 1) ∈ DF k p"
          using ‹ka ≤ Suc k› card_DF finite_DF by (auto simp: finite_enumerate_in_set)
        show "hd (list_of (AF k p)) ∈ AF k p"
          using AF_non_Nil finite_AF hd_in_set set_sorted_list_of_set by blast
      qed

      have less_RF_RF: "RF n p ≪ RF n q" if "n < k" for n
        using that ‹p<q› by (simp add: less_RF_same)
      have less_RF_Suc: "RF n q ≪ RF (Suc n) q" if "n < k" for n
        using ‹q < m› that by (auto simp: RF_def less_QF)
      have less_RF_k: "RF k q ≪ RF k p"
        using ‹q < m› less_RF_same_k ‹p<q› by blast
      have less_RF_k_ka: "RF (k-1) p ≪ RF (ka - 1) q"
        using ka_k_or_Suc less_RF_RF
        by (metis One_nat_def RF_def ‹0 < k› ‹ka - 1 ≤ k› ‹p < m› diff_Suc_1 diff_Suc_less less_QF_step)
      have Inf_DF_eq_enum: "⨅ (DF k i) = enum (DF k i) 0" for k i
        by (simp add: Inf_nat_def enumerate_0)

      have Inf_DF_less: "⨅ (DF k i') < ⨅ (DF k i)" if "i'<i" for i' i k
        by (metis DF_ne enum_0_eq_Inf enum_0_eq_Inf_finite enum_DF_less_iff le0 that)
      have AF_Inf_DF_less: "⋀x. x ∈ AF k i ⟹ ⨅ (DF k i') < x" if "i'≤i" for i' i k
        using less_setsD [OF DF_AF] DF_ne that
        by (metis Inf_DF_less Inf_nat_def1 dual_order.order_iff_strict dual_order.strict_trans)

      show ?thesis ―‹The general case requires @{term‹k>1›}, necessitating a painful special case›
      proof (cases "k=1")
        case True
        with kka consider "ka=1" | "ka=2" by linarith
        then show ?thesis
        proof cases
          case 1
          define zs where "zs = card (AF 1 p) # list_of (AF 1 p)
                              @ card (AF 1 q) # list_of (AF 1 q)"
          have zs: "Form_Body ka k x y zs"
          proof (intro that exI conjI Form_Body.intros)
            show "x = concat ([list_of (AF k p)])" "y = concat ([list_of (AF k q)])"
              by (simp_all add: x y 1 lessThan_Suc RF_0)
            have "AF k p ≪ insert (⨅ (DF k q)) (AF k q)"
              by (metis AF_DF DF_ne Inf_nat_def1 RF_0 ‹0 < k› insert_iff less_RF_RF less_sets_def pq(1))
            then have "strict_sorted (list_of (AF k p) @ ⨅ (DF k q) # list_of (AF k q))"
              by (auto simp: strict_sorted_append_iff intro: less_sets_imp_list_less AF_Inf_DF_less)
            moreover have "⋀x. x ∈ AF k q ⟹ ⨅ (DF k p) < x"
              by (meson AF_Inf_DF_less less_imp_le_nat ‹p < q›)
            moreover have "⋀x. x ∈ AF 1 p ⟹ ⨅ (DF 1 p) < x"
              by (meson DF_AF DF_ne Inf_nat_def1 less_setsD)
            ultimately show "strict_sorted zs"
              using ‹p < q› True Inf_DF_less DF_AF DF_ne
              by (auto simp: zs_def less_sets_def card_AF AF_Inf_DF_less)
          qed (auto simp: ‹k=1› ‹ka=1› zs_def AF_ne ‹length x < length y›)
          have zs_N: "list.set zs ⊆ N"
            using AF_subset_N by (auto simp: zs_def card_AF Inf_DF_N ‹k=1›)
          show ?thesis
          proof
            have "l = 1"
              using kka ‹k=1› ‹ka=1› by auto
            have "Form (2*1-1) {x,y}"
              using "1" Form.intros(2) True zs by fastforce
            then show "Form l U"
              by (simp add: ‹U = {x,y}› ‹l = 1› One_nat_def)
            show "list.set (inter_scheme l U) ⊆ N"
              using kka zs zs_N ‹k=1› Form_Body_imp_inter_scheme by (fastforce simp: ‹U = {x,y}›)
          qed
        next
          case 2 ―‹Still in our painful special case›
          note True [simp] note 2 [simp]
          have [simp]: "{0<..<2} = {1::nat}"
            by auto

          have enum_DF1_eq: "enum (DF 1 i) 1 = card (AF 1 i) + card (RF 1 i)"
            if "i < m" for i
            using card_AF_sum that by (simp add: One_nat_def)
          have card_RF: "card (RF 1 i) = enum (DF 1 i) 1 - enum (DF 1 i) 0" if "i < m" for i
            using that by (auto simp: RF_def card_QF del_def)
          have list_of_AF_RF: "list_of (AF 1 q ∪ RF 1 q) = list_of (AF 1 q) @ list_of (RF 1 q)"
            by (metis One_nat_def RF_0 True ‹0 < k› finite_RF less_RF_Suc sorted_list_of_set_Un)

          define zs where "zs = card (AF 1 p) # (card (AF 1 p) + card (RF 1 p)) # list_of (AF 1 p)
                  @ (card (AF 1 q) + card (RF 1 q)) # list_of (AF 1 q) @ list_of (RF 1 q) @ list_of (RF 1 p)"
          have zs: "Form_Body ka k x y zs"
          proof (intro that exI conjI Form_Body.intros)
            have "x = list_of (RF 0 p ∪ RF 1 p)"
              by (simp add: x eval_nat_numeral lessThan_Suc RF_0 Un_commute One_nat_def)
            also have "… = list_of (RF 0 p) @ list_of (RF 1 p)"
              using RF_def True ‹p < m› less_QF_step
              by (metis QF_0 RF_0 diff_self_eq_0 finite_RF le_refl sorted_list_of_set_Un zero_less_one)
            finally show "x = concat ([list_of (AF 1 p),list_of (RF 1 p)])"
              by (simp add: RF_0)

            have *: "i ∈ AF 1 q ∨ i ∈ RF 1 q ∨ i ∈ RF 1 p ⟹ enum (DF 1 q) 1 < i" for i
              using True card_DF finite_enumerate_in_set[OF finite_DF] 
              by (metis AF_ne DF_AF One_nat_def RF_0 RF_non_Nil finite_RF lessI less_RF_Suc less_RF_k less_setsD 
                  less_sets_trans sorted_list_of_set.sorted_key_list_of_set_eq_Nil_iff)

            show "y = concat [list_of (RF 1 q ∪ AF 1 q)]"
              by (simp add: y eval_nat_numeral lessThan_Suc RF_0 One_nat_def)
            show zs: "zs = concat [[card (AF 1 p), card (AF 1 p) + card (RF 1 p)], list_of (AF 1 p),
                                  [card (AF 1 q) + card (RF 1 q)], list_of (RF 1 q ∪ AF 1 q)] @ interact [list_of (RF 1 p)] []"
              using list_of_AF_RF by (simp add: zs_def Un_commute)

            show "strict_sorted zs"
            proof (simp add: ‹p<m› ‹q<m› ‹p<q› zs_def strict_sorted_append_iff, intro conjI strip)
              show "0 < card (RF 1 p)"
                using ‹p<m› by (simp add: card_RF card_DF finite_DF)
              show G1: "card (AF 1 p) < card (AF 1 q) + card (RF 1 q)"
                by (simp add: Inf_DF_less card_AF ‹p<q› trans_less_add1)
              show "card (AF 1 p) < x"
                if "x ∈ AF 1 p ∪ (AF 1 q ∪ (RF 1 q ∪ RF 1 p))" for x
                using that ‹q < m› *
                  by (metis (no_types) order_refl AF_Inf_DF_less Un_iff G1 card_AF order.strict_trans enum_DF1_eq that)
              show G2: "card (AF 1 p) + card (RF 1 p) < card (AF 1 q) + card (RF 1 q)"
                using ‹p < q› ‹p < m› ‹q < m› by (metis enum_DF1_eq enum_DF_less_iff le_refl)
              show "card (AF 1 q) + card (RF 1 q) < x"
                if "x ∈ AF 1 q ∪ (RF 1 q ∪ RF 1 p)" for x
                using that ‹q < m› * enum_DF1_eq by force
              then show "card (AF 1 p) + card (RF 1 p) < x"
                if "x ∈ AF 1 p ∪ (AF 1 q ∪ (RF 1 q ∪ RF 1 p))" for x
                using that ‹p < m› finite_enumerate_in_set[OF finite_DF]
                by (metis DF_AF G2 Un_iff card_DF dual_order.strict_trans enum_DF1_eq lessI less_setsD) 
              have "list_of (AF 1 p) < list_of {enum (DF 1 q) 1}"
              proof (rule less_sets_imp_sorted_list_of_set)
                show "AF 1 p ≪ {enum (DF 1 q) 1}"
                  by (metis AF_DF card_DF empty_subsetI finite_DF finite_enumerate_in_set insert_subset 
                      less_Suc_eq less_sets_weaken2 ‹p<q›)
              qed auto
              then show "list_of (AF 1 p) < (card (AF 1 q) + card (RF 1 q)) # list_of (AF 1 q) @ list_of (RF 1 q) @ list_of (RF 1 p)"
                using ‹q < m› by (simp add: less_list_def enum_DF1_eq)
              have "list_of (AF 1 q) < list_of (RF 1 q)"
                by (metis One_nat_def RF_0 True ‹0 < k› finite_RF less_RF_Suc less_sets_imp_sorted_list_of_set)           
              then show "list_of (AF 1 q) < list_of (RF 1 q) @ list_of (RF 1 p)"
                using RF_non_Nil by (auto simp: less_list_def)
              show "list_of (RF 1 q) < list_of (RF 1 p)"
                using True finite_RF less_RF_k less_sets_imp_sorted_list_of_set by metis
            qed
            show "[list_of (AF 1 p), list_of (RF 1 p)] ∈ lists (- {[]})"
              using RF_non_Nil ‹0 < k› by (auto simp: zs_def AF_ne)
            show "[card (AF 1 q) + card (RF 1 q)] = acc_lengths 0 [list_of (RF 1 q ∪ AF 1 q)]"
              using list_of_AF_RF by (auto simp: zs_def AF_ne sup_commute)
          qed (auto simp: zs_def AF_ne ‹length x < length y›)
          have zs_N: "list.set zs ⊆ N"
            using ‹p < m› ‹q < m› DF_in_N  enum_DF1_eq [symmetric]
            by (auto simp: zs_def card_AF AF_subset_N RF_subset_N Inf_DF_N)
          show ?thesis
          proof
            have "Form (2*1) {x,y}"
              by (metis "2" Form.simps Suc_1 True zero_less_one zs)
            with kka show "Form l U"
              by (simp add: ‹U = {x,y}›)
            show "list.set (inter_scheme l U) ⊆ N"
              using kka zs zs_N ‹k=1› Form_Body_imp_inter_scheme by (fastforce simp: ‹U = {x, y}›)
          qed
        qed
      next
        case False
        then have "k ≥ 2" "ka ≥ 2"
          using kka ‹k>0› by auto
        then have k_minus_1 [simp]: "Suc (k - Suc (Suc 0)) = k - Suc 0"
          by auto
        have [simp]: "Suc (k - 2) = k-1"
          using ‹k ≥ 2› by linarith
        define PP where "PP ≡ map (?R p) (list_of {0<..<ka})"
        define QQ where "QQ ≡ map (?R q) (list_of {0<..<k-1}) @ ([list_of (RF (k-1) q ∪ RF (ka-1) q)])"
        let ?INT = "interact PP QQ"
        ―‹No separate sets A and B as in the text, but instead we treat both cases as once›
        have [simp]: "length PP = ka - 1"
          by (simp add: PP_def)
        have [simp]: "length QQ = k-1"
          using ‹k ≥ 2› by (simp add: QQ_def)

        have PP_n: "PP ! n = list_of (RF (Suc n) p)"
          if "n < ka-1" for n
          using that kka by (auto simp: PP_def nth_sorted_list_of_set_greaterThanLessThan)

        have QQ_n: "QQ ! n = (if n < k-2 then list_of (RF (Suc n) q)
                              else list_of (RF (k-1) q ∪ RF (ka - 1) q))"
          if "n < k-1" for n
          using that kka by (auto simp: QQ_def nth_append nth_sorted_list_of_set_greaterThanLessThan)

        have QQ_n_same: "QQ ! n = list_of (RF (Suc n) q)"
          if "n < k-1" "k=ka" for n
          using that kka Suc_diff_Suc
          by (fastforce simp: One_nat_def QQ_def nth_append nth_sorted_list_of_set_greaterThanLessThan)

        have split_nat_interval: "{0<..<n} = insert (n-1) {0<..<n-1}" if "n ≥ 2" for n::nat
          using that by auto
        have split_list_interval: "list_of{0<..<n} = list_of{0<..<n-1} @ [n-1]" if "n ≥ 2" for n::nat
        proof (intro sorted_list_of_set_unique [THEN iffD1] conjI)
          have "list_of {0<..<n - 1} < [n - 1]"
            by (auto intro: less_sets_imp_list_less)
          then show "strict_sorted (list_of {0<..<n - 1} @ [n - 1])"
            by (auto simp: strict_sorted_append_iff)
        qed (use ‹n ≥ 2› in auto)

        have list_of_RF_Un: "list_of (RF (k-1) q ∪ RF k q) = list_of (RF (k-1) q) @ list_of (RF k q)"
          by (metis Suc_diff_1 ‹0 < k› finite_RF lessI less_RF_Suc sorted_list_of_set_Un)

        have card_AF_sum_QQ: "card (AF k q) + sum_list (map length QQ) = (∑j<ka. card (RF j q))"
        proof (cases "ka = Suc k")
          case True
          have "RF (k-1) q ∩ RF k q = {}"
            using less_RF_Suc [of "k-1"] ‹k > 0› by (auto simp: less_sets_def)
          then have "card (RF (k-1) q ∪ RF k q) = card (RF (k-1) q) + card (RF k q)"
            by (simp add: card_Un_disjoint)
          then show ?thesis
            using ‹k≥2› ‹q < m›
            apply (simp add: QQ_def True flip: RF_0)
            apply (simp add: lessThan_k split_nat_interval sum_sorted_list_of_set_map)
            done
        next
          case False
          with kka have "ka=k" by linarith
          with ‹k≥2› show ?thesis by (simp add: QQ_def lessThan_k split_nat_interval sum_sorted_list_of_set_map flip: RF_0)
        qed

        define LENS where "LENS ≡ λi. acc_lengths 0 (list_of (AF k i) # map (?R i) (list_of {0<..<ka}))"
        have LENS_subset_N: "list.set (LENS i) ⊆ N" if "i < m" for i
        proof -
          have eq: "(list_of (AF k i) # map (?R i) (list_of {0<..<ka})) = map (?R i) (list_of {..<ka})"
            using RF_0 ‹0 < ka› sorted_list_of_set_k by auto
          let ?f = "rec_nat [card (AF k i)] (λn r. r @ [(∑j≤Suc n. card (RF j i))])"
          have f: "acc_lengths 0 (map (?R i) (list_of {..v})) = ?f v" for v
            by (induction v) (auto simp: RF_0 acc_lengths_append sum_sorted_list_of_set_map)
          have 3: "list.set (?f v) ⊆ N" if "v ≤ k" for v
            using that
          proof (induction v)
            case 0
            have "card (AF k i) ∈ N"
              by (metis DF_N DF_ne Inf_nat_def1 card_AF subsetD)
            with 0 show ?case by simp
          next
            case (Suc v)
            then have "enum (DF k i) (Suc v) ∈ N"
              by (metis DF_N card_DF finite_enumerate_in_set finite_DF in_mono le_imp_less_Suc)
            with Suc ‹i < m› show ?case
              by (simp del: sum.atMost_Suc)
          qed
          show ?thesis
            unfolding LENS_def
            by (metis 3 Suc_pred' ‹0 < ka› ‹ka - 1 ≤ k› eq f lessThan_Suc_atMost)
        qed
        define LENS_QQ where "LENS_QQ ≡ acc_lengths 0 (list_of (AF k q) # QQ)"
        have LENS_QQ_subset: "list.set LENS_QQ ⊆ list.set (LENS q)"
        proof (cases "ka = Suc k")
          case True
          with ‹k ≥ 2› show ?thesis
            unfolding QQ_def LENS_QQ_def LENS_def
            by (auto simp: list_of_RF_Un split_list_interval acc_lengths_append)
        next
          case False
          then have "ka=k"
            using kka by linarith
          with ‹k ≥ 2› show ?thesis
            by (simp add: QQ_def LENS_QQ_def LENS_def split_list_interval)
        qed
        have ss_INT: "strict_sorted ?INT"
        proof (rule strict_sorted_interact_I)
          fix n
          assume "n < length QQ"
          then have n: "n < k-1"
            by simp
          have "n = k - 2" if "¬ n < k - 2"
            using n that by linarith
          moreover have "list_of (RF (Suc (k - 2)) p) < list_of (RF (k-1) q ∪ RF (ka - 1) q)"
            by (auto simp: less_sets_imp_sorted_list_of_set less_sets_Un2 less_RF_RF less_RF_k_ka ‹0 < k›)
          ultimately show "PP ! n < QQ ! n"
            using ‹k ≤ ka› n by (auto simp: PP_n QQ_n less_sets_imp_sorted_list_of_set less_RF_RF)
        next
          fix n
          have V: "⟦Suc n < ka - 1⟧ ⟹ list_of (RF (Suc n) q) < list_of (RF (Suc (Suc n)) p)" for n
            by (smt RF_def Suc_leI ‹ka - 1 ≤ k› ‹q < m› diff_Suc_1 finite_RF less_QF_step less_le_trans less_sets_imp_sorted_list_of_set nat_neq_iff zero_less_Suc)
          have "RF (k -  1) q ≪ RF k p"
            by (metis One_nat_def RF_non_Nil Suc_pred ‹0 < k› finite_RF lessI less_RF_Suc less_RF_k less_sets_trans sorted_list_of_set_eq_Nil_iff)
          with kka have "RF (k-1) q ∪ RF (ka - 1) q ≪ RF k p"
            by (metis less_RF_k One_nat_def less_sets_Un1 antisym_conv2 diff_Suc_1 le_less_Suc_eq)
          then have VI: "list_of (RF (k-1) q ∪ RF (ka - 1) q) < list_of (RF k p)"
            by (rule less_sets_imp_sorted_list_of_set) auto
          assume "Suc n < length PP"
          with ‹ka ≤ Suc k› VI
          show "QQ ! n < PP ! Suc n"
            apply (clarsimp simp: PP_n QQ_n V)
            by (metis One_nat_def Suc_1 Suc_lessI add.right_neutral add_Suc_right diff_Suc_Suc ka_k_or_Suc less_diff_conv)
        next 
          show "PP ∈ lists (- {[]})"
            using RF_non_Nil kka
            by (clarsimp simp: PP_def) (metis RF_non_Nil less_le_trans)
          show "QQ ∈ lists (- {[]})"
            using RF_non_Nil kka
            by (clarsimp simp: QQ_def) (metis RF_non_Nil Suc_pred ‹0 < k› less_SucI One_nat_def)
        qed (use kka PP_def QQ_def in auto)
        then have ss_QQ: "strict_sorted (concat QQ)"
          using strict_sorted_interact_imp_concat by blast

        obtain zs where zs: "Form_Body ka k x y zs" and zs_N: "list.set zs ⊆ N"
        proof (intro that exI conjI Form_Body.intros [OF ‹length x < length y›])
          show "x = concat (list_of (AF k p) # PP)"
            using ‹ka > 0› by (simp add: PP_def RF_0 xc sorted_list_of_set_k)
          let ?YR = "(map (list_of ∘ (λj. RF j q)) (list_of {0<..<ka}))"
          have "concat ?YR = concat QQ"
          proof (rule strict_sorted_equal [OF ss_QQ])
            show "strict_sorted (concat ?YR)"
            proof (rule strict_sorted_concat_I, simp_all)
              fix n
              assume 0: "Suc n < ka - Suc 0" 
              then have "Suc n < k"
                by (metis One_nat_def ‹ka - 1 ≤ k› less_le_trans)
              then show "list_of (RF (list_of {0<..<ka} ! n) q) < list_of (RF (list_of {0<..<ka} ! Suc n) q)"
                by (simp add: Suc_lessD 0 less_RF_Suc less_sets_imp_sorted_list_of_set nth_sorted_list_of_set_greaterThanLessThan)
            next
              show "?YR ∈ lists (- {[]})"
                using RF_non_Nil ‹ka ≤ Suc k› by (auto simp: mem_lists_non_Nil)
            qed auto
            show "list.set (concat ?YR) = list.set (concat QQ)"
              using ka_k_or_Suc
            proof
              assume "ka = k"
              then show "list.set (concat (map (list_of ∘ (λj. RF j q)) (list_of {0<..<ka}))) = list.set (concat QQ)"
                using ‹k≥2› by simp (simp add: split_nat_interval QQ_def)
            next
              assume "ka = Suc k"
              then show "list.set (concat (map (list_of ∘ (λj. RF j q)) (list_of {0<..<ka}))) = list.set (concat QQ)"
                using ‹k≥2› by simp (auto simp: QQ_def split_nat_interval)
            qed
          qed
          then show "y = concat (list_of (AF k q) # QQ)"
            using ‹ka > 0› by (simp add: RF_0 yc sorted_list_of_set_k)
          show "list_of (AF k p) # PP ∈ lists (- {[]})" "list_of (AF k q) # QQ ∈ lists (- {[]})"
            using  RF_non_Nil kka by (auto simp: AF_ne PP_def QQ_def eq_commute [of "[]"])
          show "list.set ((LENS p @ list_of (AF k p) @ LENS_QQ @ list_of (AF k q) @ ?INT)) ⊆ N"
            using AF_subset_N RF_subset_N LENS_subset_N ‹p < m› ‹q < m› LENS_QQ_subset
            by (auto simp: subset_iff PP_def QQ_def)
          show "length (list_of (AF k p) # PP) = ka" "length (list_of (AF k q) # QQ) = k"
            using ‹0 < ka› ‹0 < k› by auto
          show "LENS p = acc_lengths 0 (list_of (AF k p) # PP)"
            by (auto simp: LENS_def PP_def)
          show "strict_sorted (LENS p @ list_of (AF k p) @ LENS_QQ @ list_of (AF k q) @ ?INT)"
            unfolding strict_sorted_append_iff
          proof (intro conjI ss_INT)
            show "LENS p < list_of (AF k p) @ LENS_QQ @ list_of (AF k q) @ ?INT"
              using AF_non_Nil [of k p] ‹k ≤ ka› ‹ka ≤ Suc k› ‹p < m› card_AF_sum enum_DF_AF
              by (simp add: enum_DF_AF less_list_def card_AF_sum LENS_def sum_sorted_list_of_set_map
                       del: acc_lengths.simps)
            show "strict_sorted (LENS p)"
              unfolding LENS_def
              by (rule strict_sorted_acc_lengths) (use RF_non_Nil AF_non_Nil kka in ‹auto simp: in_lists_conv_set›)
            show "strict_sorted LENS_QQ"
              unfolding LENS_QQ_def QQ_def
              by (rule strict_sorted_acc_lengths) (use RF_non_Nil AF_non_Nil kka in ‹auto simp: in_lists_conv_set›)
            have last_AF_DF: "last (list_of (AF k p)) < ⨅ (DF k q)"
              using AF_DF [OF ‹p < q›, of k] AF_non_Nil [of k p] DF_ne [of k q]
              by (metis Inf_nat_def1 finite_AF last_in_set less_sets_def set_sorted_list_of_set)
            then show "list_of (AF k p) < LENS_QQ @ list_of (AF k q) @ ?INT"
              by (simp add: less_list_def card_AF LENS_QQ_def)
            show "LENS_QQ < list_of (AF k q) @ ?INT"
              using AF_non_Nil [of k q] ‹q < m› card_AF_sum enum_DF_AF card_AF_sum_QQ
              by (auto simp: less_list_def AF_ne hd_append card_AF_sum LENS_QQ_def)
            show "list_of (AF k q) < ?INT"
            proof -
              have "AF k q ≪ RF 1 p"
                using ‹0 < k› ‹p < m› ‹q < m› by (simp add: RF_def less_QF flip: QF_0)
              then have "last (list_of (AF k q)) < hd (list_of (RF 1 p))"
              proof (rule less_setsD)
                show "last (list_of (AF k q)) ∈ AF k q"
                  using AF_non_Nil finite_AF last_in_set set_sorted_list_of_set by blast
                show "hd (list_of (RF 1 p)) ∈ RF 1 p"
                  by (metis One_nat_def RF_non_Nil ‹0 < k› finite_RF hd_in_set not_less_eq set_sorted_list_of_set)
              qed
              with ‹k > 0› ‹ka ≥ 2› RF_non_Nil show ?thesis
                by (simp add: One_nat_def hd_interact less_list_def sorted_list_of_set_greaterThanLessThan PP_def QQ_def)
            qed
          qed auto
        qed (auto simp: LENS_QQ_def)
        show ?thesis
        proof (cases "ka = k")
          case True
          then have "l = 2*k-1"
            by (simp add: kka(3) mult_2)
          then show ?thesis
            by (metis One_nat_def Form.intros(2) Form_Body_imp_inter_scheme True ‹0 < k› ‹U = {x, y}› kka zs zs_N)
        next
          case False
          then have "l = 2*k"
            using kka by linarith
          then show ?thesis
            by (metis One_nat_def False Form.intros(3) Form_Body_imp_inter_scheme ‹0 < k› ‹U = {x, y}› antisym kka le_SucE zs zs_N)
        qed
      qed
    qed
  qed
qed


subsection ‹Larson's Lemma 3.8›

subsubsection ‹Primitives needed for the inductive construction of @{term b}›

definition IJ where "IJ ≡ λk. Sigma {..k} (λj::nat. {..<j})"

lemma IJ_iff: "u ∈ IJ k ⟷ (∃j i. u = (j,i) ∧ i<j ∧ j≤k)"
  by (auto simp: IJ_def)

lemma finite_IJ: "finite (IJ k)"
  by (auto simp: IJ_def)

fun prev where
  "prev 0 0 = None"
| "prev (Suc 0) 0 = None"
| "prev (Suc j) 0 = Some (j, j - Suc 0)"
| "prev j (Suc i) = Some (j,i)"

lemma prev_eq_None_iff: "prev j i = None ⟷ j ≤ Suc 0 ∧ i = 0"
  by (auto simp: le_Suc_eq elim: prev.elims)

lemma prev_pair_less:
  "prev j i = Some ji' ⟹ (ji', (j,i)) ∈ pair_less"
  by (auto simp: pair_lessI1 elim: prev.elims)

lemma prev_Some_less: "⟦prev j i = Some (j',i'); i ≤ j⟧ ⟹ i' < j'"
  by (auto elim: prev.elims)

lemma prev_maximal:
  "⟦prev j i = Some (j',i'); (ji'', (j,i)) ∈ pair_less; ji'' ∈ IJ k⟧
   ⟹ (ji'', (j',i')) ∈ pair_less ∨ ji'' = (j',i')"
  by (force simp: IJ_def pair_less_def elim: prev.elims)

lemma pair_less_prev:
  assumes "(u, (j,i)) ∈ pair_less" "u ∈ IJ k"
  shows "prev j i = Some u ∨ (∃x. (u, x) ∈ pair_less ∧ prev j i = Some x)"
  using assms
proof (cases "prev j i")
  case None
  then show ?thesis
    using assms by (force simp: prev_eq_None_iff pair_less_def IJ_def split: prod.split)
next
  case (Some a)
  then show ?thesis
    by (metis assms prev_maximal prod.exhaust_sel)
qed


subsubsection ‹Special primitives for the ordertype proof›

definition USigma :: "'a set set ⇒ ('a set ⇒ 'a set) ⇒ 'a set set"
  where "USigma 𝒜 B ≡ ⋃X∈𝒜. ⋃y ∈ B X. {insert y X}"

definition usplit
  where "usplit f A ≡ f (A - {Max A}) (Max A)"

lemma USigma_empty [simp]: "USigma {} B = {}"
  by (auto simp: USigma_def)

lemma USigma_iff:
  assumes "⋀I j. I ∈ ℐ ⟹ I ≪ J I ∧ finite I"
  shows "x ∈ USigma ℐ J ⟷ usplit (λI j. I ∈ ℐ ∧ j ∈ J I ∧ x = insert j I) x"
proof -
  have [simp]: "⋀I j. ⟦I ∈ ℐ; j ∈ J I⟧ ⟹ Max (insert j I) = j"
    by (meson Max_insert2 assms less_imp_le less_sets_def)
  show ?thesis
  proof -
    have §: "j ∉ I" if "I ∈ ℐ" "j ∈ J I" for I j
      using that by (metis assms less_irrefl less_sets_def)
    have "∃I∈ℐ. ∃j∈J I. x = insert j I"
      if "x - {Max x} ∈ ℐ" and "Max x ∈ J (x - {Max x})" "x ≠ {}"
      using that by (metis Max_in assms infinite_remove insert_Diff)
    then show ?thesis
      by (auto simp: USigma_def usplit_def §)
  qed
qed


proposition ordertype_append_image_IJ:
  assumes lenB [simp]: "⋀i j. i ∈ ℐ ⟹ j ∈ J i ⟹ length (B j) = c"
    and AB: "⋀i j. i ∈ ℐ ⟹ j ∈ J i ⟹ A i < B j"
    and IJ: "⋀i. i ∈ ℐ ⟹ i ≪ J i ∧ finite i"
    and β: "⋀i. i ∈ ℐ ⟹ ordertype (B ` J i) (lenlex less_than) = β"
    and A: "inj_on A ℐ"
  shows "ordertype (usplit (λi j. A i @ B j) ` USigma ℐ J) (lenlex less_than)
       = β * ordertype (A ` ℐ) (lenlex less_than)"
    (is "ordertype ?AB ?R = _ * ?α")
proof (cases "ℐ = {}")
  case False
  have "Ord β"
    using β False wf_Ord_ordertype by fastforce
  show ?thesis
  proof (subst ordertype_eq_iff)
    define split where "split ≡ λl::nat list. (take (length l - c) l, (drop (length l - c) l))"
    have oB: "ordermap (B ` J i) ?R (B j) ⊏ β" if ‹i ∈ ℐ› ‹j ∈ J i› for i j
      using β less_TC_iff that by fastforce
    then show "Ord (β * ?α)"
      by (intro ‹Ord β› wf_Ord_ordertype Ord_mult; simp)
    define f where "f ≡ λu. let (x,y) = split u in let i = inv_into ℐ A x in
                        β * ordermap (A`ℐ) ?R x + ordermap (B`J i) ?R y"
    have inv_into_IA [simp]: "inv_into ℐ A (A i) = i" if "i ∈ ℐ" for i
      by (simp add: A that)
    show "∃f. bij_betw f ?AB (elts (β * ?α)) ∧ (∀x∈?AB. ∀y∈?AB. (f x < f y) = ((x, y) ∈ ?R))"
      unfolding bij_betw_def
    proof (intro exI conjI strip)
      show "inj_on f ?AB"
      proof (clarsimp simp: f_def inj_on_def split_def USigma_iff IJ usplit_def)
        fix x y
        assume §: "β * ordermap (A ` ℐ) ?R (A (x - {Max x})) + ordermap (B ` J (x - {Max x})) ?R (B (Max x))
                 = β * ordermap (A ` ℐ) ?R (A (y - {Max y})) + ordermap (B ` J (y - {Max y})) ?R (B (Max y))"
          and x: "x - {Max x} ∈ ℐ"
          and y: "y - {Max y} ∈ ℐ"
          and mx: "Max x ∈ J (x - {Max x})"
          and "x = insert (Max x) x"
          and my: "Max y ∈ J (y - {Max y})"
        have "ordermap (A`ℐ) ?R (A (x - {Max x})) = ordermap (A`ℐ) ?R (A (y - {Max y}))"
          and B_eq: "ordermap (B ` J (x - {Max x})) ?R (B (Max x)) = ordermap (B ` J (y - {Max y})) ?R (B (Max y))"
          using mult_cancellation_lemma [OF §] oB mx my x y by blast+
        then have "A (x - {Max x}) = A (y - {Max y})"
          using x y by auto
        then have "x - {Max x} = y - {Max y}"
          by (metis x y inv_into_IA)
        then show "A (x - {Max x}) = A (y - {Max y}) ∧ B (Max x) = B (Max y)"
          using B_eq mx my by auto
      qed
      show "f ` ?AB = elts (β * ?α)"
      proof
        show "f ` ?AB ⊆ elts (β * ?α)"
          using ‹Ord β›
          apply (clarsimp simp add: f_def split_def USigma_iff IJ usplit_def)
          by (metis TC_small β add_mult_less image_eqI ordermap_in_ordertype trans_llt wf_Ord_ordertype wf_llt)
        show "elts (β * ?α) ⊆ f ` ?AB"
        proof (clarsimp simp: f_def split_def image_iff USigma_iff IJ usplit_def Bex_def elim!: elts_multE split: prod.split)
          fix γ δ
          assume δ: "δ ∈ elts β" and γ: "γ ∈ elts ?α"
          have "γ ∈ ordermap (A ` ℐ) (lenlex less_than) ` A ` ℐ"
            by (meson γ ordermap_surj subset_iff)
          then obtain i where "i ∈ ℐ" and yv: "γ = ordermap (A`ℐ) ?R (A i)"
            by blast
          have "δ ∈ ordermap (B ` J i) (lenlex less_than) ` B ` J i"
            by (metis (no_types) β δ ‹i ∈ ℐ› in_mono ordermap_surj)
          then obtain j where "j ∈ J i" and xu: "δ = ordermap (B`J i) ?R (B j)"
            by blast
          then have mji: "Max (insert j i) = j"
            by (meson IJ Max_insert2 ‹i ∈ ℐ› less_imp_le less_sets_def)
          have [simp]: "i - {j} = i"
            using IJ ‹i ∈ ℐ› ‹j ∈ J i› less_setsD by fastforce
          show "∃l. (∃K. K - {Max K} ∈ ℐ ∧ Max K ∈ J (K - {Max K}) ∧ K = insert (Max K) K ∧
                         l = A (K - {Max K}) @ B (Max K)) ∧ β * γ + δ =
                    β *
                    ordermap (A ` ℐ) ?R (take (length l - c) l) +
                    ordermap (B ` J (inv_into ℐ A (take (length l - c) l)))
                     ?R (drop (length l - c) l)"
          proof (intro conjI exI)
          let ?ji = "insert j i"
            show "A i @ B j = A (?ji - {Max ?ji}) @ B (Max ?ji)"
              by (auto simp: mji)
          qed (use ‹i ∈ ℐ› ‹j ∈ J i› mji xu yv in auto)
        qed
      qed
    next
      fix p q
      assume "p ∈ ?AB" and "q ∈ ?AB"
      then obtain x y where peq: "p = A (x - {Max x}) @ B (Max x)"
                      and qeq: "q = A (y - {Max y}) @ B (Max y)"
                      and x: "x - {Max x} ∈ ℐ"
                      and y: "y - {Max y} ∈ ℐ"
                      and mx: "Max x ∈ J (x - {Max x})"
                      and my: "Max y ∈ J (y - {Max y})"
        by (auto simp: USigma_iff IJ usplit_def)
      let ?mx = "x - {Max x}"
      let ?my = "y - {Max y}"
      show "(f p < f q) ⟷ ((p, q) ∈ ?R)"
      proof
        assume "f p < f q"
        then
        consider "ordermap (A`ℐ) ?R (A (x - {Max x})) < ordermap (A`ℐ) ?R (A (y - {Max y}))"
          | "ordermap (A`ℐ) ?R (A (x - {Max x})) = ordermap (A`ℐ) ?R (A (y - {Max y}))"
            "ordermap (B`J (x - {Max x})) ?R (B (Max x)) < ordermap (B`J (y - {Max y})) ?R (B (Max y))"
          using x y mx my
          by (auto dest: mult_cancellation_less simp: f_def split_def peq qeq oB)
        then have "(A ?mx @ B (Max x), A ?my @ B (Max y)) ∈ ?R"
        proof cases
          case 1
          then have "(A ?mx, A ?my) ∈ ?R"
            using x y by (force simp: Ord_mem_iff_lt intro: converse_ordermap_mono)
          then show ?thesis
            using x y mx my lenB lenlex_append1 by blast
        next
          case 2
          then have "A ?mx = A ?my"
            using ‹?my ∈ ℐ› ‹?mx ∈ ℐ› by auto
          then have eq: "?mx = ?my"
            by (metis ‹?my ∈ ℐ› ‹?mx ∈ ℐ› inv_into_IA)
          then have "(B (Max x), B (Max y)) ∈ ?R"
            using mx my 2 by (force simp: Ord_mem_iff_lt intro: converse_ordermap_mono)
          with 2 show ?thesis
            by (simp add: eq irrefl_less_than)
        qed
        then show "(p,q) ∈ ?R"
          by (simp add: peq qeq f_def split_def sorted_list_of_set_Un AB)
      next
        assume pqR: "(p,q) ∈ ?R"
        then have §: "(A ?mx @ B (Max x), A ?my @ B (Max y)) ∈ ?R"
          using peq qeq by blast
        then consider "(A ?mx, A ?my) ∈ ?R" | "A ?mx = A ?my ∧ (B (Max x), B (Max y)) ∈ ?R"
        proof (cases "(A ?mx, A ?my) ∈ ?R")
          case False
          have False if "(A ?my, A ?mx) ∈ ?R"
            by (metis ‹?my ∈ ℐ› ‹?mx ∈ ℐ› "§" ‹(Max y) ∈ J ?my› ‹(Max x) ∈ J ?mx› lenB lenlex_append1 omega_sum_1_less order.asym that)
          then have "A ?mx = A ?my"
            by (meson False UNIV_I total_llt total_on_def)
          then show ?thesis
            using "§" irrefl_less_than that by auto
        qed (use that in blast)
        then have "β * ordermap (A`ℐ) ?R (A ?mx) + ordermap (B`J ?mx) ?R (B (Max x))
                 < β * ordermap (A`ℐ) ?R (A ?my) + ordermap (B`J ?my) ?R (B (Max y))"
        proof cases
          case 1
          show ?thesis
          proof (rule add_mult_less_add_mult)
            show "ordermap (A`ℐ) (lenlex less_than) (A ?mx) < ordermap (A`ℐ) (lenlex less_than) (A ?my)"
              by (simp add: "1" ‹?my ∈ ℐ› ‹?mx ∈ ℐ› ordermap_mono_less)
            show "Ord (ordertype (A`ℐ) ?R)"
              using wf_Ord_ordertype by blast
            show "ordermap (B ` J ?mx) ?R (B (Max x)) ∈ elts β"
              using Ord_less_TC_mem ‹Ord β› ‹?mx ∈ ℐ› ‹(Max x) ∈ J ?mx› oB by blast
            show "ordermap (B ` J ?my) ?R (B (Max y)) ∈ elts β"
              using Ord_less_TC_mem ‹Ord β› ‹?my ∈ ℐ› ‹(Max y) ∈ J ?my› oB by blast
          qed (use ‹?my ∈ ℐ› ‹?mx ∈ ℐ› ‹Ord β› in auto)
        next
          case 2
          with ‹?mx ∈ ℐ› show ?thesis
            using ‹(Max y) ∈ J ?my› ‹(Max x) ∈ J ?mx› ordermap_mono_less
            by (metis (no_types, opaque_lifting) Kirby.add_less_cancel_left TC_small image_iff inv_into_IA trans_llt wf_llt y)
        qed
        then show "f p < f q"
          using ‹?my ∈ ℐ› ‹?mx ∈ ℐ› ‹(Max y) ∈ J ?my› ‹(Max x) ∈ J ?mx›
          by (auto simp: peq qeq f_def split_def AB)
      qed
    qed
  qed auto
qed auto


subsubsection ‹The final part of 3.8, where two sequences are merged›

inductive merge :: "[nat list list,nat list list,nat list list,nat list list] ⇒ bool"
  where NullNull: "merge [] [] [] []"
      | Null: "as ≠ [] ⟹ merge as [] [concat as] []"
      | App: "⟦as1 ≠ []; bs1 ≠ [];
               concat as1 < concat bs1; concat bs1 < concat as2; merge as2 bs2 as bs⟧
              ⟹ merge (as1@as2) (bs1@bs2) (concat as1 # as) (concat bs1 # bs)"

inductive_simps Null1 [simp]: "merge [] bs us vs"
inductive_simps Null2 [simp]: "merge as [] us vs"

lemma merge_single:
  "⟦concat as < concat bs; concat as ≠ []; concat bs ≠ []⟧ ⟹ merge as bs [concat as] [concat bs]"
  using merge.App [of as bs "[]" "[]"]
  by (fastforce simp: less_list_def)

lemma merge_length1_nonempty:
  assumes "merge as bs us vs" "as ∈ lists (- {[]})"
  shows "us ∈ lists (- {[]})"
  using assms by induction (auto simp: mem_lists_non_Nil)

lemma merge_length2_nonempty:
  assumes "merge as bs us vs" "bs ∈ lists (- {[]})"
  shows "vs ∈ lists (- {[]})"
  using assms by induction (auto simp: mem_lists_non_Nil)

lemma merge_length1_gt_0:
  assumes "merge as bs us vs" "as ≠ []"
  shows "length us > 0"
  using assms by induction auto

lemma merge_length_le:
  assumes "merge as bs us vs"
  shows "length vs ≤ length us"
  using assms by induction auto

lemma merge_length_le_Suc:
  assumes "merge as bs us vs"
  shows "length us ≤ Suc (length vs)"
  using assms by induction auto

lemma merge_length_less2:
  assumes "merge as bs us vs"
  shows "length vs ≤ length as"
  using assms
proof induction
case (App as1 bs1 as2 bs2 as bs)
  then show ?case
    using length_greater_0_conv [of as1] by (simp, presburger)
qed auto

lemma merge_preserves:
  assumes "merge as bs us vs"
  shows "concat as = concat us ∧ concat bs = concat vs"
  using assms by induction auto

lemma merge_interact:
  assumes "merge as bs us vs" "strict_sorted (concat as)" "strict_sorted (concat bs)"
           "bs ∈ lists (- {[]})"
  shows "strict_sorted (interact us vs)"
  using assms
proof induction
  case (App as1 bs1 as2 bs2 as bs)
  then have bs: "concat bs1 < concat bs" "concat bs1 < concat as" 
    and nonmt: "concat bs1 ≠ []"
    using merge_preserves strict_sorted_append_iff by fastforce+
  then have "concat bs1 < interact as bs"
    unfolding less_list_def using App bs
    by (metis (no_types, lifting) Un_iff concat_append hd_in_set last_in_set merge_preserves set_interact sorted_wrt_append strict_sorted_append_iff)
  with App show ?case
    by (metis append_in_lists_conv concat_append hd_append2 interact.simps(3) less_list_def strict_sorted_append_iff nonmt)
qed auto

lemma acc_lengths_merge1:
  assumes "merge as bs us vs"
  shows "list.set (acc_lengths k us) ⊆ list.set (acc_lengths k as)"
  using assms
proof (induction arbitrary: k)
  case (App as1 bs1 as2 bs2 as bs)
  then show ?case
    apply (simp add: acc_lengths_append strict_sorted_append_iff length_concat_acc_lengths)
    by (simp add: le_supI2 length_concat)
qed (auto simp: length_concat_acc_lengths)

lemma acc_lengths_merge2:
  assumes "merge as bs us vs"
  shows "list.set (acc_lengths k vs) ⊆ list.set (acc_lengths k bs)"
  using assms
proof (induction arbitrary: k)
  case (App as1 bs1 as2 bs2 as bs)
  then show ?case
    apply (simp add: acc_lengths_append strict_sorted_append_iff length_concat_acc_lengths)
    by (simp add: le_supI2 length_concat)
qed (auto simp: length_concat_acc_lengths)

lemma length_hd_le_concat:
  assumes "as ≠ []" shows "length (hd as) ≤ length (concat as)"
  by (metis (no_types) add.commute assms concat.simps(2) le_add2 length_append list.exhaust_sel)

lemma length_hd_merge2:
  assumes "merge as bs us vs"
  shows "length (hd bs) ≤ length (hd vs)"
  using assms by induction (auto simp: length_hd_le_concat)

lemma merge_less_sets_hd:
  assumes "merge as bs us vs" "strict_sorted (concat as)" "strict_sorted (concat bs)" "bs ∈ lists (- {[]})"
  shows "list.set (hd us) ≪ list.set (concat vs)"
  using assms
proof induction
  case (App as1 bs1 as2 bs2 as bs)
  then have §: "list.set (concat bs1) ≪ list.set (concat bs2)"
    by (force simp: dest: strict_sorted_imp_less_sets)
  have *: "list.set (concat as1) ≪ list.set (concat bs1)"
    using App by (metis concat_append strict_sorted_append_iff strict_sorted_imp_less_sets)
  then have "list.set (concat as1) ≪ list.set (concat bs)"
    using App § less_sets_trans merge_preserves
    by (metis List.set_empty append_in_lists_conv le_zero_eq length_0_conv length_concat_ge)
  with * App.hyps show ?case
    by (fastforce simp: less_sets_UN1 less_sets_UN2 less_sets_Un2)
qed auto


lemma set_takeWhile:
  assumes "strict_sorted (concat as)" "as ∈ lists (- {[]})"
  shows "list.set (takeWhile (λx. x < y) as) = {x ∈ list.set as. x < y}"
  using assms
proof (induction as)
  case (Cons a as)
  have "a < y"
    if a: "a < concat as" "strict_sorted a" "strict_sorted (concat as)" "x < y" "x ≠ []" "x ∈ list.set as"
    for x
  proof -
    have §: "last x ∈ list.set (concat as)"
      using set_concat that by fastforce
    have "last a < hd (concat as)"
      using Cons.prems that by (auto simp: less_list_def)
    also have "… ≤ hd y" if "y ≠ []"
      using that a
      by (meson § order.strict_trans less_list_def not_le sorted_hd_le strict_sorted_imp_sorted)
    finally show ?thesis
      by (simp add: less_list_def)
  qed
  then show ?case
    using Cons by (auto simp: strict_sorted_append_iff)
qed auto

proposition merge_exists:
  assumes "strict_sorted (concat as)" "strict_sorted (concat bs)"
          "as ∈ lists (- {[]})" "bs ∈ lists (- {[]})"
          "hd as < hd bs" "as ≠ []" "bs ≠ []"
  and disj: "⋀a b. ⟦a ∈ list.set as; b ∈ list.set bs⟧ ⟹ a<b ∨ b<a"
shows "∃us vs. merge as bs us vs"
  using assms
proof (induction "length as + length bs" arbitrary: as bs rule: less_induct)
  case (less as bs)
  obtain as1 as2 bs1 bs2
    where A: "as1 ≠ []" "bs1 ≠ []" "concat as1 < concat bs1" "concat bs1 < concat as2"
      and B: "as = as1@as2" "bs = bs1@bs2" and C: "bs2 = [] ∨ (as2 ≠ [] ∧ hd as2 < hd bs2)"
  proof
    define as1 where "as1 ≡ takeWhile (λx. x < hd bs) as"
    define as2 where "as2 ≡ dropWhile (λx. x < hd bs) as"
    define bs1 where "bs1 ≡ if as2=[] then bs else takeWhile (λx. x < hd as2) bs"
    define bs2 where "bs2 ≡ if as2=[] then [] else dropWhile (λx. x < hd as2) bs"

    have as1: "as1 = takeWhile (λx. last x < hd (hd bs)) as"
      using less.prems by (auto simp: as1_def less_list_def cong: takeWhile_cong)
    have as2: "as2 = dropWhile (λx. last x < hd (hd bs)) as"
      using less.prems by (auto simp: as2_def less_list_def cong: dropWhile_cong)

    have hd_as2: "as2 ≠ [] ⟹ ¬ hd as2 < hd bs"
      using as2_def hd_dropWhile by metis
    have hd_bs2: "bs2 ≠ [] ⟹ ¬ hd bs2 < hd as2"
      using bs2_def hd_dropWhile by metis
    show "as1 ≠ []"
      by (simp add: as1_def less.prems takeWhile_eq_Nil_iff)
    show "bs1 ≠ []"
      by (metis as2 bs1_def hd_as2 hd_in_set less.prems(7) less.prems(8) set_dropWhileD takeWhile_eq_Nil_iff)
    show "bs2 = [] ∨ (as2 ≠ [] ∧ hd as2 < hd bs2)"
      by (metis as2_def bs2_def hd_bs2 less.prems(8) list.set_sel(1) set_dropWhileD)
    have AB: "list.set A ≪ list.set B"
      if "A ∈ list.set as1" "B ∈ list.set bs" for A B
    proof -
      have "A ∈ list.set as"
        using that by (metis as1 set_takeWhileD)
      then have "sorted A"
        by (metis concat.simps(2) concat_append less.prems(1) sorted_append split_list_last strict_sorted_imp_sorted)
      moreover have "sorted (hd bs)"
        by (metis concat.simps(2) hd_Cons_tl less.prems(2) less.prems(7) strict_sorted_append_iff strict_sorted_imp_sorted)
      ultimately show ?thesis
        using that less.prems
       apply (clarsimp simp add: as1_def set_takeWhile less_list_iff_less_sets less_sets_def)
        by (metis (full_types) UN_I hd_concat less_le_trans list.set_sel(1) set_concat sorted_hd_le strict_sorted_imp_sorted)
    qed
    show "as = as1@as2"
      by (simp add: as1_def as2_def)
    show "bs = bs1@bs2"
      by (simp add: bs1_def bs2_def)
    have "list.set (concat as1) ≪ list.set (concat bs1)"
      using AB set_takeWhileD by (fastforce simp: as1_def bs1_def less_sets_UN1 less_sets_UN2)
    then show "concat as1 < concat bs1"
      by (rule less_sets_imp_list_less)
    have "list.set (concat bs1) ≪ list.set (concat as2)" if "as2 ≠ []"
    proof (clarsimp simp add: bs1_def less_sets_UN1 less_sets_UN2 set_takeWhile less.prems)
      fix A B
      assume "A ∈ list.set as2" "B ∈ list.set bs" "B < hd as2"
      with that show "list.set B ≪ list.set A"
        using hd_as2 less.prems(1,2)
        apply (clarsimp simp add: less_sets_def less_list_def)
        apply (auto simp: as2_def)
        apply (simp flip: as2_def)
        by (smt (verit, ccfv_SIG) UN_I ‹as = as1 @ as2› concat.simps(2) concat_append hd_concat in_set_conv_decomp_first le_less_trans less_le_trans set_concat sorted_append sorted_hd_le sorted_le_last strict_sorted_imp_sorted that)
    qed
    then show "concat bs1 < concat as2"
      by (simp add: bs1_def less_sets_imp_list_less)
  qed
  obtain cs ds where "merge as2 bs2 cs ds"
  proof (cases "as2 = [] ∨ bs2 = []")
    case True
    then show thesis
      using that C NullNull Null by metis
  next
    have †: "length as2 + length bs2 < length as + length bs"
      by (simp add: A B)
    case False
    moreover have "strict_sorted (concat as2)" "strict_sorted (concat bs2)"
      "as2 ∈ lists (- {[]})" "bs2 ∈ lists (- {[]})"
      "⋀a b. ⟦a ∈ list.set as2; b ∈ list.set bs2⟧ ⟹ a < b ∨ b < a"
      using B less.prems strict_sorted_append_iff by auto
    ultimately show ?thesis
      using C less.hyps [OF †] False that by force
  qed
  then obtain cs where "merge (as1 @ as2) (bs1 @ bs2) (concat as1 # cs) (concat bs1 # ds)"
    using A merge.App by blast
  then show ?case
    using B by blast
qed

subsubsection ‹Actual proof of Larson's Lemma 3.8›

proposition lemma_3_8:
  assumes "infinite N"
  obtains X where "X ⊆ WW" "ordertype X (lenlex less_than) = ω↑ω"
            "⋀u. u ∈ [X]⇗2⇖ ⟹
                   ∃l. Form l u ∧ (l > 0 ⟶ [enum N l] < inter_scheme l u ∧ List.set (inter_scheme l u) ⊆ N)"
proof -
  let ?LL = "lenlex less_than"
  define bf where "bf ≡ λM q. wfrec pair_less (λf (j,i).
                                  let R = (case prev j i of None ⇒ M | Some u ⇒ snd (f u))
                                  in grab R (q j i))"

  have bf_rec: "bf M q (j,i) =
                 (let R = (case prev j i of None ⇒ M | Some u ⇒ snd (bf M q u))
                  in  grab R (q j i))" for M q j i
    by (subst (1) bf_def) (simp add: Let_def wfrec bf_def cut_apply prev_pair_less cong: conj_cong split: option.split)

  have "infinite (snd (bf M q u)) = infinite M ∧ fst (bf M q u) ⊆ M ∧ snd (bf M q u) ⊆ M" for M q u
    using wf_pair_less
  proof (induction u rule: wf_induct_rule)
    case (less u)
    then show ?case
    proof (cases u)
      case (Pair j i)
      with less.IH prev_pair_less show ?thesis
        apply (simp add: bf_rec [of M q j i] split: option.split)
        using fst_grab_subset snd_grab_subset by blast
    qed
  qed
  then have infinite_bf [simp]: "infinite (snd (bf M q u)) = infinite M"
       and  bf_subset: "fst (bf M q u) ⊆ M ∧ snd (bf M q u) ⊆ M" for M q u
    by auto

  have bf_less_sets: "fst (bf M q ij) ≪ snd (bf M q ij)" if "infinite M" for M q ij
    using wf_pair_less
  proof (induction ij rule: wf_induct_rule)
    case (less u)
    then show ?case
      by (metis bf_rec finite_grab_iff infinite_bf less_sets_grab prod.exhaust_sel that)
  qed

  have card_fst_bf: "finite (fst (bf M q (j,i))) ∧ card (fst (bf M q (j,i))) = q j i" if "infinite M" for M q j i
    by (simp add: that bf_rec [of M q j i] split: option.split)

  have bf_cong: "bf M q u = bf M q' u"
    if "snd u ≤ fst u" and eq: "⋀y x. ⟦x≤y; y≤fst u⟧ ⟹ q' y x = q y x" for M q q' u
    using wf_pair_less that
  proof (induction u rule: wf_induct_rule)
    case (less u)
    show ?case
    proof (cases u)
      case (Pair j i)
      with less.prems show ?thesis
      proof (clarsimp simp add: bf_rec [of M _ j i] split: option.split)
        fix j' i'
        assume *: "prev j i = Some (j',i')"
        then have **: "((j', i'), u) ∈ pair_less"
          by (simp add: Pair prev_pair_less)
        moreover have "i' < j'"
          using Pair less.prems by (simp add: prev_Some_less [OF *])
        moreover have "⋀x y. ⟦x ≤ y; y ≤ j'⟧ ⟹ q' y x = q y x"
          using ** less.prems by (auto simp: pair_less_def Pair)
        ultimately show "grab (snd (bf M q (j',i'))) (q j i) = grab (snd (bf M q' (j',i'))) (q j i)"
          using less.IH by auto
      qed
    qed
  qed

  define ediff where "ediff ≡ λD:: nat ⇒ nat set. λj i. enum (D j) (Suc i) - enum (D j) i"
  define F where "F ≡ λl (dl,a0::nat set,b0::nat × nat ⇒ nat set,M).
          let (d,Md) = grab (nxt M (enum N (Suc (2 * Suc l)))) (Suc l) in
          let (a,Ma) = grab Md (Min d) in
          let Gb = bf Ma (ediff (dl(l := d))) in
          let dl' = dl(l := d) in
          (dl', a, fst ∘ Gb, snd (Gb(l, l-1)))"
  define DF where "DF ≡ rec_nat (λi∈{..<0}. {}, {}, λp. {}, N) F"
  have DF_simps: "DF 0 = (λi∈{..<0}. {}, {}, λp. {}, N)"
                 "DF (Suc l) = F l (DF l)" for l
    by (auto simp: DF_def)
  note cut_apply [simp]

  have inf [rule_format]: "∀dl al bl L. DF l = (dl,al,bl,L) ⟶ infinite L" for l
    by (induction l) (auto simp: DF_simps F_def Let_def grab_eqD infinite_nxtN assms split: prod.split)

  define Ψ where
    "Ψ ≡ λ(dl, a, b, M). λl::nat.
           dl l ≪ a ∧ card a > 0 ∧
           (∀j≤l. card (dl j) = Suc j) ∧ a ≪ ⋃(range b) ∧ range b ⊆ Collect finite ∧
           a ⊆ N ∧ ⋃(range b) ⊆ N ∧ infinite M ∧ b(l,l-1) ≪ M ∧ M ⊆ N"
  have Ψ_DF: "Ψ (DF (Suc l)) l" for l
  proof (induction l)
    case 0
    show ?case
      using assms
      apply (clarsimp simp add: bf_rec F_def DF_simps Ψ_def split: prod.split)
      apply (drule grab_eqD, blast dest: grab_eqD infinite_nxtN)+
      apply (auto simp: less_sets_UN2 less_sets_grab card_fst_bf elim!: less_sets_weaken2)
      apply (metis card_1_singleton_iff Min_singleton greaterThan_iff insertI1 le0 nxt_subset_greaterThan subsetD)
      using nxt_subset snd_grab_subset bf_subset by blast+
  next
    case (Suc l)
    then show ?case
      using assms
      unfolding Let_def DF_simps(2)[of "Suc l"] F_def Ψ_def
      apply (clarsimp simp add: bf_rec DF_simps split: prod.split)
      apply (drule grab_eqD, metis grab_eqD infinite_nxtN)+
      apply (safe, simp_all add: less_sets_UN2 less_sets_grab card_fst_bf card_Suc_eq_finite)
             apply (meson less_sets_weaken2)
            apply (metis Min_in gr0I greaterThan_iff insert_not_empty le_inf_iff less_asym nxt_def subsetD)
           apply (meson bf_subset less_sets_weaken2)
          apply (meson nxt_subset subset_eq)
         apply (meson bf_subset nxt_subset subset_eq)
        using bf_rec infinite_bf apply force
       using bf_less_sets bf_rec apply force
      by (metis bf_rec bf_subset nxt_subset subsetD)
  qed

  define d where "d ≡ λk. let (dk,ak,bk,M) = DF(Suc k) in dk k"
  define a where "a ≡ λk. let (dk,ak,bk,M) = DF(Suc k) in ak"
  define b where "b ≡ λk. let (dk,ak,bk,M) = DF(Suc k) in bk"
  define M where "M ≡ λk. let (dk,ak,bk,M) = DF k in M"

  have infinite_M [simp]: "infinite (M k)" for k
    by (auto simp: M_def inf split: prod.split)

  have M_Suc_subset: "M (Suc k) ⊆ M k" for k
    apply (clarsimp simp add: Let_def M_def F_def DF_simps split: prod.split)
    by (metis bf_subset in_mono nxt_subset snd_conv snd_grab_subset)

  have Inf_M_Suc_ge: "Inf (M k) ≤ Inf (M (Suc k))" for k
    by (simp add: M_Suc_subset cInf_superset_mono infinite_imp_nonempty)

  have Inf_M_telescoping: "{Inf (M k)..} ⊆ {Inf (M k')..}" if k': "k'≤k" for k k'
    using that Inf_nat_def1 infinite_M unfolding Inf_nat_def atLeast_subset_iff
    by (metis M_Suc_subset finite.emptyI le_less_linear lift_Suc_antimono_le not_less_Least subsetD)

  have d_eq: "d k = fst (grab (nxt (M k) (enum N (Suc (2 * Suc k)))) (Suc k))" for k
    by (simp add: d_def M_def Let_def DF_simps F_def split: prod.split)
  then have finite_d [simp]: "finite (d k)" for k
    by simp
  then have d_ne [simp]: "d k ≠ {}" for k
    by (metis card.empty card_grab d_eq infinite_M infinite_nxtN nat.distinct(1))
  have a_eq: "∃M. a k = fst (grab M (Min (d k))) ∧ infinite M" for k
    apply (simp add: a_def d_def M_def Let_def DF_simps F_def split: prod.split)
    by (metis fst_conv grab_eqD infinite_nxtN local.inf)
  then have card_a: "card (a k) = Inf (d k)" for k
    by (metis cInf_eq_Min card_grab d_ne finite_d)

  have d_eq_dl: "d k = dl k" if "(dl,a,b,P) = DF l" "k < l" for k l dl a b P
    using that
    by (induction l arbitrary: dl a b P) (simp_all add: d_def DF_simps F_def Let_def split: prod.split_asm prod.split)

  have card_d [simp]: "card (d k) = Suc k" for k
    by (auto simp: d_eq infinite_nxtN)

  have d_ne [simp]: "d j ≠ {}" and a_ne [simp]: "a j ≠ {}"
    and finite_d [simp]: "finite (d j)" and finite_a [simp]: "finite (a j)" for j
    using Ψ_DF [of "j"]  by (auto simp: Ψ_def a_def d_def card_gt_0_iff split: prod.split_asm)

  have da: "d k ≪ a k" for k
    using Ψ_DF [of "k"] by (simp add: Ψ_def a_def d_def split: prod.split_asm)

  have ab_same: "a k ≪ ⋃(range(b k))" for k
    using Ψ_DF [of "k"] by (simp add: Ψ_def a_def b_def M_def split: prod.split_asm)

  have snd_bf_subset: "snd (bf M r (j,i)) ⊆ snd (bf M r (j',i'))"
    if ji: "((j',i'), (j,i)) ∈ pair_less" "(j',i') ∈ IJ k"
    for M r k j i j' i'
    using wf_pair_less ji
  proof (induction rule: wf_induct_rule [where a= "(j,i)"])
    case (less u)
    show ?case
    proof (cases u)
      case (Pair j i)
      then consider "prev j i = Some (j', i')" | x where "((j', i'), x) ∈ pair_less" "prev j i = Some x"
        using less.prems pair_less_prev by blast
      then show ?thesis
      proof cases
        case 2 with less.IH show ?thesis
          unfolding bf_rec Pair
          by (metis in_mono option.simps(5) prev_pair_less snd_grab_subset subsetI that(2)) 
      qed (simp add: Pair bf_rec snd_grab_subset)
    qed
  qed

  have less_bf: "fst (bf M r (j',i')) ≪ fst (bf M r (j,i))"
    if ji: "((j',i'), (j,i)) ∈ pair_less" "(j',i') ∈ IJ k" and "infinite M"
    for M r k j i j' i'
  proof -
    consider "prev j i = Some (j', i')" | j'' i'' where "((j', i'), (j'',i'')) ∈ pair_less" "prev j i = Some (j'',i'')"
      by (metis pair_less_prev ji prod.exhaust_sel)
    then show ?thesis
    proof cases
      case 1
      then show ?thesis
        using bf_less_sets bf_rec less_sets_fst_grab ‹infinite M› by force
    next
      case 2
      then have "fst (bf M r (j',i')) ≪ snd (bf M r (j'',i''))"
        by (meson bf_less_sets snd_bf_subset less_sets_weaken2 that)
      with 2 show ?thesis
        using bf_rec bf_subset less_sets_fst_grab ‹infinite M› by auto
    qed
  qed

  have aM: "a k ≪ M (Suc k)" for k
    apply (clarsimp simp add: a_def M_def DF_simps F_def Let_def split: prod.split)
    by (meson bf_subset grab_eqD infinite_nxtN less_sets_weaken2 local.inf)
  then have "a k ≪ a (Suc k)" for k
    by (metis IntE card_d card.empty d_eq da fst_grab_subset less_sets_trans less_sets_weaken2 nat.distinct(1) nxt_def subsetI)
  then have aa: "a j ≪ a k" if "j<k" for k j
    by (meson UNIV_I a_ne less_sets_imp_strict_mono_sets strict_mono_sets_def that)
  then have ab: "a k' ≪ b k (j,i)" if "k'≤k" for k k' j i
    by (metis a_ne ab_same le_less less_sets_UN2 less_sets_trans rangeI that)
  have db: "d j ≪ b k (j,i)" if "j≤k" for k j i
    by (meson a_ne ab da less_sets_trans that)

  have bMkk: "b k (k,k-1) ≪ M (Suc k)" for k
    using Ψ_DF [of k]
    by (simp add: Ψ_def b_def d_def M_def split: prod.split_asm)

  have b: "∃P ⊆ M k. infinite P ∧ (∀j i. i≤j ⟶ j≤k ⟶ b k (j,i) = fst (bf P (ediff d) (j,i)))" for k
  proof (clarsimp simp: b_def DF_simps F_def Let_def split: prod.split)
    fix a a' d' dl bb P M' M''
    assume gr: "grab M'' (Min d') = (a', M')" "grab (nxt P (enum N (Suc (Suc (Suc (2 * k)))))) (Suc k) = (d', M'')"
      and DF: "DF k = (dl, a, bb, P)"
    have deq: "d j = (if j = k then d' else dl j)" if "j≤k" for j
    proof (cases "j < k")
      case True
      then show ?thesis by (metis DF d_eq_dl less_not_refl)
    next
      case False
      then show ?thesis
        using that DF gr by (auto simp: d_def DF_simps F_def Let_def split: prod.split)
    qed
    have "M' ⊆ P"
      by (metis gr in_mono nxt_subset snd_conv snd_grab_subset subsetI)
    also have "P ⊆ M k"
      using DF by (simp add: M_def)
    finally have "M' ⊆ M k" .
    moreover have "infinite M'"
      using DF by (metis (mono_tags) finite_grab_iff gr infinite_nxtN local.inf snd_conv)
    moreover
    have "ediff (dl(k := d')) j i = ediff d j i" if "j≤k" for j i
      by (simp add: deq that ediff_def)
    then have "bf M' (ediff (dl(k := d'))) (j,i)
             = bf M' (ediff d) (j,i)" if "i ≤ j" "j≤k" for j i
      using bf_cong that by fastforce
    ultimately show "∃P⊆M k. infinite P ∧
                           (∀j i. i ≤ j ⟶ j ≤ k
                                        ⟶ fst (bf M' (ediff (dl(k := d'))) (j,i))
                         = fst (bf P (ediff d) (j,i)))"
      by auto
  qed

  have card_b: "card (b k (j,i)) = enum (d j) (Suc i) - enum (d j) i" if "j≤k" for k j i
    ―‹there's a short proof of this from the previous result but it would need @{term"i≤j"}›
  proof (clarsimp simp: b_def DF_simps F_def Let_def split: prod.split)
    fix dl
      and a a' d':: "nat set"
      and bb M M' M''
    assume gr: "grab M'' (Min d') = (a', M')" "grab (nxt M (enum N (Suc (Suc (Suc (2 * k)))))) (Suc k) = (d',M'')"
      and DF: "DF k = (dl, a, bb, M)"
    have "d j = (if j = k then d' else dl j)"
    proof (cases "j < k")
      case True
      then show ?thesis by (metis DF d_eq_dl less_not_refl)
    next
      case False
      then show ?thesis
        using that DF gr by (auto simp: d_def DF_simps F_def Let_def split: prod.split)
    qed
    then show "card (fst (bf M' (ediff (dl(k := d'))) (j,i)))
             = enum (d j) (Suc i) - enum (d j) i"
      using DF gr card_fst_bf grab_eqD infinite_nxtN local.inf ediff_def by auto
  qed

  have card_b_pos: "card (b k (j,i)) > 0" if "i < j" "j≤k" for k j i
    by (simp add: card_b that finite_enumerate_step)
  have b_ne [simp]: "b k (j,i) ≠ {}" if "i < j" "j≤k" for k j i
    using card_b_pos [OF that] less_imp_neq by fastforce+

  have card_b_finite [simp]: "finite (b k u)" for k u
    using Ψ_DF [of k] by (fastforce simp: Ψ_def b_def)

  have bM: "b k (j,i) ≪ M (Suc k)" if "i<j" "j≤k" for i j k
  proof -
    obtain M' where "M' ⊆ M k" "infinite M'"
      and bk: "⋀j i. i≤j ⟹ j≤k ⟹ b k (j,i) = fst (bf M' (ediff d) (j,i))"
      using b by (metis (no_types, lifting))
    show ?thesis
    proof (cases "j=k ∧ i = k-1")
      case False
      show ?thesis
      proof (rule less_sets_trans [OF _ bMkk])
        show "b k (j,i) ≪ b k (k, k-1)"
          using that ‹infinite M'› False
            by (force simp: bk pair_less_def IJ_def intro: less_bf)
        show "b k (k, k-1) ≠ {}"
          using b_ne that by auto
      qed
    qed (use bMkk in auto)
  qed

  have b_InfM: "⋃ (range (b k)) ⊆ {⨅(M k)..}" for k
  proof (clarsimp simp add: Ψ_def b_def M_def DF_simps F_def Let_def split: prod.split)
    fix r dl :: "nat ⇒ nat set"
      and a b and d' a' M'' M' P and x j' i' :: nat
    assume gr: "grab M'' (Min d') = (a', M')"
               "grab (nxt P (enum N (Suc (Suc (Suc (2 * k)))))) (Suc k) = (d', M'')"
      and DF: "DF k = (dl, a, b, P)"
      and x: "x ∈ fst (bf M' (ediff (dl(k := d'))) (j', i'))"
    have "infinite P"
      using DF local.inf by blast
    then have "M' ⊆ P"
      by (meson gr grab_eqD infinite_nxtN nxt_subset order.trans)
    with bf_subset show "⨅ P ≤ x"
      using Inf_nat_def x le_less_linear not_less_Least by fastforce
  qed

  have b_Inf_M_Suc: "b k (j,i) ≪ {Inf(M (Suc k))}" if "i<j" "j≤k" for k j i
    using bMkk [of k] that
    by (metis Inf_nat_def1 bM finite.emptyI infinite_M less_setsD less_sets_singleton2)

  have bb_same: "b k (j',i') ≪ b k (j,i)"
    if "((j',i'), (j,i)) ∈ pair_less" "(j',i') ∈ IJ k" for k j i j' i'
    using that
    unfolding b_def DF_simps F_def Let_def
    by (auto simp: less_bf grab_eqD infinite_nxtN local.inf split: prod.split)

  have bb: "b k' (j',i') ≪ b k (j,i)"
    if j: "i' < j'" "j'≤k'" and k: "k'<k" for i i' j j' k' k
  proof (rule atLeast_less_sets)
    show "b k' (j', i') ≪ {Inf(M (Suc k'))}"
      using Suc_lessD b_Inf_M_Suc nat_less_le j by blast
    show "b k (j,i) ⊆ {Inf(M (Suc k'))..}"
      by (meson Inf_M_telescoping Suc_leI UnionI b_InfM rangeI subset_eq k)
  qed

  have M_subset_N: "M k ⊆ N" for k
  proof (cases k)
    case (Suc k')
    with Ψ_DF [of k'] show ?thesis
      by (auto simp: M_def Let_def Ψ_def split: prod.split)
  qed (auto simp: M_def DF_simps)
  have a_subset_N: "a k ⊆ N" for k
    using Ψ_DF [of k] by (simp add: a_def Ψ_def split: prod.split prod.split_asm)
  have d_subset_N: "d k ⊆ N" for k
    using M_subset_N [of k] d_eq fst_grab_subset nxt_subset by blast
  have b_subset_N: "b k (j,i) ⊆ N" for k j i
    using Ψ_DF [of k] by (force simp: b_def Ψ_def)

  define 𝒦:: "[nat,nat] ⇒ nat set set"
    where "𝒦 ≡ λj0 j. nsets {j0<..} j"
  have 𝒦_finite: "finite K" and 𝒦_card: "card K = j" if "K ∈ 𝒦 j0 j" for K j0 j
    using that by (auto simp add: 𝒦_def nsets_def)
  have 𝒦_enum: "j0 < enum K i" if "K ∈ 𝒦 j0 j" "i < card K" for K j0 j i
    using that by (auto simp: 𝒦_def nsets_def finite_enumerate_in_set subset_eq)
  have 𝒦_0 [simp]: "𝒦 k 0 = {{}}" for k
    by (auto simp: 𝒦_def)

  have 𝒦_Suc: "𝒦 j0 (Suc j) = USigma (𝒦 j0 j) (λK. {Max (insert j0 K)<..})" (is "?lhs = ?rhs")
    for j j0
  proof
    show "𝒦 j0 (Suc j) ⊆ USigma (𝒦 j0 j) (λK. {Max (insert j0 K)<..})"
      unfolding 𝒦_def nsets_def USigma_def
    proof clarsimp
      fix K
      assume K: "K ⊆ {j0<..}" "finite K" "card K = Suc j"
      then have "Max K ∈ K"
        by (metis Max_in card_0_eq nat.distinct(1))
      then obtain i where "Max (insert j0 (K - {Max K})) < i" "K = insert i (K - {Max K})"
        using K 
        by (simp add: subset_iff) (metis DiffE Max.coboundedI insertCI insert_Diff le_neq_implies_less)
      then show "∃L⊆{j0<..}. finite L ∧ card L = j ∧ (∃i∈{Max (insert j0 L)<..}. K = insert i L)"
        using K
        by (metis ‹Max K ∈ K› card_Diff_singleton_if diff_Suc_1 finite_Diff greaterThan_iff insert_subset)
    qed
    show "?rhs ⊆ 𝒦 j0 (Suc j)"
      by (force simp:  𝒦_def nsets_def USigma_def)
  qed

  define BB where "BB ≡ λj0 j K. list_of (a j0 ∪ (⋃i<j. b (enum K i) (j0,i)))"
  define XX where "XX ≡ λj. BB j j ` 𝒦 j j"

  have less_list_of:  "BB j i K < list_of (b l (j,i))"
    if K: "K ∈ 𝒦 j i" "∀j∈K. j < l" and "i ≤ j" "j ≤ l" for j i K l
    unfolding BB_def
  proof (rule less_sets_imp_sorted_list_of_set)
    have "⋀i. i < card K ⟹ b (enum K i) (j,i) ≪ b l (j, card K)"
      using that by (metis 𝒦_card 𝒦_enum 𝒦_finite bb finite_enumerate_in_set nat_less_le less_le_trans)
    then show "a j ∪ (⋃i<i. b (enum K i) (j,i)) ≪ b l (j,i)"
      using that unfolding 𝒦_def nsets_def
      by (auto simp: less_sets_Un1 less_sets_UN1 ab finite_enumerate_in_set subset_eq)
  qed auto
  have BB_Suc: "BB j0 (Suc j) K = usplit (λL k. BB j0 j L @ list_of (b k (j0, j))) K"
    if j: "j ≤ j0" and K: "K ∈ 𝒦 j0 (Suc j)" for j0 j K
    ―‹towards the ordertype proof›
  proof -
    have Kj: "K ⊆ {j0<..}" and [simp]: "finite K" and cardK: "card K = Suc j"
      using K by (auto simp: 𝒦_def nsets_def)
    have KMK: "K - {Max K} ∈ 𝒦 j0 j"
      using that by (simp add: 𝒦_Suc USigma_iff 𝒦_finite less_sets_def usplit_def)
    have "j0 < Max K"
      by (metis Kj Max_in cardK card_gt_0_iff greaterThan_iff subsetD zero_less_Suc)
    have MaxK: "Max K = enum K j"
    proof (rule Max_eqI)
      fix k
      assume "k ∈ K" 
      with K cardK show "k ≤ enum K j" 
        by (metis ‹finite K› finite_enumerate_Ex finite_enumerate_mono_iff leI lessI not_less_eq)
    qed (auto simp: cardK finite_enumerate_in_set)
    have ene: "i<j ⟹ enum (K - {enum K j}) i = enum K i" for i
      using finite_enumerate_Diff_singleton [OF ‹finite K›] by (simp add: cardK)
    have "BB j0 (Suc j) K = list_of ((a j0 ∪ (⋃x<j. b (enum K x) (j0, x))) ∪ b (enum K j) (j0, j))"
      by (simp add: BB_def lessThan_Suc Un_ac)
    also have "… = list_of ((a j0 ∪ (⋃i<j. b (enum K i) (j0, i)))) @ list_of (b (enum K j) (j0, j))"
    proof (rule sorted_list_of_set_Un)
      have "b (enum K i) (j0, i) ≪ b (enum K j) (j0, j)" if "i<j" for i
        using K 𝒦_enum bb cardK j le_eq_less_or_eq that by auto
      moreover have "a j0 ≪ b (enum K j) (j0, j)"
        using MaxK ‹j0 < Max K› ab by auto
      ultimately show "a j0 ∪ (⋃x<j. b (enum K x) (j0, x)) ≪ b (enum K j) (j0, j)"
        by (simp add: less_sets_Un1 less_sets_UN1)
    qed (auto simp: finite_UnI)
    also have "… = BB j0 j (K - {Max K}) @ list_of (b (Max K) (j0, j))"
      by (simp add: BB_def MaxK ene)
    also have "… = usplit (λL k. BB j0 j L @ list_of (b k (j0, j))) K"
      by (simp add: usplit_def)
    finally show ?thesis .
  qed

  have enum_d_0: "enum (d j) 0 = Inf (d j)" for j
    using enum_0_eq_Inf_finite by auto

  have Inf_b_less: "⨅(b k' (j',i')) < ⨅(b k (j,i))"
    if j: "i' < j'" "i < j" "j'≤k'" "j≤k" and k: "k'<k" for i i' j j' k' k
    using bb [of i' j' k' k j i] that b_ne [of i' j' k'] b_ne [of i j k]
    by (simp add: less_sets_def Inf_nat_def1)

  have b_ge_k: "⨅ (b k (k, k-1)) ≥ k-1" for k
  proof (induction k)
    case (Suc k)
    show ?case
    proof (cases "k=0")
      case False
      then have "⨅ (b k (k, k - 1)) < ⨅ (b (Suc k) (Suc k, k))"
        using Inf_b_less by auto
      with Suc show ?thesis
        by simp
    qed auto
  qed auto

  have b_ge: "⨅ (b k (j,i)) ≥ k-1" if "k ≥ j" "j > i" for k j i
    by (metis Inf_b_less Suc_leI b_ge_k diff_Suc_1 lessI not_less that diff_le_mono)
  have hd_b: "hd (list_of (b k (j,i))) = ⨅ (b k (j,i))"
    if "i < j" "j ≤ k" for k j i
    using that by (simp add: hd_list_of cInf_eq_Min)

  have b_disjoint_less: "b (enum K i) (j0, i) ∩ b (enum K i') (j0, i') = {}"
    if K: "K ⊆ {j0<..}" "finite K" "card K ≥ j0" "i' < j" "i < i'" "j ≤ j0" for i i' j j0 K
  proof (intro bb less_sets_imp_disjnt [unfolded disjnt_def])
    show "i < j0"
      using that by linarith
    then show "j0 ≤ enum K i"
      by (meson K finite_enumerate_in_set greaterThan_iff less_imp_le_nat less_le_trans subsetD)
    show "enum K i < enum K i'"
      using K ‹j ≤ j0› that by auto
  qed

  have b_disjoint: "b (enum K i) (j0, i) ∩ b (enum K i') (j0, i') = {}"
    if K: "K ⊆ {j0<..}" "finite K" "card K ≥ j0" "i < j" "i' < j" "i ≠ i'" "j ≤ j0" for i i' j j0 K
    using that b_disjoint_less inf_commute neq_iff by metis

  have otω: "ordertype ((λk. list_of (b k (j,i))) ` {Max (insert j K)<..}) ?LL = ω"
             (is "?lhs = _")
    if K: "K ∈ 𝒦 j i" "j > i" for j i K
  proof -
    have Sucj: "Suc (Max (insert j K)) ≥ j"
      using 𝒦_finite that(1) le_Suc_eq by auto
    let ?N = "{Inf(b k (j,i))| k. Max (insert j K) < k}"
    have infN: "infinite ?N"
    proof (clarsimp simp add: infinite_nat_iff_unbounded_le)
      fix m
      show "∃n≥m. ∃k. n = ⨅ (b k (j,i)) ∧ Max (insert j K) < k"
        using b_ge ‹j > i› Sucj
        by (metis (no_types, lifting) diff_Suc_1 le_SucI le_trans less_Suc_eq_le nat_le_linear)
    qed
    have [simp]: "Max (insert j K) < k ⟷ j < k ∧ (∀a∈K. a < k)" for k
      using that by (auto simp: 𝒦_finite)
    have "?lhs = ordertype ?N less_than"
    proof (intro ordertype_eqI strip)
      have "list_of (b k (j,i)) = list_of (b k' (j,i))"
        if "j ≤ k" "j ≤ k'"  "hd (list_of (b k (j,i))) = hd (list_of (b k' (j,i)))"
        for k k'
        by (metis Inf_b_less ‹i < j› hd_b nat_less_le not_le that)
      moreover have "∃k' j' i'. hd (list_of (b k (j,i))) = ⨅ (b k' (j', i')) ∧ i' < j' ∧ j' ≤ k'"
        if "j ≤ k" for k
        using that ‹i < j› hd_b less_imp_le_nat by blast
      moreover have "∃k'. hd (list_of (b k (j,i))) = ⨅ (b k' (j,i)) ∧ j < k' ∧ (∀a∈K. a < k')"
         if "j < k" "∀a∈K. a < k" for k
        using that K hd_b less_imp_le_nat by blast
      moreover have "⨅ (b k (j,i)) ∈ hd ` (λk. list_of (b k (j,i))) ` {Max (insert j K)<..}"
        if "j < k" "∀a∈K. a < k" for k
        using that K by (auto simp: hd_b image_iff)
      ultimately
      show "bij_betw hd ((λk. list_of (b k (j,i))) ` {Max (insert j K)<..}) {⨅ (b k (j,i)) |k. Max (insert j K) < k}"
        by (auto simp: bij_betw_def inj_on_def)
    next
      fix ms ns
      assume "ms ∈ (λk. list_of (b k (j,i))) ` {Max (insert j K)<..}"
        and "ns ∈ (λk. list_of (b k (j,i))) ` {Max (insert j K)<..}"
      with that obtain k k' where
        ms: "ms = list_of (b k (j,i))" and ns: "ns = list_of (b k' (j,i))"
        and "j < k" "j < k'" and lt_k: "∀a∈K. a < k" and lt_k': "∀a∈K. a < k'"
        by (auto simp: 𝒦_finite)
      then have len_eq [simp]: "length ns = length ms"
        by (simp add: card_b)
      have nz: "length ns ≠ 0"
        using b_ne ‹i < j› ‹j < k'› ns by auto
      show "(hd ms, hd ns) ∈ less_than ⟷ (ms, ns) ∈ ?LL"
      proof
        assume "(hd ms, hd ns) ∈ less_than"
        then show "(ms, ns) ∈ ?LL"
          using that nz
          by (fastforce simp: lenlex_def 𝒦_finite card_b intro: hd_lex)
      next
        assume §: "(ms, ns) ∈ ?LL"
        then have "(list_of (b k' (j,i)), list_of (b k (j,i))) ∉ ?LL"
          using less_asym ms ns omega_sum_1_less by blast
        then show "(hd ms, hd ns) ∈ less_than"
          using ‹j < k› ‹j < k'› Inf_b_less [of i j i j] ms ns
          by (metis Cons_lenlex_iff § len_eq b_ne card_b_finite diff_Suc_1 hd_Cons_tl hd_b length_Cons less_or_eq_imp_le less_than_iff linorder_neqE_nat sorted_list_of_set_eq_Nil_iff that(2))
      qed
    qed auto
    also have "… = ω"
      using infN ordertype_nat_ω by blast
    finally show ?thesis .
  qed

  have otωj: "ordertype (BB j0 j ` 𝒦 j0 j) ?LL = ω↑j" if "j ≤ j0" for j j0
    using that
  proof (induction j) ―‹a difficult proof, but no hints in Larson's text›
    case 0
    then show ?case
      by (auto simp: XX_def)
  next
    case (Suc j)
    then have ih: "ordertype (BB j0 j ` 𝒦 j0 j) ?LL = ω ↑ j"
      by simp
    have "j ≤ j0"
      by (simp add: Suc.prems Suc_leD)
    have inj_BB: "inj_on (BB j0 j) ([{j0<..}]⇗j⇖)"
    proof (clarsimp simp: inj_on_def BB_def nsets_def  sorted_list_of_set_Un less_sets_UN2)
      fix X Y
      assume X: "X ⊆ {j0<..}" and Y: "Y ⊆ {j0<..}"
        and "finite X" "finite Y"
        and jeq: "j = card X"
        and "card Y = card X"
        and eq: "list_of (a j0 ∪ (⋃i<card X. b (enum X i) (j0,i)))
               = list_of (a j0 ∪ (⋃i<card X. b (enum Y i) (j0,i)))"
      have enumX: "⋀n. ⟦n < card X⟧ ⟹ j0 ≤ enum X n"
        using X ‹finite X› finite_enumerate_in_set less_imp_le_nat by blast
      have enumY: "⋀n. ⟦n < card X⟧ ⟹ j0 ≤ enum Y n"
        using subsetD [OF Y] 
        by (metis ‹card Y = card X› ‹finite Y› finite_enumerate_in_set greaterThan_iff less_imp_le_nat)
      have smX: "strict_mono_sets {..<card X} (λi. b (enum X i) (j0, i))"
        and smY: "strict_mono_sets {..<card X} (λi. b (enum Y i) (j0, i))"
        using Suc.prems ‹card Y = card X› ‹finite X› ‹finite Y› bb enumX enumY jeq
        by (auto simp: strict_mono_sets_def)

      have len_eq: "length ms = length ns"
        if "(ms, ns) ∈ list.set (zip (map (list_of ∘ (λi. b (enum X i) (j0,i))) (list_of {..<n}))
                                     (map (list_of ∘ (λi. b (enum Y i) (j0,i))) (list_of {..<n})))"
          "n ≤ card X"
        for ms ns n
        using that
      by (induction n rule: nat.induct) (auto simp: card_b enumX enumY)
      have "concat (map (list_of ∘ (λi. b (enum X i) (j0, i))) (list_of {..<card X}))
          = concat (map (list_of ∘ (λi. b (enum Y i) (j0, i))) (list_of {..<card X}))"
        using eq
        by (simp add: sorted_list_of_set_Un less_sets_UN2 sorted_list_of_set_UN_lessThan ab enumX enumY smX smY)
      then have map_eq: "map (list_of ∘ (λi. b (enum X i) (j0, i))) (list_of {..<card X})
                       = map (list_of ∘ (λi. b (enum Y i) (j0, i))) (list_of {..<card X})"
        by (rule concat_injective) (auto simp: len_eq split: prod.split)
      have "enum X i = enum Y i" if "i < card X" for i
      proof -
        have "Inf (b (enum X i) (j0,i)) = Inf (b (enum Y i) (j0,i))"
          using iffD1 [OF map_eq_conv, OF map_eq] Suc.prems that
          by (metis (mono_tags, lifting) card_b_finite comp_apply finite_lessThan lessThan_iff set_sorted_list_of_set)
        moreover have "Inf (b (enum X i) (j0,i)) ∈ (b (enum X i) (j0,i))"
          "Inf (b (enum Y i) (j0,i)) ∈ (b (enum Y i) (j0,i))" "i < j0"
          using Inf_nat_def1 Suc.prems b_ne enumX enumY jeq that by auto
        ultimately show ?thesis
          by (metis Inf_b_less enumX enumY leI nat_less_le that)
      qed
      then show "X = Y"
        by (simp add: ‹card Y = card X› ‹finite X› ‹finite Y› finite_enum_ext)
    qed
    have BB_Suc': "BB j0 (Suc j) X = usplit (λL k. BB j0 j L @ list_of (b k (j0, j))) X"
      if "X ∈ USigma (𝒦 j0 j) (λK. {Max (insert j0 K)<..})" for X
      using that
      by (simp add: USigma_iff 𝒦_finite less_sets_def usplit_def 𝒦_Suc BB_Suc ‹j ≤ j0›)
    have "ordertype (BB j0 (Suc j) ` 𝒦 j0 (Suc j)) ?LL
        = ordertype
           (usplit (λL k. BB j0 j L @ list_of (b k (j0, j))) ` USigma (𝒦 j0 j) (λK. {Max (insert j0 K)<..})) ?LL"
      by (simp add: BB_Suc' 𝒦_Suc)
    also have "… = ω * ordertype (BB j0 j ` 𝒦 j0 j) ?LL"
    proof (intro ordertype_append_image_IJ)
      fix L k
      assume "L ∈ 𝒦 j0 j" and "k ∈ {Max (insert j0 L)<..}"
      then have "j0 < k" and L: "⋀a. a ∈ L ⟹ a < k"
        by (simp_all add: 𝒦_finite)
      then show "BB j0 j L < list_of (b k (j0, j))"
        by (simp add: ‹L ∈ 𝒦 j0 j› ‹j ≤ j0› 𝒦_finite less_list_of)
    next
      show "inj_on (BB j0 j) (𝒦 j0 j)"
        by (simp add: 𝒦_def inj_BB)
    next
      fix L
      assume L: "L ∈ 𝒦 j0 j"
      then show "L ≪ {Max (insert j0 L)<..} ∧ finite L"
        by (simp add: 𝒦_finite less_sets_def)
      show "ordertype ((λi. list_of (b i (j0, j))) ` {Max (insert j0 L)<..}) ?LL = ω"
        using L Suc.prems Suc_le_lessD otω by blast
    qed (auto simp: 𝒦_finite card_b)
    also have "… = ω ↑ ord_of_nat (Suc j)"
      by (simp add: oexp_mult_commute ih)
    finally show ?case .
  qed

  define seqs where "seqs ≡ λj0 j K. list_of (a j0) # (map (list_of ∘ (λi. b (enum K i) (j0,i))) (list_of {..<j}))"

  have length_seqs [simp]: "length (seqs j0 j K) = Suc j" for j0 j K
    by (simp add: seqs_def)

  have BB_eq_concat_seqs: "BB j0 j K = concat (seqs j0 j K)"
          and seqs_ne: "seqs j0 j K ∈ lists (- {[]})"
      if K: "K ∈ 𝒦 j0 j" and "j ≤ j0" for K j j0
  proof -
    have j0: "⋀i. i < card K ⟹ j0 ≤ enum K i" and le_j0: "card K ≤ j0"
      using finite_enumerate_in_set that unfolding 𝒦_def nsets_def by fastforce+
    show "BB j0 j K = concat (seqs j0 j K)"
      using that unfolding BB_def 𝒦_def nsets_def seqs_def
      by (fastforce simp: j0 ab bb less_sets_UN2 sorted_list_of_set_Un
          strict_mono_sets_def sorted_list_of_set_UN_lessThan)
    have "b (enum K i) (j0, i) ≠ {}" if "i < card K" for i
      using j0 le_j0 less_le_trans that by simp
    moreover have "card K = j"
      using K 𝒦_card by blast
    ultimately show "seqs j0 j K ∈ lists (- {[]})"
      by (clarsimp simp: seqs_def) (metis card_b_finite sorted_list_of_set_eq_Nil_iff)
  qed

  have BB_decomp: "∃cs. BB j0 j K = concat cs ∧ cs ∈ lists (- {[]})"
    if K: "K ∈ 𝒦 j0 j" and "j ≤ j0" for K j j0
    using BB_eq_concat_seqs seqs_ne K that(2) by blast

  have a_subset_M: "a k ⊆ M k" for k
    apply (clarsimp simp: a_def M_def DF_simps F_def Let_def split: prod.split_asm)
    by (metis (no_types) fst_conv fst_grab_subset nxt_subset snd_conv snd_grab_subset subsetD)
  have ba_Suc: "b k (j,i) ≪ a (Suc k)" if "i < j" "j ≤ k" for i j k
    by (meson a_subset_M bM less_sets_weaken2 nat_less_le that)
  have ba: "b k (j,i) ≪ a r" if "i < j" "j ≤ k" "k < r" for i j k r
    by (metis Suc_lessI a_ne aa ba_Suc less_sets_trans that)

  have disjnt_ba: "disjnt (b k (j,i)) (a r)" if "i < j" "j ≤ k" for i j k r
    by (meson ab ba disjnt_sym less_sets_imp_disjnt not_le that)

  have bb_disjnt: "disjnt (b k (j,i)) (b l (r,q))"
    if "q < r" "i < j" "j ≤ k" "r ≤ l" "j < r" for i j q r k l
  proof (cases "k=l")
    case True
    with that show ?thesis
      by (force simp: pair_less_def IJ_def intro: bb_same less_sets_imp_disjnt)
  next
    case False
    with that show ?thesis
      by (metis bb less_sets_imp_disjnt disjnt_sym nat_neq_iff)
  qed

  have sum_card_b: "(∑i<j. card (b (enum K i) (j0, i))) = enum (d j0) j - enum (d j0) 0"
    if K: "K ⊆ {j0<..}" "finite K" "card K ≥ j0" and "j ≤ j0" for j0 j K
    using ‹j ≤ j0›
  proof (induction j)
    case 0
    then show ?case
      by auto
  next
    case (Suc j)
    then have "j < card K"
      using that(3) by linarith
    have dis: "disjnt (b (enum K j) (j0, j)) (⋃i<j. b (enum K i) (j0, i))"
      unfolding disjoint_UN_iff
      by (meson Suc.prems b_disjoint_less disjnt_def disjnt_sym lessThan_iff less_Suc_eq that)
    have j0_less: "j0 < enum K j"
      using K ‹j < card K› by (force simp: finite_enumerate_in_set)
    have "(∑i<Suc j. card (b (enum K i) (j0, i)))
          = card (b (enum K j) (j0, j)) + (∑i<j. card (b (enum K i) (j0, i)))"
      by (simp add: lessThan_Suc card_Un_disjnt [OF _ _ dis])
    also have "… = card (b (enum K j) (j0, j)) + enum (d j0) j - enum (d j0) 0"
      using ‹Suc j ≤ j0› by (simp add: Suc.IH split: nat_diff_split)
    also have "… = enum (d j0) (Suc j) - enum (d j0) 0"
      using j0_less Suc.prems card_b less_or_eq_imp_le by force
    finally show ?case .
  qed

  have card_UN_b: "card (⋃i<j. b (enum K i) (j0, i)) = enum (d j0) j - enum (d j0) 0"
    if K: "K ⊆ {j0<..}" "finite K" "card K ≥ j0" and "j ≤ j0" for j0 j K
    using that by (simp add: card_UN_disjoint sum_card_b b_disjoint)

  have len_BB: "length (BB j j K) = enum (d j) j"
    if K: "K ∈ 𝒦 j j" and "j ≤ j" for j K
  proof -
    have dis_ab: "⋀i. i < j ⟹ disjnt (a j) (b (enum K i) (j,i))"
      using K 𝒦_card 𝒦_enum ab less_sets_imp_disjnt nat_less_le by blast
    show ?thesis
      using K unfolding BB_def 𝒦_def nsets_def
      by (simp add: card_UN_b card_Un_disjnt dis_ab card_a cInf_le_finite finite_enumerate_in_set enum_0_eq_Inf_finite)
  qed

  have "d k ≪ d (Suc k)" for k
    by (metis aM a_ne d_eq da less_sets_fst_grab less_sets_trans less_sets_weaken2 nxt_subset)
  then have dd: "d k' ≪ d k" if "k' < k" for k' k
    by (meson UNIV_I d_ne less_sets_imp_strict_mono_sets strict_mono_sets_def that)

  show thesis
  proof
    show "(⋃ (range XX)) ⊆ WW"
      by (auto simp: XX_def BB_def WW_def)
    show "ordertype (⋃ (range XX)) (?LL) = ω ↑ ω"
      using otωj by (simp add: XX_def ordertype_ωω)
  next
    fix U
    assume U: "U ∈ [⋃ (range XX)]⇗2⇖"
    then obtain x y where Ueq: "U = {x,y}" and len_xy: "length x ≤ length y"
      by (auto simp: lenlex_nsets_2_eq lenlex_length)

    show "∃l. Form l U ∧ (0 < l ⟶ [enum N l] < inter_scheme l U ∧ list.set (inter_scheme l U) ⊆ N)"
    proof (cases "length x = length y")
      case True
      then show ?thesis
        using Form.intros(1) U Ueq by fastforce
    next
      case False
      then have xy: "length x < length y"
        using len_xy by auto
      obtain j r K L where K: "K ∈ 𝒦 j j" and xeq: "x = BB j j K" and ne: "BB j j K ≠ BB r r L"
        and L: "L ∈ 𝒦 r r" and yeq: "y = BB r r L"
        using U by (auto simp: Ueq XX_def)
      then have "length x = enum (d j) j" "length y = enum (d r) r"
        by (auto simp: len_BB)
      then have "j < r"
        using xy dd
        by (metis card_d finite_enumerate_in_set finite_d lessI less_asym less_setsD linorder_neqE_nat)
      then have aj_ar: "a j ≪ a r"
        using aa by auto
      have Ksub: "K ⊆ {j<..}" and "finite K" "card K ≥ j"
        using K by (auto simp: 𝒦_def nsets_def)
      have Lsub: "L ⊆ {r<..}" and "finite L" "card L ≥ r"
        using L by (auto simp: 𝒦_def nsets_def)
      have enumK: "enum K i > j" if "i < j" for i
        using K 𝒦_card 𝒦_enum that by blast
      have enumL: "enum L i > r" if "i < r" for i
        using L 𝒦_card 𝒦_enum that by blast
      have "list.set (acc_lengths w (seqs j0 j K)) ⊆ (+) w ` d j0"
        if K: "K ⊆ {j0<..}" "finite K" "card K ≥ j0" and "j ≤ j0" for j0 j K w
        using ‹j ≤ j0›
      proof (induction j arbitrary: w)
        case 0
        then show ?case
          by (simp add: seqs_def Inf_nat_def1 card_a)
      next
        case (Suc j)
        let ?db = "⨅ (d j0) + ((∑i<j. card (b (enum K i) (j0,i))) + card (b (enum K j) (j0,j)))"
        have "j0 < enum K j"
          by (meson Suc.prems Suc_le_lessD finite_enumerate_in_set greaterThan_iff le_trans subsetD K)
        then have "enum (d j0) j ≥ ⨅ (d j0)"
          using Suc.prems card_d by (simp add: cInf_le_finite finite_enumerate_in_set)
        then have "?db = enum (d j0) (Suc j)"
          using Suc.prems that
          by (simp add: cInf_le_finite finite_enumerate_in_set sum_card_b card_b enum_d_0 ‹j0 < enum K j› less_or_eq_imp_le)
        then have "?db ∈ d j0"
          using Suc.prems finite_enumerate_in_set by (auto simp: finite_enumerate_in_set)
        moreover have "list.set (acc_lengths w (seqs j0 j K)) ⊆ (+) w ` d j0"
          by (simp add: Suc Suc_leD)
        then have "list.set (acc_lengths (w + ⨅ (d j0))
                             (map (list_of ∘ (λi. b (enum K i) (j0,i))) (list_of {..<j})))
                   ⊆ (+) w ` d j0"
          by (simp add: seqs_def card_a subset_insertI)
        ultimately show ?case
          by (simp add: seqs_def acc_lengths_append image_iff Inf_nat_def1
                        sum_sorted_list_of_set_map card_a)
      qed
      then have acc_lengths_subset_d: "list.set (acc_lengths 0 (seqs j0 j K)) ⊆ d j0"
        if K: "K ⊆ {j0<..}" "finite K" "card K ≥ j0" and "j ≤ j0" for j0 j K
        by (metis image_add_0 that)

      have "strict_sorted x" "strict_sorted y"
        by (auto simp: xeq yeq BB_def)
      have disjnt_xy: "disjnt (list.set x) (list.set y)"
      proof -
        have "disjnt (a j) (a r)"
          using ‹j < r› aa less_sets_imp_disjnt by blast
        moreover have "disjnt (b (enum K i) (j,i)) (a r)" if "i < j" for i
          by (simp add: disjnt_ba enumK less_imp_le_nat that)
        moreover have "disjnt (a j) (b (enum L q) (r,q))" if "q < r" for q
          by (meson disjnt_ba disjnt_sym enumL less_imp_le_nat that)
        moreover have "disjnt (b (enum K i) (j,i)) (b (enum L q) (r,q))" if "i < j" "q < r" for i q
        by (meson ‹j < r› bb_disjnt enumK enumL less_imp_le that)
      ultimately show ?thesis
        by (simp add: xeq yeq BB_def)
      qed
      have "∃us vs. merge (seqs j j K) (seqs r r L) us vs"
      proof (rule merge_exists)
        show "strict_sorted (concat (seqs j j K))"
          using BB_eq_concat_seqs K ‹strict_sorted x› xeq by auto
        show "strict_sorted (concat (seqs r r L))"
          using BB_eq_concat_seqs L ‹strict_sorted y› yeq by auto
        show "seqs j j K ∈ lists (- {[]})" "seqs r r L ∈ lists (- {[]})"
          by (auto simp: K L seqs_ne)
        show "hd (seqs j j K) < hd (seqs r r L)"
          by (simp add: aj_ar less_sets_imp_list_less seqs_def)
        show "seqs j j K ≠ []" "seqs r r L ≠ []"
          using seqs_def by blast+
        have less_bb: "b (enum K i) (j,i) ≪ b (enum L p) (r, p)"
          if "¬ b (enum L p) (r, p) ≪ b (enum K i) (j,i)" and "i < j" "p < r"
          for i p
          by (metis IJ_iff ‹j < r› bb bb_same enumK enumL less_imp_le_nat linorder_neqE_nat pair_lessI1 that)
        show "u < v ∨ v < u"
          if "u ∈ list.set (seqs j j K)" and "v ∈ list.set (seqs r r L)" for u v
          using that enumK enumL unfolding seqs_def
          apply (auto simp: seqs_def aj_ar intro!: less_bb less_sets_imp_list_less)
          apply (meson ab ba less_imp_le_nat not_le)+
          done
      qed
      then obtain uus vvs where merge: "merge (seqs j j K) (seqs r r L) uus vvs"
        by metis
      then have "uus ≠ []"
        using merge_length1_gt_0 by (auto simp: seqs_def)
      then obtain u1 us where us: "u1#us = uus"
        by (metis neq_Nil_conv)
      define ku where "ku ≡ length (u1#us)"
      define ps where "ps ≡ acc_lengths 0 (u1#us)"
      have us_ne: "u1#us ∈ lists (- {[]})"
        using merge_length1_nonempty seqs_ne us merge us K by auto
      have xu_eq: "x = concat (u1#us)"
        using BB_eq_concat_seqs K merge merge_preserves us xeq by auto
      then have "strict_sorted u1"
        using ‹strict_sorted x› strict_sorted_append_iff by auto
      have u_sub: "list.set ps ⊆ list.set (acc_lengths 0 (seqs j j K))"
        using acc_lengths_merge1 merge ps_def us by blast
      have "vvs ≠ []"
        using merge BB_eq_concat_seqs L merge_preserves xy yeq by auto
      then obtain v1 vs where vs: "v1#vs = vvs"
        by (metis neq_Nil_conv)
      define kv where "kv ≡ length (v1#vs)"
      define qs where "qs ≡ acc_lengths 0 (v1#vs)"
      have vs_ne: "v1#vs ∈ lists (- {[]})"
        using L merge merge_length2_nonempty seqs_ne vs by auto
      have yv_eq: "y = concat (v1#vs)"
        using BB_eq_concat_seqs L merge merge_preserves vs yeq by auto
      then have "strict_sorted v1"
        using ‹strict_sorted y› strict_sorted_append_iff by auto
      have v_sub: "list.set qs ⊆ list.set (acc_lengths 0 (seqs r r L))"
        using acc_lengths_merge2 merge qs_def vs by blast

      have ss_concat_jj: "strict_sorted (concat (seqs j j K))"
        using BB_eq_concat_seqs K ‹strict_sorted x› xeq by auto
      then obtain k: "0 < kv" "kv ≤ ku" "ku ≤ Suc kv" "kv ≤ Suc j"
        using us vs merge_length_le merge_length_le_Suc merge_length_less2 merge
        unfolding ku_def kv_def by fastforce

      define zs where "zs ≡ concat [ps,u1,qs,v1] @ interact us vs"
      have ss: "strict_sorted zs"
      proof -
        have ssp: "strict_sorted ps"
          unfolding ps_def by (meson strict_sorted_acc_lengths us_ne)
        have ssq: "strict_sorted qs"
          unfolding qs_def by (meson strict_sorted_acc_lengths vs_ne)

        have "d j ≪ list.set x"
          using da [of j] db [of j]  K 𝒦_card 𝒦_enum nat_less_le
          by (auto simp: xeq BB_def less_sets_Un2 less_sets_UN2)
        then have ac_x: "acc_lengths 0 (seqs j j K) < x"
          by (meson Ksub ‹finite K› ‹j ≤ card K› acc_lengths_subset_d le_refl less_sets_imp_list_less less_sets_weaken1)
        then have "ps < x"
          by (meson Ksub ‹d j ≪ list.set x› ‹finite K› ‹j ≤ card K› acc_lengths_subset_d le_refl less_sets_imp_list_less less_sets_weaken1 u_sub)
        then have "ps < u1"
          by (metis Nil_is_append_conv concat.simps(2) hd_append2 less_list_def xu_eq)

        have "d r ≪ list.set y"
          using da [of r] db [of r]  L 𝒦_card 𝒦_enum nat_less_le
          by (auto simp: yeq BB_def less_sets_Un2 less_sets_UN2)
        then have "acc_lengths 0 (seqs r r L) < y"
          by (meson Lsub ‹finite L› ‹r ≤ card L› acc_lengths_subset_d le_refl less_sets_imp_list_less less_sets_weaken1)
        then have "qs < y"
          by (metis L Lsub 𝒦_card ‹d r ≪ list.set y› ‹finite L› acc_lengths_subset_d less_sets_imp_list_less less_sets_weaken1 order_refl v_sub)
        then have "qs < v1"
          by (metis concat.simps(2) gr_implies_not0 hd_append2 less_list_def list.size(3) xy yv_eq)

        have carda_v1: "card (a r) ≤ length v1"
          using length_hd_merge2 [OF merge] unfolding vs [symmetric] by (simp add: seqs_def)
        have ab_enumK: "⋀i. i < j ⟹ a j ≪ b (enum K i) (j,i)"
          by (meson ab enumK le_trans less_imp_le_nat)

        have ab_enumL: "⋀q. q < r ⟹ a j ≪ b (enum L q) (r,q)"
          by (meson ‹j < r› ab enumL le_trans less_imp_le_nat)
        then have ay: "a j ≪ list.set y"
          by (auto simp: yeq BB_def less_sets_Un2 less_sets_UN2 aj_ar)

        have disjnt_hd_last_K_y: "disjnt {hd l..last l} (list.set y)"
          if l: "l ∈ list.set (seqs j j K)" for l
        proof (clarsimp simp add: yeq BB_def disjnt_iff Ball_def, intro conjI strip)
          fix u
          assume u: "u ≤ last l" and "hd l ≤ u"
          with l consider "u ≤ last (list_of (a j))" "hd (list_of (a j)) ≤ u"
            | i where "i<j" "u ≤ last (list_of (b (enum K i) (j,i)))" "hd (list_of (b (enum K i) (j,i))) ≤ u"
            by (force simp: seqs_def)
          note l_cases = this
          then show "u ∉ a r"
          proof cases
            case 1
            then show ?thesis
              by (metis a_ne aj_ar finite_a last_in_set leD less_setsD set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
          next
            case 2
            then show ?thesis
              by (metis enumK ab ba Inf_nat_def1 b_ne card_b_finite hd_b last_in_set less_asym less_setsD not_le set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
          qed
          fix q
          assume "q < r"
          show "u ∉ b (enum L q) (r,q)" 
            using l_cases
          proof cases
            case 1
            then show ?thesis
              by (metis ‹q < r› a_ne ab_enumL finite_a last_in_set leD less_setsD set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
          next
            case 2
            show ?thesis
            proof (cases "enum K i = enum L q")
              case True
              then show ?thesis
                using 2 bb_same [of concl: "enum L q" j i r q] ‹j < r› u
                by (metis IJ_iff b_ne card_b_finite enumK last_in_set leD less_imp_le_nat less_setsD pair_lessI1 set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
            next
              case False
              with 2 bb enumK enumL show ?thesis
                unfolding less_sets_def
                by (metis ‹q < r› b_ne card_b_finite last_in_set leD less_imp_le_nat list.set_sel(1) nat_neq_iff set_sorted_list_of_set sorted_list_of_set_eq_Nil_iff)
            qed
          qed
        qed

        have u1_y: "list.set u1 ≪ list.set y"
          using vs yv_eq L ‹strict_sorted y› merge merge_less_sets_hd merge_preserves seqs_ne ss_concat_jj us by fastforce
        have u1_subset_seqs: "list.set u1 ⊆ list.set (concat (seqs j j K))"
          using merge_preserves [OF merge] us by auto

        have "b k (j,i) ≪ d (Suc k)" if "j≤k" "i<j" for k j i
          by (metis bM d_eq less_sets_fst_grab less_sets_weaken2 nxt_subset that)
        then have bd: "b k (j,i) ≪ d k'" if "j≤k" "i<j" "k < k'" for k k' j i
          by (metis Suc_lessI d_ne dd less_sets_trans that)

        have "a k ≪ d (Suc k)" for k
          by (metis aM d_eq less_sets_fst_grab less_sets_weaken2 nxt_subset)
        then have ad: "a k ≪ d k'" if "k<k'" for k k'
          by (metis Suc_lessI d_ne dd less_sets_trans that)

        have "u1 < y"
          by (simp add: u1_y less_sets_imp_list_less)
        have "n < Inf (d r)" if n: "n ∈ list.set u1" for n
        proof -
          obtain l where l: "l ∈ list.set (seqs j j K)" and n: "n ∈ list.set l"
            using n u1_subset_seqs by auto
          then consider "l = list_of (a j)" | i where "l = list_of (b (enum K i) (j,i))" "i < j"
            by (force simp: seqs_def)
          then show ?thesis
          proof cases
            case 1
            then show ?thesis
              by (metis Inf_nat_def1 ‹j < r› ad d_ne finite_a less_setsD n set_sorted_list_of_set)
          next
            case 2
            then have "hd (list_of (b (enum K i) (j,i))) = Min (b (enum K i) (j,i))"
              by (meson b_ne card_b_finite enumK hd_list_of less_imp_le_nat)
            also have "… ≤ n"
              using 2 n by (simp add: less_list_def disjnt_iff less_sets_def)
            also have f8: "n < hd y"
              using less_setsD that u1_y
              by (metis gr_implies_not0 list.set_sel(1) list.size(3) xy)
            finally have "l < y"
              using 2 disjnt_hd_last_K_y [OF l]
              by (simp add: disjnt_iff) (metis leI less_imp_le_nat less_list_def list.set_sel(1))
            moreover have "last (list_of (b (enum K i) (j,i))) < hd (list_of (a r))"
              using ‹l < y› L n by (auto simp:  2yeq BB_eq_concat_seqs seqs_def less_list_def)
            then have "enum K i < r"
              by (metis "2"(1) a_ne ab card_b_finite empty_iff finite.emptyI finite_a last_in_set leI less_asym less_setsD list.set_sel(1) n set_sorted_list_of_set)
            moreover have "j ≤ enum K i"
              by (simp add: "2"(2) enumK less_imp_le_nat)
            ultimately show ?thesis
              using 2 n bd [of j "enum K i" i r] Inf_nat_def1 less_setsD by force
          qed
        qed
        then have "last u1 < Inf (d r)"
          using ‹uus ≠ []› us_ne by auto
        also have "… ≤ length v1"
          using card_a carda_v1 by auto
        finally have "last u1 < length v1" .
        then have "u1 < qs"
          by (simp add: qs_def less_list_def)

        have "strict_sorted (interact (u1#us) (v1#vs))"
          using L ‹strict_sorted x› ‹strict_sorted y› merge merge_interact merge_preserves seqs_ne us vs xu_eq yv_eq by auto
        then have "strict_sorted (interact us vs)" "v1 < interact us vs"
          by (auto simp: strict_sorted_append_iff)
        moreover have "ps < u1 @ qs @ v1 @ interact us vs"
          using ‹ps < u1› us_ne unfolding less_list_def by auto
        moreover have "u1 < qs @ v1 @ interact us vs"
          by (metis ‹u1 < qs› ‹vvs ≠ []› acc_lengths_eq_Nil_iff hd_append less_list_def qs_def vs)
        moreover have "qs < v1 @ interact us vs"
          using ‹qs < v1› us_ne ‹last u1 < length v1› vs_ne by (auto simp: less_list_def)
        ultimately show ?thesis
          by (simp add: zs_def strict_sorted_append_iff ssp ssq ‹strict_sorted u1› ‹strict_sorted v1›)
      qed
      have ps_subset_d: "list.set ps ⊆ d j"
          using K Ksub 𝒦_card ‹finite K› acc_lengths_subset_d u_sub by blast
      have ps_less_u1: "ps < u1"
        by (metis append.assoc concat.simps(2) ss strict_sorted_append_iff zs_def)
      have qs_subset_d: "list.set qs ⊆ d r"
        using L Lsub 𝒦_card ‹finite L› acc_lengths_subset_d v_sub by blast
      have qs_less_v1: "qs < v1"
        by (metis append.assoc concat.simps(2) ss strict_sorted_append_iff zs_def)
      have FB: "Form_Body ku kv x y zs"
        unfolding Form_Body.simps ku_def kv_def
        using ps_def qs_def ss us_ne vs_ne xu_eq xy yv_eq zs_def by blast
      then have "zs = (inter_scheme ((ku+kv) - Suc 0) {x,y})"
        by (simp add: Form_Body_imp_inter_scheme k)
      obtain l where "l ≤ 2 * (Suc j)" and l: "Form l U" and zs_eq_interact: "zs = inter_scheme l {x,y}"
      proof
        show "ku+kv-1 ≤ 2 * (Suc j)"
          using k by auto
        show "Form (ku+kv-1) U"
        proof (cases "ku=kv")
          case True
          then show ?thesis
            using FB Form.simps Ueq ‹0 < kv› by (auto simp: mult_2)
        next
          case False
          then have "ku = Suc kv"
            using k by auto
          then show ?thesis
            using FB Form.simps Ueq ‹0 < kv› by auto
        qed
        show "zs = inter_scheme (ku + kv - 1) {x, y}"
          using Form_Body_imp_inter_scheme by (simp add: FB k)
      qed
      then have "enum N l ≤ enum N (Suc (2 * Suc j))"
        by (simp add: assms less_imp_le_nat)
      also have "… < Min (d j)"
        by (smt (verit, best) Min_gr_iff d_eq d_ne finite_d fst_grab_subset greaterThan_iff in_mono le_inf_iff nxt_def)
      finally have ls: "{enum N l} ≪ d j"
        by simp
      have "l > 0"
        by (metis l False Form_0_cases_raw Set.doubleton_eq_iff Ueq gr0I)
      show ?thesis
        unfolding Ueq
      proof (intro exI conjI impI)
        have zs_subset: "list.set zs ⊆ list.set (acc_lengths 0 (seqs j j K)) ∪ list.set (acc_lengths 0 (seqs r r L)) ∪ list.set x ∪ list.set y"
          using u_sub v_sub by (auto simp: zs_def xu_eq yv_eq)
        also have "… ⊆ N"
        proof (simp, intro conjI)
          show "list.set (acc_lengths 0 (seqs j j K)) ⊆ N"
            using d_subset_N Ksub ‹finite K› ‹j ≤ card K› acc_lengths_subset_d by blast
          show "list.set (acc_lengths 0 (seqs r r L)) ⊆ N"
            using d_subset_N Lsub ‹finite L› ‹r ≤ card L› acc_lengths_subset_d by blast
          show "list.set x ⊆ N" "list.set y ⊆ N"
            by (simp_all add: xeq yeq BB_def a_subset_N UN_least b_subset_N)
        qed
        finally show "list.set (inter_scheme l {x, y}) ⊆ N"
          using zs_eq_interact by blast
        have "[enum N l] < ps"
          using ps_subset_d ls
          by (metis empty_set less_sets_imp_list_less less_sets_weaken2 list.simps(15))
        then show "[enum N l] < inter_scheme l {x, y}"
          by (simp add: zs_def less_list_def ps_def flip: zs_eq_interact)
      qed (use Ueq l in blast)
    qed
  qed
qed


subsection ‹The main partition theorem for @{term "ω↑ω"}›

definition iso_ll where "iso_ll A B ≡ iso (lenlex less_than ∩ (A×A)) (lenlex less_than ∩ (B×B))"

corollary ordertype_eq_ordertype_iso_ll:
  assumes "Field (Restr (lenlex less_than) A) = A" "Field (Restr (lenlex less_than) B) = B"
  shows "(ordertype A (lenlex less_than) = ordertype B (lenlex less_than))
         ⟷ (∃f. iso_ll A B f)"
proof -
  have "total_on A (lenlex less_than) ∧ total_on B (lenlex less_than)"
    by (meson UNIV_I total_lenlex total_on_def total_on_less_than)
  then show ?thesis
    by (simp add: assms wf_lenlex lenlex_transI iso_ll_def ordertype_eq_ordertype_iso_Restr)
qed

theorem partition_ωω_aux:
  assumes "α ∈ elts ω"
  shows "partn_lst (lenlex less_than) WW [ω↑ω,α] 2" (is "partn_lst ?R WW [ω↑ω,α] 2")
proof (cases "α ≤ 1")
  case True
  then show ?thesis
    using strict_sorted_into_WW unfolding WW_def by (auto intro!: partn_lst_triv1[where i=1])
next
  case False
  obtain m where m: "α = ord_of_nat m"
    using assms elts_ω by auto
  then have "m>1"
    using False by auto
  show ?thesis
    unfolding partn_lst_def
  proof clarsimp
    fix f
    assume f: "f ∈ [WW]⇗2⇖ → {..<Suc (Suc 0)}"
    let ?P0 = "∃X ⊆ WW. ordertype X ?R = ω↑ω ∧ f ` [X]⇗2⇖ ⊆ {0}"
    let ?P1 = "∃M ⊆ WW. ordertype M ?R = α ∧ f ` [M]⇗2⇖ ⊆ {1}"
    have †: "?P0 ∨ ?P1"
    proof (rule disjCI)
      assume not1: "¬ ?P1"
      have "∃W'. ordertype W' ?R = ω↑n ∧ f ` [W']⇗2⇖ ⊆ {0} ∧ W' ⊆ WW_seg (n*m)" for n::nat
      proof -
        have fnm: "f ∈ [WW_seg (n*m)]⇗2⇖ → {..<Suc (Suc 0)}"
          using f WW_seg_subset_WW [of "n*m"] by (meson in_mono nsets_Pi_contra)
        have *: "partn_lst ?R (WW_seg (n*m)) [ω↑n, ord_of_nat m] 2"
          using ordertype_WW_seg [of "n*m"]
          by (simp add: partn_lst_VWF_imp_partn_lst [OF Theorem_3_2])
        show ?thesis
          using partn_lst_E [OF * fnm, simplified]
          by (metis One_nat_def WW_seg_subset_WW less_2_cases m not1 nth_Cons_0 nth_Cons_Suc numeral_2_eq_2 subset_trans)
      qed
      then obtain W':: "nat ⇒ nat list set"
          where otW': "⋀n. ordertype (W' n) ?R = ω↑n"
          and f_W': "⋀n. f ` [W' n]⇗2⇖ ⊆ {0}"
          and seg_W': "⋀n. W' n ⊆ WW_seg (n*m)"
        by metis
      define WW' where "WW' ≡ (⋃n. W' n)"
      have "WW' ⊆ WW"
        using seg_W' WW_seg_subset_WW by (force simp: WW'_def)
      with f have f': "f ∈ [WW']⇗2⇖ → {..<Suc (Suc 0)}"
        using nsets_mono by fastforce
      have ot': "ordertype WW' ?R = ω↑ω"
      proof (rule antisym)
        have "ordertype WW' ?R ≤ ordertype WW ?R"
          by (simp add: ‹WW' ⊆ WW› lenlex_transI ordertype_mono wf_lenlex)
        with ordertype_WW
        show "ordertype WW' ?R ≤ ω ↑ ω"
          by simp
        have "ω ↑ n ≤ ordertype (⋃ (range W')) ?R" for n::nat
          using oexp_Limit ordertype_ωω otW' by auto
        then show "ω ↑ ω ≤ ordertype WW' ?R"
          by (auto simp: elts_ω oexp_Limit ZFC_in_HOL.SUP_le_iff WW'_def)
      qed
      have FR_WW: "Field (Restr (lenlex less_than) WW) = WW"
        by (simp add: Limit_omega_oexp Limit_ordertype_imp_Field_Restr ordertype_WW)
      have FR_WW': "Field (Restr (lenlex less_than) WW') = WW'"
        by (simp add: Limit_omega_oexp Limit_ordertype_imp_Field_Restr ot')
      have FR_W: "Field (Restr (lenlex less_than) (WW_seg n)) = WW_seg n" if "n>0" for n
        by (simp add: Limit_omega_oexp ordertype_WW_seg that Limit_ordertype_imp_Field_Restr)
      have FR_W': "Field (Restr (lenlex less_than) (W' n)) = W' n" if "n>0" for n
        by (simp add: Limit_omega_oexp otW' that Limit_ordertype_imp_Field_Restr)
      have "∃h. iso_ll (WW_seg n) (W' n) h" if "n>0" for n
      proof (subst ordertype_eq_ordertype_iso_ll [symmetric])
        show "ordertype (WW_seg n) (lenlex less_than) = ordertype (W' n) (lenlex less_than)"
          by (simp add: ordertype_WW_seg otW')
      qed (auto simp: FR_W FR_W' that)
      then obtain h_seg where h_seg: "⋀n. n > 0 ⟹ iso_ll (WW_seg n) (W' n) (h_seg n)"
        by metis
      define h where "h ≡ λl. if l=[] then [] else h_seg (length l) l"

      have bij_h_seg: "⋀n. n > 0 ⟹ bij_betw (h_seg n) (WW_seg n) (W' n)"
        using h_seg by (simp add: iso_ll_def iso_iff2 FR_W FR_W')
      have len_h_seg: "length (h_seg (length l) l) = length l * m"
        if "length l > 0" "l ∈ WW" for l
        using bij_betwE [OF bij_h_seg] seg_W' that by (simp add: WW_seg_def subset_iff)
      have hlen: "length (h x) = length (h y) ⟷ length x = length y" if "x ∈ WW" "y ∈ WW" for x y
        using that ‹1 < m› h_def len_h_seg by force

      have h: "iso_ll WW WW' h"
        unfolding iso_ll_def iso_iff2 FR_WW FR_WW'
      proof (intro conjI strip)
        have W'_ne: "W' n ≠ {}" for n
          using otW' [of n] by auto
        then have "[] ∈ WW'"
          using seg_W' [of 0] by (auto simp: WW'_def WW_seg_def)
        let ?g = "λl. if l=[] then l else inv_into (WW_seg (length l div m)) (h_seg (length l div m)) l"
        have h_seg_iff: "⋀n a b. ⟦a ∈ WW_seg n; b ∈ WW_seg n; n>0⟧ ⟹
                          (a, b) ∈ lenlex less_than ⟷
                          (h_seg n a, h_seg n b) ∈ lenlex less_than ∧ h_seg n a ∈ W' n ∧ h_seg n b ∈ W' n"
          using h_seg by (auto simp: iso_ll_def iso_iff2 FR_W FR_W')

        show "bij_betw h WW WW'"
          unfolding bij_betw_iff_bijections
        proof (intro exI conjI ballI)
          fix l
          assume "l ∈ WW"
          then have l: "l ∈ WW_seg (length l)"
            by (simp add: WW_seg_def)
          have "h l ∈ W' (length l)"
          proof (cases "l=[]")
            case True
            with seg_W' [of 0] W'_ne show ?thesis
              by (auto simp: WW_seg_def h_def)
          next
            case False
            then show ?thesis
              using bij_betwE bij_h_seg h_def l by fastforce
          qed
          show "h l ∈ WW'"
            using WW'_def ‹h l ∈ W' (length l)› by blast
          show "?g (h l) = l"
          proof (cases "l=[]")
            case False
            then have "length l > 0"
              by auto
            then have "h_seg (length l) l ≠ []"
              using ‹1 < m› ‹l ∈ WW› len_h_seg by fastforce
            moreover have "bij_betw (h_seg (length l)) (WW_seg (length l)) (W' (length l))"
              using ‹0 < length l› bij_h_seg by presburger
            ultimately show ?thesis
              using ‹l ∈ WW› bij_betw_inv_into_left h_def l len_h_seg by fastforce
          qed (auto simp: h_def)
        next
          fix l
          assume "l ∈ WW'"
          then have l: "l ∈ W' (length l div m)"
            using WW_seg_def ‹1 < m› seg_W' by (fastforce simp: WW'_def)
          show "?g l ∈ WW"
          proof (cases "l=[]")
            case False
            then have "l ∉ W' 0"
              using WW_seg_def seg_W' by fastforce
            with l have "inv_into (WW_seg (length l div m)) (h_seg (length l div m)) l ∈ WW_seg (length l div m)"
              by (metis Nat.neq0_conv bij_betwE bij_betw_inv_into bij_h_seg)
            then show ?thesis
              using False WW_seg_subset_WW by auto
          qed (auto simp: WW_def)

          show "h (?g l) = l"
          proof (cases "l=[]")
            case False
            then have "0 < length l div m"
              using WW_seg_def l seg_W' by fastforce
            then have "inv_into (WW_seg (length l div m)) (h_seg (length l div m)) l ∈ WW_seg (length l div m)"
              by (metis bij_betw_imp_surj_on bij_h_seg inv_into_into l)
            then show ?thesis
              using bij_h_seg [of "length l div m"] WW_seg_def ‹0 < length l div m› bij_betw_inv_into_right l
              by (fastforce simp: h_def)
          qed (auto simp: h_def)
        qed
        fix a b
        assume "a ∈ WW" "b ∈ WW"
        show "(a, b) ∈ Restr (lenlex less_than) WW ⟷ (h a, h b) ∈ Restr (lenlex less_than) WW'"
          (is "?lhs = ?rhs")
        proof
          assume L: ?lhs
          then consider "length a < length b" | "length a = length b" "(a, b) ∈ lex less_than"
            by (auto simp: lenlex_conv)
          then show ?rhs
          proof cases
            case 1
            then have "length (h a) < length (h b)"
              using ‹1 < m› ‹a ∈ WW› ‹b ∈ WW› h_def len_h_seg by auto
            then have "(h a, h b) ∈ lenlex less_than"
              by (auto simp: lenlex_conv)
            then show ?thesis
              using ‹a ∈ WW› ‹b ∈ WW› ‹bij_betw h WW WW'› bij_betwE by fastforce
          next
            case 2
            then have ab: "a ∈ WW_seg (length a)" "b ∈ WW_seg (length a)"
              using ‹a ∈ WW› ‹b ∈ WW› by (auto simp: WW_seg_def)
            have "length (h a) = length (h b)"
              using 2 ‹a ∈ WW› ‹b ∈ WW› h_def len_h_seg by force
            moreover have "(a, b) ∈ lenlex less_than"
              using L by blast
            then have "(h_seg (length a) a, h_seg (length a) b) ∈ lenlex less_than"
              using 2 ab h_seg_iff by blast
            ultimately show ?thesis
              using 2 ‹a ∈ WW› ‹b ∈ WW› ‹bij_betw h WW WW'› bij_betwE h_def by fastforce
          qed
        next
          assume R: ?rhs
          then have R': "(h a, h b) ∈ lenlex less_than"
            by blast
          then consider "length a < length b"
            | "length a = length b" "(h a, h b) ∈ lex less_than"
            using  ‹a ∈ WW› ‹b ∈ WW› ‹m > 1›
            by (auto simp: lenlex_conv h_def len_h_seg split: if_split_asm)
          then show ?lhs
          proof cases
            case 1
            then show ?thesis
              using omega_sum_less_iff ‹a ∈ WW› ‹b ∈ WW› by auto
          next
            case 2
            then have ab: "a ∈ WW_seg (length a)" "b ∈ WW_seg (length a)"
              using ‹a ∈ WW› ‹b ∈ WW› by (auto simp: WW_seg_def)
            then have "(a, b) ∈ lenlex less_than"
              using bij_betwE [OF bij_h_seg] ‹a ∈ WW› ‹b ∈ WW› R' 2
              by (simp add: h_def h_seg_iff split: if_split_asm)
            then show ?thesis
              using ‹a ∈ WW› ‹b ∈ WW› by blast
          qed
        qed
      qed

      let ?fh = "f ∘ image h"
      have "bij_betw h WW WW'" 
        using h unfolding iso_ll_def iso_iff2 by (fastforce simp: FR_WW FR_WW')
      moreover have "{..<Suc (Suc 0)} = {0,1}"
        by auto
      ultimately have fh: "?fh ∈ [WW]⇗2⇖ → {0,1}"
        unfolding Pi_iff using bij_betwE f' bij_betw_nsets by (metis PiE comp_apply)
      have "f{x,y} = 0" if "x ∈ WW'" "y ∈ WW'" "length x = length y" "x ≠ y" for x y
      proof -
        obtain p q where "x ∈ W' p" and "y ∈ W' q"
          using WW'_def ‹x ∈ WW'› ‹y ∈ WW'› by blast
        then obtain n where "{x,y} ∈ [W' n]⇗2⇖"
          using seg_W' ‹1 < m› ‹length x = length y› ‹x ≠ y›
          by (auto simp: WW'_def WW_seg_def subset_iff)
        then show "f{x,y} = 0"
          using f_W' by blast
      qed
      then have fh_eq_0_eqlen: "?fh{x,y} = 0" if "x ∈ WW" "y ∈ WW" "length x = length y" "x≠y" for x y
        using ‹bij_betw h WW WW'› that hlen by (simp add: bij_betw_iff_bijections) metis
      have m_f_0: "∃x∈[M]⇗2⇖. f x = 0" if "M ⊆ WW" "card M = m" for M
      proof -
        have "finite M"
          using False m that by auto
        with not1 [simplified, rule_format, of M] that 
        have "∃x∈[M]⇗2⇖. f x ≠ Suc 0"
          by (simp add: image_subset_iff finite_ordertype_eq_card m)
        with that show ?thesis
          by (metis PiE f lessThan_iff less_2_cases nsets_mono numeral_2_eq_2 subset_iff)
      qed
      have m_fh_0: "∃x∈[M]⇗2⇖. ?fh x = 0" if "M ⊆ WW" "card M = m" for M
      proof -
        have "h ` M ⊆ WW"
          using ‹WW' ⊆ WW› ‹bij_betw h WW WW'› bij_betwE that(1) by fastforce
        moreover have "card (h ` M) = m"
          by (metis ‹bij_betw h WW WW'› bij_betw_def bij_betw_subset card_image that)
        ultimately have "∃x ∈ [h ` M]⇗2⇖. f x = 0"
          by (metis m_f_0)
        then obtain Y where Y: "f (h ` Y) = 0" "Y ⊆ M" and "finite (h ` Y)" "card (h ` Y) = 2"
          by (auto simp: nsets_def subset_image_iff)
        then have "card Y = 2"
          using ‹bij_betw h WW WW'› ‹M ⊆ WW›
          by (metis bij_betw_def card_image inj_on_subset)
        with Y card.infinite[of Y] show ?thesis
          by (auto simp: nsets_def)
      qed

      obtain N j where "infinite N"
        and N: "⋀k u. ⟦k > 0; u ∈ [WW]⇗2⇖; Form k u; [enum N k] < inter_scheme k u; List.set (inter_scheme k u) ⊆ N⟧ ⟹ ?fh u = j k"
        using lemma_3_6 [OF fh] by blast

      have infN': "infinite (enum N ` {k<..})" for k
        by (simp add: ‹infinite N› enum_works finite_image_iff infinite_Ioi strict_mono_imp_inj_on)
      have j_0: "j k = 0" if "k>0" for k
      proof -
        obtain M where M: "M ∈ [WW]⇗m⇖"
                 and MF: "⋀u. u ∈ [M]⇗2⇖ ⟹ Form k u"
                 and Mi: "⋀u. u ∈ [M]⇗2⇖ ⟹ List.set (inter_scheme k u) ⊆ enum N ` {k<..}"
          using lemma_3_7 [OF infN' ‹k > 0›] by metis
        obtain u where u: "u ∈ [M]⇗2⇖" "?fh u = 0"
          using m_fh_0 [of M] M [unfolded nsets_def] by force
        moreover
        have §: "Form k u" "List.set (inter_scheme k u) ⊆ enum N ` {k<..}"
          by (simp_all add: MF Mi ‹u ∈ [M]⇗2⇖›)
        then have "hd (inter_scheme k u) ∈ enum N ` {k<..}"
          using hd_in_set inter_scheme_simple that by blast
        then have "[enum N k] < inter_scheme k u"
          using strict_mono_enum [OF ‹infinite N›] by (auto simp: less_list_def strict_mono_def)
        moreover have "u ∈ [WW]⇗2⇖"
          using M u by (auto simp: nsets_def)
        moreover have "enum N ` {k<..} ⊆ N"
          using ‹infinite N› range_enum by auto
        ultimately show ?thesis
          using N § that by auto
      qed
      obtain X where "X ⊆ WW" and otX: "ordertype X (lenlex less_than) = ω↑ω"
            and X: "⋀u. u ∈ [X]⇗2⇖ ⟹
                   ∃l. Form l u ∧ (l > 0 ⟶ [enum N l] < inter_scheme l u ∧ List.set (inter_scheme l u) ⊆ N)"
        using lemma_3_8 [OF ‹infinite N›] ot' by blast
      have 0: "?fh ` [X]⇗2⇖ ⊆ {0}"
      proof clarsimp
        fix u
        assume u: "u ∈ [X]⇗2⇖"
        obtain l where "Form l u" and l: "l > 0 ⟶ [enum N l] < inter_scheme l u ∧ List.set (inter_scheme l u) ⊆ N"
          using u X by blast
        have "?fh u = 0"
        proof (cases "l = 0")
          case True
          then show ?thesis
            by (metis Form_0_cases_raw ‹Form l u› ‹X ⊆ WW› doubleton_in_nsets_2 fh_eq_0_eqlen subset_iff u)
        next
          case False
          then obtain "[enum N l] < inter_scheme l u" "List.set (inter_scheme l u) ⊆ N" "j l = 0"
            using Nat.neq0_conv j_0 l by blast
          with False show ?thesis
            using ‹X ⊆ WW› N inter_scheme ‹Form l u› doubleton_in_nsets_2 u by (auto simp: nsets_def)
        qed
        then show "f (h ` u) = 0"
          by auto
      qed
      show ?P0
      proof (intro exI conjI)
        show "h ` X ⊆ WW"
          using ‹WW' ⊆ WW› ‹X ⊆ WW› ‹bij_betw h WW WW'› bij_betw_imp_surj_on by fastforce
        show "ordertype (h ` X) (lenlex less_than) = ω ↑ ω"
        proof (subst ordertype_inc_eq)
          show "(h x, h y) ∈ lenlex less_than"
            if "x ∈ X" "y ∈ X" "(x, y) ∈ lenlex less_than" for x y
            using that h ‹X ⊆ WW› by (auto simp: FR_WW FR_WW' iso_iff2 iso_ll_def)
        qed (use otX in auto)
        show "f ` [h ` X]⇗2⇖ ⊆ {0}"
        proof (clarsimp simp: image_subset_iff nsets_def)
          fix Y
          assume Y: "Y ⊆ h ` X" "finite Y" "card Y = 2"
          then have "inv_into WW h ` Y ⊆ X"
            by (metis ‹X ⊆ WW› ‹bij_betw h WW WW'› bij_betw_inv_into_LEFT image_mono)
          moreover have "finite (inv_into WW h ` Y)"
            using ‹finite Y› by blast
          moreover have "card (inv_into WW h ` Y) = 2"
            using Y by (metis ‹X ⊆ WW› card_image inj_on_inv_into subset_image_iff subset_trans)
          ultimately have "f (h ` inv_into WW h ` Y) = 0"
            using 0 by (auto simp: image_subset_iff nsets_def)
          then show "f Y = 0"
            by (metis ‹X ⊆ WW› ‹Y ⊆ h ` X› image_inv_into_cancel image_mono order_trans)
        qed
      qed
    qed
    then show "∃i<Suc (Suc 0). ∃H⊆WW. ordertype H ?R = [ω↑ω, α] ! i ∧ f ` [H]⇗2⇖ ⊆ {i}"
      by (metis One_nat_def lessI nth_Cons_0 nth_Cons_Suc zero_less_Suc)
  qed
qed

text ‹Theorem 3.1 of Jean A. Larson, ibid.›
theorem partition_ωω: "α ∈ elts ω ⟹ partn_lst_VWF (ω↑ω) [ω↑ω,α] 2"
  using partn_lst_imp_partn_lst_VWF_eq [OF partition_ωω_aux] ordertype_WW by auto

end