Theory Totally_Ordered_Hoops

section‹Totally ordered hoops›

theory Totally_Ordered_Hoops
  imports Ordinal_Sums
begin

subsection‹Definitions›

locale totally_ordered_hoop = hoop +
  assumes total_order: "x ∈ A ⟹ y ∈ A ⟹ x ≤A y ∨ y ≤A x "
begin

function fixed_points :: "'a ⇒ 'a set" (‹F›) where
  "F a = {b ∈ A-{1A}. a →A b = b}" if "a ∈ A-{1A}"
| "F a = {1A}" if "a = 1A" 
| "F a = undefined" if "a ∉ A"
  by auto
termination by lexicographic_order 

definition rel_F :: "'a ⇒ 'a ⇒ bool" (infix ‹∼F› 60)
  where "x ∼F y ≡ ∀ z ∈ A. (x →A z = z) ⟷ (y →A z = z)" 

definition rel_F_canonical_map :: "'a ⇒ 'a set" (‹π›)
  where "π x = {b ∈ A. x ∼F b}"

end

subsection‹Properties of @{text F}›

context totally_ordered_hoop 
begin

lemma F_equiv:
  assumes "a ∈ A-{1A}" "b ∈ A"
  shows "b ∈ F a ⟷ (b ∈ A ∧ b ≠ 1A ∧ a →A b = b)"
  using assms by auto

lemma F_subset:
  assumes "a ∈ A" 
  shows "F a ⊆ A"
proof -
  have "a = 1A ∨ a ≠ 1A"
    by auto
  then
  show ?thesis
    using assms by fastforce
qed 

lemma F_of_one:
  assumes "a ∈ A"
  shows "F a = {1A} ⟷ a = 1A"
  using F_equiv assms fixed_points.simps(2) top_closed by blast

lemma F_of_mult:
  assumes "a ∈ A-{1A}" "b ∈ A-{1A}"
  shows "F (a *A b) = {c ∈ A-{1A}. (a *A b) →A c = c}"
  using assms mult_C by auto

lemma F_of_imp:
  assumes "a ∈ A" "b ∈ A" "a →A b ≠ 1A"
  shows "F (a →A b) = {c ∈ A-{1A}. (a →A b) →A c = c}"
  using assms imp_closed by auto

lemma F_bound:
  assumes "a ∈ A" "b ∈ A" "a ∈ F b"
  shows "a ≤A b"
proof -
  consider (1) "b ≠ 1A"
    | (2) "b = 1A"
    by auto
  then
  show "?thesis"
  proof(cases)
    case 1
    then
    have "b →A a ≠ 1A"
      using assms(2,3) by simp
    then
    show ?thesis     
      using assms hoop_order_def total_order by auto
  next
    case 2
    then
    show ?thesis
      using assms(1) ord_top by auto
  qed
qed

text‹The following results can be found in Lemma 3.3 in cite‹"BUSANICHE2005"›.›

lemma LEMMA_3_3_1:
  assumes "a ∈ A-{1A}" "b ∈ A" "c ∈ A" "b ∈ F a" "c ≤A b"
  shows "c ∈ F a"
proof -
  from assms
  have "(a →A c) ≤A (a →A b)"
    using DiffD1 F_equiv ord_imp_mono_B by metis
  then
  have "(a →A c) ≤A b"
    using assms(1,4,5) by simp
  then
  have "(a →A c) →A c = ((a →A c) *A ((a →A c) →A b)) →A c"
    using assms(1,3) hoop_order_def imp_closed by force
  also
  have "… = (b *A (b →A (a →A c))) →A c"
    using assms divisibility imp_closed by simp
  also
  have "… = (b →A (a →A c)) →A (b →A c)"
    using DiffD1 assms(1-3) imp_closed swap residuation by metis
  also
  have "… = ((a →A b) →A (a →A c)) →A (b →A c)"
    using assms(1,4) by simp
  also
  have "… = (((a →A b) *A a) →A c) →A (b →A c)"
    using assms(1,3,4) residuation by simp
  also
  have "… = (((b →A a) *A b) →A c) →A (b →A c)"
    using assms(1,2) divisibility imp_closed mult_comm by simp
  also
  have "… = (b →A c) →A (b →A c)"
    using F_bound assms(1,4) hoop_order_def by simp
  also
  have "… = 1A"
    using F_bound assms hoop_order_def imp_closed by simp
  finally
  have "(a →A c) ≤A c"
    using hoop_order_def by simp
  moreover
  have "c ≤A (a →A c)"
    using assms(1,3) ord_A by simp
  ultimately
  have "a →A c = c"
    using assms(1,3) imp_closed ord_antisymm by simp
  moreover 
  have "c ∈ A-{1A}"
    using assms(1,3-5) hoop_order_def imp_one_C by auto
  ultimately
  show ?thesis
    using F_equiv assms(1) by blast
qed

lemma LEMMA_3_3_2:
  assumes "a ∈ A-{1A}" "b ∈ A-{1A}" "F a = F b"
  shows "F a = F (a *A b)"
proof 
  show "F a ⊆ F (a *A b)"
  proof 
    fix c 
    assume "c ∈ F a"
    then
    have "(a *A b) →A c = b →A (a →A c)"
      using DiffD1 F_subset assms(1,2) in_mono swap residuation by metis
    also
    have "… = b →A c"
      using ‹c ∈ F a› assms(1) by auto
    also
    have "… = c"
      using ‹c ∈ F a› assms(2,3) by auto
    finally
    show "c ∈ F (a *A b)"
      using ‹c ∈ F a› assms(1,2) mult_C by auto
  qed
next 
  show "F (a *A b) ⊆ F a"
  proof 
    fix c
    assume "c ∈ F (a *A b)"
    then
    have "(a *A b) ≤A a"
      using assms(1,2) mult_A by auto
    then
    have "(a →A c) ≤A ((a *A b) →A c)"
      using DiffD1 F_subset ‹c ∈ F (a *A b)› assms mult_closed 
            ord_imp_anti_mono_B subsetD
      by meson
    moreover
    have "(a *A b) →A c = c"
      using ‹c ∈ F (a *A b)› assms(1,2) mult_C by auto
    ultimately
    have "(a →A c) ≤A c"
      by simp
    moreover
    have "c ≤A (a →A c)"
      using DiffD1 F_subset ‹c ∈ F (a *A b)› assms(1,2) insert_Diff
            insert_subset mult_closed ord_A
      by metis
    ultimately
    show "c ∈ F a"
      using ‹c ∈ F (a *A b)› assms(1,2) imp_closed mult_C ord_antisymm by auto
  qed
qed

lemma LEMMA_3_3_3:
  assumes "a ∈ A-{1A}" "b ∈ A-{1A}" "a ≤A b" 
  shows "F a ⊆ F b"
proof 
  fix c
  assume "c ∈ F a"
  then 
  have "(b →A c) ≤A (a →A c)"
    using DiffD1 F_subset assms in_mono ord_imp_anti_mono_B by meson
  moreover 
  have "a →A c = c"
    using ‹c ∈ F a› assms(1) by auto
  ultimately 
  have "(b →A c) ≤A c"
    by simp
  moreover
  have "c ≤A (b →A c)"
    using ‹c ∈ F a› assms(1,2) ord_A by force
  ultimately
  show "c ∈ F b"
    using ‹c ∈ F a› assms(1,2) imp_closed ord_antisymm by auto
qed

lemma LEMMA_3_3_4:
  assumes "a ∈ A-{1A}" "b ∈ A-{1A}" "a <A b" "F a ≠ F b"
  shows "a ∈ F b"
proof -
  from assms
  obtain c where "c ∈ F b ∧ c ∉ F a"
    using LEMMA_3_3_3 hoop_order_strict_def by auto
  then
  have witness: "c ∈ A-{1A} ∧ b →A c = c ∧ c <A (a →A c)"
    using DiffD1 assms(1,2) hoop_order_strict_def ord_A by auto
  then
  have "(a →A c) →A c ∈ F b"
    using DiffD1 F_equiv assms(1,2) imp_closed swap ord_D by metis
  moreover
  have "a ≤A ((a →A c) →A c)"
    using assms(1) ord_C witness by force
  ultimately
  show "a ∈ F b"
    using Diff_iff LEMMA_3_3_1 assms(1,2) imp_closed witness by metis
qed

lemma LEMMA_3_3_5:
  assumes "a ∈ A-{1A}" "b ∈ A-{1A}" "F a ≠ F b"
  shows "a *A b = a ∧A b"
proof -
  have "a <A b ∨ b <A a"
    using DiffD1 assms hoop_order_strict_def total_order by metis
  then
  have "a ∈ F b ∨ b ∈ F a"
    using LEMMA_3_3_4 assms by metis
  then
  have "a *A b = (b →A a) *A b ∨ a *A b = a *A (a →A b)"
    using assms(1,2) by force
  then
  show ?thesis
    using assms(1,2) divisibility hoop_inf_def imp_closed mult_comm by auto
qed

lemma LEMMA_3_3_6:
  assumes "a ∈ A-{1A}" "b ∈ A-{1A}" "a <A b" "F a = F b"
  shows "F (b →A a) = F b"
proof -
  have "a ∉ F a"
    using assms(1) DiffD1 F_equiv imp_reflex by metis
  then
  have "a <A (b →A a)"
    using assms(1,2,4) hoop_order_strict_def ord_A by auto
  moreover
  have "b *A (b →A a) = a"
    using assms(1-3) divisibility hoop_order_def hoop_order_strict_def by simp
  moreover
  have "b ≤A (b →A a) ∨ (b →A a) ≤A b"
    using DiffD1 assms(1,2) imp_closed ord_reflex total_order by metis
  ultimately
  have "b *A (b →A a) ≠ b ∧A (b →A a)"
    using assms(1-3) hoop_order_strict_def imp_closed inf_comm inf_order by force
  then
  show "F (b →A a) = F b"
    using LEMMA_3_3_5 assms(1-3) imp_closed ord_D by blast
qed

subsection‹Properties of @{term rel_F}›

subsubsection‹@{term rel_F} is an equivalence relation›

lemma rel_F_reflex:
  assumes "a ∈ A"
  shows "a ∼F a"
  using rel_F_def by auto

lemma rel_F_symm: 
  assumes "a ∈ A" "b ∈ A" "a ∼F b"
  shows "b ∼F a"
  using assms rel_F_def by auto

lemma rel_F_trans:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ∼F b" "b ∼F c"
  shows "a ∼F c"
  using assms rel_F_def by auto

subsubsection‹Equivalent definition›

lemma rel_F_equiv: 
  assumes "a ∈ A" "b ∈ A"
  shows "(a ∼F b) = (F a = F b)"
proof 
  assume "a ∼F b"
  then
  consider (1) "a ≠ 1A" "b ≠ 1A"
    | (2) "a = 1A" "b = 1A"
    using assms imp_one_C rel_F_def by fastforce
  then
  show "F a = F b"
  proof(cases)
    case 1
    then 
    show ?thesis
      using ‹a ∼F b› assms rel_F_def by auto
  next
    case 2
    then
    show ?thesis
      by simp
  qed
next
  assume "F a = F b"
  then
  consider (1) "a ≠ 1A" "b ≠ 1A"
    | (2) "a = 1A" "b = 1A"
    using F_of_one assms by blast
  then
  show "a ∼F b"
  proof(cases)
    case 1
    then
    show ?thesis
      using ‹F a = F b› assms imp_one_A imp_one_C rel_F_def by auto
  next
    case 2
    then
    show ?thesis
      using rel_F_reflex by simp
  qed
qed

subsubsection‹Properties of equivalence classes given by @{term rel_F}›

lemma class_one: "π 1A = {1A}"
  using imp_one_C rel_F_canonical_map_def rel_F_def by auto

lemma classes_subsets:
  assumes "a ∈ A"
  shows "π a ⊆ A"
  using rel_F_canonical_map_def by simp

lemma classes_not_empty:
  assumes "a ∈ A"
  shows "a ∈ π a"
  using assms rel_F_canonical_map_def rel_F_reflex by simp

corollary class_not_one:
  assumes "a ∈ A-{1A}"
  shows "π a ≠ {1A}"
  using assms classes_not_empty by blast

lemma classes_disjoint: 
  assumes "a ∈ A" "b ∈ A" "π a ∩ π b ≠ ∅"
  shows "π a = π b"
  using assms rel_F_canonical_map_def rel_F_def rel_F_trans by force

lemma classes_cover: "A = {x. ∃ y ∈ A. x ∈ π y}"
  using classes_subsets classes_not_empty by auto

lemma classes_convex:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "d ∈ A" "b ∈ π a" "c ∈ π a" "b ≤A d" "d ≤A c" 
  shows "d ∈ π a"
proof -
  have eq_F: "F a = F b ∧ F a = F c"
    using assms(1,5,6) rel_F_canonical_map_def rel_F_equiv by auto
  from assms 
  consider (1) "c = 1A"
    | (2) "c ≠ 1A"
    by auto
  then 
  show ?thesis
  proof(cases)
    case 1 
    then
    have "b = 1A"
      using F_of_one eq_F assms(2) by auto
    then
    show ?thesis
      using "1" assms(2,4,5,7,8) ord_antisymm by blast
  next
    case 2
    then 
    have "b ≠ 1A ∧ c ≠ 1A ∧ d ≠ 1A"
      using eq_F assms(3,8) ord_antisymm ord_top by auto
    then
    have "F b ⊆ F d ∧ F d ⊆ F c"
      using LEMMA_3_3_3 assms(2-4,7,8) by simp
    then
    have "F a = F d"
      using eq_F by blast
    then
    have "a ∼F d"
      using assms(1,4) rel_F_equiv by simp
    then
    show ?thesis
      using assms(4) rel_F_canonical_map_def by simp
  qed
qed

lemma related_iff_same_class:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∼F b ⟷ π a = π b"
proof 
  assume "a ∼F b"
  then
  have "a = 1A ⟷ b = 1A"
    using assms imp_one_C imp_reflex rel_F_def by metis
  then
  have "(a = 1A ∧ b = 1A) ∨ (a ≠ 1A ∧ b ≠ 1A)"
    by auto
  then
  show "π a = π b"
    using ‹a ∼F b› assms rel_F_canonical_map_def rel_F_def rel_F_symm by force
next
  show "π a = π b ⟹ a ∼F b"
    using assms(2) classes_not_empty rel_F_canonical_map_def by auto
qed

corollary same_F_iff_same_class:
  assumes "a ∈ A" "b ∈ A"
  shows "F a = F b ⟷ π a = π b"
  using assms rel_F_equiv related_iff_same_class by auto

end

subsection‹Irreducible hoops: definition and equivalences›

text‹A totally ordered hoop is @{text irreducible} if it cannot be written as the ordinal sum
of two nontrivial totally ordered hoops.›

locale totally_ordered_irreducible_hoop = totally_ordered_hoop +
  assumes irreducible:  "∄ B C. 
    (A = B ∪ C) ∧
    ({1A} = B ∩ C) ∧
    (∃ y ∈ B. y ≠ 1A) ∧
    (∃ y ∈ C. y ≠ 1A) ∧
    (hoop B (*A) (→A) 1A) ∧
    (hoop C (*A) (→A) 1A) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x *A y = x) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x →A y = 1A) ∧
    (∀ x ∈ C. ∀ y ∈ B. x →A y = y)"

lemma irr_test: 
  assumes "totally_ordered_hoop A PA RA a"
          "¬totally_ordered_irreducible_hoop A PA RA a"
  shows "∃ B C. 
    (A = B ∪ C) ∧
    ({a} = B ∩ C) ∧
    (∃ y ∈ B. y ≠ a) ∧
    (∃ y ∈ C. y ≠ a) ∧
    (hoop B PA RA a) ∧
    (hoop C PA RA a) ∧ 
    (∀ x ∈ B-{a}. ∀ y ∈ C. PA x y = x) ∧
    (∀ x ∈ B-{a}. ∀ y ∈ C. RA x y = a) ∧
    (∀ x ∈ C. ∀ y ∈ B. RA x y = y)" 
  using assms unfolding totally_ordered_irreducible_hoop_def
                        totally_ordered_irreducible_hoop_axioms_def
  by force

locale totally_ordered_one_fixed_hoop = totally_ordered_hoop +
  assumes one_fixed: "x ∈ A ⟹ y ∈ A ⟹ y →A x = x ⟹ x = 1A ∨ y = 1A"

locale totally_ordered_wajsberg_hoop = totally_ordered_hoop + wajsberg_hoop

context totally_ordered_hoop
begin

text‹The following result can be found in cite‹"AGLIANO2003"› (see Lemma 3.5).›

lemma not_one_fixed_implies_not_irreducible:
  assumes "¬totally_ordered_one_fixed_hoop A (*A) (→A) 1A"
  shows "¬totally_ordered_irreducible_hoop A (*A) (→A) 1A"
proof -
  have "∃ x y. x ∈ A ∧ y ∈ A ∧ y →A x = x ∧ x ≠ 1A ∧ y ≠ 1A"
    using assms totally_ordered_hoop_axioms totally_ordered_one_fixed_hoop.intro
          totally_ordered_one_fixed_hoop_axioms.intro
    by meson
  then
  obtain b0 c0 where witnesses: "b0 ∈ A-{1A} ∧ c0 ∈ A-{1A} ∧ b0 →A c0 = c0"
    by auto
  define B C where "B = (F b0) ∪ {1A}" and "C = A-(F b0)"

  have B_mult_b0: "b *A b0 = b" if "b ∈ B-{1A}" for b 
  proof -
    have upper_bound: "b ≤A b0" if "b ∈ B-{1A}" for b
      using B_def F_bound witnesses that by force
    then
    have "b *A b0 = b0 *A b"
      using B_def witnesses mult_comm that by simp
    also
    have "… = b0 *A (b0 →A b)"
      using B_def witnesses that by fastforce
    also
    have "… = b *A (b →A b0)"
      using B_def witnesses that divisibility by auto
    also 
    have "… = b"
      using B_def hoop_order_def that upper_bound witnesses by auto
    finally
    show "b *A b0 = b"
      by auto
  qed

  have C_upper_set: "a ∈ C" if "a ∈ A" "c ∈ C" "c ≤A a" for a c
  proof -
    consider (1) "a ≠ 1A"
      | (2) "a = 1A"
      by auto
    then
    show "a ∈ C"
    proof(cases)
      case 1
      then
      have "a ∉ C ⟹ a ∈ F b0"
        using C_def that(1) by blast
      then
      have "a ∉ C ⟹ c ∈ F b0"
        using C_def DiffD1 witnesses LEMMA_3_3_1 that by metis
      then 
      show ?thesis
        using C_def that(2) by blast
    next
      case 2
      then
      show ?thesis
        using C_def witnesses by auto
    qed
  qed

  have B_union_C: "A = B ∪ C"
    using B_def C_def witnesses one_closed by auto

  moreover

  have B_inter_C: "{1A} = B ∩ C"
    using B_def C_def witnesses by force

  moreover

  have B_not_trivial: "∃ y ∈ B. y ≠ 1A"
  proof -
    have "c0 ∈ B ∧ c0 ≠ 1A"
      using B_def witnesses by auto
    then
    show ?thesis
      by auto
  qed

  moreover

  have C_not_trivial: "∃ y ∈ C. y ≠ 1A"
  proof -
    have "b0 ∈ C ∧ b0 ≠ 1A"
      using C_def witnesses by auto
    then
    show ?thesis
      by auto
  qed

  moreover

  have B_mult_closed: "a *A b ∈ B" if "a ∈ B" "b ∈ B" for a b
  proof -
    from that
    consider (1) "a ∈ F b0"
      | (2) "a = 1A"
      using B_def by blast
    then
    show "a *A b ∈ B"
    proof(cases)
      case 1
      then
      have "a ∈ A ∧ a *A b ∈ A ∧ (a *A b) ≤A a"
        using B_union_C that mult_A mult_closed by blast
      then
      have "a *A b ∈ F b0"
        using "1" witnesses LEMMA_3_3_1 by metis
      then
      show ?thesis
        using B_def by simp
    next
      case 2
      then
      show ?thesis
        using B_union_C that(2) by simp
    qed
  qed

  moreover

  have B_imp_closed: "a →A b ∈ B" if "a ∈ B" "b ∈ B" for a b
  proof -
    from that
    consider (1) "a = 1A ∨ b = 1A ∨ (a ∈ F b0 ∧ b ∈ F b0 ∧ a →A b = 1A)"
      | (2) "a ∈ F b0" "b ∈ F b0" "a →A b ≠ 1A"
      using B_def by fastforce
    then 
    show "a →A b ∈ B"
    proof(cases)
      case 1
      then
      have "a →A b = b ∨ a →A b = 1A"
        using B_union_C that imp_one_C imp_one_top by blast
      then
      show ?thesis
        using B_inter_C that(2) by fastforce
    next
      case 2
      then
      have "a *A b0 = a"
        using B_def B_mult_b0 witnesses by auto
      then
      have "b0 →A (a →A b) = (a →A b)"
        using B_union_C witnesses that mult_comm residuation by simp
      then
      have "a →A b ∈ F b0"
        using "2"(3) B_union_C F_equiv witnesses that imp_closed by auto
      then
      show ?thesis
        using B_def by auto
    qed
  qed

  moreover

  have B_hoop: "hoop B (*A) (→A) 1A"
  proof
    show "x *A y ∈ B" if "x ∈ B" "y ∈ B" for x y
      using B_mult_closed that by simp
  next
    show "x →A y ∈ B" if "x ∈ B" "y ∈ B" for x y
      using B_imp_closed that by simp
  next
    show "1A ∈ B"
      using B_def by simp
  next
    show "x *A y = y *A x" if "x ∈ B" "y ∈ B" for x y
      using B_union_C mult_comm that by simp
  next
    show "x *A (y *A z) = (x *A y) *A z" if "x ∈ B" "y ∈ B" "z ∈ B" for x y z
      using B_union_C mult_assoc that by simp
  next 
    show "x *A 1A = x" if "x ∈ B" for x
      using B_union_C that by simp
  next
    show "x →A x = 1A" if "x ∈ B" for x
      using B_union_C that by simp
  next 
    show "x *A (x →A y) = y *A (y →A x)" if "x ∈ B" "y ∈ B" for x y
      using B_union_C divisibility that by simp
  next 
    show "x →A (y →A z) = (x *A y) →A z" if "x ∈ B" "y ∈ B" "z ∈ B" for x y z
      using B_union_C residuation that by simp
  qed

  moreover

  have C_imp_B: "c →A b = b" if "b ∈ B" "c ∈ C" for b c
  proof -
    from that
    consider (1) "b ∈ F b0" "c ≠ 1A"
      | (2) "b = 1A ∨ c = 1A"
      using B_def by blast
    then
    show "c →A b = b"
    proof(cases)
      case 1
      have "b0 →A ((c →A b) →A b) = (c →A b) →A (b0 →A b)"
        using B_union_C witnesses that imp_closed swap by simp
      also
      have "… = (c →A b) →A b"
        using "1"(1) witnesses by auto
      finally
      have "(c →A b) →A b ∈ F b0" if "(c →A b) →A b ≠ 1A"
        using B_union_C F_equiv witnesses ‹b ∈ B› ‹c ∈ C› that imp_closed by auto
      moreover
      have "c ≤A ((c →A b) →A b)"
        using B_union_C that ord_C by simp
      ultimately 
      have "(c →A b) →A b = 1A"
        using B_def B_union_C C_def C_upper_set that(2) by blast
      moreover
      have "b →A (c →A b) = 1A"
        using B_union_C that imp_A by simp
      ultimately
      show ?thesis
        using B_union_C that imp_closed ord_antisymm_equiv by blast
    next
      case 2
      then
      show ?thesis
        using B_union_C that imp_one_C imp_one_top by auto
    qed
  qed

  moreover

  have B_imp_C: "b →A c = 1A" if "b ∈ B-{1A}" "c ∈ C" for b c
  proof -
    from that
    have "b ≤A c ∨ c ≤A b"
      using total_order B_union_C by blast
    moreover
    have "c →A b = b"
      using C_imp_B that by simp
    ultimately
    show "b →A c = 1A"
      using that(1) hoop_order_def by force
  qed

  moreover

  have B_mult_C: "b *A c = b" if "b ∈ B-{1A}" "c ∈ C" for b c
  proof -
    have "b = b *A 1A"
      using that(1) B_union_C by fastforce
    also
    have "… = b *A (b →A c)"
      using B_imp_C that by blast
    also
    have "… = c *A (c →A b)"
      using that divisibility B_union_C by simp
    also
    have "… = c *A b"
      using C_imp_B that by auto
    finally
    show "b *A c = b"
      using that mult_comm B_union_C by auto
  qed

  moreover

  have C_mult_closed: "c *A d ∈ C" if "c ∈ C" "d ∈ C" for c d
  proof -
    consider (1) "c ≠ 1A" "d ≠ 1A"
      | (2) "c = 1A ∨ d = 1A"
      by auto
    then
    show "c *A d ∈ C"
    proof(cases)
      case 1
      have "c *A d ∈ F b0" if "c *A d ∉ C"
        using C_def ‹c ∈ C› ‹d ∈ C› mult_closed that by force
      then
      have "c →A (c *A d) ∈ F b0" if "c *A d ∉ C"
        using B_def C_imp_B ‹c ∈ C› that by simp
      moreover
      have "d ≤A (c →A (c *A d))"
        using C_def DiffD1 that ord_reflex ord_residuation residuation
              mult_closed mult_comm
        by metis
      moreover
      have "c →A (c *A d) ∈ A ∧ d ∈ A"
        using C_def Diff_iff that imp_closed mult_closed by metis
      ultimately
      have "d ∈ F b0" if "c *A d ∉ C"
        using witnesses LEMMA_3_3_1 that by blast
      then
      show ?thesis
        using C_def that(2) by blast
    next
      case 2
      then
      show ?thesis
        using B_union_C that mult_neutr mult_neutr_2 by auto
    qed
  qed

  moreover

  have C_imp_closed: "c →A d ∈ C" if "c ∈ C" "d ∈ C" for c d
    using C_upper_set imp_closed ord_A B_union_C that by blast

  moreover

  have C_hoop: "hoop C (*A) (→A) 1A"
  proof
    show "x *A y ∈ C" if "x ∈ C" "y ∈ C" for x y
      using C_mult_closed that by simp
  next
    show "x →A y ∈ C" if "x ∈ C" "y ∈ C" for x y
      using C_imp_closed that by simp
  next
    show "1A ∈ C"
      using B_inter_C by auto
  next
    show "x *A y = y *A x" if "x ∈ C" "y ∈ C" for x y
      using B_union_C mult_comm that by simp
  next
    show "x *A (y *A z) = (x *A y) *A z" if "x ∈ C" "y ∈ C" "z ∈ C" for x y z
      using B_union_C mult_assoc that by simp
  next 
    show "x *A 1A = x" if "x ∈ C" for x
      using B_union_C that by simp
  next
    show "x →A x = 1A" if "x ∈ C" for x
      using B_union_C that by simp
  next 
    show "x *A (x →A y) = y *A (y →A x)" if "x ∈ C" "y ∈ C" for x y
      using B_union_C divisibility that by simp
  next 
    show "x →A (y →A z) = (x *A y) →A z" if "x ∈ C" "y ∈ C" "z ∈ C" for x y z
      using B_union_C residuation that by simp
  qed

  ultimately

  have "∃ B C. 
    (A = B ∪ C) ∧
    ({1A} = B ∩ C) ∧
    (∃ y ∈ B. y ≠ 1A) ∧
    (∃ y ∈ C. y ≠ 1A) ∧
    (hoop B (*A) (→A) 1A) ∧
    (hoop C (*A) (→A) 1A) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x *A y = x) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x →A y = 1A) ∧
    (∀ x ∈ C. ∀ y ∈ B. x →A y = y)"
    by (smt (verit)) 
  then
  show ?thesis
    using totally_ordered_irreducible_hoop.irreducible by (smt (verit))
qed

text‹Next result can be found in cite‹"BLOK2000"› (see Proposition 2.2).›

lemma one_fixed_implies_wajsberg:
  assumes "totally_ordered_one_fixed_hoop A (*A) (→A) 1A"
  shows "totally_ordered_wajsberg_hoop A (*A) (→A) 1A"
proof 
  have "(a →A b) →A b = (b →A a) →A a" if "a ∈ A" "b ∈ A" "a <A b" for a b
  proof -
    from that
    have "(((b →A a) →A a) →A b) →A (b →A a) = b →A a ∧ b →A a ≠ 1A"
      using imp_D ord_D by simp
    then
    have "((b →A a) →A a) →A b = 1A"
      using assms that(1,2) imp_closed totally_ordered_one_fixed_hoop.one_fixed
      by metis
    moreover
    have "b →A ((b →A a) →A a) = 1A"
      using hoop_order_def that(1,2) ord_C by simp
    ultimately
    have "(b →A a) →A a = b"
      using imp_closed ord_antisymm_equiv hoop_axioms that(1,2) by metis
    also
    have "… = (a →A b) →A b"
      using hoop_order_def hoop_order_strict_def that(2,3) imp_one_C by force
    finally
    show "(a →A b) →A b = (b →A a) →A a"
      by auto
  qed
  then
  show "(x →A y) →A y = (y →A x) →A x" if "x ∈ A" "y ∈ A" for x y 
    using total_order hoop_order_strict_def that by metis
qed

text‹The proof of the following result can be found in cite‹"AGLIANO2003"› (see Theorem 3.6).›

lemma not_irreducible_implies_not_wajsberg:
  assumes "¬totally_ordered_irreducible_hoop A (*A) (→A) 1A"
  shows "¬totally_ordered_wajsberg_hoop A (*A) (→A) 1A"
proof -
  have "∃ B C. 
    (A = B ∪ C) ∧
    ({1A} = B ∩ C) ∧
    (∃ y ∈ B. y ≠ 1A) ∧
    (∃ y ∈ C. y ≠ 1A) ∧
    (hoop B (*A) (→A) 1A) ∧
    (hoop C (*A) (→A) 1A) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x *A y = x) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x →A y = 1A) ∧
    (∀ x ∈ C. ∀ y ∈ B. x →A y = y)"
    using irr_test[OF totally_ordered_hoop_axioms] assms by auto
  then  
  obtain B C where H:
    "(A = B ∪ C) ∧
    ({1A} = B ∩ C) ∧
    (∃ y ∈ B. y ≠ 1A) ∧
    (∃ y ∈ C. y ≠ 1A) ∧
    (∀ x ∈ B-{1A}. ∀ y ∈ C. x →A y = 1A) ∧
    (∀ x ∈ C. ∀ y ∈ B. x →A y = y)"
    by blast
  then
  obtain b c where assms: "b ∈ B-{1A} ∧ c ∈ C-{1A}"
    by auto
  then
  have "b →A c = 1A"
    using H by simp
  then
  have "(b →A c) →A c = c"
    using H assms imp_one_C by blast
  moreover
  have "(c →A b) →A b = 1A"
    using assms H by force
  ultimately
  have "(b →A c) →A c ≠ (c →A b) →A b"
    using assms by force
  moreover
  have "b ∈ A ∧ c ∈ A"
    using assms H by blast
  ultimately
  show ?thesis
    using totally_ordered_wajsberg_hoop.axioms(2) wajsberg_hoop.T by meson
qed

text‹Summary of all results in this subsection:›

theorem one_fixed_equivalent_to_wajsberg: 
  shows "totally_ordered_one_fixed_hoop A (*A) (→A) 1A ≡ 
         totally_ordered_wajsberg_hoop A (*A) (→A) 1A"
  using not_irreducible_implies_not_wajsberg not_one_fixed_implies_not_irreducible
        one_fixed_implies_wajsberg
  by linarith

theorem wajsberg_equivalent_to_irreducible:
  shows "totally_ordered_wajsberg_hoop A (*A) (→A) 1A ≡
         totally_ordered_irreducible_hoop A (*A) (→A) 1A"
  using not_irreducible_implies_not_wajsberg not_one_fixed_implies_not_irreducible
        one_fixed_implies_wajsberg
  by linarith

theorem irreducible_equivalent_to_one_fixed:
  shows "totally_ordered_irreducible_hoop A (*A) (→A) 1A ≡
         totally_ordered_one_fixed_hoop A (*A) (→A) 1A"
  using one_fixed_equivalent_to_wajsberg wajsberg_equivalent_to_irreducible
  by simp

end

subsection‹Decomposition›
                               
locale tower_of_irr_hoops = tower_of_hoops +
  assumes family_of_irr_hoops: "i ∈ I ⟹
                         totally_ordered_irreducible_hoop (𝔸⇩i) (*⇧i) (→⇧i) 1S"

locale tower_of_nontrivial_irr_hoops = tower_of_irr_hoops + 
  assumes nontrivial: "i ∈ I ⟹ ∃ x ∈ 𝔸⇩i. x ≠ 1S"

context totally_ordered_hoop
begin

subsubsection‹Definition of index set @{text "I"}›

definition index_set :: "('a set) set" (‹I›)
  where "I = {y. (∃ x ∈ A. π x = y)}"

lemma indexes_subsets: 
  assumes "i ∈ I"
  shows "i ⊆ A"
  using index_set_def assms rel_F_canonical_map_def by auto

lemma indexes_not_empty:
  assumes "i ∈ I"
  shows "i ≠ ∅"
  using index_set_def assms classes_not_empty by blast

lemma indexes_disjoint:
  assumes "i ∈ I" "j ∈ I" "i ≠ j"
  shows "i ∩ j = ∅"
proof -
  obtain a b where "a ∈ A ∧ b ∈ A ∧ a ≠ b ∧ i = π a ∧ j = π b"
    using index_set_def assms by auto
  then
  show ?thesis
    using assms(3) classes_disjoint by auto
qed

lemma indexes_cover: "A = {x. ∃ i ∈ I. x ∈ i}"
  using classes_subsets classes_not_empty index_set_def by auto

lemma indexes_class_of_elements: 
  assumes "i ∈ I" "a ∈ A" "a ∈ i"
  shows "π a = i"
proof -
  obtain c where class_element:  "c ∈ A ∧ i = π c"
    using assms(1) index_set_def by auto
  then
  have "a ∼F c"
    using assms(3) rel_F_canonical_map_def rel_F_symm by auto
  then
  show ?thesis
    using assms(2) class_element related_iff_same_class by simp
qed

lemma indexes_convex:
  assumes "i ∈ I" "a ∈ i" "b ∈ i" "d ∈ A" "a ≤A d" "d ≤A b"
  shows "d ∈ i"
proof -
  have "a ∈ A ∧ b ∈ A ∧ d ∈ A ∧ i = π a"
    using assms(1-4) indexes_class_of_elements indexes_subsets by blast
  then
  show ?thesis
    using assms(2-6) classes_convex by auto
qed

subsubsection‹Definition of total partial order over @{term I}›

text‹Since each equivalence class is convex, @{term hoop_order} induces a total order on @{term I}.›

function index_order :: "('a set) ⇒ ('a set) ⇒ bool" (infix ‹≤I› 60) where
  "x ≤I y = ((x = y) ∨ (∀ v ∈ x. ∀ w ∈ y. v ≤A w))" if "x ∈ I" "y ∈ I"
| "x ≤I y = undefined" if "x ∉ I ∨ y ∉ I"
  by auto
termination by lexicographic_order

definition index_order_strict (infix ‹<I› 60)
  where "x <I y = (x ≤I y ∧ x ≠ y)"

lemma index_ord_reflex: 
  assumes "i ∈ I"
  shows "i ≤I i"
  using assms by simp

lemma index_ord_antisymm:
  assumes "i ∈ I" "j ∈ I" "i ≤I j" "j ≤I i"
  shows "i = j"
proof -
  have "i = j ∨ (∀ a ∈ i. ∀ b ∈ j. a ≤A b ∧ b ≤A a)"
    using assms by auto
  then
  have "i = j ∨ (∀ a ∈ i. ∀ b ∈ j. a = b)"
    using assms(1,2) indexes_subsets insert_Diff insert_subset ord_antisymm
    by metis
  then
  show ?thesis
    using assms(1,2) indexes_not_empty by force
qed

lemma index_ord_trans:
  assumes "i ∈ I" "j ∈ I" "k ∈ I" "i ≤I j" "j ≤I k" 
  shows "i ≤I k"
proof -
  consider (1) "i ≠ j" "j ≠ k"
    | (2) "i = j ∨ j = k"
    by auto
  then
  show "i ≤I k"
  proof(cases)
    case 1
    then
    have "(∀ a ∈ i. ∀ b ∈ j. a ≤A b) ∧ (∀ b ∈ j. ∀ c ∈ k. b ≤A c)"
      using assms by force
    moreover
    have "j ≠ ∅"
      using assms(2) indexes_not_empty by simp
    ultimately
    have "∀ a ∈ i. ∀ c ∈ k. ∃ b ∈ j. a ≤A b ∧ b ≤A c"
      using all_not_in_conv by meson
    then
    have "∀ a ∈ i. ∀ c ∈ k. a ≤A c"
      using assms indexes_subsets ord_trans subsetD by metis
    then
    show ?thesis
      using assms(1,3) by simp
  next
    case 2
    then
    show ?thesis
      using assms(4,5) by auto
  qed
qed

lemma index_order_total :
  assumes "i ∈ I" "j ∈ I" "¬(j ≤I i)"
  shows "i ≤I j"
proof -
  have "i ≠ j"
    using assms(1,3) by auto
  then
  have disjoint: "i ∩ j = ∅"
    using assms(1,2) indexes_disjoint by simp
  moreover
  have "∃ x ∈ j. ∃ y ∈ i. ¬(x ≤A y)"
    using assms index_order.simps(1) by blast
  moreover
  have subsets: "i ⊆ A ∧ j ⊆ A"
    using assms indexes_subsets by simp
  ultimately
  have "∃ x ∈ j. ∃ y ∈ i. y <A x"
    using total_order hoop_order_strict_def insert_absorb insert_subset by metis
  then
  obtain ai aj where witnesses: "ai ∈ i ∧ aj ∈ j ∧ ai <A aj"
    using assms(1,2) total_order hoop_order_strict_def indexes_subsets by metis
  then
  have "a ≤A b" if "a ∈ i" "b ∈ j" for a b
  proof 
    from that
    consider (1) "ai ≤A a" "aj ≤A b"
      | (2) "a <A ai" "b <A aj"
      | (3) "ai ≤A a" "b <A aj"
      | (4) "a <A ai" "aj ≤A b" 
      using total_order hoop_order_strict_def subset_eq subsets witnesses by metis
    then
    show "a ≤A b"
    proof(cases)
      case 1 
      then
      have "ai ≤A aj ∧ aj ≤A b ∧ b ≤A a" if "b <A a"
        using hoop_order_strict_def that witnesses by blast
      then
      have "ai ≤A b ∧ b ≤A a" if "b <A a"
        using ‹b ∈ j› in_mono ord_trans subsets that witnesses by meson
      then
      have "b ∈ i" if "b <A a"
        using assms(1) ‹a ∈ i› ‹b ∈ j› indexes_convex subsets that witnesses
        by blast
      then
      show "a ≤A b"
        using disjoint disjoint_iff_not_equal hoop_order_strict_def subset_eq
              subsets that total_order
        by metis
    next
      case 2
      then
      have "b ≤A a ∧ a ≤A ai ∧ ai ≤A aj" if "b <A a"
        using hoop_order_strict_def that witnesses by blast
      then
      have "b ≤A a ∧ a ≤A aj" if "b <A a"
        using ‹a ∈ i› ord_trans subset_eq subsets that witnesses by metis
      then
      have "a ∈ j" if "b <A a"
        using assms(2) ‹a ∈ i› ‹b ∈ j› indexes_convex subsets that witnesses
        by blast
      then
      show "a ≤A b"
        using disjoint disjoint_iff_not_equal hoop_order_strict_def subset_eq
              subsets that total_order
        by metis
    next
      case 3 
      have "b ≤A ai ∧ ai ≤A aj" if "b ≤A ai"
        using hoop_order_strict_def that witnesses by auto
      then
      have "ai ∈ j" if "b ≤A ai"
        using assms(2) ‹b ∈ j› indexes_convex subsets that witnesses by blast
      moreover 
      have "ai ∉ j"
        using disjoint witnesses by blast
      ultimately
      have "ai <A b"
        using total_order hoop_order_strict_def ‹b ∈ j› subsets witnesses by blast
      then
      have "ai ≤A b ∧ b ≤A a" if "b <A a"
        using hoop_order_strict_def that by auto
      then
      have "b ∈ i" if "b <A a"
        using assms(1) ‹a ∈ i› ‹b ∈ j› indexes_convex subsets that witnesses
        by blast
      then
      show "a ≤A b"
        using disjoint disjoint_iff_not_equal hoop_order_strict_def subset_eq
              subsets that total_order
        by metis
    next
      case 4
      then
      show "a ≤A b"
        using hoop_order_strict_def in_mono ord_trans subsets that witnesses
        by meson
    qed
  qed
  then
  show "i ≤I j"
    using assms by simp
qed

sublocale total_poset_on "I" "(≤I)" "(<I)"
proof
  show "I ≠ ∅"
    using indexes_cover by auto
next 
  show "reflp_on I (≤I)"
    using index_ord_reflex reflp_onI by blast
next
  show "antisymp_on I (≤I)"
    using antisymp_on_def index_ord_antisymm by blast
next
  show "transp_on I (≤I)"
    using index_ord_trans transp_on_def by blast
next
  show "x <I y = (x ≤I y ∧ x ≠ y)" if "x ∈ I" "y ∈ I" for x y
    using index_order_strict_def by auto
next 
  show "totalp_on I (≤I)"
    using index_order_total totalp_onI by metis
qed

subsubsection‹Definition of universes›

definition universes :: "'a set ⇒ 'a set" (‹UNIA›)
  where "UNIA x = x ∪ {1A}"

abbreviation (uniA_i)
  uniA_i :: "['a set] ⇒ ('a set)" (‹(𝔸(⇩_))› [61] 60)
  where "𝔸⇩i ≡ UNIA i"

abbreviation (uniA_pi)
  uniA_pi :: "['a] ⇒ ('a set)" (‹(𝔸π (⇩_))› [61] 60)
  where "𝔸π⇩x ≡ UNIA (π x)"

abbreviation (uniA_pi_one)
  uniA_pi_one :: "'a set" (‹(𝔸π1A)› 60)
  where "𝔸π1A ≡ UNIA (π 1A)"

lemma universes_subsets: 
  assumes "i ∈ I" "a ∈ 𝔸⇩i"
  shows "a ∈ A"
  using assms universes_def indexes_subsets one_closed by fastforce

lemma universes_not_empty:
  assumes "i ∈ I"
  shows "𝔸⇩i ≠ ∅"
  using universes_def by simp

lemma universes_almost_disjoint:
  assumes "i ∈ I" "j ∈ I" "i ≠ j" 
  shows "(𝔸⇩i) ∩ (𝔸⇩j) = {1A}"
  using assms indexes_disjoint universes_def by auto

lemma universes_cover: "A = {x. ∃ i ∈ I. x ∈ 𝔸⇩i}"
  using one_closed indexes_cover universes_def by auto

lemma universes_aux: 
  assumes "i ∈ I" "a ∈ i"
  shows "𝔸⇩i = π a ∪ {1A}"
  using assms universes_def universes_subsets indexes_class_of_elements by force

subsubsection‹Universes are subhoops of @{text "A"}›

lemma universes_one_closed:
  assumes "i ∈ I"
  shows "1A ∈ 𝔸⇩i"
  using universes_def by auto

lemma universes_mult_closed:
  assumes "i ∈ I" "a ∈ 𝔸⇩i" "b ∈ 𝔸⇩i"
  shows "a *A b ∈ 𝔸⇩i"
proof -
  consider (1) "a ≠ 1A" "b ≠ 1A"
    | (2) "a = 1A ∨ b = 1A"
    by auto
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have UNI_def: "𝔸⇩i = π a ∪ {1A} ∧ 𝔸⇩i = π b ∪ {1A}"
      using assms universes_def universes_subsets indexes_class_of_elements
      by simp
    then
    have "π a = π b"
      using "1" assms universes_def universes_subsets indexes_class_of_elements
      by force
    then
    have "F a = F b"
      using assms universes_subsets rel_F_equiv related_iff_same_class by meson
    then
    have "F (a *A b) = F a"
      using "1" LEMMA_3_3_2 assms universes_subsets by blast
    then
    have "π a = π (a *A b)"
      using assms universes_subsets mult_closed rel_F_equiv related_iff_same_class
      by metis
    then
    show ?thesis
      using UNI_def UnI1 assms classes_not_empty universes_subsets mult_closed
      by metis
  next
    case 2
    then
    show ?thesis
      using assms universes_subsets by auto
  qed
qed

lemma universes_imp_closed:
  assumes "i ∈ I" "a ∈ 𝔸⇩i" "b ∈ 𝔸⇩i"
  shows "a →A b ∈ 𝔸⇩i"
proof -
  from assms
  consider (1) "a ≠ 1A" "b ≠ 1A" "b <A a"
    | (2) "a = 1A ∨ b = 1A ∨ (a ≠ 1A ∧ b ≠ 1A ∧ a ≤A b)"
    using total_order universes_subsets hoop_order_strict_def by auto
  then
  show ?thesis
  proof(cases)
    case 1
    then
    have UNI_def: "𝔸⇩i = π a ∪ {1A} ∧ 𝔸⇩i = π b ∪ {1A}"
      using assms universes_def universes_subsets indexes_class_of_elements
      by simp
    then
    have "π a = π b"
      using "1" assms universes_def universes_subsets indexes_class_of_elements
      by force
    then
    have "F a = F b"
      using assms universes_subsets rel_F_equiv related_iff_same_class by simp
    then
    have "F (a →A b) = F a"
      using "1" LEMMA_3_3_6 assms universes_subsets by simp
    then
    have "π a = π (a →A b)"
      using assms universes_subsets imp_closed same_F_iff_same_class by simp
    then
    show ?thesis
      using UNI_def UnI1 assms classes_not_empty universes_subsets imp_closed
      by metis
  next
    case 2
    then
    show ?thesis
      using assms universes_subsets universes_one_closed hoop_order_def imp_one_A
            imp_one_C
      by auto
  qed
qed

subsubsection‹Universes are irreducible hoops›

lemma universes_one_fixed:
  assumes "i ∈ I" "a ∈ 𝔸⇩i" "b ∈ 𝔸⇩i" "a →A b = b" 
  shows "a = 1A ∨ b = 1A"
proof -
  from assms
  have "π a = π b" if "a ≠ 1A" "b ≠ 1A"
    using universes_def universes_subsets indexes_class_of_elements that by force
  then
  have "F a = F b" if "a ≠ 1A" "b ≠ 1A"
    using assms(1-3) universes_subsets same_F_iff_same_class that by blast
  then
  have "b = 1A" if "a ≠ 1A" "b ≠ 1A"
    using F_equiv assms universes_subsets fixed_points.cases imp_reflex that by metis
  then 
  show ?thesis
    by blast
qed

corollary universes_one_fixed_hoops:
  assumes "i ∈ I"
  shows "totally_ordered_one_fixed_hoop (𝔸⇩i) (*A) (→A) 1A"
proof
  show "x *A y ∈ 𝔸⇩i" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for x y
    using assms universes_mult_closed that by simp
next
  show "x →A y ∈ 𝔸⇩i" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for x y
    using assms universes_imp_closed that by simp
next
  show "1A ∈ 𝔸⇩i"
    using assms universes_one_closed by simp
next
  show "x *A y = y *A x" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for x y
    using assms universes_subsets mult_comm that by simp
next
  show "x *A (y *A z) = (x *A y) *A z" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for x y z
    using assms universes_subsets mult_assoc that by simp
next 
  show "x *A 1A = x" if "x ∈ 𝔸⇩i" for x
    using assms universes_subsets that by simp
next 
  show "x →A x = 1A" if "x ∈ 𝔸⇩i" for x
    using assms universes_subsets that by simp
next 
  show "x *A (x →A y) = y *A (y →A x)" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for x y
    using assms divisibility universes_subsets that by simp
next 
  show "x →A (y →A z) = (x *A y) →A z" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for x y z
    using assms universes_subsets residuation that by simp
next 
  show "x ≤A y ∨ y ≤A x" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for x y
    using assms total_order universes_subsets that by simp
next 
  show "x = 1A ∨ y = 1A" if "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "y →A x = x" for x y
    using assms universes_one_fixed that by blast
qed

corollary universes_irreducible_hoops:
  assumes "i ∈ I"
  shows "totally_ordered_irreducible_hoop (𝔸⇩i) (*A) (→A) 1A"
  using assms universes_one_fixed_hoops totally_ordered_hoop.irreducible_equivalent_to_one_fixed
        totally_ordered_one_fixed_hoop.axioms(1)
  by metis

subsubsection‹Some useful results›

lemma index_aux:
  assumes "i ∈ I" "j ∈ I" "i <I j" "a ∈ (𝔸⇩i)-{1A}" "b ∈ (𝔸⇩j)-{1A}"
  shows "a <A b ∧ ¬(a ∼F b)"
proof -
  have noteq: "i ≠ j ∧ x ≤A y" if "x ∈ i" "y ∈ j" for x y
    using assms that index_order_strict_def by fastforce
  moreover 
  have ij_def: "i = π a ∧ j = π b"
    using UnE assms universes_def universes_subsets indexes_class_of_elements
    by auto
  ultimately
  have "a <A b"
    using assms(1,2,4,5) classes_not_empty universes_subsets hoop_order_strict_def
    by blast
  moreover
  have "i = j" if "a ∼F b"
    using assms(1,2,4,5) that universes_subsets ij_def related_iff_same_class by auto
  ultimately
  show ?thesis
    using assms(2,3) trichotomy by blast
qed

lemma different_indexes_mult: 
  assumes "i ∈ I" "j ∈ I" "i <I j" "a ∈ (𝔸⇩i)-{1A}" "b ∈ (𝔸⇩j)-{1A}"
  shows "a *A b = a"
proof -
  have "a <A b ∧ ¬(a ∼F b)"
    using assms index_aux by blast
  then
  have "a <A b ∧ F a ≠ F b"
    using DiffD1 assms(1,2,4,5) universes_subsets rel_F_equiv by meson
  then
  have "a <A b ∧ a *A b = a ∧A b"
    using DiffD1 LEMMA_3_3_5 assms(1,2,4,5) universes_subsets by auto
  then
  show ?thesis
    using assms(1,2,4,5) universes_subsets hoop_order_strict_def inf_order by auto
qed

lemma different_indexes_imp_1:
  assumes "i ∈ I" "j ∈ I" "i <I j" "a ∈ (𝔸⇩i)-{1A}" "b ∈ (𝔸⇩j)-{1A}"
  shows "a →A b = 1A"
proof -
  have "x ≤A y" if "x ∈ i" "y ∈ j" for x y
    using assms(1-3) index_order_strict_def that by fastforce
  moreover
  have "a ∈ i ∧ b ∈ j"
    using assms(4,5) assms(5) universes_def by auto
  ultimately
  show ?thesis
    using hoop_order_def by auto
qed

lemma different_indexes_imp_2 :
  assumes "i ∈ I" "j ∈ I" "i <I j" "a ∈ (𝔸⇩j)-{1A}" "b ∈ (𝔸⇩i)-{1A}"
  shows "a →A b = b"
proof -
  have "b <A a ∧ ¬(b ∼F a)"
    using assms index_aux by blast
  then 
  have "b <A a ∧ F b ≠ F a"
    using DiffD1 assms(1,2,4,5) universes_subsets rel_F_equiv by metis
  then
  have "b ∈ F a"
    using LEMMA_3_3_4 assms(1,2,4,5) universes_subsets by simp
  then
  show ?thesis
    using assms(2,4,5) universes_subsets by fastforce
qed

subsubsection‹Definition of multiplications, implications and one›

definition mult_map :: "'a set ⇒ ('a ⇒ 'a ⇒ 'a)" (‹MULA›)
  where "MULA x = (*A)"

definition imp_map :: "'a set ⇒ ('a ⇒ 'a ⇒ 'a)" (‹IMPA›)
  where "IMPA x = (→A)"

definition sum_one :: "'a" (‹1S›)
  where "1S = 1A"

abbreviation (multA_i)
  multA_i :: "['a set] ⇒ ('a ⇒ 'a ⇒ 'a)"  (‹(*(⇧_))› [50] 60)
  where "*⇧i ≡ MULA i"

abbreviation (impA_i)
  impA_i:: "['a set] ⇒ ('a ⇒ 'a ⇒ 'a)" (‹(→(⇧_))› [50] 60)
  where "→⇧i ≡ IMPA i"

abbreviation (multA_i_xy)
  multA_i_xy :: "['a, 'a set, 'a] ⇒ 'a" (‹((_)/ *(⇧_) / (_))› [61, 50, 61] 60)
  where "x *⇧i y ≡ MULA i x y"

abbreviation (impA_i_xy)
  impA_i_xy :: "['a, 'a set, 'a] ⇒ 'a" (‹((_)/ →(⇧_) / (_))› [61, 50, 61] 60)
  where "x →⇧i y ≡ IMPA i x y"

abbreviation (ord_i_xy)
  ord_i_xy :: "['a, 'a set, 'a] ⇒ bool" (‹((_)/ ≤(⇧_) / (_))› [61, 50, 61] 60)
  where "x ≤⇧i y ≡ hoop.hoop_order (IMPA i) 1S x y"

subsubsection‹Main result›

text‹We prove the main result: a totally ordered hoop is equal 
to an ordinal sum of a tower of irreducible hoops.›

sublocale A_SUM: tower_of_irr_hoops "I" "(≤I)" "(<I)" "UNIA" "MULA" "IMPA" "1S" 
proof 
  show "(𝔸⇩i) ∩ (𝔸⇩j) = {1S}" if "i ∈ I" "j ∈ I" "i ≠ j" for i j
    using universes_almost_disjoint sum_one_def that by simp
next 
  show "x *⇧i y ∈ 𝔸⇩i" if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using universes_mult_closed mult_map_def that by simp
next
  show "x →⇧i y ∈ 𝔸⇩i" if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using universes_imp_closed imp_map_def that by simp
next
  show "1S ∈ 𝔸⇩i" if "i ∈ I" for i
    using universes_one_closed sum_one_def that by simp
next 
  show "x *⇧i y = y *⇧i x" if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using universes_subsets mult_comm mult_map_def that by simp
next
  show "x *⇧i (y *⇧i z) = (x *⇧i y) *⇧i z"
    if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for i x y z
    using universes_subsets mult_assoc mult_map_def that by simp
next
  show "x *⇧i 1S = x" if "i ∈ I" "x ∈ 𝔸⇩i" for i x
    using universes_subsets sum_one_def mult_map_def that by simp
next 
  show "x →⇧i x = 1S" if "i ∈ I" "x ∈ 𝔸⇩i" for i x
    using universes_subsets imp_map_def sum_one_def that by simp
next
  show "x *⇧i (x →⇧i y) = y *⇧i (y →⇧i x)"
    if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for i x y z
    using divisibility universes_subsets imp_map_def mult_map_def that by simp
next 
  show "x →⇧i (y →⇧i z) = (x *⇧i y) →⇧i z"
    if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for i x y z
    using universes_subsets imp_map_def mult_map_def residuation that by simp
next 
  show "x ≤⇧i y ∨ y ≤⇧i x" if "i ∈ I" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using total_order universes_subsets imp_map_def sum_one_def that by simp
next
  show "∄ B C.
       (𝔸⇩i = B ∪ C) ∧
       ({1S} = B ∩ C) ∧
       (∃ y ∈ B. y ≠ 1S) ∧
       (∃ y ∈ C. y ≠ 1S) ∧ 
       (hoop B (*⇧i) (→⇧i) 1S) ∧
       (hoop C (*⇧i) (→⇧i) 1S) ∧
       (∀ x ∈ B-{1S}. ∀ y ∈ C. x *⇧i y = x) ∧
       (∀ x ∈ B-{1S}. ∀ y ∈ C. x →⇧i y = 1S) ∧
       (∀ x ∈ C. ∀ y ∈ B. x →⇧i y = y)"
    if "i ∈ I" for i
    using that Un_iff universes_one_fixed_hoops imp_map_def sum_one_def
          totally_ordered_one_fixed_hoop.one_fixed
    by metis
qed

lemma same_uni [simp]: "A_SUM.sum_univ = A"
  using A_SUM.sum_univ_def universes_cover by auto 

lemma floor_is_class:
  assumes "a ∈ A-{1A}"
  shows "A_SUM.floor a = π a"
proof -
  have "a ∈ π a ∧ π a ∈ I"
    using index_set_def assms classes_not_empty by fastforce
  then
  show ?thesis
    using same_uni A_SUM.floor_prop A_SUM.floor_unique UnCI assms universes_aux
          sum_one_def
    by metis
qed

lemma same_mult:
  assumes "a ∈ A" "b ∈ A"
  shows "a *A b = A_SUM.sum_mult a b"
proof -
  from assms
  consider (1) "a ∈ A-{1A}" "b ∈ A-{1A}" "A_SUM.floor a = A_SUM.floor b"
    | (2) "a ∈ A-{1A}" "b ∈ A-{1A}" "A_SUM.floor a <I A_SUM.floor b"
    | (3) "a ∈ A-{1A}" "b ∈ A-{1A}" "A_SUM.floor b <I A_SUM.floor a"
    | (4) "a = 1A ∨ b = 1A"
    using same_uni A_SUM.floor_prop fixed_points.cases sum_one_def trichotomy
    by metis
  then
  show ?thesis
  proof(cases)
    case 1 
    then
    show ?thesis
      using A_SUM.sum_mult.simps(1) sum_one_def mult_map_def by auto
  next
    case 2
    define i j where "i = A_SUM.floor a" and "j = A_SUM.floor b"
    then
    have "i ∈ I ∧ j ∈ I ∧ a ∈ (𝔸⇩i)-{1A} ∧ b ∈ (𝔸⇩j)-{1A}"
      using "2"(1,2) A_SUM.floor_prop sum_one_def by auto
    then
    have "a *A b = a"
      using "2"(3) different_indexes_mult i_def j_def by blast
    moreover
    have "A_SUM.sum_mult a b = a"
      using "2" A_SUM.sum_mult.simps(2) sum_one_def by simp
    ultimately
    show ?thesis
      by simp
  next
    case 3
    define i j where "i = A_SUM.floor a" and "j = A_SUM.floor b"
    then
    have "i ∈ I ∧ j ∈ I ∧ a ∈ (𝔸⇩i)-{1A} ∧ b ∈ (𝔸⇩j)-{1A}"
      using "3"(1,2) A_SUM.floor_prop sum_one_def by auto
    then
    have "a *A b = b"
      using "3"(3) assms different_indexes_mult i_def j_def mult_comm by metis
    moreover
    have "A_SUM.sum_mult a b = b"
      using "3" A_SUM.sum_mult.simps(3) sum_one_def by simp
    ultimately
    show ?thesis
      by simp
  next
    case 4
    then
    show ?thesis
      using A_SUM.mult_neutr A_SUM.mult_neutr_2 assms sum_one_def by force
  qed
qed

lemma same_imp:
  assumes "a ∈ A" "b ∈ A"
  shows "a →A b = A_SUM.sum_imp a b"
proof -
  from assms
  consider (1) "a ∈ A-{1A}" "b ∈ A-{1A}" "A_SUM.floor a = A_SUM.floor b"
    | (2) "a ∈ A-{1A}" "b ∈ A-{1A}" "A_SUM.floor a <I A_SUM.floor b"
    | (3) "a ∈ A-{1A}" "b ∈ A-{1A}" "A_SUM.floor b <I A_SUM.floor a"
    | (4) "a = 1A ∨ b = 1A"
    using same_uni A_SUM.floor_prop fixed_points.cases sum_one_def trichotomy
    by metis
  then
  show ?thesis
  proof(cases)
    case 1 
    then
    show ?thesis
      using A_SUM.sum_imp.simps(1) imp_map_def sum_one_def by auto
  next
    case 2
    define i j where "i = A_SUM.floor a" and "j = A_SUM.floor b"
    then
    have "i ∈ I ∧ j ∈ I ∧ a ∈ (𝔸⇩i)-{1A} ∧ b ∈ (𝔸⇩j)-{1A}"
      using "2"(1,2) A_SUM.floor_prop sum_one_def by simp
    then
    have "a →A b = 1A"
      using "2"(3) different_indexes_imp_1 i_def j_def by blast
    moreover
    have "A_SUM.sum_imp a b = 1A"
      using "2" A_SUM.sum_imp.simps(2) sum_one_def by simp
    ultimately
    show ?thesis
      by simp
  next
    case 3
    define i j where "i = A_SUM.floor a" and "j = A_SUM.floor b"
    then
    have "i ∈ I ∧ j ∈ I ∧ a ∈ (𝔸⇩i)-{1A} ∧ b ∈ (𝔸⇩j)-{1A}"
      using "3"(1,2) A_SUM.floor_prop sum_one_def by simp
    then
    have "a →A b = b"
      using "3"(3) different_indexes_imp_2 i_def j_def by blast
    moreover
    have "A_SUM.sum_imp a b = b"
      using "3" A_SUM.sum_imp.simps(3) sum_one_def by auto
    ultimately
    show ?thesis
      by simp
  next
    case 4
    then
    show ?thesis
      using A_SUM.imp_one_C A_SUM.imp_one_top assms imp_one_C
            imp_one_top sum_one_def
      by force
  qed
qed

lemma ordinal_sum_is_totally_ordered_hoop:
  "totally_ordered_hoop A_SUM.sum_univ A_SUM.sum_mult A_SUM.sum_imp 1S"
proof
  show "A_SUM.hoop_order x y ∨ A_SUM.hoop_order y x"
    if "x ∈ A_SUM.sum_univ" "y ∈ A_SUM.sum_univ" for x y
    using that A_SUM.hoop_order_def total_order hoop_order_def
          sum_one_def same_imp
    by auto
qed

theorem totally_ordered_hoop_is_equal_to_ordinal_sum_of_tower_of_irr_hoops: 
  shows eq_universe: "A = A_SUM.sum_univ"
  and eq_mult: "x ∈ A ⟹ y ∈ A ⟹ x *A y = A_SUM.sum_mult x y"
  and eq_imp: "x ∈ A ⟹ y ∈ A ⟹ x →A y = A_SUM.sum_imp x y"
  and eq_one: "1A = 1S"
proof
  show "A ⊆ A_SUM.sum_univ"
    by simp
next
  show "A_SUM.sum_univ ⊆ A"
    by simp
next
  show "x *A y = A_SUM.sum_mult x y" if "x ∈ A" "y ∈ A" for x y
    using same_mult that by blast
next
  show "x →A y = A_SUM.sum_imp x y" if "x ∈ A" "y ∈ A" for x y
    using same_imp that by blast
next 
  show "1A = 1S"
    using sum_one_def by simp
qed

subsubsection‹Remarks on the nontrivial case›

text‹In the nontrivial case we have that every totally ordered hoop
can be written as the ordinal sum of a tower of nontrivial irreducible hoops. The 
proof of this fact is almost immediate. By definition, @{text "𝔸π1A = {1A}"}
is the only trivial hoop in our tower. Moreover, @{text "𝔸πa"} is non-trivial for every
 @{text "a ∈ A-{1A}"}. Given that @{text "1A ∈ 𝔸i"} for every @{text "i ∈ I"}
 we can simply remove @{text "π 1A"} from @{text "I"} and obtain the desired result.›

lemma nontrivial_tower: 
  assumes "∃ x ∈ A. x ≠ 1A"
  shows
    "tower_of_nontrivial_irr_hoops (I-{π 1A}) (≤I) (<I) UNIA MULA IMPA 1S"
proof
  show "I-{π 1A} ≠ ∅"
  proof -
    obtain a where "a ∈ A-{1A}"
      using assms by blast
    then
    have "π a ∈ I-{π 1A}"
      using A_SUM.floor_prop class_not_one class_one floor_is_class sum_one_def by auto
    then
    show ?thesis
      by auto
  qed
next
  show "reflp_on (I-{π 1A}) (≤I)"
    using Diff_subset reflex reflp_on_subset by meson
next 
  show "antisymp_on (I-{π 1A}) (≤I)"
    using Diff_subset antisymm antisymp_on_subset by meson
next
  show "transp_on (I-{π 1A}) (≤I)"
    using Diff_subset trans transp_on_subset by meson
next
  show "i <I j = (i ≤I j ∧ i ≠ j)" if "i ∈ I-{π 1A}" "j ∈ I-{π 1A}" for i j
    using index_order_strict_def by simp
next
  show "totalp_on (I-{π 1A}) (≤I)"
    using Diff_subset total totalp_on_subset by meson
next
  show "(𝔸⇩i) ∩ (𝔸⇩j) = {1S}" if "i ∈ I-{π 1A}" "j ∈ I-{π 1A}" "i ≠ j" for i j
    using A_SUM.almost_disjoint that by blast
next
  show "x *⇧i y ∈ 𝔸⇩i" if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using A_SUM.floor_mult_closed that by blast
next 
  show "x →⇧i y ∈ 𝔸⇩i" if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using A_SUM.floor_imp_closed that by blast
next 
  show "1S ∈ 𝔸⇩i" if "i ∈ I-{π 1A}" for i
    using universes_one_closed sum_one_def that by simp
next
  show "x *⇧i y = y *⇧i x" if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using universes_subsets mult_comm mult_map_def that by force
next 
  show "x *⇧i (y *⇧i z) = (x *⇧i y) *⇧i z" 
    if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for i x y z
    using universes_subsets mult_assoc mult_map_def that by force
next 
  show "x *⇧i 1S = x" if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" for i x
    using universes_subsets sum_one_def mult_map_def that by force
next
  show "x →⇧i x = 1S" if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" for i x
    using universes_subsets imp_map_def sum_one_def that by force
next
  show "x *⇧i (x →⇧i y) = y *⇧i (y →⇧i x)"
    if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for i x y z
    using divisibility universes_subsets imp_map_def mult_map_def that by auto
next
  show "x →⇧i (y →⇧i z) = (x *⇧i y) →⇧i z"
    if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" "z ∈ 𝔸⇩i" for i x y z
    using universes_subsets imp_map_def mult_map_def residuation that by force
next
  show "x ≤⇧i y ∨ y ≤⇧i x" if "i ∈ I-{π 1A}" "x ∈ 𝔸⇩i" "y ∈ 𝔸⇩i" for i x y
    using DiffE total_order universes_subsets imp_map_def sum_one_def that by metis
next
  show "∄ B C.
       (𝔸⇩i = B ∪ C) ∧
       ({1S} = B ∩ C) ∧
       (∃ y ∈ B. y ≠ 1S) ∧
       (∃ y ∈ C. y ≠ 1S) ∧ 
       (hoop B (*⇧i) (→⇧i) 1S) ∧
       (hoop C (*⇧i) (→⇧i) 1S) ∧
       (∀ x ∈ B-{1S}. ∀ y ∈ C. x *⇧i y = x) ∧
       (∀ x ∈ B-{1S}. ∀ y ∈ C. x →⇧i y = 1S) ∧
       (∀ x ∈ C. ∀ y ∈ B. x →⇧i y = y)"
    if "i ∈ I-{π 1A}" for i
    using that Diff_iff Un_iff universes_one_fixed imp_map_def sum_one_def by metis
next
  show "∃ x ∈ 𝔸⇩i. x ≠ 1S" if "i ∈ I-{π 1A}" for i 
    using universes_def indexes_class_of_elements indexes_not_empty that
    by fastforce
qed

lemma ordinal_sum_of_nontrivial: 
  assumes "∃ x ∈ A. x ≠ 1A"
  shows "A_SUM.sum_univ = {x. ∃ i ∈ I-{π 1A}. x ∈ 𝔸⇩i}"
proof
  show "A_SUM.sum_univ ⊆ {x. ∃ i ∈ I-{π 1A}. x ∈ 𝔸⇩i}"
  proof 
    fix a 
    assume "a ∈ A_SUM.sum_univ"
    then
    consider (1) "a ∈ A-{1A}"
      | (2) "a = 1A"
      by auto
    then
    show "a ∈ {x. ∃ i ∈ I-{π 1A}. x ∈ 𝔸⇩i}"
    proof(cases)
      case 1 
      then
      obtain i where "i = π a"
        by simp
      then
      have "a ∈ 𝔸⇩i ∧ i ∈ I-{π 1A}"
        using "1" A_SUM.floor_prop class_not_one class_one floor_is_class sum_one_def
        by auto
      then
      show ?thesis
        by blast
    next
      case 2
      obtain c where "c ∈ A-{1A}"
        using assms by blast
      then
      obtain i where "i = π c"
        by simp
      then
      have "a ∈ 𝔸⇩i ∧ i ∈ I-{π 1A}"
        using "2" A_SUM.floor_prop ‹c ∈ A-{1A}› class_not_one class_one
              universes_one_closed floor_is_class sum_one_def
        by auto
      then
      show ?thesis
        by auto
    qed
  qed
next
  show "{x. ∃ i ∈ I-{π 1A}. x ∈ 𝔸⇩i} ⊆ A_SUM.sum_univ"
    using universes_subsets by force
qed

end

subsubsection‹Converse of main result›

text‹We show that the converse of the main result also holds, that is,
the ordinal sum of a tower of irreducible hoops is a totally ordered hoop.›

context tower_of_irr_hoops
begin

proposition ordinal_sum_of_tower_of_irr_hoops_is_totally_ordered_hoop:
  shows "totally_ordered_hoop S (*S) (→S) 1S"
proof 
  show "hoop_order a b ∨ hoop_order b a" if "a ∈ S" "b ∈ S" for a b
  proof - 
    from that
    consider (1) "a ∈ S-{1S}" "b ∈ S-{1S}" "floor a = floor b"
      | (2) "a ∈ S-{1S}" "b ∈ S-{1S}" "floor a <I floor b ∨ floor b <I floor a"
      | (3) "a = 1S ∨ b = 1S"
      using floor.cases floor_prop trichotomy by metis
    then
    show "hoop_order a b ∨ hoop_order b a"
    proof(cases)
      case 1
      then
      have "a ∈ 𝔸floor ⇩a ∧ b ∈ 𝔸floor ⇩a"
        using "1" floor_prop by metis
      moreover
      have "totally_ordered_hoop (𝔸floor ⇩a) (*floor ⇧a) (→floor ⇧a) 1S"
        using "1"(1) family_of_irr_hoops totally_ordered_irreducible_hoop.axioms(1)
              floor_prop
        by meson
      ultimately
      have "a →floor ⇧a b = 1S ∨ b →floor ⇧a a = 1S"
        using hoop.hoop_order_def totally_ordered_hoop.total_order
              totally_ordered_hoop_def
        by meson
      moreover
      have "a →S b = a →floor ⇧a b ∧ b →S a = b →floor ⇧a a"
        using "1" by auto
      ultimately
      show ?thesis
        using hoop_order_def by force
    next
      case 2
      then
      show ?thesis
        using sum_imp.simps(2) hoop_order_def by blast
    next
      case 3
      then
      show ?thesis
        using that ord_top by auto
    qed
  qed
qed

end

end