Theory conditions_relativized

theory conditions_relativized
  imports conditions_negative
begin

subsection ‹Relativized Conditions›

text‹We continue defining and interrelating axiomatic conditions on unary operations (operators). 
 This time we consider their 'relativized' variants.›

text‹Relativized order and equality relations.›
definition subset_in::‹'p σ ⇒ 'p σ ⇒ 'p σ ⇒ bool› (‹_❙≤⇩__›) 
  where ‹A ❙≤⇩U B ≡ ∀x. U x ⟶ (A x ⟶ B x)›
definition subset_out::‹'p σ ⇒ 'p σ ⇒ 'p σ ⇒ bool› (‹_❙≤⇧__›) 
  where ‹A ❙≤⇧U B ≡ ∀x. ¬U x ⟶ (A x ⟶ B x)›
definition setequ_in::‹'p σ ⇒ 'p σ ⇒ 'p σ ⇒ bool› (‹_❙=⇩__›) 
  where ‹A ❙=⇩U B ≡ ∀x. U x ⟶ (A x ⟷ B x)›
definition setequ_out::‹'p σ ⇒ 'p σ ⇒ 'p σ ⇒ bool› (‹_❙=⇧__›) 
  where ‹A ❙=⇧U B ≡ ∀x. ¬U x ⟶ (A x ⟷ B x)›

declare subset_in_def[order] subset_out_def[order] setequ_in_def[order] setequ_out_def[order]

lemma subset_in_out: "(let U=C in (A ❙≤⇩U B)) = (let U=❙─C in (A ❙≤⇧U B))" by (simp add: compl_def subset_in_def subset_out_def)
lemma setequ_in_out: "(let U=C in (A ❙=⇩U B)) = (let U=❙─C in (A ❙=⇧U B))" by (simp add: compl_def setequ_in_def setequ_out_def)

lemma subset_in_char: "(A ❙≤⇩U B) = (U ❙∧ A ❙≤ U ❙∧ B)" unfolding order conn by blast
lemma subset_out_char: "(A ❙≤⇧U B) = (U ❙∨ A ❙≤ U ❙∨ B)" unfolding order conn by blast
lemma setequ_in_char: "(A ❙=⇩U B) = (U ❙∧ A ❙= U ❙∧ B)" unfolding order conn by blast
lemma setequ_out_char: "(A ❙=⇧U B) = (U ❙∨ A ❙= U ❙∨ B)" unfolding order conn by blast

text‹Relativization cannot be meaningfully applied to conditions (n)NORM or (n)DNRM.›
lemma "NORM φ  = (let U = ❙⊤ in ((φ ❙⊥) ❙=⇩U ❙⊥))" by (simp add: NORM_def setequ_def setequ_in_def top_def)
lemma "(let U = ❙⊥ in ((φ ❙⊥) ❙=⇩U ❙⊥))" by (simp add: bottom_def setequ_in_def)

text‹Relativization ('in' resp. 'out') leaves (n)EXPN/(n)CNTR unchanged or trivializes them.›
lemma "EXPN φ  = (∀A. A ❙≤⇩A φ A)" by (simp add: EXPN_def subset_def subset_in_def)
lemma "CNTR φ  = (∀A. (φ A) ❙≤⇧A A)" by (metis (mono_tags, lifting) CNTR_def subset_def subset_out_def)
lemma "∀A. A ❙≤⇧A φ A" by (simp add: subset_out_def)
lemma "∀A. (φ A) ❙≤⇩A A" by (simp add: subset_in_def)


text‹Relativized ADDI variants.›
definition ADDIr::"('w σ ⇒ 'w σ) ⇒ bool" (‹ADDIr›)
  where "ADDIr φ  ≡ ∀A B. let U = (A ❙∨ B) in      (φ(A ❙∨ B) ❙=⇧U (φ A) ❙∨ (φ B))"
definition ADDIr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹ADDIr⇧^a›)
  where "ADDIr⇧^a φ ≡ ∀A B. let U = (A ❙∨ B) in      (φ(A ❙∨ B) ❙≤⇧U (φ A) ❙∨ (φ B))" 
definition ADDIr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹ADDIr⇧^b›)
  where "ADDIr⇧^b φ ≡ ∀A B. let U = (A ❙∨ B) in ((φ A) ❙∨ (φ B) ❙≤⇧U φ(A ❙∨ B))"
 
declare ADDIr_def[cond] ADDIr_a_def[cond] ADDIr_b_def[cond]

lemma ADDIr_char: "ADDIr φ = (ADDIr⇧^a φ ∧ ADDIr⇧^b φ)" unfolding cond by (meson setequ_char setequ_out_char subset_out_char)

lemma ADDIr_a_impl: "ADDI⇧^a φ ⟶ ADDIr⇧^a φ" by (simp add: ADDI_a_def ADDIr_a_def subset_def subset_out_def)
lemma ADDIr_a_equ:  "EXPN φ ⟹ ADDIr⇧^a φ = ADDI⇧^a φ" unfolding cond by (smt (verit, del_insts) join_def subset_def subset_out_def)
lemma ADDIr_a_equ':"nEXPN φ ⟹ ADDIr⇧^a φ = ADDI⇧^a φ" unfolding cond by (smt (verit, ccfv_threshold) compl_def subset_def subset_out_def)

lemma ADDIr_b_impl: "ADDI⇧^b φ ⟶ ADDIr⇧^b φ" by (simp add: ADDI_b_def ADDIr_b_def subset_def subset_out_def)
lemma "nEXPN φ ⟹ ADDIr⇧^b φ ⟶ ADDI⇧^b φ" nitpick oops ―‹ countermodel ›
lemma ADDIr_b_equ: "EXPN φ ⟹ ADDIr⇧^b φ = ADDI⇧^b φ" unfolding cond by (smt (z3) subset_def subset_out_def)


text‹Relativized MULT variants.›
definition MULTr::"('w σ ⇒ 'w σ) ⇒ bool" (‹MULTr›)
  where "MULTr φ  ≡ ∀A B. let U = (A ❙∧ B) in      (φ(A ❙∧ B) ❙=⇩U (φ A) ❙∧ (φ B))"
definition MULTr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹MULTr⇧^a›)
  where "MULTr⇧^a φ ≡ ∀A B. let U = (A ❙∧ B) in      (φ(A ❙∧ B) ❙≤⇩U (φ A) ❙∧ (φ B))"
definition MULTr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹MULTr⇧^b›)
  where "MULTr⇧^b φ ≡ ∀A B. let U = (A ❙∧ B) in ((φ A) ❙∧ (φ B) ❙≤⇩U φ(A ❙∧ B))"

declare MULTr_def[cond] MULTr_a_def[cond] MULTr_b_def[cond]

lemma MULTr_char: "MULTr φ = (MULTr⇧^a φ ∧ MULTr⇧^b φ)" unfolding cond by (meson setequ_char setequ_in_char subset_in_char)

lemma MULTr_a_impl: "MULT⇧^a φ ⟶ MULTr⇧^a φ" by (simp add: MULT_a_def MULTr_a_def subset_def subset_in_def)
lemma "nCNTR φ ⟹ MULTr⇧^a φ ⟶ MULT⇧^a φ" nitpick oops ―‹ countermodel ›
lemma MULTr_a_equ: "CNTR φ ⟹ MULTr⇧^a φ = MULT⇧^a φ" unfolding cond by (smt (verit, del_insts) subset_def subset_in_def)

lemma MULTr_b_impl: "MULT⇧^b φ ⟶ MULTr⇧^b φ" by (simp add: MULT_b_def MULTr_b_def subset_def subset_in_def)
lemma "MULTr⇧^b φ ⟶ MULT⇧^b φ" nitpick oops ―‹ countermodel ›
lemma MULTr_b_equ:  "CNTR φ ⟹ MULTr⇧^b φ = MULT⇧^b φ" unfolding cond by (smt (verit, del_insts) meet_def subset_def subset_in_def)
lemma MULTr_b_equ':"nCNTR φ ⟹ MULTr⇧^b φ = MULT⇧^b φ" unfolding cond by (smt (z3) compl_def subset_def subset_in_def)

text‹Weak variants of monotonicity.›
definition MONOw1::"('w σ ⇒ 'w σ) ⇒ bool" (‹MONOw⇧¹›) 
  where "MONOw⇧¹ φ ≡ ∀A B. A ❙≤ B ⟶ (φ A) ❙≤ B ❙∨ (φ B)"
definition MONOw2::"('w σ ⇒ 'w σ) ⇒ bool" (‹MONOw⇧²›)
  where "MONOw⇧² φ ≡ ∀A B. A ❙≤ B ⟶ A ❙∧ (φ A) ❙≤ (φ B)"

declare MONOw1_def[cond] MONOw2_def[cond]

lemma MONOw1_ADDIr_b: "MONOw⇧¹ φ = ADDIr⇧^b φ" proof -
  have l2r: "MONOw⇧¹ φ ⟶ ADDIr⇧^b φ"  unfolding cond subset_out_char by (metis (mono_tags, opaque_lifting) L7 join_def subset_def) 
  have r2l: "ADDIr⇧^b φ ⟶ MONOw⇧¹ φ" unfolding cond subset_out_char by (metis (full_types) L9 join_def setequ_ext subset_def)
  show ?thesis using l2r r2l by blast
qed
lemma MONOw2_MULTr_a: "MONOw⇧² φ = MULTr⇧^a φ" proof -
  have l2r: "MONOw⇧² φ ⟶ MULTr⇧^a φ" unfolding cond subset_in_char by (meson L4 L5 L8 L9)
  have r2l:"MULTr⇧^a φ ⟶ MONOw⇧² φ" unfolding cond subset_in_char by (metis BA_distr1 L2 L5 L6 L9 setequ_ext)
  show ?thesis using l2r r2l by blast
qed

lemma MONOw1_impl: "MONO φ ⟶ MONOw⇧¹ φ" by (simp add: ADDIr_b_impl MONO_ADDIb MONOw1_ADDIr_b)
lemma "MONOw⇧¹ φ ⟶ MONO φ" nitpick oops ―‹ countermodel ›
lemma MONOw2_impl: "MONO φ ⟶ MONOw⇧² φ" by (simp add: MONO_MULTa MONOw2_MULTr_a MULTr_a_impl)
lemma "MONOw⇧² φ ⟶ MONO φ" nitpick oops ―‹ countermodel ›


text‹We have in fact that (n)CNTR (resp. (n)EXPN) implies MONOw-1/ADDIr-b (resp. MONOw-2/MULTr-a).›
lemma CNTR_MONOw1_impl: "CNTR φ ⟶ MONOw⇧¹ φ" by (metis CNTR_def L3 MONOw1_def subset_char1)
lemma nCNTR_MONOw1_impl: "nCNTR φ ⟶ MONOw⇧¹ φ" by (smt (verit, ccfv_threshold) MONOw1_def compl_def join_def nCNTR_def subset_def)
lemma EXPN_MONOw2_impl: "EXPN φ ⟶ MONOw⇧² φ" by (metis EXPN_def L4 MONOw2_def subset_char1)
lemma nEXPN_MONOw2_impl: "nEXPN φ ⟶ MONOw⇧² φ" by (smt (verit) MONOw2_def compl_def meet_def nEXPN_def subset_def)

text‹Relativized nADDI variants.›
definition nADDIr::"('w σ ⇒ 'w σ) ⇒ bool" (‹nADDIr›)
  where "nADDIr φ  ≡ ∀A B. let U = (A ❙∨ B) in      (φ(A ❙∨ B) ❙=⇧U (φ A) ❙∧ (φ B))"
definition nADDIr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹nADDIr⇧^a›)
  where "nADDIr⇧^a φ ≡ ∀A B. let U = (A ❙∨ B) in ((φ A) ❙∧ (φ B) ❙≤⇧U φ(A ❙∨ B))" 
definition nADDIr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹nADDIr⇧^b›)
  where "nADDIr⇧^b φ ≡ ∀A B. let U = (A ❙∨ B) in      (φ(A ❙∨ B) ❙≤⇧U (φ A) ❙∧ (φ B))"
 
declare nADDIr_def[cond] nADDIr_a_def[cond] nADDIr_b_def[cond]

lemma nADDIr_char: "nADDIr φ = (nADDIr⇧^a φ ∧ nADDIr⇧^b φ)" unfolding cond by (meson setequ_char setequ_out_char subset_out_char)

lemma nADDIr_a_impl: "nADDI⇧^a φ ⟶ nADDIr⇧^a φ" unfolding cond by (simp add: subset_def subset_out_def)
lemma "nADDIr⇧^a φ ⟶ nADDI⇧^a φ" nitpick oops ―‹ countermodel ›
lemma nADDIr_a_equ:  "EXPN φ ⟹ nADDIr⇧^a φ = nADDI⇧^a φ" unfolding cond by (smt (z3) subset_def subset_out_def)
lemma nADDIr_a_equ':"nEXPN φ ⟹ nADDIr⇧^a φ = nADDI⇧^a φ" unfolding cond by (smt (z3) compl_def join_def meet_def subset_def subset_out_def)

lemma nADDIr_b_impl: "nADDI⇧^b φ ⟶ nADDIr⇧^b φ" by (simp add: nADDI_b_def nADDIr_b_def subset_def subset_out_def)
lemma "EXPN φ ⟹ nADDIr⇧^b φ ⟶ nADDI⇧^b φ" nitpick oops ―‹ countermodel ›
lemma nADDIr_b_equ: "nEXPN φ ⟹ nADDIr⇧^b φ = nADDI⇧^b φ" unfolding cond by (smt (z3) compl_def subset_def subset_out_def)


text‹Relativized nMULT variants.›
definition nMULTr::"('w σ ⇒ 'w σ) ⇒ bool" (‹nMULTr›)
  where "nMULTr φ  ≡ ∀A B. let U = (A ❙∧ B) in      (φ(A ❙∧ B) ❙=⇩U (φ A) ❙∨ (φ B))"
definition nMULTr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹nMULTr⇧^a›)
  where "nMULTr⇧^a φ ≡ ∀A B. let U = (A ❙∧ B) in ((φ A) ❙∨ (φ B) ❙≤⇩U φ(A ❙∧ B))"
definition nMULTr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹nMULTr⇧^b›)
  where "nMULTr⇧^b φ ≡ ∀A B. let U = (A ❙∧ B) in      (φ(A ❙∧ B) ❙≤⇩U (φ A) ❙∨ (φ B))"

declare nMULTr_def[cond] nMULTr_a_def[cond] nMULTr_b_def[cond]

lemma nMULTr_char: "nMULTr φ = (nMULTr⇧^a φ ∧ nMULTr⇧^b φ)" unfolding cond by (meson setequ_char setequ_in_char subset_in_char)

lemma nMULTr_a_impl: "nMULT⇧^a φ ⟶ nMULTr⇧^a φ" by (simp add: nMULT_a_def nMULTr_a_def subset_def subset_in_def)
lemma "CNTR φ ⟹ nMULTr⇧^a φ ⟶ nMULT⇧^a φ" nitpick oops ―‹ countermodel ›
lemma nMULTr_a_equ: "nCNTR φ ⟹ nMULTr⇧^a φ = nMULT⇧^a φ" unfolding cond by (smt (z3) compl_def subset_def subset_in_def)

lemma nMULTr_b_impl: "nMULT⇧^b φ ⟶ nMULTr⇧^b φ" by (simp add: nMULT_b_def nMULTr_b_def subset_def subset_in_def)
lemma "nMULTr⇧^b φ ⟶ nMULT⇧^b φ" nitpick oops ―‹ countermodel ›
lemma nMULTr_b_equ:  "CNTR φ ⟹ nMULTr⇧^b φ = nMULT⇧^b φ" unfolding cond by (smt (z3) compl_def join_def meet_def subset_def subset_in_def)
lemma nMULTr_b_equ':"nCNTR φ ⟹ nMULTr⇧^b φ = nMULT⇧^b φ" unfolding cond by (smt (z3) compl_def join_def meet_def subset_def subset_in_def)


text‹Weak variants of antitonicity.›
definition ANTIw1::"('w σ ⇒ 'w σ) ⇒ bool" (‹ANTIw⇧¹›) 
  where "ANTIw⇧¹ φ ≡ ∀A B. A ❙≤ B ⟶ (φ B) ❙≤ B ❙∨ (φ A)"
definition ANTIw2::"('w σ ⇒ 'w σ) ⇒ bool" (‹ANTIw⇧²›)
  where "ANTIw⇧² φ ≡ ∀A B. A ❙≤ B ⟶ A ❙∧ (φ B) ❙≤ (φ A)"

declare ANTIw1_def[cond] ANTIw2_def[cond]

lemma ANTIw1_nADDIr_b: "ANTIw⇧¹ φ = nADDIr⇧^b φ" proof -
  have l2r: "ANTIw⇧¹ φ ⟶ nADDIr⇧^b φ" unfolding cond subset_out_char by (smt (verit, ccfv_SIG) BA_distr2 L8 join_def setequ_ext subset_def)
  have r2l: "nADDIr⇧^b φ ⟶ ANTIw⇧¹ φ" unfolding cond subset_out_def by (metis (full_types) L9 join_def meet_def setequ_ext subset_def)
  show ?thesis using l2r r2l by blast
qed
lemma ANTIw2_nMULTr_a: "ANTIw⇧² φ = nMULTr⇧^a φ" proof -
  have l2r: "ANTIw⇧² φ ⟶ nMULTr⇧^a φ" unfolding cond subset_in_char by (metis BA_distr1 L3 L4 L5 L7 L8 setequ_ext)
  have r2l: "nMULTr⇧^a φ ⟶ ANTIw⇧² φ" unfolding cond subset_in_def by (metis (full_types) L10 join_def meet_def setequ_ext subset_def)
  show ?thesis using l2r r2l by blast
qed

lemma "ANTI φ ⟶ ANTIw⇧¹ φ" by (simp add: ANTI_nADDIb ANTIw1_nADDIr_b nADDIr_b_impl)
lemma "ANTIw⇧¹ φ ⟶ ANTI φ" nitpick oops ―‹ countermodel ›
lemma "ANTI φ ⟶ ANTIw⇧² φ" by (simp add: ANTI_nMULTa ANTIw2_nMULTr_a nMULTr_a_impl)
lemma "ANTIw⇧² φ ⟶ ANTI φ" nitpick oops ―‹ countermodel ›

text‹We have in fact that (n)CNTR (resp. (n)EXPN) implies ANTIw-1/nADDIr-b (resp. ANTIw-2/nMULTr-a).›
lemma CNTR_ANTIw1_impl: "CNTR φ ⟶ ANTIw⇧¹ φ" unfolding cond using L3 subset_char1 by blast
lemma nCNTR_ANTIw1_impl: "nCNTR φ ⟶ ANTIw⇧¹ φ" unfolding cond by (metis (full_types) compl_def join_def subset_def)
lemma EXPN_ANTIw2_impl: "EXPN φ ⟶ ANTIw⇧² φ" unfolding cond using L4 subset_char1 by blast
lemma nEXPN_ANTIw2_impl: "nEXPN φ ⟶ ANTIw⇧² φ" unfolding cond by (metis (full_types) compl_def meet_def subset_def)

text‹Dual interrelations.›
lemma ADDIr_dual1: "ADDIr⇧^a φ = MULTr⇧^b φ⇧^d" unfolding cond subset_in_char subset_out_char by (smt (z3) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext)
lemma ADDIr_dual2: "ADDIr⇧^b φ = MULTr⇧^a φ⇧^d" unfolding cond subset_in_char subset_out_char by (smt (verit, ccfv_threshold) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext)
lemma ADDIr_dual:  "ADDIr φ = MULTr φ⇧^d" using ADDIr_char ADDIr_dual1 ADDIr_dual2 MULTr_char by blast

lemma nADDIr_dual1: "nADDIr⇧^a φ = nMULTr⇧^b φ⇧^d" unfolding cond subset_in_char subset_out_char by (smt (verit, del_insts) BA_cp BA_deMorgan1 BA_dn op_dual_def setequ_ext)
lemma nADDIr_dual2: "nADDIr⇧^b φ = nMULTr⇧^a φ⇧^d" by (smt (z3) BA_deMorgan1 BA_dn compl_def nADDIr_b_def nMULTr_a_def op_dual_def setequ_ext subset_in_def subset_out_def)
lemma nADDIr_dual: "nADDIr φ = nMULTr φ⇧^d" using nADDIr_char nADDIr_dual1 nADDIr_dual2 nMULTr_char by blast


text‹Complement interrelations.›
lemma ADDIr_a_cmpl: "ADDIr⇧^a φ = nADDIr⇧^a φ⇧^-" unfolding cond by (smt (verit, del_insts) BA_deMorgan1 compl_def setequ_ext subset_out_def svfun_compl_def)
lemma ADDIr_b_cmpl: "ADDIr⇧^b φ = nADDIr⇧^b φ⇧^-" unfolding cond by (smt (verit, del_insts) BA_deMorgan1 compl_def setequ_ext subset_out_def svfun_compl_def)
lemma ADDIr_cmpl: "ADDIr φ = nADDIr φ⇧^-" by (simp add: ADDIr_a_cmpl ADDIr_b_cmpl ADDIr_char nADDIr_char)
lemma MULTr_a_cmpl: "MULTr⇧^a φ = nMULTr⇧^a φ⇧^-" unfolding cond by (smt (verit, del_insts) BA_deMorgan2 compl_def setequ_ext subset_in_def svfun_compl_def)
lemma MULTr_b_cmpl: "MULTr⇧^b φ = nMULTr⇧^b φ⇧^-" unfolding cond by (smt (verit, ccfv_threshold) BA_deMorgan2 compl_def setequ_ext subset_in_def svfun_compl_def)
lemma MULTr_cmpl: "MULTr φ = nMULTr φ⇧^-" by (simp add: MULTr_a_cmpl MULTr_b_cmpl MULTr_char nMULTr_char)


text‹Fixed-point interrelations.›
lemma EXPN_fp:  "EXPN φ = EXPN φ⇧^f⇧^p" by (simp add: EXPN_def dimpl_def op_fixpoint_def subset_def)
lemma EXPN_fpc: "EXPN φ = nEXPN φ⇧^f⇧^p⇧^-" using EXPN_fp nEXPN_CNTR_compl by blast
lemma CNTR_fp:  "CNTR φ = nCNTR φ⇧^f⇧^p" by (metis EXPN_CNTR_dual1 EXPN_fp dual_compl_char2 dual_invol nCNTR_EXPN_compl ofp_comm_dc1 sfun_compl_invol)
lemma CNTR_fpc: "CNTR φ = CNTR φ⇧^f⇧^p⇧^-" by (metis CNTR_fp nCNTR_EXPN_compl ofp_comm_compl ofp_invol)

lemma nNORM_fp: "NORM φ = nNORM φ⇧^f⇧^p" by (metis NORM_def fixpoints_def fp_rel nNORM_def)
lemma NORM_fpc: "NORM φ = NORM φ⇧^f⇧^p⇧^-" by (simp add: NORM_def bottom_def ofp_fixpoint_compl_def sdiff_def)
lemma DNRM_fp:  "DNRM φ = DNRM φ⇧^f⇧^p" by (simp add: DNRM_def dimpl_def op_fixpoint_def top_def)
lemma DNRM_fpc: "DNRM φ = nDNRM φ⇧^f⇧^p⇧^-" using DNRM_fp nDNRM_DNRM_compl by blast

lemma ADDIr_a_fpc: "ADDIr⇧^a φ = ADDIr⇧^a φ⇧^f⇧^p⇧^-" unfolding cond subset_out_def by (simp add: join_def ofp_fixpoint_compl_def sdiff_def)
lemma ADDIr_a_fp: "ADDIr⇧^a φ = nADDIr⇧^a φ⇧^f⇧^p" by (metis ADDIr_a_cmpl ADDIr_a_fpc sfun_compl_invol)
lemma ADDIr_b_fpc: "ADDIr⇧^b φ = ADDIr⇧^b φ⇧^f⇧^p⇧^-" unfolding cond subset_out_def by (simp add: join_def ofp_fixpoint_compl_def sdiff_def)
lemma ADDIr_b_fp: "ADDIr⇧^b φ = nADDIr⇧^b φ⇧^f⇧^p" by (metis ADDIr_b_cmpl ADDIr_b_fpc sfun_compl_invol)

lemma MULTr_a_fp: "MULTr⇧^a φ = MULTr⇧^a φ⇧^f⇧^p" unfolding cond subset_in_def by (simp add: dimpl_def meet_def op_fixpoint_def)
lemma MULTr_a_fpc: "MULTr⇧^a φ = nMULTr⇧^a φ⇧^f⇧^p⇧^-" using MULTr_a_cmpl MULTr_a_fp by blast
lemma MULTr_b_fp: "MULTr⇧^b φ = MULTr⇧^b φ⇧^f⇧^p" unfolding cond subset_in_def by (simp add: dimpl_def meet_def op_fixpoint_def)
lemma MULTr_b_fpc: "MULTr⇧^b φ = nMULTr⇧^b φ⇧^f⇧^p⇧^-" using MULTr_b_cmpl MULTr_b_fp by blast


text‹Relativized IDEM variants.›
definition IDEMr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹IDEMr⇧^a›)
  where "IDEMr⇧^a φ ≡ ∀A. φ(A ❙∨ φ A) ❙≤⇧A (φ A)"
definition IDEMr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹IDEMr⇧^b›) 
  where "IDEMr⇧^b φ ≡ ∀A. (φ A) ❙≤⇩A φ(A ❙∧ φ A)"
declare IDEMr_a_def[cond] IDEMr_b_def[cond]

text‹Relativized nIDEM variants.›
definition nIDEMr_a::"('w σ ⇒ 'w σ) ⇒ bool" (‹nIDEMr⇧^a›) 
  where "nIDEMr⇧^a φ ≡ ∀A. (φ A) ❙≤⇧A φ(A ❙∨ ❙─(φ A))"
definition nIDEMr_b::"('w σ ⇒ 'w σ) ⇒ bool" (‹nIDEMr⇧^b›) 
  where "nIDEMr⇧^b φ ≡ ∀A. φ(A ❙∧ ❙─(φ A)) ❙≤⇩A (φ A)"

declare nIDEMr_a_def[cond] nIDEMr_b_def[cond]


text‹Complement interrelations.›
lemma IDEMr_a_cmpl: "IDEMr⇧^a φ = nIDEMr⇧^a φ⇧^-" unfolding cond subset_in_def subset_out_def by (metis compl_def sfun_compl_invol svfun_compl_def)
lemma IDEMr_b_cmpl: "IDEMr⇧^b φ = nIDEMr⇧^b φ⇧^-" unfolding cond subset_in_def subset_out_def by (metis compl_def sfun_compl_invol svfun_compl_def)

text‹Dual interrelation.›
lemma IDEMr_dual: "IDEMr⇧^a φ = IDEMr⇧^b φ⇧^d" unfolding cond subset_in_def subset_out_def op_dual_def by (metis (mono_tags, opaque_lifting) BA_dn compl_def diff_char1 diff_char2 impl_char setequ_ext)
lemma nIDEMr_dual: "nIDEMr⇧^a φ = nIDEMr⇧^b φ⇧^d" by (metis IDEMr_dual IDEMr_a_cmpl IDEMr_b_cmpl dual_compl_char1 dual_compl_char2 sfun_compl_invol)

text‹Fixed-point interrelations.›
lemma nIDEMr_a_fpc: "nIDEMr⇧^a φ = nIDEMr⇧^a φ⇧^f⇧^p⇧^-" proof -
  have "∀A. (λp. A p ∨ ¬φ A p) = (λp. A p ∨ φ A p = A p)" by blast
  thus ?thesis unfolding cond subset_out_def ofp_fixpoint_compl_def conn order by simp
qed
lemma IDEMr_a_fp: "IDEMr⇧^a φ = nIDEMr⇧^a φ⇧^f⇧^p" by (metis IDEMr_a_cmpl nIDEMr_a_fpc ofp_invol)
lemma IDEMr_a_fpc: "IDEMr⇧^a φ = IDEMr⇧^a φ⇧^f⇧^p⇧^-" by (metis IDEMr_a_cmpl nIDEMr_a_fpc ofp_comm_compl)
lemma IDEMr_b_fp: "IDEMr⇧^b φ = IDEMr⇧^b φ⇧^f⇧^p" by (metis IDEMr_a_fpc IDEMr_dual dual_compl_char1 dual_invol ofp_comm_compl ofp_comm_dc2)
lemma IDEMr_b_fpc: "IDEMr⇧^b φ = nIDEMr⇧^b φ⇧^f⇧^p⇧^-" using IDEMr_b_fp IDEMr_b_cmpl by blast


text‹The original border condition B1' (by Zarycki) is equivalent to the conjuntion of nMULTr and CNTR.›
abbreviation "B1' φ ≡ ∀A B. φ(A ❙∧ B) ❙= (A ❙∧ φ B) ❙∨ (φ A ❙∧ B)" 

lemma "B1' φ = (nMULTr φ ∧ CNTR φ)" proof -
  have l2ra: "B1' φ ⟶ nMULTr φ" unfolding cond by (smt (z3) join_def meet_def setequ_ext setequ_in_def)
  have l2rb: "B1' φ ⟶ CNTR φ" unfolding cond by (metis L2 L4 L5 L7 L9 setequ_ext)
  have r2l: "(nMULTr φ ∧ CNTR φ) ⟶ B1' φ" unfolding cond by (smt (z3) L10 join_def meet_def setequ_def setequ_in_char)
  from l2ra l2rb r2l show ?thesis by blast
qed

text‹Modulo conditions nMULTr and CNTR the border condition B4 is equivalent to nIDEMr-b.›
abbreviation "B4 φ ≡ ∀A. φ(❙─φ(❙─A)) ❙≤ A"

lemma "nMULTr φ ⟹ CNTR φ ⟹ B4 φ = nIDEMr⇧^b φ" proof -
  assume a1: "nMULTr φ" and a2: "CNTR φ"
  have l2r: "nMULTr⇧^b φ ⟹ B4 φ ⟶ nIDEMr⇧^b φ" unfolding cond subset_in_char subset_def by (metis BA_deMorgan1 BA_dn compl_def meet_def setequ_ext)
  have r2l: "nMULTr⇧^a φ ⟹ CNTR φ ⟹ nIDEMr⇧^b φ ⟶ B4 φ" unfolding cond by (smt (verit) compl_def join_def meet_def subset_def subset_in_def)
  from l2r r2l show ?thesis using a1 a2 nMULTr_char by blast
qed

end