Theory Eta_Bisimilarity

section ‹‹η›-Bisimilarity›

theory Eta_Bisimilarity
  imports Expressiveness_Price
begin

subsection ‹Definition and Properties of ‹η›-(Bi-)Similarity›

context LTS_Tau
begin

―‹Following Def 2.1 in Divide and congruence›
definition eta_simulation :: ‹('s ⇒ 's ⇒ bool) ⇒ bool› where
  ‹eta_simulation R ≡ ∀p α p' q. R p q ⟶ p ↦ α p' ⟶
    ((α = τ ∧ R p' q) ∨ (∃q' q'' q'''. q ↠ q' ∧ q' ↦ α q'' ∧ q'' ↠ q'''  ∧ R p q' ∧ R p' q'''))›

definition eta_bisimulated :: ‹'s ⇒ 's ⇒ bool› (infix ‹~η› 40) where
  ‹p ~η q ≡ ∃R. eta_simulation R ∧ symp R ∧ R p q›

lemma eta_bisim_sim:
  shows ‹eta_simulation (~η)›
  unfolding eta_bisimulated_def eta_simulation_def by blast

lemma eta_bisim_sym:
  assumes ‹p ~η q›
  shows ‹q ~η p›
  using assms unfolding eta_bisimulated_def
  by (meson sympD)

lemma silence_retains_eta_sim:
assumes
  ‹eta_simulation R›
  ‹R p q›
  ‹p ↠ p'›
shows ‹∃q'. R p' q' ∧ q ↠ q'›
  using assms(3,2)
proof (induct arbitrary: q)
  case (refl p)
  then show ?case
    using silent_reachable.refl by blast
next
  case (step p p' p'')
  then obtain q' where ‹R p' q'› ‹q ↠ q'›
    using ‹eta_simulation R› silent_reachable.refl silent_reachable_append_τ silent_reachable_trans
    unfolding eta_simulation_def by blast
  then obtain q'' where ‹R p'' q''› ‹q' ↠ q''› using step by blast
  then show ?case
    using ‹q ↠ q'› silent_reachable_trans by blast
qed

lemma eta_bisimulated_silently_retained:
  assumes
    ‹p ~η q›
    ‹p ↠ p'›
  shows
    ‹∃q'. q ↠ q' ∧ p' ~η q'› using assms(2,1)
  using silence_retains_eta_sim unfolding eta_bisimulated_def by blast

subsection ‹Logical Characterization of ‹η›-Bisimilarity through Expressiveness Price›

lemma logic_eta_bisim_invariant:
  assumes
    ‹p0 ~η q0›
    ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
    ‹p0 ⊨SRBB φ›
  shows ‹q0 ⊨SRBB φ›
proof -
  have ‹⋀φ χ ψ.
    (∀p q. p ~η q ⟶ φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
    (∀p q. p ~η q ⟶ χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
    (∀p q. p ~η q ⟶ ψ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
  proof-
    fix φ χ ψ
    show
      ‹(∀p q. p ~η q ⟶ φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ p ⊨SRBB φ ⟶ q ⊨SRBB φ) ∧
      (∀p q. p ~η q ⟶ χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ hml_srbb_inner_models p χ ⟶ (∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ)) ∧
      (∀p q. p ~η q ⟶ ψ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ⟶ hml_srbb_conjunct_models p ψ ⟶ hml_srbb_conjunct_models q ψ)›
    proof (induct rule: hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct)
      case TT
      then show ?case by simp
    next
      case (Internal χ)
      show ?case
      proof safe
        fix p q
        assume case_assms:
          ‹p ~η q› ‹p ⊨SRBB hml_srbb.Internal χ› ‹Internal χ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
        then obtain p' where p'_spec: ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
        have ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          using case_assms(3) unfolding 𝒪_inner_def 𝒪_def by auto
        hence ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ›
          using Internal case_assms(1) p'_spec eta_bisimulated_silently_retained
          by (meson  silent_reachable_trans)
        thus ‹q ⊨SRBB hml_srbb.Internal χ› by auto
      qed
    next
      case (ImmConj I Ψ)
      then show ?case unfolding 𝒪_inner_def 𝒪_def by auto
    next
      case (Obs α φ)
      then show ?case
      proof (safe)
        fix p q
        assume case_assms:
          ‹p ~η q›
          ‹Obs α φ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          ‹hml_srbb_inner_models p (hml_srbb_inner.Obs α φ)›
        hence ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› unfolding 𝒪_inner_def 𝒪_def by auto
        hence no_imm_conj: ‹∄I Ψ. φ = ImmConj I Ψ ∧ I ≠ {}› unfolding 𝒪_def by force
        have back_step: ‹∀p0 p1. p1 ⊨SRBB φ ⟶ p0 ↠ p1 ⟶ p0 ⊨SRBB φ›
        proof (cases φ)
          case TT
          then show ?thesis by auto
        next
          case (Internal _)
          then show ?thesis
            using silent_reachable_trans by auto
        next
          case (ImmConj _ _)
          then show ?thesis using no_imm_conj by auto
        qed
        from case_assms obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
        then obtain q' q'' q''' where ‹q ↠ q'› ‹q' ↦a α q''› ‹q'' ↠ q'''›  ‹p' ~η q'''›
          using ‹p ~η q› eta_bisim_sim unfolding eta_simulation_def
          using silent_reachable.refl by blast
        hence ‹q''' ⊨SRBB φ› using ‹p' ⊨SRBB φ› Obs ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› by blast
        hence ‹hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
          using ‹q' ↦a α q''› ‹q'' ↠ q'''› back_step by auto
        thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Obs α φ)›
          using ‹q ↠ q'› by blast
      qed
    next
      case (Conj I Ψ)
      show ?case
      proof safe
        fix p q
        assume case_assms:
          ‹p ~η q›
          ‹Conj I Ψ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          ‹hml_srbb_inner_models p (Conj I Ψ)›
        hence conj_price: ‹∀i∈I. Ψ i ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          unfolding 𝒪_conjunct_def 𝒪_inner_def
          by (simp, metis SUP_bot_conv(1) le_zero_eq sup_bot_left sup_ge1)
        from case_assms have ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› by auto
        hence ‹∀i∈I. hml_srbb_conjunct_models q (Ψ i)›
          using Conj ‹p ~η q› conj_price by blast
        hence ‹hml_srbb_inner_models q (hml_srbb_inner.Conj I Ψ)› by simp
        thus ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (hml_srbb_inner.Conj I Ψ)›
          using silent_reachable.refl by blast
      qed
    next
      case (StableConj I Ψ)
      thus ?case unfolding 𝒪_inner_def 𝒪_def by auto
    next
      case (BranchConj α φ I Ψ)
      show ?case
      proof safe
        fix p q
        assume case_assms:
          ‹p ~η q›
          ‹BranchConj α φ I Ψ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          ‹hml_srbb_inner_models p (BranchConj α φ I Ψ)›
        hence ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› unfolding 𝒪_inner_def 𝒪_def
          by (simp, metis le_zero_eq sup_ge1)
        hence no_imm_conj: ‹∄I Ψ. φ = ImmConj I Ψ ∧ I ≠ {}› unfolding 𝒪_def by force
        have back_step: ‹∀p0 p1. p1 ⊨SRBB φ ⟶ p0 ↠ p1 ⟶ p0 ⊨SRBB φ›
        proof (cases φ)
          case TT
          then show ?thesis by auto
        next
          case (Internal _)
          then show ?thesis
            using silent_reachable_trans by auto
        next
          case (ImmConj _ _)
          then show ?thesis using no_imm_conj by auto
        qed
        from case_assms have conj_price: ‹∀i∈I. Ψ i ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          unfolding 𝒪_conjunct_def 𝒪_inner_def
          by (simp, metis SUP_bot_conv(1) le_zero_eq sup_bot_left sup_ge1)
        from case_assms have ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)›
              ‹hml_srbb_inner_models p (Obs α φ)›
          using branching_conj_parts branching_conj_obs by blast+
        then obtain p' where ‹p ↦a α p'› ‹p' ⊨SRBB φ› by auto
        then obtain q' q'' q''' where q'_q''_spec:
          ‹q ↠ q'› ‹q' ↦a α q''› ‹q'' ↠ q'''›
          ‹p ~η q'› ‹p' ~η q'''›
          using eta_bisim_sim ‹p ~η q› silent_reachable.refl
          unfolding eta_simulation_def by blast
        hence ‹q''' ⊨SRBB φ›
          using BranchConj.hyps ‹p' ⊨SRBB φ› ‹φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› by auto
        hence ‹q'' ⊨SRBB φ› using back_step q'_q''_spec by blast
        hence ‹hml_srbb_inner_models q' (Obs α φ)› using q'_q''_spec by auto
        moreover have ‹∀i∈I. hml_srbb_conjunct_models q' (Ψ i)›
          using BranchConj.hyps ‹∀i∈I. hml_srbb_conjunct_models p (Ψ i)› q'_q''_spec conj_price
          by blast
        ultimately show ‹∃q'. q ↠ q' ∧ hml_srbb_inner_models q' (BranchConj α φ I Ψ)›
          using ‹q ↠ q'› by auto
      qed
    next
      case (Pos χ)
      show ?case
      proof safe
        fix p q
        assume case_assms:
          ‹p ~η q›
          ‹Pos χ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          ‹hml_srbb_conjunct_models p (Pos χ)›
        hence ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          unfolding 𝒪_inner_def 𝒪_conjunct_def by simp
        from case_assms obtain p' where ‹p ↠ p'› ‹hml_srbb_inner_models p' χ› by auto
        then obtain q' where ‹q ↠ q'› ‹hml_srbb_inner_models q' χ›
          using Pos ‹p ~η q› ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          by (meson eta_bisimulated_silently_retained silent_reachable_trans)
        thus ‹hml_srbb_conjunct_models q (Pos χ)› by auto
      qed
    next
      case (Neg χ)
      show ?case
      proof safe
        fix p q
        assume case_assms:
          ‹p ~η q›
          ‹Neg χ ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          ‹hml_srbb_conjunct_models p (Neg χ)›
        hence ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
          unfolding 𝒪_inner_def 𝒪_conjunct_def by simp
        from case_assms have ‹∀p'. p ↠ p' ⟶ ¬hml_srbb_inner_models p' χ› by simp
        moreover have
          ‹(∃q'. q ↠ q' ∧ hml_srbb_inner_models q' χ) ⟶ (∃p'. p ↠ p' ∧ hml_srbb_inner_models p' χ)›
          using Neg eta_bisim_sym[OF ‹p ~η q›] eta_bisimulated_silently_retained
            silent_reachable_trans ‹χ ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)› by blast
        ultimately have ‹∀q'. q ↠ q' ⟶ ¬hml_srbb_inner_models q' χ› by blast
        thus ‹hml_srbb_conjunct_models q (Neg χ)› by simp
      qed
    qed
  qed
  thus ?thesis using assms by blast
qed

lemma modal_eta_sim_eq: ‹eta_simulation (equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)))›
proof -
  have ‹∄p α p' q. (equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞))) p q ∧ p ↦ α p' ∧
      (α ≠ τ ∨ ¬(equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞))) p' q) ∧
      (∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q''' ⟶
    ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p q' ∨ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p' q''')›
  proof clarify
    fix p α p' q
    define Qα where ‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ∧ (distinguishes φ p q' ∨ distinguishes φ q' p))}›
    assume contradiction:
      ‹equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p q› ‹p ↦ α p'›
      ‹∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q''' ⟶
      ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p q' ∨ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p' q'''›
      ‹α ≠ τ ∨ ¬ equivalent (𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)) p' q›
    hence distinctions: ‹∀q'. q ↠ q' ⟶
      (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p) ∨
      (∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p' q''' ∨ distinguishes φ q''' p'))›
      unfolding equivalent_no_distinction
      by (metis silent_reachable.cases silent_reachable.refl)
    hence ‹∀q'' q''' . ∀q'∈Qα.
        q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p' q''' ∨ distinguishes φ q''' p')›
      unfolding Qα_def using silent_reachable.refl by fastforce
    hence ‹∀q'' q'''. q'' ↠ q''' ⟶ (∃q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ∧ (distinguishes φ p q' ∨ distinguishes φ q' p)) ∧ q' ↦a α q'')
        ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p' q''' ∨ distinguishes φ q''' p')›
      unfolding Qα_def by blast
    hence ‹∀q'''. (∃q' q''. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ∧ (distinguishes φ p q' ∨ distinguishes φ q' p)) ∧ q' ↦a α q'' ∧  q'' ↠ q''')
        ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p' q''' ∨ distinguishes φ q''' p')›
      by blast
    then obtain Φα where Φα_def:
      ‹∀q'''. (∃q' q''. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ∧ (distinguishes φ p q' ∨ distinguishes φ q' p)) ∧ q' ↦a α q'' ∧ q'' ↠ q''')
        ⟶ (Φα q''') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ∧ (distinguishes (Φα q''') p' q''' ∨ distinguishes (Φα q''') q''' p')› by metis
    hence distinctions_α: ‹∀q'∈Qα. ∀q'' q'''.
        q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ distinguishes (Φα q''') p' q''' ∨ distinguishes (Φα q''') q''' p'›
      unfolding Qα_def by blast
    from distinctions obtain Φη where
      ‹∀q'. q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)}
        ⟶ (distinguishes (Φη q') p q' ∨ distinguishes (Φη q') q' p) ∧ (Φη q') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      unfolding mem_Collect_eq by moura
    hence
      ‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)}.
        (distinguishes (Φη q') p q' ∨ distinguishes (Φη q') q' p)›
      ‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)}.
         (Φη q') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      by blast+
    from distinction_conjunctification_two_way[OF this(1)] distinction_conjunctification_two_way_price[OF this]
      have ‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)}.
        hml_srbb_conj.distinguishes ((if distinguishes (Φη q') p q' then conjunctify_distinctions else conjunctify_distinctions_dual) Φη p q') p q' ∧
         (if distinguishes (Φη q') p q' then conjunctify_distinctions else conjunctify_distinctions_dual) Φη p q' ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
        by blast
    then obtain Ψη where distinctions_η:
      ‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)}.
        hml_srbb_conj.distinguishes (Ψη q') p q' ∧ Ψη q' ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      by auto
    have ‹p ↦a α p'› using ‹p ↦ α p'› by auto
    from distinction_combination_eta_two_way[OF this, of q Φα] distinctions_α have obs_dist:
      ‹∀q'∈Qα.
        hml_srbb_inner.distinguishes (Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
        (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))) p q'›
      unfolding Qα_def by fastforce
    have ‹Qα ≠ {}›
      using Qα_def contradiction(1) silent_reachable.refl by fastforce
    hence conjunct_prices: ‹∀q'''∈{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
          ((if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p' q''') ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      using distinction_conjunctification_two_way_price[of ‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}›]
      using Qα_def Φα_def by auto
    have ‹(Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
          (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
    proof (cases ‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} = {}›)
      case True
      then show ?thesis
        unfolding 𝒪_inner_def 𝒪_conjunct_def
        by (auto simp add: True bot_enat_def)
    next
      case False
      then show ?thesis
        using conjunct_prices
        unfolding 𝒪_inner_def 𝒪_conjunct_def by force
    qed
    hence obs_price: ‹(Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
         (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      using distinction_conjunctification_price distinctions_α unfolding 𝒪_inner_def 𝒪_def by simp
    from obs_dist distinctions_η have
      ‹hml_srbb_inner_models p (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)›
      using ‹Qα ≠ {}› silent_reachable.refl
      unfolding hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_def
      by (smt (verit) Qα_def empty_Collect_eq hml_srbb_inner_models.simps(1,4) mem_Collect_eq)
    moreover have ‹∀q'. q ↠ q' ⟶ ¬ hml_srbb_inner_models q'
        (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)›
    proof safe
      fix q'
      assume contradiction: ‹q ↠ q'›
        ‹hml_srbb_inner_models q' (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)›
      thus ‹False›
        using obs_dist distinctions_η  branching_conj_obs branching_conj_parts
        unfolding distinguishes_def hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_def Qα_def
        by blast
    qed
    moreover have branch_price: ‹(BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)
      ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      using distinctions_η obs_price
      unfolding Qα_def 𝒪_inner_def 𝒪_def 𝒪_conjunct_def Φα_def
      by (simp, metis (mono_tags, lifting) SUP_bot_conv(2) bot_enat_def sup_bot_left)
    ultimately have ‹distinguishes (Internal (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη)) p q›
      unfolding distinguishes_def Qα_def
      using silent_reachable.refl hml_srbb_models.simps(2) by blast
    moreover have ‹(Internal (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (λq'''. (if distinguishes (Φα q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φα p'
                   q''')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞). distinguishes φ p q' ∨ distinguishes φ q' p)} Ψη))
      ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
      using branch_price
      unfolding Qα_def 𝒪_def 𝒪_conjunct_def
      by (metis (no_types, lifting) 𝒪_inner_def expr_internal_eq mem_Collect_eq)
    ultimately show False using contradiction(1) equivalent_no_distinction by blast
  qed
  thus ?thesis
    unfolding eta_simulation_def by blast
qed

theorem ‹(p ~η q) = (p ∼ (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) q)›
  using modal_eta_sim_eq logic_eta_bisim_invariant sympD equivalent_no_distinction
  unfolding eta_bisimulated_def expr_equiv_def distinguishes_def
  by (smt (verit, best) equivalent_equiv equivpE)

―‹This proof essentially is a simpler version of the proof for the equivalence›
lemma modal_eta_sim: ‹eta_simulation (preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)))›
proof -
  have ‹∄p α p' q. (preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0))) p q ∧ p ↦ α p' ∧
      (α ≠ τ ∨ ¬(preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0))) p' q) ∧
      (∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q''' ⟶
    ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p q' ∨ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p' q''')›
  proof clarify
    have less_obs: ‹modal_depth (E ∞ ∞ ∞ 0 0 ∞ 0 0) ≤ pos_conjuncts (E ∞ ∞ ∞ 0 0 ∞ 0 0)› by simp
    fix p α p' q
    define Qα where ‹Qα ≡ {q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q')}›
    assume contradiction:
      ‹preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p q› ‹p ↦ α p'›
      ‹∀q' q'' q'''. q ↠ q' ⟶ q' ↦ α q'' ⟶ q'' ↠ q''' ⟶
      ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p q' ∨ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p' q'''›
      ‹α ≠ τ ∨ ¬ preordered (𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)) p' q›
    hence distinctions: ‹∀q'. q ↠ q' ⟶
      (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q') ∨
      (∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q'''))›
      unfolding preordered_no_distinction
      by (metis silent_reachable.cases silent_reachable.refl)
    hence ‹∀q'' q''' . ∀q'∈Qα.
        q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q''')›
      unfolding Qα_def using silent_reachable.refl by fastforce
    hence ‹∀q'' q'''. q'' ↠ q''' ⟶ (∃q'. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q') ∧ q' ↦a α q'')
        ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q''')›
      unfolding Qα_def by blast
    hence ‹∀q'''. (∃q' q''. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q') ∧ q' ↦a α q'' ∧  q'' ↠ q''')
        ⟶ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p' q''')›
      by blast
    then obtain Φα where Φα_def:
      ‹∀q'''. (∃q' q''. q ↠ q' ∧ (∄φ. φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q') ∧ q' ↦a α q'' ∧ q'' ↠ q''')
        ⟶ (Φα q''') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes (Φα q''') p' q'''› by metis
    hence distinctions_α: ‹∀q'∈Qα. ∀q'' q'''.
        q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ distinguishes (Φα q''') p' q'''›
      unfolding Qα_def by blast
    from distinctions obtain Φη where
      ‹∀q'. q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')}
        ⟶ distinguishes (Φη q') p q' ∧ (Φη q') ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)› unfolding mem_Collect_eq by moura
    then obtain Ψη where distinctions_η:
      ‹∀q'∈{q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')}.
        hml_srbb_conj.distinguishes (Ψη q') p q' ∧ (Ψη q') ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
      using less_obs  distinction_conjunctification distinction_conjunctification_price
      by (smt (verit, del_insts))
    have ‹p ↦a α p'› using ‹p ↦ α p'› by auto
    from distinction_combination_eta[OF this] distinctions_α have obs_dist:
      ‹∀q'∈Qα.
        hml_srbb_inner.distinguishes (Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                                                     (conjunctify_distinctions Φα p')))) p q'›
      unfolding Qα_def by blast
    have ‹Qα ≠ {}›
      using Qα_def contradiction(1) silent_reachable.refl by fastforce
    hence conjunct_prices: ‹∀q'''∈{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
          (conjunctify_distinctions Φα p' q''') ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
      using distinction_conjunctification_price[of ‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}›]
      using Qα_def Φα_def by auto
    have ‹(Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
          (conjunctify_distinctions Φα p')) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
    proof (cases ‹{q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} = {}›)
      case True
      then show ?thesis
        unfolding 𝒪_inner_def 𝒪_conjunct_def
        by (auto simp add: True bot_enat_def)
    next
      case False
      then show ?thesis
        using conjunct_prices
        unfolding 𝒪_inner_def 𝒪_conjunct_def by force
    qed
    hence obs_price: ‹(Obs α (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
         (conjunctify_distinctions Φα p')))) ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
      using distinction_conjunctification_price distinctions_α unfolding 𝒪_inner_def 𝒪_def by simp
    from obs_dist distinctions_η have
      ‹hml_srbb_inner_models p (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (conjunctify_distinctions Φα p')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)›
      using contradiction(1) silent_reachable.refl
      unfolding Qα_def by force
    moreover have ‹∀q'. q ↠ q' ⟶ ¬ hml_srbb_inner_models q'
        (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (conjunctify_distinctions Φα p')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)›
    proof safe
      fix q'
      assume contradiction: ‹q ↠ q'›
        ‹hml_srbb_inner_models q' (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (conjunctify_distinctions Φα p')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)›
      thus ‹False›
        using obs_dist distinctions_η
        unfolding distinguishes_def hml_srbb_conj.distinguishes_def hml_srbb_inner.distinguishes_def Qα_def
        by (auto) blast+
    qed
    moreover have branch_price: ‹(BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (conjunctify_distinctions Φα p')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)
      ∈ 𝒪_inner (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
      using distinctions_η obs_price
      unfolding Qα_def 𝒪_inner_def 𝒪_def 𝒪_conjunct_def Φα_def
      by (simp, metis (mono_tags, lifting) SUP_bot_conv(2) bot_enat_def sup_bot_left)
    ultimately have ‹distinguishes (Internal (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (conjunctify_distinctions Φα p')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη)) p q›
      unfolding distinguishes_def Qα_def
      using silent_reachable.refl hml_srbb_models.simps(2) by blast
    moreover have ‹(Internal (BranchConj α
          (Internal (Conj {q'''. ∃q'∈Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
                   (conjunctify_distinctions Φα p')))
          {q'. q ↠ q' ∧ (∃φ∈𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0). distinguishes φ p q')} Ψη))
      ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0)›
      using branch_price
      unfolding Qα_def 𝒪_def 𝒪_conjunct_def
      by (metis (no_types, lifting) 𝒪_inner_def expr_internal_eq mem_Collect_eq)
    ultimately show False using contradiction(1) preordered_no_distinction by blast
  qed
  thus ?thesis
    unfolding eta_simulation_def by blast
qed

theorem ‹(p ≼ (E ∞ ∞ ∞ 0 0 ∞ 0 0) q) ⟹ (∃R. eta_simulation R ∧ R p q)›
  using modal_eta_sim unfolding expr_preord_def
  by auto

end

end