Theory SimulationRelationsOnEncodedLabels

(* Kirstin Peters, University of Augsburg, 2026 *)

theory SimulationRelationsOnEncodedLabels
  imports SimulationRelations Encodings
begin

section ‹Simulation Relations with Encoded Labels›

text ‹The standard notion of labelled simulation relations require labels to match exactly. We now
      relax this requirement by allowing to simulate a source term step in the target with an
      encoded label.›

subsection ‹Simulation›

text ‹A weak labelled simulation on encoded labels is relation R such that if (P, Q) in R and P
      evolves to some P' using label a then there exist b and Q' such that Q evolves to Q' using b,
      (P', Q') in R, and a and b are related labels. Remember that a and b are related, if they are
      equal or if one is the translation of the other.›

abbreviation (in encodingLS_encL) weak_labelled_simulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "weak_labelled_simulation_encL Rel ≡
   ∀P Q α P'. (P, Q) ∈ Rel ∧ P ─⁀α→(STLCal Source Target)* P' ⟶
   (∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"

text ‹A weak labelled simulation on encoded labels simulates words of labels including the empty
      word, if the label encoding preserves the internal action. We can relax the requirement of
      the respection of the internal to preservation (respectively reflection), if the considered
      relation never relates a target to a source term (respectively a source to a target term).›

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_respection_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation: "weak_labelled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →(STLCal Source Target)* P'"
      and respection: "encL_respects_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-STLCal→(STLCal Source Target)* P'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'"
                                         and A2: "(P', Q') ∈ Rel" and A3: "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  from respection A3 have "β = τ-STLCal"
    using encL_respects_internal_implies_iff_internal[of P "τ-STLCal" Q β]
    by blast
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_preservation_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation:   "weak_labelled_simulation_encL Rel"
      and relation:     "(P, Q) ∈ Rel"
      and execution:    "P →(STLCal Source Target)* P'"
      and no_T_to_S:    "¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-STLCal→(STLCal Source Target)* P'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'"
                                         and A2: "(P', Q') ∈ Rel" and A3: "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  have "β = τ-STLCal"
  proof (cases "P ∈ ProcS")
    assume "P ∈ ProcS"
    with preservation A3 show "β = τ-STLCal"
      using encL_preserves_internal_implies_source_internal_to_internal[of P Q β]
      by simp
  next
    assume "¬P ∈ ProcS"
    with no_T_to_S have B1: "P ∼ST Q"
      using source_or_target[of P] source_or_target[of Q]
      by blast
    hence B2: "¬⦇P, τ-STLCal⦈↦⟨Q, β⟩"
      using kinds_of_encoded_label(1, 3)[of P "τ-STLCal" Q β]
      by blast
    from B1 have "¬⦇Q, β⦈↦⟨P, τ-STLCal⟩"
      using kinds_of_encoded_label(1, 3)[of Q β P "τ-STLCal"]
      by blast
    with A3 B2 show "β = τ-STLCal"
      using related_labels_get_condition(1)[of P "τ-STLCal" Q β]
      by simp
  qed
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_reflection_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation: "weak_labelled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →(STLCal Source Target)* P'"
      and no_S_to_T:  "¬(P ∈ ProcS ∧ Q ∈ ProcT)"
      and reflection: "encL_reflects_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-STLCal→(STLCal Source Target)* P'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'"
                                         and A2: "(P', Q') ∈ Rel" and A3: "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  have "β = τ-STLCal"
  proof (cases "P ∈ ProcS")
    assume "P ∈ ProcS"
    with no_S_to_T have B1: "P ∼ST Q"
      using source_or_target[of P] source_or_target[of Q]
      by blast
    hence B2: "¬⦇P, τ-STLCal⦈↦⟨Q, β⟩"
      using kinds_of_encoded_label(1, 3)[of P "τ-STLCal" Q β]
      by blast
    from B1 have "¬⦇Q, β⦈↦⟨P, τ-STLCal⟩"
      using kinds_of_encoded_label(1, 3)[of Q β P "τ-STLCal"]
      by blast
    with A3 B2 show "β = τ-STLCal"
      using related_labels_get_condition(1)[of P "τ-STLCal" Q β]
      by simp
  next
    assume "¬P ∈ ProcS"
    hence "P ∈ ProcT"
      using source_or_target[of P]
      by simp
    with reflection A3 show "β = τ-STLCal"
      using encL_reflects_internal_implies_target_internal_to_internal[of P Q β]
      by simp
  qed
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_respection_word:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
    and w v    :: "('labS, 'labT) Lab list"
  assumes simulation: "weak_labelled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P ─⌢w→(STLCal Source Target)* P'"
      and respection: "encL_respects_internal"
    shows "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P ─⌢w→Cal* P'"
    by simp
  from this simulation relation respection Cal_def
  show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  proof (induct arbitrary: v)
    case (WLS_Nil P Cal P')
    assume "P →Cal* P'" and "Cal = STLCal Source Target"
    hence "P →(STLCal Source Target)* P'"
      by simp
    moreover assume "weak_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
                and "encL_respects_internal"
    ultimately obtain Q' where A1: "Q →(STLCal Source Target)* Q'" and A2: "(P', Q') ∈ Rel"
      using weak_labelled_simulation_encL_and_respection_internal[of Rel P Q P']
      by blast
    from A1 have A3: "Q ─⌢[]→(STLCal Source Target)* Q'"
      using weakLabelledSequence.WLS_Nil[of Q "STLCal Source Target" Q']
      by simp
    have "⟨P, []⟩ ≡⦇⦈* ⟨Q, []⟩"
      using ELNil[of P Q] ELNil[of Q P] source_or_target[of P] source_or_target[of Q]
      unfolding related_words_def
      by auto
    with A2 A3
    show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  next
    case (WLS_Cons P w Cal P' α P'')
    from WLS_Cons(2) have IH: "weak_labelled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧
      encL_respects_internal ∧ Cal = STLCal Source Target ⟹
      ∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by simp
    assume A1: "weak_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel" and "encL_respects_internal"
       and A2: "Cal = STLCal Source Target"
    with IH obtain v Q' where A3: "Q ─⌢v→(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
                          and A5: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
    assume "P' ─⁀α→Cal* P''"
    with A1 A2 A4 obtain β Q'' where A6: "Q' ─⁀β→(STLCal Source Target)* Q''"
                                 and A7: "(P'', Q'') ∈ Rel" and A8: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    with A3 A6 have A9: "Q ─⌢(v@[β])→(STLCal Source Target)* Q''"
      using weakLabelledSequence.WLS_Cons[of Q v "STLCal Source Target" Q' β Q'']
      by simp
    assume "P ─⌢w→Cal* P'"
    with A2 have A10: "P ∼ST P'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
      by blast
    from A3 have "Q ∼ST Q'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q v Q']
      by blast
    with A5 A8 A10 have "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
      using related_words_compose[of P w Q v P' α Q' β]
      by simp
    with A7 A9
    show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, w@[α]⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  qed
qed

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_preservation_word:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
    and w v    :: "('labS, 'labT) Lab list"
  assumes simulation:   "weak_labelled_simulation_encL Rel"
      and relation:     "(P, Q) ∈ Rel"
      and execution:    "P ─⌢w→(STLCal Source Target)* P'"
      and no_T_to_S:    "¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
    shows "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P ─⌢w→Cal* P'"
    by simp
  from this simulation relation no_T_to_S preservation Cal_def
  show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  proof (induct arbitrary: v)
    case (WLS_Nil P Cal P')
    assume "P →Cal* P'" and "Cal = STLCal Source Target"
    hence "P →(STLCal Source Target)* P'"
      by simp
    moreover assume "weak_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
                and "¬(P ∈ ProcT ∧ Q ∈ ProcS)" and "encL_preserves_internal"
    ultimately obtain Q' where A1: "Q →(STLCal Source Target)* Q'" and A2: "(P', Q') ∈ Rel"
      using weak_labelled_simulation_encL_and_preservation_internal[of Rel P Q P']
      by blast
    from A1 have A3: "Q ─⌢[]→(STLCal Source Target)* Q'"
      using weakLabelledSequence.WLS_Nil[of Q "STLCal Source Target" Q']
      by simp
    have "⟨P, []⟩ ≡⦇⦈* ⟨Q, []⟩"
      using ELNil[of P Q] ELNil[of Q P] source_or_target[of P] source_or_target[of Q]
      unfolding related_words_def
      by auto
    with A2 A3
    show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  next
    case (WLS_Cons P w Cal P' α P'')
    from WLS_Cons(2) have IH: "weak_labelled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧
      ¬(P ∈ ProcT ∧ Q ∈ ProcS) ∧ encL_preserves_internal ∧ Cal = STLCal Source Target ⟹
      ∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by simp
    assume A1: "weak_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and "¬(P ∈ ProcT ∧ Q ∈ ProcS)" and "encL_preserves_internal"
       and A2: "Cal = STLCal Source Target"
    with IH obtain v Q' where A3: "Q ─⌢v→(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
                          and A5: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
    assume "P' ─⁀α→Cal* P''"
    with A1 A2 A4 obtain β Q'' where A6: "Q' ─⁀β→(STLCal Source Target)* Q''"
                                 and A7: "(P'', Q'') ∈ Rel" and A8: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    with A3 A6 have A9: "Q ─⌢(v@[β])→(STLCal Source Target)* Q''"
      using weakLabelledSequence.WLS_Cons[of Q v "STLCal Source Target" Q' β Q'']
      by simp
    assume "P ─⌢w→Cal* P'"
    with A2 have A10: "P ∼ST P'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
      by blast
    from A3 have "Q ∼ST Q'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q v Q']
      by blast
    with A5 A8 A10 have "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
      using related_words_compose[of P w Q v P' α Q' β]
      by simp
    with A7 A9
    show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, w@[α]⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  qed
qed

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_reflection_word:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
    and w v    :: "('labS, 'labT) Lab list"
  assumes simulation: "weak_labelled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P ─⌢w→(STLCal Source Target)* P'"
      and no_S_to_T:  "¬(P ∈ ProcS ∧ Q ∈ ProcT)"
      and reflection: "encL_reflects_internal"
    shows "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P ─⌢w→Cal* P'"
    by simp
  from this simulation relation no_S_to_T reflection Cal_def
  show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  proof (induct arbitrary: v)
    case (WLS_Nil P Cal P')
    assume "P →Cal* P'" and "Cal = STLCal Source Target"
    hence "P →(STLCal Source Target)* P'"
      by simp
    moreover assume "weak_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
                and "¬(P ∈ ProcS ∧ Q ∈ ProcT)" and "encL_reflects_internal"
    ultimately obtain Q' where A1: "Q →(STLCal Source Target)* Q'" and A2: "(P', Q') ∈ Rel"
      using weak_labelled_simulation_encL_and_reflection_internal[of Rel P Q P']
      by blast
    from A1 have A3: "Q ─⌢[]→(STLCal Source Target)* Q'"
      using weakLabelledSequence.WLS_Nil[of Q "STLCal Source Target" Q']
      by simp
    have "⟨P, []⟩ ≡⦇⦈* ⟨Q, []⟩"
      using ELNil[of P Q] ELNil[of Q P] source_or_target[of P] source_or_target[of Q]
      unfolding related_words_def
      by auto
    with A2 A3
    show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  next
    case (WLS_Cons P w Cal P' α P'')
    from WLS_Cons(2) have IH: "weak_labelled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧
      ¬(P ∈ ProcS ∧ Q ∈ ProcT) ∧ encL_reflects_internal ∧ Cal = STLCal Source Target ⟹
      ∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by simp
    assume A1: "weak_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and "¬(P ∈ ProcS ∧ Q ∈ ProcT)" and "encL_reflects_internal"
       and A2: "Cal = STLCal Source Target"
    with IH obtain v Q' where A3: "Q ─⌢v→(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
                          and A5: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
    assume "P' ─⁀α→Cal* P''"
    with A1 A2 A4 obtain β Q'' where A6: "Q' ─⁀β→(STLCal Source Target)* Q''"
                                 and A7: "(P'', Q'') ∈ Rel" and A8: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    with A3 A6 have A9: "Q ─⌢(v@[β])→(STLCal Source Target)* Q''"
      using weakLabelledSequence.WLS_Cons[of Q v "STLCal Source Target" Q' β Q'']
      by simp
    assume "P ─⌢w→Cal* P'"
    with A2 have A10: "P ∼ST P'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
      by blast
    from A3 have "Q ∼ST Q'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q v Q']
      by blast
    with A5 A8 A10 have "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
      using related_words_compose[of P w Q v P' α Q' β]
      by simp
    with A7 A9
    show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, w@[α]⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  qed
qed

text ‹Again the reflexive and closure of a weak simulation is a weak simulation. However, the
      transitive closure of a weak simulation is not necessarily a weak simulation, since the
      labels can not necessarily be combined. The transitive closure is a weak simulation, if the
      label encoding is injective.›

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes simulation: "weak_labelled_simulation_encL Rel"
  shows "weak_labelled_simulation_encL (Rel⇧=)"
  using assms
proof auto
  fix P Q α P'
  assume "weak_labelled_simulation_encL Rel" and "P ─⁀α→(STLCal Source Target)* P'"
     and "(P, Q) ∈ Rel"
  hence "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
  thus "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix Q α P'
  assume "Q ─⁀α→(STLCal Source Target)* P'"
  moreover have "Q ∼ST Q"
    using source_or_target[of Q]
    by presburger
  hence "⟨Q, α⟩ ≡⦇⦈ ⟨Q, α⟩"
    unfolding related_labels_def
    by simp
  ultimately
  show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨Q, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_simulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes simulation: "weak_labelled_simulation_encL Rel"
      and injective:  "inj encL"
    shows "weak_labelled_simulation_encL (Rel⇧=)"
      and "weak_labelled_simulation_encL (Rel⇧+)"
      and "weak_labelled_simulation_encL (Rel⇧*)"
proof -
  from simulation show A1: "weak_labelled_simulation_encL (Rel⇧=)"
    using weak_labelled_simulation_encL_and_refl_closure[of Rel]
    by simp
  have A2: "⋀Rel. weak_labelled_simulation_encL Rel ⟹ weak_labelled_simulation_encL (Rel⇧+)"
  proof clarify
    fix Rel P Q α P'
    assume B: "weak_labelled_simulation_encL Rel"
    assume "(P, Q) ∈ Rel⇧+" and "P ─⁀α→(STLCal Source Target)* P'"
    thus "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ─⁀α→(STLCal Source Target)* P'"
      with B obtain β Q' where "Q ─⁀β→(STLCal Source Target)* Q'" and "(P', Q') ∈ Rel"
                           and "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
      thus "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ─⁀α→(STLCal Source Target)* P' ⟹
              (∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
         and "P ─⁀α→(STLCal Source Target)* P'"
      from this obtain β Q' where C1: "Q ─⁀β→(STLCal Source Target)* Q'" and C2: "(P', Q') ∈ Rel⇧+"
                              and C3: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
      assume "(Q, R) ∈ Rel"
      with B C1 obtain γ R' where C4: "R ─⁀γ→(STLCal Source Target)* R'" and C5: "(Q', R') ∈ Rel⇧+"
                              and C6: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
        by blast
      from C2 C5 have C7: "(P', R') ∈ Rel⇧+"
        by simp
      from injective C3 C6 have "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        using related_labels_trans_inj[of P α Q β R γ]
        by simp
      with C4 C7
      show "∃γ R'. R ─⁀γ→(STLCal Source Target)* R' ∧ (P', R') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        by blast
    qed
  qed
  with simulation show "weak_labelled_simulation_encL (Rel⇧+)"
    by blast
  from simulation A1 A2[of "Rel⇧="] show "weak_labelled_simulation_encL (Rel⇧*)"
      using trancl_reflcl[of Rel]
    by fast
qed

text ‹A strong labelled simulation with encoded labels is relation R such that for each pair (P, Q)
      in R and each step of P to some P' using a there exists some b and Q' such that there is a
      step of Q to Q' using b, (P', Q') in R, and a and b are related labels.›

abbreviation (in encodingLS_encL) strong_labelled_simulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "strong_labelled_simulation_encL Rel ≡
   ∀P Q α P'. (P, Q) ∈ Rel ∧ P ─α→(STLCal Source Target) P' ⟶
   (∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"

text ‹A strong simulation is also a weak simulation, if the label encoding respects the internal.
      Again we can relax the requirement of the respection of the internal to preservation, if the
      considered relation never relates a target to a source term. However, if the label encoding
      reflects the internal, then a strong simulation that does not relate any source term to a
      target term also simulates weak internal steps but is not a weak simulation. Reflection does
      not allows to related internal labels.›

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_respection_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation: "strong_labelled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →(STLCal Source Target)* P'"
      and respection: "encL_respects_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P →Cal* P'"
    by simp
  from this simulation relation Cal_def show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
  proof (induct)
    case (WTS_refl P Cal)
    assume "(P, Q) ∈ Rel" and "Cal = STLCal Source Target"
    moreover have "Q →Cal* Q"
      using weakTauStep.WTS_refl[of Q Cal] .
    ultimately show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P, Q') ∈ Rel"
      by blast
  next
    case (WTS_trans P Cal P' P'')
    from WTS_trans(2)
    have IH: "strong_labelled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧ Cal = STLCal Source Target ⟹
              ∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
      by simp
    assume A1: "strong_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and A2: "Cal = STLCal Source Target"
    with IH obtain Q' where A3: "Q →(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
      by blast
    assume "P' ─τ-Cal→Cal P''"
    with A1 A2 A4 obtain β Q'' where A5: "Q' ─β→(STLCal Source Target) Q''"
                                 and A6: "(P'', Q'') ∈ Rel"
                                 and A7: "⟨P', τ-(STLCal Source Target)⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    from respection A2 A7 have "β = τ-(STLCal Source Target)"
      using encL_respects_internal_implies_iff_internal[of P' "τ-Cal" Q' β] internalST_iff_internal
      by simp
    with A3 A5 have "Q →(STLCal Source Target)* Q''"
      using weakTauStep.WTS_trans[of Q "STLCal Source Target" Q' Q'']
      by simp
    with A6 show "∃Q''. Q →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel"
      by blast
  qed
qed

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_preservation_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation:   "strong_labelled_simulation_encL Rel"
      and relation:     "(P, Q) ∈ Rel"
      and execution:    "P →(STLCal Source Target)* P'"
      and no_T_to_S:    "¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P →Cal* P'"
    by simp
  from this simulation relation no_T_to_S Cal_def
  show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
  proof (induct)
    case (WTS_refl P Cal)
    assume "(P, Q) ∈ Rel" and "Cal = STLCal Source Target"
    moreover have "Q →Cal* Q"
      using weakTauStep.WTS_refl[of Q Cal] .
    ultimately show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P, Q') ∈ Rel"
      by blast
  next
    case (WTS_trans P Cal P' P'')
    from WTS_trans(2)
    have IH: "strong_labelled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧ ¬(P ∈ ProcT ∧ Q ∈ ProcS) ∧
              Cal = STLCal Source Target ⟹ ∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
      by simp
    assume A1: "strong_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and A2: "¬(P ∈ ProcT ∧ Q ∈ ProcS)" and A3: "Cal = STLCal Source Target"
    with IH obtain Q' where A4: "Q →(STLCal Source Target)* Q'" and A5: "(P', Q') ∈ Rel"
      by blast
    assume "P' ─τ-Cal→Cal P''"
    with A1 A3 A5 obtain β Q'' where A6: "Q' ─β→(STLCal Source Target) Q''"
                                 and A7: "(P'', Q'') ∈ Rel"
                                 and A8: "⟨P', τ-(STLCal Source Target)⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    assume A9: "P →Cal* P'"
    have "β = τ-(STLCal Source Target)"
    proof (cases "P' ∈ ProcS")
      assume "P' ∈ ProcS"
      with preservation A3 A8 show "β = τ-(STLCal Source Target)"
        using encL_preserves_internal_implies_source_internal_to_internal[of P' Q' β]
              internalST_iff_internal
        by simp
    next
      assume "¬P' ∈ ProcS"
      hence B1: "P' ∈ ProcT"
        using source_or_target[of P']
        by blast
      with A3 A9 have "P ∈ ProcT"
        using weakTauStepsST_STLCal_weakTauSteps[of P P']
        by blast
      with A2 have "Q ∈ ProcT"
        using source_or_target[of Q]
        by blast
      with A4 have "Q' ∈ ProcT"
        using weakTauStepsST_STLCal_weakTauSteps[of Q Q']
        by blast
      hence B2: "¬⦇Q', β⦈↦⟨P', τ-STLCal⟩"
        using kinds_of_encoded_label(1)[of Q' β P' "τ-STLCal"]
        by blast
      from B1 have "¬⦇P', τ-STLCal⦈↦⟨Q', β⟩"
        using kinds_of_encoded_label(1)[of P' "τ-STLCal" Q' β]
        by blast
      with A8 B2 show "β = τ-(STLCal Source Target)"
        using related_labels_get_condition(1)[of P' "τ-STLCal" Q' β] internalST_iff_internal
        by simp
    qed
    with A4 A6 have "Q →(STLCal Source Target)* Q''"
      using weakTauStep.WTS_trans[of Q "STLCal Source Target" Q' Q'']
      by simp
    with A7 show "∃Q''. Q →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel"
      by blast
  qed
qed

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_reflection_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation: "strong_labelled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →(STLCal Source Target)* P'"
      and no_S_to_T:  "¬(P ∈ ProcS ∧ Q ∈ ProcT)"
      and reflection: "encL_reflects_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P →Cal* P'"
    by simp
  from this simulation relation no_S_to_T Cal_def
  show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
  proof (induct)
    case (WTS_refl P Cal)
    assume "(P, Q) ∈ Rel" and "Cal = STLCal Source Target"
    moreover have "Q →Cal* Q"
      using weakTauStep.WTS_refl[of Q Cal] .
    ultimately show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P, Q') ∈ Rel"
      by blast
  next
    case (WTS_trans P Cal P' P'')
    from WTS_trans(2)
    have IH: "strong_labelled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧ ¬(P ∈ ProcS ∧ Q ∈ ProcT) ∧
              Cal = STLCal Source Target ⟹ ∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
      by simp
    assume A1: "strong_labelled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and A2: "¬(P ∈ ProcS ∧ Q ∈ ProcT)" and A3: "Cal = STLCal Source Target"
    with IH obtain Q' where A4: "Q →(STLCal Source Target)* Q'" and A5: "(P', Q') ∈ Rel"
      by blast
    assume "P' ─τ-Cal→Cal P''"
    with A1 A3 A5 obtain β Q'' where A6: "Q' ─β→(STLCal Source Target) Q''"
                                 and A7: "(P'', Q'') ∈ Rel"
                                 and A8: "⟨P', τ-(STLCal Source Target)⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    assume A9: "P →Cal* P'"
    have "β = τ-(STLCal Source Target)"
    proof (cases "P' ∈ ProcS")
      assume B1: "P' ∈ ProcS"
      with A3 A9 have "P ∈ ProcS"
        using weakTauStepsST_STLCal_weakTauSteps[of P P']
        by blast
      with A2 have "Q ∈ ProcS"
        using source_or_target[of Q]
        by blast
      with A4 have "Q' ∈ ProcS"
        using weakTauStepsST_STLCal_weakTauSteps[of Q Q']
        by blast
      hence B2: "¬⦇P', τ-STLCal⦈↦⟨Q', β⟩"
        using kinds_of_encoded_label(3)[of P' "τ-STLCal" Q' β]
        by blast
      from B1 have "¬⦇Q', β⦈↦⟨P', τ-STLCal⟩"
        using kinds_of_encoded_label(3)[of Q' β P' "τ-STLCal"]
        by blast
      with A8 B2 show "β = τ-(STLCal Source Target)"
        using related_labels_get_condition(1)[of P' "τ-STLCal" Q' β] internalST_iff_internal
        by simp
    next
      assume "¬P' ∈ ProcS"
      hence "P' ∈ ProcT"
        using source_or_target[of P']
        by blast
      with reflection A3 A8 show "β = τ-(STLCal Source Target)"
        using encL_reflects_internal_implies_target_internal_to_internal[of P' Q' β]
              internalST_iff_internal
        by simp
    qed
    with A4 A6 have "Q →(STLCal Source Target)* Q''"
      using weakTauStep.WTS_trans[of Q "STLCal Source Target" Q' Q'']
      by simp
    with A7 show "∃Q''. Q →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel"
      by blast
  qed
qed

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_respection_weak_simulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes simulation: "strong_labelled_simulation_encL Rel"
      and respection: "encL_respects_internal"
  shows "weak_labelled_simulation_encL Rel"
proof clarify
  fix P Q α P'
  assume A1: "(P, Q) ∈ Rel" and A2: "P ─⁀α→(STLCal Source Target)* P'"
  show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
  proof (cases "α = τ-(STLCal Source Target)")
    assume B1: "α = τ-(STLCal Source Target)"
    with A2 have "P →(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      by simp
    with simulation respection A1 obtain Q' where B2: "Q →(STLCal Source Target)* Q'"
                                              and B3: "(P', Q') ∈ Rel"
      using strong_labelled_simulation_encL_and_respection_internal[of Rel P Q P']
      by blast
    from B2 have B4: "Q ─⁀(τ-(STLCal Source Target))→(STLCal Source Target)* Q'"
      unfolding weakLabelledStep_def
      by simp
    have "⟨P, α⟩ ≡⦇⦈ ⟨Q, τ-(STLCal Source Target)⟩"
      using source_or_target[of P] source_or_target[of Q]
    proof auto
      fix S S'
      from B1 show "⟨SourceTerm S, α⟩ ≡⦇⦈ ⟨SourceTerm S', τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    next
      fix S T
      from respection B1 have "⦇SourceTerm S, α⦈↦⟨TargetTerm T, τ-(STLCal Source Target)⟩"
        using internalST_iff_internal
        unfolding encLST_def getSourceLabel_def getTargetLabel_def
        by auto
      thus "⟨SourceTerm S, α⟩ ≡⦇⦈ ⟨TargetTerm T, τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    next
      fix T S
      from respection B1 have "⦇SourceTerm S, τ-(STLCal Source Target)⦈↦⟨TargetTerm T, α⟩"
        using internalST_iff_internal
        unfolding encLST_def getSourceLabel_def getTargetLabel_def
        by auto
      thus "⟨TargetTerm T, α⟩ ≡⦇⦈ ⟨SourceTerm S, τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    next
      fix T T'
      from B1 show "⟨TargetTerm T, α⟩ ≡⦇⦈ ⟨TargetTerm T', τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    qed
    with B3 B4 show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      by blast
  next
    assume B1: "α ≠ τ-(STLCal Source Target)"
    with A2 have "P ─α→(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      by simp
    with B1 obtain R S where B2: "P →(STLCal Source Target)* R"
      and B3: "R ─α→(STLCal Source Target) S" and B4: "S →(STLCal Source Target)* P'"
      unfolding weakLabelledActionStep_def
      by blast
    from simulation respection A1 B2 obtain Q' where B5: "Q →(STLCal Source Target)* Q'"
                                                 and B6: "(R, Q') ∈ Rel"
      using strong_labelled_simulation_encL_and_respection_internal[of Rel P Q R]
      by blast
    from simulation B3 B6 obtain β Q'' where B7: "Q' ─β→(STLCal Source Target) Q''"
                                         and B8: "(S, Q'') ∈ Rel" and B9: "⟨R, α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    from simulation respection B4 B8 obtain Q''' where B10: "Q'' →(STLCal Source Target)* Q'''"
                                                   and B11: "(P', Q''') ∈ Rel"
      using strong_labelled_simulation_encL_and_respection_internal[of Rel S Q'' P']
      by blast
    from respection B1 B9 have B12: "β ≠ τ-(STLCal Source Target)"
      using encL_respects_internal_implies_iff_internal[of R α Q' β] internalST_iff_internal
      by simp
    with B5 B7 B10 have "Q ─β→(STLCal Source Target)* Q'''"
      unfolding weakLabelledActionStep_def
      by blast
    with B12 have B13: "Q ─⁀β→(STLCal Source Target)* Q'''"
      unfolding weakLabelledStep_def
      by simp
    from B2 have B14: "R ∼ST P"
      using weakTauStepsST_STLCal_weakTauSteps[of P R]
      by blast
    from B5 have "Q' ∼ST Q"
      using weakTauStepsST_STLCal_weakTauSteps[of Q Q']
      by blast
    with B9 B14 have "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      using related_labels_exchange_processes[of R α Q' β P Q]
      by simp
    with B11 B13
    show "∃β Q'''. Q ─⁀β→(STLCal Source Target)* Q''' ∧ (P', Q''') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      by blast
  qed
qed

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_preservation_weak_simulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes simulation:   "strong_labelled_simulation_encL Rel"
      and no_T_to_S:    "∀P Q. (P, Q) ∈ Rel ⟶ ¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
  shows "weak_labelled_simulation_encL Rel"
proof clarify
  fix P Q α P'
  assume A1: "(P, Q) ∈ Rel" and A2: "P ─⁀α→(STLCal Source Target)* P'"
  show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
  proof (cases "α = τ-(STLCal Source Target)")
    assume B1: "α = τ-(STLCal Source Target)"
    with A2 have "P →(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      by simp
    with simulation no_T_to_S preservation A1 obtain Q' where B2: "Q →(STLCal Source Target)* Q'"
                                                          and B3: "(P', Q') ∈ Rel"
      using strong_labelled_simulation_encL_and_preservation_internal[of Rel P Q P']
      by blast
    from B2 have B4: "Q ─⁀(τ-(STLCal Source Target))→(STLCal Source Target)* Q'"
      unfolding weakLabelledStep_def
      by simp
    have "⟨P, α⟩ ≡⦇⦈ ⟨Q, τ-(STLCal Source Target)⟩"
      using source_or_target[of P] source_or_target[of Q]
    proof auto
      fix S S'
      from B1 show "⟨SourceTerm S, α⟩ ≡⦇⦈ ⟨SourceTerm S', τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    next
      fix S T
      from preservation B1 have "⦇SourceTerm S, α⦈↦⟨TargetTerm T, τ-(STLCal Source Target)⟩"
        using internalST_iff_internal
        unfolding encLST_def getSourceLabel_def getTargetLabel_def
        by auto
      thus "⟨SourceTerm S, α⟩ ≡⦇⦈ ⟨TargetTerm T, τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    next
      fix T S
      assume "T ∈T P" and "S ∈S Q"
      with no_T_to_S A1 have False
        by blast
      thus "⟨TargetTerm T, α⟩ ≡⦇⦈ ⟨SourceTerm S, τ-(STLCal Source Target)⟩"
        by simp
    next
      fix T T'
      from B1 show "⟨TargetTerm T, α⟩ ≡⦇⦈ ⟨TargetTerm T', τ-(STLCal Source Target)⟩"
        unfolding related_labels_def
        by simp
    qed
    with B3 B4 show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      by blast
  next
    assume B1: "α ≠ τ-(STLCal Source Target)"
    with A2 have "P ─α→(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      by simp
    with B1 obtain R S where B2: "P →(STLCal Source Target)* R"
      and B3: "R ─α→(STLCal Source Target) S" and B4: "S →(STLCal Source Target)* P'"
      unfolding weakLabelledActionStep_def
      by blast
    from simulation no_T_to_S preservation A1 B2 obtain Q' where
      B5: "Q →(STLCal Source Target)* Q'" and B6: "(R, Q') ∈ Rel"
      using strong_labelled_simulation_encL_and_preservation_internal[of Rel P Q R]
      by blast
    from simulation B3 B6 obtain β Q'' where B7: "Q' ─β→(STLCal Source Target) Q''"
                                         and B8: "(S, Q'') ∈ Rel" and B9: "⟨R, α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    from simulation no_T_to_S preservation B4 B8 obtain Q''' where
      B10: "Q'' →(STLCal Source Target)* Q'''" and B11: "(P', Q''') ∈ Rel"
      using strong_labelled_simulation_encL_and_preservation_internal[of Rel S Q'' P']
      by blast
    have B12: "Q ─⁀β→(STLCal Source Target)* Q'''"
    proof (cases "β = τ-(STLCal Source Target)")
      assume C: "β = τ-(STLCal Source Target)"
      with B5 B7 have "Q →(STLCal Source Target)* Q''"
        using WTS_trans[of Q "STLCal Source Target" Q' Q'']
        by simp
      with B10 have "Q →(STLCal Source Target)* Q'''"
        using weakTauStepsST_trans[of Q Q'' Q'''] weakTauStepsST_STLCal_weakTauSteps[of Q Q'']
              weakTauStepsST_STLCal_weakTauSteps[of Q'' Q''']
              weakTauStepsST_STLCal_weakTauSteps[of Q Q''']
        by simp
      with C show "Q ─⁀β→(STLCal Source Target)* Q'''"
        unfolding weakLabelledStep_def
        by simp
    next
      assume C: "β ≠ τ-(STLCal Source Target)"
      with B5 B7 B10 have "Q ─β→(STLCal Source Target)* Q'''"
        unfolding weakLabelledActionStep_def
        by blast
      with C show "Q ─⁀β→(STLCal Source Target)* Q'''"
        unfolding weakLabelledStep_def
        by simp
    qed
    from B2 have B13: "R ∼ST P"
      using weakTauStepsST_STLCal_weakTauSteps[of P R]
      by blast
    from B5 have "Q' ∼ST Q"
      using weakTauStepsST_STLCal_weakTauSteps[of Q Q']
      by blast
    with B9 B13 have "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      using related_labels_exchange_processes[of R α Q' β P Q]
      by simp
    with B11 B12
    show "∃β Q'''. Q ─⁀β→(STLCal Source Target)* Q''' ∧ (P', Q''') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      by blast
  qed
qed

text ‹The reflexive closure of a strong simulation is a strong simulation. If the label encoding
      is injective, then also the transitive closure of a strong simulation is a strong simulation
      on encoded labels.›

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes simulation: "strong_labelled_simulation_encL Rel"
  shows "strong_labelled_simulation_encL (Rel⇧=)"
  using assms
proof auto
  fix P Q α P'
  assume "strong_labelled_simulation_encL Rel" and "P ─α→(STLCal Source Target) P'"
     and "(P, Q) ∈ Rel"
  hence "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
  thus "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix Q α P'
  assume "Q ─α→(STLCal Source Target) P'"
  moreover have "Q ∼ST Q"
    using source_or_target[of Q]
    by presburger
  hence "⟨Q, α⟩ ≡⦇⦈ ⟨Q, α⟩"
    unfolding related_labels_def
    by simp
  ultimately
  show "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨Q, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) strong_labelled_simulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes simulation: "strong_labelled_simulation_encL Rel"
      and injective:  "inj encL"
    shows "strong_labelled_simulation_encL (Rel⇧=)"
      and "strong_labelled_simulation_encL (Rel⇧+)"
      and "strong_labelled_simulation_encL (Rel⇧*)"
proof -
  from simulation show A1: "strong_labelled_simulation_encL (Rel⇧=)"
    using strong_labelled_simulation_encL_and_refl_closure[of Rel]
    by simp
  have A2: "⋀Rel. strong_labelled_simulation_encL Rel ⟹ strong_labelled_simulation_encL (Rel⇧+)"
  proof clarify
    fix Rel P Q α P'
    assume B: "strong_labelled_simulation_encL Rel"
    assume "(P, Q) ∈ Rel⇧+" and "P ─α→(STLCal Source Target) P'"
    thus "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ─α→(STLCal Source Target) P'"
      with B obtain β Q' where "Q ─β→(STLCal Source Target) Q'" and "(P', Q') ∈ Rel"
                           and "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
      thus "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ─α→(STLCal Source Target) P' ⟹
              (∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
         and "P ─α→(STLCal Source Target) P'"
      from this obtain β Q' where C1: "Q ─β→(STLCal Source Target) Q'" and C2: "(P', Q') ∈ Rel⇧+"
                              and C3: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
      assume "(Q, R) ∈ Rel"
      with B C1 obtain γ R' where C4: "R ─γ→(STLCal Source Target) R'" and C5: "(Q', R') ∈ Rel⇧+"
                              and C6: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
        by blast
      from C2 C5 have C7: "(P', R') ∈ Rel⇧+"
        by simp
      from injective C3 C6 have "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        using related_labels_trans_inj[of P α Q β R γ]
        by simp
      with C4 C7
      show "∃γ R'. R ─γ→(STLCal Source Target) R' ∧ (P', R') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        by blast
    qed
  qed
  with simulation show "strong_labelled_simulation_encL (Rel⇧+)"
    by blast
  from simulation A1 A2[of "Rel⇧="] show "strong_labelled_simulation_encL (Rel⇧*)"
      using trancl_reflcl[of Rel]
    by fast
qed

subsection ‹Contrasimulation›

text ‹A weak labelled contrasimulation on encoded labels is relation R such that if (P, Q) in R
      and P evolves to some P' using word w of labels then there exists some v and Q' such that Q
      evolves to Q' using v, (Q', P') in R, and w and v are related words.›

abbreviation (in encodingLS_encL) weak_labelled_contrasimulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "weak_labelled_contrasimulation_encL Rel ≡
   ∀P Q w P'. (P, Q) ∈ Rel ∧ P ─⌢w→(STLCal Source Target)* P' ⟶
   (∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (Q', P') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩)"

text ‹The reflexive closure of a weak contrasimulation on encoded words is a weak contrasimulation.
      For the transitive closure we require again that the label encoding is injective.›

lemma (in encodingLS_encL) weak_labelled_contrasimulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes contrasimulation: "weak_labelled_contrasimulation_encL Rel"
  shows "weak_labelled_contrasimulation_encL (Rel⇧=)"
  using assms
proof auto
  fix P Q w P'
  assume "weak_labelled_contrasimulation_encL Rel" and "P ─⌢w→(STLCal Source Target)* P'"
     and "(P, Q) ∈ Rel"
  hence "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (Q', P') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    by simp
  thus "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ ((Q', P') ∈ Rel ∨ Q' = P') ∧
        ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    by blast
next
  fix Q w P'
  assume "Q ─⌢w→(STLCal Source Target)* P'"
  moreover have "Q ∼ST Q"
    using source_or_target[of Q]
    by presburger
  hence "⟨Q, w⟩ ≡⦇⦈* ⟨Q, w⟩"
    unfolding related_words_def
    by simp
  ultimately show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ ((Q', P') ∈ Rel ∨ Q' = P') ∧
                   ⟨Q, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_contrasimulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes contrasimulation: "weak_labelled_contrasimulation_encL Rel"
      and injective:        "inj encL"
    shows "weak_labelled_contrasimulation_encL (Rel⇧=)"
      and "weak_labelled_contrasimulation_encL (Rel⇧+)"
      and "weak_labelled_contrasimulation_encL (Rel⇧*)"
proof -
  from contrasimulation show A1: "weak_labelled_contrasimulation_encL (Rel⇧=)"
    using weak_labelled_contrasimulation_encL_and_refl_closure[of Rel]
    by simp
  have A2: "⋀Rel. weak_labelled_contrasimulation_encL Rel ⟹
            weak_labelled_contrasimulation_encL (Rel⇧+)"
  proof clarify
    fix Rel P Q w P'
    assume B1: "weak_labelled_contrasimulation_encL Rel"
    assume "(P, Q) ∈ Rel⇧+" and "P ─⌢w→(STLCal Source Target)* P'"
    thus "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (Q', P') ∈ Rel⇧+ ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    proof (induct arbitrary: P')
      fix Q P'
      assume "(P, Q) ∈ Rel" and "P ─⌢w→(STLCal Source Target)* P'"
      with B1 obtain v Q' where "Q ─⌢v→(STLCal Source Target)* Q'" and "(Q', P') ∈ Rel"
                            and "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
        by blast
      thus "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (Q', P') ∈ Rel⇧+ ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
        by auto
    next
      case (step Q R P')
      assume "⋀P'. P ─⌢w→(STLCal Source Target)* P' ⟹
              (∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (Q', P') ∈ Rel⇧+ ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩)"
         and C1: "P ─⌢w→(STLCal Source Target)* P'"
      from this obtain v Q' where C2: "Q ─⌢v→(STLCal Source Target)* Q'"
                              and C3: "(Q', P') ∈ Rel⇧+" and C4: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
        by blast
      assume "(Q, R) ∈ Rel"
      with B1 C2 obtain y R' where C5: "R ─⌢y→(STLCal Source Target)* R'"
                               and C6: "(R', Q') ∈ Rel⇧+" and C7: "⟨Q, v⟩ ≡⦇⦈* ⟨R, y⟩"
        by blast
      from C3 C6 have C8: "(R', P') ∈ Rel⇧+"
        by simp
      from injective C4 C7 have "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        using related_words_trans_inj[of P w Q v R y]
        by simp
      with C5 C8
      show "∃y R'. R ─⌢y→(STLCal Source Target)* R' ∧ (R', P') ∈ Rel⇧+ ∧ ⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        by blast
    qed
  qed
  with contrasimulation show "weak_labelled_contrasimulation_encL (Rel⇧+)"
    by blast
  from contrasimulation A1 A2[of"Rel⇧="] show "weak_labelled_contrasimulation_encL (Rel⇧*)"
    using trancl_reflcl[of Rel]
    by fast
qed

subsection ‹Coupled Simulation›

text ‹A weak labelled coupled simulation on encoded labels is relation R such that if (P, Q) in R
      and P evolves to some P' using label a then there exists some Q' such that Q evolves to Q'
      using some b, (P', Q') in R, and a and b are related (simulation) and there exits some Q'
      such that Q evolves to Q' and (Q', P) in R (coupling).›

abbreviation (in encodingLS_encL) weak_labelled_coupled_simulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "weak_labelled_coupled_simulation_encL Rel ≡
   ∀P Q. (P, Q) ∈ Rel ⟶
   ((∀α P'. P ─⁀α→(STLCal Source Target)* P' ⟶
    (∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)) ∧
   (∃Q'. Q →(STLCal Source Target)* Q' ∧ (Q', P) ∈ Rel))"

text ‹A weak labelled coupled simulation simulates words of labels including the empty word, if the
      label encoding respects the internal. The requirement on the respection of internals can be
      relaxed similar to the case of weak labelled simulation on encoded labels.›

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_respection_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation: "weak_labelled_coupled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →(STLCal Source Target)* P'"
      and respection: "encL_respects_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-STLCal→(STLCal Source Target)* P'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'"
                                         and A2: "(P', Q') ∈ Rel" and A3: "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  from respection A3 have "β = τ-STLCal"
    using encL_respects_internal_implies_iff_internal[of P "τ-STLCal" Q β]
    by blast
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_preservation_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation:   "weak_labelled_coupled_simulation_encL Rel"
      and relation:     "(P, Q) ∈ Rel"
      and execution:    "P →(STLCal Source Target)* P'"
      and no_T_to_S:    "¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-STLCal→(STLCal Source Target)* P'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'"
                                         and A2: "(P', Q') ∈ Rel" and A3: "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  have "β = τ-STLCal"
  proof (cases "P ∈ ProcS")
    assume "P ∈ ProcS"
    with preservation A3 show "β = τ-STLCal"
      using encL_preserves_internal_implies_source_internal_to_internal[of P Q β]
      by simp
  next
    assume "¬P ∈ ProcS"
    with no_T_to_S have B1: "P ∼ST Q"
      using source_or_target[of P] source_or_target[of Q]
      by blast
    hence B2: "¬⦇P, τ-STLCal⦈↦⟨Q, β⟩"
      using kinds_of_encoded_label(1, 3)[of P "τ-STLCal" Q β]
      by blast
    from B1 have "¬⦇Q, β⦈↦⟨P, τ-STLCal⟩"
      using kinds_of_encoded_label(1, 3)[of Q β P "τ-STLCal"]
      by blast
    with A3 B2 show "β = τ-STLCal"
      using related_labels_get_condition(1)[of P "τ-STLCal" Q β]
      by simp
  qed
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_reflection_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
  assumes simulation: "weak_labelled_coupled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P →(STLCal Source Target)* P'"
      and no_S_to_T:  "¬(P ∈ ProcS ∧ Q ∈ ProcT)"
      and reflection: "encL_reflects_internal"
    shows "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
proof -
  from execution have "P ─⁀τ-STLCal→(STLCal Source Target)* P'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with simulation relation obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'"
                                         and A2: "(P', Q') ∈ Rel" and A3: "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  have "β = τ-STLCal"
  proof (cases "P ∈ ProcS")
    assume "P ∈ ProcS"
    with no_S_to_T have B1: "P ∼ST Q"
      using source_or_target[of P] source_or_target[of Q]
      by blast
    hence B2: "¬⦇P, τ-STLCal⦈↦⟨Q, β⟩"
      using kinds_of_encoded_label(1, 3)[of P "τ-STLCal" Q β]
      by blast
    from B1 have "¬⦇Q, β⦈↦⟨P, τ-STLCal⟩"
      using kinds_of_encoded_label(1, 3)[of Q β P "τ-STLCal"]
      by blast
    with A3 B2 show "β = τ-STLCal"
      using related_labels_get_condition(1)[of P "τ-STLCal" Q β]
      by simp
  next
    assume "¬P ∈ ProcS"
    hence "P ∈ ProcT"
      using source_or_target[of P]
      by simp
    with reflection A3 show "β = τ-STLCal"
      using encL_reflects_internal_implies_target_internal_to_internal[of P Q β]
      by simp
  qed
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internalST_iff_internal
    unfolding weakLabelledStep_def
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_respection_word:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
    and w v    :: "('labS, 'labT) Lab list"
  assumes simulation: "weak_labelled_coupled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P ─⌢w→(STLCal Source Target)* P'"
      and respection: "encL_respects_internal"
    shows "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P ─⌢w→Cal* P'"
    by simp
  from this simulation relation respection Cal_def
  show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  proof (induct arbitrary: v)
    case (WLS_Nil P Cal P')
    assume "P →Cal* P'" and "Cal = STLCal Source Target"
    hence "P →(STLCal Source Target)* P'"
      by simp
    moreover assume "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
                and "encL_respects_internal"
    ultimately obtain Q' where A1: "Q →(STLCal Source Target)* Q'" and A2: "(P', Q') ∈ Rel"
      using weak_labelled_simulation_encL_and_respection_internal[of Rel P Q P']
      by blast
    from A1 have A3: "Q ─⌢[]→(STLCal Source Target)* Q'"
      using weakLabelledSequence.WLS_Nil[of Q "STLCal Source Target" Q']
      by simp
    have "⟨P, []⟩ ≡⦇⦈* ⟨Q, []⟩"
      using ELNil[of P Q] ELNil[of Q P] source_or_target[of P] source_or_target[of Q]
      unfolding related_words_def
      by auto
    with A2 A3
      show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  next
    case (WLS_Cons P w Cal P' α P'')
    from WLS_Cons(2) have IH: "weak_labelled_coupled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧
      encL_respects_internal ∧ Cal = STLCal Source Target ⟹
      ∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by simp
    assume A1: "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and "encL_respects_internal" and A2: "Cal = STLCal Source Target"
    with IH obtain v Q' where A3: "Q ─⌢v→(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
                          and A5: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
    assume "P' ─⁀α→Cal* P''"
    with A1 A2 A4 obtain β Q'' where A6: "Q' ─⁀β→(STLCal Source Target)* Q''"
                                 and A7: "(P'', Q'') ∈ Rel" and A8: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    with A3 A6 have A9: "Q ─⌢(v@[β])→(STLCal Source Target)* Q''"
      using weakLabelledSequence.WLS_Cons[of Q v "STLCal Source Target" Q' β Q'']
      by simp
    assume "P ─⌢w→Cal* P'"
    with A2 have A10: "P ∼ST P'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
      by blast
    from A3 have "Q ∼ST Q'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q v Q']
      by blast
    with A5 A8 A10 have "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
      using related_words_compose[of P w Q v P' α Q' β]
      by simp
    with A7 A9
    show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, w@[α]⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  qed
qed

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_preservation_word:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
    and w v    :: "('labS, 'labT) Lab list"
  assumes simulation:   "weak_labelled_coupled_simulation_encL Rel"
      and relation:     "(P, Q) ∈ Rel"
      and execution:    "P ─⌢w→(STLCal Source Target)* P'"
      and no_T_to_S:    "¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
    shows "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P ─⌢w→Cal* P'"
    by simp
  from this simulation relation no_T_to_S preservation Cal_def
  show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  proof (induct arbitrary: v)
    case (WLS_Nil P Cal P')
    assume "P →Cal* P'" and "Cal = STLCal Source Target"
    hence "P →(STLCal Source Target)* P'"
      by simp
    moreover assume "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
                and "¬(P ∈ ProcT ∧ Q ∈ ProcS)" and "encL_preserves_internal"
    ultimately obtain Q' where A1: "Q →(STLCal Source Target)* Q'" and A2: "(P', Q') ∈ Rel"
      using weak_labelled_simulation_encL_and_preservation_internal[of Rel P Q P']
      by blast
    from A1 have A3: "Q ─⌢[]→(STLCal Source Target)* Q'"
      using weakLabelledSequence.WLS_Nil[of Q "STLCal Source Target" Q']
      by simp
    have "⟨P, []⟩ ≡⦇⦈* ⟨Q, []⟩"
      using ELNil[of P Q] ELNil[of Q P] source_or_target[of P] source_or_target[of Q]
      unfolding related_words_def
      by auto
    with A2 A3
    show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  next
    case (WLS_Cons P w Cal P' α P'')
    from WLS_Cons(2) have IH: "weak_labelled_coupled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧
      ¬(P ∈ ProcT ∧ Q ∈ ProcS) ∧ encL_preserves_internal ∧ Cal = STLCal Source Target ⟹
      ∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by simp
    assume A1: "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and "¬(P ∈ ProcT ∧ Q ∈ ProcS)" and "encL_preserves_internal"
       and A2: "Cal = STLCal Source Target"
    with IH obtain v Q' where A3: "Q ─⌢v→(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
                          and A5: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
    assume "P' ─⁀α→Cal* P''"
    with A1 A2 A4 obtain β Q'' where A6: "Q' ─⁀β→(STLCal Source Target)* Q''"
                                 and A7: "(P'', Q'') ∈ Rel" and A8: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    with A3 A6 have A9: "Q ─⌢(v@[β])→(STLCal Source Target)* Q''"
      using weakLabelledSequence.WLS_Cons[of Q v "STLCal Source Target" Q' β Q'']
      by simp
    assume "P ─⌢w→Cal* P'"
    with A2 have A10: "P ∼ST P'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
      by blast
    from A3 have "Q ∼ST Q'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q v Q']
      by blast
    with A5 A8 A10 have "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
      using related_words_compose[of P w Q v P' α Q' β]
      by simp
    with A7 A9
    show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, w@[α]⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  qed
qed

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_reflection_word:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q P' :: "('procS, 'procT) Proc"
    and w v    :: "('labS, 'labT) Lab list"
  assumes simulation: "weak_labelled_coupled_simulation_encL Rel"
      and relation:   "(P, Q) ∈ Rel"
      and execution:  "P ─⌢w→(STLCal Source Target)* P'"
      and no_S_to_T:  "¬(P ∈ ProcS ∧ Q ∈ ProcT)"
      and reflection: "encL_reflects_internal"
    shows "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with execution have "P ─⌢w→Cal* P'"
    by simp
  from this simulation relation no_S_to_T reflection Cal_def
  show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  proof (induct arbitrary: v)
    case (WLS_Nil P Cal P')
    assume "P →Cal* P'" and "Cal = STLCal Source Target"
    hence "P →(STLCal Source Target)* P'"
      by simp
    moreover assume "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
                and "¬(P ∈ ProcS ∧ Q ∈ ProcT)" and "encL_reflects_internal"
    ultimately obtain Q' where A1: "Q →(STLCal Source Target)* Q'" and A2: "(P', Q') ∈ Rel"
      using weak_labelled_simulation_encL_and_reflection_internal[of Rel P Q P']
      by blast
    from A1 have A3: "Q ─⌢[]→(STLCal Source Target)* Q'"
      using weakLabelledSequence.WLS_Nil[of Q "STLCal Source Target" Q']
      by simp
    have "⟨P, []⟩ ≡⦇⦈* ⟨Q, []⟩"
      using ELNil[of P Q] ELNil[of Q P] source_or_target[of P] source_or_target[of Q]
      unfolding related_words_def
      by auto
    with A2 A3
    show "∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  next
    case (WLS_Cons P w Cal P' α P'')
    from WLS_Cons(2) have IH: "weak_labelled_coupled_simulation_encL Rel ∧ (P, Q) ∈ Rel ∧
      ¬(P ∈ ProcS ∧ Q ∈ ProcT) ∧ encL_reflects_internal ∧ Cal = STLCal Source Target ⟹
      ∃v Q'. Q ─⌢v→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by simp
    assume A1: "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
       and "¬(P ∈ ProcS ∧ Q ∈ ProcT)" and "encL_reflects_internal"
       and A2: "Cal = STLCal Source Target"
    with IH obtain v Q' where A3: "Q ─⌢v→(STLCal Source Target)* Q'" and A4: "(P', Q') ∈ Rel"
                          and A5: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
    assume "P' ─⁀α→Cal* P''"
    with A1 A2 A4 obtain β Q'' where A6: "Q' ─⁀β→(STLCal Source Target)* Q''"
                                 and A7: "(P'', Q'') ∈ Rel" and A8: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      by blast
    with A3 A6 have A9: "Q ─⌢(v@[β])→(STLCal Source Target)* Q''"
      using weakLabelledSequence.WLS_Cons[of Q v "STLCal Source Target" Q' β Q'']
      by simp
    assume "P ─⌢w→Cal* P'"
    with A2 have A10: "P ∼ST P'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
      by blast
    from A3 have "Q ∼ST Q'"
      using weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q v Q']
      by blast
    with A5 A8 A10 have "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
      using related_words_compose[of P w Q v P' α Q' β]
      by simp
    with A7 A9
    show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, w@[α]⟩ ≡⦇⦈* ⟨Q, v⟩"
      by blast
  qed
qed

text ‹A weak coupled simulation combines the conditions on a weak simulation and a weak
      contrasimulation, if the label encoding respects the internal. Instead of respection of the
      internal we can require instead preservation and that the coupled simulation does not relate
      a target term and a source term.›

lemma (in encodingLS_encL)
  wl_coupled_simulation_encL_and_respection_versus_simulation_and_contrasimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes respection: "encL_respects_internal"
  shows "weak_labelled_coupled_simulation_encL Rel
         = (weak_labelled_simulation_encL Rel ∧ weak_labelled_contrasimulation_encL Rel)"
proof auto
  fix P Q w P'
  assume A1: "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
     and "P ─⌢w→(STLCal Source Target)* P'"
  with respection obtain v Q' where A2: "Q ─⌢v→(STLCal Source Target)* Q'"
                                and A3: "(P', Q') ∈ Rel" and A4: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    using weak_labelled_coupled_simulation_encL_and_respection_word[of Rel P Q w P']
    by blast
  from A1 A3 obtain Q'' where A5: "Q' →(STLCal Source Target)* Q''" and A6: "(Q'', P') ∈ Rel"
    by blast
  from A2 A5 have "Q ─⌢v→(STLCal Source Target)* Q''"
    using weakLabelledSequence_extend_by_internal[of Q v "STLCal Source Target" Q' Q'']
    by simp
  with A4 A6
  show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (Q'', P') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    by blast
next
  fix P Q
  assume "weak_labelled_contrasimulation_encL Rel" and "(P, Q) ∈ Rel"
  moreover have "P ─⌢[]→(STLCal Source Target)* P"
    using WTS_refl[of P "STLCal Source Target"] WLS_Nil[of P "STLCal Source Target" P]
    by simp
  ultimately obtain v Q' where A1: "Q ─⌢v→(STLCal Source Target)* Q'" and A2: "(Q', P) ∈ Rel"
                           and A3: "⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
    by blast
  from A3 have "v = []"
    using related_words_length[of P "[]" Q v]
    by simp
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internal_weakLabelledSequence[of Q "STLCal Source Target" Q']
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (Q', P) ∈ Rel"
    by blast
qed

lemma (in encodingLS_encL)
  wl_coupled_simulation_encL_and_preservation_versus_simulation_and_contrasimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes no_T_to_S:    "∀P Q. (P, Q) ∈ Rel ⟶ ¬(P ∈ ProcT ∧ Q ∈ ProcS)"
      and preservation: "encL_preserves_internal"
  shows "weak_labelled_coupled_simulation_encL Rel
         = (weak_labelled_simulation_encL Rel ∧ weak_labelled_contrasimulation_encL Rel)"
proof auto
  fix P Q w P'
  assume A1: "weak_labelled_coupled_simulation_encL Rel" and "(P, Q) ∈ Rel"
     and "P ─⌢w→(STLCal Source Target)* P'"
  with no_T_to_S preservation obtain v Q' where A2: "Q ─⌢v→(STLCal Source Target)* Q'"
                                            and A3: "(P', Q') ∈ Rel" and A4: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    using weak_labelled_coupled_simulation_encL_and_preservation_word[of Rel P Q w P']
    by blast
  from A1 A3 obtain Q'' where A5: "Q' →(STLCal Source Target)* Q''" and A6: "(Q'', P') ∈ Rel"
    by blast
  from A2 A5 have "Q ─⌢v→(STLCal Source Target)* Q''"
    using weakLabelledSequence_extend_by_internal[of Q v "STLCal Source Target" Q' Q'']
    by simp
  with A4 A6
  show "∃v Q''. Q ─⌢v→(STLCal Source Target)* Q'' ∧ (Q'', P') ∈ Rel ∧ ⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
    by blast
next
  fix P Q
  assume "weak_labelled_contrasimulation_encL Rel" and "(P, Q) ∈ Rel"
  moreover have "P ─⌢[]→(STLCal Source Target)* P"
    using WTS_refl[of P "STLCal Source Target"] WLS_Nil[of P "STLCal Source Target" P]
    by simp
  ultimately obtain v Q' where A1: "Q ─⌢v→(STLCal Source Target)* Q'" and A2: "(Q', P) ∈ Rel"
                           and A3: "⟨P, []⟩ ≡⦇⦈* ⟨Q, v⟩"
    by blast
  from A3 have "v = []"
    using related_words_length[of P "[]" Q v]
    by simp
  with A1 have "Q →(STLCal Source Target)* Q'"
    using internal_weakLabelledSequence[of Q "STLCal Source Target" Q']
    by simp
  with A2 show "∃Q'. Q →(STLCal Source Target)* Q' ∧ (Q', P) ∈ Rel"
    by blast
qed

text ‹The reflexive and/or transitive closure of a weak coupled simulation is a weak coupled
      simulation, where we need for transitivity that the label encoding is injective and preserves
      the internal. Injectivity is necessary to combine the labels and the preservation of the
      internal is necessary to simulation internal steps.›

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes coupledSimulation: "weak_labelled_coupled_simulation_encL Rel"
  shows "weak_labelled_coupled_simulation_encL (Rel⇧=)"
proof auto
  fix P Q α P'
  assume "P ─⁀α→(STLCal Source Target)* P'" and "(P, Q) ∈ Rel"
  with coupledSimulation
  have "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
  thus "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix P Q
  assume "(P, Q) ∈ Rel"
  with coupledSimulation have "∃Q'. Q →(STLCal Source Target)* Q' ∧ (Q', P) ∈ Rel"
    by simp
  thus "∃Q'. Q →(STLCal Source Target)* Q' ∧ ((Q', P) ∈ Rel ∨ Q' = P)"
    by blast
next
  fix Q α P'
  assume "Q ─⁀α→(STLCal Source Target)* P'"
  moreover have "Q ∼ST Q"
    using source_or_target[of Q]
    by presburger
  hence "⟨Q, α⟩ ≡⦇⦈ ⟨Q, α⟩"
    unfolding related_labels_def
    by simp
  ultimately
  show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨Q, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix Q
  have "Q →(STLCal Source Target)* Q"
    using WTS_refl[of Q "STLCal Source Target"]
    by simp
  thus "∃Q'. Q →(STLCal Source Target)* Q' ∧ ((Q', Q) ∈ Rel ∨ Q' = Q)"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_coupled_simulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes coupledSimulation: "weak_labelled_coupled_simulation_encL Rel"
      and injective:         "inj encL"
      and preserves:         "encL_preserves_internal"
    shows "weak_labelled_coupled_simulation_encL (Rel⇧=)"
      and "weak_labelled_coupled_simulation_encL (Rel⇧+)"
      and "weak_labelled_coupled_simulation_encL (Rel⇧*)"
proof -
  from injective preserves have A1: "encL_respects_internal"
    using inj_preserves_is_respects_internal
    by blast
  with coupledSimulation have A2: "weak_labelled_simulation_encL Rel"
                          and A3: "weak_labelled_contrasimulation_encL Rel"
    using wl_coupled_simulation_encL_and_respection_versus_simulation_and_contrasimulation[of
            "Rel"]
    by simp_all
  from injective preserves A2 have A4: "weak_labelled_simulation_encL (Rel⇧=)"
                               and A5: "weak_labelled_simulation_encL (Rel⇧+)"
                               and A6: "weak_labelled_simulation_encL (Rel⇧*)"
    using weak_labelled_simulation_encL_and_closures[of "Rel"]
    by simp_all
  from injective preserves A3 have A7: "weak_labelled_contrasimulation_encL (Rel⇧=)"
                               and A8: "weak_labelled_contrasimulation_encL (Rel⇧+)"
                               and A9: "weak_labelled_contrasimulation_encL (Rel⇧*)"
    using weak_labelled_contrasimulation_encL_and_closures[of "Rel"]
    by simp_all
  from A1 A4 A7 show "weak_labelled_coupled_simulation_encL (Rel⇧=)"
    using wl_coupled_simulation_encL_and_respection_versus_simulation_and_contrasimulation[of
            "Rel⇧="]
    by simp
  from A1 A5 A8 show "weak_labelled_coupled_simulation_encL (Rel⇧+)"
    using wl_coupled_simulation_encL_and_respection_versus_simulation_and_contrasimulation[of
            "Rel⇧+"]
    by simp
  from A1 A6 A9 show "weak_labelled_coupled_simulation_encL (Rel⇧*)"
    using wl_coupled_simulation_encL_and_respection_versus_simulation_and_contrasimulation[of
            "Rel⇧*"]
    by simp
qed

subsection ‹Correspondence Simulation›

text ‹A weak labelled correspondence simulation on encoded labels is relation R such that
      (1) if (P, Q) in R and P evolves to some P' using label a then there exist b and Q' such that
          Q evolves to Q' using b, (P', Q') in R, and a and b are related, and
      (2) if (P, Q) in R and Q evolves to some Q' using label a then there exist b, P'', and Q''
          such that P evolves to P'' using b and Q' evolves to Q'' using only internal steps,
          (P'', Q'') in R, and a and b are related.›

abbreviation (in encodingLS_encL) weak_labelled_correspondence_simulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "weak_labelled_correspondence_simulation_encL Rel ≡
   (∀P Q α P'. (P, Q) ∈ Rel ∧ P ─⁀α→(STLCal Source Target)* P' ⟶
    (∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩))
   ∧ (∀P Q β Q'. (P, Q) ∈ Rel ∧ Q ─⁀β→(STLCal Source Target)* Q'
      ⟶ (∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧ Q' →(STLCal Source Target)* Q'' ∧
           (P'', Q'') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩))"

text ‹The reflexive and/or transitive closure of a weak correspondence simulation is a weak
      correspondence simulation, where for transitivity we need again that the label encoding is
      injective and preserves the internal.›

lemma (in encodingLS_encL) labelled_correspondence_simulation_encL_condition_trans:
  fixes P Q R :: "('procS, 'procT) Proc"
    and Rel   :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes A1:  "∀β Q'. Q ─⁀β→(STLCal Source Target)* Q' ⟶
                (∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧
                 Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
      and A2:  "∀γ R'. R ─⁀γ→(STLCal Source Target)* R' ⟶
                (∃β Q'' R''. Q ─⁀β→(STLCal Source Target)* Q'' ∧
                 R' →(STLCal Source Target)* R'' ∧ (Q'', R'') ∈ Rel ∧ ⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩)"
      and A3:  "weak_labelled_simulation_encL Rel"
      and A4:  "trans Rel"
      and inj: "inj encL"
      and pre: "encL_preserves_internal"
    shows "∀γ R'. R ─⁀γ→(STLCal Source Target)* R' ⟶
           (∃α P'' R''. P ─⁀α→(STLCal Source Target)* P'' ∧
            R' →(STLCal Source Target)* R'' ∧ (P'', R'') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩)"
proof clarify
  fix γ R'
  assume "R ─⁀γ→(STLCal Source Target)* R'"
  with A2 obtain β Q'' R'' where A5: "Q ─⁀β→(STLCal Source Target)* Q''"
                             and A6: "R' →(STLCal Source Target)* R''" and A7: "(Q'', R'') ∈ Rel"
                             and A8: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
    by blast
  from A1 A5 obtain α P''' Q''' where A9:  "P ─⁀α→(STLCal Source Target)* P'''"
                                  and A10: "Q'' →(STLCal Source Target)* Q'''"
                                  and A11: "(P''', Q''') ∈ Rel" and A12: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
  from inj pre have "encL_respects_internal"
    using inj_preserves_is_respects_internal
    by blast
  with A3 A7 A10 obtain R''' where A13: "R'' →(STLCal Source Target)* R'''"
                               and A14: "(Q''', R''') ∈ Rel"
    using weak_labelled_simulation_encL_and_respection_internal[of Rel Q'' R'' Q''']
    by blast
  from A6 A13 have A15: "R' →(STLCal Source Target)* R'''"
    using weakTauSteps_trans[of R' "(STLCal Source Target)" R'' R''']
    by simp
  from A4 A11 A14 have A16: "(P''', R''') ∈ Rel"
    unfolding trans_def
    by blast
  from inj A8 A12 have "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    using related_labels_trans_inj[of P α Q β R γ]
    by simp
  with A9 A15 A16 show "∃α P''' R'''. P ─⁀α→(STLCal Source Target)* P''' ∧
                        R' →(STLCal Source Target)* R''' ∧ (P''', R''') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_correspondence_simulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes corrSim: "weak_labelled_correspondence_simulation_encL Rel"
  shows "weak_labelled_correspondence_simulation_encL (Rel⇧=)"
proof
  from corrSim show "weak_labelled_simulation_encL (Rel⇧=)"
    using weak_labelled_simulation_encL_and_refl_closure[of "Rel"]
    by blast
next
  show "∀P Q β Q'. (P, Q) ∈ Rel⇧= ∧ Q ─⁀β→(STLCal Source Target)* Q'
        ⟶ (∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧ Q' →(STLCal Source Target)* Q'' ∧
            (P'', Q'') ∈ Rel⇧= ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
  proof clarify
    fix P Q β Q'
    assume "(P, Q) ∈ Rel⇧=" and A1: "Q ─⁀β→(STLCal Source Target)* Q'"
    moreover have "P = Q ⟹ ∃P'' Q''. P ─⁀β→(STLCal Source Target)* P'' ∧
                   Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel⇧= ∧ ⟨Q, β⟩ ≡⦇⦈ ⟨Q, β⟩"
    proof -
      assume "P = Q"
      moreover have "Q' →(STLCal Source Target)* Q'"
        using WTS_refl[of Q' "STLCal Source Target"]
        by simp
      moreover have "Q ∼ST Q"
        using source_or_target[of Q]
        by presburger
      hence "⟨Q, β⟩ ≡⦇⦈ ⟨Q, β⟩"
        unfolding related_labels_def
        by simp
      ultimately show "∃P'' Q''. P ─⁀β→(STLCal Source Target)* P'' ∧
                       Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel⇧= ∧ ⟨Q, β⟩ ≡⦇⦈ ⟨Q, β⟩"
        using A1
        by blast
    qed
    moreover have "(P, Q) ∈ Rel ⟹ ∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧
                   Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel⇧= ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    proof -
      assume "(P, Q) ∈ Rel"
      with corrSim A1 obtain α P'' Q'' where "P ─⁀α→(STLCal Source Target)* P''"
        and "Q' →(STLCal Source Target)* Q''" and "(P'', Q'') ∈ Rel" and "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
      thus "∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧ Q' →(STLCal Source Target)* Q'' ∧
            (P'', Q'') ∈ Rel⇧= ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by auto
    qed
    ultimately show "∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧
                     Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel⇧= ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      by auto
  qed
qed

lemma (in encodingLS_encL) weak_labelled_correspondence_simulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes corrSim:   "weak_labelled_correspondence_simulation_encL Rel"
      and injective: "inj encL"
      and preserves: "encL_preserves_internal"
    shows "weak_labelled_correspondence_simulation_encL (Rel⇧=)"
      and "weak_labelled_correspondence_simulation_encL (Rel⇧+)"
      and "weak_labelled_correspondence_simulation_encL (Rel⇧*)"
proof -
  from corrSim show A1: "weak_labelled_correspondence_simulation_encL (Rel⇧=)"
    using weak_labelled_correspondence_simulation_encL_and_refl_closure[of Rel]
    by simp
  have A2: "⋀Rel. weak_labelled_correspondence_simulation_encL Rel
            ⟹ weak_labelled_correspondence_simulation_encL (Rel⇧+)"
  proof
    fix Rel
    assume "weak_labelled_correspondence_simulation_encL Rel"
    with injective preserves show "weak_labelled_simulation_encL (Rel⇧+)"
      using weak_labelled_simulation_encL_and_closures(2)[of "Rel"]
      by blast
  next
    fix Rel
    assume B: "weak_labelled_correspondence_simulation_encL Rel"
    show "∀P Q β Q'. (P, Q) ∈ Rel⇧+ ∧ Q ─⁀β→(STLCal Source Target)* Q' ⟶
          (∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧ Q' →(STLCal Source Target)* Q'' ∧
          (P'', Q'') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
    proof clarify
      fix P Q β Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ─⁀β→(STLCal Source Target)* Q'"
      thus "∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧ Q' →(STLCal Source Target)* Q'' ∧
            (P'', Q'') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      proof (induct arbitrary: β Q')
        fix Q β Q'
        assume "(P, Q) ∈ Rel" and "Q ─⁀β→(STLCal Source Target)* Q'"
        with B obtain α P'' Q'' where C1: "P ─⁀α→(STLCal Source Target)* P''"
                                  and C2: "Q' →(STLCal Source Target)* Q''"
                                  and C3: "(P'', Q'') ∈ Rel" and C4: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by blast
        from C3 have "(P'', Q'') ∈ Rel⇧+"
          by simp
        with C1 C2 C4 show "∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧
          Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by blast
      next
        case (step Q R α R')
        assume "⋀β Q'. Q ─⁀β→(STLCal Source Target)* Q' ⟹
                ∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧
                Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        moreover assume "(Q, R) ∈ Rel"
        with B have "⋀β R'. R ─⁀β→(STLCal Source Target)* R' ⟹
                     ∃α Q'' R''. Q ─⁀α→(STLCal Source Target)* Q'' ∧
                     R' →(STLCal Source Target)* R'' ∧ (Q'', R'') ∈ Rel⇧+ ∧ ⟨Q, α⟩ ≡⦇⦈ ⟨R, β⟩"
          by blast
        moreover from injective preserves B have "weak_labelled_simulation_encL (Rel⇧+)"
          using weak_labelled_simulation_encL_and_closures(2)[of "Rel"]
          by blast
        moreover have "trans (Rel⇧+)"
          using trans_trancl[of Rel]
          by blast
        moreover assume "R ─⁀α→(STLCal Source Target)* R'"
        ultimately show "∃γ P'' R''. P ─⁀γ→(STLCal Source Target)* P'' ∧
                         R' →(STLCal Source Target)* R'' ∧ (P'', R'') ∈ Rel⇧+ ∧ ⟨P, γ⟩ ≡⦇⦈ ⟨R, α⟩"
          using labelled_correspondence_simulation_encL_condition_trans[of Q P "Rel⇧+" R]
                injective preserves
          by auto
      qed
    qed
  qed
  from corrSim A2[of "Rel"] show "weak_labelled_correspondence_simulation_encL (Rel⇧+)"
    by blast
  from A1 A2[of "Rel⇧="] show "weak_labelled_correspondence_simulation_encL (Rel⇧*)"
    using trancl_reflcl[of Rel]
    by auto
qed

subsection ‹Bisimulation›

text ‹A weak labelled bisimulation on encoded labels is a relation R such that
      (1) if (P, Q) in R and P evolves to some P' using a then there exist b and Q' such that Q
          evolves to Q' using b, (P', Q') in R, and a and b are related, and
      (2) if (P, Q) in R and Q evolves to some Q' using a then there exist b and P' such that P
          evolves to P' using b, (P', Q') in R, and a and b are related.›

abbreviation (in encodingLS_encL) weak_labelled_bisimulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "weak_labelled_bisimulation_encL Rel ≡
   (∀P Q α P'. ((P, Q) ∈ Rel ∧ P ─⁀α→(STLCal Source Target)* P') ⟶
    (∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)) ∧
   (∀P Q β Q'. (P, Q) ∈ Rel ∧ Q ─⁀β→(STLCal Source Target)* Q' ⟶
    (∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩))"

text ‹A symetric weak simulation is a weak bisimulation.›

lemma (in encodingLS_encL) symm_weak_labelled_simulation_encL_is_bisimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes "sym Rel"
      and "weak_labelled_simulation_encL Rel"
    shows "weak_labelled_bisimulation_encL Rel"
  using assms symD[of Rel] related_labels_sym
  by blast

text ‹If a relation as well as its inverse are weak simulations, then this relation is a weak
      bisimulation.›

lemma (in encodingLS_encL) weak_labelled_simulations_encL_impl_bisimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes sim:    "weak_labelled_simulation_encL Rel"
      and simInv: "weak_labelled_simulation_encL (Rel¯)"
    shows "weak_labelled_bisimulation_encL Rel"
proof auto
  fix P Q α P'
  assume "(P, Q) ∈ Rel" and "P ─⁀α→(STLCal Source Target)* P'"
  with sim show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
next
  fix P Q β Q'
  assume "(P, Q) ∈ Rel"
  hence "(Q, P) ∈ Rel¯"
    by simp
  moreover assume "Q ─⁀β→(STLCal Source Target)* Q'"
  ultimately obtain α P' where A1: "P ─⁀α→(STLCal Source Target)* P'" and A2: "(Q', P') ∈ Rel¯"
                           and A3: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    using simInv related_labels_sym
    by blast
  from A2 have "(P', Q') ∈ Rel"
    by induct
  with A1 A3 show "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_bisimulations_encL_impl_inverse_is_simulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "weak_labelled_bisimulation_encL Rel"
  shows "weak_labelled_simulation_encL (Rel¯)"
proof clarify
  fix P Q α P'
  assume "(Q, P) ∈ Rel"
  moreover assume "P ─⁀α→(STLCal Source Target)* P'"
  ultimately obtain β Q' where A1: "Q ─⁀β→(STLCal Source Target)* Q'" and A2: "(Q', P') ∈ Rel"
                           and A3: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    using bisim related_labels_sym
    by blast
  from A2 have "(P', Q') ∈ Rel¯"
    by simp
  with A1 A3 show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel¯ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_simulations_encL_iff_bisimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  shows "(weak_labelled_simulation_encL Rel ∧ weak_labelled_simulation_encL (Rel¯)) =
         weak_labelled_bisimulation_encL Rel"
  using weak_labelled_simulations_encL_impl_bisimulation[of "Rel"]
        weak_labelled_bisimulations_encL_impl_inverse_is_simulation[of "Rel"]
  by blast

text ‹A weak bisimulation is a weak correspondence simulation.›

lemma (in encodingLS_encL) weak_labelled_bisimulation_encL_is_correspondence_simulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "weak_labelled_bisimulation_encL Rel"
  shows "weak_labelled_correspondence_simulation_encL Rel"
proof
  from bisim show "weak_labelled_simulation_encL Rel"
    by blast
next
  show "∀P Q β Q'. (P, Q) ∈ Rel ∧ Q ─⁀β→(STLCal Source Target)* Q' ⟶
        (∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧ Q' →(STLCal Source Target)* Q'' ∧
        (P'', Q'') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
  proof clarify
    fix P Q β Q'
    assume "(P, Q) ∈ Rel" and "Q ─⁀β→(STLCal Source Target)* Q'"
    with bisim obtain α P' where "P ─⁀α→(STLCal Source Target)* P'" and "(P', Q') ∈ Rel"
                             and "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      by blast
    moreover have "Q' →(STLCal Source Target)* Q'"
      using WTS_refl[of Q' "STLCal Source Target"]
      by simp
    ultimately show "(∃α P'' Q''. P ─⁀α→(STLCal Source Target)* P'' ∧
                     Q' →(STLCal Source Target)* Q'' ∧ (P'', Q'') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
      by blast
  qed
qed

text ‹The reflexive, symmetric, and/or transitive closure of a weak bisimulation is a weak
      bisimulation, where we need for transitivity that the label encoding is injective.›

lemma (in encodingLS_encL) weak_labelled_bisimulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "weak_labelled_bisimulation_encL Rel"
  shows "weak_labelled_bisimulation_encL (Rel⇧=)"
proof auto
  fix P Q α P'
  assume "P ─⁀α→(STLCal Source Target)* P'" and "(P, Q) ∈ Rel"
  with bisim have "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
  thus "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix Q α P'
  assume "Q ─⁀α→(STLCal Source Target)* P'"
  moreover have "Q ∼ST Q"
    using source_or_target[of Q]
    by presburger
  hence "⟨Q, α⟩ ≡⦇⦈ ⟨Q, α⟩"
    unfolding related_labels_def
    by simp
  ultimately
  show "∃β Q'. Q ─⁀β→(STLCal Source Target)* Q' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨Q, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix P Q β Q'
  assume "Q ─⁀β→(STLCal Source Target)* Q'" and "(P, Q) ∈ Rel"
  with bisim have "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
  thus "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
next
  fix Q β Q'
  assume "Q ─⁀β→(STLCal Source Target)* Q'"
  moreover have "Q ∼ST Q"
    using source_or_target[of Q]
    by presburger
  hence "⟨Q, β⟩ ≡⦇⦈ ⟨Q, β⟩"
    unfolding related_labels_def
    by simp
  ultimately
  show "∃α P'. Q ─⁀α→(STLCal Source Target)* P' ∧ ((P', Q') ∈ Rel ∨ P' = Q') ∧ ⟨Q, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) weak_labelled_bisimulation_encL_and_symm_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "weak_labelled_bisimulation_encL Rel"
  shows "weak_labelled_bisimulation_encL (symcl Rel)"
  using bisim related_labels_sym
  by (auto simp add: symcl_def, blast+)

lemma (in encodingLS_encL) weak_labelled_bisimulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim:     "weak_labelled_bisimulation_encL Rel"
      and injective: "inj encL"
    shows "weak_labelled_bisimulation_encL (Rel⇧=)"
      and "weak_labelled_bisimulation_encL (symcl Rel)"
      and "weak_labelled_bisimulation_encL (Rel⇧+)"
      and "weak_labelled_bisimulation_encL (symcl (Rel⇧=))"
      and "weak_labelled_bisimulation_encL (Rel⇧*)"
      and "weak_labelled_bisimulation_encL ((symcl (Rel⇧=))⇧+)"
proof -
  from bisim show A1: "weak_labelled_bisimulation_encL (Rel⇧=)"
    using weak_labelled_bisimulation_encL_and_refl_closure[of Rel]
    by simp
  from bisim show "weak_labelled_bisimulation_encL (symcl Rel)"
    using weak_labelled_bisimulation_encL_and_symm_closure[of Rel]
    by simp
  have A2: "⋀Rel. weak_labelled_bisimulation_encL Rel ⟹ weak_labelled_bisimulation_encL (Rel⇧+)"
  proof
    fix Rel
    assume "weak_labelled_bisimulation_encL Rel"
    with injective show "weak_labelled_simulation_encL (Rel⇧+)"
      using weak_labelled_simulation_encL_and_closures(2)[of "Rel"]
      by blast
  next
    fix Rel
    assume B: "weak_labelled_bisimulation_encL Rel"
    show "∀P Q β Q'. (P, Q) ∈ Rel⇧+ ∧ Q ─⁀β→(STLCal Source Target)* Q' ⟶
          (∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
    proof clarify
      fix P Q β Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ─⁀β→(STLCal Source Target)* Q'"
      thus "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      proof (induct arbitrary: β Q')
        fix Q β Q'
        assume "(P, Q) ∈ Rel" and "Q ─⁀β→(STLCal Source Target)* Q'"
        with B obtain α P' where "P ─⁀α→(STLCal Source Target)* P'" and "(P', Q') ∈ Rel"
                             and "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by blast
        thus "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by auto
      next
        case (step Q R γ R')
        assume "(Q, R) ∈ Rel" and "R ─⁀γ→(STLCal Source Target)* R'"
        with B obtain β Q' where C1: "Q ─⁀β→(STLCal Source Target)* Q'" and C2: "(Q', R') ∈ Rel⇧+"
                             and C3: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
          by blast
        assume "⋀β Q'. Q ─⁀β→(STLCal Source Target)* Q' ⟹
                ∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        with C1 obtain α P' where C4: "P ─⁀α→(STLCal Source Target)* P'"
                              and C5: "(P', Q') ∈ Rel⇧+" and C6: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by blast
        from C2 C5 have C7: "(P', R') ∈ Rel⇧+"
          by simp
        from injective C3 C6 have "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          using related_labels_trans_inj[of P α Q β  R γ]
          by simp
        with C4 C7
        show "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', R') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          by blast
      qed
    qed
  qed
  from bisim A2[of "Rel"] show "weak_labelled_bisimulation_encL (Rel⇧+)"
    by blast
  from A1 show "weak_labelled_bisimulation_encL (symcl (Rel⇧=))"
    using weak_labelled_bisimulation_encL_and_symm_closure[of "Rel⇧="]
    by blast
  from A1 A2[of "Rel⇧="] show "weak_labelled_bisimulation_encL (Rel⇧*)"
    using trancl_reflcl[of Rel]
    by auto
  from A1 A2[of "symcl (Rel⇧=)"] show "weak_labelled_bisimulation_encL ((symcl (Rel⇧=))⇧+)"
    using weak_labelled_bisimulation_encL_and_symm_closure[of "Rel⇧="]
    by blast
qed

text ‹A strong labelled bisimulation on encoded labels is a relation R such that
      (1) if (P, Q) in R and P' is a derivative of P using a then there exist b and Q' such that
          Q' is a derivative of Q using b, (P', Q') in R, and a and b are related, and
      (2) if (P, Q) in R and Q' is a derivative of Q using a then there exist b and P' such that
          P' is a derivative of P using b, (P', Q') in R, and a and b are related.›

abbreviation (in encodingLS_encL) strong_labelled_bisimulation_encL
  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool" where
  "strong_labelled_bisimulation_encL Rel ≡
   (∀P Q α P'. (P, Q) ∈ Rel ∧ P ─α→(STLCal Source Target) P' ⟶
   (∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩))
   ∧ (∀P Q β Q'. (P, Q) ∈ Rel ∧ Q ─β→(STLCal Source Target) Q' ⟶
      (∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩))"

text ‹A symetric strong simulation is a strong bisimulation.›

lemma (in encodingLS_encL) symm_strong_labelled_simulation_encL_is_bisimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes "sym Rel"
      and "strong_labelled_simulation_encL Rel"
    shows "strong_labelled_bisimulation_encL Rel"
  using assms symD[of Rel] related_labels_sym
  by blast

text ‹If a relation as well as its inverse are strong simulations, then this relation is a strong
      bisimulation.›

lemma (in encodingLS_encL) strong_labelled_simulations_encL_impl_bisimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes sim:    "strong_labelled_simulation_encL Rel"
      and simInv: "strong_labelled_simulation_encL (Rel¯)"
    shows "strong_labelled_bisimulation_encL Rel"
proof auto
  fix P Q α P'
  assume "(P, Q) ∈ Rel" and "P ─α→(STLCal Source Target) P'"
  with sim show "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by simp
next
  fix P Q β Q'
  assume "(P, Q) ∈ Rel"
  hence "(Q, P) ∈ Rel¯"
    by simp
  moreover assume "Q ─β→(STLCal Source Target) Q'"
  ultimately obtain α P' where A1: "P ─α→(STLCal Source Target) P'" and A2: "(Q', P') ∈ Rel¯"
                           and A3: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    using simInv related_labels_sym
    by blast
  from A2 have "(P', Q') ∈ Rel"
    by induct
  with A1 A3 show "∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) strong_labelled_bisimulations_encL_impl_inverse_is_simulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "strong_labelled_bisimulation_encL Rel"
  shows "strong_labelled_simulation_encL (Rel¯)"
proof clarify
  fix P Q α P'
  assume "(Q, P) ∈ Rel"
  moreover assume "P ─α→(STLCal Source Target) P'"
  ultimately obtain β Q' where A1: "Q ─β→(STLCal Source Target) Q'" and A2: "(Q', P') ∈ Rel"
                           and A3: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    using bisim related_labels_sym
    by blast
  from A2 have "(P', Q') ∈ Rel¯"
    by simp
  with A1 A3 show "∃β Q'. Q ─β→(STLCal Source Target) Q' ∧ (P', Q') ∈ Rel¯ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    by blast
qed

lemma (in encodingLS_encL) strong_labelled_simulations_encL_iff_bisimulation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  shows "(strong_labelled_simulation_encL Rel ∧ strong_labelled_simulation_encL (Rel¯)) =
         strong_labelled_bisimulation_encL Rel"
  using strong_labelled_simulations_encL_impl_bisimulation[of "Rel"]
        strong_labelled_bisimulations_encL_impl_inverse_is_simulation[of "Rel"]
  by blast

text ‹A strong bisimulation is a weak bisimulation, if the label encoding respects the internal.
      Since bisimulation is symmetric, we cannot relax the requirement on the respection of the
      internal.›

lemma (in encodingLS_encL) strong_labelled_bisimulation_encL_impl_weak_simulation_of_internal:
  fixes Rel    :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q Q' :: "('procS, 'procT) Proc"
  assumes bisim:    "strong_labelled_bisimulation_encL Rel"
      and relation: "(P, Q) ∈ Rel"
      and internal: "Q →(STLCal Source Target)* Q'"
      and respects: "encL_respects_internal"
    shows "∃P'. P →(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel"
proof -
  define Cal where Cal_def: "Cal = STLCal Source Target"
  with internal have "Q →Cal* Q'"
    by simp
  from this bisim relation Cal_def show "∃P'. P →(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel"
  proof induct
    case (WTS_refl Q Cal)
    have "P →(STLCal Source Target)* P"
      using weakTauStep.WTS_refl[of P "STLCal Source Target"]
      by simp
    moreover assume "(P, Q) ∈ Rel"
    ultimately show "∃P'. P →(STLCal Source Target)* P' ∧ (P', Q) ∈ Rel"
      by blast
  next
    case (WTS_trans Q Cal Q' Q'')
    from WTS_trans(2) have IH: "strong_labelled_bisimulation_encL Rel ∧ (P, Q) ∈ Rel ∧
                                Cal = STLCal Source Target ⟹
                                ∃P'. P →(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel"
      by simp
    assume A1: "strong_labelled_bisimulation_encL Rel"
      and "(P, Q) ∈ Rel" and A2: "Cal = STLCal Source Target"
    with IH obtain P' where A3: "P →(STLCal Source Target)* P'" and A4: "(P', Q') ∈ Rel"
      by blast
    assume "Q' ─τ-Cal→Cal Q''"
    with A1 A2 A4 obtain α P'' where A5: "P' ─α→(STLCal Source Target) P''"
      and A6: "(P'', Q'') ∈ Rel" and A7: "⟨P', α⟩ ≡⦇⦈ ⟨Q', τ-(STLCal Source Target)⟩"
      by blast
    from respects A7 have "α = τ-(STLCal Source Target)"
      using encL_respects_internal_implies_iff_internal[of P' α Q' "τ-(STLCal Source Target)"]
            internalST_iff_internal
      by simp
    with A5 have "P' →(STLCal Source Target)* P''"
      using WTS_refl[of P' "STLCal Source Target"]
            weakTauStep.WTS_trans[of P' "STLCal Source Target" P' P'']
      by simp
    with A3 have "P →(STLCal Source Target)* P''"
      using weakTauSteps_trans[of P "STLCal Source Target" P' P'']
      by simp
    with A6 show "∃P''. P →(STLCal Source Target)* P'' ∧ (P'', Q'') ∈ Rel"
      by blast
  qed
qed

lemma (in encodingLS_encL) strong_impl_weak_labelled_bisimulation_encL:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim:    "strong_labelled_bisimulation_encL Rel"
      and respects: "encL_respects_internal"
    shows "weak_labelled_bisimulation_encL Rel"
proof
  from bisim respects show "weak_labelled_simulation_encL Rel"
    using strong_labelled_simulation_encL_and_respection_weak_simulation[of "Rel"]
    by blast
next
  show "∀P Q β Q'. (P, Q) ∈ Rel ∧ Q ─⁀β→(STLCal Source Target)* Q' ⟶
        (∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
  proof clarify
    fix P Q β Q'
    assume A1: "(P, Q) ∈ Rel" and A2: "Q ─⁀β→(STLCal Source Target)* Q'"
    thus "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
    proof (cases "β = τ-(STLCal Source Target)")
      assume B1: "β = τ-(STLCal Source Target)"
      with A2 have "Q →(STLCal Source Target)* Q'"
        unfolding weakLabelledStep_def
        by simp
      with bisim respects A1 obtain P' where B2: "P →(STLCal Source Target)* P'"
                                         and B3: "(P', Q') ∈ Rel"
        using strong_labelled_bisimulation_encL_impl_weak_simulation_of_internal[of Rel P Q Q']
        by blast
      from B1 B2 have B4: "P ─⁀β→(STLCal Source Target)* P'"
        unfolding weakLabelledStep_def
        by simp
      have "⟨P, β⟩ ≡⦇⦈ ⟨Q, β⟩"
        using source_or_target[of P] source_or_target[of Q]
      proof auto
        fix S S'
        show "⟨SourceTerm S, β⟩ ≡⦇⦈ ⟨SourceTerm S', β⟩"
          unfolding related_labels_def
          by simp
      next
        fix S T
        from respects B1 have "⦇SourceTerm S, β⦈↦⟨TargetTerm T, β⟩"
          using internalST_iff_internal
          unfolding encLST_def getSourceLabel_def getTargetLabel_def
          by auto
        thus "⟨SourceTerm S, β⟩ ≡⦇⦈ ⟨TargetTerm T, β⟩"
          unfolding related_labels_def
          by simp
      next
        fix T S
        from respects B1 have "⦇SourceTerm S, β⦈↦⟨TargetTerm T, β⟩"
          using internalST_iff_internal
          unfolding encLST_def getSourceLabel_def getTargetLabel_def
          by auto
        thus "⟨TargetTerm T, β⟩ ≡⦇⦈ ⟨SourceTerm S, β⟩"
          unfolding related_labels_def
          by simp
      next
        fix T T'
        show "⟨TargetTerm T, β⟩ ≡⦇⦈ ⟨TargetTerm T', β⟩"
          unfolding related_labels_def
          by simp
      qed
      with B3 B4
      show "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
    next
      assume B1: "β ≠ τ-(STLCal Source Target)" and "Q ─⁀β→(STLCal Source Target)* Q'"
      then obtain R S where B2: "Q →(STLCal Source Target)* R"
        and B3: "R ─β→(STLCal Source Target) S" and B4: "S →(STLCal Source Target)* Q'"
        unfolding weakLabelledStep_def weakLabelledActionStep_def
        by auto
      from bisim respects A1 B2 obtain T where B5: "P →(STLCal Source Target)* T"
                                           and B6: "(T, R) ∈ Rel"
        using strong_labelled_bisimulation_encL_impl_weak_simulation_of_internal[of Rel P Q R]
        by blast
      from bisim B3 B6 obtain α U where B7: "T ─α→(STLCal Source Target) U"
                                    and B8: "(U, S) ∈ Rel" and B9: "⟨T, α⟩ ≡⦇⦈ ⟨R, β⟩"
        by blast
      from bisim respects B4 B8 obtain P' where B10: "U →(STLCal Source Target)* P'"
                                            and B11: "(P', Q') ∈ Rel"
        using strong_labelled_bisimulation_encL_impl_weak_simulation_of_internal[of Rel U S Q']
        by blast
      from respects B1 B9 have "α ≠ τ-(STLCal Source Target)"
        using encL_respects_internal_implies_iff_internal[of T α R β] internalST_iff_internal
        by simp
      with B5 B7 B10 have B12: "P ─⁀α→(STLCal Source Target)* P'"
        unfolding weakLabelledStep_def weakLabelledActionStep_def
        by auto
      from B5 have B13: "T ∼ST P"
        using weakTauStepsST_STLCal_weakTauSteps[of P T]
        by blast
      from B2 have "R ∼ST Q"
        using weakTauStepsST_STLCal_weakTauSteps[of Q R]
        by blast
      with B9 B13 have "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        using related_labels_exchange_processes[of T α R β P Q]
        by simp
      with B11 B12
      show "∃α P'. P ─⁀α→(STLCal Source Target)* P' ∧ (P', Q') ∈ Rel ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        by blast
    qed
  qed
qed

text ‹The reflexive, symmetric, and/or transitive closure of a strong bisimulation is a strong
      bisimulation, where for transitivitiy we need that the label encoding is injective and
      preserves the internal.›

lemma (in encodingLS_encL) strong_labelled_bisimulation_encL_and_refl_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "strong_labelled_bisimulation_encL Rel"
  shows "strong_labelled_bisimulation_encL (Rel⇧=)"
  using bisim related_labels_refl
  by (auto simp add: refl, blast+)

lemma (in encodingLS_encL) strong_labelled_bisimulation_encL_and_symm_closure:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim: "strong_labelled_bisimulation_encL Rel"
  shows "strong_labelled_bisimulation_encL (symcl Rel)"
  using bisim related_labels_sym
  by (auto simp add: symcl_def, blast+)

lemma (in encodingLS_encL) strong_labelled_bisimulation_encL_and_closures:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes bisim:     "strong_labelled_bisimulation_encL Rel"
      and injective: "inj encL"
      and preserves: "encL_preserves_internal"
    shows "strong_labelled_bisimulation_encL (Rel⇧=)"
      and "strong_labelled_bisimulation_encL (symcl Rel)"
      and "strong_labelled_bisimulation_encL (Rel⇧+)"
      and "strong_labelled_bisimulation_encL (symcl (Rel⇧=))"
      and "strong_labelled_bisimulation_encL (Rel⇧*)"
      and "strong_labelled_bisimulation_encL ((symcl (Rel⇧=))⇧+)"
proof -
  from bisim show A1: "strong_labelled_bisimulation_encL (Rel⇧=)"
    using strong_labelled_bisimulation_encL_and_refl_closure[of Rel]
    by simp
  from bisim show "strong_labelled_bisimulation_encL (symcl Rel)"
    using strong_labelled_bisimulation_encL_and_symm_closure[of Rel]
    by simp
  have A2: "⋀Rel. strong_labelled_bisimulation_encL Rel ⟹
            strong_labelled_bisimulation_encL (Rel⇧+)"
  proof
    fix Rel
    assume "strong_labelled_bisimulation_encL Rel"
    with injective preserves show "strong_labelled_simulation_encL (Rel⇧+)"
      using strong_labelled_simulation_encL_and_closures(2)[of "Rel"]
      by blast
  next
    fix Rel
    assume B: "strong_labelled_bisimulation_encL Rel"
    show "∀P Q β Q'. (P, Q) ∈ Rel⇧+ ∧ Q ─β→(STLCal Source Target) Q' ⟶
          (∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩)"
    proof clarify
      fix P Q β Q'
      assume "(P, Q) ∈ Rel⇧+" and "Q ─β→(STLCal Source Target) Q'"
      thus "∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      proof (induct arbitrary: β Q')
        fix Q β Q'
        assume "(P, Q) ∈ Rel" and "Q ─β→(STLCal Source Target) Q'"
        with B obtain α P' where "P ─α→(STLCal Source Target) P'" and "(P', Q') ∈ Rel"
                             and "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by blast
        thus "∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by auto
      next
        case (step Q R γ R')
        assume "(Q, R) ∈ Rel" and "R ─γ→(STLCal Source Target) R'"
        with B obtain β Q' where C1: "Q ─β→(STLCal Source Target) Q'" and C2: "(Q', R') ∈ Rel⇧+"
                             and C3: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
          by blast
        assume "⋀β Q'. Q ─β→(STLCal Source Target) Q' ⟹
                ∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', Q') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
        with C1 obtain α P' where C4: "P ─α→(STLCal Source Target) P'" and C5: "(P', Q') ∈ Rel⇧+"
                              and C6: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
          by blast
        from C2 C5 have C7: "(P', R') ∈ Rel⇧+"
          by simp
        from injective C3 C6 have "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          using related_labels_trans_inj[of P α Q β R γ]
          by simp
        with C4 C7
        show "∃α P'. P ─α→(STLCal Source Target) P' ∧ (P', R') ∈ Rel⇧+ ∧ ⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          by blast
      qed
    qed
  qed
  from bisim A2[of "Rel"] show "strong_labelled_bisimulation_encL (Rel⇧+)"
    by blast
  from A1 show "strong_labelled_bisimulation_encL (symcl (Rel⇧=))"
    using strong_labelled_bisimulation_encL_and_symm_closure[of "Rel⇧="]
    by blast
  from A1 A2[of "Rel⇧="] show "strong_labelled_bisimulation_encL (Rel⇧*)"
    using trancl_reflcl[of Rel]
    by auto
  from A1 A2[of "symcl (Rel⇧=)"] show "strong_labelled_bisimulation_encL ((symcl (Rel⇧=))⇧+)"
    using strong_labelled_bisimulation_encL_and_symm_closure[of "Rel⇧="]
    by blast
qed

end