Theory Power_Allegories_Properties

section ‹Properties of Power Allegories›

theory Power_Allegories_Properties

imports Relational_Properties

begin

subsection ‹Power transpose, epsilon, epsiloff›

definition Lambda :: "('a,'b) rel ⇒ ('a,'b set) rel" (‹Λ›) where
  "Λ R = {(a,B) |a B. B = {b. (a,b) ∈ R}}"

definition epsilon :: "('a,'a set) rel" where
  "epsilon = {(a,A). a ∈ A}"

definition "epsiloff = {(A,a). a ∈ A}"

definition alpha :: "('a,'b set) rel ⇒ ('a,'b) rel" (‹α›) where
  "α R = R ; epsiloff"

text ‹alpha can be seen as a relational approximation of a multirelation.
The next lemma provides a relational definition of Lambda.›

lemma Lambda_syq: "Λ R = R⇧⌣ ÷ epsilon"
  unfolding Lambda_def syq_set epsilon_def by blast

lemma epsiloff_epsilon: "epsiloff = epsilon⇧⌣"
  unfolding epsiloff_def epsilon_def converse_unfold by simp

lemma alpha_set: "α R = {(a,b) |a b. b ∈ ⋃{B. (a,B) ∈ R}}"
  unfolding alpha_def epsiloff_def by force

lemma alpha_relcomp [simp]: "α (R ; S) = R ; α S"
  by (simp add: O_assoc alpha_def)

lemma Lambda_epsiloff_up1: "f = Λ R ⟹ R = α f"
  unfolding Lambda_def alpha_set by simp

lemma Lambda_epsiloff_up2: "deterministic f ⟹ R = α f ⟹ f = Λ R"
  unfolding Lambda_def alpha_set deterministic_set
  apply safe
  apply force
  by (clarsimp, smt (verit, best) mem_Collect_eq set_eq_iff)

lemma Lambda_epsiloff_up:
  assumes "deterministic f"
  shows "(R = α f) = (f = Λ R)"
  by (meson Lambda_epsiloff_up1 Lambda_epsiloff_up2 assms)

lemma det_lambda: "deterministic (Λ R)"
  unfolding Lambda_def deterministic_set by simp

lemma Lambda_alpha_canc: "deterministic f ⟹ Λ (α f) = f"
  using Lambda_epsiloff_up2 by blast

lemma alpha_Lambda_canc [simp]: "α (Λ R) = R"
  using Lambda_epsiloff_up1 by blast

lemma alpha_cancel:
  assumes "deterministic f"
  and "deterministic g"
  shows "α f = α g ⟹ f = g"
  by (metis Lambda_epsiloff_up2 assms)

lemma Lambda_fusion:
  assumes "deterministic f"
  shows "Λ (f ; R) = f ; Λ R"
proof -
  have h: "deterministic (f ; Λ R)"
    by (simp add: assms det_lambda det_relcomp)
  have "f ; R = α (f ; Λ R)"
    by simp
  also have "… = f ; α (Λ R)"
    by simp
  thus ?thesis
    by (simp add: alpha_cancel det_lambda h)
qed

lemma Lambda_fusion_var: "Λ (Λ R ; S) = Λ R ; Λ S"
  by (simp add: Lambda_fusion det_lambda)

lemma Lambda_epsiloff [simp]: "Λ epsiloff = Id"
proof -
  have "Λ epsiloff = Λ (Id ; epsiloff)"
    by simp
  also have "… = Id"
    by (metis Lambda_epsiloff_up alpha_def det_Id)
  finally show ?thesis.
qed

lemma alpha_epsiloff [simp]: "α Id = epsiloff"
  by (simp add: alpha_def)

lemma alpha_Sup_pres: "α (⋃ℛ) = (⋃R ∈ ℛ. α R)"
  unfolding alpha_def by force

lemma alpha_ord_pres: "R ⊆ S ⟹ alpha R ⊆ alpha S"
  unfolding alpha_def by force

lemma alpha_inf_pres: "α {(a,A). ∃B C. A = B ∩ C ∧ (a,B) ∈ R ∧ (a,C) ∈ S} = α R ∩ α S"
  unfolding alpha_set by blast


subsection ‹Relational image functor›

definition pow :: "('a, 'b) rel ⇒ ('a set, 'b set) rel" (‹𝒫›) where
  "𝒫 R = Λ (epsiloff ; R)"

lemma pow_set: "𝒫 R = {(A,B). B = Image R A}"
  unfolding pow_def epsiloff_def Lambda_def relcomp_def Image_def by force

lemma pow_set_var: "𝒫 R = {(A,B). B = {b. ∃a ∈ A. (a,b) ∈ R}}"
  unfolding pow_set Image_def by simp

lemma pow_converse_set: "𝒫 (R⇧⌣) = {(Q,P). P = {a. ∃b. (a,b) ∈ R ∧ b ∈ Q}}"
  unfolding pow_set Image_def by force

lemma det_pow: "deterministic (𝒫 R)"
  unfolding pow_set deterministic_set Image_def by simp

lemma Lambda_pow: "Λ (R ; S) = Λ R ; 𝒫 S"
proof -
  have "Λ R ; 𝒫 S = Λ R ; Λ (epsiloff ; S)"
    by (simp add: pow_def)
  also have "… = Λ (Λ R ; epsiloff ; S)"
    by (simp add: Lambda_fusion_var O_assoc)
  also have "… = Λ (R ; S)"
    by (metis alpha_Lambda_canc alpha_def)
  finally show ?thesis..
qed

lemma pow_func1 [simp]: "𝒫 Id = Id"
  by (simp add: pow_def)

lemma pow_func2: "𝒫 (R ; S) = 𝒫 R ; 𝒫 S"
  by (metis Lambda_pow pow_def O_assoc)

lemma Grph_Image [simp]: "Grph ∘ Image = 𝒫"
  apply (simp add: fun_eq_iff)
  unfolding pow_def Grph_def Image_def Lambda_def epsiloff_def by blast

lemma lambda_alpha_idem [simp]: "Λ (α (Λ (α R))) = Λ (α R)"
  by simp


subsection ‹Unit and multiplication of powerset monad›

definition eta :: "('a,'a set) rel" (‹η›) where
  "η = Λ Id"

definition mu :: "('a set set, 'a set) rel" (‹μ›) where
  "μ = pow epsiloff"

lemma eta_set: "η = {(a,{a}) |a. True}"
  unfolding eta_def Lambda_def Id_def by simp

lemma alpha_eta [simp]: "α η = Id"
  by (simp add: eta_def)

lemma det_eta: "deterministic η"
  unfolding deterministic_set eta_set by simp

lemma mu_set: "μ = {(A,B). B = {b. ∃C. C ∈ A ∧ b ∈ C}}"
  unfolding mu_def pow_def Lambda_def epsiloff_def by force

lemma det_mu: "deterministic μ"
  unfolding deterministic_set mu_set by simp

lemma Lambda_eta:
  assumes "deterministic R"
  shows "Λ R = R ; η"
proof -
  have "Λ R = Λ (R ; Id)"
    by simp
  also have "… = R ; Λ Id"
    using Lambda_fusion assms by blast
  also have "… = R ; η"
    by (simp add: eta_def)
  finally show ?thesis.
qed

lemma eta_nat_trans:
  assumes "deterministic R"
  shows "η ; 𝒫 R = R ; η"
proof -
  have "η ; 𝒫 R = Λ Id ; 𝒫 R"
    by (simp add: eta_def)
  also have "… = Λ (Id ; R)"
    using Lambda_pow by blast
  also have "… = Λ R"
    by simp
  also have "… = R ; η"
    by (simp add: Lambda_eta assms)
  finally show ?thesis.
qed

lemma mu_nat_trans:
  assumes "deterministic R"
  shows "𝒫 (𝒫 R) ; μ = μ ; 𝒫 R"
  by (metis pow_def alpha_Lambda_canc alpha_def mu_def pow_func2)

text ‹The standard axioms for the powerset monad are derivable.›

lemma pow_monad1 [simp]: "𝒫 μ ; μ = μ ; μ"
  by (metis pow_def alpha_Lambda_canc alpha_def mu_def pow_func2)

lemma pow_monad2 [simp]: "𝒫 η ; μ = Id"
  by (metis alpha_Lambda_canc alpha_def eta_def mu_def pow_func1 pow_func2)

lemma pow_monad3 [simp]: "η ; μ = Id"
  by (metis Lambda_epsiloff Lambda_pow alpha_def alpha_epsiloff eta_def mu_def)

lemma Lambda_mu:
  assumes "deterministic R"
  shows "Λ(R) ; μ = R"
proof -
  have "Λ R ; μ = R ; η ; μ"
    by (simp add: Lambda_eta assms)
  also have "… = R"
    by (simp add: O_assoc)
  finally show ?thesis.
qed

lemma pow_Lambda_mu [simp]: "𝒫 (Λ R) ; μ = 𝒫 R"
  by (metis alpha_Lambda_canc alpha_def mu_def pow_func2)

lemma lambda_alpha_mu: "Λ (α R) = Λ R ; μ"
  by (simp add: Lambda_pow alpha_def mu_def)

lemma alpha_eta_pow [simp]: "α (η ; 𝒫 R) = R"
proof -
  have "α (η ; 𝒫 R) = α (Λ Id ; 𝒫 R)"
    by (simp add: eta_def)
  also have "… = α (Λ (Id ; R))"
    by (metis Lambda_pow)
  also have "… = R"
    by simp
  finally show ?thesis.
qed

lemma eta_pow_Lambda [simp]: "η ; 𝒫 R = Λ R"
  by (metis Id_O_R Lambda_pow eta_def)

lemma pow_prop1: "𝒫 R ⊆ S ⟹ R ⊆ α (η ; S)"
  by (metis alpha_eta_pow alpha_ord_pres relcomp_distrib subset_Un_eq)

lemma pow_prop_2: "R ⊆ 𝒫 S ⟹ α (η ; R) ⊆ S"
  by (metis alpha_eta_pow alpha_ord_pres relcomp_distrib subset_Un_eq)

lemma pow_prop: "R = 𝒫 S ⟹ α (η ; R) = S"
  using alpha_eta_pow by blast

lemma alpha_eta_id [simp]: "α (R ; η) = R"
  by simp

lemma eta_alpha_idem [simp]: "α (α R; η) ; η = α R ; η"
  by simp

lemma lambda_eta_alpha [simp]: "Λ (α (α R ; η)) = Λ (α R)"
  by simp

lemma eta_lambda_idem [simp]: "α (Λ (α R)) ; η = α R ; η"
  by simp

lemma Grph_eta [simp]: "Grph (λx. {x}) = η"
  unfolding Grph_def eta_def Lambda_def Id_def by force

lemma Grph_epsiloff [simp]: "Grph (λx. {x}) ; epsiloff = Id"
  by (metis Grph_eta alpha_def alpha_eta)

lemma Image_epsiloff [simp]: "Image epsiloff ∘ (λx. {x}) = id"
  unfolding Image_def epsiloff_def id_def by force


subsection ‹Subset relation›

definition Omega :: "('a set, 'a set) rel" (‹Ω›) where
  "Ω = epsilon ∖ epsilon"

lemma Omega_set: "Ω = {(A,B). A ⊆ B}"
  unfolding Omega_def rres_def epsilon_def by force

lemma conv_Omega: "Omega⇧⌣ = epsiloff ⫽ epsiloff"
  by (simp add: Omega_def epsiloff_epsilon rres_lres_conv)

lemma epsilon_eta_Omega [simp]: "η ; Ω = epsilon"
  unfolding eta_set Omega_set epsilon_def by force

lemma epsiloff_eta_Omega [simp]: "Ω⇧⌣ ; η⇧⌣ = epsiloff"
  by (metis converse_relcomp epsiloff_epsilon epsilon_eta_Omega)

lemma epsilon_Omega [simp]: "epsilon ; Ω = epsilon"
  by (simp add: Omega_def)

lemma conv_Omega_epsiloff [simp]: "Ω⇧⌣ ; epsiloff = epsiloff"
  by (simp add: conv_Omega)

lemma Lambda_conv [simp]: "(Λ R)⇧⌣ = epsilon ÷ R⇧⌣"
  by (simp add: Lambda_syq)

lemma Lambda_Omega: "Λ R ; Ω = R⇧⌣ ∖ epsilon"
proof -
  have "Λ R ; Ω = Λ R ; (epsilon ∖ epsilon)"
    by (simp add: Omega_def)
  also have "… = Λ R ; -(epsiloff ; -epsilon)"
    by (simp add: epsiloff_epsilon rres_compl)
  also have "… = -(Λ R ; epsiloff ; -epsilon)"
    by (metis O_assoc det_lambda deterministic_var2)
  also have "… = - (R ; -epsilon)"
    by (metis alpha_Lambda_canc alpha_def)
  also have "… = R⇧⌣ ∖ epsilon"
    by (simp add: rres_compl)
  finally show ?thesis.
qed

lemma syq_epsiloff_prop [simp]: "Ω⇧⌣ ; (epsilon ÷ R) = epsiloff ⫽ R⇧⌣"
  by (metis Lambda_Omega Lambda_syq converse_converse converse_relcomp converse_syq epsiloff_epsilon rres_lres_conv)

lemma pow_semicomm: "((P,Q) ∈ 𝒫 R ; Ω) = (Δ P ; R ⊆ R ; Δ Q)"
  unfolding pow_set Image_def Omega_def rres_def epsilon_def Delta_def by blast


subsection ‹Complementation relation›

definition Compl :: "('a set,'a set) rel" (‹𝒞›) where
  "𝒞 = epsilon ÷ -epsilon"

lemma Compl_set: "𝒞 = {(A,-A) |A. True}"
  unfolding Compl_def syq_set epsilon_def by force

lemma Compl_Compl [simp]: "𝒞 ; 𝒞 = Id"
  by (metis Compl_def Lambda_syq boolean_algebra_class.boolean_algebra.double_compl converse_converse converse_syq det_lambda deterministic_def set_eq_subset syq_compl2 total_def univalent_def)

lemma Compl_def_var: "𝒞 = Λ (-epsiloff)"
  by (metis Compl_def Lambda_syq boolean_algebra_class.boolean_algebra.double_compl compl_conv converse_converse epsiloff_epsilon syq_compl2)

lemma converse_Compl [simp]: "𝒞⇧⌣ = 𝒞"
  by (metis Compl_def converse_syq double_complement syq_compl2)

lemma det_Compl: "deterministic 𝒞"
  by (simp add: Compl_def_var det_lambda)

lemma bij_Compl: "bijective 𝒞"
  by (simp add: bij_det det_Compl)

lemma Compl_compl_epsiloff [simp]: "𝒞 ; -epsiloff = epsiloff"
  by (metis Compl_Compl Compl_def_var alpha_Lambda_canc alpha_epsiloff alpha_relcomp)

lemma Compl_epsiloff [simp]: "𝒞 ; epsiloff = -epsiloff"
  by (smt (z3) Compl_def_var alpha_Lambda_canc alpha_def)

lemma compl_epsilon_Compl [simp]: "-epsilon ; 𝒞 = epsilon"
  by (metis Compl_compl_epsiloff compl_conv converse_Compl converse_converse converse_relcomp epsiloff_epsilon)

lemma epsilon_Compl [simp]: "epsilon ; 𝒞 = -epsilon"
  by (metis Compl_epsiloff compl_conv converse_Compl converse_converse converse_relcomp epsiloff_epsilon)

lemma Lambda_Compl_var: "Λ R ; 𝒞 = R⇧⌣ ÷ -epsilon"
  by (simp add: Lambda_syq bij_det det_Compl syq_bij)

lemma Lambda_Compl: "Λ R ; 𝒞 = Λ (-R)"
proof -
  have "Λ R ; 𝒞 = Λ R ; Λ (-epsiloff)"
    by (simp add: Compl_def_var)
  also have "… = Λ (Λ R ; -epsiloff)"
    by (simp add: Lambda_fusion_var)
  also have "… = Λ (-(Λ R ; epsiloff))"
    by (metis det_lambda deterministic_var2)
  also have "… = Λ (-R)"
    by (metis alpha_Lambda_canc alpha_def)
  finally show ?thesis.
qed


subsection ‹Kleisli lifting and Kleisli composition›

definition klift :: "('a,'b set) rel ⇒ ('a set,'b set) rel" (‹_⇩𝒫› [1000] 999) where
  "(R)⇩𝒫 = 𝒫 (α R)"

definition kcomp :: "('a,'b set) rel ⇒ ('b,'c set) rel ⇒ ('a,'c set) rel" (infixl ‹⋅⇩𝒫› 70) where
  "R ⋅⇩𝒫 S = R ; (S)⇩𝒫"

lemma klift_var: "(R)⇩𝒫 = Λ (epsiloff ; R ; epsiloff)"
  by (simp add: pow_def O_assoc alpha_def klift_def)

lemma klift_set: "(R)⇩𝒫 = {(A,B). B = ⋃(Image R A)}"
  unfolding klift_def Image_def pow_set alpha_set by force

lemma klift_set_var: "(R)⇩𝒫 = {(A,B). B = ⋃{C. ∃a ∈ A.(a,C) ∈ R}}"
  unfolding klift_set Image_def by auto

lemma klift_mu: "(R)⇩𝒫 = 𝒫 R ; μ"
proof -
  have "(R)⇩𝒫 = 𝒫 (R ; epsiloff)"
    by (simp add: alpha_def klift_def)
  also have "… = 𝒫 R ; 𝒫 epsiloff"
    by (simp add: pow_func2)
  also have "… = 𝒫 R ; μ"
    by (simp add: mu_def)
  finally show ?thesis.
qed

lemma klift_empty: "({},A) ∈ (R)⇩𝒫 ⟷ A = {}"
  using klift_set by auto

lemma klift_ext1: "(R ; (S)⇩𝒫)⇩𝒫 = (R)⇩𝒫 ; (S)⇩𝒫"
  by (metis (no_types, opaque_lifting) Lambda_epsiloff_up1 Lambda_fusion_var O_assoc alpha_def klift_var)

lemma klift_ext2: "deterministic R ⟹ η ; (R)⇩𝒫 = R"
  by (metis Id_O_R Lambda_alpha_canc Lambda_pow eta_def klift_def)

lemma klift_ext3 [simp]: "(η)⇩𝒫 = Id"
  by (simp add: klift_def)

lemma pow_klift [simp]: "(R ; η)⇩𝒫 = 𝒫 R"
  by (simp add: klift_def)

lemma mu_klift [simp]: "(Id)⇩𝒫 = μ"
  by (simp add: klift_def mu_def)

lemma kcomp_var: "R ⋅⇩𝒫 S = R ; 𝒫 S ; μ"
  by (simp add: O_assoc kcomp_def klift_mu)

lemma kcomp_assoc: "R ⋅⇩𝒫 (S ⋅⇩𝒫 T) = (R ⋅⇩𝒫 S) ⋅⇩𝒫T"
proof -
  have "R ⋅⇩𝒫 (S ⋅⇩𝒫 T) = R ; (S ; (T)⇩𝒫)⇩𝒫"
    by (simp add: kcomp_def)
  also have "… = R ; ((S)⇩𝒫 ; (T)⇩𝒫)"
    by (simp add: klift_ext1)
  also have "… = (R ⋅⇩𝒫 S) ⋅⇩𝒫 T"
    by (simp add: O_assoc kcomp_def)
  finally show ?thesis.
qed

lemma kcomp_oner: "R ⋅⇩𝒫 η = R"
  by (simp add: kcomp_def)

lemma kcomp_onel: "deterministic R ⟹ η ⋅⇩𝒫 R = R"
  by (simp add: kcomp_def klift_ext2)


subsection ‹Relational box›

definition rbox :: "('a,'b) rel ⇒ ('b set, 'a set) rel" where
  "rbox R = Λ (epsiloff ⫽ R)"

lemma rbox_set: "rbox R = {(Q,P). P = {a. ∀b. (a,b) ∈ R ⟶ b ∈ Q}}"
  unfolding rbox_def Lambda_def lres_def epsiloff_def
  by force

lemma rbox_exp: "((Q,P) ∈ (rbox (R::('a,'b) rel))) = (P = -{a. ∃b. (a,b) ∈ R ∧ b ∈ -Q})"
  by (smt (z3) Collect_cong Collect_neg_eq ComplD ComplI case_prodD case_prodI mem_Collect_eq rbox_set)

lemma rbox_subset: "rbox R ; Ω⇧⌣ = {(Q,P). P ⊆ {a. ∀b. (a,b) ∈ R ⟶ b ∈ Q}}"
  unfolding rbox_set Omega_set by blast

lemma rbox_semicomm: "(Q,P) ∈ rbox R ; Ω⇧⌣ = (Δ P ; R ⊆ R ; Δ Q)"
  unfolding rbox_subset Delta_def by blast

lemma rbox_semicomm_var: "(Q,P) ∈ rbox R ; Ω⇧⌣ = (Δ P ⊆ (R ; Δ Q) ⫽ R)"
  by (simp add: lres_galois rbox_semicomm)

lemma rbox_omega: "rbox epsiloff = Λ (Ω⇧⌣)"
  by (simp add: conv_Omega rbox_def)

lemma Omega_rbox: "Ω = (α (rbox epsiloff))⇧⌣"
  by (simp add: rbox_omega)

lemma pow_rbox: "((Q,P) ∈ rbox R ; Ω⇧⌣) = ((P,Q) ∈ 𝒫 R ; Ω)"
proof -
  have "(Q,P) ∈ rbox R ; Ω⇧⌣ = (Δ P ; R ⊆ R ; Δ Q)"
    by (simp add: rbox_semicomm)
  also have "… = ((P,Q) ∈ 𝒫 R ; Ω)"
    by (simp add: pow_semicomm)
  finally show ?thesis.
qed

lemma rbox_pow_Compl: "rbox R = 𝒞 ; 𝒫 (R⇧⌣) ; 𝒞"
proof -
  have "𝒞 ; 𝒫 (R⇧⌣) ; 𝒞 = Λ (-epsiloff) ; 𝒫 (R⇧⌣) ; 𝒞"
    by (simp add: Compl_def_var)
  also have "… = Λ (-epsiloff ; R⇧⌣) ; 𝒞"
    by (simp add: Lambda_pow)
  also have "… = Λ (-(-epsiloff ; R⇧⌣))"
    by (simp add: Lambda_Compl)
  also have "… = Λ (epsiloff ⫽ R)"
    by (simp add: lres_compl)
  also have "… = rbox R"
    by (simp add: rbox_def)
  finally show ?thesis..
qed

lemma pow_rbox_Compl: "𝒫 R = 𝒞 ; rbox (R⇧⌣) ; 𝒞"
  by (metis Compl_Compl Id_O_R O_assoc R_O_Id converse_converse rbox_pow_Compl)

lemma pow_conjugation: "𝒞 ; (𝒫 (R⇧⌣) ; Ω)⇧⌣ = 𝒫 R ; 𝒞 ; Ω⇧⌣"
proof -
  have "𝒫 R ; 𝒞 ; Ω⇧⌣ = Λ (-(epsiloff ; R)) ; -(- epsiloff ; epsilon)"
    by (simp add: Lambda_Compl pow_def conv_Omega epsiloff_epsilon lres_compl)
  also have "… = -(Λ (-(epsiloff ; R)) ; - epsiloff ; epsilon)"
    by (metis (no_types, opaque_lifting) alpha_Lambda_canc alpha_def converse_converse det_lambda det_lres deterministic_var2 epsiloff_epsilon lres_compl)
  also have "… = -(Λ (-(epsiloff ; R)) ; 𝒞 ; epsiloff ; epsilon)"
    by (metis Compl_epsiloff alpha_def alpha_relcomp)
  also have "… = -(Λ (epsiloff ; R) ; epsiloff ; epsilon)"
    by (simp add: Lambda_Compl)
  also have "… = -(epsiloff ; R ; epsilon)"
    by (metis Lambda_epsiloff_up1 alpha_def)
  also have "… = -(𝒞 ; -epsiloff ; (epsiloff ; R⇧⌣)⇧⌣)"
    by (metis Compl_compl_epsiloff O_assoc converse_converse converse_relcomp epsiloff_epsilon)
  also have "… = 𝒞 ; (epsiloff ⫽ (epsiloff ; R⇧⌣))"
    by (metis (no_types, opaque_lifting) Compl_def_var Lambda_Compl Lambda_fusion_var pow_def alpha_Lambda_canc boolean_algebra_class.boolean_algebra.double_compl converse_converse pow_rbox_Compl rbox_def)
  also have "… = 𝒞; (𝒫 (R⇧⌣) ; Ω)⇧⌣"
    by (simp add: Lambda_Omega pow_def epsiloff_epsilon rres_lres_conv)
  finally show ?thesis..
qed

lemma pow_rbox_eq: "rbox R ; Ω⇧⌣ = (𝒫 R ; Ω)⇧⌣"
  by (metis (no_types, lifting) Compl_Compl O_assoc R_O_Id converse_converse converse_relcomp pow_conjugation rbox_pow_Compl)

end