# Theory Domain_Recursion

(* Title:      Domain Recursion
Author:     Walter Guttmann
Maintainer: Walter Guttmann <walter.guttmann at canterbury.ac.nz>
*)

section Domain Recursion

theory Domain_Recursion

imports Domain_Iterings Approximation

begin

class domain_semiring_lattice_apx = domain_semiring_lattice_L + apx +
assumes apx_def: "x  y  x  y  L  d(L) * y  x  d(x * bot) * top"
begin

lemma apx_transitive:
assumes "x  y"
and "y  z"
shows "x  z"
proof -
have 1: "x  z  L"
by (smt assms sup_assoc sup_commute apx_def le_iff_sup)
have "d(d(L) * y * bot) * top  d((x  d(x * bot) * top) * bot) * top"
by (metis assms(1) apx_def d_isotone mult_left_isotone)
also have "...  d(x * bot) * top"
by (metis le_sup_iff d_galois mult_left_isotone mult_right_dist_sup order_refl zero_right_mult_decreasing)
finally have 2: "d(d(L) * y * bot) * top  d(x * bot) * top"
.
have "d(L) * z = d(L) * (d(L) * z)"
also have "...  d(L) * y  d(d(L) * y * bot) * top"
by (metis assms(2) apx_def d_export mult_assoc mult_left_dist_sup mult_right_isotone)
also have "...  x  d(x * bot) * top"
using 2 by (meson assms(1) apx_def le_supI2 sup_least)
finally show ?thesis
using 1 by (simp add: apx_def)
qed

lemma apx_meet_L:
assumes "y  x"
shows "x  L  y  L"
proof -
have "x  L = d(L) * x  L"
using meet_intro_domain by auto
also have "...  (y  d(y * bot) * top)  L"
using assms apx_def inf.sup_left_isotone by blast
also have "...  y"
finally show ?thesis
by simp
qed

lemma sup_apx_left_isotone:
assumes "x  y"
shows "x  z  y  z"
proof -
have 1: "x  z  y  z  L"
by (smt assms sup_assoc sup_commute sup_left_isotone apx_def)
have "d(L) * (y  z) = d(L) * y  d(L) * z"
also have "...  d(L) * y  z"
by (simp add: d_mult_below le_supI1 sup_commute)
also have "...  x  d(x * bot) * top  z"
using assms apx_def sup_left_isotone by blast
also have "...  x  z  d((x  z) * bot) * top"
finally show ?thesis
using 1 by (simp add: apx_def)
qed

subclass apx_biorder
apply unfold_locales
apply (metis le_sup_iff sup_ge1 apx_def d_plus_one mult_left_one mult_right_dist_sup)
apply (meson apx_meet_L order.antisym apx_def relative_equality sup_same_context)
using apx_transitive by blast

lemma mult_apx_left_isotone:
assumes "x  y"
shows "x * z  y * z"
proof -
have "x * z  y * z  L * z"
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
hence 1: "x * z  y * z  L"
using l40 order_lesseq_imp semiring.add_left_mono by blast
have "d(L) * y * z  x * z  d(x * bot) * top * z"
by (metis assms apx_def mult_left_isotone mult_right_dist_sup)
also have "...  x * z  d(x * z * bot) * top"
by (metis sup_right_isotone d_isotone mult_assoc mult_isotone mult_right_isotone top_greatest bot_least)
finally show ?thesis
using 1 by (simp add: apx_def mult_assoc)
qed

lemma mult_apx_right_isotone:
assumes "x  y"
shows "z * x  z * y"
proof -
have "z * x  z * y  z * L"
by (metis assms apx_def mult_left_dist_sup mult_right_isotone)
also have "...  z * y  z * bot  L"
finally have 1: "z * x  z * y  L"
using mult_right_isotone sup.order_iff by auto
have "d(L) * z * y  z * d(L) * y"
also have "...  z * (x  d(x * bot) * top)"
by (metis assms apx_def mult_assoc mult_right_isotone)
also have "... = z * x  z * d(x * bot) * top"
also have "...  z * x  d(z * x * bot) * top"
by (metis sup_right_isotone mult_assoc mult_domain_top)
finally show ?thesis
using 1 by (simp add: apx_def mult_assoc)
qed

subclass apx_semiring
apply unfold_locales
apply (metis sup_ge2 apx_def l3 mult_right_isotone order_trans top_greatest)

lemma meet_L_apx_isotone:
"x  y  x  L  y  L"
by (smt (z3) inf.cobounded2 sup.coboundedI1 sup_absorb sup_commute apx_def apx_meet_L d_restrict_equals l20 inf_commute meet_domain)

definition kappa_apx_meet :: "('a  'a)  bool"
where "kappa_apx_meet f  apx.has_least_fixpoint f  has_apx_meet (μ f) (ν f)  κ f = μ f  ν f"

definition kappa_mu_nu :: "('a  'a)  bool"
where "kappa_mu_nu f  apx.has_least_fixpoint f  κ f = μ f  (ν f  L)"

definition nu_below_mu_nu :: "('a  'a)  bool"
where "nu_below_mu_nu f  d(L) * ν f  μ f  (ν f  L)  d(ν f * bot) * top"

definition nu_below_mu_nu_2 :: "('a  'a)  bool"
where "nu_below_mu_nu_2 f  d(L) * ν f  μ f  (ν f  L)  d((μ f  (ν f  L)) * bot) * top"

definition mu_nu_apx_nu :: "('a  'a)  bool"
where "mu_nu_apx_nu f  μ f  (ν f  L)  ν f"

definition mu_nu_apx_meet :: "('a  'a)  bool"
where "mu_nu_apx_meet f  has_apx_meet (μ f) (ν f)  μ f  ν f = μ f  (ν f  L)"

definition apx_meet_below_nu :: "('a  'a)  bool"
where "apx_meet_below_nu f  has_apx_meet (μ f) (ν f)  μ f  ν f  ν f"

lemma mu_below_l:
"μ f  μ f  (ν f  L)"
by simp

lemma l_below_nu:

lemma n_l_nu:
"has_least_fixpoint f  has_greatest_fixpoint f  (μ f  (ν f  L))  L = ν f  L"
by (meson l_below_nu inf.sup_same_context inf_le1 order_trans sup.cobounded2)

lemma l_apx_mu:
"μ f  (ν f  L)  μ f"
by (simp add: apx_def d_mult_below le_supI1 sup_inf_distrib1)

lemma nu_below_mu_nu_nu_below_mu_nu_2:
assumes
shows
proof -
have "d(L) * ν f = d(L) * (d(L) * ν f)"
also have "...  d(L) * (μ f  (ν f  L)  d(ν f * bot) * top)"
using assms mult_isotone nu_below_mu_nu_def by blast
also have "... = d(L) * (μ f  (ν f  L))  d(L) * d(ν f * bot) * top"
also have "...  μ f  (ν f  L)  d(L) * d(ν f * bot) * top"
using d_mult_below sup_left_isotone by auto
also have "... = μ f  (ν f  L)  d(d(ν f * bot) * L) * top"
also have "... = μ f  (ν f  L)  d((ν f  L) * bot) * top"
using l51 by auto
also have "...  μ f  (ν f  L)  d((μ f  (ν f  L)) * bot) * top"
by (meson d_isotone inf.eq_refl mult_isotone semiring.add_left_mono sup.cobounded2)
finally show ?thesis
using nu_below_mu_nu_2_def by auto
qed

lemma nu_below_mu_nu_2_nu_below_mu_nu:
assumes
and
and
shows
proof -
have "d(L) * ν f  μ f  (ν f  L)  d((μ f  (ν f  L)) * bot) * top"
using assms(3) nu_below_mu_nu_2_def by blast
also have "...  μ f  (ν f  L)  d(ν f * bot) * top"
by (metis assms(1,2) d_isotone inf.sup_monoid.add_commute inf.sup_right_divisibility le_supI le_supI2 mu_below_nu mult_left_isotone sup_left_divisibility)
finally show ?thesis
qed

lemma nu_below_mu_nu_equivalent:

using nu_below_mu_nu_2_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2 by blast

lemma nu_below_mu_nu_2_mu_nu_apx_nu:
assumes
and
and
shows "mu_nu_apx_nu f"
proof -
have "μ f  (ν f  L)  ν f  L"
using assms(1,2) l_below_nu le_supI1 by blast
thus ?thesis
using assms(3) apx_def mu_nu_apx_nu_def nu_below_mu_nu_2_def by blast
qed

lemma mu_nu_apx_nu_mu_nu_apx_meet:
assumes "mu_nu_apx_nu f"
shows
proof -
let ?l = "μ f  (ν f  L)"
have "is_apx_meet (μ f) (ν f) ?l"
apply (unfold is_apx_meet_def, intro conjI)
using assms mu_nu_apx_nu_def apply blast
by (metis apx_meet_L le_supI2 sup.order_iff sup_apx_left_isotone sup_inf_absorb)
thus ?thesis
by (smt apx_meet_char mu_nu_apx_meet_def)
qed

lemma mu_nu_apx_meet_apx_meet_below_nu:

using apx_meet_below_nu_def l_below_nu mu_nu_apx_meet_def by auto

lemma apx_meet_below_nu_nu_below_mu_nu_2:
assumes
shows
proof -
let ?l = "μ f  (ν f  L)"
have "m . m  μ f  m  ν f  m  ν f  d(L) * ν f  ?l  d(?l * bot) * top"
proof
fix m
show "m  μ f  m  ν f  m  ν f  d(L) * ν f  ?l  d(?l * bot) * top"
proof
assume 1: "m  μ f  m  ν f  m  ν f"
hence "m  ?l"
by (metis apx_def ils.il_associative sup.orderE sup.orderI sup_inf_distrib1 sup_inf_distrib2)
hence "m  d(m * bot) * top  ?l  d(?l * bot) * top"
by (meson d_isotone order.trans le_supI le_supI2 mult_left_isotone sup.cobounded1)
thus "d(L) * ν f  ?l  d(?l * bot) * top"
using 1 apx_def order_lesseq_imp by blast
qed
qed
thus ?thesis
by (smt (verit) assms apx_meet_below_nu_def apx_meet_same apx_meet_unique is_apx_meet_def nu_below_mu_nu_2_def)
qed

lemma has_apx_least_fixpoint_kappa_apx_meet:
assumes
and
and
shows
proof -
have 1: "w . w  μ f  w  ν f  d(L) * κ f  w  d(w * bot) * top"
by (metis assms(2,3) apx_def mult_right_isotone order_trans kappa_below_nu)
have "w . w  μ f  w  ν f  w  κ f  L"
by (metis assms(1,3) sup_left_isotone apx_def mu_below_kappa order_trans)
hence "w . w  μ f  w  ν f  w  κ f"
using 1 apx_def by blast
hence "is_apx_meet (μ f) (ν f) (κ f)"
using assms apx_meet_char is_apx_meet_def kappa_apx_below_mu kappa_apx_below_nu kappa_apx_meet_def by presburger
thus ?thesis
by (simp add: assms(3) kappa_apx_meet_def apx_meet_char)
qed

lemma kappa_apx_meet_apx_meet_below_nu:

using apx_meet_below_nu_def kappa_apx_meet_def kappa_below_nu by force

lemma apx_meet_below_nu_kappa_mu_nu:
assumes
and
and "isotone f"
and "apx.isotone f"
and
shows "kappa_mu_nu f"
proof -
let ?l = "μ f  (ν f  L)"
let ?m = "μ f  ν f"
have 1: "?m = ?l"
by (metis assms(1,2,5) apx_meet_below_nu_nu_below_mu_nu_2 mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_2_mu_nu_apx_nu)
have 2: "?l  f(?l)  L"
proof -
have "?l  μ f  L"
using sup_right_isotone by auto
also have "... = f(μ f)  L"
also have "...  f(?l)  L"
by (metis assms(3) sup_left_isotone sup_ge1 isotone_def)
finally show ?thesis
.
qed
have "d(L) * f(?l)  ?l  d(?l * bot) * top"
proof -
have "d(L) * f(?l)  d(L) * f(ν f)"
by (metis assms(1-3) l_below_nu mult_right_isotone ord.isotone_def)
also have "... = d(L) * ν f"
by (metis assms(2) nu_unfold)
also have "...  ?l  d(?l * bot) * top"
using apx_meet_below_nu_nu_below_mu_nu_2 assms(5) nu_below_mu_nu_2_def by blast
finally show ?thesis
.
qed
hence 3: "?l  f(?l)"
using 2 by (simp add: apx_def)
have 4: "f(?l)  μ f"
proof -
have "?l  μ f"
thus ?thesis
by (metis assms(1,4) mu_unfold ord.isotone_def)
qed
have 5: "f(?l)  ν f"
proof -
have "?l  ν f"
by (meson apx_meet_below_nu_nu_below_mu_nu_2 assms(1,2,5) l_below_nu apx_def le_supI1 nu_below_mu_nu_2_def)
thus ?thesis
by (metis assms(2,4) nu_unfold ord.isotone_def)
qed
hence "f(?l)  ?l"
using 1 4 apx_meet_below_nu_def assms(5) apx_greatest_lower_bound by fastforce
hence 6: "f(?l) = ?l"
using 3 apx.order.antisym by blast
have "y . f(y) = y  ?l  y"
proof
fix y
show "f(y) = y  ?l  y"
proof
assume 7: "f(y) = y"
hence 8: "?l  y  L"
using assms(1) inf.cobounded2 is_least_fixpoint_def least_fixpoint semiring.add_mono by blast
have "y  ν f"
using 7 assms(2) greatest_fixpoint is_greatest_fixpoint_def by auto
hence "d(L) * y  ?l  d(?l * bot) * top"
using 3 5 by (smt (z3) apx.order.trans apx_def semiring.distrib_left sup.absorb_iff2 sup_assoc)
thus "?l  y"
using 8 by (simp add: apx_def)
qed
qed
thus ?thesis
using 1 6 by (smt (verit) kappa_mu_nu_def apx.is_least_fixpoint_def apx.least_fixpoint_char)
qed

lemma kappa_mu_nu_has_apx_least_fixpoint:

lemma nu_below_mu_nu_kappa_mu_nu:

using apx_meet_below_nu_kappa_mu_nu mu_nu_apx_meet_apx_meet_below_nu mu_nu_apx_nu_mu_nu_apx_meet nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_nu_below_mu_nu_2 by blast

lemma kappa_mu_nu_nu_below_mu_nu:

by (simp add: apx_meet_below_nu_nu_below_mu_nu_2 has_apx_least_fixpoint_kappa_apx_meet kappa_apx_meet_apx_meet_below_nu kappa_mu_nu_def nu_below_mu_nu_2_nu_below_mu_nu)

definition kappa_mu_nu_L :: "('a  'a)  bool"
where "kappa_mu_nu_L f  apx.has_least_fixpoint f  κ f = μ f  d(ν f * bot) * L"

definition nu_below_mu_nu_L :: "('a  'a)  bool"
where "nu_below_mu_nu_L f  d(L) * ν f  μ f  d(ν f * bot) * top"

definition mu_nu_apx_nu_L :: "('a  'a)  bool"
where "mu_nu_apx_nu_L f  μ f  d(ν f * bot) * L  ν f"

definition mu_nu_apx_meet_L :: "('a  'a)  bool"
where "mu_nu_apx_meet_L f  has_apx_meet (μ f) (ν f)  μ f  ν f = μ f  d(ν f * bot) * L"

lemma n_below_l:
"x  d(y * bot) * L  x  (y  L)"
using d_mult_below l13 sup_right_isotone by auto

lemma n_equal_l:
assumes
shows"μ f  d(ν f * bot) * L = μ f  (ν f  L)"
proof -
have "ν f  L  (μ f  d(ν f * bot) * top)  L"
using assms l31 nu_below_mu_nu_L_def by force
also have "...  μ f  d(ν f * bot) * L"
using distrib(4) inf.sup_monoid.add_commute meet_domain_top sup_left_isotone by force
finally have "μ f  (ν f  L)  μ f  d(ν f * bot) * L"
by auto
thus ?thesis
by (meson order.antisym n_below_l)
qed

lemma nu_below_mu_nu_L_nu_below_mu_nu:

using order_lesseq_imp sup.cobounded1 sup_left_isotone nu_below_mu_nu_L_def nu_below_mu_nu_def by blast

lemma nu_below_mu_nu_L_kappa_mu_nu_L:

using kappa_mu_nu_L_def kappa_mu_nu_def n_equal_l nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_kappa_mu_nu by auto

lemma nu_below_mu_nu_L_mu_nu_apx_nu_L:

using mu_nu_apx_nu_L_def mu_nu_apx_nu_def n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2 by auto

lemma nu_below_mu_nu_L_mu_nu_apx_meet_L:

using mu_nu_apx_meet_L_def mu_nu_apx_meet_def mu_nu_apx_nu_mu_nu_apx_meet n_equal_l nu_below_mu_nu_2_mu_nu_apx_nu nu_below_mu_nu_L_nu_below_mu_nu nu_below_mu_nu_nu_below_mu_nu_2 by auto

lemma mu_nu_apx_nu_L_nu_below_mu_nu_L:
assumes
and
and
shows
proof -
let ?n = "μ f  d(ν f * bot) * L"
let ?l = "μ f  (ν f  L)"
have "d(L) * ν f  ?n  d(?n * bot) * top"
using assms(3) apx_def mu_nu_apx_nu_L_def by blast
also have "...  ?n  d(?l * bot) * top"
using d_isotone mult_left_isotone semiring.add_left_mono n_below_l by auto
also have "...  ?n  d(ν f * bot) * top"
by (meson assms(1,2) l_below_nu d_isotone mult_left_isotone sup_right_isotone)
finally show ?thesis
by (metis sup_assoc sup_right_top mult_left_dist_sup nu_below_mu_nu_L_def)
qed

lemma kappa_mu_nu_L_mu_nu_apx_nu_L:

using kappa_mu_nu_L_def kappa_apx_below_nu mu_nu_apx_nu_L_def by force

lemma mu_nu_apx_meet_L_mu_nu_apx_nu_L:

using apx_greatest_lower_bound mu_nu_apx_meet_L_def mu_nu_apx_nu_L_def by fastforce

lemma kappa_mu_nu_L_nu_below_mu_nu_L:

using kappa_mu_nu_L_mu_nu_apx_nu_L mu_nu_apx_nu_L_nu_below_mu_nu_L by auto

end

class itering_apx = domain_itering_lattice_L + domain_semiring_lattice_apx
begin

lemma circ_apx_isotone:
assumes "x  y"
shows "x  y"
proof -
have 1: "x  y  L  d(L) * y  x  d(x * bot) * top"
using assms apx_def by auto
have "d(L) * y  (d(L) * y)"
by (metis d_circ_import d_mult_below l2)
also have "...  x * (d(x * bot) * top * x)"
using 1 by (metis circ_sup_1 circ_isotone)
also have "... = x  x * d(x * bot) * top"
by (metis circ_left_top mult_assoc mult_left_dist_sup mult_1_right mult_top_circ)
also have "...  x  d(x * x * bot) * top"
by (metis sup_right_isotone mult_assoc mult_domain_top)
finally have 2: "d(L) * y  x  d(x * bot) * top"
using circ_plus_same d0_circ_left_unfold by auto
have "x  y * L"
using 1 by (metis circ_sup_1 circ_back_loop_fixpoint circ_isotone l40 le_iff_sup mult_assoc)
also have "... = y  y * L"
by (simp add: circ_L mult_left_dist_sup sup_commute)
also have "...  y  y * bot  L"
finally have "x  y  L"
using sup.absorb_iff1 zero_right_mult_decreasing by auto
thus ?thesis
using 2 by (simp add: apx_def)
qed

end

class omega_algebra_apx = domain_omega_algebra_lattice_L + domain_semiring_lattice_apx

sublocale omega_algebra_apx < star: itering_apx where circ = star ..

context omega_algebra_apx
begin

lemma omega_apx_isotone:
assumes "x  y"
shows "xω  yω"
proof -
have 1: "x  y  L  d(L) * y  x  d(x * bot) * top"
using assms apx_def by auto
have "d(L) * yω = (d(L) * y)ω"
also have "...  (x  d(x * bot) * top)ω"
using 1 by (simp add: omega_isotone)
also have "... = (x * d(x * bot) * top)ω  (x * d(x * bot) * top) * xω"
also have "...  x * d(x * bot) * top  (x * d(x * bot) * top) * xω"
using mult_top_omega sup_left_isotone by blast
also have "... = x * d(x * bot) * top  (1  x * d(x * bot) * top * (x * d(x * bot) * top)) * xω"
also have "...  xω  x * d(x * bot) * top"
by (smt (verit, ccfv_threshold) sup_mono le_sup_iff mult_assoc mult_left_one mult_right_dist_sup mult_right_isotone order_refl top_greatest)
also have "...  xω  d(x * x * bot) * top"
by (metis sup_right_isotone mult_assoc mult_domain_top)
also have "...  xω  d(x * bot) * top"
finally have 2: "d(L) * yω  xω  d(xω * bot) * top"
by (meson sup_right_isotone d0_star_below_d0_omega mult_left_isotone order_trans)
have "xω  (y  L)ω"
using 1 by (simp add: omega_isotone)
also have "... = (y * L)ω  (y * L) * yω"
also have "... = y * L * (y * L)ω  (y * L) * yω"
using omega_unfold by auto
also have "...  y * L  (y * L) * yω"
using mult_L_omega omega_unfold sup_left_isotone by auto
also have "... = y * L  (1  y * L * (y * L)) * yω"
also have "...  y * L  yω"
by (simp add: dL_star.mult_L_circ_mult_below star_left_unfold_equal sup_commute)
also have "...  y * bot  L  yω"
finally have "xω  yω  L"
using star_bot_below_omega sup.left_commute sup.order_iff sup_commute by auto
thus ?thesis
using 2 by (simp add: apx_def)
qed

lemma combined_apx_isotone:
"x  y  (xω  L)  x * z  (yω  L)  y * z"
using meet_L_apx_isotone mult_apx_left_isotone star.circ_apx_isotone sup_apx_isotone omega_apx_isotone by auto

lemma d_split_nu_mu:
"d(L) * (yω  y * z)  y * z  ((yω  y * z)  L)  d((yω  y * z) * bot) * top"
proof -
have "d(L) * yω  (yω  L)  d(yω * bot) * top"
using l31 l91 omega_vector sup_right_isotone by auto
hence "d(L) * (yω  y * z)  y * z  (yω  L)  d(yω * bot) * top"
by (smt sup_assoc sup_commute sup_mono d_mult_below mult_left_dist_sup)
also have "...  y * z  ((yω  y * z)  L)  d(yω * bot) * top"
also have "...  y * z  ((yω  y * z)  L)  d((yω  y * z) * bot) * top"
by (meson d_isotone mult_left_isotone sup.cobounded1 sup_right_isotone)
finally show ?thesis
.
qed

lemma loop_exists:
"d(L) * ν (λx . y * x  z)  μ (λx . y * x  z)  (ν (λx . y * x  z)  L)  d(ν (λx . y * x  z) * bot) * top"
by (simp add: d_split_nu_mu omega_loop_nu star_loop_mu)

lemma loop_apx_least_fixpoint:
"apx.is_least_fixpoint (λx . y * x  z) (μ (λx . y * x  z)  (ν (λx . y * x  z)  L))"
using apx.least_fixpoint_char affine_apx_isotone loop_exists affine_has_greatest_fixpoint affine_has_least_fixpoint affine_isotone nu_below_mu_nu_def nu_below_mu_nu_kappa_mu_nu kappa_mu_nu_def by auto

lemma loop_has_apx_least_fixpoint:
"apx.has_least_fixpoint (λx . y * x  z)"
by (metis apx.has_least_fixpoint_def loop_apx_least_fixpoint)

lemma loop_semantics:
"κ (λx . y * x  z) = μ (λx . y * x  z)  (ν (λx . y * x  z)  L)"
using apx.least_fixpoint_char loop_apx_least_fixpoint by auto

lemma loop_semantics_kappa_mu_nu:
"κ (λx . y * x  z) = (yω  L)  y * z"
proof -
have "κ (λx . y * x  z) = y * z  ((yω  y * z)  L)"
by (metis loop_semantics omega_loop_nu star_loop_mu)
thus ?thesis
by (metis sup.absorb2 sup_commute sup_ge2 sup_inf_distrib1)
qed

lemma loop_semantics_kappa_mu_nu_domain:
"κ (λx . y * x  z) = d(yω) * L  y * z"