Theory Hoops

section‹Hoops›

text‹A @{text hoop} is a naturally ordered @{text "pocrim"} (i.e., a partially ordered commutative
 residuated integral monoid). This structures have been introduced by Büchi and Owens in \<^cite>‹"BUCHI1975"›
and constitute the algebraic counterpart of fragments without negation and falsum of some nonclassical logics.›

theory Hoops
  imports Posets
begin

subsection‹Definitions›

locale hoop =
  fixes universe :: "'a set" (‹A›)
  and multiplication :: "'a ⇒ 'a ⇒ 'a" (infix ‹*⇧^A› 60)
  and implication :: "'a ⇒ 'a ⇒ 'a" (infix ‹→⇧^A› 60)
  and one :: 'a (‹1⇧^A›)
  assumes mult_closed: "x ∈ A ⟹ y ∈ A ⟹ x *⇧^A y ∈ A"
  and imp_closed: "x ∈ A ⟹ y ∈ A ⟹ x →⇧^A y ∈ A"
  and one_closed [simp]: "1⇧^A ∈ A"
  and mult_comm:  "x ∈ A ⟹ y ∈ A ⟹ x *⇧^A y = y *⇧^A x"
  and mult_assoc: "x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹ x *⇧^A (y *⇧^A z) = (x *⇧^A y) *⇧^A z"
  and mult_neutr [simp]: "x ∈ A ⟹ x *⇧^A 1⇧^A = x" 
  and imp_reflex [simp]: "x ∈ A ⟹ x →⇧^A x = 1⇧^A" 
  and divisibility: "x ∈ A ⟹ y ∈ A ⟹ x *⇧^A (x →⇧^A y) = y *⇧^A (y →⇧^A x)" 
  and residuation: "x ∈ A ⟹ y ∈ A ⟹ z ∈ A ⟹
                    x →⇧^A (y →⇧^A z) = (x *⇧^A y) →⇧^A z"
begin

definition hoop_order :: "'a ⇒ 'a ⇒ bool" (infix ‹≤⇧^A› 60)
  where "x ≤⇧^A y ≡ (x →⇧^A y = 1⇧^A)" 

definition hoop_order_strict :: "'a ⇒ 'a ⇒ bool" (infix ‹<⇧^A› 60)
  where "x <⇧^A y ≡ (x ≤⇧^A y ∧ x ≠ y)"

definition hoop_inf :: "'a ⇒ 'a ⇒ 'a" (infix ‹∧⇧^A› 60)
  where "x ∧⇧^A y = x *⇧^A (x →⇧^A y)"

definition hoop_pseudo_sup :: "'a ⇒ 'a ⇒ 'a" (infix ‹∨⇧^*⇧^A› 60)
  where "x ∨⇧^*⇧^A y = ((x →⇧^A y) →⇧^A y) ∧⇧^A ((y →⇧^A x) →⇧^A x)" 

end

locale wajsberg_hoop = hoop +
  assumes T: "x ∈ A ⟹ y ∈ A ⟹ (x →⇧^A y) →⇧^A y = (y →⇧^A x) →⇧^A x"
begin

definition wajsberg_hoop_sup :: "'a ⇒ 'a ⇒ 'a" (infix ‹∨⇧^A› 60)
  where "x ∨⇧^A y = (x →⇧^A y) →⇧^A y"

end

subsection‹Basic properties›

context hoop
begin

lemma mult_neutr_2 [simp]: 
  assumes "a ∈ A"
  shows "1⇧^A *⇧^A a = a"
  using assms mult_comm by simp

lemma imp_one_A:
  assumes "a ∈ A"
  shows "(1⇧^A →⇧^A a) →⇧^A 1⇧^A = 1⇧^A"
proof -
  have "(1⇧^A →⇧^A a) →⇧^A 1⇧^A = (1⇧^A →⇧^A a) →⇧^A (1⇧^A →⇧^A 1⇧^A)"
    using assms by simp
  also
  have "… = ((1⇧^A →⇧^A a) *⇧^A 1⇧^A) →⇧^A 1⇧^A"
    using assms imp_closed residuation by simp
  also
  have "… = ((a →⇧^A 1⇧^A) *⇧^A a) →⇧^A 1⇧^A"
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (a →⇧^A 1⇧^A) →⇧^A (a →⇧^A 1⇧^A)"
    using assms imp_closed one_closed residuation by metis
  also
  have "… = 1⇧^A"
    using assms imp_closed by simp
  finally
  show ?thesis 
    by auto
qed

lemma imp_one_B:
  assumes "a ∈ A"
  shows "(1⇧^A →⇧^A a) →⇧^A a = 1⇧^A"
proof -
  have "(1⇧^A →⇧^A a) →⇧^A a = ((1⇧^A →⇧^A a) *⇧^A 1⇧^A) →⇧^A a"
    using assms imp_closed by simp
  also
  have "… = (1⇧^A →⇧^A a) →⇧^A (1⇧^A →⇧^A a)" 
    using assms imp_closed one_closed residuation by metis
  also
  have "… = 1⇧^A"
    using assms imp_closed by simp
  finally
  show ?thesis
    by auto
qed

lemma imp_one_C:
  assumes "a ∈ A"
  shows "1⇧^A →⇧^A a = a" 
proof -
  have "1⇧^A →⇧^A a = (1⇧^A →⇧^A a) *⇧^A 1⇧^A" 
    using assms imp_closed by simp
  also
  have "… = (1⇧^A →⇧^A a) *⇧^A ((1⇧^A →⇧^A a) →⇧^A a)" 
    using assms imp_one_B by simp
  also
  have "… = a *⇧^A (a →⇧^A (1⇧^A →⇧^A a))" 
    using assms divisibility imp_closed by simp
  also
  have "… = a" 
    using assms residuation by simp
  finally
  show ?thesis
    by auto
qed

lemma imp_one_top:
  assumes "a ∈ A"
  shows "a →⇧^A 1⇧^A = 1⇧^A"
proof -
  have "a →⇧^A 1⇧^A = (1⇧^A →⇧^A a) →⇧^A 1⇧^A"
    using assms imp_one_C by auto
  also
  have "… = 1⇧^A"
    using assms imp_one_A by auto
  finally
  show ?thesis
    by auto
qed

text‹The proofs of @{thm [source] imp_one_A}, @{thm [source] imp_one_B}, @{thm [source] imp_one_C}
and  @{thm [source] imp_one_top} are based on proofs found in \<^cite>‹"BOSBACH1969"›
 (see Section 1: (4), (6), (7) and (12)).›
 
lemma swap: 
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "a →⇧^A (b →⇧^A c) = b →⇧^A (a →⇧^A c)"
proof -
  have "a →⇧^A (b →⇧^A c) = (a *⇧^A b) →⇧^A c"
    using assms residuation by auto
  also
  have "… = (b *⇧^A a) →⇧^A c"
    using assms mult_comm by auto
  also
  have "… = b →⇧^A (a →⇧^A c)"
    using assms residuation by auto
  finally
  show ?thesis
    by auto
qed

lemma imp_A:
  assumes "a ∈ A" "b ∈ A"
  shows "a →⇧^A (b →⇧^A a) = 1⇧^A"
proof -
  have "a →⇧^A (b →⇧^A a) = b →⇧^A (a →⇧^A a)"
    using assms swap by blast
  then
  show ?thesis
    using assms imp_one_top by simp
qed

subsection‹Multiplication monotonicity›

lemma mult_mono:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →⇧^A b) →⇧^A ((a *⇧^A c) →⇧^A (b *⇧^A c)) = 1⇧^A"
proof -
  have "(a →⇧^A b) →⇧^A ((a *⇧^A c) →⇧^A (b *⇧^A c)) =
        (a →⇧^A b) →⇧^A (a →⇧^A (c →⇧^A (b *⇧^A c)))"
    using assms mult_closed residuation by auto
  also
  have "… = ((a →⇧^A b) *⇧^A a) →⇧^A (c →⇧^A (b *⇧^A c))"
    using assms imp_closed mult_closed residuation by metis
  also
  have "… = ((b →⇧^A a) *⇧^A b) →⇧^A (c →⇧^A (b *⇧^A c))"
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (b →⇧^A a) →⇧^A (b →⇧^A (c →⇧^A (b *⇧^A c)))"
    using assms imp_closed mult_closed residuation by metis
  also
  have "… = (b →⇧^A a) →⇧^A ((b *⇧^A c) →⇧^A (b *⇧^A c))" 
    using assms(2,3) mult_closed residuation by simp
  also
  have "… = 1⇧^A"
    using assms imp_closed imp_one_top mult_closed by simp
  finally
  show ?thesis
    by auto
qed

subsection‹Implication monotonicity and anti-monotonicity›

lemma imp_mono:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →⇧^A b) →⇧^A ((c →⇧^A a) →⇧^A (c →⇧^A b)) = 1⇧^A"
proof -
  have "(a →⇧^A b) →⇧^A ((c →⇧^A a) →⇧^A (c →⇧^A b)) =
        (a →⇧^A b) →⇧^A (((c →⇧^A a) *⇧^A c) →⇧^A b)" 
    using assms imp_closed residuation by simp
  also
  have "… = (a →⇧^A b) →⇧^A (((a →⇧^A c) *⇧^A a) →⇧^A b)" 
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (a →⇧^A b) →⇧^A ((a →⇧^A c) →⇧^A (a →⇧^A b))" 
    using assms imp_closed residuation by simp
  also
  have "… = 1⇧^A" 
    using assms imp_A imp_closed by simp
  finally
  show ?thesis
    by auto
qed

lemma imp_anti_mono:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →⇧^A b) →⇧^A ((b →⇧^A c) →⇧^A (a →⇧^A c)) = 1⇧^A"
  using assms imp_closed imp_mono swap by metis

subsection‹@{term hoop_order} defines a partial order over @{term A}›

lemma ord_reflex: 
  assumes "a ∈ A"
  shows "a ≤⇧^A a"
  using assms hoop_order_def by simp

lemma ord_trans:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤⇧^A b" "b ≤⇧^A c"
  shows "a ≤⇧^A c"
proof -
  have "a →⇧^A c = 1⇧^A →⇧^A (1⇧^A →⇧^A (a →⇧^A c))"
    using assms(1,3) imp_closed imp_one_C by simp
  also
  have "… = (a →⇧^A b) →⇧^A ((b →⇧^A c) →⇧^A (a →⇧^A c))"
    using assms(4,5) hoop_order_def by simp
  also
  have "… = 1⇧^A"
    using assms(1-3) imp_anti_mono by simp
  finally
  show ?thesis
    using hoop_order_def by auto
qed

lemma ord_antisymm:
  assumes "a ∈ A" "b ∈ A" "a ≤⇧^A b" "b ≤⇧^A a"
  shows "a = b"
proof -
  have "a = a *⇧^A (a →⇧^A b)"
    using assms(1,3) hoop_order_def by simp
  also
  have "… = b *⇧^A (b →⇧^A a)" 
    using assms(1,2) divisibility by simp
  also
  have "… = b"
    using assms(2,4) hoop_order_def by simp
  finally
  show ?thesis
    by auto
qed

lemma ord_antisymm_equiv:
  assumes "a ∈ A" "b ∈ A" "a →⇧^A b = 1⇧^A" "b →⇧^A a = 1⇧^A"
  shows "a = b"
  using assms hoop_order_def ord_antisymm by auto

lemma ord_top:
  assumes "a ∈ A"
  shows "a ≤⇧^A 1⇧^A"
  using assms hoop_order_def imp_one_top by simp

sublocale top_poset_on "A" "(≤⇧^A)" "(<⇧^A)" "1⇧^A"
proof
  show "A ≠ ∅"
    using one_closed by blast
next
  show "reflp_on A (≤⇧^A)"
    using ord_reflex reflp_onI by blast
next
  show "antisymp_on A (≤⇧^A)"
    using antisymp_onI ord_antisymm by blast
next 
  show "transp_on A (≤⇧^A)"
    using ord_trans transp_onI by blast
next
  show "x <⇧^A y = (x ≤⇧^A y ∧ x ≠ y)" if "x ∈ A" "y ∈ A" for x y
    using hoop_order_strict_def by blast
next
  show "1⇧^A ∈ A"
    by simp
next
  show "x ≤⇧^A 1⇧^A" if "x ∈ A" for x
    using ord_top that by simp
qed
 
subsection‹Order properties›

lemma ord_mult_mono_A:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →⇧^A b) ≤⇧^A ((a *⇧^A c) →⇧^A (b *⇧^A c))"
  using assms hoop_order_def mult_mono by simp

lemma ord_mult_mono_B:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤⇧^A b"
  shows "(a *⇧^A c) ≤⇧^A (b *⇧^A c)"
  using assms hoop_order_def imp_one_C swap mult_closed mult_mono top_closed
  by metis

lemma ord_residuation:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a *⇧^A b) ≤⇧^A c ⟷ a ≤⇧^A (b →⇧^A c)"
  using assms hoop_order_def residuation by simp

lemma ord_imp_mono_A:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →⇧^A b) ≤⇧^A ((c →⇧^A a) →⇧^A (c →⇧^A b))"
  using assms hoop_order_def imp_mono by simp

lemma ord_imp_mono_B:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤⇧^A b"
  shows "(c →⇧^A a) ≤⇧^A (c →⇧^A b)"
  using assms imp_closed ord_trans ord_reflex ord_residuation mult_closed
  by metis

lemma ord_imp_anti_mono_A:
  assumes "a ∈ A" "b ∈ A" "c ∈ A"
  shows "(a →⇧^A b) ≤⇧^A ((b →⇧^A c) →⇧^A (a →⇧^A c))"
  using assms hoop_order_def imp_anti_mono by simp

lemma ord_imp_anti_mono_B:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤⇧^A b"
  shows "(b →⇧^A c) ≤⇧^A (a →⇧^A c)"
  using assms hoop_order_def imp_one_C swap ord_imp_mono_A top_closed
  by metis

lemma ord_A:
  assumes "a ∈ A" "b ∈ A"
  shows "b ≤⇧^A (a →⇧^A b)"
  using assms hoop_order_def imp_A by simp

lemma ord_B:
  assumes "a ∈ A" "b ∈ A"
  shows "b ≤⇧^A ((a →⇧^A b) →⇧^A b)"
  using assms imp_closed ord_A by simp

lemma ord_C:
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤⇧^A ((a →⇧^A b) →⇧^A b)"
  using assms imp_one_C one_closed ord_imp_anti_mono_A by metis

lemma ord_D:
  assumes "a ∈ A" "b ∈ A" "a <⇧^A b"
  shows "b →⇧^A a ≠ 1⇧^A"
  using assms hoop_order_def hoop_order_strict_def ord_antisymm by auto

subsection‹Additional multiplication properties›

lemma mult_lesseq_inf:
  assumes "a ∈ A" "b ∈ A"
  shows "(a *⇧^A b) ≤⇧^A (a ∧⇧^A b)"
proof -
  have "b ≤⇧^A (a →⇧^A b)"
    using assms ord_A by simp
  then
  have "(a *⇧^A b) ≤⇧^A (a *⇧^A (a →⇧^A b))"
    using assms imp_closed ord_mult_mono_B mult_comm by metis
  then
  show ?thesis
    using hoop_inf_def by metis
qed

lemma mult_A:
  assumes "a ∈ A" "b ∈ A"
  shows "(a *⇧^A b) ≤⇧^A a"
  using assms ord_A ord_residuation by simp

lemma mult_B:
  assumes "a ∈ A" "b ∈ A"
  shows "(a *⇧^A b) ≤⇧^A b"
  using assms mult_A mult_comm by metis

lemma mult_C:
  assumes "a ∈ A-{1⇧^A}" "b ∈ A-{1⇧^A}"
  shows "a *⇧^A b ∈ A-{1⇧^A}"
  using assms ord_antisymm ord_top mult_A mult_closed by force

subsection‹Additional implication properties›

lemma imp_B:
  assumes "a ∈ A" "b ∈ A"
  shows "a →⇧^A b = ((a →⇧^A b) →⇧^A b) →⇧^A b"
proof -
  have "a ≤⇧^A ((a →⇧^A b) →⇧^A b)"
    using assms ord_C by simp
  then 
  have "(((a →⇧^A b) →⇧^A b) →⇧^A b) ≤⇧^A (a →⇧^A b)"
    using assms imp_closed ord_imp_anti_mono_B by simp
  moreover
  have "(a →⇧^A b) ≤⇧^A (((a →⇧^A b) →⇧^A b) →⇧^A b)"
    using assms imp_closed ord_C by simp
  ultimately
  show ?thesis
    using assms imp_closed ord_antisymm by simp
qed

text‹The following two results can be found in \<^cite>‹"BLOK2000"› (see Proposition 1.7 and 2.2).›

lemma imp_C:
  assumes "a ∈ A" "b ∈ A"
  shows "(a →⇧^A b) →⇧^A (b →⇧^A a) = b →⇧^A a"
proof -
  have "a ≤⇧^A ((a →⇧^A b) →⇧^A a)"
    using assms imp_closed ord_A by simp
  then
  have "(((a →⇧^A b) →⇧^A a) →⇧^A b) ≤⇧^A (a →⇧^A b)"
    using assms imp_closed ord_imp_anti_mono_B by simp
  moreover 
  have "(a →⇧^A b) ≤⇧^A (((a →⇧^A b) →⇧^A a) →⇧^A a)"
    using assms imp_closed ord_C by simp
  ultimately
  have "(((a →⇧^A b) →⇧^A a) →⇧^A b) ≤⇧^A (((a →⇧^A b) →⇧^A a) →⇧^A a)"
    using assms imp_closed ord_trans by meson
  then
  have "((((a →⇧^A b) →⇧^A a) →⇧^A b) *⇧^A ((a →⇧^A b) →⇧^A a)) ≤⇧^A a"
    using assms imp_closed ord_residuation by simp
  then
  have "((b →⇧^A ((a →⇧^A b) →⇧^A a)) *⇧^A b) ≤⇧^A a"
    using assms divisibility imp_closed mult_comm by simp
  then
  have "(b →⇧^A ((a →⇧^A b) →⇧^A a)) ≤⇧^A (b →⇧^A a)"
    using assms imp_closed ord_residuation by simp
  then 
  have "((a →⇧^A b) →⇧^A (b →⇧^A a)) ≤⇧^A (b →⇧^A a)"
    using assms imp_closed swap by simp
  moreover
  have "(b →⇧^A a) ≤⇧^A ((a →⇧^A b) →⇧^A (b →⇧^A a))"
    using assms imp_closed ord_A by simp
  ultimately
  show ?thesis
    using assms imp_closed ord_antisymm by auto
qed

lemma imp_D:
  assumes "a ∈ A" "b ∈ A"
  shows "(((b →⇧^A a) →⇧^A a) →⇧^A b) →⇧^A (b →⇧^A a) = b →⇧^A a"
proof -
  have "(((b →⇧^A a) →⇧^A a) →⇧^A b) →⇧^A (b →⇧^A a) =
        (((b →⇧^A a) →⇧^A a) →⇧^A b) →⇧^A (((b →⇧^A a) →⇧^A a) →⇧^A a)" 
    using assms imp_B by simp
  also
  have "… = ((((b →⇧^A a) →⇧^A a) →⇧^A b) *⇧^A ((b →⇧^A a) →⇧^A a)) →⇧^A a" 
    using assms imp_closed residuation by simp
  also
  have "… = ((b →⇧^A ((b →⇧^A a) →⇧^A a)) *⇧^A b) →⇧^A a" 
    using assms divisibility imp_closed mult_comm by simp
  also
  have "… = (1⇧^A *⇧^A b) →⇧^A a"
    using assms hoop_order_def ord_C by simp
  also
  have "… = b →⇧^A a"
    using assms(2) mult_neutr_2 by simp
  finally
  show ?thesis
    by auto
qed

subsection‹@{term hoop_inf} defines a semilattice over @{term A}›

lemma inf_closed:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∧⇧^A b ∈ A"
  using assms hoop_inf_def imp_closed mult_closed by simp

lemma inf_comm:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∧⇧^A b = b ∧⇧^A a"
  using assms divisibility hoop_inf_def by simp

lemma inf_A:
  assumes "a ∈ A" "b ∈ A"
  shows "(a ∧⇧^A b) ≤⇧^A a"
proof -
  have "(a ∧⇧^A b) →⇧^A a = (a *⇧^A (a →⇧^A b)) →⇧^A a"
    using hoop_inf_def by simp
  also
  have "… = (a →⇧^A b) →⇧^A (a →⇧^A a)"
    using assms mult_comm imp_closed residuation by metis
  finally
  show ?thesis
    using assms hoop_order_def imp_closed imp_one_top by simp
qed

lemma inf_B:
  assumes "a ∈ A" "b ∈ A"
  shows "(a ∧⇧^A b) ≤⇧^A b" 
  using assms inf_comm inf_A by metis

lemma inf_C:
  assumes "a ∈ A" "b ∈ A" "c ∈ A" "a ≤⇧^A b" "a ≤⇧^A c"
  shows "a ≤⇧^A (b ∧⇧^A c)"
proof -
  have "(b →⇧^A a) ≤⇧^A (b →⇧^A c)"
    using assms(1-3,5) ord_imp_mono_B by simp
  then
  have "(b *⇧^A (b →⇧^A a)) ≤⇧^A (b *⇧^A (b →⇧^A c))"
    using assms imp_closed ord_mult_mono_B mult_comm by metis
  moreover
  have "a = b *⇧^A (b →⇧^A a)"
    using assms(1-3,4) divisibility hoop_order_def mult_neutr by simp
  ultimately
  show ?thesis
    using hoop_inf_def by auto
qed

lemma inf_order: 
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤⇧^A b ⟷ (a ∧⇧^A b = a)"
  using assms hoop_inf_def hoop_order_def inf_B mult_neutr by metis

subsection‹Properties of @{term hoop_pseudo_sup}›

lemma pseudo_sup_closed:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∨⇧^*⇧^A b ∈ A"
  using assms hoop_pseudo_sup_def imp_closed inf_closed by simp

lemma pseudo_sup_comm:
  assumes "a ∈ A" "b ∈ A"
  shows "a ∨⇧^*⇧^A b = b ∨⇧^*⇧^A a"
  using assms hoop_pseudo_sup_def imp_closed inf_comm by auto

lemma pseudo_sup_A:
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤⇧^A (a ∨⇧^*⇧^A b)"
  using assms hoop_pseudo_sup_def imp_closed inf_C ord_B ord_C by simp

lemma pseudo_sup_B:
  assumes "a ∈ A" "b ∈ A"
  shows "b ≤⇧^A (a ∨⇧^*⇧^A b)"
  using assms pseudo_sup_A pseudo_sup_comm by metis

lemma pseudo_sup_order:
  assumes "a ∈ A" "b ∈ A"
  shows "a ≤⇧^A b ⟷ a ∨⇧^*⇧^A b = b"
proof
  assume "a ≤⇧^A b"
  then 
  have "a ∨⇧^*⇧^A b = b ∧⇧^A ((b →⇧^A a) →⇧^A a)"
    using assms(2) hoop_order_def hoop_pseudo_sup_def imp_one_C by simp
  also
  have "… = b"
    using assms imp_closed inf_order ord_C by meson
  finally
  show "a ∨⇧^*⇧^A b = b"
    by auto
next
  assume "a ∨⇧^*⇧^A b = b"
  then
  show "a ≤⇧^A b"
    using assms pseudo_sup_A by metis
qed

end

end