Theory DCR3_Optimality

(*     License:    LGPL  *)

subsection ‹Optimality of the DCR3 method for proving confluence of relations of the least uncountable cardinality›

theory DCR3_Optimality
  imports 
    "HOL-Cardinals.Cardinals"
    Finite_DCR_Hierarchy
begin

(* ----------------------------------------------------------------------- *)

subsubsection ‹Auxiliary definitions›

(* ----------------------------------------------------------------------- *)

datatype Lev = 𝗅0 | 𝗅1 | 𝗅2 | 𝗅3 | 𝗅4 | 𝗅5 | 𝗅6 | 𝗅7 | 𝗅8

type_synonym 'U rD = "Lev × 'U set × 'U set × 'U set"

fun rP :: "Lev ⇒ 'U set ⇒ 'U set ⇒ 'U set ⇒ Lev ⇒ 'U set ⇒ 'U set ⇒ 'U set ⇒ bool"
where
  "rP 𝗅0 A B C n' A' B' C' = (A = {} ∧ B = {} ∧ C = {} ∧ n' = 𝗅1 ∧ finite A' ∧ B' = {} ∧ C' = {})"
| "rP 𝗅1 A B C n' A' B' C' = (finite A ∧ B = {} ∧ C = {} ∧ n' = 𝗅2 ∧ A' = A ∧ B' = {} ∧ C' = {})"
| "rP 𝗅2 A B C n' A' B' C' = (finite A ∧ B = {} ∧ C = {} ∧ n' = 𝗅3 ∧ A' = A ∧ finite B' ∧ C' = {})"
| "rP 𝗅3 A B C n' A' B' C' = (finite A ∧ finite B ∧ C = {} ∧ n' = 𝗅4 ∧ A' = A ∧ B' = B ∧ C' = {})"
| "rP 𝗅4 A B C n' A' B' C' = (finite A ∧ finite B ∧ C = {} ∧ n' = 𝗅5 ∧ A' = A ∧ B' = B ∧ finite C')"
| "rP 𝗅5 A B C n' A' B' C' = (finite A ∧ finite B ∧ finite C ∧ n' = 𝗅6 ∧ A' = A ∧ B' = B ∧ C' = C)"
| "rP 𝗅6 A B C n' A' B' C' = (finite A ∧ finite B ∧ finite C ∧ n' = 𝗅7 ∧ A' = A ∪ B ∪ C ∧ B' = A' ∧ C' = A')"
| "rP 𝗅7 A B C n' A' B' C' = (finite A ∧ B = A ∧ C = A ∧ n' = 𝗅8 ∧ A' = A ∧ B' = A' ∧ C' = A')"
| "rP 𝗅8 A B C n' A' B' C' = (finite A ∧ B = A ∧ C = A ∧ n' = 𝗅7 ∧ A ⊂ A' ∧ finite A' ∧ B' = A' ∧ C' = A')"

definition rC :: "'U set ⇒ 'U set ⇒ 'U set ⇒ 'U set ⇒ bool"
where
  "rC S A B C = (A ⊆ S ∧ B ⊆ S ∧ C ⊆ S)"

definition rE :: "'U set ⇒ ('U rD) rel"
where
  "rE S = { ((n1, A1, B1, C1), (n2, A2, B2, C2)). rP n1 A1 B1 C1 n2 A2 B2 C2 ∧ rC S A1 B1 C1 ∧ rC S A2 B2 C2 }"

fun lev_next :: "Lev ⇒ Lev"
where
  "lev_next 𝗅0 = 𝗅1" 
| "lev_next 𝗅1 = 𝗅2"
| "lev_next 𝗅2 = 𝗅3"
| "lev_next 𝗅3 = 𝗅4"
| "lev_next 𝗅4 = 𝗅5"
| "lev_next 𝗅5 = 𝗅6"
| "lev_next 𝗅6 = 𝗅7"
| "lev_next 𝗅7 = 𝗅8"
| "lev_next 𝗅8 = 𝗅7"

fun levrd :: "'U rD ⇒ Lev"
where
  "levrd (n, A, B, C) = n"

fun wrd :: "'U rD ⇒ 'U set"
where
  "wrd (n, A, B, C) = A ∪ B ∪ C"

definition Wrd :: "'U rD set ⇒ 'U set"
where
  "Wrd S = (⋃ (wrd ` S))"

definition bkset :: "'a rel ⇒ 'a set ⇒ 'a set" 
where 
  "bkset r A = ((r^*)^-1)``A"

(* ----------------------------------------------------------------------- *)

subsubsection ‹Auxiliary lemmas›

(* ----------------------------------------------------------------------- *)

lemma lem_rtr_field: "(x,y) ∈ r^* ⟹ (x = y) ∨ (x ∈ Field r ∧ y ∈ Field r)"
  by (metis Field_def Not_Domain_rtrancl Range.RangeI UnCI rtranclE)

lemma lem_fin_fl_rel: "finite (Field r) = finite r"
  using finite_Field finite_subset trancl_subset_Field2 by fastforce

lemma lem_rel_inf_fld_card:
fixes r::"'U rel"
assumes "¬ finite r"
shows "|Field r| =o |r|"
proof -
  obtain f1::"'U × 'U ⇒ 'U" where b1: "f1 = (λ (x,y). x)" by blast
  obtain f2::"'U × 'U ⇒ 'U" where b2: "f2 = (λ (x,y). y)" by blast
  then have "f1 ` r = Domain r ∧ f2 ` r = Range r" using b1 b2 by force
  then have b3: "|Domain r| ≤o |r| ∧ |Range r| ≤o |r|" 
    using card_of_image[of f1 r] card_of_image[of f2 r] by simp
  have "|Domain r| ≤o |Range r| ∨ |Range r| ≤o |Domain r|" by (simp add: ordLeq_total)
  moreover have "|Domain r| ≤o |Range r| ⟶ |Field r| ≤o |r|"
  proof
    assume c1: "|Domain r| ≤o |Range r|"
    moreover have "finite (Domain r) ∧ finite (Range r) ⟶ finite (Field r)" unfolding Field_def by blast
    ultimately have "¬ finite (Range r)" 
      using assms lem_fin_fl_rel card_of_ordLeq_finite by blast
    then have "|Field r| =o |Range r|" using c1 card_of_Un_infinite unfolding Field_def by blast
    then show "|Field r| ≤o |r|" using b3 ordIso_ordLeq_trans by blast
  qed
  moreover have "|Range r| ≤o |Domain r| ⟶ |Field r| ≤o |r|"
  proof
    assume c1: "|Range r| ≤o |Domain r|"
    moreover have "finite (Domain r) ∧ finite (Range r) ⟶ finite (Field r)" unfolding Field_def by blast
    ultimately have "¬ finite (Domain r)" 
      using assms lem_fin_fl_rel card_of_ordLeq_finite by blast
    then have "|Field r| =o |Domain r|" using c1 card_of_Un_infinite unfolding Field_def by blast
    then show "|Field r| ≤o |r|" using b3 ordIso_ordLeq_trans by blast
  qed
  ultimately have "|Field r| ≤o |r|" by blast
  moreover have "|r| ≤o |Field r|"
  proof -
    have "r ⊆ (Field r) × (Field r)" unfolding Field_def by force
    then have c1: "|r| ≤o |Field r × Field r|" by simp
    have "¬ finite (Field r)" using assms lem_fin_fl_rel by blast
    then have c2: "|Field r × Field r| =o |Field r|" by simp
    show ?thesis using c1 c2 using ordLeq_ordIso_trans by blast
  qed
  ultimately show ?thesis using ordIso_iff_ordLeq by blast
qed

lemma lem_confl_field: "confl_rel r = (∀ a ∈ Field r. ∀ b ∈ Field r. ∀ c ∈ Field r. (a,b) ∈ r^* ∧ (a,c) ∈ r^* ⟶ 
                  (∃ d ∈ Field r. (b,d) ∈ r^* ∧ (c,d) ∈ r^*))"
proof
  assume b1: "confl_rel r"
  show "∀ a ∈ Field r. ∀ b ∈ Field r. ∀ c ∈ Field r. (a,b) ∈ r^* ∧ (a,c) ∈ r^* ⟶ 
                  (∃ d ∈ Field r. (b,d) ∈ r^* ∧ (c,d) ∈ r^*)"
  proof (intro ballI impI)
    fix a b c
    assume c1: "a ∈ Field r" and c2: "b ∈ Field r" and c3: "c ∈ Field r" and c4: "(a,b) ∈ r^* ∧ (a,c) ∈ r^*"
    obtain d where "(b,d) ∈ r^* ∧ (c,d) ∈ r^*" using b1 c4 unfolding confl_rel_def by blast
    moreover then have "d ∈ Field r" using c2 using lem_rtr_field by fastforce
    ultimately show "∃ d ∈ Field r. (b,d) ∈ r^* ∧ (c,d) ∈ r^*" by blast
  qed
next
  assume b1: "∀ a ∈ Field r. ∀ b ∈ Field r. ∀ c ∈ Field r. (a,b) ∈ r^* ∧ (a,c) ∈ r^* ⟶ 
                  (∃ d ∈ Field r. (b,d) ∈ r^* ∧ (c,d) ∈ r^*)"
  have "∀a b c. (a, b) ∈ r^* ∧ (a, c) ∈ r^* ⟶ (∃d. (b, d) ∈ r^* ∧ (c, d) ∈ r^*)"
  proof (intro allI impI)
    fix a b c
    assume "(a, b) ∈ r^* ∧ (a, c) ∈ r^*"
    moreover then have "a ∉ Field r ∨ b ∉ Field r ∨ c ∉ Field r ⟶ a = b ∨ a = c" by (meson lem_rtr_field)
    ultimately show "∃d. (b, d) ∈ r^* ∧ (c, d) ∈ r^*" using b1 by blast
  qed
  then show "confl_rel r" unfolding confl_rel_def by blast
qed

lemma lem_d2_to_dc2:
fixes r::"'U rel"
assumes "DCR2 r"
shows "DCR 2 r"
proof -
  obtain r0 r1 where b1: "r = r0 ∪ r1"
       and b2: "∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0 ⟶ jn00 r0 b c"
       and b3: "∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r1 ⟶ jn01 r0 r1 b c"
       and b4: "∀ a b c. (a,b) ∈ r1 ∧ (a,c) ∈ r1 ⟶ jn11 r0 r1 b c" 
     using assms unfolding DCR2_def LD2_def by blast
  obtain g::"nat ⇒ 'U rel" 
    where b5: "g = (λ α::nat. if α = 0 then r0 else (if α = 1 then r1 else {}))" by blast
  have b6: "g 0 = r0 ∧ g 1 = r1" using b5 by simp
  have b7: "∀ n. (¬ (n = 0 ∨ n = 1)) ⟶ g n = {}" using b5 by simp
  have "∀α β a b c. (a, b) ∈ g α ∧ (a, c) ∈ g β ⟶
       (∃b' b'' c' c'' d. (b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α)"
  proof (intro allI impI)
    fix α β a b c
    assume c1: "(a, b) ∈ g α ∧ (a, c) ∈ g β"
    then have c2: "(α = 0 ∨ α = 1) ∧ (β = 0 ∨ β = 1)" using b7 by blast
    show "∃b' b'' c' c'' d. (b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α"
    proof -
      have "α = 0 ∧ β = 0 ⟶ ?thesis"
      proof
        assume e1: "α = 0 ∧ β = 0"
        then have "jn00 r0 b c" using c1 b2 b6 by blast
        then obtain d where "(b, d) ∈ r0^= ∧ (c, d) ∈ r0^=" unfolding jn00_def by blast
        then have "(b, b, d, d) ∈ 𝔇 g 0 0 ∧ (c, c, d, d) ∈ 𝔇 g 0 0" using b6 unfolding 𝔇_def by blast
        then show "∃b' b'' c' c'' d. (b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α" using e1 by blast
      qed
      moreover have "α = 0 ∧ β = 1 ⟶ ?thesis"
      proof
        assume e1: "α = 0 ∧ β = 1"
        then have "jn01 r0 r1 b c" using c1 b3 b6 by blast
        then obtain b'' d where "(b,b'') ∈ r1^= ∧ (b'',d) ∈ r0^* ∧ (c,d) ∈ r0^*" unfolding jn01_def by blast
        moreover have "𝔏v g 0 1 = g 0 ∧ 𝔏v g 1 0 = g 0" using b6 b7 unfolding 𝔏v_def by blast
        ultimately have "(b, b, b'', d) ∈ 𝔇 g 0 1 ∧ (c, c, c, d) ∈ 𝔇 g 1 0" using b6 unfolding 𝔇_def by simp
        then show "∃b' b'' c' c'' d. (b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α" using e1 by blast
      qed
      moreover have "α = 1 ∧ β = 0 ⟶ ?thesis"
      proof
        assume e1: "α = 1 ∧ β = 0"
        then have "jn01 r0 r1 c b" using c1 b3 b6 by blast
        then obtain c'' d where "(c,c'') ∈ r1^= ∧ (c'',d) ∈ r0^* ∧ (b,d) ∈ r0^*" unfolding jn01_def by blast
        moreover have "𝔏v g 0 1 = g 0 ∧ 𝔏v g 1 0 = g 0" using b6 b7 unfolding 𝔏v_def by blast
        ultimately have "(b, b, b, d) ∈ 𝔇 g 1 0 ∧ (c, c, c'', d) ∈ 𝔇 g 0 1" using b6 unfolding 𝔇_def by simp
        then show "∃b' b'' c' c'' d. (b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α" using e1 by blast
      qed
      moreover have "α = 1 ∧ β = 1 ⟶ ?thesis"
      proof
        assume e1: "α = 1 ∧ β = 1"
        then have "jn11 r0 r1 b c" using c1 b4 b6 by blast
        then obtain b' b'' c' c'' d where 
              e2: "(b,b') ∈ r0^* ∧ (b',b'') ∈ r1^= ∧ (b'',d) ∈ r0^*"
          and e3: "(c,c') ∈ r0^* ∧ (c',c'') ∈ r1^= ∧ (c'',d) ∈ r0^*" unfolding jn11_def by blast
        moreover have "𝔏v g 1 1 = g 0 ∧ 𝔏1 g 1 = g 0" using b6 b7 unfolding 𝔏1_def 𝔏v_def by blast
        ultimately have "(b, b', b'', d) ∈ 𝔇 g 1 1 ∧ (c, c', c'', d) ∈ 𝔇 g 1 1" using b6 unfolding 𝔇_def by simp
        then show "∃b' b'' c' c'' d. (b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α" using e1 by blast
      qed
      ultimately show ?thesis using c2 by blast
    qed
  qed
  then have "DCR_generating g" unfolding DCR_generating_def by blast
  moreover have "r = ⋃{r'. ∃α'<2. r' = g α'}"
  proof
    show "r ⊆ ⋃{r'. ∃α'<2. r' = g α'}"
    proof
      fix p
      assume "p ∈ r"
      then have "p ∈ r0 ∨ p ∈ r1" using b1 by blast
      moreover have "(0::nat) < (2::nat) ∧ (1::nat) < (2::nat)" by simp
      ultimately show "p ∈ ⋃{r'. ∃α'<2. r' = g α'}" using b6 by blast
    qed
  next
    show "⋃{r'. ∃α'<2. r' = g α'} ⊆ r"
    proof
      fix p
      assume "p ∈ ⋃{r'. ∃α'<2. r' = g α'}"
      then obtain α' where "α'<2 ∧ p ∈ g α'" by blast
      moreover then have "α' = 0 ∨ α' = 1" by force
      ultimately show "p ∈ r" using b1 b6 by blast
    qed
  qed
  ultimately show ?thesis unfolding DCR_def by blast
qed

lemma lem_dc2_to_d2:
fixes r::"'U rel"
assumes "DCR 2 r"
shows "DCR2 r"
proof -
  obtain g where b1: "DCR_generating g" and b2: "r = ⋃{r'. ∃α'<2. r' = g α'}" 
      using assms unfolding DCR_def by blast
  have "∀ α::nat. α<2 ⟷ α = 0 ∨ α = 1" by force
  then have b3: "𝔏1 g 0 = {} ∧ 𝔏1 g 1 = g 0 ∧ 𝔏1 g 2 = g 0 ∪ g 1
      ∧ 𝔏v g 0 0 = {} ∧ 𝔏v g 1 0 = g 0 ∧ 𝔏v g 0 1 = g 0 ∧ 𝔏v g 1 1 = g 0"
    unfolding 𝔏1_def 𝔏v_def by (simp_all, blast+)
  have "r = (g 0) ∪ (g 1)"
  proof
    show "r ⊆ (g 0) ∪ (g 1)"
    proof
      fix p
      assume "p ∈ r"
      then obtain α where "p ∈ g α ∧ α < 2" using b2 by blast
      moreover have "∀ α::nat. α<2 ⟷ α = 0 ∨ α = 1" by force
      ultimately show "p ∈ (g 0) ∪ (g 1)" by force
    qed
  next
    have "(0::nat) < (2::nat) ∧ (1::nat) < (2::nat)" by simp
    then show "(g 0) ∪ (g 1) ⊆ r" using b2 by blast
  qed
  moreover have "∀ a b c. (a,b) ∈ (g 0) ∧ (a,c) ∈ (g 0) ⟶ jn00 (g 0) b c"
  proof (intro allI impI)
    fix a b c
    assume "(a,b) ∈ (g 0) ∧ (a,c) ∈ (g 0)"
    then obtain b' b'' c' c'' d where "(b, b', b'', d) ∈ 𝔇 g 0 0 ∧ (c, c', c'', d) ∈ 𝔇 g 0 0" 
      using b1 unfolding DCR_generating_def by blast
    then show "jn00 (g 0) b c" unfolding jn00_def 𝔇_def 𝔏1_def 𝔏v_def by force
  qed
  moreover have "∀ a b c. (a,b) ∈ (g 0) ∧ (a,c) ∈ (g 1) ⟶ jn01 (g 0) (g 1) b c"
  proof (intro allI impI)
    fix a b c
    assume "(a,b) ∈ (g 0) ∧ (a,c) ∈ (g 1)"
    then obtain b' b'' c' c'' d where 
      "(b, b', b'', d) ∈ 𝔇 g 0 1 ∧ (c, c', c'', d) ∈ 𝔇 g 1 0" 
        using b1 unfolding DCR_generating_def by blast
    then show "jn01 (g 0) (g 1) b c" unfolding jn01_def 𝔇_def 𝔏1_def 𝔏v_def by force
  qed
  moreover have "∀ a b c. (a,b) ∈ (g 1) ∧ (a,c) ∈ (g 1) ⟶ jn11 (g 0) (g 1) b c"
  proof (intro allI impI)
    fix a b c
    assume "(a,b) ∈ (g 1) ∧ (a,c) ∈ (g 1)"
    then obtain b' b'' c' c'' d where "(b, b', b'', d) ∈ 𝔇 g 1 1 ∧ (c, c', c'', d) ∈ 𝔇 g 1 1" 
        using b1 unfolding DCR_generating_def by blast
    then show "jn11 (g 0) (g 1) b c" 
        unfolding jn11_def 𝔇_def apply (simp only: b3) 
        by blast
  qed
  ultimately have "LD2 r (g 0) (g 1)" unfolding LD2_def by blast
  then show ?thesis unfolding DCR2_def by blast
qed

lemma lem_rP_inv: "rP n A B C n' A' B' C' ⟹ ( A ⊆ A' ∧ B ⊆ B' ∧ C ⊆ C' 
        ∧ finite A ∧ finite B ∧ finite C ∧ finite A' ∧ finite B' ∧ finite C' )"
  by (cases n, cases n', force+)

lemma lem_infset_finext:
fixes S::"'U set" and A::"'U set"
assumes "¬ finite S" and "finite A" and "A ⊆ S"
shows "∃ B. B ⊆ S ∧ A ⊂ B ∧ finite B"
proof -
  have b1: "finite A" using assms lem_rP_inv by blast
  then have "A ≠ S" using assms by blast
  then obtain A2 x where "x ∈ S ∧ A2 = A ∪ {x} ∧ x ∉ A ∧ A2 ⊆ S" using assms by force
  moreover then have "finite A2" using b1 by blast
  ultimately show ?thesis by blast
qed

lemma lem_rE_df:
fixes S::"'U set"
shows  "(u,v) ∈ rE S ⟹ (u,w) ∈ rE S ⟹ (v,t) ∈ (rE S)^= ⟹ (w,t) ∈ (rE S)^= ⟹ v = w"
proof -
  assume "(u,v) ∈ rE S" and "(u,w) ∈ rE S" and "(v,t) ∈ (rE S)^=" and "(w,t) ∈ (rE S)^="
  moreover have "⋀ u v w t. (u,v) ∈ rE S ⟹ (u, w) ∈ rE S ⟹ (v, t) ∈ rE S ∨ v = t ⟹ (w, t) ∈ rE S ⟹ v = w"
  proof -
    fix u v w t
    assume "(u,v) ∈ (rE S)" and "(u, w) ∈ (rE S)" and "(v, t) ∈ (rE S) ∨ v = t" and "(w, t) ∈ (rE S)"
    moreover obtain n::Lev and a b c where "u = (n,a,b,c)" using prod_cases4 by blast
    moreover obtain n'::Lev and a' b' c' where "v = (n',a',b',c')" using prod_cases4 by blast
    moreover obtain n''::Lev and a'' b'' c'' where "w = (n'',a'',b'',c'')" using prod_cases4 by blast
    moreover obtain n'''::Lev and a''' b''' c''' where "t = (n''',a''',b''',c''')" using prod_cases4 by blast
    ultimately show "v = w" 
      apply (simp add: rE_def) 
      apply (cases n)
      apply (cases n')
      apply (cases n'')
      apply (cases n''')
      by simp+
  qed
  ultimately show ?thesis by blast
qed

lemma lem_rE_succ_lev:
fixes S::"'U set"
assumes "(u,v) ∈ rE S" 
shows "levrd v = (lev_next (levrd u))"
proof -
  obtain n A B C where b1: "u = (n,A,B,C)" using prod_cases4 by blast
  moreover obtain n' A' B' C' where b2: "v = (n',A',B',C')" using prod_cases4 by blast
  ultimately have "rP n A B C n' A' B' C'" using assms unfolding rE_def by blast
  then have "n' = (lev_next n)" by (cases n, auto+)
  then show ?thesis using b1 b2 by simp
qed

lemma lem_rE_levset_inv:
fixes S::"'U set" and L u v
assumes a1: "(u,v) ∈ (rE S)^*" and a2: "levrd u ∈ L" and a3: "lev_next ` L ⊆ L"
shows "levrd v ∈ L"
proof -
  have "⋀ k. ∀ u v::'U rD. (u,v) ∈ (rE S)^^k ∧ levrd u ∈ L ⟶ levrd v ∈ L"
  proof -
    fix k
    show "∀ u v::'U rD. (u,v) ∈ (rE S)^^k ∧ levrd u ∈ L ⟶ levrd v ∈ L"
    proof (induct k)
      show "∀ u v::'U rD. (u,v) ∈ (rE S)^^0 ∧ levrd u ∈ L ⟶ levrd v ∈ L" by simp
    next
      fix k
      assume d1: "∀ u v::'U rD. (u,v) ∈ (rE S)^^k ∧ levrd u ∈ L ⟶ levrd v ∈ L"
      show "∀ u v::'U rD. (u,v) ∈ (rE S)^^(Suc k) ∧ levrd u ∈ L ⟶ levrd v ∈ L"
      proof (intro allI impI)
        fix u v::"'U rD"
        assume "(u,v) ∈ (rE S)^^(Suc k) ∧ levrd u ∈ L"
        moreover then obtain v' where e1: "(u,v') ∈ (rE S)^^k ∧ (v',v) ∈ (rE S)" by force
        ultimately have "levrd v' ∈ L" using d1 by blast
        then have "levrd v ∈ lev_next ` L" using e1 lem_rE_succ_lev[of v' v] by force
        then show "levrd v ∈ L" using a3 by force
      qed
    qed
  qed
  then show ?thesis using a1 a2 rtrancl_imp_relpow by blast
qed

lemma lem_rE_levun: 
fixes S::"'U set"
shows "u ∈ Domain (rE S) ⟹ levrd u ∈ {𝗅1, 𝗅3, 𝗅5} ⟹ ∃ v. (rE S)``{u} ⊆ {v}"
proof -
  assume a1: "u ∈ Domain (rE S)" and a2: "levrd u ∈ {𝗅1, 𝗅3, 𝗅5}"
  then obtain v where b1: "(u,v) ∈ (rE S)" by blast
  obtain n a b c where b2: "u = (n,a,b,c)" using prod_cases4 by blast
  obtain n' a' b' c' where b3: "v = (n',a',b',c')" using prod_cases4 by blast
  have b4: "rP n a b c n' a' b' c'" using b1 b2 b3 unfolding rE_def by blast
  have "n = 𝗅1 ∨ n = 𝗅3 ∨ n = 𝗅5" using b2 a2 by simp
  moreover have "n = 𝗅1 ⟶ (rE S) `` {u} ⊆ {v}" using b2 b3 b4 unfolding rE_def by force
  moreover have "n = 𝗅3 ⟶ (rE S) `` {u} ⊆ {v}" using b2 b3 b4 unfolding rE_def by force
  moreover have "n = 𝗅5 ⟶ (rE S) `` {u} ⊆ {v}" using b2 b3 b4 unfolding rE_def by force
  ultimately show "∃ v. (rE S)``{u} ⊆ {v}" by blast
qed

lemma lem_rE_domfield:
fixes S::"'U set"
assumes "¬ finite S"
shows "Domain (rE S) = Field (rE S)"
proof -
  have "⋀ u2 u1::'U rD. (u2,u1) ∈ rE S ⟹ ∃ u3. (u1,u3) ∈ rE S"
  proof -
    fix u2 u1::"'U rD"
    assume c1: "(u2,u1) ∈ rE S"
    obtain n1 A1 B1 C1 where c2: "u1 = (n1,A1,B1,C1)" using prod_cases4 by blast
    obtain n2 A2 B2 C2 where c3: "u2 = (n2,A2,B2,C2)" using prod_cases4 by blast
    have c4: "rP n2 A2 B2 C2 n1 A1 B1 C1 ∧ rC S A2 B2 C2 ∧ rC S A1 B1 C1" using c1 c2 c3 unfolding rE_def by blast
    then have "finite (A1 ∪ A2)" using lem_rP_inv by blast
    moreover have "A1 ∪ A2 ⊆ S" using c4 unfolding rC_def by blast
    ultimately obtain A3 where c5: "A3 ⊆ S ∧ A1 ⊂ A3 ∧ A2 ⊂ A3 ∧ finite A3" 
      using assms lem_infset_finext[of S "A1 ∪ A2"] by blast
    have "∃ n3 A3 B3 C3. (rP n1 A1 B1 C1 n3 A3 B3 C3 ∧ rC S A3 B3 C3)" 
    using c4 unfolding rC_def
      apply (cases n1)
      apply (cases n2, simp+)
      apply (cases n2, simp+)
      apply (cases n2, simp+)
      apply (force, simp+)
      apply (cases n2, simp+)
      apply (cases n2, simp+)
      apply (force, simp+)
      apply (cases n2, simp+)
      apply (cases n2, simp+)
      apply (cases n2, simp+)
      using c5 apply (cases n2)
      apply simp+
      apply blast
      apply simp
      done
    then obtain n3 A3 B3 C3 where "rP n1 A1 B1 C1 n3 A3 B3 C3 ∧ rC S A3 B3 C3" by blast
    moreover obtain u3 where "u3 = (n3, A3, B3, C3)" by blast
    moreover have "rC S A1 B1 C1" using c1 c2 unfolding rE_def by blast
    ultimately have "(u1,u3) ∈ rE S" using c2 unfolding rE_def by blast
    then show "∃ u3. (u1,u3) ∈ rE S" by blast
  qed
  then show ?thesis unfolding Field_def by blast
qed

lemma lem_wrd_fin_field_rE: 
fixes S::"'U set"
assumes "¬ finite S"
shows "u ∈ Field (rE S) ⟹ finite (wrd u)"
proof -
  assume "u ∈ Field (rE S)"
  then have "u ∈ Domain (rE S)" using assms lem_rE_domfield by blast
  then show "finite (wrd u)" using lem_rP_inv unfolding rE_def by force
qed

lemma lem_rE_rtr_wrd_mon:
fixes S::"'U set" and u v::"'U rD"
shows "(u,v) ∈ (rE S)^* ⟹ wrd u ⊆ wrd v"
proof -
  assume a1: "(u,v) ∈ (rE S)^*"
  have b1: "⋀ u v::'U rD. (u,v) ∈ (rE S) ⟹ wrd u ⊆ wrd v"
  proof -
    fix u v::"'U rD"
    assume a1: "(u,v) ∈ (rE S)"
    obtain n A B C where b1: "u = (n,A,B,C)" using prod_cases4 by blast
    obtain n' A' B' C' where b2: "v = (n',A',B',C')" using prod_cases4 by blast
    have "wrd u = A ∪ B ∪ C ∧ wrd v = A'∪ B'∪ C'" using a1 b1 b2 by simp
    then show "wrd u ⊆ wrd v" using a1 b1 b2 lem_rP_inv unfolding rE_def by fast
  qed
  have "⋀ n. ∀ u v::'U rD. (u,v) ∈ (rE S)^^n ⟶ wrd u ⊆ wrd v"
  proof -
    fix n 
    show "∀ u v::'U rD. (u,v) ∈ (rE S)^^n ⟶ wrd u ⊆ wrd v"
    proof (induct n)
      show "∀ u v. (u,v) ∈ (rE S)^^0 ⟶ wrd u ⊆ wrd v" by simp
    next
      fix m
      assume d1: "∀ u v::'U rD. (u,v) ∈ (rE S)^^m ⟶ wrd u ⊆ wrd v"
      show "∀ u v::'U rD. (u,v) ∈ (rE S)^^(Suc m) ⟶ wrd u ⊆ wrd v"
      proof (intro allI impI)
        fix u v::"'U rD"
        assume "(u,v) ∈ (rE S)^^(Suc m)"
        then obtain v' where "(u,v') ∈ (rE S)^^m ∧ (v',v) ∈ (rE S)" by force
        then show "wrd u ⊆ wrd v" using d1 b1 by blast
      qed
    qed
  qed
  then show "wrd u ⊆ wrd v" using a1 rtrancl_imp_relpow by blast
qed

lemma lem_Wrd_bkset_rE: "Wrd (bkset (rE S) U) = Wrd U"
proof
  show "Wrd (bkset (rE S) U) ⊆ Wrd U"
  proof
    fix y
    assume "y ∈ Wrd (bkset (rE S) U)"
    then obtain u v where "u ∈ U ∧ (v,u) ∈ (rE S)^* ∧ y ∈ wrd v" unfolding Wrd_def bkset_def by force
    moreover then have "wrd v ⊆ wrd u" using lem_rE_rtr_wrd_mon by blast
    ultimately show "y ∈ Wrd U" unfolding Wrd_def by blast
  qed
next
  show "Wrd U ⊆ Wrd (bkset (rE S) U)" unfolding Wrd_def bkset_def by blast
qed

lemma lem_Wrd_rE_field_subs_cnt: 
fixes S::"'U set" and U::"('U rD) set"
assumes "¬ finite S"
shows "U ⊆ Field (rE S) ⟹ |U| ≤o |UNIV::nat set| ⟹ |Wrd U| ≤o |UNIV::nat set|"
proof -
  assume b1: "U ⊆ Field (rE S)" and a2: "|U| ≤o |UNIV::nat set|"
  moreover have "∀u∈U. |wrd u| ≤o |UNIV::nat set|"
  proof
    fix u::"'U rD"
    assume "u ∈ U"
    then have "finite (wrd u)" using b1 assms lem_wrd_fin_field_rE by blast
    then show "|wrd u| ≤o |UNIV::nat set|" using ordLess_imp_ordLeq by force
  qed
  ultimately have "|⋃u∈U. wrd u| ≤o |UNIV::nat set|" 
    using card_of_UNION_ordLeq_infinite infinite_UNIV_nat by blast
  then show "|Wrd U| ≤o |UNIV::nat set|" unfolding Wrd_def by simp
qed

lemma lem_rE_dn_cnt: 
fixes S::"'U set" and U::"('U rD) set"
assumes "¬ finite S"
shows "U ⊆ Field (rE S) ⟹ |U| ≤o |UNIV::nat set| ⟹ V ⊆ bkset (rE S) U ⟹ |Wrd V| ≤o |UNIV::nat set|"
proof -
  assume a1: "U ⊆ Field (rE S)" and a2: "|U| ≤o |UNIV::nat set|" and a3: "V ⊆ bkset (rE S) U"
  have "Wrd V ⊆ Wrd (bkset (rE S) U)" using a3 unfolding Wrd_def by blast
  then have "|Wrd V| ≤o |Wrd (bkset (rE S) U)|" by simp
  moreover have "|Wrd (bkset (rE S) U)| ≤o |UNIV::nat set|" 
    using a1 a2 assms lem_Wrd_bkset_rE[of S U] lem_Wrd_rE_field_subs_cnt[of S U] by force
  ultimately show "|Wrd V| ≤o |UNIV::nat set|" using ordLeq_transitive by blast
qed

lemma lem_rE_succ_Wrd_univ: "(u,w) ∈ (rE S) ⟹ levrd u ∈ {𝗅0, 𝗅2, 𝗅4} ⟹ S - wrd w ⊆ Wrd (((rE S)``{u}) - {w})"
proof -
  assume a1: "(u,w) ∈ (rE S)" and a2: "levrd u ∈ {𝗅0, 𝗅2, 𝗅4}"
  moreover obtain n a b c where b2: "u = (n,a,b,c)" using prod_cases4 by blast
  moreover obtain n' a' b' c' where b3: "w = (n',a',b',c')" using prod_cases4 by blast
  ultimately have b4: "rP n a b c n' a' b' c' ∧ rC S a b c ∧ rC S a' b' c'" unfolding rE_def by blast
  have "∀ y ∈ S. y ∉ wrd w ⟶ (∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v)"
  proof (intro ballI impI)
    fix y
    assume c0: "y ∈ S" and c1: "y ∉ wrd w"
    have "n = 𝗅0 ⟶ (∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v)"
    proof
      assume "n = 𝗅0"
      then have "(u, (𝗅1, {y}, {}, {})) ∈ (rE S)" using c0 b2 b4 unfolding rE_def rC_def by force
      then show "∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v" using c1 by force
    qed
    moreover have "n = 𝗅2 ⟶ (∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v)"
    proof
      assume "n = 𝗅2"
      then have "(u, (𝗅3, a, {y}, {})) ∈ (rE S)" using c0 b2 b4 unfolding rE_def rC_def by force
      then show "∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v" using c1 by force
    qed
    moreover have "n = 𝗅4 ⟶ (∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v)"
    proof
      assume "n = 𝗅4"
      then have "(u, (𝗅5, a, b, {y})) ∈ (rE S)" using c0 b2 b4 unfolding rE_def rC_def by force
      then show "∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v" using c1 by force
    qed
    ultimately show "∃ v ∈ (rE S)``{u} - {w}. y ∈ wrd v" using a2 b2 by force
  qed
  then show "S - wrd w ⊆ Wrd (((rE S)``{u}) - {w})" unfolding Wrd_def by blast
qed

lemma lem_rE_succ_nocntbnd:
fixes S::"'U set" and u0::"'U rD" and v0::"'U rD" and U::"('U rD) set"
assumes a0: "¬ |S| ≤o |UNIV::nat set|" and a1: "(u0, v0) ∈ (rE S)" and a2: "levrd u0 ∈ {𝗅0, 𝗅2, 𝗅4}"
    and a3: "U ⊆ Field (rE S)" and a4: "((rE S) `` {u0}) - {v0} ⊆ bkset (rE S) U"
shows "¬ |U| ≤o |UNIV::nat set|"
proof
  assume "|U| ≤o |UNIV::nat set|"
  moreover have c0: "¬ finite S" using a0 by (meson card_of_Well_order infinite_iff_card_of_nat ordLeq_total)
  ultimately have c1: "|Wrd (((rE S)``{u0}) - {v0})| ≤o |UNIV::nat set|" using a3 a4 lem_rE_dn_cnt by blast
  have "v0 ∈ Field (rE S)" using a1 unfolding Field_def by blast
  then have "finite (wrd v0)" using c0 a0 lem_wrd_fin_field_rE by blast
  then have "¬ |S - wrd v0| ≤o |UNIV::nat set|" using a0 
    by (metis card_of_infinite_diff_finite finite_iff_cardOf_nat ordIso_symmetric ordLeq_iff_ordLess_or_ordIso ordLeq_transitive)
  moreover have "S - wrd v0 ⊆ Wrd (((rE S)``{u0}) - {v0})" using lem_rE_succ_Wrd_univ a1 a2 by blast
  ultimately have "¬ |Wrd (((rE S)``{u0}) - {v0})| ≤o |UNIV::nat set|" by (metis card_of_mono1 ordLeq_transitive)
  then show "False" using c1 by blast
qed

lemma lem_rE_succ_nocntbnd2:
fixes S::"'U set" and u0::"'U rD" and v0::"'U rD"
assumes a0: "¬ |S| ≤o |UNIV::nat set|"
    and a1: "(u0, v0) ∈ (rE S)" and a2: "levrd u0 ∈ {𝗅0, 𝗅2, 𝗅4}"
    and a3: "r ⊆ (rE S)" and a4: "∀ u. |r``{u}| ≤o |UNIV::nat set|"
    and a5: "((rE S) `` {u0}) - {v0} ⊆ bkset (rE S) ((r^*)``{u0})"
shows "False"
proof -
  have b1: "⋀ n::nat. ⋀ u::('U rD). u ∈ Field (rE S) ⟶ (r^^n)``{u} ⊆ Field (rE S) ∧ |(r^^n)``{u}| ≤o |UNIV::nat set|"
  proof (intro impI)
    fix n::nat and u::"'U rD"
    assume c1: "u ∈ Field (rE S)"
    show "(r^^n)``{u} ⊆ Field (rE S) ∧ |(r^^n) `` {u}| ≤o |UNIV::nat set|"
    proof (induct n)
      show "(r^^0)``{u} ⊆ Field (rE S) ∧ |(r ^^ 0) `` {u}| ≤o |UNIV::nat set|" using c1 by simp
    next
      fix m
      assume d1: "(r^^m)``{u} ⊆ Field (rE S) ∧ |(r^^m)``{u}| ≤o |UNIV::nat set|"
      moreover have "∀ v ∈ (r^^m)``{u}. |r``{v}| ≤o |UNIV::nat set|" using a4 by blast
      moreover have  "(r ^^ Suc m) `` {u} = (⋃v∈((r^^m)``{u}). r ``{v})" by force
      ultimately have "|(r ^^ Suc m) `` {u}| ≤o |UNIV::nat set|" 
        using card_of_UNION_ordLeq_infinite[of "UNIV::nat set" "(r^^m)``{u}"] infinite_UNIV_nat by simp
      moreover have "(r ^^ Suc m)``{u} ⊆ Field (rE S)" using d1 a3 unfolding Field_def by fastforce
      ultimately show "(r ^^ Suc m)``{u} ⊆ Field (rE S) ∧ |(r ^^ Suc m) `` {u}| ≤o |UNIV::nat set|" by blast
    qed
  qed
  have b2: "⋀ u::'U rD. u ∈ Field (rE S) ⟶ |(r^*) `` {u}| ≤o |UNIV::nat set|"
  proof (intro impI)
    fix u::"'U rD"
    assume c1: "u ∈ Field (rE S)"
    have "|UNIV::nat set| ≤ |UNIV::nat set|" by simp
    moreover have "∀n. |(r^^n) `` {u}| ≤o |UNIV::nat set|" using c1 b1 by blast
    ultimately have c1: "|⋃n. (r^^n) `` {u}| ≤o |UNIV::nat set|"
      using card_of_UNION_ordLeq_infinite[of "UNIV::nat set" "UNIV::nat set"] infinite_UNIV_nat by simp
    have "(r^*) `` {u} ⊆ (⋃n. (r^^n) `` {u})" by (simp add: rtrancl_is_UN_relpow subset_eq)
    then have "|(r^*) `` {u}| ≤o |⋃n. (r^^n) `` {u}|" by simp
    then show "|(r^*) `` {u}| ≤o |UNIV::nat set|" using c1 ordLeq_transitive by blast
  qed
  obtain U where b3: "U = ((r^*) `` {u0})" by blast
  have "U ⊆ (⋃n. (r^^n) `` {u0})" using b3 by (simp add: rtrancl_is_UN_relpow subset_eq)
  moreover have "u0 ∈ Field (rE S)" using a1 unfolding Field_def by blast
  ultimately have "U ⊆ Field (rE S) ∧ |U| ≤o |UNIV::nat set|" using b1 b2 b3 by blast
  moreover have "((rE S) `` {u0}) - {v0} ⊆ bkset (rE S) U" using b3 a5 by blast
  ultimately show "False" using a0 a1 a2 lem_rE_succ_nocntbnd[of S u0 v0 U] by blast
qed

lemma lem_rE_diamsubr_un:
fixes S::"'U set"
assumes a1: "r0 ⊆ (rE S)" and a2: "∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0 ⟶ (∃ d. (b,d) ∈ r0^= ∧ (c,d) ∈ r0^=)"
shows "∀ u. ∃ v. r0``{u} ⊆ {v}"
proof
  fix u
  have "∀ v w. (u,v) ∈ r0 ∧ (u,w) ∈ r0 ⟶ v = w"
  proof (intro allI impI)
    fix v w
    assume "(u,v) ∈ r0 ∧ (u,w) ∈ r0"
    moreover then obtain t where "(v,t) ∈ r0^= ∧ (w,t) ∈ r0^=" using a2 by blast
    ultimately have "(u,v) ∈ (rE S) ∧ (u,w) ∈ (rE S) ∧ (v,t) ∈ (rE S)^= ∧ (w,t) ∈ (rE S)^=" using a1 by blast
    then show "v = w" using lem_rE_df by blast
  qed
  then show "∃ v. r0``{u} ⊆ {v}" by blast
qed

lemma lem_rE_succ_nocntbnd3:
fixes S::"'U set" and u0::"'U rD" and v0::"'U rD"
assumes a0: "¬ |S| ≤o |UNIV::nat set|"
    and a1: "LD2 (rE S) r0 r1"
    and a2: "(u0, v0) ∈ (rE S)" and a3: "levrd u0 ∈ {𝗅0, 𝗅2, 𝗅4}"
    and a4: "r = {(u,v) ∈ rE S. u = v0} ∪ r0"
    and a5: "((rE S) `` {u0}) - {v0} ⊆ bkset (rE S) ((r^*)``{u0})"
shows "False"
proof -
  have b1: "r0 ⊆ (rE S)" using a1 unfolding LD2_def by blast
  then have "r ⊆ (rE S)" using a4 by blast
  moreover have "∀ u. |r``{u}| ≤o |UNIV::nat set|"
  proof
    fix u
    have "∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0 ⟶ (∃ d. (b,d) ∈ r0^= ∧ (c,d) ∈ r0^=)"
      using a1 unfolding LD2_def jn00_def by blast
    then obtain v where "r0``{u} ⊆ {v}" using b1 lem_rE_diamsubr_un[of r0] by blast
    moreover have "r``{u} ⊆ r0``{u} ∪ (rE S)``{v0}" using a4 by blast
    ultimately have "r``{u} ⊆ {v} ∪ (rE S)``{v0}" by blast
    moreover have "|{v} ∪ (rE S)``{v0}| ≤o |UNIV::nat set|"
    proof -
      have "levrd v0 ∈ {𝗅1, 𝗅3, 𝗅5}" using a2 a3 unfolding rE_def by force
      moreover have "¬ finite S" using a0 by (meson card_of_Well_order infinite_iff_card_of_nat ordLeq_total)
      moreover then have "v0 ∈ Domain (rE S)" using a2 a0 lem_rE_domfield unfolding Field_def by blast
      ultimately obtain v0' where "(rE S)``{v0} ⊆ {v0'}" using lem_rE_levun by blast
      then have "{v} ∪ (rE S)``{v0} ⊆ {v,v0'}" by blast
      then have "finite ({v} ∪ (rE S)``{v0})" by (meson finite.emptyI finite.insertI rev_finite_subset)
      then show ?thesis by (simp add: ordLess_imp_ordLeq)
    qed
    ultimately show "|r``{u}| ≤o |UNIV::nat set|" using card_of_mono1 ordLeq_transitive by blast
  qed
  ultimately show ?thesis using a0 a2 a3 a5 lem_rE_succ_nocntbnd2[of S u0 v0 r] by blast
qed

lemma lem_rE_one:
fixes S::"'U set" and u0::"'U rD" and v0::"'U rD"
assumes a0: "¬ |S| ≤o |UNIV::nat set|" and a1: "LD2 (rE S) r0 r1" 
    and a2: "(u0, v0) ∈ r0" and a3: "levrd u0 ∈ {𝗅0, 𝗅2, 𝗅4}"
shows "False"
proof -
  obtain r where b1: "r = {(u,v) ∈ rE S. u = v0} ∪ r0" by blast
  moreover have "(u0, v0) ∈ (rE S)" using a1 a2 unfolding LD2_def by blast
  moreover have "((rE S) `` {u0}) - {v0} ⊆ bkset (rE S) ((r^*)``{u0})"
  proof
    fix v
    assume c1: "v ∈ ((rE S) `` {u0}) - {v0}"
    have "∃ v. r0``{u0} ⊆ {v}" using a1 lem_rE_diamsubr_un[of r0 S] unfolding LD2_def jn00_def by blast
    then have "r0 `` {u0} ⊆ {v0}" using a2 by blast
    moreover have c2: "(rE S) = r0 ∪ r1" using a1 unfolding LD2_def by blast
    ultimately have "(u0, v) ∈ r1" using c1 by blast
    then have "jn01 r0 r1 v0 v" using a1 a2 unfolding LD2_def by blast
    then obtain v0' d where c3: "(v0, v0') ∈ r1^= ∧ (v0', d) ∈ r0^* ∧ (v, d) ∈ r0^*" unfolding jn01_def by blast
    obtain U where c4: "U = (r^*)``{u0}" by blast
    have "(u0, d) ∈ r^*"
    proof -
      have "v0 = v0' ∨ (v0,v0') ∈ (rE S)" using c2 c3 by blast
      then have "(v0, v0') ∈ r^=" using b1 by blast
      moreover have "(u0, v0) ∈ r" using b1 a2 by blast
      ultimately have "(u0, v0') ∈ r^*" by force
      moreover have "(v0',d) ∈ r^*" using c3 b1 rtrancl_mono[of r0 r] by blast
      ultimately show ?thesis by force
    qed
    then have "d ∈ U" using c4 by blast
    then have c3: "v ∈ bkset r0 U" using c3 unfolding bkset_def by blast
    have "r0 ⊆ (rE S)" using a1 unfolding LD2_def by blast
    then have "bkset r0 U ⊆ bkset (rE S) U" unfolding bkset_def by (simp add: Image_mono rtrancl_mono)
    then show "v ∈ bkset (rE S) ((r^*)``{u0})" using c3 c4 by blast
  qed
  ultimately show "False" using a0 a1 a3 lem_rE_succ_nocntbnd3[of S r0 r1 u0 v0 r] by blast
qed

lemma lem_rE_jn0:
fixes S::"'U set" and u1::"'U rD" and u2::"'U rD" and v::"'U rD"
assumes a1: "(u1,v) ∈ (rE S)" and a2: "(u2,v) ∈ (rE S)" and a3: "u1 ≠ u2"
shows "levrd v ∈ {𝗅7, 𝗅8}"
proof -
  obtain n1 a1 b1 c1 where b1: "u1 = (n1,a1,b1,c1)" using prod_cases4 by blast
  obtain n2 a2 b2 c2 where b2: "u2 = (n2,a2,b2,c2)" using prod_cases4 by blast
  obtain n a b c where b3: "v = (n,a,b,c)" using prod_cases4 by blast
  have "rP n1 a1 b1 c1 n a b c" using b1 b3 a1 unfolding rE_def by blast
  moreover have "rP n2 a2 b2 c2 n a b c" using b2 b3 a2 unfolding rE_def by blast
  moreover have "(n1,a1,b1,c1) ≠ (n2,a2,b2,c2)" using a3 b1 b2 by blast
  ultimately have "n ∈ { 𝗅7, 𝗅8}"
    apply (cases n1, cases n2)
    apply (simp+, cases n2)
    apply (simp+, cases n2)
    apply (simp+, cases n2)
    apply (simp+, cases n2)
    apply (simp+, cases n2)
    apply simp+
    done
  then show ?thesis using b3 by simp
qed

lemma lem_rE_jn1:
fixes S::"'U set" and u1::"'U rD" and u2::"'U rD" and v::"'U rD"
assumes a1: "(u1,v) ∈ (rE S)" and a2: "(u2,v) ∈ (rE S)^*" and a3: "(u1,u2) ∉ (rE S) ∧ (u2,u1) ∉ (rE S)^*"
shows "levrd v ∈ {𝗅7, 𝗅8}"
proof -
  have "⋀ k2. ∀ u1 u2 v::'U rD. ∀ i. i ≤ k2 ∧ (u1,u2) ∉ (rE S) ∧ (u2,u1) ∉ (rE S)^* ⟶ (u1,v) ∈ (rE S) ⟶ (u2,v) ∈ (rE S)^^i ⟶ levrd v ∈ {𝗅7, 𝗅8}"
  proof -
    fix k2
    show "∀ u1 u2 v::'U rD. ∀ i. i ≤ k2 ∧ (u1,u2) ∉ (rE S) ∧ (u2,u1) ∉ (rE S)^* ⟶ (u1,v) ∈ (rE S) ⟶ (u2,v) ∈ (rE S)^^i ⟶ levrd v ∈ {𝗅7, 𝗅8}"
    proof (induct k2)
      show "∀u1 u2 v::'U rD. ∀ i. i ≤ 0 ∧ (u1,u2) ∉ (rE S) ∧ (u2,u1) ∉ (rE S)^* ⟶ (u1, v) ∈ (rE S) ⟶ (u2, v) ∈ (rE S)^^i ⟶ levrd v ∈ {𝗅7, 𝗅8}" by force
    next
      fix k2
      assume d1: "∀u1 u2 v::'U rD. ∀ i.  i ≤ k2 ∧ (u1,u2) ∉ (rE S) ∧ (u2, u1) ∉ (rE S)^* ⟶
                 (u1, v) ∈ (rE S) ⟶ (u2, v) ∈ (rE S)^^i ⟶ levrd v ∈ {𝗅7, 𝗅8}"
      show "∀u1 u2 v::'U rD. ∀ i. i ≤ Suc k2 ∧ (u1,u2) ∉ (rE S) ∧ (u2, u1) ∉ (rE S)^* ⟶
          (u1, v) ∈ (rE S) ⟶ (u2, v) ∈ (rE S)^^i ⟶ levrd v ∈ {𝗅7, 𝗅8}"
      proof (intro allI impI)
        fix u1 u2 v::"'U rD" and i
        assume e1: "i ≤ Suc k2 ∧ (u1, u2) ∉ (rE S) ∧ (u2, u1) ∉ (rE S)^*" 
           and e2: "(u1, v) ∈ (rE S)" and e3: "(u2, v) ∈ (rE S)^^i"
        show "levrd v ∈ {𝗅7, 𝗅8}"
        proof (cases "i = Suc k2")
          assume f1: "i = Suc k2"
          then obtain v' where f2: "(u2, v') ∈ (rE S)" and f3: "(v', v) ∈ (rE S)^^k2" using e3 by (meson relpow_Suc_E2)
          moreover have "k2 ≤ k2" using e1 by force
          ultimately have "(v',u1) ∉ (rE S)^* ∧ (u1,v') ∉ (rE S) ⟶ levrd v ∈ {𝗅7, 𝗅8}" using e2 d1 by blast
          moreover have "(v',u1) ∈ (rE S)^* ⟶ False"
          proof
            assume "(v',u1) ∈ (rE S)^*"
            then have "(u2,u1) ∈ (rE S)^*" using f2 by force
            then show "False" using e1 by blast
          qed
          moreover have "(u1,v') ∈ (rE S) ⟶ levrd v ∈ {𝗅7, 𝗅8}"
          proof
            assume "(u1,v') ∈ (rE S)"
            moreover have "u1 ≠ u2" using e1 by force
            ultimately have "levrd v' ∈ {𝗅7, 𝗅8}" using f2 lem_rE_jn0[of u1 v' S u2] by blast
            moreover have "(v', v) ∈ (rE S)^*" using f3 rtrancl_power by blast
            moreover have "lev_next ` {𝗅7, 𝗅8} ⊆ {𝗅7, 𝗅8}" by simp
            ultimately show "levrd v ∈ {𝗅7, 𝗅8}" using lem_rE_levset_inv[of v' v S "{𝗅7, 𝗅8}"] by blast
          qed
          ultimately show ?thesis by blast
        next
          assume "i ≠ Suc k2"
          then have "i ≤ k2" using e1 by force
          then show ?thesis using d1 e1 e2 e3 by blast
        qed
      qed
    qed
  qed
  moreover obtain k2 where "(u2,v) ∈ (rE S)^^k2" using a2 rtrancl_imp_relpow by blast  
  moreover have "k2 ≤ k2" by force
  ultimately show ?thesis using a1 a3 by blast
qed

lemma lem_rE_jn2:
fixes S::"'U set" and u1::"'U rD" and u2::"'U rD" and v::"'U rD"
assumes a1: "(u1,v) ∈ (rE S)^*" and a2: "(u2,v) ∈ (rE S)^*" and a3: "(u1,u2) ∉ (rE S)^* ∧ (u2,u1) ∉ (rE S)^*"
shows "levrd v ∈ {𝗅7, 𝗅8}"
proof -
  have "⋀ k1. ∀ u1 u2 v::'U rD. ∀ i. i ≤ k1 ∧ (u1,u2) ∉ (rE S)^* ∧ (u2,u1) ∉ (rE S)^* ⟶ (u1,v) ∈ (rE S)^^i ⟶ (u2,v) ∈ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}"
  proof -
    fix k1
    show "∀ u1 u2 v::'U rD. ∀ i. i ≤ k1 ∧ (u1,u2) ∉ (rE S)^* ∧ (u2,u1) ∉ (rE S)^* ⟶ (u1,v) ∈ (rE S)^^i ⟶ (u2,v) ∈ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}"
    proof (induct k1)
      show "∀u1 u2 v::'U rD. ∀ i. i ≤ 0 ∧ (u1,u2) ∉ (rE S)^* ∧ (u2,u1) ∉ (rE S)^* ⟶ (u1, v) ∈ (rE S)^^i ⟶ (u2, v) ∈ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}"
      proof (intro allI impI)
        fix u1 u2 v::"'U rD" and i
        assume "i ≤ 0 ∧ (u1,u2) ∉ (rE S)^* ∧ (u2,u1) ∉ (rE S)^*" and "(u1, v) ∈ (rE S)^^i" and "(u2, v) ∈ (rE S)^*"
        moreover then have "(u2,u1) ∈ (rE S)^*" using rtrancl_power by fastforce
        ultimately have "False" by blast
        then show "levrd v ∈ {𝗅7, 𝗅8}" by blast
      qed
    next
      fix k1
      assume d1: "∀u1 u2 v::'U rD. ∀ i.  i ≤ k1 ∧ (u1, u2) ∉ (rE S)^* ∧ (u2, u1) ∉ (rE S)^* ⟶
                 (u1, v) ∈ (rE S) ^^ i ⟶ (u2, v) ∈ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}"
      show "∀u1 u2 v::'U rD. ∀ i. i ≤ Suc k1 ∧ (u1, u2) ∉ (rE S)^* ∧ (u2, u1) ∉ (rE S)^* ⟶
          (u1, v) ∈ (rE S) ^^ i ⟶ (u2, v) ∈ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}"
      proof (intro allI impI)
        fix u1 u2 v::"'U rD" and i
        assume e1: "i ≤ Suc k1 ∧ (u1, u2) ∉ (rE S)^* ∧ (u2, u1) ∉ (rE S)^*" 
           and e2: "(u1, v) ∈ (rE S)^^i" and e3: "(u2, v) ∈ (rE S)^*"
        show "levrd v ∈ {𝗅7, 𝗅8}"
        proof (cases "i = Suc k1")
          assume f1: "i = Suc k1"
          then obtain v' where f2: "(u1, v') ∈ (rE S)" and f3: "(v', v) ∈ (rE S)^^k1" using e2 by (meson relpow_Suc_E2)
          moreover have "k1 ≤ k1" using e1 by force
          ultimately have "(v',u2) ∉ (rE S)^* ∧ (u2,v') ∉ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}" using e3 d1 by blast
          moreover have "(v',u2) ∈ (rE S)^* ⟶ False"
          proof
            assume "(v',u2) ∈ (rE S)^*"
            then have "(u1,u2) ∈ (rE S)^*" using f2 by force
            then show "False" using e1 by blast
          qed
          moreover have "(u2,v') ∈ (rE S)^* ⟶ levrd v ∈ {𝗅7, 𝗅8}"
          proof
            assume "(u2,v') ∈ (rE S)^*"
            then have "levrd v' ∈ {𝗅7, 𝗅8}" using e1 f2 lem_rE_jn1[of u1 v' S u2] by blast
            moreover have "(v', v) ∈ (rE S)^*" using f3 rtrancl_power by blast
            moreover have "lev_next ` {𝗅7, 𝗅8} ⊆ {𝗅7, 𝗅8}" by simp
            ultimately show "levrd v ∈ {𝗅7, 𝗅8}" using lem_rE_levset_inv[of v' v S "{𝗅7, 𝗅8}"] by blast
          qed
          ultimately show ?thesis by blast
        next
          assume "i ≠ Suc k1"
          then have "i ≤ k1" using e1 by force
          then show ?thesis using d1 e1 e2 e3 by blast
        qed
      qed
    qed
  qed
  moreover obtain k1 where "(u1,v) ∈ (rE S)^^k1" using a1 rtrancl_imp_relpow by blast  
  moreover have "k1 ≤ k1" by force
  ultimately show ?thesis using a2 a3 by blast
qed

lemma lem_rel_pow2fw: "(u,u1) ∈ r ∧ (u1,v) ∈ r⟶ (u,v) ∈ r^^2" 
  by (metis Suc_1 relpow_1 relpow_Suc_I)

lemma lem_rel_pow3fw: "(u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,v) ∈ r ⟶ (u,v) ∈ r^^3" 
  by (metis One_nat_def numeral_3_eq_3 relpow_1 relpow_Suc_I)

lemma lem_rel_pow3: "(u,v) ∈ r^^3 ⟹ ∃ u1 u2. (u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,v) ∈ r"
  by (metis One_nat_def numeral_3_eq_3 relpow_1 relpow_Suc_E)

lemma lem_rel_pow4: "(u,v) ∈ r^^4 ⟹ ∃ u1 u2 u3. (u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,u3) ∈ r ∧ (u3,v) ∈ r"
proof -
  assume "(u,v) ∈ r^^4"
  then obtain u3 where "(u,u3) ∈ r^^3 ∧ (u3,v) ∈ r" using relpow_E by force
  moreover then obtain u1 u2 where "(u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,u3) ∈ r"
    by (metis One_nat_def numeral_3_eq_3 relpow_1 relpow_Suc_E)
  ultimately show "∃ u1 u2 u3. (u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,u3) ∈ r ∧ (u3,v) ∈ r" by blast
qed

lemma lem_rel_pow5: "(u,v) ∈ r^^5 ⟹ ∃ u1 u2 u3 u4. (u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,u3) ∈ r ∧ (u3,u4) ∈ r ∧ (u4,v) ∈ r"
proof -
  assume "(u,v) ∈ r^^5"
  then obtain u4 where "(u,u4) ∈ r^^4 ∧ (u4,v) ∈ r" using relpow_E by force
  moreover then obtain u1 u2 u3 where "(u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,u3) ∈ r ∧ (u3, u4) ∈ r"
    using lem_rel_pow4[of u u4 r] by blast
  ultimately show "∃ u1 u2 u3 u4. (u,u1) ∈ r ∧ (u1,u2) ∈ r ∧ (u2,u3) ∈ r ∧ (u3,u4) ∈ r ∧ (u4,v) ∈ r" by blast
qed

lemma lem_rE_l1_l78_dist:
fixes S::"'U set"
assumes a1: "levrd u = 𝗅1" and a2: "levrd v ∈ {𝗅7, 𝗅8}" and a3: "n ≤ 5"
shows "(u,v) ∉ (rE S)^^n"
proof -
  have b0: "(u,v) ∉ (rE S)^^0" using a1 a2 by force
  have b1: "(u,v) ∉ (rE S)^^1" using a1 a2 lem_rE_succ_lev[of u v] by force
  have "⋀ u1. (u,u1) ∈ (rE S) ∧ (u1,v) ∈ (rE S) ⟹ False" 
    using a1 a2 lem_rE_succ_lev
    by (metis Lev.distinct(49) Lev.distinct(51) insertE lev_next.simps(2) lev_next.simps(3) singletonD) 
  then have b2: "(u,v) ∉ (rE S)^^2" by (metis Suc_1 relpow_1 relpow_Suc_D2)
  have "⋀ u1 u2. (u,u1) ∈ (rE S) ∧ (u1,u2) ∈ (rE S) ∧ (u2,v) ∈ (rE S) ⟹ False"
    using a1 a2 lem_rE_succ_lev
    by (metis Lev.distinct(57) Lev.distinct(59) insertE lev_next.simps(2) lev_next.simps(3) lev_next.simps(4) singletonD)
  then have b3: "(u,v) ∉ (rE S)^^3" using lem_rel_pow3[of u v "rE S"] by blast
  have "⋀ u1 u2 u3. (u,u1) ∈ (rE S) ∧ (u1,u2) ∈ (rE S) ∧ (u2,u3) ∈ (rE S) ∧ (u3,v) ∈ (rE S) ⟹ False"
    using a1 a2 lem_rE_succ_lev
    by (metis Lev.distinct(63) Lev.distinct(65) insertE lev_next.simps(2) lev_next.simps(3) lev_next.simps(4) lev_next.simps(5) singletonD)
  then have b4: "(u,v) ∉ (rE S)^^4" using lem_rel_pow4[of u v "rE S"] by blast
  have "⋀ u1 u2 u3 u4. (u,u1) ∈ (rE S) ∧ (u1,u2) ∈ (rE S) ∧ (u2,u3) ∈ (rE S) ∧ (u3,u4) ∈ (rE S) ∧ (u4,v) ∈ (rE S) ⟹ False"
    using a1 a2 lem_rE_succ_lev
    by (metis Lev.distinct(67) Lev.distinct(69) insertE lev_next.simps(2) lev_next.simps(3) lev_next.simps(4) lev_next.simps(5) lev_next.simps(6) singletonD)
  then have b5: "(u,v) ∉ (rE S)^^5" using lem_rel_pow5[of u v "rE S"] by blast
  have "n = 0 ∨ n = 1 ∨ n = 2 ∨ n = 3 ∨ n = 4 ∨ n = 5" using a3 by force
  then show ?thesis using b0 b1 b2 b3 b4 b5 by blast
qed

lemma lem_rE_notLD2:
fixes S::"'U set" and r0 r1::"('U rD) rel"
assumes a0: "¬ |S| ≤o |UNIV::nat set|" and a1: "LD2 (rE S) r0 r1"
shows "False"
proof -
  obtain x0::'U where b0: "x0 ∈ S" using a0
    by (metis all_not_in_conv card_of_mono1 card_of_singl_ordLeq empty_subsetI 
        finite.emptyI infinite_UNIV_char_0 ordLeq_transitive)
  obtain u::"'U rD" where b1: "u = (𝗅0, {}, {}, {})" by blast
  obtain v1::"'U rD" where b2: "v1 = (𝗅1, {}, {}, {})" by blast
  obtain v2::"'U rD" where b3: "v2 = (𝗅1, {x0}, {}, {})" by blast
  have "levrd u = 𝗅0" using b1 by simp
  then have "(u,v1) ∉ r0 ∧ (u,v2) ∉ r0" using a0 a1 lem_rE_one[of S r0 r1 u ] by blast
  moreover have "(u,v1) ∈ (rE S) ∧ (u,v2) ∈ (rE S)" using b0 b1 b2 b3 unfolding rE_def rC_def by simp
  ultimately have "(u,v1) ∈ r1 ∧ (u,v2) ∈ r1" using a1 unfolding LD2_def by blast
  then have "jn11 r0 r1 v1 v2" using a1 unfolding LD2_def by blast
  then obtain b' b'' c' c'' d where 
       b4: "(v1, b') ∈ r0^* ∧ (b', b'') ∈ r1^= ∧ (b'', d) ∈ r0^*"
   and b5: "(v2, c') ∈ r0^* ∧ (c', c'') ∈ r1^= ∧ (c'', d) ∈ r0^*" unfolding jn11_def by blast
  have b6: "⋀ v v'::'U rD. levrd v ∈ {𝗅1, 𝗅3} ∧ (v, v') ∈ r0^* ⟹ (v,v') ∈ r0^="
  proof -
    fix v v'::"'U rD"
    assume c1: "levrd v ∈ {𝗅1, 𝗅3} ∧ (v, v') ∈ r0^*"
    then obtain k1 where c2: "(v, v') ∈ r0^^k1" using rtrancl_imp_relpow by blast
    have "k1 ≥ 2 ⟶ False"
    proof
      assume "k1 ≥ 2"
      then obtain k where "k1 = 2 + k" using le_Suc_ex by blast
      then obtain w' where "(v, w') ∈ r0^^2" using c2 relpow_add[of 2 k r0] by fastforce
      then obtain w w' where "(v, w) ∈ r0 ∧ (w, w') ∈ r0" by (metis One_nat_def numeral_2_eq_2 relpow_1 relpow_Suc_E)
      moreover then have "(v, w) ∈ (rE S)" using a1 unfolding LD2_def by blast
      moreover then have "levrd w ∈ {𝗅2, 𝗅4}" using c1 unfolding rE_def by force
      ultimately show "False" using a0 a1 lem_rE_one by blast
    qed
    then have "k1 = 0 ∨ k1 = 1" by (simp add: less_2_cases)
    then show "(v, v') ∈ r0^=" using c2 by force
  qed
  then have b7: "(v1, b') ∈ r0^= ∧ (v2, c') ∈ r0^=" using b2 b3 b4 b5 by simp
  have b8: "levrd d ∈ {𝗅7, 𝗅8}"
  proof -
    have "r0 ⊆ (rE S) ∧ r1 ⊆ (rE S)" using a1 unfolding LD2_def by blast
    then have "r0^* ⊆ (rE S)^* ∧ r1^= ⊆ (rE S)^*" using rtrancl_mono by blast
    then have "(v1, b') ∈ (rE S)^* ∧ (b', b'') ∈ (rE S)^* ∧ (b'', d) ∈ (rE S)^*" 
          and "(v2, c') ∈ (rE S)^* ∧ (c', c'') ∈ (rE S)^* ∧ (c'', d) ∈ (rE S)^*" using b4 b5 by blast+
    then have e1: "(v1,d) ∈ (rE S)^* ∧ (v2,d) ∈ (rE S)^*" by force
    have "⋀ v v'::'U rD. levrd v = 𝗅1 ⟶ (v,v') ∈ (rE S)^* ⟶ v ≠ v' ⟶ levrd v' ≠ 𝗅1"
    proof (intro impI)
      fix v v'::"'U rD"
      assume d1: "levrd v = 𝗅1" and d2: "(v,v') ∈ (rE S)^*" and d3: "v ≠ v'"
      moreover then obtain k where "(v,v') ∈ (rE S)^^k" using rtrancl_imp_relpow by blast
      ultimately obtain k' where "(v,v') ∈ (rE S)^^(Suc k')" by (cases k, force+)
      then obtain v'' where "(v,v'') ∈ (rE S) ∧ (v'',v') ∈ (rE S)^^k'" by (meson relpow_Suc_D2)
      then have "levrd v'' = 𝗅2 ∧ (v'',v') ∈ (rE S)^*" using d1 lem_rE_succ_lev[of v v''] relpow_imp_rtrancl by force
      moreover have "lev_next ` {𝗅2, 𝗅3, 𝗅4, 𝗅5, 𝗅6, 𝗅7, 𝗅8} ⊆ {𝗅2, 𝗅3, 𝗅4, 𝗅5, 𝗅6, 𝗅7, 𝗅8}" by simp
      ultimately have "levrd v' ∈ {𝗅2, 𝗅3, 𝗅4, 𝗅5, 𝗅6, 𝗅7, 𝗅8}" using lem_rE_levset_inv[of v'' v' S "{𝗅2, 𝗅3, 𝗅4, 𝗅5, 𝗅6, 𝗅7, 𝗅8}"] by simp
      then show "levrd v' ≠ 𝗅1" by force
    qed
    then have "(v1,v2) ∉ (rE S)^*" and "(v2,v1) ∉ (rE S)^*" using b2 b3 by fastforce+
    then show "levrd d ∈ {𝗅7, 𝗅8}" using e1 lem_rE_jn2 by blast
  qed
  then have b9: "∀ n ≤ 5. (v1,d) ∉ (rE S)^^n ∧ (v2,d) ∉ (rE S)^^n" using b2 b3 lem_rE_l1_l78_dist[of _ d] by simp
  have b10: "levrd b'' = 𝗅2"
  proof -
    have c1: "v1 = b' ∨ (v1,b') ∈ (rE S)" using b7 a1 unfolding LD2_def by blast
    then have "levrd b' ∈ {𝗅1, 𝗅2}" using b2 lem_rE_succ_lev[of v1 b'] by force
    moreover have c2: "b' = b'' ∨ (b',b'') ∈ (rE S)" using b4 a1 unfolding LD2_def by blast
    ultimately have "levrd b'' ∈ {𝗅1, 𝗅2, 𝗅3}" using lem_rE_succ_lev[of b' b''] by force
    moreover have "levrd b'' ∈ {𝗅1, 𝗅3} ⟶ False"
    proof
      assume "levrd b'' ∈ {𝗅1, 𝗅3}"
      then have "(b'',d) ∈ r0^=" using b4 b6 by blast
      then have d1: "b'' = d ∨ (b'', d) ∈ (rE S)" using a1 unfolding LD2_def by blast
      have "(v1,d) ∈ (rE S)^^0 ∨ (v1,d) ∈ (rE S)^^1 ∨ (v1,d) ∈ (rE S)^^2 ∨ (v1,d) ∈ (rE S)^^3"
        using c1 c2 d1 lem_rel_pow2fw[of _ _ "rE S"] lem_rel_pow3fw[of _ _ "rE S"] by (metis relpow_0_I relpow_1)
      then show "False" using b9
        by (meson le0 numeral_le_iff one_le_numeral semiring_norm(68) semiring_norm(72) semiring_norm(73))
    qed
    ultimately show "levrd b'' = 𝗅2" by blast
  qed
  then have "b'' ≠ d" using b8 by force
  then obtain t where b11: "(b'',t) ∈ r0 ∧ (t, d) ∈ r0^*" using b4 by (meson converse_rtranclE)
  then have b12: "(b'',t) ∈ (rE S)" using a1 unfolding LD2_def by blast
  then have "levrd t = 𝗅3" using b10 a1 lem_rE_succ_lev[of b'' t S] unfolding LD2_def by simp
  then have "(t,d) ∈ r0^=" using b11 b6 by blast
  then have b13: "t = d ∨ (t,d) ∈ (rE S)" using a1 unfolding LD2_def by blast
  have b14: "v1 = b' ∨ (v1,b') ∈ (rE S)" using b7 a1 unfolding LD2_def by blast
  moreover have b15: "b' = b'' ∨ (b',b'') ∈ (rE S)" using b4 a1 unfolding LD2_def by blast
  ultimately have "(v1,b'') ∈ (rE S)^^0 ∨ (v1,b'') ∈ (rE S)^^1 ∨ (v1,b'') ∈ (rE S)^^2"
    using lem_rel_pow2fw[of _ _ "rE S"] by (metis relpow_0_I relpow_1)
  then have "(v1,t) ∈ (rE S)^^1 ∨ (v1,t) ∈ (rE S)^^2 ∨ (v1,t) ∈ (rE S)^^3" using b12 b14 b15
   lem_rel_pow2fw[of _ _ "rE S"] lem_rel_pow3fw[of _ _ "rE S"] by (metis relpow_1)
  moreover have "(v1,t) ∈ (rE S)^^1 ⟶ (v1,d) ∈ (rE S)^^1 ∨ (v1,d) ∈ (rE S)^^2" using b13 lem_rel_pow2fw by fastforce
  moreover have "(v1,t) ∈ (rE S)^^2 ⟶ (v1,d) ∈ (rE S)^^2 ∨ (v1,d) ∈ (rE S)^^3" using b13 relpow_Suc_I by fastforce
  moreover have "(v1,t) ∈ (rE S)^^3 ⟶ (v1,d) ∈ (rE S)^^3 ∨ (v1,d) ∈ (rE S)^^4" using b13 relpow_Suc_I by fastforce
  ultimately have "∃ n ∈ {1,2,3,4}. (v1,d) ∈ (rE S)^^n" by blast
  moreover have "∀ n ∈ {1,2,3,4}::nat set. n ≤ 5" by simp
  ultimately show "False" using b9 by blast
qed

lemma lem_rE_dominv:
fixes S::"'U set"
assumes "¬ finite S"
shows "u ∈ Domain (rE S) ⟹ (u,v) ∈ (rE S)^* ⟹ v ∈ Domain (rE S)"
  using assms lem_rE_domfield unfolding Field_def by (metis Range.RangeI UnCI rtranclE)

lemma lem_rE_next:
fixes S::"'U set"
assumes "¬ finite S" and "u ∈ Domain (rE S)" 
shows "∃ v. (u,v) ∈ (rE S) ∧ v ∈ Domain (rE S) ∧ levrd v = (lev_next (levrd u))"
proof -
  obtain u' where b1: "(u,u') ∈ (rE S)" using assms by blast
  obtain n A B C where b2: "u = (n,A,B,C)" using prod_cases4 by blast
  obtain n' A' B' C' where b3: "u' = (n',A',B',C')" using prod_cases4 by blast
  have b4: "rP n A B C n' A' B' C' ∧ rC S A B C ∧ rC S A' B' C'" using b1 b2 b3 unfolding rE_def by blast
  moreover then have "A ⊆ S" unfolding rC_def by blast
  moreover then have b4': "∃A2⊆S. A ⊂ A2 ∧ finite A2" 
    using b4 assms lem_rP_inv lem_infset_finext[of S A] by metis
  ultimately have "(∃ A1 B1 C1 n2 A2 B2 C2. rP n A B C (lev_next n) A1 B1 C1 ∧ rC S A1 B1 C1
                               ∧ rP (lev_next n) A1 B1 C1 n2 A2 B2 C2 ∧ rC S A2 B2 C2)" 
    apply (cases n) 
    unfolding rC_def by auto+
  then obtain A1 B1 C1 n2 A2 B2 C2 where 
    "rP n A B C (lev_next n) A1 B1 C1 ∧ rC S A1 B1 C1 ∧ rP (lev_next n) A1 B1 C1 n2 A2 B2 C2 ∧ rC S A2 B2 C2" by blast
  moreover obtain v where "v = ((lev_next n), A1, B1, C1)" by blast
  ultimately have "(u,v) ∈ (rE S) ∧ v ∈ Domain (rE S) ∧ levrd v = (lev_next (levrd u))"
    using b2 b4 unfolding rE_def by force
  then show ?thesis by blast
qed

lemma lem_rE_reachl8:
fixes S::"'U set"
assumes "¬ finite S" and "u ∈ Domain (rE S)"
shows "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8"
proof -
  have "levrd u = 𝗅8 ⟶ ?thesis" using assms by blast
  moreover have b0: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅7 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅7"
    moreover then have "(lev_next (levrd u)) = 𝗅8" by force
    ultimately obtain v where "(u,v) ∈ (rE S) ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using assms lem_rE_next by metis
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b1: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅6 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅6"
    moreover then have "(lev_next (levrd u)) = 𝗅7" by force
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅7" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b0 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force    
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b2: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅5 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅5"
    moreover then have "(lev_next (levrd u)) = 𝗅6" by simp
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅6" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b1 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b3: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅4 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅4"
    moreover then have "(lev_next (levrd u)) = 𝗅5" by simp
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅5" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b2 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b4: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅3 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅3"
    moreover then have "(lev_next (levrd u)) = 𝗅4" by simp
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅4" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b3 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b5: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅2 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅2"
    moreover then have "(lev_next (levrd u)) = 𝗅3" by simp
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅3" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b4 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b6: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅1 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅1"
    moreover then have "(lev_next (levrd u)) = 𝗅2" by simp
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅2" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b5 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  moreover have b7: "⋀ u::'U rD. u ∈ Domain (rE S) ⟹ levrd u = 𝗅0 ⟹ (∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8)"
  proof -
    fix u::"'U rD"
    assume "u ∈ Domain (rE S)" and "levrd u = 𝗅0"
    moreover then have "(lev_next (levrd u)) = 𝗅1" by simp
    ultimately obtain v' where "(u,v') ∈ (rE S) ∧ v' ∈ Domain (rE S) ∧ levrd v' = 𝗅1" using assms lem_rE_next by metis
    moreover then obtain v where "(v',v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" using b6 by blast
    ultimately have "(u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by force
    then show "∃ v. (u,v) ∈ (rE S)^* ∧ v ∈ Domain (rE S) ∧ levrd v = 𝗅8" by blast
  qed
  ultimately show ?thesis using assms by (meson lev_next.cases)
qed

lemma lem_rE_jn:
fixes S::"'U set"
assumes a0: "¬ finite S" and a1: "u1 ∈ Domain (rE S)" and a2: "u2 ∈ Domain (rE S)"
shows "∃ t. (u1,t) ∈ (rE S)^* ∧ (u2,t) ∈ (rE S)^*"
proof -
  obtain v1 where b1: "(u1,v1) ∈ (rE S)^*" and b2: "v1 ∈ Domain (rE S) ∧ levrd v1 = 𝗅8" using a0 a1 lem_rE_reachl8 by blast
  obtain v2 where b3: "(u2,v2) ∈ (rE S)^*" and b4: "v2 ∈ Domain (rE S) ∧ levrd v2 = 𝗅8" using a0 a2 lem_rE_reachl8 by blast
  obtain n1 A1 B1 C1 where b5: "v1 = (n1,A1,B1,C1)" using prod_cases4 by blast
  obtain n2 A2 B2 C2 where b6: "v2 = (n2,A2,B2,C2)" using prod_cases4 by blast
  have b7: "n1 = 𝗅8 ∧ A1 = B1 ∧ A1 = C1 ∧ finite A1 ∧ A1 ⊆ S" using b5 b2 unfolding rE_def rC_def by force
  have b8: "n2 = 𝗅8 ∧ A2 = B2 ∧ A2 = C2 ∧ finite A2 ∧ A2 ⊆ S" using b6 b4 unfolding rE_def rC_def by force 
  have "finite (A1 ∪ A2) ∧ A1 ∪ A2 ⊆ S" using b7 b8 by blast
  then obtain A3 where "A3 ⊆ S ∧ A1 ∪ A2 ⊂ A3 ∧ finite A3" using a0 lem_infset_finext[of S "A1 ∪ A2"] by blast
  moreover obtain t where "t = (𝗅7, A3, A3, A3)" by blast
  ultimately have "(v1, t) ∈ (rE S) ∧ (v2, t) ∈ (rE S)" using b5 b6 b7 b8 unfolding rE_def rC_def by force
  then have "(u1,t) ∈ (rE S)^* ∧ (u2,t) ∈ (rE S)^*" using b1 b3 by force
  then show ?thesis by blast
qed

lemma lem_rE_confl:
fixes S::"'U set"
assumes "¬ finite S"
shows "confl_rel (rE S)"
proof -
  have "∀ a b c::'U rD. (a,b) ∈ (rE S)^* ⟶ (a,c) ∈ (rE S)^* ⟶ (∃ d. (b,d) ∈ (rE S)^* ∧ (c,d) ∈ (rE S)^*)"
  proof (intro allI impI)
    fix a b c::"'U rD"
    assume c1: "(a,b) ∈ (rE S)^*" and c2: "(a,c) ∈ (rE S)^*"
    show "∃ d. (b,d) ∈ (rE S)^* ∧ (c,d) ∈ (rE S)^*"
    proof (cases "a ∈ Domain (rE S)")
      assume "a ∈ Domain (rE S)"
      then have "b ∈ Domain (rE S) ∧ c ∈ Domain (rE S)" using c1 c2 assms lem_rE_dominv by blast
      then obtain d where "(b,d) ∈ (rE S)^* ∧ (c,d) ∈ (rE S)^*" using assms lem_rE_jn by blast
      then show ?thesis by blast
    next
      assume "a ∉ Domain (rE S)"
      then have "a = b ∧ a = c" using c1 c2 by (meson Not_Domain_rtrancl)
      then show ?thesis by blast
    qed
  qed
  then show ?thesis unfolding confl_rel_def by blast
qed

lemma lem_rE_dc3dc2:
fixes S::"'U set"
assumes "¬ |S| ≤o |UNIV::nat set|"
shows "confl_rel (rE S) ∧ (¬ DCR2 (rE S))"
proof (intro conjI)
  have "¬ finite S" using assms by (meson card_of_Well_order infinite_iff_card_of_nat ordLeq_total)
  then show "confl_rel (rE S)" using lem_rE_confl by blast
next
  show "¬ DCR2 (rE S)" using assms lem_rE_notLD2 unfolding DCR2_def by blast
qed

lemma lem_rE_cardbnd:
fixes S::"'U set"
assumes "¬ finite S"
shows "|rE S| ≤o |S|"
proof -
  obtain L where b1: "L = (UNIV::Lev set)" by blast
  obtain F where b2: "F = { A. A ⊆ S ∧ finite A }" by blast
  obtain D where b3: "D = (L × (F × (F × F)))" by blast
  have "∀ u v. (u,v) ∈ rE S ⟶ u ∈ D ∧ v ∈ D"
  proof (intro allI impI)
    fix u v
    assume "(u,v) ∈ rE S"
    then obtain n A B C n' A' B' C' 
      where "u = (n,A,B,C) ∧ v = (n',A',B',C') ∧ rC S A B C ∧ rC S A' B' C'
        ∧ rP n A B C n' A' B' C'" unfolding rE_def by blast
    moreover then have "n ∈ L ∧ A ∈ F ∧ B ∈ F ∧ C ∈ F ∧ n' ∈ L ∧ A' ∈ F ∧ B' ∈ F ∧ C' ∈ F" 
      using b1 b2 lem_rP_inv unfolding rC_def by fast
    ultimately show "u ∈ D ∧ v ∈ D" using b3 by blast
  qed
  then have "rE S ⊆ D × D" by force
  then have "|rE S| ≤o |D × D|" by simp
  moreover have "|D × D| ≤o |S|"
  proof -
    have "F = Fpow S" using b2 unfolding Fpow_def by simp
    then have c1: "|F| =o |S|" using assms by simp
    then have "|F × F| =o |F| ∧ ¬ finite F" using assms by simp
    then have "|F| ≤o |F| ∧ |F × F| ≤o |F| ∧ ¬ finite F" using ordIso_iff_ordLeq by force
    then have c2: "|F × (F × F)| ≤o |S|" using c1 card_of_Times_ordLeq_infinite ordLeq_ordIso_trans by blast
    have "L ⊆ {𝗅0,𝗅1,𝗅2,𝗅3,𝗅4,𝗅5,𝗅6,𝗅7,𝗅8}"
    proof
      fix l
      assume "l ∈ L"
      show "l ∈ {𝗅0,𝗅1,𝗅2,𝗅3,𝗅4,𝗅5,𝗅6,𝗅7,𝗅8}" by (cases l, simp+)
    qed
    moreover have "finite {𝗅0,𝗅1,𝗅2,𝗅3,𝗅4,𝗅5,𝗅6,𝗅7,𝗅8}" by simp
    ultimately have "finite L" using finite_subset by blast
    then have "|L| ≤o |S|" using assms ordLess_imp_ordLeq by force
    then have "|D| ≤o |S|" using b3 c2 assms card_of_Times_ordLeq_infinite by blast
    then show ?thesis using assms card_of_Times_ordLeq_infinite by blast
  qed
  ultimately show "|rE S| ≤o |S|" using ordLeq_transitive by blast
qed

lemma lem_fmap_rel:
fixes f r s a0 b0
assumes a1: "(a0, b0) ∈ r^*" and a2: "∀ a b. (a,b) ∈ r ⟶ (f a, f b) ∈ s"
shows "(f a0, f b0) ∈ s^*"
proof -
  have "⋀ n. ∀ a b. (a,b) ∈ r^^n ⟶ (f a, f b) ∈ s^*"
  proof -
    fix n0
    show "∀ a b. (a,b) ∈ r^^n0 ⟶ (f a, f b) ∈ s^*"
    proof (induct n0)
      show "∀ a b. (a,b) ∈ r^^0 ⟶ (f a, f b) ∈ s^*" by simp
    next
      fix n
      assume "∀ a b. (a,b) ∈ r^^n ⟶ (f a, f b) ∈ s^*"
      then show "∀ a b. (a,b) ∈ r^^(Suc n) ⟶ (f a, f b) ∈ s^*" using a2 by force
    qed
  qed
  then show ?thesis using a1 rtrancl_power by blast
qed

lemma lem_fmap_confl:
fixes r::"'a rel" and f::"'a ⇒ 'b"
assumes a1: "inj_on f (Field r)" and a2: "confl_rel r"
shows "confl_rel {(u,v). ∃ a b. u = f a ∧ v = f b ∧ (a,b) ∈ r}"
proof -
  obtain rA where q1: "rA = {(u,v). ∃ a b. u = f a ∧ v = f b ∧ (a,b) ∈ r}" by blast
  then have q2: "∀a b. (a, b) ∈ r ⟶ (f a, f b) ∈ rA" by blast
  have q3: "Field rA ⊆ f`(Field r)" using q1 unfolding Field_def by blast
  obtain g where q4: "g = inv_into (Field r) f" by blast
  then have q5: "∀ x ∈ Field r. g (f x) = x" using a1 by simp
  have q6: "∀ u v. (u,v) ∈ rA ⟶ (g u, g v) ∈ r"
  proof (intro allI impI)
    fix u v
    assume "(u,v) ∈ rA"
    then obtain a b where "u = f a ∧ v = f b ∧ (a,b) ∈ r" using q1 by blast
    moreover then have "a ∈ Field r ∧ b ∈ Field r" unfolding Field_def by blast
    ultimately show "(g u, g v) ∈ r" using q5 by force
  qed
  have "∀u ∈ Field rA. ∀ v ∈ Field rA. ∀ w ∈ Field rA. 
    (u,v) ∈ rA^* ∧ (u,w) ∈ rA^* ⟶ (∃ t ∈ Field rA. (v,t) ∈ rA^* ∧ (w,t) ∈ rA^*)"
  proof (intro ballI impI)
    fix u v w
    assume c1: "u ∈ Field rA" and c2: "v ∈ Field rA" and c3: "w ∈ Field rA" 
       and c4: "(u,v) ∈ rA^* ∧ (u,w) ∈ rA^*"
    then have "(g u, g v) ∈ r^* ∧ (g u, g w) ∈ r^*" using q6 lem_fmap_rel[of u _ rA g r] by blast
    then obtain d where c5: "(g v, d) ∈ r^* ∧ (g w, d) ∈ r^*" using a2 unfolding confl_rel_def by blast
    moreover have c6: "g v ∈ Field r ∧ g w ∈ Field r" using c2 c3 q3 q5 by force
    ultimately have "d ∈ Field r" using lem_rtr_field by fastforce
    have "v = f (g v) ∧ w = f (g w)" using c2 c3 q3 q4 a1 by force
    moreover have "(f (g v), f d) ∈ rA^* ∧ (f (g w), f d) ∈ rA^*" 
      using c5 q2 lem_fmap_rel[of _ d r f rA] by blast
    ultimately have "(v, f d) ∈ rA^* ∧ (w, f d) ∈ rA^*" by simp
    moreover then have "f d ∈ Field rA" using c2 lem_rtr_field by fastforce
    ultimately show "∃ t ∈ Field rA. (v,t) ∈ rA^* ∧ (w,t) ∈ rA^*" by blast
  qed
  then show ?thesis using q1 lem_confl_field by blast
qed

lemma lem_fmap_dcn:
fixes r::"'a rel" and f::"'a ⇒ 'b"
assumes a1: "inj_on f (Field r)" and a2: "DCR n r"
shows "DCR n {(u,v). ∃ a b. u = f a ∧ v = f b ∧ (a,b) ∈ r}"
proof -
  obtain rA where q1: "rA = {(u,v). ∃ a b. u = f a ∧ v = f b ∧ (a,b) ∈ r}" by blast
  have q2: "∀ a ∈ Field r. ∀ b ∈ Field r. (a,b) ∈ r ⟷ (f a, f b) ∈ rA" 
    using a1 q1 unfolding Field_def inj_on_def by blast
  have q3: "Field rA ⊆ f`(Field r)" using q1 unfolding Field_def by blast  
  obtain g::"nat ⇒ 'a rel" where b1: "DCR_generating g" 
         and b2: "r = ⋃ { r'. ∃ α'. α' < n ∧ r' = g α' }" using a2 unfolding DCR_def by blast
  obtain gA::"nat ⇒ 'b rel" 
    where b3: "gA = (λ α. if α < n then {(x,y). ∃ a b. x = f a ∧ y = f b ∧ (a,b) ∈ g α } else {})" by blast
  have "∀α β u v w. (u, v) ∈ gA α ∧ (u, w) ∈ gA β ⟶
       (∃v' v'' w' w'' e. (v, v', v'', e) ∈ 𝔇 gA α β ∧ (w, w', w'', e) ∈ 𝔇 gA β α)"
  proof (intro allI impI)
    fix α β u v w
    assume c1: "(u, v) ∈ gA α ∧ (u, w) ∈ gA β"
    obtain a b where c2: "α < n ∧ u = f a ∧ v = f b ∧ (a,b) ∈ g α" using c1 b3 by (cases "α < n", force+)
    obtain a' c where c3: "β < n ∧ u = f a' ∧ w = f c ∧ (a',c) ∈ g β" using c1 b3 by (cases "β < n", force+)
    have "(a,b) ∈ r ∧ (a',c) ∈ r" using c2 c3 b2 by blast
    then have "a' = a" using c2 c3 a1 unfolding inj_on_def Field_def by blast
    then have "(a,b) ∈ g α ∧ (a,c) ∈ g β" using c2 c3 by blast
    then obtain b' b'' c' c'' d where c4: "(b, b', b'', d) ∈ 𝔇 g α β ∧ (c, c', c'', d) ∈ 𝔇 g β α" 
      using b1 unfolding DCR_generating_def by blast
    have c5: "⋀ α'. α' < n ⟹ ∀ a0 b0. (a0,b0) ∈ 𝔏1 g α' ⟶ (f a0, f b0) ∈ 𝔏1 gA α'"
    proof (intro allI impI)
      fix α' a0 b0
      assume d1: "α' < n" and "(a0,b0) ∈ 𝔏1 g α'"
      then obtain α'' where "(a0,b0) ∈ g α'' ∧ α'' < α'" unfolding 𝔏1_def by blast
      moreover then have "(f a0, f b0) ∈ gA α''" using d1 c2 b3 by force
      ultimately show "(f a0, f b0) ∈ 𝔏1 gA α'" using c2 b3 unfolding 𝔏1_def by blast
    qed
    have c6: "⋀ α' a0 b0. α' < n ⟹ (a0,b0) ∈ (g α')^= ⟶ (f a0, f b0) ∈ (gA α')^=" using b3 by force
    have c7: "⋀ α' β'. α' < n ⟹ β' < n ⟹ ∀ a0 b0. (a0,b0) ∈ 𝔏v g α' β' ⟶ (f a0, f b0) ∈ 𝔏v gA α' β'"
    proof (intro allI impI)
      fix α' β' a0 b0
      assume d1: "α' < n" and d2: "β' < n" and "(a0,b0) ∈ 𝔏v g α' β'"
      then obtain α'' where "(a0,b0) ∈ g α'' ∧ (α'' < α' ∨ α'' < β')" unfolding 𝔏v_def by blast
      moreover then have "(f a0, f b0) ∈ gA α''" using d1 d2 c2 b3 by force
      ultimately show "(f a0, f b0) ∈ 𝔏v gA α' β'" using c2 b3 unfolding 𝔏v_def by blast
    qed
    have "(v, f b') ∈ (𝔏1 gA α)^*" using c2 c4 c5[of α] lem_fmap_rel[of b b'] unfolding 𝔇_def by blast
    moreover have "(f b', f b'') ∈ (gA β)^=" using c3 c4 c6 unfolding 𝔇_def by blast
    moreover have "(f b'', f d) ∈ (𝔏v gA α β)^*" using c2 c3 c4 c7[of α β] lem_fmap_rel[of b'' d] unfolding 𝔇_def by blast
    moreover have "(w, f c') ∈ (𝔏1 gA β)^*" using c3 c4 c5[of β] lem_fmap_rel[of c c'] unfolding 𝔇_def by blast
    moreover have "(f c', f c'') ∈ (gA α)^=" using c2 c4 c6 unfolding 𝔇_def by blast
    moreover have "(f c'', f d) ∈ (𝔏v gA β α)^*" using c2 c3 c4 c7[of β α] lem_fmap_rel[of c'' d] unfolding 𝔇_def by blast
    ultimately show "∃v' v'' w' w'' e. (v, v', v'', e) ∈ 𝔇 gA α β ∧ (w, w', w'', e) ∈ 𝔇 gA β α"
      unfolding 𝔇_def by blast
  qed
  then have "DCR_generating gA" unfolding DCR_generating_def by blast
  moreover have "rA = ⋃ { r'. ∃ α'. α' < n ∧ r' = gA α'}"
  proof
    show "rA ⊆ ⋃ { r'. ∃ α'. α' < n ∧ r' = gA α'}"
    proof
      fix p
      assume "p ∈ rA"
      then obtain x y where d1: "p = (x,y) ∧ p ∈ rA" by force
      moreover then obtain a b where d2: "x = f a ∧ y = f b ∧ a ∈ Field r ∧ b ∈ Field r" 
        using q3 unfolding Field_def by blast
      ultimately have "(a,b) ∈ r" using q2 by blast
      then obtain α' where "α' < n ∧ (a,b) ∈ g α'" using b2 by blast
      then have "α' < n ∧ (x,y) ∈ gA α'" using d2 b3 by force
      then show "p ∈ ⋃{r'. ∃α'<n. r' = gA α'}" using d1 by blast
    qed
  next
    show "⋃ { r'. ∃ α'. α' < n ∧ r' = gA α'} ⊆ rA"
    proof
      fix p
      assume "p ∈ ⋃ { r'. ∃ α'. α' < n ∧ r' = gA α'}"
      then obtain α' where d1: "α' < n ∧ p ∈ gA α'" by blast
      then obtain x y where d2: "p = (x,y) ∧ p ∈ gA α'" by force
      then obtain a b where "x = f a ∧ y = f b ∧ (a,b) ∈ g α'" using d1 b3 by force
      moreover then have "(a,b) ∈ r" using d1 b2 by blast
      ultimately show "p ∈ rA" using d2 q2 unfolding Field_def by blast
    qed
  qed
  ultimately have "DCR n rA" unfolding DCR_def by blast
  then show ?thesis using q1 by blast
qed

lemma lem_not_dcr2: 
assumes "cardSuc |UNIV::nat set| ≤o |UNIV::'U set|"
shows "∃ r::'U rel. confl_rel r ∧ |r| ≤o cardSuc |UNIV::nat set| ∧ (¬ DCR2 r)"
proof -
  obtain A where b1: "A = (UNIV::'U set)" by blast
  obtain S where b2: "S ⊆ A ∧ |S| =o cardSuc |UNIV::nat set|"
    using b1 assms
      by (smt Card_order_ordIso2 Field_card_of cardSuc_Card_order card_of_Field_ordIso 
          card_of_card_order_on internalize_ordLeq ordIso_symmetric ordIso_transitive)
  then have "¬ ( |S| ≤o |UNIV::nat set| )" by (simp add: cardSuc_ordLess_ordLeq ordIso_iff_ordLeq)
  moreover then have "¬ finite S" by (meson card_of_Well_order infinite_iff_card_of_nat ordLeq_total)
  moreover obtain s where b3: "s = (rE S)" by blast
  ultimately have b4: "confl_rel s ∧ ¬ DCR2 s ∧ |s| ≤o |S|" using lem_rE_dc3dc2 lem_rE_cardbnd by blast
  obtain B where b5: "B = Field s" by blast
  obtain C::"'U set" where b6: "C = UNIV" by blast
  then have "cardSuc |UNIV::nat set| ≤o |C|" using assms by blast
  moreover have b6': "|s| ≤o cardSuc |UNIV::nat set|" using b2 b4 ordLeq_ordIso_trans by blast
  ultimately have "|s| ≤o |C|" using ordLeq_transitive by blast
  moreover have b6'': "¬ finite (Field s) ⟶ |Field s| =o |s|" using lem_fin_fl_rel lem_rel_inf_fld_card by blast
  ultimately have "¬ finite (Field s) ⟶ |Field s| ≤o |C|" using ordIso_ordLeq_trans by blast
  moreover have "¬ finite C" using b6 assms ordLeq_finite_Field by fastforce
  moreover then have "finite (Field s) ⟶ |Field s| ≤o |C|" using ordLess_imp_ordLeq by force
  ultimately have "|B| ≤o |C|" using b5 by blast
  then obtain f where b7: "f`B ⊆ C ∧ inj_on f B" by (meson card_of_ordLeq) 
  moreover obtain g where b8: "g = inv_into B f" by blast
  ultimately have b9: "∀ x ∈ B. g (f x) = x" by simp
  obtain r where b10: "r = {(a,b). ∃ x y. a = f x ∧ b = f y ∧ (x,y) ∈ s}" by blast
  have "s ⊆ {(x,y). ∃ a b. x = g a ∧ y = g b ∧ (a,b) ∈ r}"
  proof
    fix p
    assume "p ∈ s"
    then obtain x y where "p = (x,y) ∧ (x,y) ∈ s" by (cases p, blast)
    moreover then have "(f x, f y) ∈ r ∧ x ∈ B ∧ y ∈ B" using b5 b10 unfolding Field_def by blast
    moreover then have "x = g (f x) ∧ y = g (f y)" using b9 by simp
    ultimately show "p ∈ {(x,y). ∃ a b. x = g a ∧ y = g b ∧ (a,b) ∈ r}" using b9 by blast
  qed
  moreover have "{(x,y). ∃ a b. x = g a ∧ y = g b ∧ (a,b) ∈ r} ⊆ s"
  proof
    fix p
    assume "p ∈ {(x,y). ∃ a b. x = g a ∧ y = g b ∧ (a,b) ∈ r}"
    then obtain a b where "p = (g a, g b) ∧ (a,b) ∈ r" by blast
    moreover then obtain x y where "a = f x ∧ b = f y ∧ (x,y) ∈ s" using b10 by blast
    moreover then have "x ∈ B ∧ y ∈ B" using b5 unfolding Field_def by blast
    ultimately show "p ∈ s" using b9 by force
  qed
  ultimately have b11: "s = {(x,y). ∃ a b. x = g a ∧ y = g b ∧ (a,b) ∈ r}" by blast
  have "inj_on g (f`B)" using b8 inj_on_inv_into[of "f`B" f B] by blast
  moreover have b12: "Field r ⊆ f`B" 
  proof
    fix c
    assume "c ∈ Field r"
    then obtain a b where "(a,b) ∈ r ∧ (c = a ∨ c = b)" unfolding Field_def by blast
    moreover then obtain x y where "a = f x ∧ b = f y ∧ (x,y) ∈ s" using b10 by blast
    moreover then have "x ∈ B ∧ y ∈ B" using b5 unfolding Field_def by blast
    ultimately show "c ∈ f ` B" by blast
  qed
  ultimately have "inj_on g (Field r)" using Fun.subset_inj_on by blast
  moreover have "¬ DCR 2 s" using b4 lem_dc2_to_d2 by blast
  ultimately have "¬ DCR 2 r" using b11 lem_fmap_dcn[of g r 2] by blast
  then have "¬ DCR2 r" using lem_d2_to_dc2 by blast
  moreover have "confl_rel r" using b4 b5 b7 b10 lem_fmap_confl[of f s] by blast
  moreover have "|r| ≤o cardSuc |UNIV::nat set|"
  proof -
    have "finite (Field s) ⟶ |B| ≤o cardSuc |UNIV::nat set|" using b2 b5 
      by (metis Field_card_of cardSuc_greater card_of_card_order_on finite_ordLess_infinite2 
          infinite_UNIV_nat ordLeq_transitive ordLess_imp_ordLeq) 
    moreover have "¬ finite (Field s) ⟶ |B| ≤o cardSuc |UNIV::nat set|" 
      using b5 b6' b6'' ordIso_ordLeq_trans by blast
    ultimately have "|B| ≤o cardSuc |UNIV::nat set|" by blast
    moreover have "|f`B| ≤o |B|" by simp
    moreover have "|Field r| ≤o |f`B|" using b12 by simp
    ultimately have "|Field r| ≤o cardSuc |UNIV::nat set|" using ordLeq_transitive by metis
    then have "¬ finite r ⟶ |r| ≤o cardSuc |UNIV::nat set|" 
      using lem_rel_inf_fld_card[of r] ordIso_ordLeq_trans ordIso_symmetric by blast
    moreover have "finite r ⟶ |r| ≤o cardSuc |UNIV::nat set|" by (simp add: ordLess_imp_ordLeq)
    ultimately show ?thesis by blast
  qed
  ultimately show ?thesis by blast
qed

(* ----------------------------------------------------------------------- *)

subsubsection ‹Result›

(* ----------------------------------------------------------------------- *)

text ‹The next theorem has the following meaning:
  if the set of elements of type ‹'U› is uncountable,
  then there exists a confluent binary relation $r$ on ‹'U›
  such that the cardinality of $r$ does not exceed the first uncountable cardinal
  and confluence of $r$ cannot be proved using the decreasing diagrams method with 2 labels.›

theorem thm_example_not_dcr2: 
assumes "cardSuc |{n::nat. True}| ≤o |{x::'U. True}|"
shows "∃ r::'U rel. ( 
            ( ∀a b c. (a,b) ∈ r^* ∧ (a,c) ∈ r^* ⟶ (∃ d. (b,d) ∈ r^* ∧ (c,d) ∈ r^*) ) 
          ∧ |r| ≤o cardSuc |{n::nat. True}| 
          ∧ (¬ ( ∃r0 r1. (  
                ( r = (r0 ∪ r1) )
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0  
                   ⟶ (∃ d. 
                          (b,d) ∈ r0^= 
                        ∧ (c,d) ∈ r0^=) )
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r1  
                   ⟶ (∃b' d. 
                          (b,b') ∈ r1^= ∧ (b',d) ∈ r0^* 
                        ∧ (c,d) ∈ r0^*) )
              ∧ (∀ a b c. (a,b) ∈ r1 ∧ (a,c) ∈ r1  
                   ⟶ (∃b' b'' c' c'' d.  
                          (b,b') ∈ r0^* ∧ (b',b'') ∈ r1^= ∧ (b'',d) ∈ r0^* 
                        ∧ (c,c') ∈ r0^* ∧ (c',c'') ∈ r1^= ∧ (c'',d) ∈ r0^*) ) ) )
            ) )"
proof -
  have "cardSuc |UNIV::nat set| ≤o |UNIV::'U set|" using assms by (simp only: UNIV_def)
  then have "∃ r::'U rel. confl_rel r ∧ |r| ≤o cardSuc |UNIV::nat set| ∧ (¬ DCR2 r)" 
    using assms lem_not_dcr2 by blast
  then show ?thesis unfolding confl_rel_def DCR2_def LD2_def jn00_def jn01_def jn11_def
    by (simp only: UNIV_def) 
qed

corollary cor_example_not_dcr2:
shows "∃ r::(nat set) rel. ( 
            ( ∀a b c. (a,b) ∈ r^* ∧ (a,c) ∈ r^* ⟶ (∃ d. (b,d) ∈ r^* ∧ (c,d) ∈ r^*) ) 
          ∧ |r| ≤o cardSuc |{n::nat. True}| 
          ∧ (¬ ( ∃r0 r1. (  
                ( r = (r0 ∪ r1) )
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r0  
                   ⟶ (∃ d. 
                          (b,d) ∈ r0^= 
                        ∧ (c,d) ∈ r0^=) )
              ∧ (∀ a b c. (a,b) ∈ r0 ∧ (a,c) ∈ r1  
                   ⟶ (∃b' d. 
                          (b,b') ∈ r1^= ∧ (b',d) ∈ r0^* 
                        ∧ (c,d) ∈ r0^*) )
              ∧ (∀ a b c. (a,b) ∈ r1 ∧ (a,c) ∈ r1  
                   ⟶ (∃b' b'' c' c'' d.  
                          (b,b') ∈ r0^* ∧ (b',b'') ∈ r1^= ∧ (b'',d) ∈ r0^* 
                        ∧ (c,c') ∈ r0^* ∧ (c',c'') ∈ r1^= ∧ (c'',d) ∈ r0^*) ) ) )
            ) )"
proof -
  have "cardSuc |{x::nat. True}| ≤o |{x::nat set. True}|" by force
  then show ?thesis using thm_example_not_dcr2 by blast
qed

end