Theory KAD.Modal_Kleene_Algebra_Applications

(* Title:      Applications of Modal Kleene Algebras
   Author:     Victor B. F. Gomes, Walter Guttmann, Peter Höfner, Georg Struth, Tjark Weber
   Maintainer: Walter Guttmann <walter.guttman at canterbury.ac.nz>
               Georg Struth <g.struth at sheffield.ac.uk>
               Tjark Weber <tjark.weber at it.uu.se>
*)

section ‹Applications of Modal Kleene Algebras›

theory Modal_Kleene_Algebra_Applications
imports Antidomain_Semiring
begin

text ‹This file collects some applications of the theories developed so far. These are described
 in~cite"guttmannstruthweber11algmeth".›

context antidomain_kleene_algebra
begin

subsection ‹A Reachability Result›

text ‹This example is taken from~cite"desharnaismoellerstruth06kad".›

lemma opti_iterate_var [simp]: "|(ad y  x) y = |x y"
proof (rule order.antisym)
  show "|(ad y  x) y  |x y"
    by (simp add: a_subid_aux1' ds.fd_iso2 star_iso)
  have "d y + |x |(ad y  x) y = d y + ad y  |x |(ad y  x) y"
    using local.ads_d_def local.d_6 local.fdia_def by auto
  also have "... = d y + |ad y  x |(ad y  x) y"
    by (simp add: fdia_export_2)
  finally have "d y + |x |(ad y  x) y = |(ad y  x) y"
    by simp
  thus "|x y  |(ad y  x) y"
    using local.dka.fd_def local.dka.fdia_star_induct_eq by auto
qed

lemma opti_iterate [simp]: "d y + |(x  ad y) |x y = |x y"
proof -
  have "d y + |(x  ad y) |x y = d y + |x |(ad y  x) y"
    by (metis local.conway.dagger_slide local.ds.fdia_mult)
  also have "... = d y + |x |x y"
    by simp
  finally show ?thesis
    by force
qed

lemma opti_iterate_var_2 [simp]: "d y + |ad y  x |x y = |x y"
  by (metis local.dka.fdia_star_unfold_var opti_iterate_var)

subsection ‹Derivation of Segerberg's Formula›

text ‹This example is taken from~cite"DesharnaisMoellerStruthLMCS".›

definition Alpha :: "'a  'a  'a" ("A")
  where "A x y = d (x  y)  ad y"

lemma A_dom [simp]: "d (A x y) = A x y"
  using Alpha_def local.a_d_closed local.ads_d_def local.apd_d_def by auto

lemma A_fdia: "A x y = |x y  ad y"
  by (simp add: Alpha_def local.dka.fd_def)

lemma A_fdia_var: "A x y = |x d y  ad y"
  by (simp add: A_fdia)

lemma a_A: "ad (A x (ad y)) = |x] y + ad y"
  using Alpha_def local.a_6 local.a_d_closed local.apd_d_def local.fbox_def by force

lemma fsegerberg [simp]: "d y + |x A x y = |x y"
proof (rule order.antisym)
  have "d y + |x (d y + |x A x y) = d y + |x y + |x |x ( |x y  ad y )"
    by (simp add: A_fdia add_assoc local.ds.fdia_add1)
  also have "... = d y + |x y  ad y + |x |x ( |x y  ad y )"
    by (metis local.am2 local.d_6 local.dka.fd_def local.fdia_def)
  finally have "d y + |x (d y + |x A x y) = d y + |x A x y"
    by (metis A_dom A_fdia add_assoc local.dka.fdia_star_unfold_var)
  thus "|x y  d y + |x A x y"
    by (metis local.a_d_add_closure local.ads_d_def local.dka.fdia_star_induct_eq local.fdia_def)
  have "d y + |x A x y = d y + |x ( |x y  ad y )"
    by (simp add: A_fdia)
  also have "...  d y + |x |x y"
    using local.dpdz.domain_1'' local.ds.fd_iso1 local.join.sup_mono by blast
  finally show "d y + |x A x y  |x y"
    by simp
qed

lemma fbox_segerberg [simp]: "d y  |x] ( |x] y + ad y ) = |x] y"
proof -
  have "|x] ( |x] y + ad y ) = d ( |x] ( |x] y + ad y ) )"
    using local.a_d_closed local.ads_d_def local.apd_d_def local.fbox_def by auto
  hence f1: "|x] ( |x] y + ad y ) = ad ( |x (A x (ad y)) )"
    by (simp add: a_A local.fdia_fbox_de_morgan_2)
  have "ad y + |x (A x (ad y)) = |x ad y"
    by (metis fsegerberg local.a_d_closed local.ads_d_def local.apd_d_def)
  thus ?thesis
    by (metis f1 local.ads_d_def local.ans4 local.fbox_simp local.fdia_fbox_de_morgan_2)
qed

subsection ‹Wellfoundedness and Loeb's Formula›

text ‹This example is taken from~cite"DesharnaisStruthSCP".›

definition Omega :: "'a  'a  'a" ("Ω")
  where "Ω x y = d y  ad (x  y)"

text ‹If $y$ is a set, then $\Omega(x,y)$ describes those elements in $y$ from which no further $x$ transitions are possible.›

lemma omega_fdia: "Ω x y = d y  ad ( |x y )"
  using Omega_def local.a_d_closed local.ads_d_def local.apd_d_def local.dka.fd_def by auto

lemma omega_fbox: "Ω x y = d y  |x] (ad y)"
  by (simp add: fdia_fbox_de_morgan_2 omega_fdia)

lemma omega_absorb1 [simp]: "Ω x y  ad ( |x y ) = Ω x y"
  by (simp add: mult_assoc omega_fdia)

lemma omega_absorb2 [simp]: "Ω x y  ad (x  y) = Ω x y"
  by (simp add: Omega_def mult_assoc)

lemma omega_le_1: "Ω x y  d y"
  by (simp add: Omega_def d_a_galois1)

lemma omega_subid: "Ω x (d y)  d y"
  by (simp add: Omega_def local.a_subid_aux2)

lemma omega_le_2: "Ω x y  ad ( |x y )"
  by (simp add: local.dka.dom_subid_aux2 omega_fdia)

lemma omega_dom [simp]: "d (Ω x y) = Ω x y"
  using Omega_def local.a_d_closed local.ads_d_def local.apd_d_def by auto

lemma a_omega: "ad (Ω x y) = ad y + |x y"
  by (simp add: Omega_def local.a_6 local.ds.fd_def)

lemma omega_fdia_3 [simp]: "d y  ad (Ω x y) = d y  |x y"
  using Omega_def local.ads_d_def local.fdia_def local.s4 by presburger

lemma omega_zero_equiv_1: "Ω x y = 0  d y  |x y"
  by (simp add: Omega_def local.a_gla local.ads_d_def local.fdia_def)

definition Loebian :: "'a  bool"
  where "Loebian x = (y. |x y  |x Ω x y)"

definition PreLoebian :: "'a  bool"
  where "PreLoebian x = (y. d y  |x Ω x y)"

definition Noetherian :: "'a  bool"
  where "Noetherian x = (y. Ω x y = 0  d y = 0)"

lemma noetherian_alt: "Noetherian x  (y. d y  |x y  d y = 0)"
  by (simp add: Noetherian_def omega_zero_equiv_1)

lemma Noetherian_iff_PreLoebian: "Noetherian x  PreLoebian x"
proof
  assume hyp: "Noetherian x"
  {
    fix y
    have "d y  ad ( |x Ω x y ) = d y  ad (Ω x y + |x |x Ω x y)"
      by (metis local.dka.fdia_star_unfold_var omega_dom)
    also have "... = d y  ad (Ω x y)  ad ( |x |x Ω x y )"
      using ans4 mult_assoc by presburger
    also have "...  |x d y  ad ( |x |x Ω x y )"
      by (simp add: local.dka.dom_subid_aux2 local.mult_isor)
    also have "...  |x (d y  ad ( |x Ω x y ))"
      by (simp add: local.dia_diff)
    finally have "d y  ad ( |x Ω x y )  |x (d y  ad ( |x Ω x y ))"
      by blast
    hence "d y  ad ( |x Ω x y ) = 0"
      by (metis hyp local.ads_d_def local.dpdz.dom_mult_closed local.fdia_def noetherian_alt)
    hence "d y  |x Ω x y"
      by (simp add: local.a_gla local.ads_d_def local.dka.fd_def)
  }
  thus "PreLoebian x"
    using PreLoebian_def by blast
next
  assume a: "PreLoebian x"
  {
    fix y
    assume b: "Ω x y = 0"
    hence "d y  |x d y"
      using omega_zero_equiv_1 by auto
    hence "d y = 0"
      by (metis (no_types) PreLoebian_def a b a_one a_zero add_zeror annir fdia_def less_eq_def)
  }
  thus "Noetherian x"
    by (simp add: Noetherian_def)
qed

lemma Loebian_imp_Noetherian: "Loebian x  Noetherian x"
proof -
  assume a: "Loebian x"
  {
    fix y
    assume b: "Ω x y = 0"
    hence "d y  |x d y"
      using omega_zero_equiv_1 by auto
    also have "...  |x (Ω x y)"
      using Loebian_def a by auto
    finally have "d y = 0"
      by (simp add: b order.antisym fdia_def)
  }
  thus "Noetherian x"
    by (simp add: Noetherian_def)
qed

lemma d_transitive: "(y. |x |x y  |x y)  (y. |x y = |x |x y)"
proof -
  assume a: "y. |x |x y  |x y"
  {
    fix y
    have "|x y + |x |x y  |x y"
      by (simp add: a)
    hence "|x |x y  |x y"
      using local.dka.fd_def local.dka.fdia_star_induct_var by auto
    have "|x y  |x |x y"
      using local.dka.fd_def local.order_prop opti_iterate by force
  }
  thus ?thesis
    using a order.antisym dka.fd_def dka.fdia_star_induct_var by auto
qed

lemma d_transitive_var: "(y. |x |x y  |x y)  (y. |x y = |x |x y)"
proof -
  assume "y. |x |x y  |x y"
  then have "a. |x |x a = |x a"
    by (metis (full_types) d_transitive local.dka.fd_def local.dka.fdia_d_simp local.star_slide_var mult_assoc)
  then show ?thesis
    by presburger
qed

lemma d_transitive_PreLoebian_imp_Loebian: "(y. |x |x y  |x y)  PreLoebian x  Loebian x"
proof -
  assume wt: "(y. |x |x y  |x y)"
  and "PreLoebian x"
  hence "y. |x y  |x |x Ω x y"
    using PreLoebian_def local.ads_d_def local.dka.fd_def local.ds.fd_iso1 by auto
  hence "y. |x y  |x Ω x y"
    by (metis wt d_transitive_var)
  then show "Loebian x"
    using Loebian_def fdia_def by auto
qed

lemma d_transitive_Noetherian_iff_Loebian: "y. |x |x y  |x y  Noetherian x  Loebian x"
  using Loebian_imp_Noetherian Noetherian_iff_PreLoebian d_transitive_PreLoebian_imp_Loebian by blast

lemma Loeb_iff_box_Loeb: "Loebian x  (y. |x] (ad ( |x] y ) + d y)  |x] y)"
proof -
  have "Loebian x  (y. |x y  |x (d y  |x] (ad y)))"
    using Loebian_def omega_fbox by auto
  also have "...  (y. ad ( |x (d y  |x] (ad y)) )  ad ( |x y ))"
    using a_antitone' fdia_def by fastforce
  also have "...  (y. |x] ad (d y  |x] (ad y))  |x] (ad y))"
    by (simp add: fdia_fbox_de_morgan_2)
  also have "...  (y. |x] (d (ad y) + ad ( |x] (ad y) ))  |x] (ad y))"
    by (simp add: local.ads_d_def local.fbox_def)
  finally show ?thesis
    by (metis add_commute local.a_d_closed local.ads_d_def local.apd_d_def local.fbox_def)
qed

end

subsection ‹Divergence Kleene Algebras and Separation of Termination›

text ‹The notion of divergence has been added to modal Kleene algebras in~cite"DesharnaisMoellerStruthLMCS".
More facts about divergence could be added in the future. Some could be adapted from omega algebras.›

class nabla_op =
  fixes nabla :: "'a  'a" ("_" [999] 1000)

class fdivergence_kleene_algebra = antidomain_kleene_algebra + nabla_op +
  assumes nabla_closure [simp]: "d  x =  x"
  and nabla_unfold: " x  |x  x"
  and nabla_coinduction: "d y  |x y + d z  d y   x + |x z"

begin

lemma nabla_coinduction_var: "d y  |x y  d y   x"
proof -
  assume "d y  |x y"
  hence "d y  |x y + d 0"
    by simp
  hence "d y   x + |x 0"
    using nabla_coinduction by blast
  thus "d y   x"
    by (simp add: fdia_def)
qed

lemma nabla_unfold_eq [simp]: "|x  x =  x"
proof -
  have f1: "ad (ad (x  x)) = ad (ad (x  x)) + x"
    using local.ds.fd_def local.join.sup.order_iff local.nabla_unfold by presburger
  then have "ad (ad (x  x))  ad (ad x) = x"
    by (metis local.ads_d_def local.dpdz.dns5 local.dpdz.dsg4 local.join.sup_commute local.nabla_closure)
  then show ?thesis
    using f1 by (metis local.ads_d_def local.ds.fd_def local.ds.fd_subdist_2 local.join.sup.order_iff local.join.sup_commute nabla_coinduction_var)
qed

lemma nabla_subdist: " x   (x + y)"
proof -
  have "d  x   (x + y)"
    by (metis local.ds.fd_iso2 local.join.sup.cobounded1 local.nabla_closure nabla_coinduction_var nabla_unfold_eq)
  thus ?thesis
    by simp
qed

lemma nabla_iso: "x  y   x   y"
  by (metis less_eq_def nabla_subdist)

lemma nabla_omega: "Ω x (d y) = 0  d y   x"
  using omega_zero_equiv_1 nabla_coinduction_var by fastforce

lemma nabla_noether: " x = 0  Noetherian x"
  using local.join.le_bot local.noetherian_alt nabla_coinduction_var by blast

lemma nabla_preloeb: " x = 0  PreLoebian x"
  using Noetherian_iff_PreLoebian nabla_noether by auto

lemma star_nabla_1 [simp]: "|x  x =  x"
proof (rule order.antisym)
  show "|x  x   x"
    by (metis dka.fdia_star_induct_var order.eq_iff nabla_closure nabla_unfold_eq)
  show " x  |x  x"
    by (metis ds.fd_iso2 star_ext nabla_unfold_eq)
qed

lemma nabla_sum_expand [simp]: "|x  (x + y) + |y  (x + y) =  (x + y)"
proof -
  have "d ((x + y)  (x + y)) = (x + y)"
    using local.dka.fd_def nabla_unfold_eq by presburger
  thus ?thesis
    by (simp add: local.dka.fd_def)
qed

lemma wagner_3:
  assumes "d z + |x  (x + y) =  (x + y)"
  shows " (x + y) =  x + |x z"
proof (rule order.antisym)
  have "d (x + y)  d z + |x (x + y)"
    by (simp add: assms)
  thus " (x + y)   x + |x z"
    by (metis add_commute nabla_closure nabla_coinduction)
  have "d z + |x  (x + y)   (x + y)"
    using assms by auto
  hence "|x z   (x + y)"
    by (metis local.dka.fdia_star_induct local.nabla_closure)
  thus " x + |x z   (x + y)"
    by (simp add: sup_least nabla_subdist)
qed

lemma nabla_sum_unfold [simp]: " x + |x |y  (x + y) =  (x + y)"
proof -
  have " (x + y) = |x  (x + y) + |y  (x + y)"
    by simp
  thus ?thesis
    by (metis add_commute local.dka.fd_def local.ds.fd_def local.ds.fdia_d_simp wagner_3)
qed

lemma nabla_separation: "y  x  x  (x + y)  ( (x + y) =  x + |x  y)"
proof (rule order.antisym)
  assume quasi_comm: "y  x  x  (x + y)"
  hence a: "y  x  x  (x + y)"
    using quasicomm_var by blast
  have " (x + y) =  y + |y x  (x + y)"
    by (metis local.ds.fdia_mult local.join.sup_commute nabla_sum_unfold)
  also have "...   y + |x  (x + y)  (x + y)"
    using a local.ds.fd_iso2 local.join.sup.mono by blast
  also have "... =  y + |x |(x + y)  (x + y)"
    by (simp add: fdia_def mult_assoc)
  finally have " (x + y)   y + |x  (x + y)"
    by (metis star_nabla_1)
  thus " (x + y)   x + |x  y"
    by (metis add_commute nabla_closure nabla_coinduction)
next
  have " x + |x  y =  x + |x |y  y"
    by simp
  also have "... =  x + |x  y  y"
    by (simp add: fdia_def mult_assoc)
  also have "...   x + |x  y  (x + y)"
    using dpdz.dom_iso eq_refl fdia_def join.sup_ge2 join.sup_mono mult_isol nabla_iso by presburger
  also have "... =  x + |x |y  (x + y)"
    by (simp add: fdia_def mult_assoc)
  finally show " x + |x  y   (x + y)"
    by (metis nabla_sum_unfold)
qed

text ‹The next lemma is a separation of termination theorem by Bachmair and Dershowitz~cite"bachmair86commutation".›

lemma bachmair_dershowitz: "y  x  x  (x + y)   x +  y = 0   (x + y) = 0"
proof -
  assume quasi_comm: "y  x  x  (x + y)"
  have "x. |x 0 = 0"
    by (simp add: fdia_def)
  hence "y = 0  x + y = 0  (x + y) = 0"
    using quasi_comm nabla_separation by presburger
  thus ?thesis
    using add_commute local.join.le_bot nabla_subdist by fastforce
qed

text ‹The next lemma is a more complex separation of termination theorem by Doornbos,
Backhouse and van der Woude~cite"doornbos97calculational".›

lemma separation_of_termination:
assumes "y  x  x  (x + y) + y"
shows " x +  y = 0   (x + y) = 0"
proof
  assume xy_wf: " x +  y = 0"
  hence x_preloeb: " (x + y)  |x Ω x ( (x + y))"
    by (metis PreLoebian_def no_trivial_inverse nabla_closure nabla_preloeb)
  hence y_div: " y = 0"
    using add_commute no_trivial_inverse xy_wf by blast
  have " (x + y)  |y  (x + y) + |x  (x + y)"
    by (simp add: local.join.sup_commute)
  hence " (x + y)  ad ( |x  (x + y) )  |y (x + y)"
    by (simp add: local.da_shunt1 local.dka.fd_def local.join.sup_commute)
  hence "Ω x (x + y)  |y  (x + y)"
    by (simp add: fdia_def omega_fdia)
  also have "...  |y |x (Ω x (x + y))"
    using local.dpdz.dom_iso local.ds.fd_iso1 x_preloeb by blast
  also have "... = |y  x (Ω x (x + y))"
    by (simp add: fdia_def mult_assoc)
  also have "...  |x  (x + y) + y (Ω x (x + y))"
    using assms local.ds.fd_iso2 local.lazycomm_var by blast
  also have "... = |x  (x + y) (Ω x (x + y)) + |y (Ω x (x + y))"
    by (simp add: local.dka.fd_def)
  also have "...  |(x  (x + y)) (x + y) + |y (Ω x (x + y))"
    using local.add_iso local.dpdz.domain_1'' local.ds.fd_iso1 local.omega_fdia by auto
  also have "...  |x |(x + y) (x + y) + |y (Ω x (x + y))"
    by (simp add: fdia_def mult_assoc)
  finally have "Ω x (x + y)  |x (x + y) + |y (Ω x (x + y))"
    by (metis star_nabla_1)
  hence "Ω x (x + y)  ad ( |x (x + y) )  |y (Ω x (x + y))"
    by (simp add: local.da_shunt1 local.dka.fd_def)
  hence "Ω x (x + y)  |y (Ω x (x + y))"
    by (simp add: omega_fdia mult_assoc)
  hence "(Ω x (x + y)) = 0"
    by (metis noetherian_alt omega_dom nabla_noether y_div)
  thus " (x + y) = 0"
    using local.dka.fd_def local.join.le_bot x_preloeb by auto
next
  assume " (x + y) = 0"
  thus "( x) + ( y) = 0"
    by (metis local.join.le_bot local.join.sup.order_iff local.join.sup_commute nabla_subdist)
qed

text ‹The final examples can be found in~cite"guttmannstruthweber11algmeth".›

definition T :: "'a  'a  'a  'a" ("_  _  _" [61,61,61] 60)
  where "pxq  ad p + |x] d q"

lemma T_d [simp]: "d (pxq) = pxq"
  using T_def local.a_d_add_closure local.fbox_def by auto

lemma T_p: "d p  (pxq) = d p  |x] d q"
proof -
  have "d p  (pxq) = ad (ad p + ad (pxq))"
    using T_d local.ads_d_def by auto
  thus ?thesis
    using T_def add_commute local.a_mult_add local.ads_d_def by auto
qed

lemma T_a [simp]: "ad p  (pxq) = ad p"
  by (metis T_d T_def local.a_d_closed local.ads_d_def local.apd_d_def local.dpdz.dns5 local.join.sup.left_idem)

lemma T_seq: "(pxq)  |x](qys)  px  ys"
proof -
  have f1: "|x] q = |x] d q"
    using local.fbox_simp by auto
  have "ad p  ad (x  ad (qys)) + |x] d q  |x] (ad q + |y] d s)  ad p + |x] d q  |x] (ad q + |y] d s)"
    using local.a_subid_aux2 local.add_iso by blast
  hence "(pxq)  |x](qys)  ad p + |x](d q  (qys))"
    by (metis T_d T_def f1 local.distrib_right' local.fbox_add1 local.fbox_def)
  also have "... = ad p + |x](d q  (ad q + |y] d s))"
    by (simp add: T_def)
  also have "... = ad p + |x](d q  |y] d s)"
    using T_def T_p by auto
  also have "...  ad p + |x] |y] d s"
    by (metis (no_types, lifting) dka.dom_subid_aux2 dka.dsg3 order.eq_iff fbox_iso join.sup.mono)
  finally show ?thesis
    by (simp add: T_def fbox_mult)
qed

lemma T_square: "(pxq)  |x](qxp)  pxxp"
  by (simp add: T_seq)

lemma T_segerberg [simp]: "d p  |x](pxp) = |x] d p"
  using T_def add_commute local.fbox_segerberg local.fbox_simp by force

lemma lookahead [simp]: "|x](d p  |x] d p) = |x] d p"
  by (metis (full_types) local.dka.dsg3 local.fbox_add1 local.fbox_mult local.fbox_simp local.fbox_star_unfold_var local.star_slide_var local.star_trans_eq)

lemma alternation: "d p  |x]((pxq)  (qxp)) = |(xx)](d p  (qxp))  |x(xx)](d q  (pxq))"
proof -
  have fbox_simp_2: "x p. |x]p = d( |x] p )"
    using local.a_d_closed local.ads_d_def local.apd_d_def local.fbox_def by fastforce
  have "|(xx)]((pxq)  |x](qxp)  (qxp)  |x](pxq))  |(xx)]((pxq)  |x](qxp))"
    using local.dka.domain_1'' local.fbox_iso local.order_trans by blast
  also have "...  |(xx)](pxxp)"
    using T_seq local.dka.dom_iso local.fbox_iso by blast
  finally have 1: "|(xx)]((pxq)  |x](qxp)  (qxp)  |x](pxq))  |(xx)](pxxp)".
  have "d p  |x]((pxq)  (qxp)) = d p  |1+x] |(xx)]((pxq)  (qxp))"
    by (metis (full_types) fbox_mult meyer_1)
  also have "... = d p  |(xx)]((pxq)  (qxp))  |x(xx)]((pxq)  (qxp))"
    using fbox_simp_2 fbox_mult fbox_add2 mult_assoc by auto
  also have "... = d p  |(xx)]((pxq)  (qxp))  |(xx)x]((pxq)  (qxp))"
    by (simp add: star_slide)
  also have "... = d p  |(xx)]((pxq)  (qxp))  |(xx)] |x]((pxq)  (qxp))"
    by (simp add: fbox_mult)
  also have "... = d p  |(xx)]((pxq)  (qxp)  |x]((pxq)  (qxp)))"
    by (metis T_d fbox_simp_2 local.dka.dom_mult_closed local.fbox_add1 mult_assoc)
  also have "... = d p  |(xx)]((pxq)  |x](qxp)  (qxp)  |x](pxq))"
  proof -
    have f1: "d ((q  x  p)  |x] (p  x  q)) = (q  x  p)  |x] (p  x  q)"
      by (metis (full_types) T_d fbox_simp_2 local.dka.dsg3)
    then have "|(x  x)] (d ( |x] (q  x  p))  ((q  x  p)  |x] (p  x  q))) = |(x  x)] d ( |x] (q  x  p))  |(x  x)] ((q  x  p)  |x] (p  x  q))"
      by (metis (full_types) fbox_simp_2 local.fbox_add1)
    then have f2: "|(x  x)] (d ( |x] (q  x  p))  ((q  x  p)  |x] (p  x  q))) = ad ((x  x)  ad ((q  x  p)  |x] (p  x  q)) + (x  x)  ad (d ( |x] (q  x  p))))"
      by (simp add: add_commute local.fbox_def)
    have "d ( |x] (p  x  q))  d ( |x] (q  x  p)) = |x] ((p  x  q)  (q  x  p))"
      by (metis (no_types) T_d fbox_simp_2 local.fbox_add1)
    then have "d ((q  x  p)  |x] (p  x  q))  d (d ( |x] (q  x  p))) = (q  x  p)  |x] ((p  x  q)  (q  x  p))"
      using f1 fbox_simp_2 mult_assoc by force
    then have "|(x  x)] (d ( |x] (q  x  p))  ((q  x  p)  |x] (p  x  q))) = |(x  x)] ((q  x  p)  |x] ((p  x  q)  (q  x  p)))"
      using f2 by (metis (no_types) local.ans4 local.fbox_add1 local.fbox_def)
    then show ?thesis
      by (metis (no_types) T_d fbox_simp_2 local.dka.dsg3 local.fbox_add1 mult_assoc)
  qed
  also have "... = d p  |(xx)](pxxp)  |(xx)]((pxq)  |x](qxp)  (qxp)  |x](pxq))" using "1"
    by (metis fbox_simp_2 dka.dns5 dka.dsg4 join.sup.absorb2 mult_assoc)
  also have "... = |(xx)](d p  (pxq)  |x](qxp)  (qxp)  |x](pxq))"
    using T_segerberg local.a_d_closed local.ads_d_def local.apd_d_def local.distrib_left local.fbox_def mult_assoc by auto
  also have "... = |(xx)](d p  |x] d q  |x](qxp)  (qxp)  |x](pxq))"
    by (simp add: T_p)
  also have "... = |(xx)](d p  |x] d q  |x] |x] d p  (qxp)  |x](pxq))"
    by (metis T_d T_p fbox_simp_2 fbox_add1 fbox_simp mult_assoc)
  also have "... = |(xx)](d p  |xx] d p  (qxp)  |x] d q  |x](pxq))"
  proof -
    have f1: "ad (x  ad ( |x] d p)) = |x  x] d p"
      using local.fbox_def local.fbox_mult by presburger
    have f2: "ad (d q  d (x  ad (d p))) = q  x  p"
      by (simp add: T_def local.a_de_morgan_var_4 local.fbox_def)
    have "ad q + |x] d p = ad (d q  d (x  ad (d p)))"
      by (simp add: local.a_de_morgan_var_4 local.fbox_def)
    then have "ad (x  ad ( |x] d p))  ((q  x  p)  |x] d q) = ad (x  ad ( |x] d p))  ad (x  ad (d q))  (ad q + |x] d p)"
      using f2 by (metis (no_types) local.am2 local.fbox_def mult_assoc)
    then show ?thesis
      using f1 by (simp add: T_def local.am2 local.fbox_def mult_assoc)
  qed
  also have "... = |(xx)](d p  |xx] d p  (qxp)  |x](d q  (pxq)))"
    using local.a_d_closed local.ads_d_def local.apd_d_def local.distrib_left local.fbox_def mult_assoc by auto
  also have "... = |(xx)](d p  |xx] d p)  |(xx)](qxp)  |(xx)] |x](d q  (pxq))"
    by (metis T_d fbox_simp_2 local.dka.dom_mult_closed local.fbox_add1)
  also have "... = |(xx)](d p  (qxp))  |(xx)] |x] (d q  (pxq))"
    by (metis T_d local.fbox_add1 local.fbox_simp lookahead)
  finally show ?thesis
    by (metis fbox_mult star_slide)
qed

lemma "|(xx)] d p  |x(xx)] ad p = d p  |x]((pxad p)  (ad pxp))"
  using alternation local.a_d_closed local.ads_d_def local.apd_d_def by auto

lemma "|x] d p = d p  |x](pxp)"
  by (simp add: alternation)

end

end