Theory Expressiveness_Price

text ‹\newpage›
section ‹Expressiveness Price Function \label{sect:ExpressivenessMeasure}›

theory Expressiveness_Price
  imports HML_SRBB Energy
begin

text ‹
The expressiveness price function assigns a price - an eight-dimensional vector - to a HML$_\text{SRBB}$ formula.
This price is supposed to capture the expressiveness power needed to describe a certain property and
will later be used to select subsets of specific expressiveness power associated with the behavioural equivalence characterized by that subset of the HML$_\text{SRBB}$ sublanguage.
\\\\
The expressiveness price function may be defined as a single function:
\begin{align*}
  expr(\top) := expr^\varepsilon(\top) :=& 0 \\
  expr(\langle\varepsilon\rangle\chi) :=& expr^\varepsilon(\chi) \\
  expr(\bigwedge\Psi) :=& \hat{e}_5 + expr^\varepsilon(\bigwedge\Psi) \\
  expr^\varepsilon((\alpha)\varphi) :=& \hat{e}_1 + expr(\varphi) \\
  expr^\varepsilon(\bigwedge(\{(\alpha)\varphi\} \cup \Psi)) :=& \hat{e}_2 + expr^\varepsilon(\bigwedge(\{\langle\varepsilon\rangle(\alpha)\varphi\} \cup \Psi \setminus \{(\alpha)\varphi\})) \\
  expr^\varepsilon(\bigwedge\Psi) :=& \sup \{expr^\wedge(\psi) | \psi \in \Psi\} +
    \begin{cases}
      \hat{e}_4 & \text{if} \neg\langle\tau\rangle\top \in \Psi \\
      \hat{e}_3 & \text{otherwise}
    \end{cases} \\
  expr^\wedge(\neg\langle\tau\rangle\top) :=&  0 \\
  expr^\wedge(\neg\varphi) :=& \sup \{\hat{e}_8 + expr(\varphi), (0,0,0,0,0,0,expr_1(\varphi),0)\} \\
  expr^\wedge(\varphi) :=& \sup \{expr(\varphi), (0,0,0,0,0,expr_1(\varphi),0,0)\}
\end{align*}

The eight dimensions are intended to measure the following properties of formulas:
\begin{enumerate}
  \item Modal depth (of observations $\langle\alpha\rangle$, $(\alpha)$),
  \item Depth of branching conjunctions (with one observation clause not starting with $\langle\varepsilon\rangle$),
  \item Depth of stable conjunctions (that do enforce stability by a $\neg\langle\tau\rangle\top$-conjunct),
  \item Depth of unstable conjunctions (that do not enforce stability by a $\neg\langle\tau\rangle\top$-conjunct),
  \item Depth of immediate conjunctions (that are not preceded by $\langle\varepsilon\rangle$),
  \item Maximal modal depth of positive clauses in conjunctions,
  \item Maximal modal depth of negative clauses in conjunctions,
  \item Depth of negations
\end{enumerate}

Instead of defining the expressiveness price function in one go, we define eight functions (one for each dimension)
and then use them in combination to build the the result vector.\\

Note that since all these functions stem from the above singular function, they all look very similar,
but differ mostly in where the $1+$ is placed.
›

subsection ‹Modal Depth›

text ‹
The (maximal) modal depth (of observations $\langle\alpha\rangle$, $(\alpha)$) is increased on each:
\begin{itemize}
  \item ‹Obs›
  \item ‹BranchConj›
\end{itemize}
›

primrec
      modal_depth_srbb :: ‹('act, 'i) hml_srbb ⇒ enat›
  and modal_depth_srbb_inner :: ‹('act, 'i) hml_srbb_inner ⇒ enat›
  and modal_depth_srbb_conjunct :: ‹('act, 'i) hml_srbb_conjunct ⇒ enat› where
 ‹modal_depth_srbb TT = 0› |
 ‹modal_depth_srbb (Internal χ) = modal_depth_srbb_inner χ› |
 ‹modal_depth_srbb (ImmConj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)› |

 ‹modal_depth_srbb_inner (Obs α φ) = 1 + modal_depth_srbb φ› |
 ‹modal_depth_srbb_inner (Conj I ψs) =
    Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)› |
 ‹modal_depth_srbb_inner (StableConj I ψs) =
    Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)› |
 ‹modal_depth_srbb_inner (BranchConj a φ I ψs) =
    Sup ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ ψs) ` I))› |

 ‹modal_depth_srbb_conjunct (Pos χ) = modal_depth_srbb_inner χ› |
 ‹modal_depth_srbb_conjunct (Neg χ) = modal_depth_srbb_inner χ›

lemma ‹modal_depth_srbb TT = 0›
  using Sup_enat_def by simp

lemma ‹modal_depth_srbb (Internal (Obs α (Internal (BranchConj β TT {} ψs2)))) = 2›
  using Sup_enat_def by simp

fun observe_n_alphas :: ‹'a ⇒ nat ⇒ ('a, nat) hml_srbb› where
  ‹observe_n_alphas α 0 = TT› |
  ‹observe_n_alphas α (Suc n) = Internal (Obs α (observe_n_alphas α n))›

lemma obs_n_α_depth_n: ‹modal_depth_srbb (observe_n_alphas α n) = n›
proof (induct n)
  case 0
  show ?case unfolding observe_n_alphas.simps(1) and modal_depth_srbb.simps(2)
    using zero_enat_def and Sup_enat_def by force
next
  case (Suc n)
  then show ?case
    using eSuc_enat plus_1_eSuc(1) by auto
qed

lemma sup_nats_in_enats_infinite: ‹(SUP x∈ℕ. enat x) = ∞›
  by (metis Nats_infinite Sup_enat_def enat.inject finite.emptyI finite_imageD inj_on_def)

lemma sucs_of_nats_in_enats_sup_infinite: ‹(SUP x∈ℕ. 1 + enat x) = ∞›
  using sup_nats_in_enats_infinite
  by (metis Sup.SUP_cong eSuc_Sup eSuc_infinity image_image image_is_empty plus_1_eSuc(1))

lemma ‹modal_depth_srbb (ImmConj ℕ (λn. Pos (Obs α (observe_n_alphas α n)))) = ∞›
  unfolding modal_depth_srbb.simps(3)
        and o_def
        and modal_depth_srbb_conjunct.simps(1)
        and modal_depth_srbb_inner.simps(1)
        and obs_n_α_depth_n
  by (metis sucs_of_nats_in_enats_sup_infinite)


subsection ‹Depth of Branching Conjunctions›

text ‹
The depth of branching conjunctions (with one observation clause not starting with $\langle\varepsilon\rangle$) is increased on each:
\begin{itemize}
  \item ‹BranchConj› if there are other conjuncts besides the branching conjunct
\end{itemize}

Note that if the ‹BranchConj› is empty (has no other conjuncts),
then it is treated like a simple ‹Obs›.
›

primrec
      branching_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and branch_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and branch_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹branching_conjunction_depth TT = 0› |
  ‹branching_conjunction_depth (Internal χ) = branch_conj_depth_inner χ› |
  ‹branching_conjunction_depth (ImmConj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)› |

  ‹branch_conj_depth_inner (Obs _ φ) = branching_conjunction_depth φ› |
  ‹branch_conj_depth_inner (Conj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹branch_conj_depth_inner (StableConj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹branch_conj_depth_inner (BranchConj _ φ I ψs) =
     1 + Sup ({branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹branch_conj_depth_conjunct (Pos χ) = branch_conj_depth_inner χ› |
  ‹branch_conj_depth_conjunct (Neg χ) = branch_conj_depth_inner χ›

subsection ‹Depth of Stable Conjunctions›

text ‹
The depth of stable conjunctions (that do enforce stability by a $\neg\langle\tau\rangle\top$-conjunct)
is increased on each:
\begin{itemize}
  \item ‹StableConj›
\end{itemize}

Note that if the ‹StableConj› is empty (has no other conjuncts),
it is still counted.
›

primrec
      stable_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and st_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and st_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹stable_conjunction_depth TT = 0› |
  ‹stable_conjunction_depth (Internal χ) = st_conj_depth_inner χ› |
  ‹stable_conjunction_depth (ImmConj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)› |

  ‹st_conj_depth_inner (Obs _ φ) = stable_conjunction_depth φ› |
  ‹st_conj_depth_inner (Conj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹st_conj_depth_inner (StableConj I ψs) = 1 + Sup ((st_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹st_conj_depth_inner (BranchConj _ φ I ψs) = Sup ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹st_conj_depth_conjunct (Pos χ) = st_conj_depth_inner χ› |
  ‹st_conj_depth_conjunct (Neg χ) = st_conj_depth_inner χ›

subsection ‹Depth of Instable Conjunctions›

text ‹
The depth of unstable conjunctions (that do not enforce stability by a $\neg\langle\tau\rangle\top$-conjunct)
is increased on each:
\begin{itemize}
  \item ‹ImmConj› if there are conjuncts (i.e. $\bigwedge\{\}$ is not counted)
  \item ‹Conj› if there are conjuncts, (i.e. the conjunction is not empty)
  \item ‹BranchConj› if there are other conjuncts besides the branching conjunct
\end{itemize}

Note that if the ‹BranchConj› is empty (has no other conjuncts),
then it is treated like a simple ‹Obs›.
›

primrec
      unstable_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and inst_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and inst_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹unstable_conjunction_depth TT = 0› |
  ‹unstable_conjunction_depth (Internal χ) = inst_conj_depth_inner χ› |
  ‹unstable_conjunction_depth (ImmConj I ψs) =
    (if I = {}
     then 0
     else 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹inst_conj_depth_inner (Obs _ φ) = unstable_conjunction_depth φ› |
  ‹inst_conj_depth_inner (Conj I ψs) =
    (if I = {}
     then 0
     else 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))› |
  ‹inst_conj_depth_inner (StableConj I ψs) = Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹inst_conj_depth_inner (BranchConj _ φ I ψs) =
    1 + Sup ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹inst_conj_depth_conjunct (Pos χ) = inst_conj_depth_inner χ› |
  ‹inst_conj_depth_conjunct (Neg χ) = inst_conj_depth_inner χ›

subsection ‹Depth of Immediate Conjunctions›

text ‹
The depth of immediate conjunctions (that are not preceded by $\langle\varepsilon\rangle$)
is increased on each:
\begin{itemize}
  \item ‹ImmConj› if there are conjuncts (i.e. $\bigwedge\{\}$ is not counted)
\end{itemize}
›

primrec
      immediate_conjunction_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and imm_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and imm_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹immediate_conjunction_depth TT = 0› |
  ‹immediate_conjunction_depth (Internal χ) = imm_conj_depth_inner χ› |
  ‹immediate_conjunction_depth (ImmConj I ψs) =
    (if I = {}
     then 0
     else 1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹imm_conj_depth_inner (Obs _ φ) = immediate_conjunction_depth φ› |
  ‹imm_conj_depth_inner (Conj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹imm_conj_depth_inner (StableConj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹imm_conj_depth_inner (BranchConj _ φ I ψs) = Sup ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹imm_conj_depth_conjunct (Pos χ) = imm_conj_depth_inner χ› |
  ‹imm_conj_depth_conjunct (Neg χ) = imm_conj_depth_inner χ›


subsection ‹Maximal Modal Depth of Positive Clauses in Conjunctions›

text ‹
Now, we take a look at the maximal modal depth of positive clauses in conjunctions.

This counter calculates the modal depth for every positive clause in a conjunction (‹Pos χ›).
›

primrec
      max_positive_conjunct_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and max_pos_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and max_pos_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹max_positive_conjunct_depth TT = 0› |
  ‹max_positive_conjunct_depth (Internal χ) = max_pos_conj_depth_inner χ› |
  ‹max_positive_conjunct_depth (ImmConj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)› |

  ‹max_pos_conj_depth_inner (Obs _ φ) = max_positive_conjunct_depth φ› |
  ‹max_pos_conj_depth_inner (Conj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹max_pos_conj_depth_inner (StableConj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹max_pos_conj_depth_inner (BranchConj _ φ I ψs) = Sup ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ} ∪ ((max_pos_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹max_pos_conj_depth_conjunct (Pos χ) = modal_depth_srbb_inner χ› |
  ‹max_pos_conj_depth_conjunct (Neg χ) = max_pos_conj_depth_inner χ›

lemma modal_depth_dominates_pos_conjuncts:
  fixes
    φ::‹('a, 's) hml_srbb› and
    χ::‹('a, 's) hml_srbb_inner› and
    ψ::‹('a, 's) hml_srbb_conjunct›
  shows
    ‹(max_positive_conjunct_depth φ ≤ modal_depth_srbb φ)
    ∧ (max_pos_conj_depth_inner χ ≤ modal_depth_srbb_inner χ)
    ∧ (max_pos_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ)›
  using hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct[of
        ‹λφ::('a, 's) hml_srbb. max_positive_conjunct_depth φ ≤ modal_depth_srbb φ›
        ‹λχ. max_pos_conj_depth_inner χ ≤ modal_depth_srbb_inner χ›
        ‹λψ. max_pos_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ›]
  by (auto simp add: SUP_mono' add_increasing sup.coboundedI1 sup.coboundedI2)

subsection ‹Maximal Modal Depth of Negative Clauses in Conjunctions›

text ‹
We take a look at the maximal modal depth of negative clauses in conjunctions.

This counter calculates the modal depth for every negative clause in a conjunction (‹Neg χ›).
›

primrec
      max_negative_conjunct_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and max_neg_conj_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and max_neg_conj_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹max_negative_conjunct_depth TT = 0› |
  ‹max_negative_conjunct_depth (Internal χ) = max_neg_conj_depth_inner χ› |
  ‹max_negative_conjunct_depth (ImmConj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)› |

  ‹max_neg_conj_depth_inner (Obs _ φ) = max_negative_conjunct_depth φ› |
  ‹max_neg_conj_depth_inner (Conj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹max_neg_conj_depth_inner (StableConj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)› |
  ‹max_neg_conj_depth_inner (BranchConj _ φ I ψs) = Sup ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ ψs) ` I))› |

  ‹max_neg_conj_depth_conjunct (Pos χ) = max_neg_conj_depth_inner χ› |
  ‹max_neg_conj_depth_conjunct (Neg χ) = modal_depth_srbb_inner χ›



lemma modal_depth_dominates_neg_conjuncts:
  fixes
    φ::‹('a, 's) hml_srbb› and
    χ::‹('a, 's) hml_srbb_inner› and
    ψ::‹('a, 's) hml_srbb_conjunct›
  shows
    ‹(max_negative_conjunct_depth φ ≤ modal_depth_srbb φ)
    ∧ (max_neg_conj_depth_inner χ ≤ modal_depth_srbb_inner χ)
    ∧ (max_neg_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ)›
  using hml_srbb_hml_srbb_inner_hml_srbb_conjunct.induct[of
        ‹λφ::('a, 's) hml_srbb. max_negative_conjunct_depth φ ≤ modal_depth_srbb φ›
        ‹λχ. max_neg_conj_depth_inner χ ≤ modal_depth_srbb_inner χ›
        ‹λψ. max_neg_conj_depth_conjunct ψ ≤ modal_depth_srbb_conjunct ψ›]
  by (auto simp add: SUP_mono' add_increasing sup.coboundedI1 sup.coboundedI2)

subsection ‹Depth of Negations›

text ‹
The depth of negations (occurrences of ‹Neg χ› on a path of the syntax tree) is increased on each:
\begin{itemize}
  \item ‹Neg χ›
\end{itemize}
›

primrec
      negation_depth :: ‹('a, 's) hml_srbb ⇒ enat›
  and neg_depth_inner :: ‹('a, 's) hml_srbb_inner ⇒ enat›
  and neg_depth_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ enat› where
  ‹negation_depth TT = 0› |
  ‹negation_depth (Internal χ) = neg_depth_inner χ› |
  ‹negation_depth (ImmConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)› |

  ‹neg_depth_inner (Obs _ φ) = negation_depth φ› |
  ‹neg_depth_inner (Conj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)› |
  ‹neg_depth_inner (StableConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)› |
  ‹neg_depth_inner (BranchConj _ φ I ψs) = Sup ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ ψs) ` I))› |

  ‹neg_depth_conjunct (Pos χ) = neg_depth_inner χ› |
  ‹neg_depth_conjunct (Neg χ) = 1 + neg_depth_inner χ›

subsection ‹Expressiveness Price Function›

text ‹The @{term ‹expressiveness_price›} function combines the eight functions into one.›

fun expressiveness_price :: ‹('a, 's) hml_srbb ⇒ energy› where
  ‹expressiveness_price φ = E (modal_depth_srbb            φ)
                              (branching_conjunction_depth φ)
                              (unstable_conjunction_depth  φ)
                              (stable_conjunction_depth    φ)
                              (immediate_conjunction_depth φ)
                              (max_positive_conjunct_depth φ)
                              (max_negative_conjunct_depth φ)
                              (negation_depth              φ)›

text ‹Here, we can see the decomposed price of an immediate conjunction:›
lemma expressiveness_price_ImmConj_def:
  shows ‹expressiveness_price (ImmConj I ψs) = E
    (Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I))
    (Sup ((branch_conj_depth_conjunct ∘ ψs) ` I))
    (if I = {} then 0 else 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((st_conj_depth_conjunct ∘ ψs) ` I))
    (if I = {} then 0 else 1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((neg_depth_conjunct ∘ ψs) ` I))› by simp

lemma expressiveness_price_ImmConj_non_empty_def:
  assumes ‹I ≠ {}›
  shows ‹expressiveness_price (ImmConj I ψs) = E
    (Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I))
    (Sup ((branch_conj_depth_conjunct ∘ ψs) ` I))
    (1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((st_conj_depth_conjunct ∘ ψs) ` I))
    (1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((neg_depth_conjunct ∘ ψs) ` I))› using assms  by simp

lemma expressiveness_price_ImmConj_empty_def:
  assumes ‹I = {}›
  shows ‹expressiveness_price (ImmConj I ψs) = E 0 0 0 0 0 0 0 0› using assms
  unfolding expressiveness_price_ImmConj_def by (simp add: bot_enat_def)

text ‹We can now define a sublanguage of Hennessy-Milner Logic @{term ‹𝒪›} by the set of formulas with prices below an energy coordinate.›
definition 𝒪 :: ‹energy ⇒ (('a, 's) hml_srbb) set› where
  ‹𝒪 energy ≡ {φ . expressiveness_price φ ≤ energy}›

lemma 𝒪_sup: ‹UNIV = 𝒪 (E ∞ ∞ ∞ ∞ ∞ ∞ ∞ ∞)› unfolding 𝒪_def by auto

text ‹Formalizing HML$_{SRBB}$ by mutually recursive data types leads to expressiveness price functions of these other types,
namely @{term ‹expr_pr_inner›} and @{term ‹expr_pr_conjunct›}, and corresponding definitions and lemmas.›

fun expr_pr_inner :: ‹('a, 's) hml_srbb_inner ⇒ energy› where
  ‹expr_pr_inner χ = E (modal_depth_srbb_inner χ)
                 (branch_conj_depth_inner χ)
                 (inst_conj_depth_inner χ)
                 (st_conj_depth_inner χ)
                 (imm_conj_depth_inner χ)
                 (max_pos_conj_depth_inner χ)
                 (max_neg_conj_depth_inner χ)
                 (neg_depth_inner χ)›

definition 𝒪_inner :: ‹energy ⇒ (('a, 's) hml_srbb_inner) set› where
  ‹𝒪_inner energy ≡ {χ . expr_pr_inner χ ≤ energy}›

fun expr_pr_conjunct :: ‹('a, 's) hml_srbb_conjunct ⇒ energy› where
  ‹expr_pr_conjunct ψ = E (modal_depth_srbb_conjunct ψ)
                 (branch_conj_depth_conjunct ψ)
                 (inst_conj_depth_conjunct ψ)
                 (st_conj_depth_conjunct ψ)
                 (imm_conj_depth_conjunct ψ)
                 (max_pos_conj_depth_conjunct ψ)
                 (max_neg_conj_depth_conjunct ψ)
                 (neg_depth_conjunct ψ)›

definition 𝒪_conjunct :: ‹energy ⇒ (('a, 's) hml_srbb_conjunct) set› where
  ‹𝒪_conjunct energy ≡ {χ . expr_pr_conjunct χ ≤ energy}›

subsection ‹Prices of Certain Formulas›

text ‹
We demonstrate the pricing mechanisms for various formulas. These proofs operate under the assumption of an expressiveness price ‹e› for a given formula ‹χ› and proceed to determine the price of a derived formula such as ‹Pos χ›.
The proofs all are of a similar nature. They decompose the expression function(s) into their constituent parts and apply their definitions to the constructed formula (‹(Pos χ)›).›

context LTS_Tau
begin

text ‹For example, here, we establish that the expressiveness price of ‹Internal χ› is equal to the expressiveness price of ‹χ›.›

lemma expr_internal_eq:
  shows ‹expressiveness_price (Internal χ) = expr_pr_inner χ›
proof-
  have expr_internal: ‹expressiveness_price (Internal χ) = E (modal_depth_srbb (Internal χ))
                              (branching_conjunction_depth (Internal χ))
                              (unstable_conjunction_depth  (Internal χ))
                              (stable_conjunction_depth    (Internal χ))
                              (immediate_conjunction_depth (Internal χ))
                              (max_positive_conjunct_depth (Internal χ))
                              (max_negative_conjunct_depth (Internal χ))
                              (negation_depth              (Internal χ))›
            using expressiveness_price.simps by blast
          have ‹modal_depth_srbb (Internal χ) = modal_depth_srbb_inner χ›
            ‹(branching_conjunction_depth (Internal χ)) = branch_conj_depth_inner χ›
            ‹(unstable_conjunction_depth  (Internal χ)) = inst_conj_depth_inner χ›
            ‹(stable_conjunction_depth    (Internal χ)) = st_conj_depth_inner χ›
            ‹(immediate_conjunction_depth (Internal χ)) = imm_conj_depth_inner χ›
            ‹max_positive_conjunct_depth (Internal χ) = max_pos_conj_depth_inner χ›
            ‹max_negative_conjunct_depth (Internal χ) = max_neg_conj_depth_inner χ›
            ‹negation_depth (Internal χ) = neg_depth_inner χ›
            by simp+
          with expr_internal show ?thesis
            by auto
        qed

text ‹If the price of a formula ‹χ› is not greater than the minimum update @{term ‹min1_6›} apllied to some energy $e$,
then ‹Pos χ› is not greater than ‹e›.›
lemma expr_pos:
  assumes ‹expr_pr_inner χ ≤ the (min1_6 e)›
  shows ‹expr_pr_conjunct (Pos χ) ≤ e›
proof-
  have expr_internal: ‹expr_pr_conjunct (Pos χ) = E (modal_depth_srbb_conjunct (Pos χ))
                              (branch_conj_depth_conjunct (Pos χ))
                              (inst_conj_depth_conjunct  (Pos χ))
                              (st_conj_depth_conjunct    (Pos χ))
                              (imm_conj_depth_conjunct (Pos χ))
                              (max_pos_conj_depth_conjunct (Pos χ))
                              (max_neg_conj_depth_conjunct (Pos χ))
                              (neg_depth_conjunct            (Pos χ))›
            using expr_pr_conjunct.simps by blast
  have pos_upd: ‹(modal_depth_srbb_conjunct (Pos χ)) = modal_depth_srbb_inner χ›
                ‹(branch_conj_depth_conjunct (Pos χ)) = branch_conj_depth_inner χ›
                ‹(inst_conj_depth_conjunct  (Pos χ)) = inst_conj_depth_inner χ›
                ‹(st_conj_depth_conjunct    (Pos χ)) = st_conj_depth_inner χ›
                ‹(imm_conj_depth_conjunct (Pos χ)) = imm_conj_depth_inner χ›
                ‹(max_pos_conj_depth_conjunct (Pos χ)) = modal_depth_srbb_inner χ›
                ‹(max_neg_conj_depth_conjunct (Pos χ)) = max_neg_conj_depth_inner χ›
                ‹(neg_depth_conjunct            (Pos χ)) = neg_depth_inner χ›
    by simp+
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    by (metis energy.exhaust_sel)
  hence ‹min1_6 e = Some (E (min e1 e6) e2 e3 e4 e5 e6 e7 e8)›
    by (simp add: min1_6_def)
  hence ‹modal_depth_srbb_inner χ ≤ (min e1 e6)›
    using assms leq_components by fastforce
  hence ‹modal_depth_srbb_inner χ ≤ e6›
    using min.boundedE by blast
  thus ‹expr_pr_conjunct (Pos χ) ≤ e›
    using expr_internal pos_upd ‹e = E e1 e2 e3 e4 e5 e6 e7 e8› assms leq_components by auto
qed

lemma expr_neg:
  assumes
    ‹expr_pr_inner χ ≤ e'›
    ‹(Option.bind ((subtract_fn 0 0 0 0 0 0 0 1) e) min1_7) = Some e'›
  shows ‹expr_pr_conjunct (Neg χ) ≤ e›
proof-
  have expr_neg: ‹expr_pr_conjunct (Neg χ) =
    E (modal_depth_srbb_conjunct (Neg χ))
      (branch_conj_depth_conjunct (Neg χ))
      (inst_conj_depth_conjunct (Neg χ))
      (st_conj_depth_conjunct (Neg χ))
      (imm_conj_depth_conjunct (Neg χ))
      (max_pos_conj_depth_conjunct (Neg χ))
      (max_neg_conj_depth_conjunct (Neg χ))
      (neg_depth_conjunct (Neg χ))›
    using expr_pr_conjunct.simps by blast
  have neg_ups:
    ‹modal_depth_srbb_conjunct (Neg χ) = modal_depth_srbb_inner χ›
    ‹(branch_conj_depth_conjunct (Neg χ)) = branch_conj_depth_inner χ›
    ‹inst_conj_depth_conjunct (Neg χ) = inst_conj_depth_inner χ›
    ‹st_conj_depth_conjunct (Neg χ) = st_conj_depth_inner χ›
    ‹imm_conj_depth_conjunct (Neg χ) = imm_conj_depth_inner χ›
    ‹max_pos_conj_depth_conjunct (Neg χ) = max_pos_conj_depth_inner χ›
    ‹max_neg_conj_depth_conjunct (Neg χ) = modal_depth_srbb_inner χ›
    ‹neg_depth_conjunct (Neg χ) = 1 + neg_depth_inner χ›
    by simp+
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    by (metis energy.exhaust_sel)
  hence is_some: ‹(subtract_fn 0 0 0 0 0 0 0 1 e = Some (E e1 e2 e3 e4 e5 e6 e7 (e8-1)))›
    using assms bind_eq_None_conv by fastforce
  hence ‹modal_depth_srbb_inner χ ≤ (min e1 e7)›
    using assms expr_pr_inner.simps leq_components min_1_7_subtr_simp e_def
    by (metis energy.sel(1) energy.sel(7) option.discI option.inject)
  moreover have ‹neg_depth_inner χ ≤ (e8-1)›
    using e_def is_some energy_minus leq_components min_1_7_simps assms
    by (smt (verit, ccfv_threshold) bind.bind_lunit energy.sel(8) expr_pr_inner.simps option.sel)
  moreover hence ‹neg_depth_conjunct (Neg χ) ≤ e8›
    using ‹neg_depth_conjunct (Neg χ) = 1 + neg_depth_inner χ›
    by (metis is_some add_diff_assoc_enat add_diff_cancel_enat e_def enat.simps(3)
        enat_defs(2) enat_diff_mono energy.sel(8) leq_components linorder_not_less
        option.distinct(1) order_le_less)
  ultimately show ‹expr_pr_conjunct (Neg χ) ≤ e›
    using expr_neg e_def is_some assms neg_ups assms leq_components min_1_7_subtr_simp
    by (metis energy.sel expr_pr_inner.simps min.bounded_iff option.distinct(1) option.inject)
qed

lemma expr_obs:
  assumes
    ‹expressiveness_price φ ≤ e'›
    ‹subtract_fn 1 0 0 0 0 0 0 0 e = Some e'›
  shows ‹expr_pr_inner (Obs α φ) ≤ e›
proof-
  have expr_pr_obs:
    ‹expr_pr_inner (Obs α φ) =
      (E (modal_depth_srbb_inner (Obs α φ))
      (branch_conj_depth_inner (Obs α φ))
      (inst_conj_depth_inner (Obs α φ))
      (st_conj_depth_inner (Obs α φ))
      (imm_conj_depth_inner (Obs α φ))
      (max_pos_conj_depth_inner (Obs α φ))
      (max_neg_conj_depth_inner (Obs α φ))
      (neg_depth_inner (Obs α φ)))›
    using expr_pr_inner.simps by blast
  have obs_upds:
    ‹modal_depth_srbb_inner (Obs α φ) = 1 + modal_depth_srbb φ›
    ‹branch_conj_depth_inner (Obs α φ) = branching_conjunction_depth φ›
    ‹inst_conj_depth_inner (Obs α φ) = unstable_conjunction_depth φ›
    ‹st_conj_depth_inner (Obs α φ) = stable_conjunction_depth φ›
    ‹imm_conj_depth_inner (Obs α φ) = immediate_conjunction_depth φ›
    ‹max_pos_conj_depth_inner (Obs α φ) = max_positive_conjunct_depth φ›
    ‹max_neg_conj_depth_inner (Obs α φ) = max_negative_conjunct_depth φ›
    ‹neg_depth_inner (Obs α φ) = negation_depth φ›
    by simp_all
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    by (metis energy.exhaust_sel)
  then have is_some: ‹(subtract_fn 1 0 0 0 0 0 0 0 e = Some (E (e1-1) e2 e3 e4 e5 e6 e7 e8))›
    using energy_minus idiff_0_right assms
    by (metis option.discI)
  hence ‹modal_depth_srbb φ ≤ (e1 - 1)›
    using assms
    by (auto simp add: e_def)
  hence ‹modal_depth_srbb_inner (Obs α φ) ≤ e1›
    using obs_upds is_some
    unfolding leq_components e_def
    by (metis add_diff_assoc_enat add_diff_cancel_enat antisym enat.simps(3) enat_defs(2)
        enat_diff_mono energy.sel(1) linorder_linear option.distinct(1))
  then show ?thesis
    using is_some assms
    unfolding  e_def leq_components
    by auto
qed

lemma expr_st_conj:
  assumes
    ‹subtract_fn  0 0 0 1 0 0 0 0 e = Some e'›
    ‹I ≠ {}›
    ‹∀q ∈ I. expr_pr_conjunct (ψs q) ≤ e'›
  shows
    ‹expr_pr_inner (StableConj I ψs) ≤ e›
proof -
  have st_conj_upds:
    ‹modal_depth_srbb_inner (StableConj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
    ‹branch_conj_depth_inner (StableConj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
    ‹inst_conj_depth_inner (StableConj I ψs) = Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
    ‹st_conj_depth_inner (StableConj I ψs) = 1 + Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
    ‹imm_conj_depth_inner (StableConj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_pos_conj_depth_inner (StableConj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_neg_conj_depth_inner (StableConj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)›
    ‹neg_depth_inner (StableConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
    by force+
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    using energy.exhaust_sel by blast
  hence is_some: ‹subtract_fn  0 0 0 1 0 0 0 0 e = Some (E e1 e2 e3 (e4-1) e5 e6 e7 e8)›
    using assms minus_energy_def
    by (smt (verit, del_insts) energy_minus idiff_0_right option.distinct(1))
  hence
    ‹∀i ∈ I. modal_depth_srbb_conjunct (ψs i) ≤ e1›
    ‹∀i ∈ I. branch_conj_depth_conjunct (ψs i) ≤ e2›
    ‹∀i ∈ I. inst_conj_depth_conjunct (ψs i) ≤ e3›
    ‹∀i ∈ I. st_conj_depth_conjunct (ψs i) ≤ (e4 - 1)›
    ‹∀i ∈ I. imm_conj_depth_conjunct (ψs i) ≤ e5›
    ‹∀i ∈ I. max_pos_conj_depth_conjunct (ψs i) ≤ e6›
    ‹∀i ∈ I. max_neg_conj_depth_conjunct (ψs i) ≤ e7›
    ‹∀i ∈ I. neg_depth_conjunct (ψs i) ≤ e8›
    using assms unfolding leq_components by auto
  hence sups:
    ‹Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I) ≤ e1›
    ‹Sup ((branch_conj_depth_conjunct ∘ ψs) ` I) ≤ e2›
    ‹Sup ((inst_conj_depth_conjunct ∘ ψs) ` I) ≤ e3›
    ‹Sup ((st_conj_depth_conjunct ∘ ψs) ` I) ≤ (e4 - 1)›
    ‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ e5›
    ‹Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I) ≤ e6›
    ‹Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I) ≤ e7›
    ‹Sup ((neg_depth_conjunct ∘ ψs) ` I) ≤ e8›
    by (simp add: Sup_le_iff)+
  hence ‹st_conj_depth_inner (StableConj I ψs) ≤ e4›
    using e_def is_some minus_energy_def leq_components st_conj_upds(4)
    by (metis add_diff_cancel_enat add_left_mono enat.simps(3) enat_defs(2) energy.sel(4) le_iff_add option.distinct(1))
  then show ?thesis
    using st_conj_upds sups
    by (simp add: e_def)
qed

lemma expr_imm_conj:
  assumes
    ‹subtract_fn  0 0 0 0 1 0 0 0 e = Some e'›
    ‹I ≠ {}›
    ‹expr_pr_inner (Conj I ψs) ≤ e'›
  shows ‹expressiveness_price (ImmConj I ψs) ≤ e›
proof-
  have conj_upds:
    ‹modal_depth_srbb_inner (Conj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
    ‹branch_conj_depth_inner (Conj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
    ‹inst_conj_depth_inner (Conj I ψs) = 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
    ‹st_conj_depth_inner (Conj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
    ‹imm_conj_depth_inner (Conj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_pos_conj_depth_inner (Conj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_neg_conj_depth_inner (Conj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)›
    ‹neg_depth_inner (Conj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
    using assms
    by force+
  have imm_conj_upds:
    ‹modal_depth_srbb (ImmConj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
    ‹branching_conjunction_depth (ImmConj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
    ‹unstable_conjunction_depth (ImmConj I ψs) = 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
    ‹stable_conjunction_depth (ImmConj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
    ‹immediate_conjunction_depth (ImmConj I ψs) = 1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_positive_conjunct_depth (ImmConj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_negative_conjunct_depth (ImmConj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)›
    ‹negation_depth (ImmConj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
    using assms
    by force+
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    using assms by (metis energy.exhaust_sel)
  hence is_some: ‹(e - (E 0 0 0 0 1 0 0 0)) = (E e1 e2 e3 e4 (e5-1) e6 e7 e8)›
    using minus_energy_def
    by simp
  hence ‹e5>0› using assms(1) e_def leq_components by auto
  have
    ‹E (modal_depth_srbb_inner (Conj I ψs))
       (branch_conj_depth_inner (Conj I ψs))
       (inst_conj_depth_inner (Conj I ψs))
       (st_conj_depth_inner (Conj I ψs))
       (imm_conj_depth_inner (Conj I ψs))
       (max_pos_conj_depth_inner (Conj I ψs))
       (max_neg_conj_depth_inner (Conj I ψs))
       (neg_depth_inner (Conj I ψs)) ≤ (E e1 e2 e3 e4 (e5-1) e6 e7 e8)›
    using is_some assms
    by (metis expr_pr_inner.simps option.discI option.inject)
  hence
    ‹(modal_depth_srbb_inner (Conj I ψs))≤ e1›
    ‹(branch_conj_depth_inner (Conj I ψs)) ≤ e2›
    ‹(inst_conj_depth_inner (Conj I ψs)) ≤ e3›
    ‹(st_conj_depth_inner (Conj I ψs))≤ e4›
    ‹(imm_conj_depth_inner (Conj I ψs))≤ (e5-1)›
    ‹(max_pos_conj_depth_inner (Conj I ψs)) ≤ e6›
    ‹(max_neg_conj_depth_inner (Conj I ψs)) ≤ e7›
    ‹(neg_depth_inner (Conj I ψs))≤ e8›
    by auto
  hence E:
    ‹Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I) ≤ e1›
    ‹Sup ((branch_conj_depth_conjunct ∘ ψs) ` I) ≤ e2›
    ‹1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I) ≤ e3›
    ‹Sup ((st_conj_depth_conjunct ∘ ψs) ` I) ≤ e4›
    ‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ (e5-1)›
    ‹Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I) ≤ e6›
    ‹Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I) ≤ e7›
    ‹Sup ((neg_depth_conjunct ∘ ψs) ` I) ≤ e8›
    using conj_upds by force+
  from ‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ (e5-1)› have ‹(1 + Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)) ≤ e5›
    using assms(1) ‹e5>0› is_some e_def add.right_neutral add_diff_cancel_enat enat_add_left_cancel_le ileI1 le_iff_add plus_1_eSuc(1)
    by metis
  thus ‹expressiveness_price (ImmConj I ψs) ≤ e› using imm_conj_upds E
    by (metis e_def  energy.sel expressiveness_price.elims leD somewhere_larger_eq)

qed

lemma expr_conj:
  assumes
    ‹subtract_fn 0 0 1 0 0 0 0 0 e = Some e'›
    ‹I ≠ {}›
    ‹∀q ∈ I. expr_pr_conjunct (ψs q) ≤ e'›
  shows ‹expr_pr_inner (Conj I ψs) ≤ e›
proof-
  have conj_upds:
    ‹modal_depth_srbb_inner (Conj I ψs) = Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I)›
    ‹branch_conj_depth_inner (Conj I ψs) = Sup ((branch_conj_depth_conjunct ∘ ψs) ` I)›
    ‹inst_conj_depth_inner (Conj I ψs) = 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
    ‹st_conj_depth_inner (Conj I ψs) = Sup ((st_conj_depth_conjunct ∘ ψs) ` I)›
    ‹imm_conj_depth_inner (Conj I ψs) = Sup ((imm_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_pos_conj_depth_inner (Conj I ψs) = Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I)›
    ‹max_neg_conj_depth_inner (Conj I ψs) = Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I)›
    ‹neg_depth_inner (Conj I ψs) = Sup ((neg_depth_conjunct ∘ ψs) ` I)›
    using assms by force+
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    using energy.exhaust_sel by metis
  hence is_some: ‹e - (E 0 0 1 0 0 0 0 0) = E e1 e2 (e3-1) e4 e5 e6 e7 e8›
    using minus_energy_def by simp
  hence ‹e3>0› using assms(1) e_def leq_components by auto
  hence
    ‹∀i ∈ I. modal_depth_srbb_conjunct (ψs i) ≤ e1›
    ‹∀i ∈ I. branch_conj_depth_conjunct (ψs i) ≤ e2›
    ‹∀i ∈ I. inst_conj_depth_conjunct (ψs i) ≤ (e3-1)›
    ‹∀i ∈ I. st_conj_depth_conjunct (ψs i) ≤ e4›
    ‹∀i ∈ I. imm_conj_depth_conjunct (ψs i) ≤ e5›
    ‹∀i ∈ I. max_pos_conj_depth_conjunct (ψs i) ≤ e6›
    ‹∀i ∈ I. max_neg_conj_depth_conjunct (ψs i) ≤ e7›
    ‹∀i ∈ I. neg_depth_conjunct (ψs i) ≤ e8›
    using assms is_some energy.sel leq_components
    by (metis expr_pr_conjunct.elims option.distinct(1) option.inject)+
  hence sups:
    ‹Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I) ≤ e1›
    ‹Sup ((branch_conj_depth_conjunct ∘ ψs) ` I) ≤ e2›
    ‹Sup ((inst_conj_depth_conjunct ∘ ψs) ` I) ≤ (e3-1)›
    ‹Sup ((st_conj_depth_conjunct ∘ ψs) ` I) ≤ e4›
    ‹Sup ((imm_conj_depth_conjunct ∘ ψs) ` I) ≤ e5›
    ‹Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I) ≤ e6›
    ‹Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I) ≤ e7›
    ‹Sup ((neg_depth_conjunct ∘ ψs) ` I) ≤ e8›
    by (simp add: Sup_le_iff)+
  hence ‹inst_conj_depth_inner (Conj I ψs) ≤ e3›
    using ‹e3>0› is_some e_def
    unfolding
      ‹inst_conj_depth_inner (Conj I ψs) = 1 + Sup ((inst_conj_depth_conjunct ∘ ψs) ` I)›
    by (metis add.right_neutral add_diff_cancel_enat enat_add_left_cancel_le ileI1 le_iff_add plus_1_eSuc(1))
  then show ?thesis
    using conj_upds sups
    by (simp add: e_def)
qed

lemma expr_br_conj:
  assumes
    ‹subtract_fn 0 1 1 0 0 0 0 0 e = Some e'›
    ‹min1_6 e' = Some e''›
    ‹subtract_fn 1 0 0 0 0 0 0 0 e'' = Some e'''›
    ‹expressiveness_price φ ≤ e'''›
    ‹∀q ∈ Q. expr_pr_conjunct (Φ q) ≤ e'›
    ‹1 + modal_depth_srbb φ ≤ pos_conjuncts e›
  shows ‹expr_pr_inner (BranchConj α φ Q Φ) ≤ e›
proof-
  obtain e1 e2 e3 e4 e5 e6 e7 e8 where e_def: ‹e = E e1 e2 e3 e4 e5 e6 e7 e8›
    by (smt (z3) energy.exhaust)
  hence e'''_def: ‹e''' = (E ((min e1 e6)-1) (e2-1) (e3-1) e4 e5 e6 e7 e8)›
    using minus_energy_def
    by (smt (z3) assms energy.sel idiff_0_right min_1_6_simps option.distinct(1) option.sel)
  hence min_vals: ‹the (min1_6 (e - E 0 1 1 0 0 0 0 0)) - (E 1 0 0 0 0 0 0 0) = (E ((min e1 e6)-1) (e2-1) (e3-1) e4 e5 e6 e7 e8)›
    using assms
    by (metis not_Some_eq option.sel)
  hence ‹0 < e1› ‹0 < e2› ‹0 < e3› ‹0 < e6›
    using assms energy.sel min_1_6_simps
    unfolding e_def minus_energy_def leq_components
    by (metis (no_types, lifting) gr_zeroI idiff_0_right min_enat_simps(3) not_one_le_zero option.distinct(1) option.sel, auto)
  have e_comp: ‹e - (E 0 1 1 0 0 0 0 0) = E e1 (e2-1) (e3-1) e4 e5 e6 e7 e8› using e_def
    by simp
  have conj:
    ‹E (modal_depth_srbb            φ)
       (branching_conjunction_depth φ)
       (unstable_conjunction_depth  φ)
       (stable_conjunction_depth    φ)
       (immediate_conjunction_depth φ)
       (max_positive_conjunct_depth φ)
       (max_negative_conjunct_depth φ)
       (negation_depth              φ)
          ≤ ((E ((min e1 e6)-1) (e2-1) (e3-1) e4 e5 e6 e7 e8))›
    using assms e'''_def by force
  hence conj_single:
    ‹modal_depth_srbb φ              ≤ ((min e1 e6)-1)›
    ‹branching_conjunction_depth  φ  ≤ e2 -1›
    ‹(unstable_conjunction_depth  φ) ≤ e3-1›
    ‹(stable_conjunction_depth    φ) ≤ e4›
    ‹(immediate_conjunction_depth φ) ≤ e5›
    ‹(max_positive_conjunct_depth φ) ≤ e6›
    ‹(max_negative_conjunct_depth φ) ≤ e7›
    ‹(negation_depth              φ) ≤ e8›
    using leq_components by auto
  have ‹0 < (min e1 e6)› using ‹0 < e1› ‹0 < e6›
    using min_less_iff_conj by blast
  hence ‹1 + modal_depth_srbb φ ≤ (min e1 e6)›
    using conj_single add.commute add_diff_assoc_enat add_diff_cancel_enat add_right_mono conj_single(2) i1_ne_infinity ileI1 one_eSuc
    by (metis (no_types, lifting))
  hence ‹1 + modal_depth_srbb φ ≤ e1› ‹1 + modal_depth_srbb φ ≤ e6›
    using min.bounded_iff by blast+
  from conj have ‹1 + branching_conjunction_depth φ ≤ e2›
    by (metis ‹0 < e2› add.commute add_diff_assoc_enat add_diff_cancel_enat add_right_mono conj_single(2) i1_ne_infinity ileI1 one_eSuc)
  from conj_single have ‹1 + unstable_conjunction_depth φ ≤ e3›
    using ‹0 < e3› add.commute add_diff_assoc_enat add_diff_cancel_enat add_right_mono conj_single(2) i1_ne_infinity ileI1 one_eSuc
    by (metis (no_types, lifting))
  have branch: ‹∀q∈Q.
    E (modal_depth_srbb_conjunct (Φ q))
      (branch_conj_depth_conjunct  (Φ q))
      (inst_conj_depth_conjunct  (Φ q))
      (st_conj_depth_conjunct  (Φ q))
      (imm_conj_depth_conjunct  (Φ q))
      (max_pos_conj_depth_conjunct  (Φ q))
      (max_neg_conj_depth_conjunct  (Φ q))
      (neg_depth_conjunct  (Φ q))
    ≤ (E e1 (e2-1) (e3-1) e4 e5 e6 e7 e8)›
    using assms e_def e_comp
    by (metis expr_pr_conjunct.simps option.distinct(1) option.sel)
  hence branch_single:
    ‹∀q∈Q. (modal_depth_srbb_conjunct (Φ q)) ≤ e1›
    ‹∀q∈Q. (branch_conj_depth_conjunct  (Φ q)) ≤ (e2-1)›
    ‹∀q∈Q. (inst_conj_depth_conjunct  (Φ q)) ≤ (e3-1)›
    ‹∀q∈Q. (st_conj_depth_conjunct  (Φ q)) ≤ e4›
    ‹∀q∈Q. (imm_conj_depth_conjunct  (Φ q)) ≤ e5›
    ‹∀q∈Q. (max_pos_conj_depth_conjunct  (Φ q)) ≤ e6›
    ‹∀q∈Q. (max_neg_conj_depth_conjunct  (Φ q)) ≤ e7›
    ‹∀q∈Q. (neg_depth_conjunct  (Φ q)) ≤ e8›
    by auto
  hence ‹∀q∈Q. (1 + branch_conj_depth_conjunct  (Φ q)) ≤ e2›
    by (metis ‹0 < e2› add.commute add_diff_assoc_enat add_diff_cancel_enat add_right_mono i1_ne_infinity ileI1 one_eSuc)
  from branch_single have ‹∀q∈Q. (1 + inst_conj_depth_conjunct  (Φ q)) ≤ e3›
    using ‹0 < e3›
    by (metis add.commute add_diff_assoc_enat add_diff_cancel_enat add_right_mono i1_ne_infinity ileI1 one_eSuc)
  have
    ‹expr_pr_inner (BranchConj α φ Q Φ)
    = E (modal_depth_srbb_inner (BranchConj α φ Q Φ))
      (branch_conj_depth_inner (BranchConj α φ Q Φ))
      (inst_conj_depth_inner (BranchConj α φ Q Φ))
      (st_conj_depth_inner (BranchConj α φ Q Φ))
      (imm_conj_depth_inner (BranchConj α φ Q Φ))
      (max_pos_conj_depth_inner (BranchConj α φ Q Φ))
      (max_neg_conj_depth_inner (BranchConj α φ Q Φ))
      (neg_depth_inner (BranchConj α φ Q Φ))› by simp
  hence expr:
    ‹expr_pr_inner (BranchConj α φ Q Φ)
    = E (Sup ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ Φ) ` Q)))
      (1 + Sup ({branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ Φ) ` Q)))
      (1 + Sup ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ Φ) ` Q)))
      (Sup ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ Φ) ` Q)))
      (Sup ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ Φ) ` Q)))
      (Sup ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ} ∪ ((max_pos_conj_depth_conjunct ∘ Φ) ` Q)))
      (Sup ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ Φ) ` Q)))
      (Sup ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ Φ) ` Q)))› by auto
  from branch_single ‹1 + modal_depth_srbb φ ≤ e1›
    have ‹∀x ∈ ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ Φ) ` Q)). x ≤ e1›
    by fastforce
  hence e1_le: ‹(Sup ({1 + modal_depth_srbb φ} ∪ ((modal_depth_srbb_conjunct ∘ Φ) ` Q))) ≤ e1›
    using Sup_least by blast
  have ‹∀x ∈ {branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ Φ) ` Q). x ≤ e2 -1›
    using branch_single conj_single comp_apply image_iff insertE by auto
  hence e2_le: ‹1 + Sup ({branching_conjunction_depth φ} ∪ ((branch_conj_depth_conjunct ∘ Φ) ` Q)) ≤ e2›
    using Sup_least
    by (metis Un_insert_left ‹0 < e2› add.commute eSuc_minus_1 enat_add_left_cancel_le ileI1 le_iff_add one_eSuc plus_1_eSuc(2) sup_bot_left)
  have ‹∀x ∈ ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e3-1›
    using conj_single branch_single
    using comp_apply image_iff insertE by auto
  hence e3_le: ‹1 + Sup ({unstable_conjunction_depth φ} ∪ ((inst_conj_depth_conjunct ∘ Φ) ` Q)) ≤ e3›
    using Un_insert_left ‹0<e3›  add.commute eSuc_minus_1 enat_add_left_cancel_le ileI1 le_iff_add one_eSuc plus_1_eSuc(2) sup_bot_left
    by (metis Sup_least)
  have fa:
    ‹∀x ∈ ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e4›
    ‹∀x ∈ ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e5›
    ‹∀x ∈ ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ} ∪ ((max_pos_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e6›
    ‹∀x ∈ ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ Φ) ` Q)). x ≤ e7›
    ‹∀x ∈ ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ Φ) ` Q)). x ≤ e8›
      using conj_single branch_single ‹1 + modal_depth_srbb φ ≤ e6› by auto
  hence
    ‹(Sup ({stable_conjunction_depth φ} ∪ ((st_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e4›
    ‹(Sup ({immediate_conjunction_depth φ} ∪ ((imm_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e5›
    ‹(Sup ({1 + modal_depth_srbb φ, max_positive_conjunct_depth φ} ∪ ((max_pos_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e6›
    ‹(Sup ({max_negative_conjunct_depth φ} ∪ ((max_neg_conj_depth_conjunct ∘ Φ) ` Q))) ≤ e7›
    ‹(Sup ({negation_depth φ} ∪ ((neg_depth_conjunct ∘ Φ) ` Q))) ≤ e8›
    using Sup_least
    by metis+
  thus ‹expr_pr_inner (BranchConj α φ Q Φ) ≤ e›
    using expr e3_le e2_le e1_le e_def energy.sel leq_components by presburger
qed

lemma expressiveness_price_ImmConj_geq_parts:
  assumes ‹i ∈ I›
  shows ‹expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0 ≥ expr_pr_conjunct (ψs i)›
proof-
  from assms have ‹I ≠ {}› by blast
  from expressiveness_price_ImmConj_non_empty_def[OF ‹I ≠ {}›]
  have ‹expressiveness_price (ImmConj I ψs) ≥ E 0 0 1 0 1 0 0 0›
    using energy_leq_cases by force
  hence
  ‹expressiveness_price (ImmConj I ψs) - E 0 0 1 0 1 0 0 0 = E
    (Sup ((modal_depth_srbb_conjunct ∘ ψs) ` I))
    (Sup ((branch_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((inst_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((st_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((imm_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((max_pos_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((max_neg_conj_depth_conjunct ∘ ψs) ` I))
    (Sup ((neg_depth_conjunct ∘ ψs) ` I))›
    unfolding expressiveness_price_ImmConj_non_empty_def[OF ‹I ≠ {}›]
    by simp
  also have ‹... ≥ expr_pr_conjunct (ψs i)›
    using assms ‹I ≠ {}› SUP_upper unfolding leq_components by fastforce
  finally show ?thesis .
qed

lemma expressiveness_price_ImmConj_geq_parts':
  assumes ‹i ∈ I›
  shows ‹(expressiveness_price (ImmConj I ψs) - E 0 0 0 0 1 0 0 0) - E 0 0 1 0 0 0 0 0 ≥ expr_pr_conjunct (ψs i)›
  using expressiveness_price_ImmConj_geq_parts[OF assms]
    less_eq_energy_def minus_energy_def
  by (smt (z3) energy.sel idiff_0_right)

end (* LTS_Tau *)

text ‹Here, we show the prices for some specific formulas.›
locale Inhabited_LTS = LTS step
  for step :: ‹'s ⇒ 'a ⇒ 's ⇒ bool› (‹_ ↦ _ _› [70,70,70] 80) +
  fixes left :: 's
    and right :: 's
  assumes left_right_distinct: ‹(left::'s) ≠ (right::'s)›

begin

lemma example_φ_cp:
  fixes op::‹'a› and a::‹'a› and b::‹'a›
  defines φ: ‹φ ≡
    (Internal
      (Obs op
        (Internal
          (Conj {left, right}
                (λi. (if i = left
                      then (Pos (Obs a TT))
                      else if i = right
                           then (Pos (Obs b TT))
                           else undefined))))))›
  shows
      ‹modal_depth_srbb            φ = 2›
  and ‹branching_conjunction_depth φ = 0›
  and ‹unstable_conjunction_depth  φ = 1›
  and ‹stable_conjunction_depth    φ = 0›
  and ‹immediate_conjunction_depth φ = 0›
  and ‹max_positive_conjunct_depth φ = 1›
  and ‹max_negative_conjunct_depth φ = 0›
  and ‹negation_depth              φ = 0›
  unfolding φ
  by simp+

lemma ‹expressiveness_price (Internal
      (Obs op
        (Internal
          (Conj {left, right}
                (λi. (if i = left
                      then (Pos (Obs a TT))
                      else if i = right
                           then (Pos (Obs b TT))
                           else undefined)))))) = E 2 0 1 0 0 1 0 0›
  by simp

end (* Inhabited_LTS *)

context LTS_Tau
begin

lemma ‹expressiveness_price TT = E 0 0 0 0 0 0 0 0›
  by simp

lemma ‹expressiveness_price (ImmConj {} ψs) = E 0 0 0 0 0 0 0 0›
  by (simp add: Sup_enat_def)

lemma ‹expressiveness_price (Internal (Conj {} ψs)) = E 0 0 0 0 0 0 0 0›
  by (simp add: Sup_enat_def)

lemma ‹expressiveness_price (Internal (BranchConj α TT {} ψs)) = E 1 1 1 0 0 1 0 0›
  by (simp add: Sup_enat_def)

lemma expr_obs_phi:
  shows ‹subtract_fn 1 0 0 0 0 0 0 0 (expr_pr_inner (Obs α φ)) = Some (expressiveness_price φ)›
  by simp

subsection ‹Characterizing Equivalence by Energy Coordinates›

text ‹A state ‹p› pre-orders another state ‹q› with respect to some energy ‹e› if and only if ‹p› HML pre-orders ‹q› with respect to the HML sublanguage @{term ‹𝒪›} derived from ‹e›.›
definition expr_preord :: ‹'s ⇒ energy ⇒ 's ⇒ bool› (‹_ ≼ _ _› 60) where
  ‹(p ≼ e q) ≡ preordered (𝒪 e) p q›

text ‹Conversely, ‹p› and ‹q› are equivalent with respect to ‹e› if and only if they are equivalent with respect to that HML sublanguage @{term ‹𝒪›}.›
definition expr_equiv :: ‹'s ⇒ energy ⇒ 's ⇒ bool› (‹_ ∼ _ _› 60) where
  ‹(p ∼ e q) ≡ equivalent (𝒪 e) p q›

subsection ‹Relational Effects of Prices›


lemma distinction_combination_eta:
  fixes p q
  defines ‹Qα ≡ {q'. q ↠ q' ∧  (∄φ. φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ 0 0) ∧ distinguishes φ p q')}›
  assumes
    ‹p ↦a α p'›
    ‹∀q'∈ Qα.
      ∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ distinguishes (Φ q''') p' q'''›
  shows
    ‹∀q'∈ Qα. hml_srbb_inner.distinguishes (Obs α (Internal (Conj
      {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} (conjunctify_distinctions Φ p')))) p q'›
proof -
  have ‹∀q'∈ Qα. ∀q'''∈{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
      hml_srbb_conj.distinguishes ((conjunctify_distinctions Φ p') q''') p' q'''›
  proof clarify
    fix q' q'' q'''
    assume ‹q' ∈ Qα› ‹q' ↦a α q''› ‹q'' ↠ q'''›
    thus ‹hml_srbb_conj.distinguishes (conjunctify_distinctions Φ p' q''') p' q'''›
       using assms(3)  distinction_conjunctification by blast
  qed
  hence ‹∀q'∈ Qα. ∀q''. q' ↦a α q''
    ⟶ distinguishes (Internal (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} (conjunctify_distinctions Φ p')))  p' q''›
    using silent_reachable.refl unfolding Qα_def by fastforce
  thus ‹∀q'∈ Qα.
     hml_srbb_inner.distinguishes (Obs α (Internal (Conj
        {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} (conjunctify_distinctions Φ p')))) p q'›
    using assms(2) by (auto) (metis silent_reachable.refl)+
qed

lemma distinction_conjunctification_two_way_price:
  assumes
    ‹∀q∈I. distinguishes (Φ q) p q ∨ distinguishes (Φ q) q p›
    ‹∀q∈I. Φ q ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
  shows
    ‹∀q∈I.
      (if distinguishes (Φ q) p q then conjunctify_distinctions else conjunctify_distinctions_dual) Φ p q
      ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
proof
  fix q
  assume ‹q ∈ I›
  show ‹(if distinguishes (Φ q) p q then conjunctify_distinctions else conjunctify_distinctions_dual) Φ p q ∈ 𝒪_conjunct (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞)›
  proof (cases ‹Φ q›)
    case TT
    then show ?thesis
      using assms ‹q ∈ I›
      by fastforce
  next
    case (Internal χ)
    then show ?thesis
      using assms ‹q ∈ I›
      unfolding conjunctify_distinctions_def conjunctify_distinctions_dual_def 𝒪_def 𝒪_conjunct_def
      by fastforce
  next
    case (ImmConj J Ψ)
    hence ‹J = {}›
      using assms ‹q ∈ I› unfolding 𝒪_def
      by (simp, metis iadd_is_0 immediate_conjunction_depth.simps(3) zero_one_enat_neq(1))
    then show ?thesis
      using assms ‹q ∈ I› ImmConj by fastforce
  qed
qed

lemma distinction_combination_eta_two_way:
  fixes p q p' Φ
  defines
    ‹Qα ≡ {q'. q ↠ q' ∧  (∄φ. φ ∈ 𝒪 (E ∞ ∞ ∞ 0 0 ∞ ∞ ∞) ∧ (distinguishes φ p q' ∨ distinguishes φ q' p))}› and
    ‹Ψα ≡ λq'''. (if distinguishes (Φ q''') p' q''' then conjunctify_distinctions else conjunctify_distinctions_dual) Φ p' q'''›
  assumes
    ‹p ↦a α p'›
    ‹∀q'∈ Qα.
      ∀q'' q'''. q' ↦a α q'' ⟶ q'' ↠ q''' ⟶ distinguishes (Φ q''') p' q''' ∨ distinguishes (Φ q''') q''' p'›
  shows
    ‹∀q'∈ Qα. hml_srbb_inner.distinguishes (Obs α (Internal (Conj
      {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
      Ψα))) p q'›
proof -
  have ‹∀q'∈ Qα. ∀q'''∈{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
      hml_srbb_conj.distinguishes (Ψα q''') p' q'''›
  proof clarify
    fix q' q'' q'''
    assume ‹q' ∈ Qα› ‹q' ↦a α q''› ‹q'' ↠ q'''›
    thus ‹hml_srbb_conj.distinguishes
        (Ψα q''') p' q''' ›
      using assms(4) distinction_conjunctification_two_way Ψα_def by blast
  qed
  hence ‹∀q'∈ Qα. ∀q'''∈{q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}.
    hml_srbb_inner.distinguishes (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''}
      Ψα)  p' q'''›
    using srbb_dist_conjunct_implies_dist_conjunction
    unfolding lts_semantics.distinguishes_def
    by (metis (no_types, lifting))
  hence ‹∀q'∈ Qα. ∀q'''. (∃q''. q' ↦a α q'' ∧ q'' ↠ q''') ⟶
    hml_srbb_inner.distinguishes (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} Ψα)  p' q'''›
    by blast
  hence ‹∀q'∈ Qα. ∀q''. q' ↦a α q'' ⟶
    distinguishes (Internal  (Conj {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} Ψα)) p' q''›
    by (meson distinguishes_def hml_srbb_inner.distinguishes_def hml_srbb_models.simps(2) silent_reachable.refl)
  thus ‹∀q'∈ Qα.
     hml_srbb_inner.distinguishes (Obs α (Internal (Conj
        {q'''. ∃q'∈ Qα. ∃q''. q' ↦a α q'' ∧ q'' ↠ q'''} Ψα))) p q'›
    using assms(3)
    by auto (metis silent_reachable.refl)+
qed

lemma distinction_conjunctification_price:
  assumes
    ‹∀q∈I. distinguishes (Φ q) p q›
    ‹∀q∈I. Φ q ∈ 𝒪 pr›
    ‹modal_depth pr ≤ pos_conjuncts pr›
  shows
    ‹∀q∈I. ((conjunctify_distinctions Φ p) q) ∈ 𝒪_conjunct pr›
proof
  fix q
  assume ‹q ∈ I›
  show ‹conjunctify_distinctions Φ p q ∈ 𝒪_conjunct pr›
  proof (cases ‹Φ q›)
    case TT
    then show ?thesis
      using assms ‹q ∈ I›
      by fastforce
  next
    case (Internal χ)
    then show ?thesis
      using assms ‹q ∈ I›
      unfolding conjunctify_distinctions_def 𝒪_def 𝒪_conjunct_def
      by fastforce
  next
    case (ImmConj J Ψ)
    hence ‹∃i. i∈J ∧ hml_srbb_conj.distinguishes (Ψ i) p q›
      using ‹q ∈ I› assms(1) by fastforce
    moreover have ‹conjunctify_distinctions Φ p q  = Ψ (SOME i. i∈J ∧ hml_srbb_conj.distinguishes (Ψ i) p q)›
      unfolding ImmConj conjunctify_distinctions_def by simp
    ultimately have Ψ_i: ‹∃i∈J. hml_srbb_conj.distinguishes (Ψ i) p q ∧ conjunctify_distinctions Φ p q = Ψ i›
      by (metis (no_types, lifting) some_eq_ex)
    hence ‹conjunctify_distinctions Φ p q ∈ Ψ`J›
      unfolding image_iff by blast
    hence ‹expr_pr_conjunct (conjunctify_distinctions Φ p q) ≤ expressiveness_price (ImmConj J Ψ)›
      by (smt (verit, best) Ψ_i dual_order.trans expressiveness_price_ImmConj_geq_parts gets_smaller)
    then show ?thesis
      using assms ‹q ∈ I› ImmConj
      unfolding 𝒪_def 𝒪_conjunct_def
      by auto
  qed
qed

lemma modal_stability_respecting:
  ‹stability_respecting (preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)))›
  unfolding stability_respecting_def
proof safe
  fix p q
  assume p_stability:
    ‹preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q›
    ‹stable_state p›
  have ‹¬(∀q'. q ↠ q' ⟶ ¬ preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q' ∨ ¬ stable_state q')›
  proof safe
    assume ‹∀q'. q ↠ q' ⟶ ¬ preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q' ∨ ¬ stable_state q'›
    hence  ‹∀q'. q ↠ q' ⟶ stable_state q' ⟶ (∃φ ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8). distinguishes φ p q')› by auto
    then obtain Φ where Φ_def:
      ‹∀q'∈(silent_reachable_set {q}). stable_state q'
      ⟶ distinguishes (Φ q') p q' ∧ Φ q' ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
      using singleton_iff sreachable_set_is_sreachable by metis
    hence distinctions:
      ‹∀q'∈(silent_reachable_set {q} ∩ {q'. stable_state q'}). distinguishes (Φ q') p q'›
      ‹∀q'∈(silent_reachable_set {q} ∩ {q'. stable_state q'}). Φ q' ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)› by blast+
    from distinction_conjunctification_price[OF this] have
      ‹∀q'∈(silent_reachable_set {q} ∩ {q'. stable_state q'}). conjunctify_distinctions Φ p q' ∈ 𝒪_conjunct (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
      by fastforce
    hence conj_price: ‹StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'}) (conjunctify_distinctions Φ p)
        ∈ 𝒪_inner (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
      unfolding 𝒪_inner_def 𝒪_conjunct_def using SUP_le_iff by fastforce
    from Φ_def have
      ‹∀q'∈(silent_reachable_set {q}). stable_state q' ⟶
         hml_srbb_conj.distinguishes (conjunctify_distinctions Φ p q') p q'›
      using singleton_iff distinction_conjunctification by metis
    hence ‹hml_srbb_inner.distinguishes_from
       (StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'}) (conjunctify_distinctions Φ p))
       p (silent_reachable_set {q})›
      using p_stability(2) by fastforce
    hence
      ‹distinguishes
        (Internal (StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'})
                (conjunctify_distinctions Φ p)))
        p q›
      unfolding silent_reachable_set_def
      using silent_reachable.refl by auto
    moreover have
      ‹Internal (StableConj (silent_reachable_set {q} ∩ {q'. stable_state q'}) (conjunctify_distinctions Φ p))
        ∈ 𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)›
      using conj_price unfolding 𝒪_def 𝒪_inner_def by simp
    ultimately show False
      using p_stability(1) preordered_no_distinction by blast
  qed
  thus ‹∃q'. q ↠ q' ∧ preordered (𝒪 (E e1 e2 e3 ∞ e5 ∞ e7 e8)) p q' ∧ stable_state q'›
    by blast
qed

end

end