Theory Encodings

(* Kirstin Peters, TU Berlin, 2015 concerning the reduction semantics and
   Kirstin Peters, University of Augsburg, 2026 for the labelled semantics and the separation of
   syntax and semantics including the locale encodingFunction *)

theory Encodings
  imports ProcessCalculi
begin

section ‹Encodings›

text ‹In the simplest case an encoding from a source into a target language is a mapping from
      source into target terms. We start with some notions on such a function considering only the
      syntax and then add the different kinds of considered semantics: reduction semantics,
      reduction semantics with barbs (as subcase) and labelled semantics.›

subsection ‹A function between processes.›

text ‹Encodability criteria describe properties on the mappings from source into target terms. To
      analyse encodability criteria we map them on conditions on relations between source and
      target terms. More precisely, we consider relations on pairs of the disjoint union of source
      and target terms. We denote this disjoint union of source and target terms by Proc.›

datatype ('procS, 'procT) Proc =
  SourceTerm 'procS
| TargetTerm 'procT

locale encodingFunction =
  fixes Enc :: "'procS ⇒ 'procT"
begin

abbreviation enc :: "'procS ⇒ 'procT" (‹⟦_⟧› [65] 70) where
  "⟦S⟧ ≡ Enc S"

abbreviation isSource :: "('procS, 'procT) Proc ⇒ bool" (‹_ ∈ ProcS› [70] 80) where
  "P ∈ ProcS ≡ (∃S. P = SourceTerm S)"

abbreviation isTarget :: "('procS, 'procT) Proc ⇒ bool" (‹_ ∈ ProcT› [70] 80) where
  "P ∈ ProcT ≡ (∃T. P = TargetTerm T)"

abbreviation getSource :: "'procS ⇒ ('procS, 'procT) Proc ⇒ bool" (‹_ ∈S _› [70, 70] 80) where
  "S ∈S P ≡ (P = SourceTerm S)"

abbreviation getTarget :: "'procT ⇒ ('procS, 'procT) Proc ⇒ bool" (‹_ ∈T _› [70, 70] 80) where
  "T ∈T P ≡ (P = TargetTerm T)"

abbreviation sameKind
  :: "('procS, 'procT) Proc ⇒ ('procS, 'procT) Proc ⇒ bool" (‹_ ∼ST _› [70, 70] 80) where
  "P ∼ST Q ≡ (P ∈ ProcS ∧ Q ∈ ProcS) ∨ (P ∈ ProcT ∧ Q ∈ ProcT)"

text ‹Every term of the disjoint union is either a source or a target term.›

lemma source_or_target:
  fixes P :: "('procS, 'procT) Proc"
  shows "P ∈ ProcS ∨ P ∈ ProcT"
  by (induct, simp_all)

text ‹Similar to relations we define what it means for an encoding to preserve, reflect, or respect
      a predicate. An encoding preserves some predicate P if P(S) implies P(enc S) for all source
      terms S.›

abbreviation enc_preserves_pred :: "(('procS, 'procT) Proc ⇒ bool) ⇒ bool" where
  "enc_preserves_pred Pred ≡ ∀S. Pred (SourceTerm S) ⟶ Pred (TargetTerm (⟦S⟧))"

abbreviation enc_preserves_binary_pred :: "(('procS, 'procT) Proc ⇒ 'b ⇒ bool) ⇒ bool" where
  "enc_preserves_binary_pred Pred ≡ ∀S x. Pred (SourceTerm S) x ⟶ Pred (TargetTerm (⟦S⟧)) x"

text ‹An encoding reflects some predicate P if P(S) implies P(enc S) for all source terms S.›

abbreviation enc_reflects_pred :: "(('procS, 'procT) Proc ⇒ bool) ⇒ bool" where
  "enc_reflects_pred Pred ≡ ∀S. Pred (TargetTerm (⟦S⟧)) ⟶ Pred (SourceTerm S)"

abbreviation enc_reflects_binary_pred :: "(('procS, 'procT) Proc ⇒ 'b ⇒ bool) ⇒ bool" where
  "enc_reflects_binary_pred Pred ≡ ∀S x. Pred (TargetTerm (⟦S⟧)) x ⟶ Pred (SourceTerm S) x"

text ‹An encoding respects a predicate if it preserves and reflects it.›

abbreviation enc_respects_pred :: "(('procS, 'procT) Proc ⇒ bool) ⇒ bool" where
  "enc_respects_pred Pred ≡ enc_preserves_pred Pred ∧ enc_reflects_pred Pred"

abbreviation enc_respects_binary_pred :: "(('procS, 'procT) Proc ⇒ 'b ⇒ bool) ⇒ bool" where
  "enc_respects_binary_pred Pred ≡
   enc_preserves_binary_pred Pred ∧ enc_reflects_binary_pred Pred"

end

subsection ‹An encoding function considering reduction semantics.›

text ‹An encoding consists of a source language, a target language, and a mapping from source into
      target terms.›

definition STCal
  :: "'procS processCalculus ⇒ 'procT processCalculus ⇒ (('procS, 'procT) Proc) processCalculus"
  where
  "STCal Source Target ≡
   ⦇Reductions = λP P'.
   (∃SP SP'. P = SourceTerm SP ∧ P' = SourceTerm SP' ∧ Reductions Source SP SP') ∨
   (∃TP TP'. P = TargetTerm TP ∧ P' = TargetTerm TP' ∧ Reductions Target TP TP')⦈"

locale encoding =
  encodingFunction Enc
  for Enc      :: "'procS ⇒ 'procT" +
  fixes Source :: "'procS processCalculus"
    and Target :: "'procT processCalculus"
begin

text ‹A step of a term in Proc is either a source term step or a target term step.›

abbreviation stepST
  :: "('procS, 'procT) Proc ⇒ ('procS, 'procT) Proc ⇒ bool" (‹_ ⟼ST _› [70, 70] 80) where
  "P ⟼ST P' ≡
   (∃S S'. S ∈S P ∧ S' ∈S P' ∧ S ⟼Source S') ∨ (∃T T'. T ∈T P ∧ T' ∈T P' ∧ T ⟼Target T')"

lemma stepST_STCal_step:
  fixes P P' :: "('procS, 'procT) Proc"
  shows "P ⟼(STCal Source Target) P' = P ⟼ST P'"
  by (simp add: STCal_def)

lemma STStep_step:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼ST P' = (∃S'. S' ∈S P' ∧ S ⟼Source S')"
    and "TargetTerm T ⟼ST P' = (∃T'. T' ∈T P' ∧ T ⟼Target T')"
  by blast+

lemma STCal_step:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼(STCal Source Target) P' = (∃S'. S' ∈S P' ∧ S ⟼Source S')"
    and "TargetTerm T ⟼(STCal Source Target) P' = (∃T'. T' ∈T P' ∧ T ⟼Target T')"
  by (simp add: STCal_def)+

text ‹A sequence of steps of a term in Proc is either a sequence of source term steps or a sequence
      of target term steps.›

abbreviation stepsST
  :: "('procS, 'procT) Proc ⇒ ('procS, 'procT) Proc ⇒ bool"  (‹_ ⟼ST* _› [70, 70] 80) where
  "P ⟼ST* P' ≡
   (∃S S'. S ∈S P ∧ S' ∈S P' ∧ S ⟼Source* S') ∨ (∃T T'. T ∈T P ∧ T' ∈T P' ∧ T ⟼Target* T')"

lemma STSteps_steps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼ST* P' = (∃S'. S' ∈S P' ∧ S ⟼Source* S')"
    and "TargetTerm T ⟼ST* P' = (∃T'. T' ∈T P' ∧ T ⟼Target* T')"
  by blast+

lemma STCal_steps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ⟼(STCal Source Target)* P' = (∃S'. S' ∈S P' ∧ S ⟼Source* S')"
    and "TargetTerm T ⟼(STCal Source Target)* P' = (∃T'. T' ∈T P' ∧ T ⟼Target* T')"
proof auto
  assume "SourceTerm S ⟼(STCal Source Target)* P'"
  from this obtain n where "SourceTerm S ⟼(STCal Source Target)⇗n⇖ P'"
    by (auto simp add: steps_def)
  thus "∃S'. S' ∈S P' ∧ S ⟼Source* S'"
  proof (induct n arbitrary: P')
    case 0
    assume "SourceTerm S ⟼(STCal Source Target)⇗0⇖ P'"
    hence "S ∈S P'"
      by simp
    moreover have "S ⟼Source* S"
      by (rule steps_refl)
    ultimately show "∃S'. S' ∈S P' ∧ S ⟼Source* S'"
      by blast
  next
    case (Suc n P'')
    assume "SourceTerm S ⟼(STCal Source Target)⇗Suc n⇖ P''"
    from this obtain P' where A1: "SourceTerm S ⟼(STCal Source Target)⇗n⇖ P'"
                          and A2: "P' ⟼(STCal Source Target) P''"
      by auto
    assume "⋀P'. SourceTerm S ⟼(STCal Source Target)⇗n⇖ P' ⟹ ∃S'. S' ∈S P' ∧ S ⟼Source* S'"
    with A1 obtain S' where A3: "S' ∈S P'" and A4: "S ⟼Source* S'"
      by blast
    from A2 A3 obtain S'' where A5: "S'' ∈S P''" and A6: "S' ⟼Source S''"
      using STCal_step(1)[where S="S'" and P'="P''"]
      by blast
    from A4 A6 have "S ⟼Source* S''"
      using step_to_steps[where Cal="Source" and P="S'" and P'="S''"]
      by (simp add: steps_add[where Cal="Source" and P="S" and Q="S'" and R="S''"])
    with A5 show "∃S''. S'' ∈S P'' ∧ S ⟼Source* S''"
      by blast
  qed
next
  fix S'
  assume "S ⟼Source* S'"
  from this obtain n where "S ⟼Source⇗n⇖ S'"
    by (auto simp add: steps_def)
  thus "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
  proof (induct n arbitrary: S')
    case 0
    assume "S ⟼Source⇗0⇖ S'"
    hence "S = S'"
      by auto
    thus "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
      by (simp add: steps_refl)
  next
    case (Suc n S'')
    assume "S ⟼Source⇗Suc n⇖ S''"
    from this obtain S' where B1: "S ⟼Source⇗n⇖ S'" and B2: "S' ⟼Source S''"
      by auto
    assume "⋀S'. S ⟼Source⇗n⇖ S' ⟹ SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
    with B1 have "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
      by blast
    moreover from B2 have "SourceTerm S' ⟼(STCal Source Target)* (SourceTerm S'')"
      using step_to_steps[where Cal="STCal Source Target" and P="SourceTerm S'"]
      by (simp add: STCal_def)
    ultimately show "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S'')"
      by (rule steps_add)
  qed
next
  assume "TargetTerm T ⟼(STCal Source Target)* P'"
  from this obtain n where "TargetTerm T ⟼(STCal Source Target)⇗n⇖ P'"
    by (auto simp add: steps_def)
  thus "∃T'. T' ∈T P' ∧ T ⟼Target* T'"
  proof (induct n arbitrary: P')
    case 0
    assume "TargetTerm T ⟼(STCal Source Target)⇗0⇖ P'"
    hence "T ∈T P'"
      by simp
    moreover have "T ⟼Target* T"
      by (rule steps_refl)
    ultimately show "∃T'. T' ∈T P' ∧ T ⟼Target* T'"
      by blast
  next
    case (Suc n P'')
    assume "TargetTerm T ⟼(STCal Source Target)⇗Suc n⇖ P''"
    from this obtain P' where A1: "TargetTerm T ⟼(STCal Source Target)⇗n⇖ P'"
                          and A2: "P' ⟼(STCal Source Target) P''"
      by auto
    assume "⋀P'. TargetTerm T ⟼(STCal Source Target)⇗n⇖ P' ⟹ ∃T'. T' ∈T P' ∧ T ⟼Target* T'"
    with A1 obtain T' where A3: "T' ∈T P'" and A4: "T ⟼Target* T'"
      by blast
    from A2 A3 obtain T'' where A5: "T'' ∈T P''" and A6: "T' ⟼Target T''"
      using STCal_step(2)[where T="T'" and P'="P''"]
      by blast
    from A4 A6 have "T ⟼Target* T''"
      using step_to_steps[where Cal="Target" and P="T'" and P'="T''"]
      by (simp add: steps_add[where Cal="Target" and P="T" and Q="T'" and R="T''"])
    with A5 show "∃T''. T'' ∈T P'' ∧ T ⟼Target* T''"
      by blast
  qed
next
  fix T'
  assume "T ⟼Target* T'"
  from this obtain n where "T ⟼Target⇗n⇖ T'"
    by (auto simp add: steps_def)
  thus "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
  proof (induct n arbitrary: T')
    case 0
    assume "T ⟼Target⇗0⇖ T'"
    hence "T = T'"
      by auto
    thus "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
      by (simp add: steps_refl)
  next
    case (Suc n T'')
    assume "T ⟼Target⇗Suc n⇖ T''"
    from this obtain T' where B1: "T ⟼Target⇗n⇖ T'" and B2: "T' ⟼Target T''"
      by auto
    assume "⋀T'. T ⟼Target⇗n⇖ T' ⟹ TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
    with B1 have "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
      by blast
    moreover from B2 have "TargetTerm T' ⟼(STCal Source Target)* (TargetTerm T'')"
      using step_to_steps[where Cal="STCal Source Target" and P="TargetTerm T'"]
      by (simp add: STCal_def)
    ultimately show "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T'')"
      by (rule steps_add)
  qed
qed

lemma stepsST_STCal_steps:
  fixes P P' :: "('procS, 'procT) Proc"
  shows "P ⟼(STCal Source Target)* P' = P ⟼ST* P'"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ⟼(STCal Source Target)* P' = P ⟼ST* P'"
    using STCal_steps(1)[where S="SP" and P'="P'"] STSteps_steps(1)[where S="SP" and P'="P'"]
    by blast
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ⟼(STCal Source Target)* P' = P ⟼ST* P'"
    using STCal_steps(2)[where T="TP" and P'="P'"] STSteps_steps(2)[where T="TP" and P'="P'"]
    by blast
qed

lemma stepsST_refl:
  fixes P :: "('procS, 'procT) Proc"
  shows "P ⟼ST* P"
  by (cases P, simp_all add: steps_refl)

lemma stepsST_add:
  fixes P Q R :: "('procS, 'procT) Proc"
  assumes A1: "P ⟼ST* Q"
      and A2: "Q ⟼ST* R"
  shows "P ⟼ST* R"
proof -
  from A1 have "P ⟼(STCal Source Target)* Q"
    by (simp add: stepsST_STCal_steps)
  moreover from A2 have "Q ⟼(STCal Source Target)* R"
    by (simp add: stepsST_STCal_steps)
  ultimately have "P ⟼(STCal Source Target)* R"
    by (rule steps_add)
  thus "P ⟼ST* R"
    by (simp add: stepsST_STCal_steps)
qed

text ‹A divergent term of Proc is either a divergent source term or a divergent target term.›

abbreviation divergentST :: "('procS, 'procT) Proc ⇒ bool" (‹_ ⟼STω› [70] 80) where
  "P ⟼STω ≡ (∃S. S ∈S P ∧ S ⟼(Source)ω) ∨ (∃T. T ∈T P ∧ T ⟼(Target)ω)"

lemma STCal_divergent:
  fixes S  :: "'procS"
    and T  :: "'procT"
  shows "SourceTerm S ⟼(STCal Source Target)ω = S ⟼(Source)ω"
    and "TargetTerm T ⟼(STCal Source Target)ω = T ⟼(Target)ω"
  using STCal_steps
  by (auto simp add: STCal_def divergent_def)

lemma divergentST_STCal_divergent:
  fixes P :: "('procS, 'procT) Proc"
  shows "P ⟼(STCal Source Target)ω = P ⟼STω"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ⟼(STCal Source Target)ω = P ⟼STω"
    using STCal_divergent(1)
    by simp
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ⟼(STCal Source Target)ω = P ⟼STω"
    using STCal_divergent(2)
    by simp
qed

end

subsection ‹An encoding function considering reduction semantics and barbs.›

text ‹To compare source terms and target terms w.r.t. their barbs or observables we assume that
      each languages defines its own predicate for the existence of barbs.›

definition STCalWB
  :: "('procS, 'barbs) calculusWithBarbs ⇒ ('procT, 'barbs) calculusWithBarbs
      ⇒ (('procS, 'procT) Proc, 'barbs) calculusWithBarbs" where
  "STCalWB Source Target ≡
   ⦇Calculus = STCal (calculusWithBarbs.Calculus Source) (calculusWithBarbs.Calculus Target),
   HasBarb   = λP a. (∃SP. P = SourceTerm SP ∧ (calculusWithBarbs.HasBarb Source) SP a) ∨
                     (∃TP. P = TargetTerm TP ∧ (calculusWithBarbs.HasBarb Target) TP a)⦈"

locale encoding_wrt_barbs =
  encoding Enc Source Target
  for Source :: "'procS processCalculus"
  and Target :: "'procT processCalculus"
  and Enc    :: "'procS ⇒ 'procT" +
  fixes SWB :: "('procS, 'barbs) calculusWithBarbs"
    and TWB :: "('procT, 'barbs) calculusWithBarbs"
  assumes calS: "calculusWithBarbs.Calculus SWB = Source"
      and calT: "calculusWithBarbs.Calculus TWB = Target"
begin

lemma STCalWB_STCal:
  shows "Calculus (STCalWB SWB TWB) = STCal Source Target"
  unfolding STCalWB_def using calS calT
  by auto

text ‹We say a term P of Proc has some barbs a if either P is a source term that has barb a or P is
      a target term that has the barb b. For simplicity we assume that the sets of barbs is large
      enough to contain all barbs of the source terms, the target terms, and all barbs they might
      have in common.›

abbreviation hasBarbST :: "('procS, 'procT) Proc ⇒ 'barbs ⇒ bool" (‹_↓._› [70, 70] 80) where
  "P↓.a ≡ (∃S. S ∈S P ∧ S↓<SWB>a) ∨ (∃T. T ∈T P ∧ T↓<TWB>a)"

lemma STCalWB_hasBarbST:
  fixes P :: "('procS, 'procT) Proc"
    and a :: "'barbs"
  shows "P↓<STCalWB SWB TWB>a = P↓.a"
  by (simp add: STCalWB_def)

lemma preservation_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes preservation: "rel_preserves_barbs Rel (STCalWB SWB TWB)"
      and rel:          "(P, Q) ∈ Rel"
      and barb:         "P↓.a"
    shows "Q↓.a"
  using preservation rel barb
  by (simp add: STCalWB_def)

lemma reflection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes reflection: "rel_reflects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
      and barb:       "Q↓.a"
    shows "P↓.a"
  using reflection rel barb
  by (simp add: STCalWB_def)

lemma respection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes respection: "rel_respects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
    shows "P↓.a = Q↓.a"
  using preservation_of_barbs_in_barbed_encoding[where Rel="Rel" and P="P" and Q="Q" and a="a"]
        reflection_of_barbs_in_barbed_encoding[where Rel="Rel" and P="P" and Q="Q" and a="a"]
        respection rel
  by blast

text ‹A term P of Proc reaches a barb a if either P is a source term that reaches a or P is a
      target term that reaches a.›

abbreviation reachesBarbST :: "('procS, 'procT) Proc ⇒ 'barbs ⇒ bool" (‹_⇓._› [70, 70] 80) where
  "P⇓.a ≡ (∃S. S ∈S P ∧ S⇓<SWB>a) ∨ (∃T. T ∈T P ∧ T⇓<TWB>a)"

lemma STCalWB_reachesBarbST:
  fixes P :: "('procS, 'procT) Proc"
    and a :: "'barbs"
  shows "P⇓<STCalWB SWB TWB>a = P⇓.a"
proof -
  have "∀S. SourceTerm S⇓<STCalWB SWB TWB>a = SourceTerm S⇓.a"
    using STCal_steps(1)
    by (auto simp add: STCalWB_def calS calT)
  moreover have "∀T. TargetTerm T⇓<STCalWB SWB TWB>a = TargetTerm T⇓.a"
    using STCal_steps(2)
    by (auto simp add: STCalWB_def calS calT)
  ultimately show "P⇓<STCalWB SWB TWB>a = P⇓.a"
    by (cases P, simp+)
qed

lemma weak_preservation_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes preservation: "rel_weakly_preserves_barbs Rel (STCalWB SWB TWB)"
      and rel:          "(P, Q) ∈ Rel"
      and barb:         "P⇓.a"
    shows "Q⇓.a"
proof -
  from barb have "P⇓<STCalWB SWB TWB>a"
    by (simp add: STCalWB_reachesBarbST)
  with preservation rel have "Q⇓<STCalWB SWB TWB>a"
    by blast
  thus "Q⇓.a"
    by (simp add: STCalWB_reachesBarbST)
qed

lemma weak_reflection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes reflection: "rel_weakly_reflects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
      and barb:       "Q⇓.a"
    shows "P⇓.a"
proof -
  from barb have "Q⇓<STCalWB SWB TWB>a"
    by (simp add: STCalWB_reachesBarbST)
  with reflection rel have "P⇓<STCalWB SWB TWB>a"
    by blast
  thus "P⇓.a"
    by (simp add: STCalWB_reachesBarbST)
qed

lemma weak_respection_of_barbs_in_barbed_encoding:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and P Q :: "('procS, 'procT) Proc"
    and a   :: "'barbs"
  assumes respection: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
      and rel:        "(P, Q) ∈ Rel"
    shows "P⇓.a = Q⇓.a"
proof (rule iffI)
  assume "P⇓.a"
  with respection rel show "Q⇓.a"
    using weak_preservation_of_barbs_in_barbed_encoding[where Rel="Rel"]
    by blast
next
  assume "Q⇓.a"
  with respection rel show "P⇓.a"
    using weak_reflection_of_barbs_in_barbed_encoding[where Rel="Rel"]
    by blast
qed

end

subsection ‹An encoding function considering labelled semantics.›

text ‹Also for the labelled semantics an encoding consists of a source language, a target language,
      and a mapping from source into target terms. We also inherit the other notions of encodings
      that consider reduction semantics. Similar to the disjoint union of source and target terms,
      we also build the disjoint union of source and target labels with a fresh internal label.
      This internal label will be used instead of a source or target internal label in the calculus
      on the disjoint union, since we require a single internal label for a labelled calculus.›

datatype ('labS, 'labT) Lab =
  SourceLabel 'labS
| TargetLabel 'labT
| Internal 'labS 'labT

definition STLCal
  :: "('procS, 'labS) labelledProcessCalculus ⇒ ('procT, 'labT) labelledProcessCalculus ⇒
      (('procS, 'procT) Proc, ('labS, 'labT) Lab) labelledProcessCalculus"
  where
  "STLCal Source Target ≡
   ⦇LabelledSemantics = λP α P'.
   (∃SP Sα SP'. P = SourceTerm SP ∧ (α = SourceLabel Sα ∧ α ≠ SourceLabel (τ-Source) ∨
    α = Internal (τ-Source) (τ-Target) ∧ Sα = τ-Source) ∧ P' = SourceTerm SP' ∧
    LabelledSemantics Source SP Sα SP') ∨
   (∃TP Tα TP'. P = TargetTerm TP ∧ (α = TargetLabel Tα ∧ α ≠ TargetLabel (τ-Target) ∨
    α = Internal (τ-Source) (τ-Target) ∧ Tα = τ-Target) ∧ P' = TargetTerm TP' ∧
    LabelledSemantics Target TP Tα TP'),
   InternalAction = Internal (τ-Source) (τ-Target)⦈"

locale encodingLS =
  encodingFunction Enc
  for Enc      :: "'procS ⇒ 'procT" +
  fixes Source :: "('procS, 'labS) labelledProcessCalculus"
    and Target :: "('procT, 'labT) labelledProcessCalculus"
begin

abbreviation internalST :: "('labS, 'labT) Lab" (‹τ-STLCal› 80) where
  "τ-STLCal ≡ Internal (τ-Source) (τ-Target)"

definition isSourceLabel :: "('labS, 'labT) Lab ⇒ bool" (‹_ ∈ LabS› [70] 80) where
  "α ∈ LabS ≡ (∃β. α = SourceLabel β)"

definition isTargetLabel :: "('labS, 'labT) Lab ⇒ bool" (‹_ ∈ LabT› [70] 80) where
  "α ∈ LabT ≡ (∃β. α = TargetLabel β)"

definition getSourceLabel
  :: "'labS ⇒ ('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ bool" (‹_ ∈SL ⟨_, _⟩› [70, 70, 70] 80)
  where
  "β ∈SL ⟨P, α⟩ ≡ P ∈ ProcS ∧ (α = SourceLabel β ∧ β ≠ τ-Source ∨ α = τ-STLCal ∧ β = τ-Source)"

definition getTargetLabel
  :: "'labT ⇒ ('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ bool" (‹_ ∈TL ⟨_, _⟩› [70, 70, 70] 80)
  where
  "β ∈TL ⟨P, α⟩ ≡ P ∈ ProcT ∧ (α = TargetLabel β ∧ β ≠ τ-Target ∨ α = τ-STLCal ∧ β = τ-Target)"

inductive getSourceLabels
  :: "'labS list ⇒ ('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab list ⇒ bool"
  (‹_ ∈SL* ⟨_, _⟩› [70, 70, 70] 80) where
  SLNil:  "P ∈ ProcS ⟹ [] ∈SL* ⟨P, []⟩"
| SLCons: "⟦v ∈SL* ⟨P, w⟩; β ∈SL ⟨Q, α⟩⟧ ⟹ (v@[β]) ∈SL* ⟨P, (w@[α])⟩"

inductive getTargetLabels
  :: "'labT list ⇒ ('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab list ⇒ bool"
  (‹_ ∈TL* ⟨_, _⟩› [70, 70, 70] 80) where
  TLNil:  "P ∈ ProcT ⟹ [] ∈TL* ⟨P, []⟩"
| TLCons: "⟦v ∈TL* ⟨P, w⟩; β ∈TL ⟨Q, α⟩⟧ ⟹ (v@[β]) ∈TL* ⟨P, (w@[α])⟩"

text ‹To avoid confusion we forbid for a source label version of the internal label and similar for
      the target. Instead internal steps on the source or target are mapped on steps with the new
      internal label in the disjoint union of source and target labels. As tiebreaker for the
      internal label in the disjoint union we add a process, that is supposed to be the process
      that performs a step on this label, and use the kind of the process to determine whether the
      internal results from an internal in the source or target.›

lemma no_source_or_target_internal_step:
  fixes P P' :: "('procS, 'procT) Proc"
    and α    :: "('labS, 'labT) Lab"
  assumes "P ─α→(STLCal Source Target) P'"
  shows "α ≠ SourceLabel (τ-Source)" and "α ≠ TargetLabel (τ-Target)"
  using assms
  unfolding STLCal_def
  by auto

lemma no_source_internal_lifting:
  fixes α :: "'labS"
    and β :: "('labS, 'labT) Lab"
  assumes "α ∈SL ⟨P, β⟩"
  shows "β ≠ SourceLabel (τ-Source)"
  using assms
  unfolding getSourceLabel_def
  by blast

lemma no_target_internal_lifting:
  fixes α :: "'labT"
    and β :: "('labS, 'labT) Lab"
  assumes "α ∈TL ⟨P, β⟩"
  shows "β ≠ TargetLabel (τ-Target)"
  using assms
  unfolding getTargetLabel_def
  by blast

lemma internalST_iff_internal:
  shows "τ-STLCal = τ-(STLCal Source Target)"
  by (simp add: STLCal_def)

lemma lifted_label_is_unique:
  fixes α :: "'labS"
    and β :: "'labT"
    and γ :: "('labS, 'labT) Lab"
  assumes "α ∈SL ⟨P, γ⟩"
      and "β ∈TL ⟨P, γ⟩"
    shows False
  using assms
  unfolding getSourceLabel_def getTargetLabel_def
  by blast

text ‹A labelled step of a term in Proc is either a labelled source term step or a labelled target
      term step.›

abbreviation labelledStepST
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ ('procS, 'procT) Proc ⇒ bool"
  (‹_ ─_→ST _› [70, 70, 70] 80) where
  "P ─α→ST P' ≡ (∃S β S'. S ∈S P ∧ β ∈SL ⟨P, α⟩ ∧ S' ∈S P' ∧ S ─β→Source S') ∨
                  (∃T β T'. T ∈T P ∧ β ∈TL ⟨P, α⟩ ∧ T' ∈T P' ∧ T ─β→Target T')"

lemma labelledStepST_STLCal_labelledStep:
  fixes P P' :: "('procS, 'procT) Proc"
    and α    :: "('labS, 'labT) Lab"
  shows "P ─α→(STLCal Source Target) P' = P ─α→ST P'"
  unfolding STLCal_def getSourceLabel_def getTargetLabel_def
  by auto

lemma labelledSTStep_labelledStep:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
    and α  :: "('labS, 'labT) Lab"
  shows "SourceTerm S ─α→ST P' = (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source S')"
    and "TargetTerm T ─α→ST P' = (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target T')"
  by blast+

lemma STLCal_labelledStep:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
    and α  :: "('labS, 'labT) Lab"
  shows "SourceTerm S ─α→(STLCal Source Target) P' =
         (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source S')"
    and "TargetTerm T ─α→(STLCal Source Target) P' =
         (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target T')"
  unfolding STLCal_def getSourceLabel_def getTargetLabel_def
  by auto

text ‹A weak internal step of a term in Proc is either a weak internal source step or a weak
      internal target step.›

abbreviation weakTauStepST
  :: "('procS, 'procT) Proc ⇒ ('procS, 'procT) Proc ⇒ bool" (‹_ →ST* _› [70, 70] 80) where
  "P →ST* P' ≡ (∃S S'. S ∈S P ∧ S' ∈S P' ∧ S →Source* S') ∨
                (∃T T'. T ∈T P ∧ T' ∈T P' ∧ T →Target* T')"

lemma STWeakTauSteps_weakTauSteps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S →ST* P' = (∃S'. S' ∈S P' ∧ S →Source* S')"
    and "TargetTerm T →ST* P' = (∃T'. T' ∈T P' ∧ T →Target* T')"
  by blast+

lemma STLCal_weakTauSteps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S →(STLCal Source Target)* P' = (∃S'. S' ∈S P' ∧ S →Source* S')"
    and "TargetTerm T →(STLCal Source Target)* P' = (∃T'. T' ∈T P' ∧ T →Target* T')"
proof auto
  define P :: "('procS, 'procT) Proc" where def_P: "P = SourceTerm S"
  define Cal where def_Cal: "Cal = STLCal Source Target"
  assume "SourceTerm S →(STLCal Source Target)* P'"
  with def_P def_Cal have "P →Cal* P'"
    by simp
  from this def_P def_Cal show "∃S'. S' ∈S P' ∧ S →Source* S'"
  proof (induct)
    case (WTS_refl P Cal)
    assume "S ∈S P"
    moreover have "S →Source* S"
      using weakTauStep.WTS_refl[of S Source]
      by simp
    ultimately show "∃S'. S' ∈S P ∧ S →Source* S'"
      by blast
  next
    case (WTS_trans P Cal P' P'')
    from WTS_trans(2)
    have IH: "S ∈S P ∧ Cal = STLCal Source Target ⟹ ∃S'. S' ∈S P' ∧ S →Source* S'"
      by simp
    assume "S ∈S P" and A1: "Cal = STLCal Source Target"
    with IH obtain S' where A2: "S' ∈S P'" and A3: "S →Source* S'"
      by blast
    assume "P' ─τ-Cal→Cal P''"
    with A1 A2 obtain β S'' where A4: "β ∈SL ⟨P', τ-Cal⟩" and A5: "S'' ∈S P''"
                              and A6: "S' ─β→Source S''"
      using STLCal_labelledStep(1)[of S' "τ-Cal" P'']
      by blast
    from A1 A3 A4 A6 have "S →Source* S''"
      using weakTauStep.WTS_trans[of S Source S' S'']
      unfolding getSourceLabel_def
      by (simp add: STLCal_def)
    with A5 show "∃S''. S'' ∈S P'' ∧ S →Source* S''"
      by blast
  qed
next
  fix S'
  define Cal where def_Cal: "Cal = Source"
  assume "S →Source* S'"
  with def_Cal have "S →Cal* S'"
    by simp
  from this def_Cal show "SourceTerm S →(STLCal Source Target)* (SourceTerm S')"
  proof (induct)
    case (WTS_refl S Cal)
    show "SourceTerm S →(STLCal Source Target)* SourceTerm S"
      using weakTauStep.WTS_refl[of "SourceTerm S" "STLCal Source Target"]
      by simp
  next
    case (WTS_trans S Cal S' S'')
    assume "Cal = Source ⟹ SourceTerm S →(STLCal Source Target)* SourceTerm S'"
       and A: "Cal = Source"
    hence "SourceTerm S →(STLCal Source Target)* SourceTerm S'"
      by simp
    moreover assume "S' ─τ-Cal→Cal S''"
    with A have "SourceTerm S' ─τ-(STLCal Source Target)→(STLCal Source Target) (SourceTerm S'')"
      using STLCal_labelledStep(1)[of S' "τ-STLCal" "SourceTerm S''"]
      by (simp add: STLCal_def)
    ultimately show "SourceTerm S →(STLCal Source Target)* SourceTerm S''"
      using weakTauStep.WTS_trans[of "SourceTerm S" "STLCal Source Target" "SourceTerm S'"
              "SourceTerm S''"]
      by simp
  qed
next
  define P :: "('procS, 'procT) Proc" where def_P: "P = TargetTerm T"
  define Cal where def_Cal: "Cal = STLCal Source Target"
  assume "TargetTerm T →(STLCal Source Target)* P'"
  with def_P def_Cal have "P →Cal* P'"
    by simp
  from this def_P def_Cal show "∃T'. T' ∈T P' ∧ T →Target* T'"
  proof induct
    case (WTS_refl P Cal)
    assume "T ∈T P"
    moreover have "T →Target* T"
      using weakTauStep.WTS_refl[of T Target]
      by simp
    ultimately show "∃T'. T' ∈T P ∧ T →Target* T'"
      by blast
  next
    case (WTS_trans P Cal P' P'')
    from WTS_trans(2)
    have IH: "T ∈T P ∧ Cal = STLCal Source Target ⟹ ∃T'. T' ∈T P' ∧ T →Target* T'"
      by simp
    assume "T ∈T P" and A1: "Cal = STLCal Source Target"
    with IH obtain T' where A2: "T' ∈T P'" and A3: "T →Target* T'"
      by blast
    assume "P' ─τ-Cal→Cal P''"
    with A1 A2 obtain β T'' where A4: "β ∈TL ⟨P', τ-Cal⟩" and A5: "T'' ∈T P''"
                              and A6: "T' ─β→Target T''"
      using STLCal_labelledStep(2)[of T' "τ-Cal" P'']
      by blast
    from A1 A3 A4 A6 have "T →Target* T''"
      using weakTauStep.WTS_trans[of T Target T' T'']
      unfolding getTargetLabel_def
      by (simp add: STLCal_def)
    with A5 show "∃T''. T'' ∈T P'' ∧ T →Target* T''"
      by blast
  qed
next
  fix T'
  define Cal where def_Cal: "Cal = Target"
  assume "T →Target* T'"
  with def_Cal have "T →Cal* T'"
    by simp
  from this def_Cal show "TargetTerm T →(STLCal Source Target)* (TargetTerm T')"
  proof (induct)
    case (WTS_refl T Cal)
    show "TargetTerm T →(STLCal Source Target)* TargetTerm T"
      using weakTauStep.WTS_refl[of "TargetTerm T" "STLCal Source Target"]
      by simp
  next
    case (WTS_trans T Cal T' T'')
    assume "Cal = Target ⟹ TargetTerm T →(STLCal Source Target)* TargetTerm T'"
       and A: "Cal = Target"
    hence "TargetTerm T →(STLCal Source Target)* TargetTerm T'"
      by simp
    moreover assume "T' ─τ-Cal→Cal T''"
    with A have "TargetTerm T' ─τ-(STLCal Source Target)→(STLCal Source Target) (TargetTerm T'')"
      using STLCal_labelledStep(2)[of T' "τ-STLCal" "TargetTerm T''"]
      by (simp add: STLCal_def)
    ultimately show "TargetTerm T →(STLCal Source Target)* TargetTerm T''"
      using weakTauStep.WTS_trans[of "TargetTerm T" "STLCal Source Target" "TargetTerm T'"
              "TargetTerm T''"]
      by simp
  qed
qed

lemma weakTauStepsST_STLCal_weakTauSteps:
  fixes P P' :: "('procS, 'procT) Proc"
  shows "P →(STLCal Source Target)* P' = P →ST* P'"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P →(STLCal Source Target)* P' = P →ST* P'"
    using STLCal_weakTauSteps(1)[where S="SP" and P'="P'"]
          STWeakTauSteps_weakTauSteps(1)[where S="SP" and P'="P'"]
    by blast
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P →(STLCal Source Target)* P' = P →ST* P'"
    using STLCal_weakTauSteps(2)[where T="TP" and P'="P'"]
          STWeakTauSteps_weakTauSteps(2)[where T="TP" and P'="P'"]
    by blast
qed

lemma weakTauStepsST_refl:
  fixes P :: "('procS, 'procT) Proc"
  shows "P →ST* P"
  by (cases P, simp_all add: WTS_refl)

lemma weakTauStepsST_trans:
  fixes P Q R :: "('procS, 'procT) Proc"
  assumes A1: "P →ST* Q"
      and A2: "Q →ST* R"
  shows "P →ST* R"
proof -
  from A1 have "P →(STLCal Source Target)* Q"
    by (simp add: weakTauStepsST_STLCal_weakTauSteps)
  moreover from A2 have "Q →(STLCal Source Target)* R"
    by (simp add: weakTauStepsST_STLCal_weakTauSteps)
  ultimately have "P →(STLCal Source Target)* R"
    by (rule weakTauSteps_trans)
  thus "P →ST* R"
    by (simp add: weakTauStepsST_STLCal_weakTauSteps)
qed

text ‹A weak labelled step of a term in Proc is either a weak labelled source step or a weak
      labelled target step.›

abbreviation weakLabelledActionStepST
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ ('procS, 'procT) Proc ⇒ bool"
  (‹_ ─_→ST* _› [70, 70, 70] 80) where
  "P ─α→ST* P' ≡ (∃S β S'. S ∈S P ∧ β ∈SL ⟨P, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S') ∨
                   (∃T β T'. T ∈T P ∧ β ∈TL ⟨P, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T')"

abbreviation weakLabelledStepST
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ ('procS, 'procT) Proc ⇒ bool"
  (‹_ ─⁀_→ST* _› [70, 70, 70] 80) where
  "P ─⁀α→ST* P' ≡ (∃S β S'. S ∈S P ∧ β ∈SL ⟨P, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S') ∨
                    (∃T β T'. T ∈T P ∧ β ∈TL ⟨P, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T')"

lemma STWeakLabelledActionSteps_weakLabelledActionSteps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and α  :: "('labS, 'labT) Lab"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ─α→ST* P' = (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S')"
    and "TargetTerm T ─α→ST* P' = (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T')"
  by blast+

lemma STWeakLabelledSteps_weakLabelledSteps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and α  :: "('labS, 'labT) Lab"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ─⁀α→ST* P' =
         (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S')"
    and "TargetTerm T ─⁀α→ST* P' =
         (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T')"
  by blast+

lemma STLCal_weakLabelledActionSteps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and α  :: "('labS, 'labT) Lab"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ─α→(STLCal Source Target)* P' =
         (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S')"
    and "TargetTerm T ─α→(STLCal Source Target)* P' =
         (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T')"
proof -
  have "SourceTerm S ─α→(STLCal Source Target)* P' ⟹
        (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S')"
  proof (cases "α = τ-STLCal")
    assume "SourceTerm S ─α→(STLCal Source Target)* P'" and "α = τ-STLCal"
    hence False
      unfolding STLCal_def weakLabelledActionStep_def
      by simp
    thus "∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S'"
      by simp
  next
    assume "SourceTerm S ─α→(STLCal Source Target)* P'" and A1: "α ≠ τ-STLCal"
    then obtain Q Q' where A2: "SourceTerm S →(STLCal Source Target)* Q"
                       and A3: "Q ─α→(STLCal Source Target) Q'"
                       and A4: "Q' →(STLCal Source Target)* P'"
      unfolding weakLabelledActionStep_def
      using internalST_iff_internal
      by blast
    from A2 obtain S' where A5: "S' ∈S Q" and A6: "S →Source* S'"
      using STLCal_weakTauSteps(1)[of S Q]
      by blast
    from A1 A3 A5 obtain β S'' where A7: "β ∈SL ⟨SourceTerm S, α⟩" and A8: "S'' ∈S Q'"
                                 and A9: "S' ─β→Source S''"
      unfolding STLCal_def getSourceLabel_def
      by auto
    from A4 A8 obtain S''' where A10: "S''' ∈S P'" and A11: "S'' →Source* S'''"
      using STLCal_weakTauSteps(1)[of S'' P']
      by blast
    from A1 A6 A7 A9 A11 have "S ─β→Source* S'''"
      unfolding weakLabelledActionStep_def getSourceLabel_def
      by blast
    with A7 A10 show "∃β S'''. β ∈SL ⟨SourceTerm S, α⟩ ∧ S''' ∈S P' ∧ S ─β→Source* S'''"
      by blast
  qed
  moreover have "(∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S') ⟹
                 SourceTerm S ─α→(STLCal Source Target)* P'"
  proof -
    assume "∃β S'''. β ∈SL ⟨SourceTerm S, α⟩ ∧ S''' ∈S P' ∧ S ─β→Source* S'''"
    then obtain β S''' where A1: "β ∈SL ⟨SourceTerm S, α⟩" and A2: "S''' ∈S P'"
                         and A3: "S ─β→Source* S'''"
      by blast
    from A3 obtain S' S'' where A4: "β ≠ τ-Source" and A5: "S →Source* S'"
                            and A6: "S' ─β→Source S''" and A7: "S'' →Source* S'''"
      unfolding weakLabelledActionStep_def
      by blast
    from A1 A4 have "α ≠ τ-(STLCal Source Target)"
      unfolding STLCal_def getSourceLabel_def
      by simp
    moreover from A5 have "SourceTerm S →(STLCal Source Target)* SourceTerm S'"
      using STLCal_weakTauSteps(1)[of S "SourceTerm S'"]
      by simp
    moreover from A1 A4 A6 have "SourceTerm S' ─α→(STLCal Source Target) (SourceTerm S'')"
      using STLCal_labelledStep(1)[of S' α "SourceTerm S''"]
      unfolding getSourceLabel_def
      by simp
    moreover from A2 A7 have "SourceTerm S'' →(STLCal Source Target)* P'"
      using STLCal_weakTauSteps(1)[of S'' P']
      by simp
    ultimately show "SourceTerm S ─α→(STLCal Source Target)* P'"
      unfolding weakLabelledActionStep_def
      by blast
  qed
  ultimately show "SourceTerm S ─α→(STLCal Source Target)* P' =
                   (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─β→Source* S')"
    by auto
  have "TargetTerm T ─α→(STLCal Source Target)* P' ⟹
        (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T')"
  proof (cases "α = τ-STLCal")
    assume "TargetTerm T ─α→(STLCal Source Target)* P'" and "α = τ-STLCal"
    hence False
      unfolding STLCal_def weakLabelledActionStep_def
      by simp
    thus "∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T'"
      by simp
  next
    assume "TargetTerm T ─α→(STLCal Source Target)* P'" and A1: "α ≠ τ-STLCal"
    then obtain Q Q' where A2: "TargetTerm T →(STLCal Source Target)* Q"
                       and A3: "Q ─α→(STLCal Source Target) Q'"
                       and A4: "Q' →(STLCal Source Target)* P'"
      unfolding weakLabelledActionStep_def
      using internalST_iff_internal
      by blast
    from A2 obtain T' where A5: "T' ∈T Q" and A6: "T →Target* T'"
      using STLCal_weakTauSteps(2)[of T Q]
      by blast
    from A1 A3 A5 obtain β T'' where A7: "β ∈TL ⟨TargetTerm T, α⟩" and A8: "T'' ∈T Q'"
                                 and A9: "T' ─β→Target T''"
      unfolding STLCal_def getTargetLabel_def
      by auto
    from A4 A8 obtain T''' where A10: "T''' ∈T P'" and A11: "T'' →Target* T'''"
      using STLCal_weakTauSteps(2)[of T'' P']
      by blast
    from A1 A6 A7 A9 A11 have "T ─β→Target* T'''"
      unfolding weakLabelledActionStep_def getTargetLabel_def
      by blast
    with A7 A10 show "∃β T'''. β ∈TL ⟨TargetTerm T, α⟩ ∧ T''' ∈T P' ∧ T ─β→Target* T'''"
      by blast
  qed
  moreover have "(∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T') ⟹
                 TargetTerm T ─α→(STLCal Source Target)* P'"
  proof -
    assume "∃β T'''. β ∈TL ⟨TargetTerm T, α⟩ ∧ T''' ∈T P' ∧ T ─β→Target* T'''"
    then obtain β T''' where A1: "β ∈TL ⟨TargetTerm T, α⟩" and A2: "T''' ∈T P'"
                         and A3: "T ─β→Target* T'''"
      by blast
    from A3 obtain T' T'' where A4: "β ≠ τ-Target" and A5: "T →Target* T'"
                            and A6: "T' ─β→Target T''" and A7: "T'' →Target* T'''"
      unfolding weakLabelledActionStep_def
      by blast
    from A1 A4 have "α ≠ τ-(STLCal Source Target)"
      unfolding STLCal_def getTargetLabel_def
      by simp
    moreover from A5 have "TargetTerm T →(STLCal Source Target)* TargetTerm T'"
      using STLCal_weakTauSteps(2)[of T "TargetTerm T'"]
      by simp
    moreover from A1 A4 A6 have "TargetTerm T' ─α→(STLCal Source Target) (TargetTerm T'')"
      using STLCal_labelledStep(2)[of T' α "TargetTerm T''"]
      unfolding getTargetLabel_def
      by simp
    moreover from A2 A7 have "TargetTerm T'' →(STLCal Source Target)* P'"
      using STLCal_weakTauSteps(2)[of T'' P']
      by simp
    ultimately show "TargetTerm T ─α→(STLCal Source Target)* P'"
      unfolding weakLabelledActionStep_def
      by blast
  qed
  ultimately show "TargetTerm T ─α→(STLCal Source Target)* P' =
                   (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─β→Target* T')"
    by auto
qed

lemma STLCal_weakLabelledSteps:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and α  :: "('labS, 'labT) Lab"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ─⁀α→(STLCal Source Target)* P' =
         (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S')"
    and "TargetTerm T ─⁀α→(STLCal Source Target)* P' =
         (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T')"
proof -
  have "SourceTerm S ─⁀α→(STLCal Source Target)* P' ⟹
        (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S')"
  proof (cases "α = τ-STLCal")
    assume A1: "α = τ-STLCal"
    then have A2: "(τ-Source) ∈SL ⟨SourceTerm S, α⟩"
      unfolding getSourceLabel_def
      by simp
    assume "SourceTerm S ─⁀α→(STLCal Source Target)* P'"
    with A1 have "SourceTerm S →(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      using internalST_iff_internal
      by simp
    then obtain S' where A3: "S' ∈S P'" and A4: "S →Source* S'"
      using STLCal_weakTauSteps(1)[of S P']
      by blast
    from A4 have "S ─⁀(τ-Source)→Source* S'"
      unfolding weakLabelledStep_def
      by simp
    with A2 A3 show "∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S'"
      by blast
  next
    assume "SourceTerm S ─⁀α→(STLCal Source Target)* P'" and A1: "α ≠ τ-STLCal"
    hence "SourceTerm S ─α→(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      using internalST_iff_internal
      by simp
    then obtain β S' where A2: "β ∈SL ⟨SourceTerm S, α⟩" and A3: "S' ∈S P'"
                       and A4: "S ─β→Source* S'"
      using STLCal_weakLabelledActionSteps(1)[of S α P']
      by blast
    from A1 A2 A4 have "S ─⁀β→Source* S'"
      unfolding weakLabelledStep_def getSourceLabel_def
      by simp
    with A2 A3 show "∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S'"
      by blast
  qed
  moreover have "(∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S') ⟹
                 SourceTerm S ─⁀α→(STLCal Source Target)* P'"
  proof -
    assume "∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S'"
    then obtain β S' where A1: "β ∈SL ⟨SourceTerm S, α⟩" and A2: "S' ∈S P'"
                       and A3: "S ─⁀β→Source* S'"
      by blast
    from A1 show "SourceTerm S ─⁀α→(STLCal Source Target)* P'"
      unfolding getSourceLabel_def
    proof auto
      assume B: "β ≠ τ-Source"
      with A3 have "S ─β→Source* S'"
        unfolding weakLabelledStep_def
        by simp
      with A2 B have "SourceTerm S ─(SourceLabel β)→(STLCal Source Target)* P'"
        using STLCal_weakLabelledActionSteps(1)[of S "SourceLabel β" P']
        unfolding getSourceLabel_def
        by simp
      thus "SourceTerm S ─⁀(SourceLabel β)→(STLCal Source Target)* P'"
        unfolding weakLabelledStep_def weakLabelledActionStep_def
        by simp
    next
      assume "β = τ-Source"
      with A3 have "S →Source* S'"
        unfolding weakLabelledStep_def
        by simp
      with A2 have "SourceTerm S →(STLCal Source Target)* P'"
        using STLCal_weakTauSteps(1)[of S P']
        by simp
      thus "SourceTerm S ─⁀τ-STLCal→(STLCal Source Target)* P'"
        unfolding weakLabelledStep_def
        using internalST_iff_internal
        by simp
    qed
  qed
  ultimately show "SourceTerm S ─⁀α→(STLCal Source Target)* P' =
                   (∃β S'. β ∈SL ⟨SourceTerm S, α⟩ ∧ S' ∈S P' ∧ S ─⁀β→Source* S')"
    by blast
next
  have "TargetTerm T ─⁀α→(STLCal Source Target)* P' ⟹
        (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T')"
  proof (cases "α = τ-STLCal")
    assume A1: "α = τ-STLCal"
    then have A2: "(τ-Target) ∈TL ⟨TargetTerm T, α⟩"
      unfolding getTargetLabel_def
      by simp
    assume "TargetTerm T ─⁀α→(STLCal Source Target)* P'"
    with A1 have "TargetTerm T →(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      using internalST_iff_internal
      by simp
    then obtain T' where A3: "T' ∈T P'" and A4: "T →Target* T'"
      using STLCal_weakTauSteps(2)[of T P']
      by blast
    from A4 have "T ─⁀(τ-Target)→Target* T'"
      unfolding weakLabelledStep_def
      by simp
    with A2 A3 show "∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T'"
      by blast
  next
    assume "TargetTerm T ─⁀α→(STLCal Source Target)* P'" and A1: "α ≠ τ-STLCal"
    hence "TargetTerm T ─α→(STLCal Source Target)* P'"
      unfolding weakLabelledStep_def
      using internalST_iff_internal
      by simp
    then obtain β T' where A2: "β ∈TL ⟨TargetTerm T, α⟩" and A3: "T' ∈T P'"
                       and A4: "T ─β→Target* T'"
      using STLCal_weakLabelledActionSteps(2)[of T α P']
      by blast
    from A1 A2 A4 have "T ─⁀β→Target* T'"
      unfolding weakLabelledStep_def getTargetLabel_def
      by simp
    with A2 A3 show "∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T'"
      by blast
  qed
  moreover have "(∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T') ⟹
                 TargetTerm T ─⁀α→(STLCal Source Target)* P'"
  proof -
    assume "∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T'"
    then obtain β T' where A1: "β ∈TL ⟨TargetTerm T, α⟩" and A2: "T' ∈T P'"
                       and A3: "T ─⁀β→Target* T'"
      by blast
    from A1 show "TargetTerm T ─⁀α→(STLCal Source Target)* P'"
      unfolding getTargetLabel_def
    proof auto
      assume B: "β ≠ τ-Target"
      with A3 have "T ─β→Target* T'"
        unfolding weakLabelledStep_def
        by simp
      with A2 B have "TargetTerm T ─(TargetLabel β)→(STLCal Source Target)* P'"
        using STLCal_weakLabelledActionSteps(2)[of T "TargetLabel β" P']
        unfolding getTargetLabel_def
        by simp
      thus "TargetTerm T ─⁀(TargetLabel β)→(STLCal Source Target)* P'"
        unfolding weakLabelledStep_def weakLabelledActionStep_def
        by simp
    next
      assume "β = τ-Target"
      with A3 have "T →Target* T'"
        unfolding weakLabelledStep_def
        by simp
      with A2 have "TargetTerm T →(STLCal Source Target)* P'"
        using STLCal_weakTauSteps(2)[of T P']
        by simp
      thus "TargetTerm T ─⁀τ-STLCal→(STLCal Source Target)* P'"
        unfolding weakLabelledStep_def
        using internalST_iff_internal
        by simp
    qed
  qed
  ultimately show "TargetTerm T ─⁀α→(STLCal Source Target)* P' =
                   (∃β T'. β ∈TL ⟨TargetTerm T, α⟩ ∧ T' ∈T P' ∧ T ─⁀β→Target* T')"
    by blast
qed

lemma weakLabelledActionStepsST_STLCal_weakLabelledActionSteps:
  fixes P P' :: "('procS, 'procT) Proc"
    and α    :: "('labS, 'labT) Lab"
  shows "P ─α→(STLCal Source Target)* P' = P ─α→ST* P'"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ─α→(STLCal Source Target)* P' = P ─α→ST* P'"
    using STLCal_weakLabelledActionSteps(1)[of SP α P']
    by blast
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ─α→(STLCal Source Target)* P' = P ─α→ST* P'"
    using STLCal_weakLabelledActionSteps(2)[of TP α P']
    by blast
qed

lemma weakLabelledStepsST_STLCal_weakLabelledSteps:
  fixes P P' :: "('procS, 'procT) Proc"
    and α    :: "('labS, 'labT) Lab"
  shows "P ─⁀α→(STLCal Source Target)* P' = P ─⁀α→ST* P'"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ─⁀α→(STLCal Source Target)* P' = P ─⁀α→ST* P'"
    using STLCal_weakLabelledSteps(1)[of SP α P']
    by blast
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ─⁀α→(STLCal Source Target)* P' = P ─⁀α→ST* P'"
    using STLCal_weakLabelledSteps(2)[of TP α P']
    by blast
qed

text ‹A sequence of weak labelled steps of a term in Proc is either a sequence of weak labelled
      source term steps or a sequence of weak labelled target term steps.›

abbreviation weakLabelledSequenceST
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab list ⇒ ('procS, 'procT) Proc ⇒ bool"
  (‹_ ─⌢_→ST* _› [70, 70, 70] 80) where
  "P ─⌢w→ST* P' ≡ (∃S v S'. S ∈S P ∧ v ∈SL* ⟨P, w⟩ ∧ S' ∈S P' ∧ S ─⌢v→Source* S') ∨
                     (∃T v T'. T ∈T P ∧ v ∈TL* ⟨P, w⟩ ∧ T' ∈T P' ∧ T ─⌢v→Target* T')"

lemma lifted_word_on_source_labels_kinds:
  fixes v :: "'labS list"
    and P :: "('procS, 'procT) Proc"
    and w :: "('labS, 'labT) Lab list"
  assumes "v ∈SL* ⟨P, w⟩"
  shows "∀α ∈ set w. α ∈ LabS ∨ α = τ-STLCal" and "P ∈ ProcS"
  using assms
  by (induct, auto simp add: isSourceLabel_def getSourceLabel_def)

lemma lifted_word_on_target_labels_kinds:
  fixes v :: "'labT list"
    and P :: "('procS, 'procT) Proc"
    and w :: "('labS, 'labT) Lab list"
  assumes "v ∈TL* ⟨P, w⟩"
  shows "∀α ∈ set w. α ∈ LabT ∨ α = τ-STLCal" and "P ∈ ProcT"
  using assms
  by (induct, auto simp add: isTargetLabel_def getTargetLabel_def)

lemma lift_word_on_source_labels:
  fixes w :: "'labS list"
  shows "∃P v. w ∈SL* ⟨P, v⟩"
proof (induct w rule: rev_induct)
  case Nil
  show "∃P v. [] ∈SL* ⟨P, v⟩"
    using SLNil
    by blast
next
  case (snoc α w)
  assume "∃P v. w ∈SL* ⟨P, v⟩"
  then obtain P v where "w ∈SL* ⟨P, v⟩"
    by blast
  moreover obtain Q β where "α ∈SL ⟨Q, β⟩" and "Q ∈ ProcS"
    unfolding getSourceLabel_def
    by blast
  ultimately show "∃P v'. (w@[α]) ∈SL* ⟨P, v'⟩"
    using SLCons[of w P v α Q β]
    by blast
qed

lemma lift_word_on_target_labels:
  fixes w :: "'labT list"
  shows "∃P v. w ∈TL* ⟨P, v⟩"
proof (induct w rule: rev_induct)
  case Nil
  show "∃P v. [] ∈TL* ⟨P, v⟩"
    using TLNil
    by blast
next
  case (snoc α w)
  assume "∃P v. w ∈TL* ⟨P, v⟩"
  then obtain P v where "w ∈TL* ⟨P, v⟩"
    by blast
  moreover obtain Q β where "α ∈TL ⟨Q, β⟩" and "Q ∈ ProcT"
    unfolding getTargetLabel_def
    by blast
  ultimately show "∃P' v'. (w@[α]) ∈TL* ⟨P', v'⟩"
    using TLCons[of w P v α Q β]
    by blast
qed

lemma lift_source_word_length:
  fixes w :: "'labS list"
    and P :: "('procS, 'procT) Proc"
    and v :: "('labS, 'labT) Lab list"
  assumes "w ∈SL* ⟨P, v⟩"
  shows "length w = length v" and "P ∈ ProcS"
  using assms
  by (induct, simp_all)

lemma lift_target_word_length:
  fixes w :: "'labT list"
    and P :: "('procS, 'procT) Proc"
    and v :: "('labS, 'labT) Lab list"
  assumes "w ∈TL* ⟨P, v⟩"
  shows "length w = length v" and "P ∈ ProcT"
  using assms
  by (induct, simp_all)

lemma lift_composed_word_on_source_labels:
  fixes v  :: "'labS list"
    and β  :: "'labS"
    and P  :: "('procS, 'procT) Proc"
    and w' :: "('labS, 'labT) Lab list"
  assumes lifting: "(v@[β]) ∈SL* ⟨P, w'⟩"
  shows "∃w α. w' = w@[α] ∧ v ∈SL* ⟨P, w⟩ ∧ β ∈SL ⟨P, α⟩"
proof -
  define v' where v'_def: "v' = v@[β]"
  with lifting have "v' ∈SL* ⟨P, w'⟩"
    by simp
  from this v'_def show "∃w α. w' = w@[α] ∧ v ∈SL* ⟨P, w⟩ ∧ β ∈SL ⟨P, α⟩"
  proof induct
    case (SLNil P)
    assume "[] = v@[β]"
    hence False
      by simp
    thus "∃w α. [] = w@[α] ∧ v ∈SL* ⟨P, w⟩ ∧ β ∈SL ⟨P, α⟩"
      by simp
  next
    case (SLCons v' P w β' Q α)
    assume "v'@[β'] = v@[β]"
    hence A1: "v' = v" and A2: "β' = β"
      by simp_all
    assume "v' ∈SL* ⟨P, w⟩"
    with A1 have A3: "v ∈SL* ⟨P, w⟩"
      by simp
    hence A4: "P ∈ ProcS"
      using lift_source_word_length(2)[of v P w]
      by simp
    assume "β' ∈SL ⟨Q, α⟩"
    with A2 A4 have "β ∈SL ⟨P, α⟩"
      unfolding getSourceLabel_def
      by simp
    with A3 show "∃w' α'. w@[α] = w'@[α'] ∧ v ∈SL* ⟨P, w'⟩ ∧ β ∈SL ⟨P, α'⟩"
      by blast
  qed
qed

lemma lift_composed_word_on_target_labels:
  fixes v  :: "'labT list"
    and β  :: "'labT"
    and P  :: "('procS, 'procT) Proc"
    and w' :: "('labS, 'labT) Lab list"
  assumes lifting: "(v@[β]) ∈TL* ⟨P, w'⟩"
  shows "∃w α. w' = w@[α] ∧ v ∈TL* ⟨P, w⟩ ∧ β ∈TL ⟨P, α⟩"
proof -
  define v' where v'_def: "v' = v@[β]"
  with lifting have "v' ∈TL* ⟨P, w'⟩"
    by simp
  from this v'_def show "∃w α. w' = w@[α] ∧ v ∈TL* ⟨P, w⟩ ∧ β ∈TL ⟨P, α⟩"
  proof induct
    case (TLNil P)
    assume "[] = v@[β]"
    hence False
      by simp
    thus "∃w α. [] = w@[α] ∧ v ∈TL* ⟨P, w⟩ ∧ β ∈TL ⟨P, α⟩"
      by simp
  next
    case (TLCons v' P w β' Q α)
    assume "v'@[β'] = v@[β]"
    hence A1: "v' = v" and A2: "β' = β"
      by simp_all
    assume "v' ∈TL* ⟨P, w⟩"
    with A1 have A3: "v ∈TL* ⟨P, w⟩"
      by simp
    hence A4: "P ∈ ProcT"
      using lift_target_word_length(2)[of v P w]
      by simp
    assume "β' ∈TL ⟨Q, α⟩"
    with A2 A4 have "β ∈TL ⟨P, α⟩"
      unfolding getTargetLabel_def
      by simp
    with A3 show "∃w' α'. w@[α] = w'@[α'] ∧ v ∈TL* ⟨P, w'⟩ ∧ β ∈TL ⟨P, α'⟩"
      by blast
  qed
qed

lemma lifted_composed_word_on_source_labels:
  fixes v' :: "'labS list"
    and P  :: "('procS, 'procT) Proc"
    and w  :: "('labS, 'labT) Lab list"
    and α  :: "('labS, 'labT) Lab"
  assumes lifting: "v' ∈SL* ⟨P, (w@[α])⟩"
  shows "∃v β. v' = v@[β] ∧ v ∈SL* ⟨P, w⟩ ∧ β ∈SL ⟨P, α⟩"
proof -
  define w' where w'_def: "w' = w@[α]"
  with lifting have "v' ∈SL* ⟨P, w'⟩"
    by simp
  from this w'_def show "∃v β. v' = v@[β] ∧ v ∈SL* ⟨P, w⟩ ∧ β ∈SL ⟨P, α⟩"
  proof induct
    case (SLNil P)
    assume "[] = w@[α]"
    hence False
      by simp
    thus "∃v β. [] = v@[β] ∧ v ∈SL* ⟨P, w⟩ ∧ β ∈SL ⟨P, α⟩"
      by simp
  next
    case (SLCons v P w' β Q α')
    assume "w'@[α'] = w@[α]"
    hence A1: "w' = w" and A2: "α' = α"
      by simp_all
    assume "v ∈SL* ⟨P, w'⟩"
    with A1 have A3: "v ∈SL* ⟨P, w⟩"
      by simp
    hence A4: "P ∈ ProcS"
      using lift_source_word_length(2)[of v P w]
      by simp
    assume "β ∈SL ⟨Q, α'⟩"
    with A2 A4 have "β ∈SL ⟨P, α⟩"
      unfolding getSourceLabel_def
      by simp
    with A3 show "∃v' β'. v@[β] = v'@[β'] ∧ v' ∈SL* ⟨P, w⟩ ∧ β' ∈SL ⟨P, α⟩"
      by blast
  qed
qed

lemma lifted_composed_word_on_target_labels:
  fixes v' :: "'labT list"
    and P  :: "('procS, 'procT) Proc"
    and w  :: "('labS, 'labT) Lab list"
    and α  :: "('labS, 'labT) Lab"
  assumes lifting: "v' ∈TL* ⟨P, (w@[α])⟩"
  shows "∃v β. v' = v@[β] ∧ v ∈TL* ⟨P, w⟩ ∧ β ∈TL ⟨P, α⟩"
proof -
  define w' where w'_def: "w' = w@[α]"
  with lifting have "v' ∈TL* ⟨P, w'⟩"
    by simp
  from this w'_def show "∃v β. v' = v@[β] ∧ v ∈TL* ⟨P, w⟩ ∧ β ∈TL ⟨P, α⟩"
  proof induct
    case (TLNil P)
    assume "[] = w@[α]"
    hence False
      by simp
    thus "∃v β. [] = v@[β] ∧ v ∈TL* ⟨P, w⟩ ∧ β ∈TL ⟨P, α⟩"
      by simp
  next
    case (TLCons v P w' β Q α')
    assume "w'@[α'] = w@[α]"
    hence A1: "w' = w" and A2: "α' = α"
      by simp_all
    assume "v ∈TL* ⟨P, w'⟩"
    with A1 have A3: "v ∈TL* ⟨P, w⟩"
      by simp
    hence A4: "P ∈ ProcT"
      using lift_target_word_length(2)[of v P w]
      by simp
    assume "β ∈TL ⟨Q, α'⟩"
    with A2 A4 have "β ∈TL ⟨P, α⟩"
      unfolding getTargetLabel_def
      by simp
    with A3 show "∃v' β'. v@[β] = v'@[β'] ∧ v' ∈TL* ⟨P, w⟩ ∧ β' ∈TL ⟨P, α⟩"
      by blast
  qed
qed

lemma lifted_word_on_source_labels_is_unique:
  fixes v1 v2 :: "'labS list"
    and P     :: "('procS, 'procT) Proc"
    and w     :: "('labS, 'labT) Lab list"
  assumes "v1 ∈SL* ⟨P, w⟩"
      and "v2 ∈SL* ⟨P, w⟩"
    shows "v1 = v2"
  using assms
proof (induct arbitrary: v2)
  case (SLNil P)
  assume "v2 ∈SL* ⟨P, []⟩"
  thus "[] = v2"
    using lift_source_word_length(1)[of v2 P "[]"]
    by simp
next
  case (SLCons v P w β Q α)
  assume "β ∈SL ⟨Q, α⟩" and "v2 ∈SL* ⟨P, (w@[α])⟩"
  then obtain v' where A1: "v2 = v'@[β]" and A2: "v' ∈SL* ⟨P, w⟩"
    using lifted_composed_word_on_source_labels[of v2 P w α]
    unfolding getSourceLabel_def
    by blast
  assume "⋀v'. v' ∈SL* ⟨P, w⟩ ⟹ v = v'"
  with A2 have "v = v'"
    by simp
  with A1 show "v@[β] = v2"
    by simp
qed

lemma lifted_word_on_target_labels_is_unique:
  fixes v1 v2 :: "'labT list"
    and P     :: "('procS, 'procT) Proc"
    and w     :: "('labS, 'labT) Lab list"
  assumes "v1 ∈TL* ⟨P, w⟩"
      and "v2 ∈TL* ⟨P, w⟩"
    shows "v1 = v2"
  using assms
proof (induct arbitrary: v2)
  case (TLNil P)
  assume "v2 ∈TL* ⟨P, []⟩"
  thus "[] = v2"
    using lift_target_word_length(1)[of v2 P "[]"]
    by simp
next
  case (TLCons v P w β Q α)
  assume "β ∈TL ⟨Q, α⟩" and "v2 ∈TL* ⟨P, (w@[α])⟩"
  then obtain v' where A1: "v2 = v'@[β]" and A2: "v' ∈TL* ⟨P, w⟩"
    using lifted_composed_word_on_target_labels[of v2 P w α]
    unfolding getTargetLabel_def
    by blast
  assume "⋀v'. v' ∈TL* ⟨P, w⟩ ⟹ v = v'"
  with A2 have "v = v'"
    by simp
  with A1 show "v@[β] = v2"
    by simp
qed

lemma lifted_word_is_either_source_or_target:
  fixes v1 :: "'labS list"
    and v2 :: "'labT list"
    and P  :: "('procS, 'procT) Proc"
    and w  :: "('labS, 'labT) Lab list"
  assumes v1: "v1 ∈SL* ⟨P, w⟩"
      and v2: "v2 ∈TL* ⟨P, w⟩"
    shows False
proof -
  from v1 have "P ∈ ProcS"
    using lift_source_word_length(2)[of v1 P w]
    by simp
  moreover from v2 have "P ∈ ProcT"
    using lift_target_word_length(2)[of v2 P w]
    by simp
  ultimately show False
    by blast
qed

lemma lifted_non_internal_word_is_either_source_or_target:
  fixes v1  :: "'labS list"
    and v2  :: "'labT list"
    and P Q :: "('procS, 'procT) Proc"
    and w   :: "('labS, 'labT) Lab list"
  assumes "v1 ∈SL* ⟨P, w⟩"
      and "v2 ∈TL* ⟨Q, w⟩"
      and "∃α ∈ set w. α ≠ τ-STLCal"
    shows False
  using assms
proof (induct arbitrary: v2 Q)
  case (SLNil P)
  assume "∃α ∈ set []. α ≠ τ-STLCal"
  thus False
    by simp
next
  case (SLCons v P w β Q' α v2 Q)
  from SLCons(2) have IH: "⋀v2 Q. v2 ∈TL* ⟨Q, w⟩ ∧ (∃α ∈ set w. α ≠ τ-STLCal) ⟹ False"
    by blast
  assume A1: "β ∈SL ⟨Q', α⟩" and A2: "v2 ∈TL* ⟨Q, (w@[α])⟩"
     and A3: "∃α ∈ set (w@[α]). α ≠ τ-STLCal"
  from A2 obtain v2' β' where A4: "v2' ∈TL* ⟨Q, w⟩" and A5: "β' ∈TL ⟨Q, α⟩"
    using lifted_composed_word_on_target_labels[of v2 Q w α]
    by blast
  show False
  proof (cases "α = τ-STLCal")
    assume "α = τ-STLCal"
    with A3 have "∃α ∈ set w. α ≠ τ-STLCal"
      by simp
    with IH A4 show False
      by simp
  next
    assume "α ≠ τ-STLCal"
    with A1 A5 show False
      unfolding getSourceLabel_def getTargetLabel_def
      by simp
  qed
qed

lemma lift_source_word_exchange:
  fixes w   :: "'labS list"
    and v   :: "('labS, 'labT) Lab list"
    and P Q :: "('procS, 'procT) Proc"
  assumes "w ∈SL* ⟨P, v⟩"
      and "Q ∈ ProcS"
    shows "w ∈SL* ⟨Q, v⟩"
  using assms
proof induct
  case (SLNil P)
  assume "Q ∈ ProcS"
  thus "[] ∈SL* ⟨Q, []⟩"
    using getSourceLabels.SLNil[of Q]
    by simp
next
  case (SLCons v P w β P' α)
  assume "Q ∈ ProcS ⟹ v ∈SL* ⟨Q, w⟩" and "Q ∈ ProcS"
  hence "v ∈SL* ⟨Q, w⟩"
    by simp
  moreover assume "β ∈SL ⟨P', α⟩"
  ultimately show "(v@[β]) ∈SL* ⟨Q, (w@[α])⟩"
    using getSourceLabels.SLCons[of v Q w β P' α]
    by simp
qed

lemma lift_target_word_exchange:
  fixes w   :: "'labT list"
    and v   :: "('labS, 'labT) Lab list"
    and P Q :: "('procS, 'procT) Proc"
  assumes "w ∈TL* ⟨P, v⟩"
      and "Q ∈ ProcT"
    shows "w ∈TL* ⟨Q, v⟩"
  using assms
proof induct
  case (TLNil P)
  assume "Q ∈ ProcT"
  thus "[] ∈TL* ⟨Q, []⟩"
    using getTargetLabels.TLNil[of Q]
    by simp
next
  case (TLCons v P w β P' α)
  assume "Q ∈ ProcT ⟹ v ∈TL* ⟨Q, w⟩" and "Q ∈ ProcT"
  hence "v ∈TL* ⟨Q, w⟩"
    by simp
  moreover assume "β ∈TL ⟨P', α⟩"
  ultimately show "(v@[β]) ∈TL* ⟨Q, (w@[α])⟩"
    using getTargetLabels.TLCons[of v Q w β P' α]
    by simp
qed

lemma STWeakLabelledSequence_weakLabelledSequence:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and w  :: "('labS, 'labT) Lab list"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ─⌢w→ST* P' =
         (∃v S'. v ∈SL* ⟨SourceTerm S, w⟩ ∧ S' ∈S P' ∧ S ─⌢v→Source* S')"
    and "TargetTerm T ─⌢w→ST* P' =
         (∃v T'. v ∈TL* ⟨TargetTerm T, w⟩ ∧ T' ∈T P' ∧ T ─⌢v→Target* T')"
  by blast+

lemma STLCal_weakLabelledSequence:
  fixes S  :: "'procS"
    and T  :: "'procT"
    and w  :: "('labS, 'labT) Lab list"
    and P' :: "('procS, 'procT) Proc"
  shows "SourceTerm S ─⌢w→(STLCal Source Target)* P' =
         (∃v S'. v ∈SL* ⟨SourceTerm S, w⟩ ∧ S' ∈S P' ∧ S ─⌢v→Source* S')"
    and "TargetTerm T ─⌢w→(STLCal Source Target)* P' =
         (∃v T'. v ∈TL* ⟨TargetTerm T, w⟩ ∧ T' ∈T P' ∧ T ─⌢v→Target* T')"
proof auto
  define P :: "('procS, 'procT) Proc" where def_P:   "P = SourceTerm S"
  define Cal                          where def_Cal: "Cal = STLCal Source Target"
  assume "SourceTerm S ─⌢w→(STLCal Source Target)* P'"
  with def_P def_Cal have "P ─⌢w→Cal* P'"
    by simp
  from this def_P def_Cal
  show "∃v. v ∈SL* ⟨SourceTerm S, w⟩ ∧ (∃S'. S' ∈S P' ∧ S ─⌢v→Source* S')"
  proof induct
    case (WLS_Nil P Cal P')
    have A1: "[] ∈SL* ⟨SourceTerm S, []⟩"
      using SLNil
      by simp
    assume "P →Cal* P'" and "S ∈S P" and "Cal = STLCal Source Target"
    then obtain S' where A2: "S' ∈S P'" and A3: "S →Source* S'"
      using STLCal_weakTauSteps(1)[of S P']
      by blast
    from A3 have "S ─⌢[]→Source* S'"
      using weakLabelledSequence.WLS_Nil[of S Source S']
      by simp
    with A1 A2 show "∃v. v ∈SL* ⟨SourceTerm S, []⟩ ∧ (∃S'. S' ∈S P' ∧ S ─⌢v→Source* S')"
      by blast
  next
    case (WLS_Cons P w Cal Q α R)
    from WLS_Cons(2) have IH: "S ∈S P ∧ Cal = STLCal Source Target ⟹
                               ∃v. v ∈SL* ⟨SourceTerm S, w⟩ ∧ (∃S'. S' ∈S Q ∧ S ─⌢v→Source* S')"
      by simp
    assume "S ∈S P" and A1: "Cal = STLCal Source Target"
    with IH obtain v S' where A2: "v ∈SL* ⟨SourceTerm S, w⟩" and A3: "S' ∈S Q"
                          and A4: "S ─⌢v→Source* S'"
      by blast
    assume "Q ─⁀α→Cal* R"
    with A1 A3 obtain β S'' where A5: "β ∈SL ⟨Q, α⟩" and A6: "S'' ∈S R"
                              and A7: "S' ─⁀β→Source* S''"
      using STLCal_weakLabelledSteps(1)[of S' α R]
      by blast
    from A2 A3 A5 have A8: "(v@[β]) ∈SL* ⟨SourceTerm S, (w@[α])⟩"
      using SLCons[of v "SourceTerm S" w β Q α]
      by simp
    from A4 A7 have "S ─⌢(v@[β])→Source* S''"
      using weakLabelledSequence.WLS_Cons[of S v Source S' β S'']
      by simp
    with A6 A8
    show "∃v'. v' ∈SL* ⟨SourceTerm S, (w@[α])⟩ ∧ (∃S''. S'' ∈S R ∧ S ─⌢v'→Source* S'')"
      by blast
  qed
next
  fix v S'
  define Cal where def_Cal: "Cal = Source"
  assume A1: "v ∈SL* ⟨SourceTerm S, w⟩" and A2: "S' ∈S P'"
  assume "S ─⌢v→Source* S'"
  with def_Cal have "S ─⌢v→Cal* S'"
    by simp
  from this def_Cal A1 A2 show "SourceTerm S ─⌢w→(STLCal Source Target)* SourceTerm S'"
  proof (induct arbitrary: w P')
    case (WLS_Nil S Cal S')
    assume "[] ∈SL* ⟨SourceTerm S, w⟩"
    hence B: "w = []"
      using lift_source_word_length(1)[of "[]" "SourceTerm S" w]
      by simp
    assume "S →Cal* S'" and "Cal = Source"
    hence "SourceTerm S →(STLCal Source Target)* SourceTerm S'"
      using STLCal_weakTauSteps(1)[of S "SourceTerm S'"]
      by simp
    with B show "SourceTerm S ─⌢w→(STLCal Source Target)* SourceTerm S'"
      using weakLabelledSequence.WLS_Nil[of "SourceTerm S" "STLCal Source Target" "SourceTerm S'"]
      by simp
  next
    case (WLS_Cons S v Cal S' β S'' w' P'')
    from WLS_Cons(2) have IH: "⋀w P'. Cal = Source ∧ v ∈SL* ⟨SourceTerm S, w⟩ ∧ S' ∈S P' ⟹
                               SourceTerm S ─⌢w→(STLCal Source Target)* SourceTerm S'"
      by simp
    assume "(v@[β]) ∈SL* ⟨SourceTerm S, w'⟩"
    then obtain w α where B1: "w' = w@[α]" and B2: "v ∈SL* ⟨SourceTerm S, w⟩"
                      and B3: "β ∈SL ⟨SourceTerm S, α⟩"
      using lift_composed_word_on_source_labels[of v β "SourceTerm S" w']
      by blast
    assume B4: "Cal = Source"
    with IH[of w "SourceTerm S'"] B2
    have B5: "SourceTerm S ─⌢w→(STLCal Source Target)* SourceTerm S'"
      by simp
    from B3 have B6: "β ∈SL ⟨SourceTerm S', α⟩"
      unfolding getSourceLabel_def
      by blast
    assume "S' ─⁀β→Cal* S''"
    with B4 B6 have "SourceTerm S' ─⁀α→(STLCal Source Target)* SourceTerm S''"
      using STLCal_weakLabelledSteps(1)[of S' α "SourceTerm S''"]
      by blast
    with B1 B5 show "SourceTerm S ─⌢w'→(STLCal Source Target)* SourceTerm S''"
      using weakLabelledSequence.WLS_Cons[of "SourceTerm S" w "STLCal Source Target"
              "SourceTerm S'" α "SourceTerm S''"]
      by simp
  qed
next
  define P :: "('procS, 'procT) Proc" where def_P:   "P = TargetTerm T"
  define Cal                          where def_Cal: "Cal = STLCal Source Target"
  assume "TargetTerm T ─⌢w→(STLCal Source Target)* P'"
  with def_P def_Cal have "P ─⌢w→Cal* P'"
    by simp
  from this def_P def_Cal
  show "∃v. v ∈TL* ⟨TargetTerm T, w⟩ ∧ (∃T'. T' ∈T P' ∧ T ─⌢v→Target* T')"
  proof induct
    case (WLS_Nil P Cal P')
    have A1: "[] ∈TL* ⟨TargetTerm T, []⟩"
      using TLNil
      by simp
    assume "P →Cal* P'" and "T ∈T P" and "Cal = STLCal Source Target"
    then obtain T' where A2: "T' ∈T P'" and A3: "T →Target* T'"
      using STLCal_weakTauSteps(2)[of T P']
      by blast
    from A3 have "T ─⌢[]→Target* T'"
      using weakLabelledSequence.WLS_Nil[of T Target T']
      by simp
    with A1 A2 show "∃v. v ∈TL* ⟨TargetTerm T, []⟩ ∧ (∃T'. T' ∈T P' ∧ T ─⌢v→Target* T')"
      by blast
  next
    case (WLS_Cons P w Cal Q α R)
    from WLS_Cons(2) have IH: "T ∈T P ∧ Cal = STLCal Source Target ⟹
                               ∃v. v ∈TL* ⟨TargetTerm T, w⟩ ∧ (∃T'. T' ∈T Q ∧ T ─⌢v→Target* T')"
      by simp
    assume "T ∈T P" and A1: "Cal = STLCal Source Target"
    with IH obtain v T' where A2: "v ∈TL* ⟨TargetTerm T, w⟩" and A3: "T' ∈T Q"
                          and A4: "T ─⌢v→Target* T'"
      by blast
    assume "Q ─⁀α→Cal* R"
    with A1 A3 obtain β T'' where A5: "β ∈TL ⟨Q, α⟩" and A6: "T'' ∈T R"
                              and A7: "T' ─⁀β→Target* T''"
      using STLCal_weakLabelledSteps(2)[of T' α R]
      by blast
    from A2 A5 have A8: "(v@[β]) ∈TL* ⟨TargetTerm T, (w@[α])⟩"
      using TLCons[of v "TargetTerm T" w β Q α]
      by simp
    from A4 A7 have "T ─⌢(v@[β])→Target* T''"
      using weakLabelledSequence.WLS_Cons[of T v Target T' β T'']
      by simp
    with A6 A8
    show "∃v'. v' ∈TL* ⟨TargetTerm T, (w@[α])⟩ ∧ (∃T''. T'' ∈T R ∧ T ─⌢v'→Target* T'')"
      by blast
  qed
next
  fix v T'
  define Cal where def_Cal: "Cal = Target"
  assume A1: "v ∈TL* ⟨TargetTerm T, w⟩" and A2: "T' ∈T P'"
  assume "T ─⌢v→Target* T'"
  with def_Cal have "T ─⌢v→Cal* T'"
    by simp
  from this def_Cal A1 A2 show "TargetTerm T ─⌢w→(STLCal Source Target)* TargetTerm T'"
  proof (induct arbitrary: w P')
    case (WLS_Nil T Cal T')
    assume "[] ∈TL* ⟨TargetTerm T, w⟩"
    hence B: "w = []"
      using lift_target_word_length(1)[of "[]" "TargetTerm T" w]
      by simp
    assume "T →Cal* T'" and "Cal = Target"
    hence "TargetTerm T →(STLCal Source Target)* TargetTerm T'"
      using STLCal_weakTauSteps(2)[of T "TargetTerm T'"]
      by simp
    with B show "TargetTerm T ─⌢w→(STLCal Source Target)* TargetTerm T'"
      using weakLabelledSequence.WLS_Nil[of "TargetTerm T" "STLCal Source Target" "TargetTerm T'"]
      by simp
  next
    case (WLS_Cons T v Cal T' β T'' w' P'')
    from WLS_Cons(2) have IH: "⋀w P'. Cal = Target ∧ v ∈TL* ⟨TargetTerm T, w⟩ ∧ T' ∈T P' ⟹
                               TargetTerm T ─⌢w→(STLCal Source Target)* TargetTerm T'"
      by simp
    assume "(v@[β]) ∈TL* ⟨TargetTerm T, w'⟩"
    then obtain w P α where B1: "w' = w@[α]" and B2: "v ∈TL* ⟨TargetTerm T, w⟩"
                        and B3: "β ∈TL ⟨P, α⟩"
      using lift_composed_word_on_target_labels[of v β "TargetTerm T" w']
      by blast
    assume B4: "Cal = Target"
    with IH[of w "TargetTerm T'"] B2
    have B5: "TargetTerm T ─⌢w→(STLCal Source Target)* TargetTerm T'"
      by simp
    from B3 have B6: "β ∈TL ⟨TargetTerm T', α⟩"
      unfolding getTargetLabel_def
      by blast
    assume "T' ─⁀β→Cal* T''"
    with B4 B6 have "TargetTerm T' ─⁀α→(STLCal Source Target)* TargetTerm T''"
      using STLCal_weakLabelledSteps(2)[of T' α "TargetTerm T''"]
      by blast
    with B1 B5 show "TargetTerm T ─⌢w'→(STLCal Source Target)* TargetTerm T''"
      using weakLabelledSequence.WLS_Cons[of "TargetTerm T" w "STLCal Source Target"
              "TargetTerm T'" α "TargetTerm T''"]
      by simp
  qed
qed

lemma weakLabelledSequenceST_STLCal_weakLabelledSequence:
  fixes P P' :: "('procS, 'procT) Proc"
    and w    :: "('labS, 'labT) Lab list"
  shows "P ─⌢w→(STLCal Source Target)* P' = P ─⌢w→ST* P'"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P ─⌢w→(STLCal Source Target)* P' = P ─⌢w→ST* P'"
    using STLCal_weakLabelledSequence(1)[of SP w P']
    by blast
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P ─⌢w→(STLCal Source Target)* P' = P ─⌢w→ST* P'"
    using STLCal_weakLabelledSequence(2)[of TP w P']
    by blast
qed

text ‹To weak labelled steps on the same label imply the the corresponding processes are of the
      same kind, i.e., are all source terms or are all target terms.›

lemma weakLabelledStepsST_on_same_label_are_on_same_kind_of_processes:
  fixes P P' Q Q' :: "('procS, 'procT) Proc"
    and α         :: "('labS, 'labT) Lab"
  assumes "α ≠ τ-STLCal"
      and "P ─⁀α→ST* P'"
      and "Q ─⁀α→ST* Q'"
    shows "P ∼ST Q"
  using assms
  unfolding getSourceLabel_def getTargetLabel_def
  by blast

lemma weakLabelledSteps_on_same_label_are_on_same_kind_of_processes:
  fixes P P' Q Q' :: "('procS, 'procT) Proc"
    and α         :: "('labS, 'labT) Lab"
  assumes "α ≠ τ-(STLCal Source Target)"
      and "P ─⁀α→(STLCal Source Target)* P'"
      and "Q ─⁀α→(STLCal Source Target)* Q'"
    shows "P ∼ST Q"
  using assms internalST_iff_internal weakLabelledStepsST_STLCal_weakLabelledSteps[of P α P']
        weakLabelledStepsST_STLCal_weakLabelledSteps[of Q α Q']
        weakLabelledStepsST_on_same_label_are_on_same_kind_of_processes[of α P P' Q Q']
  by simp

text ‹Similarly, two sequences of weak labelled steps on the same words have the same kind of
      processes.›

lemma weakLabelledSequenceST_on_same_word_are_on_same_kind_of_processes:
  fixes P P' Q Q' :: "('procS, 'procT) Proc"
    and w         :: "('labS, 'labT) Lab list"
  assumes stepP: "P ─⌢w→ST* P'"
      and stepQ: "Q ─⌢w→ST* Q'"
      and word:  "∃α ∈ set w. α ≠ τ-STLCal"
    shows "P ∼ST Q"
  using assms
proof auto
  fix α v1 S T v2 T' S'
  assume "α ∈ set w" and "α ≠ τ-STLCal" and "v1 ∈SL* ⟨SourceTerm S', w⟩"
     and "v2 ∈TL* ⟨TargetTerm T', w⟩"
  thus False
    using lifted_non_internal_word_is_either_source_or_target[of v1 "SourceTerm S'" w v2
            "TargetTerm T'"]
    by blast
next
  fix α T v2 T' v1 S S'
  assume "α ∈ set w" and "α ≠ τ-STLCal" and "v1 ∈SL* ⟨SourceTerm S', w⟩"
     and "v2 ∈TL* ⟨TargetTerm T', w⟩"
  thus False
    using lifted_non_internal_word_is_either_source_or_target[of v1 "SourceTerm S'" w v2
            "TargetTerm T'"]
    by blast
qed

lemma weakLabelledSequence_on_same_word_are_on_same_kind_of_processes:
  fixes P P' Q Q' :: "('procS, 'procT) Proc"
    and w         :: "('labS, 'labT) Lab list"
  assumes "P ─⌢w→(STLCal Source Target)* P'"
      and "Q ─⌢w→(STLCal Source Target)* Q'"
      and "∃α ∈ set w. α ≠ τ-STLCal"
    shows "P ∼ST Q"
  using assms weakLabelledSequenceST_on_same_word_are_on_same_kind_of_processes[of P w P' Q Q']
        weakLabelledSequenceST_STLCal_weakLabelledSequence[of P w P']
        weakLabelledSequenceST_STLCal_weakLabelledSequence[of Q w Q']
  by simp

text ‹In a weak labelled sequence the process at the beginning and the process at the end are of
      the same kind. Moreover, the word used in this sequence is of the same kind as the processes,
      i.e., consists of only source labels if the processes are source terms and else of only
      target labels.›

lemma weakLabelledSequenceST_kinds:
  fixes P P' :: "('procS, 'procT) Proc"
    and w    :: "('labS, 'labT) Lab list"
  assumes "P ─⌢w→ST* P'"
  shows "P ∼ST P'"
    and "P ∼ST P'"
    and "P ∈ ProcS ⟶ (∀α ∈ set w. α ∈ LabS ∨ α = τ-STLCal)"
    and "P ∈ ProcT ⟶ (∀α ∈ set w. α ∈ LabT ∨ α = τ-STLCal)"
  using assms
proof (induct P)
  case (SourceTerm S)
  assume A1: "SourceTerm S ─⌢w→ST* P'"
  then obtain v S' where A2: "v ∈SL* ⟨SourceTerm S, w⟩" and A3: "S' ∈S P'"
    using STLCal_weakLabelledSequence(1)[of S w P']
    by blast
  from A3 show "SourceTerm S ∼ST P'"
    by simp
  from A3 show "SourceTerm S ∼ST P'"
    by simp
  from A1 A2 show "SourceTerm S ∈ ProcS ⟶ (∀α ∈ set w. α ∈ LabS ∨ α = τ-STLCal)"
    using lifted_word_on_source_labels_kinds(1)[of v "SourceTerm S" w]
    by simp
  show "SourceTerm S ∈ ProcT ⟶ (∀α ∈ set w. α ∈ LabT ∨ α = τ-STLCal)"
    by simp
next
  case (TargetTerm T)
  assume A1: "TargetTerm T ─⌢w→ST* P'"
  then obtain v T' where A2: "v ∈TL* ⟨TargetTerm T, w⟩" and A3: "T' ∈T P'"
    using STLCal_weakLabelledSequence(2)[of T w P']
    by blast
  from A3 show "TargetTerm T ∼ST P'"
    by simp
  from A3 show "TargetTerm T ∼ST P'"
    by simp
  show "TargetTerm T ∈ ProcS ⟶ (∀α ∈ set w. α ∈ LabS ∨ α = τ-STLCal)"
    by simp
  from A1 A2 show "TargetTerm T ∈ ProcT ⟶ (∀α ∈ set w. α ∈ LabT ∨ α = τ-STLCal)"
    using lifted_word_on_target_labels_kinds[of v "TargetTerm T" w]
    by simp
qed

text ‹A divergent term of Proc is either a divergent source term or a divergent target term.›

abbreviation divergentST :: "('procS, 'procT) Proc ⇒ bool" (‹_ →STω› [70] 80) where
  "P →STω ≡ (∃S. S ∈S P ∧ S →(Source)ω) ∨ (∃T. T ∈T P ∧ T →(Target)ω)"

lemma STLCal_divergent:
  fixes S  :: "'procS"
    and T  :: "'procT"
  shows "SourceTerm S →(STLCal Source Target)ω = S →(Source)ω"
    and "TargetTerm T →(STLCal Source Target)ω = T →(Target)ω"
proof auto
  assume "SourceTerm S →(STLCal Source Target)ω"
  thus "S →(Source)ω"
    unfolding divergentLS_def
  proof auto
    fix S'
    assume "S →Source* S'"
    hence "SourceTerm S →(STLCal Source Target)* SourceTerm S'"
      using STLCal_weakTauSteps(1)[of S "SourceTerm S'"]
      by simp
    moreover assume "∀P'. SourceTerm S →(STLCal Source Target)* P' ⟶
                     (∃P''. P' ─τ-(STLCal Source Target)→(STLCal Source Target) P'')"
    ultimately obtain P'' where "SourceTerm S' ─τ-STLCal→(STLCal Source Target) P''"
      using internalST_iff_internal
      by auto
    thus "∃S''. S' ─τ-Source→Source S''"
      using STLCal_labelledStep(1)[of S' "τ-STLCal" P'']
      unfolding getSourceLabel_def
      by blast
  qed
next
  assume "S →(Source)ω"
  thus "SourceTerm S →(STLCal Source Target)ω"
    unfolding divergentLS_def
  proof auto
    fix P'
    assume "SourceTerm S →(STLCal Source Target)* P'"
    then obtain S' where A1: "S' ∈S P'" and A2: "S →Source* S'"
      using STLCal_weakTauSteps(1)[of S P']
      by blast
    assume "∀S'. S →Source* S' ⟶ (∃S''. S' ─τ-Source→Source S'')"
    with A2 obtain S'' where "S' ─τ-Source→Source S''"
      by blast
    with A1 show "∃P''. P' ─τ-(STLCal Source Target)→(STLCal Source Target) P''"
      using STLCal_labelledStep(1)[of S' "τ-STLCal" "SourceTerm S''"] internalST_iff_internal
      unfolding getSourceLabel_def
      by auto
  qed
next
  assume "TargetTerm T →(STLCal Source Target)ω"
  thus "T →(Target)ω"
    unfolding divergentLS_def
  proof auto
    fix T'
    assume "T →Target* T'"
    hence "TargetTerm T →(STLCal Source Target)* TargetTerm T'"
      using STLCal_weakTauSteps(2)[of T "TargetTerm T'"]
      by simp
    moreover assume "∀P'. TargetTerm T →(STLCal Source Target)* P' ⟶
                     (∃P''. P' ─τ-(STLCal Source Target)→(STLCal Source Target) P'')"
    ultimately obtain P'' where "TargetTerm T' ─τ-STLCal→(STLCal Source Target) P''"
      using internalST_iff_internal
      by auto
    thus "∃T''. T' ─τ-Target→Target T''"
      using STLCal_labelledStep(2)[of T' "τ-STLCal" P'']
      unfolding getTargetLabel_def
      by blast
  qed
next
  assume "T →(Target)ω"
  thus "TargetTerm T →(STLCal Source Target)ω"
    unfolding divergentLS_def
  proof auto
    fix P'
    assume "TargetTerm T →(STLCal Source Target)* P'"
    then obtain T' where A1: "T' ∈T P'" and A2: "T →Target* T'"
      using STLCal_weakTauSteps(2)[of T P']
      by blast
    assume "∀T'. T →Target* T' ⟶ (∃T''. T' ─τ-Target→Target T'')"
    with A2 obtain T'' where "T' ─τ-Target→Target T''"
      by blast
    with A1 show "∃P''. P' ─τ-(STLCal Source Target)→(STLCal Source Target) P''"
      using STLCal_labelledStep(2)[of T' "τ-STLCal" "TargetTerm T''"] internalST_iff_internal
      unfolding getTargetLabel_def
      by auto
  qed
qed

lemma divergentST_STCal_divergent:
  fixes P :: "('procS, 'procT) Proc"
  shows "P →(STLCal Source Target)ω = P →STω"
proof (cases P)
  case (SourceTerm SP)
  assume "SP ∈S P"
  thus "P →(STLCal Source Target)ω = P →STω"
    using STLCal_divergent(1)
    by simp
next
  case (TargetTerm TP)
  assume "TP ∈T P"
  thus "P →(STLCal Source Target)ω = P →STω"
    using STLCal_divergent(2)
    by simp
qed

end

subsection ‹An encoding function considering labelled semantics and a translation of labels.›

text ‹ToDo: By using a single fresh internal label in the labelled calculus on the disjoint union of the
      source and target language and moreover by the implementation of weak steps, we implicitly
      already add a requirement on the translation of internal labels. It is not yet visible, but
      since we will use these definitions of weak steps in the two weaker versions of operational
      correspondence, we indeed implicitly assume that internal steps of the source are translated
      to internal steps on the target. Similarly, this implicit assumption is present also for the
      criterion on divergence reflection. However, there is not yet any implicit requirement on the
      translation of label for cases without weak steps as e.g. the later defined strong version of
      operational correspondence. More precisely, so far we only require that internal source term
      steps are translated into internal target term steps but only for the later considered
      criteria using weak notions of steps. We did not yet pose any requirement on the translation
      of arbitrary labels. We will however need such a requirement for some of our results.
      Therefore, we extend our notion of encoding on labelled semantics by an additional encoding
      function on labels. In order to allow for more flexibility, we allow the translation of
      labels to consider as input not only a source term label but actually the whole source term
      steps, by having also two source terms as inputs.›

locale encodingLS_encL =
  encodingLS Enc Source Target
    for Source :: "('procS, 'labS) labelledProcessCalculus"
    and Target :: "('procT, 'labT) labelledProcessCalculus"
    and Enc    :: "'procS ⇒ 'procT" +
  fixes EncL :: "'labS ⇒ 'labT"
begin

abbreviation encL :: "'labS ⇒ 'labT" (‹⦉_⦊› [65] 70) where
  "⦉α⦊ ≡ EncL α"

definition encLST
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ ('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒
      bool" (‹⦇_, _⦈↦⟨_, _⟩› [65, 65, 65, 65] 70) where
  "⦇P, α⦈↦⟨Q, β⟩ ≡ (∃α' β'. α' ∈SL ⟨P, α⟩ ∧ β' ∈TL ⟨Q, β⟩ ∧ ⦉α'⦊ = β')"

inductive encLST_list
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab list ⇒ ('procS, 'procT) Proc ⇒
      ('labS, 'labT) Lab list ⇒ bool" (‹⦇_, _⦈↦*⟨_, _⟩› [65, 65, 65, 65] 70) where
  ELNil:  "⟦P ∈ ProcS; Q ∈ ProcT⟧ ⟹ ⦇P, []⦈↦*⟨Q, []⟩"
| ELCons: "⟦⦇P, w⦈↦*⟨Q, v⟩; ⦇P', α⦈↦⟨Q', β⟩⟧ ⟹ ⦇P, w@[α]⦈↦*⟨Q, v@[β]⟩"

text ‹In the translation of a word the considered word is of source labels and the resulting word
      is a word on target term labels.›

lemma kinds_of_encoded_label:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes "⦇P, α⦈↦⟨Q, β⟩"
  shows "P ∈ ProcS"
    and "α ∈ LabS ∨ α = τ-STLCal"
    and "Q ∈ ProcT"
    and "β ∈ LabT ∨ β = τ-STLCal"
  using assms
  unfolding encLST_def isSourceLabel_def getSourceLabel_def isTargetLabel_def getTargetLabel_def
  by blast+

lemma kinds_of_encoded_word:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⦇P, w⦈↦*⟨Q, v⟩"
  shows "P ∈ ProcS"
    and "∀α ∈ set w. α ∈ LabS ∨ α = τ-STLCal"
    and "Q ∈ ProcT"
    and "∀β ∈ set v. β ∈ LabT ∨ β = τ-STLCal"
  using assms
proof induct
  case (ELNil P Q)
  assume "P ∈ ProcS"
  thus "P ∈ ProcS" .
  show "∀α ∈ set []. α ∈ LabS ∨ α = τ-STLCal"
    by simp
  assume "Q ∈ ProcT"
  thus "Q ∈ ProcT" .
  show "∀β ∈ set []. β ∈ LabT ∨ β = τ-STLCal"
    by simp
next
  case (ELCons P w Q v P' α Q' β)
  assume "P ∈ ProcS"
  thus "P ∈ ProcS" .
  assume "⦇P', α⦈↦⟨Q', β⟩"
  hence A1: "α ∈ LabS ∨ α = τ-STLCal" and A2: "β ∈ LabT ∨ β = τ-STLCal"
    unfolding encLST_def isSourceLabel_def getSourceLabel_def isTargetLabel_def getTargetLabel_def
    by blast+
  assume "∀α ∈ set w. α ∈ LabS ∨ α = τ-STLCal"
  with A1 show "∀α ∈ set (w@[α]). α ∈ LabS ∨ α = τ-STLCal"
    by simp
  assume "Q ∈ ProcT"
  thus "Q ∈ ProcT" .
  assume "∀β ∈ set v. β ∈ LabT ∨ β = τ-STLCal"
  with A2 show "∀β ∈ set (v@[β]). β ∈ LabT ∨ β = τ-STLCal"
    by simp
qed

text ‹What matters about the process in the notation of encoded words is only its kind.›

lemma encoded_label_exchange_processes:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes "⦇P, α⦈↦⟨Q, β⟩"
      and "P' ∈ ProcS"
      and "Q' ∈ ProcT"
    shows "⦇P', α⦈↦⟨Q', β⟩"
  using assms
  unfolding encLST_def getSourceLabel_def getTargetLabel_def
  by blast

lemma encoded_word_exchange_processes:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⦇P, w⦈↦*⟨Q, v⟩"
      and "P' ∈ ProcS"
      and "Q' ∈ ProcT"
    shows "⦇P', w⦈↦*⟨Q', v⟩"
  using assms
proof induct
  case (ELNil P Q)
  assume "P' ∈ ProcS" and  "Q' ∈ ProcT"
  thus "⦇P', []⦈↦*⟨Q', []⟩"
    using encLST_list.ELNil[of P' Q']
    by simp
next
  case (ELCons P w Q v P'' α Q'' β)
  from ELCons(2) have IH: "P' ∈ ProcS ∧ Q' ∈ ProcT ⟹ ⦇P', w⦈↦*⟨Q', v⟩"
    by simp
  assume "P' ∈ ProcS" "Q' ∈ ProcT"
  with IH have "⦇P', w⦈↦*⟨Q', v⟩"
    by simp
  moreover assume "⦇P'', α⦈↦⟨Q'', β⟩"
  ultimately show "⦇P', w@[α]⦈↦*⟨Q', v@[β]⟩"
    using encLST_list.ELCons[of P' w Q' v P'' α Q'' β]
    by simp
qed

text ‹The encoded word and the original word have the same length.›

lemma encoded_word_length:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⦇P, w⦈↦*⟨Q, v⟩"
  shows "length v = length w"
  using assms
  by (induct, simp_all)

text ‹The encoding of a composed word results in a composed word.›

lemma encoded_word_decompose:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⦇P, w⦈↦*⟨Q, v⟩"
  shows "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⦇P, w'⦈↦*⟨Q, v'⟩ ∧
                   ⦇P', α⦈↦⟨Q', β⟩ ∧ P' ∈ ProcS ∧ Q' ∈ ProcT)"
  using assms
proof induct
  case (ELNil P Q)
  show "[] = [] ∨ (∃w' α v' β P' Q'. [] = w'@[α] ∧ [] = v'@[β] ∧ ⦇P, w'⦈↦*⟨Q, v'⟩ ∧
                   ⦇P', α⦈↦⟨Q', β⟩ ∧ P' ∈ ProcS ∧ Q' ∈ ProcT)"
    by simp
next
  case (ELCons P w Q v P' α Q' β)
  assume "⦇P, w⦈↦*⟨Q, v⟩" and A: "⦇P', α⦈↦⟨Q', β⟩"
  moreover from A have "P' ∈ ProcS" and "Q' ∈ ProcT"
    using kinds_of_encoded_label(1, 3)[of P' α Q' β]
    by simp_all
  ultimately
  show "w@[α] = [] ∨ (∃w' α' v' β' P' Q'. w@[α] = w'@[α'] ∧ v@[β] = v'@[β'] ∧ ⦇P, w'⦈↦*⟨Q, v'⟩ ∧
                      ⦇P', α'⦈↦⟨Q', β'⟩ ∧ P' ∈ ProcS ∧ Q' ∈ ProcT)"
    by auto
qed

text ‹The encoding of a word is unambiguous. If the label encoding is injective we also obtain that
      the source label/word of an encoded label/word is unique.›

lemma encoded_label_unique:
  fixes P Q R :: "('procS, 'procT) Proc"
    and α β γ :: "('labS, 'labT) Lab"
  assumes "⦇P, α⦈↦⟨Q, β⟩"
      and "⦇P, α⦈↦⟨R, γ⟩"
    shows "β = γ"
  using assms
  unfolding encLST_def getSourceLabel_def getTargetLabel_def
  by blast

lemma encoded_word_unique:
  fixes P Q R :: "('procS, 'procT) Proc"
    and w v y :: "('labS, 'labT) Lab list"
  assumes "⦇P, w⦈↦*⟨Q, v⟩"
      and "⦇P, w⦈↦*⟨R, y⟩"
    shows "v = y"
  using assms
proof (induct arbitrary: y)
  case (ELNil P Q)
  assume "⦇P, []⦈↦*⟨R, y⟩"
  thus "[] = y"
    using encoded_word_length[of P "[]" R y]
    by simp
next
  case (ELCons P w Q v P' α Q' β)
  assume "⦇P, w@[α]⦈↦*⟨R, y⟩"
  then obtain y' γ P'' R' where A1: "y = y'@[γ]" and A2: "⦇P, w⦈↦*⟨R, y'⟩"
                            and A3: "⦇P'', α⦈↦⟨R', γ⟩"
    using encoded_word_decompose[of P "w@[α]" R y]
    by auto
  assume "⋀y. ⦇P, w⦈↦*⟨R, y⟩ ⟹ v = y"
  with A2 have A4: "v = y'"
    by simp
  assume "⦇P', α⦈↦⟨Q', β⟩"
  with A3 have "⦇P'', α⦈↦⟨Q', β⟩"
    unfolding encLST_def getSourceLabel_def
    by simp
  with A3 have "β = γ"
    using encoded_label_unique[of P'' α R' γ Q' β]
    by simp
  with A1 A4 show "v@[β] = y"
    by simp
qed

lemma encoded_label_unique_rev:
  fixes P Q R :: "('procS, 'procT) Proc"
    and α β γ :: "('labS, 'labT) Lab"
  assumes "⦇P, α⦈↦⟨R, γ⟩"
      and "⦇Q, β⦈↦⟨R, γ⟩"
      and "inj encL"
    shows "α = β"
  using assms
  unfolding inj_def encLST_def getSourceLabel_def getTargetLabel_def
  by auto

lemma encoded_word_unique_rev:
  fixes P Q R :: "('procS, 'procT) Proc"
    and w v y :: "('labS, 'labT) Lab list"
  assumes "⦇P, w⦈↦*⟨R, y⟩"
      and "⦇Q, v⦈↦*⟨R, y⟩"
      and "inj encL"
    shows "w = v"
  using assms
proof (induct arbitrary: v)
  case (ELNil P R)
  assume "⦇Q, v⦈↦*⟨R, []⟩"
  thus "[] = v"
    using encoded_word_length[of Q v R "[]"]
    by simp
next
  case (ELCons P w R y P' α R' γ)
  assume A1: "⦇Q, v⦈↦*⟨R, y@[γ]⟩"
  hence "v ≠ []"
    using encoded_word_length[of Q v R "y@[γ]"]
    by auto
  with A1 obtain v' β Q' R'' where A2: "v = v'@[β]" and A3: "⦇Q, v'⦈↦*⟨R, y⟩"
                               and A4: "⦇Q', β⦈↦⟨R'', γ⟩"
    using encoded_word_decompose[of Q v R "y@[γ]"]
    by auto
  from ELCons(2) have IH: "⋀v. ⦇Q, v⦈↦*⟨R, y⟩ ∧ inj encL ⟹ w = v"
    by simp
  assume A5: "inj encL"
  with A2 A3 IH have A6: "w = v'"
    by simp
  assume A7: "⦇P', α⦈↦⟨R', γ⟩"
  hence "R' ∈ ProcT"
    using kinds_of_encoded_label(3)[of P' α R' γ]
    by simp
  with A2 A4 have "⦇Q', β⦈↦⟨R', γ⟩"
    using encoded_label_exchange_processes[of Q' β R'' γ Q' R']
          kinds_of_encoded_label(1)[of Q' β R'' γ]
    by simp
  with A5 A7 have "β = α"
    using encoded_label_unique_rev[of Q' β R' γ P' α]
    by simp
  with A2 A6 show "w@[α] = v"
    by simp
qed

text ‹We have to consider three cases of pairs of labelled steps in the calculus on the disjoint
      union of the source and target with related labels:
      (1) The two steps are of the same kind, i.e., both are source or both are target term steps.
          In this case (but only this case) the two steps might actually use the same label.
      (2) A source term step on a label and a target term step on the label that results from
          translating the label of the source term step.
      (3) A target term step on a label that results from the translation of a source term step and
          the corresponding source term step.
      In all other cases we consider the labels as unrelated. The described relation of labels is
      relevant for the definition of behavioural relations that are respecting the encoding of
      labels as defined later. The processes in the cases of labels are necessary to clearly
      distinguish, whether two internal labels in the disjoint union are actually the same or
      result from a source internal and a target internal that should rather be compared by the
      label encoding. For words we do not need that, since we do not consider the internals in the
      words.›

definition related_labels
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒ ('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab ⇒
      bool" (‹⟨_, _⟩ ≡⦇⦈ ⟨_, _⟩› [65, 65, 65, 65] 70) where
  "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩ ≡ α = β ∧ P ∼ST Q ∨ ⦇P, α⦈↦⟨Q, β⟩ ∨ ⦇Q, β⦈↦⟨P, α⟩"

definition related_words
  :: "('procS, 'procT) Proc ⇒ ('labS, 'labT) Lab list ⇒ ('procS, 'procT) Proc ⇒
      ('labS, 'labT) Lab list ⇒ bool" (‹⟨_, _⟩ ≡⦇⦈* ⟨_, _⟩› [65, 65, 65, 65] 70) where
  "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩ ≡ w = v ∧ P ∼ST Q ∨ ⦇P, w⦈↦*⟨Q, v⟩ ∨ ⦇Q, v⦈↦*⟨P, w⟩"

text ‹We prove that the three parts of the condition for related labels are mutual exclusive.›

lemma related_labels_conditions_mutual_exclusive:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  shows "α = β ∧ P ∼ST Q ⟹ ¬⦇P, α⦈↦⟨Q, β⟩"
    and "α = β ∧ P ∼ST Q ⟹ ¬⦇Q, β⦈↦⟨P, α⟩"
    and "⦇P, α⦈↦⟨Q, β⟩ ⟹ ¬(α = β ∧ P ∼ST Q)"
    and "⦇P, α⦈↦⟨Q, β⟩ ⟹ ¬⦇Q, β⦈↦⟨P, α⟩"
    and "⦇Q, β⦈↦⟨P, α⟩ ⟹ ¬(α = β ∧ P ∼ST Q)"
    and "⦇Q, β⦈↦⟨P, α⟩ ⟹ ¬⦇P, α⦈↦⟨Q, β⟩"
  unfolding encLST_def getSourceLabel_def getTargetLabel_def
  by blast+

lemma related_words_conditions_mutual_exclusive:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  shows "w = v ∧ P ∼ST Q ⟹ ¬⦇P, w⦈↦*⟨Q, v⟩"
    and "w = v ∧ P ∼ST Q ⟹ ¬⦇Q, v⦈↦*⟨P, w⟩"
    and "⦇P, w⦈↦*⟨Q, v⟩ ⟹ ¬(w = v ∧ P ∼ST Q)"
    and "⦇P, w⦈↦*⟨Q, v⟩ ⟹ ¬⦇Q, v⦈↦*⟨P, w⟩"
    and "⦇Q, v⦈↦*⟨P, w⟩ ⟹ ¬(w = v ∧ P ∼ST Q)"
    and "⦇Q, v⦈↦*⟨P, w⟩ ⟹ ¬⦇P, w⦈↦*⟨Q, v⟩"
proof -
  assume "w = v ∧ P ∼ST Q"
  thus "¬⦇P, w⦈↦*⟨Q, v⟩"
    using kinds_of_encoded_word(1,3)[of P w Q v]
    by blast
next
  assume "w = v ∧ P ∼ST Q"
  thus "¬⦇Q, v⦈↦*⟨P, w⟩"
    using kinds_of_encoded_word(1,3)[of Q v P w]
    by blast
next
  assume "⦇P, w⦈↦*⟨Q, v⟩"
  thus "¬(w = v ∧ P ∼ST Q)"
    using kinds_of_encoded_word(1,3)[of P w Q v]
    by blast
next
  assume "⦇P, w⦈↦*⟨Q, v⟩"
  thus "¬⦇Q, v⦈↦*⟨P, w⟩"
    using kinds_of_encoded_word(1,3)[of P w Q v] kinds_of_encoded_word(1,3)[of Q v P w]
    by blast
next
  assume "⦇Q, v⦈↦*⟨P, w⟩"
  thus "¬(w = v ∧ P ∼ST Q)"
    using kinds_of_encoded_word(1,3)[of Q v P w]
    by blast
next
  assume "⦇Q, v⦈↦*⟨P, w⟩"
  thus "¬⦇P, w⦈↦*⟨Q, v⟩"
    using kinds_of_encoded_word(1,3)[of P w Q v] kinds_of_encoded_word(1,3)[of Q v P w]
    by blast
qed

lemma related_labels_get_condition:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
  shows "⟦¬⦇P, α⦈↦⟨Q, β⟩; ¬⦇Q, β⦈↦⟨P, α⟩⟧ ⟹ α = β ∧ P ∼ST Q"
    and "⟦¬(α = β ∧ P ∼ST Q); ¬⦇Q, β⦈↦⟨P, α⟩⟧ ⟹ ⦇P, α⦈↦⟨Q, β⟩"
    and "⟦¬(α = β ∧ P ∼ST Q); ¬⦇P, α⦈↦⟨Q, β⟩⟧ ⟹ ⦇Q, β⦈↦⟨P, α⟩"
  using assms
  unfolding related_labels_def
  by blast+

lemma related_words_get_condition:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  shows "⟦¬⦇P, w⦈↦*⟨Q, v⟩; ¬⦇Q, v⦈↦*⟨P, w⟩⟧ ⟹ w = v ∧ P ∼ST Q"
    and "⟦¬(w = v ∧ P ∼ST Q); ¬⦇Q, v⦈↦*⟨P, w⟩⟧ ⟹ ⦇P, w⦈↦*⟨Q, v⟩"
    and "⟦¬(w = v ∧ P ∼ST Q); ¬⦇P, w⦈↦*⟨Q, v⟩⟧ ⟹ ⦇Q, v⦈↦*⟨P, w⟩"
  using assms
  unfolding related_words_def
  by blast+

text ‹Two related words have the same length.›

lemma related_words_length:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  shows "length w = length v"
  using assms encoded_word_length[of P w Q v] encoded_word_length[of Q v P w]
  unfolding related_words_def
  by auto

text ‹We can lift related labels to related words of size one.›

lemma related_words_single:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes rel:   "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
  shows "⟨P, [α]⟩ ≡⦇⦈* ⟨Q, [β]⟩"
  using rel
  unfolding related_labels_def
proof auto
  fix S S'
  show "⟨SourceTerm S, [β]⟩ ≡⦇⦈* ⟨SourceTerm S', [β]⟩"
    unfolding related_words_def
    by simp
next
  fix T T'
  show "⟨TargetTerm T, [β]⟩ ≡⦇⦈* ⟨TargetTerm T', [β]⟩"
    unfolding related_words_def
    by simp
next
  assume "⦇P, α⦈↦⟨Q, β⟩"
  hence "⦇P, [α]⦈↦*⟨Q, [β]⟩"
    using ELNil[of P Q] ELCons[of P "[]" Q "[]" P α Q β] kinds_of_encoded_label(1,3)[of P α Q β]
    by simp
  thus "⟨P, [α]⟩ ≡⦇⦈* ⟨Q, [β]⟩"
    unfolding related_words_def
    by simp
next
  assume "⦇Q, β⦈↦⟨P, α⟩"
  hence "⦇Q, [β]⦈↦*⟨P, [α]⟩"
    using ELNil[of Q P] ELCons[of Q "[]" P "[]" Q β P α] kinds_of_encoded_label(1,3)[of Q β P α]
    by simp
  thus "⟨P, [α]⟩ ≡⦇⦈* ⟨Q, [β]⟩"
    unfolding related_words_def
    by simp
qed

text ‹Two related words of the same kind have to be equal.›

lemma related_labels_equal:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes rel:   "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and kinds: "P ∼ST Q"
    shows "α = β"
proof -
  from kinds have A: "¬⦇P, α⦈↦⟨Q, β⟩"
    using kinds_of_encoded_label(1, 3)[of P α Q β]
    by blast
  from kinds have "¬⦇Q, β⦈↦⟨P, α⟩"
    using kinds_of_encoded_label(1, 3)[of Q β P α]
    by blast
  with rel A show "α = β"
    using related_labels_get_condition(1)[of P α Q β]
    by simp
qed

lemma related_words_equal:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes rel:   "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and kinds: "P ∼ST Q"
    shows "w = v"
proof -
  from kinds have A: "¬⦇P, w⦈↦*⟨Q, v⟩"
    using kinds_of_encoded_word(1, 3)[of P w Q v]
    by blast
  from kinds have "¬⦇Q, v⦈↦*⟨P, w⟩"
    using kinds_of_encoded_word(1, 3)[of Q v P w]
    by blast
  with rel A show "w = v"
    using related_words_get_condition(1)[of P w Q v]
    by simp
qed

lemma related_labels_encL:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes rel:   "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and Pkind: "P ∈ ProcS"
      and Qkind: "Q ∈ ProcT"
    shows "⦇P, α⦈↦⟨Q, β⟩"
proof -
  from Pkind Qkind have A: "¬(α = β ∧ P ∼ST Q)"
    by blast
  from Pkind Qkind have "¬⦇Q, β⦈↦⟨P, α⟩"
    using kinds_of_encoded_label(1, 3)[of Q β P α]
    by blast
  with rel A show "⦇P, α⦈↦⟨Q, β⟩"
    using related_labels_get_condition(2)[of P α Q β]
    by simp
qed

lemma related_words_encL:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes rel:   "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and Pkind: "P ∈ ProcS"
      and Qkind: "Q ∈ ProcT"
    shows "⦇P, w⦈↦*⟨Q, v⟩"
proof -
  from Pkind Qkind have A: "¬(w = v ∧ P ∼ST Q)"
    by blast
  from Pkind Qkind have "¬⦇Q, v⦈↦*⟨P, w⟩"
    using kinds_of_encoded_word(1, 3)[of Q v P w]
    by blast
  with rel A show "⦇P, w⦈↦*⟨Q, v⟩"
    using related_words_get_condition(2)[of P w Q v]
    by simp
qed

lemma related_labels_encL_rev:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes rel:   "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and Pkind: "P ∈ ProcT"
      and Qkind: "Q ∈ ProcS"
    shows "⦇Q, β⦈↦⟨P, α⟩"
proof -
  from Pkind Qkind have A: "¬(α = β ∧ P ∼ST Q)"
    by blast
  from Pkind Qkind have "¬⦇P, α⦈↦⟨Q, β⟩"
    using kinds_of_encoded_label(1, 3)[of P α Q β]
    by blast
  with rel A show "⦇Q, β⦈↦⟨P, α⟩"
    using related_labels_get_condition(3)[of P α Q β]
    by simp
qed

lemma related_words_encL_rev:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes rel:   "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and Pkind: "P ∈ ProcT"
      and Qkind: "Q ∈ ProcS"
    shows "⦇Q, v⦈↦*⟨P, w⟩"
proof -
  from Pkind Qkind have A: "¬(w = v ∧ P ∼ST Q)"
    by blast
  from Pkind Qkind have "¬⦇P, w⦈↦*⟨Q, v⟩"
    using kinds_of_encoded_word(1, 3)[of P w Q v]
    by blast
  with rel A show "⦇Q, v⦈↦*⟨P, w⟩"
    using related_words_get_condition(3)[of P w Q v]
    by simp
qed

text ‹Also in the definition of related labels/words the only thing that matters of the mentioned
      processes is their kind.›

lemma related_labels_exchange_processes:
  fixes P Q P' Q' :: "('procS, 'procT) Proc"
    and α β       :: "('labS, 'labT) Lab"
  assumes rel:   "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and Pkind: "P ∼ST P'"
      and Qkind: "Q ∼ST Q'"
    shows "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
proof (cases "⦇P, α⦈↦⟨Q, β⟩")
  assume A1: "⦇P, α⦈↦⟨Q, β⟩"
  with Pkind have A2: "P' ∈ ProcS"
    using kinds_of_encoded_label(1)[of P α Q β]
    by blast
  from Qkind A1 have "Q' ∈ ProcT"
    using kinds_of_encoded_label(3)[of P α Q β]
    by blast
  with A1 A2 have "⦇P', α⦈↦⟨Q', β⟩"
    using encoded_label_exchange_processes[of P α Q β P' Q']
    by simp
  thus "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
    unfolding related_labels_def
    by simp
next
  assume A: "¬⦇P, α⦈↦⟨Q, β⟩"
  show "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
  proof (cases "⦇Q, β⦈↦⟨P, α⟩")
    assume B1: "⦇Q, β⦈↦⟨P, α⟩"
    with Qkind have B2: "Q' ∈ ProcS"
      using kinds_of_encoded_label(1)[of Q β P α]
      by blast
    from Pkind B1 have "P' ∈ ProcT"
      using kinds_of_encoded_label(3)[of Q β P α]
      by blast
    with B1 B2 have "⦇Q', β⦈↦⟨P', α⟩"
      using encoded_label_exchange_processes[of Q β P α Q' P']
      by simp
    thus "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      unfolding related_labels_def
      by simp
  next
    assume "¬⦇Q, β⦈↦⟨P, α⟩"
    with rel A have B1: "α = β" and B2: "P ∼ST Q"
      using related_labels_get_condition(1)[of P α Q β]
      by simp_all
    from Pkind Qkind B2 have "P' ∼ST Q'"
      by blast
    with B1 show "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      unfolding related_labels_def
      by simp
  qed
qed

lemma related_words_exchange_processes:
  fixes P Q P' Q' :: "('procS, 'procT) Proc"
    and w v       :: "('labS, 'labT) Lab list"
  assumes rel:   "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and Pkind: "P ∼ST P'"
      and Qkind: "Q ∼ST Q'"
    shows "⟨P', w⟩ ≡⦇⦈* ⟨Q', v⟩"
proof (cases "⦇P, w⦈↦*⟨Q, v⟩")
  assume A1: "⦇P, w⦈↦*⟨Q, v⟩"
  with Pkind have A2: "P' ∈ ProcS"
    using kinds_of_encoded_word(1)[of P w Q v]
    by blast
  from Qkind A1 have "Q' ∈ ProcT"
    using kinds_of_encoded_word(3)[of P w Q v]
    by blast
  with A1 A2 have "⦇P', w⦈↦*⟨Q', v⟩"
    using encoded_word_exchange_processes[of P w Q v P' Q']
    by simp
  thus "⟨P', w⟩ ≡⦇⦈* ⟨Q', v⟩"
    unfolding related_words_def
    by simp
next
  assume A: "¬⦇P, w⦈↦*⟨Q, v⟩"
  show "⟨P', w⟩ ≡⦇⦈* ⟨Q', v⟩"
  proof (cases "⦇Q, v⦈↦*⟨P, w⟩")
    assume B1: "⦇Q, v⦈↦*⟨P, w⟩"
    with Qkind have B2: "Q' ∈ ProcS"
      using kinds_of_encoded_word(1)[of Q v P w]
      by blast
    from Pkind B1 have "P' ∈ ProcT"
      using kinds_of_encoded_word(3)[of Q v P w]
      by blast
    with B1 B2 have "⦇Q', v⦈↦*⟨P', w⟩"
      using encoded_word_exchange_processes[of Q v P w Q' P']
      by simp
    thus "⟨P', w⟩ ≡⦇⦈* ⟨Q', v⟩"
      unfolding related_words_def
      by simp
  next
    assume "¬⦇Q, v⦈↦*⟨P, w⟩"
    with rel A have B1: "w = v" and B2: "P ∼ST Q"
      using related_words_get_condition(1)[of P w Q v]
      by simp_all
    from Pkind Qkind B2 have "P' ∼ST Q'"
      by blast
    with B1 show "⟨P', w⟩ ≡⦇⦈* ⟨Q', v⟩"
      unfolding related_words_def
      by simp
  qed
qed

text ‹Two related words and two related labels of of matching kinds can be composed into larger
      related words.›

lemma related_words_compose:
  fixes P Q P' Q' :: "('procS, 'procT) Proc"
    and w v       :: "('labS, 'labT) Lab list"
    and α β       :: "('labS, 'labT) Lab"
  assumes word:  "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and label: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      and Pkind: "P ∼ST P'"
      and Qkind: "Q ∼ST Q'"
    shows "⟨P, (w@[α])⟩ ≡⦇⦈* ⟨Q, (v@[β])⟩"
  using Pkind Qkind
proof auto
  fix SP SP' SQ SQ'
  assume "SP ∈S P" and "SQ ∈S Q"
  with word have A: "w = v"
    using related_words_equal[of P w Q v]
    by simp
  assume "SP' ∈S P'" and "SQ' ∈S Q'"
  with label have "α = β"
    using related_labels_equal[of P' α Q' β]
    by simp
  with A show "⟨SourceTerm SP, (w@[α])⟩ ≡⦇⦈* ⟨SourceTerm SQ, (v@[β])⟩"
    unfolding related_words_def
    by simp
next
  fix SP SP' TQ TQ'
  assume A1: "SP ∈S P" and A2: "TQ ∈T Q"
  with word have A3: "⦇P, w⦈↦*⟨Q, v⟩"
    using related_words_encL[of P w Q v]
    by simp
  assume "SP' ∈S P'" and "TQ' ∈T Q'"
  with label have "⦇P', α⦈↦⟨Q', β⟩"
    using related_labels_encL[of P' α Q' β]
    by simp
  with A1 A2 A3 have "⦇SourceTerm SP, w@[α]⦈↦*⟨TargetTerm TQ, v@[β]⟩"
    using ELCons[of P w Q v P' α Q' β]
    by simp
  thus "⟨SourceTerm SP, (w@[α])⟩ ≡⦇⦈* ⟨TargetTerm TQ, (v@[β])⟩"
    unfolding related_words_def
    by simp
next
  fix TP TP' SQ SQ'
  assume A1: "TP ∈T P" and A2: "SQ ∈S Q"
  with word have A3: "⦇Q, v⦈↦*⟨P, w⟩"
    using related_words_encL_rev[of P w Q v]
    by simp
  assume "TP' ∈T P'" and "SQ' ∈S Q'"
  with label have "⦇Q', β⦈↦⟨P', α⟩"
    using related_labels_encL_rev[of P' α Q' β]
    by simp
  with A1 A2 A3 have "⦇SourceTerm SQ, v@[β]⦈↦*⟨TargetTerm TP, w@[α]⟩"
    using ELCons[of Q v P w Q' β P' α]
    by simp
  thus "⟨TargetTerm TP, (w@[α])⟩ ≡⦇⦈* ⟨SourceTerm SQ, (v@[β])⟩"
    unfolding related_words_def
    by simp
next
  fix TP TP' TQ TQ'
  assume "TP ∈T P" and "TQ ∈T Q"
  with word have A: "w = v"
    using related_words_equal[of P w Q v]
    by simp
  assume "TP' ∈T P'" and "TQ' ∈T Q'"
  with label have "α = β"
    using related_labels_equal[of P' α Q' β]
    by simp
  with A show "⟨TargetTerm TP, (w@[α])⟩ ≡⦇⦈* ⟨TargetTerm TQ, (v@[β])⟩"
    unfolding related_words_def
    by simp
qed

lemma related_words_decompose:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes rel: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  shows "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                   ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
proof (cases "w = []")
  assume "w = []"
  thus "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                  ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
    by simp
next
  assume A1: "w ≠ []"
  with rel have A2: "v ≠ []"
    using related_words_length[of P w Q v]
    by auto
  show "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                  ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
  proof (cases "⦇P, w⦈↦*⟨Q, v⟩")
    assume B1: "⦇P, w⦈↦*⟨Q, v⟩"
    hence B2: "P ∈ ProcS" and B3: "Q ∈ ProcT"
      using kinds_of_encoded_word(1, 3)[of P w Q v]
      by simp_all
    from A1 B1 obtain w' α v' β P' Q' where B4: "w = w'@[α]" and B5: "v = v'@[β]"
                                        and B6: "⦇P, w'⦈↦*⟨Q, v'⟩" and B7: "⦇P', α⦈↦⟨Q', β⟩"
                                        and B8: "P' ∈ ProcS" and B9: "Q' ∈ ProcT"
      using encoded_word_decompose[of P w Q v]
      by blast
    from B6 have B10: "⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩"
      unfolding related_words_def
      by simp
    from B7 have B11: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
      unfolding related_labels_def
      by simp
    from B2 B8 have B12: "P ∼ST P'"
      by simp
    from B3 B9 have "Q ∼ST Q'"
      by simp
    with A1 B4 B5 B10 B11 B12
    show "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                    ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
      by blast
  next
    assume B: "¬⦇P, w⦈↦*⟨Q, v⟩"
    show "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                    ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
    proof (cases "⦇Q, v⦈↦*⟨P, w⟩")
      assume C1: "⦇Q, v⦈↦*⟨P, w⟩"
      hence C2: "Q ∈ ProcS" and C3: "P ∈ ProcT"
        using kinds_of_encoded_word(1, 3)[of Q v P w]
        by simp_all
      from A2 C1 obtain w' α v' β P' Q' where C4: "w = w'@[α]" and C5: "v = v'@[β]"
                                          and C6: "⦇Q, v'⦈↦*⟨P, w'⟩" and C7: "⦇Q', β⦈↦⟨P', α⟩"
                                          and C8: "Q' ∈ ProcS" and C9: "P' ∈ ProcT"
        using encoded_word_decompose[of Q v P w]
        by blast
      from C6 have C10: "⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩"
        unfolding related_words_def
        by simp
      from C7 have C11: "⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩"
        unfolding related_labels_def
        by simp
      from C2 C8 have C12: "Q ∼ST Q'"
        by simp
      from C3 C9 have "P ∼ST P'"
        by simp
      with A1 C4 C5 C10 C11 C12
      show "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                      ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
        by blast
    next
      assume "¬⦇Q, v⦈↦*⟨P, w⟩"
      with rel B have C1: "w = v" and C2: "P ∼ST Q"
        using related_words_get_condition(1)[of P w Q v]
        by simp_all
      from A1 obtain w' α where C3: "w = w'@[α]"
        by (metis snoc_eq_iff_butlast)
      from C1 C3 have C4: "v = w'@[α]"
        by simp
      have C5: "P ∼ST P"
        using source_or_target
        by presburger
      hence "⟨P, w'⟩ ≡⦇⦈* ⟨P, w'⟩"
        unfolding related_words_def
        by simp
      with C2 C5 have C6: "⟨P, w'⟩ ≡⦇⦈* ⟨Q, w'⟩"
        using related_words_exchange_processes[of P w' P w' P Q]
        by simp
      from C5 have "⟨P, α⟩ ≡⦇⦈ ⟨P, α⟩"
        unfolding related_labels_def
        by simp
      with C2 C5 have C7: "⟨P, α⟩ ≡⦇⦈ ⟨Q, α⟩"
        using related_labels_exchange_processes[of P α P α P Q]
        by simp
      have "Q ∼ST Q"
        using source_or_target
        by presburger
      with A1 C3 C4 C5 C6 C7
      show "w = [] ∨ (∃w' α v' β P' Q'. w = w'@[α] ∧ v = v'@[β] ∧ ⟨P, w'⟩ ≡⦇⦈* ⟨Q, v'⟩ ∧
                      ⟨P', α⟩ ≡⦇⦈ ⟨Q', β⟩ ∧ P ∼ST P' ∧ Q ∼ST Q')"
        by blast
    qed
  qed
qed

text ‹The relations of related labels and related words are equivalences, where for transitivity
      we have to additionally require that the label encoding is injective or that no target
      process is ever related to a source process.›

lemma related_labels_refl:
  fixes P :: "('procS, 'procT) Proc"
    and α :: "('labS, 'labT) Lab"
  shows "⟨P, α⟩ ≡⦇⦈ ⟨P, α⟩"
proof -
  have "P ∼ST P"
    using source_or_target[of P]
    by presburger
  thus "⟨P, α⟩ ≡⦇⦈ ⟨P, α⟩"
    unfolding related_labels_def
    by simp
qed

lemma related_words_refl:
  fixes P :: "('procS, 'procT) Proc"
    and w :: "('labS, 'labT) Lab list"
  shows "⟨P, w⟩ ≡⦇⦈* ⟨P, w⟩"
proof -
  have "P ∼ST P"
    using source_or_target[of P]
    by presburger
  thus "⟨P, w⟩ ≡⦇⦈* ⟨P, w⟩"
    unfolding related_words_def
    by simp
qed

lemma related_labels_sym:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
  shows "⟨Q, β⟩ ≡⦇⦈ ⟨P, α⟩"
  using assms
  unfolding related_labels_def
  by auto

lemma related_words_sym:
  fixes P Q :: "('procS, 'procT) Proc"
    and w v :: "('labS, 'labT) Lab list"
  assumes "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
  shows "⟨Q, v⟩ ≡⦇⦈* ⟨P, w⟩"
  using assms
  unfolding related_words_def
  by auto

lemma related_labels_trans_inj:
  fixes P Q R :: "('procS, 'procT) Proc"
    and α β γ :: "('labS, 'labT) Lab"
  assumes rel1: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and rel2: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
      and inj:  "inj encL"
    shows "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
proof (cases "⦇P, α⦈↦⟨Q, β⟩")
  assume A1: "⦇P, α⦈↦⟨Q, β⟩"
  hence A2: "P ∈ ProcS" and A3: "Q ∈ ProcT"
    using kinds_of_encoded_label(1, 3)[of P α Q β]
    by simp_all
  show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
  proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
    assume "⦇Q, β⦈↦⟨R, γ⟩"
    hence "Q ∈ ProcS"
      using kinds_of_encoded_label(1)[of Q β R γ]
      by simp
    with A3 have False
      by blast
    thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      by simp
  next
    assume B: "¬⦇Q, β⦈↦⟨R, γ⟩"
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
      assume C1: "⦇R, γ⦈↦⟨Q, β⟩"
      with inj A1 have C2: "α = γ"
        using encoded_label_unique_rev[of P α Q β R γ]
        by simp
      from C1 have "R ∈ ProcS"
        using kinds_of_encoded_label(1)[of R γ Q β]
        by simp
      with A2 have "P ∼ST R"
        by simp
      with C2 show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        unfolding related_labels_def
        by simp
    next
      assume "¬⦇R, γ⦈↦⟨Q, β⟩"
      with rel2 B have C1: "β = γ" and C2: "Q ∼ST R"
        using related_labels_get_condition(1)[of Q β R γ]
        by simp_all
      from A1 C1 have C3: "⦇P, α⦈↦⟨Q, γ⟩"
        by simp
      from A3 C2 have "R ∈ ProcT"
        by blast
      with A2 C3 have "⦇P, α⦈↦⟨R, γ⟩"
        using encoded_label_exchange_processes[of P α Q γ P R]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        unfolding related_labels_def
        by simp
    qed
  qed
next
  assume A: "¬⦇P, α⦈↦⟨Q, β⟩"
  show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
  proof (cases "⦇Q, β⦈↦⟨P, α⟩")
    assume B1: "⦇Q, β⦈↦⟨P, α⟩"
    hence B2: "Q ∈ ProcS" and B3: "P ∈ ProcT"
      using kinds_of_encoded_label(1, 3)[of Q β P α]
      by simp_all
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
      assume C1: "⦇Q, β⦈↦⟨R, γ⟩"
      with inj B1 have C2: "α = γ"
        using encoded_label_unique[of Q β P α R γ]
        by simp
      from C1 have "R ∈ ProcT"
        using kinds_of_encoded_label(3)[of Q β R γ]
        by simp
      with B3 have "P ∼ST R"
        by simp
      with C2 show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        unfolding related_labels_def
        by simp
    next
      assume C: "¬⦇Q, β⦈↦⟨R, γ⟩"
      show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
        assume "⦇R, γ⦈↦⟨Q, β⟩"
        hence "Q ∈ ProcT"
          using kinds_of_encoded_label(3)[of R γ Q β]
          by simp
        with B2 have False
          by blast
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          by simp
      next
        assume "¬⦇R, γ⦈↦⟨Q, β⟩"
        with rel2 C have D1: "β = γ" and D2: "Q ∼ST R"
          using related_labels_get_condition(1)[of Q β R γ]
          by simp_all
        from B1 D1 have D3: "⦇Q, γ⦈↦⟨P, α⟩"
          by simp
        from B2 D2 have "R ∈ ProcS"
          by blast
        with B3 D3 have "⦇R, γ⦈↦⟨P, α⟩"
          using encoded_label_exchange_processes[of Q γ P α R P]
          by simp
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      qed
    qed
  next
    assume "¬⦇Q, β⦈↦⟨P, α⟩"
    with rel1 A have A1: "α = β" and A2: "P ∼ST Q"
      using related_labels_get_condition(1)[of P α Q β]
      by simp_all
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
      assume B1: "⦇Q, β⦈↦⟨R, γ⟩"
      with A1 have B2: "⦇Q, α⦈↦⟨R, γ⟩"
        by simp
      from B1 have "Q ∈ ProcS"
        using kinds_of_encoded_label(1)[of Q β R γ]
        by simp
      with A2 have B3: "P ∈ ProcS"
        by blast
      from B1 have "R ∈ ProcT"
        using kinds_of_encoded_label(3)[of Q β R γ]
        by simp
      with B2 B3 have "⦇P, α⦈↦⟨R, γ⟩"
        using encoded_label_exchange_processes[of Q α R γ P R]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        unfolding related_labels_def
        by simp
    next
      assume B: "¬⦇Q, β⦈↦⟨R, γ⟩"
      show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
        assume C1: "⦇R, γ⦈↦⟨Q, β⟩"
        with A1 have C2: "⦇R, γ⦈↦⟨Q, α⟩"
          by simp
        from C1 have C3: "R ∈ ProcS"
          using kinds_of_encoded_label(1)[of R γ Q β]
          by simp
        from C1 have "Q ∈ ProcT"
          using kinds_of_encoded_label(3)[of R γ Q β]
          by simp
        with A2 have "P ∈ ProcT"
          by blast
        with C2 C3 have "⦇R, γ⦈↦⟨P, α⟩"
          using encoded_label_exchange_processes[of R γ Q α R P]
          by simp
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      next
        assume "¬⦇R, γ⦈↦⟨Q, β⟩"
        with rel2 B have C1: "β = γ" and C2: "Q ∼ST R"
          using related_labels_get_condition(1)[of Q β R γ]
          by simp_all
        from A1 C1 have "α = γ"
          by simp
        moreover from A2 C2 have "P ∼ST R"
          by blast
        ultimately show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      qed
    qed
  qed
qed

lemma related_labels_trans_no_T_to_S:
  fixes P Q R :: "('procS, 'procT) Proc"
    and α β γ :: "('labS, 'labT) Lab"
  assumes rel1: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and rel2: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
      and noTS: "¬(P ∈ ProcT ∧ Q ∈ ProcS) ∧ ¬(Q ∈ ProcT ∧ R ∈ ProcS)"
    shows "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
proof (cases "⦇P, α⦈↦⟨Q, β⟩")
  assume A1: "⦇P, α⦈↦⟨Q, β⟩"
  hence A2: "P ∈ ProcS" and A3: "Q ∈ ProcT"
    using kinds_of_encoded_label(1, 3)[of P α Q β]
    by simp_all
  show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
  proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
    assume "⦇Q, β⦈↦⟨R, γ⟩"
    hence "Q ∈ ProcS"
      using kinds_of_encoded_label(1)[of Q β R γ]
      by simp
    with A3 have False
      by blast
    thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      by simp
  next
    assume B: "¬⦇Q, β⦈↦⟨R, γ⟩"
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
      assume "⦇R, γ⦈↦⟨Q, β⟩"
      with noTS have False
        using kinds_of_encoded_label(1, 3)[of R γ Q β]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        by simp
    next
      assume "¬⦇R, γ⦈↦⟨Q, β⟩"
      with rel2 B have C1: "β = γ" and C2: "Q ∼ST R"
        using related_labels_get_condition(1)[of Q β R γ]
        by simp_all
      from A1 C1 have C3: "⦇P, α⦈↦⟨Q, γ⟩"
        by simp
      from A3 C2 have "R ∈ ProcT"
        by blast
      with A2 C3 have "⦇P, α⦈↦⟨R, γ⟩"
        using encoded_label_exchange_processes[of P α Q γ P R]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        unfolding related_labels_def
        by simp
    qed
  qed
next
  assume A: "¬⦇P, α⦈↦⟨Q, β⟩"
  show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
  proof (cases "⦇Q, β⦈↦⟨P, α⟩")
    assume "⦇Q, β⦈↦⟨P, α⟩"
    with noTS have False
      using kinds_of_encoded_label(1, 3)[of Q β P α]
      by simp
    thus  "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      by simp
  next
    assume "¬⦇Q, β⦈↦⟨P, α⟩"
    with rel1 A have A1: "α = β" and A2: "P ∼ST Q"
      using related_labels_get_condition(1)[of P α Q β]
      by simp_all
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
      assume B1: "⦇Q, β⦈↦⟨R, γ⟩"
      with A1 have B2: "⦇Q, α⦈↦⟨R, γ⟩"
        by simp
      from B1 have "Q ∈ ProcS"
        using kinds_of_encoded_label(1)[of Q β R γ]
        by simp
      with A2 have B3: "P ∈ ProcS"
        by blast
      from B1 have "R ∈ ProcT"
        using kinds_of_encoded_label(3)[of Q β R γ]
        by simp
      with B2 B3 have "⦇P, α⦈↦⟨R, γ⟩"
        using encoded_label_exchange_processes[of Q α R γ P R]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        unfolding related_labels_def
        by simp
    next
      assume B: "¬⦇Q, β⦈↦⟨R, γ⟩"
      show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
        assume "⦇R, γ⦈↦⟨Q, β⟩"
        with noTS have False
          using kinds_of_encoded_label(1, 3)[of R γ Q β]
          by simp
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          by simp
      next
        assume "¬⦇R, γ⦈↦⟨Q, β⟩"
        with rel2 B have C1: "β = γ" and C2: "Q ∼ST R"
          using related_labels_get_condition(1)[of Q β R γ]
          by simp_all
        from A1 C1 have "α = γ"
          by simp
        moreover from A2 C2 have "P ∼ST R"
          by blast
        ultimately show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      qed
    qed
  qed
qed

lemma related_labels_trans_no_S_to_T:
  fixes P Q R :: "('procS, 'procT) Proc"
    and α β γ :: "('labS, 'labT) Lab"
  assumes rel1: "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and rel2: "⟨Q, β⟩ ≡⦇⦈ ⟨R, γ⟩"
      and noST: "¬(P ∈ ProcS ∧ Q ∈ ProcT) ∧ ¬(Q ∈ ProcS ∧ R ∈ ProcT)"
    shows "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
proof (cases "⦇P, α⦈↦⟨Q, β⟩")
  assume A1: "⦇P, α⦈↦⟨Q, β⟩"
  with noST have False
    using kinds_of_encoded_label(1, 3)[of P α Q β]
    by simp
  thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    by simp
next
  assume A: "¬⦇P, α⦈↦⟨Q, β⟩"
  show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
  proof (cases "⦇Q, β⦈↦⟨P, α⟩")
    assume B1: "⦇Q, β⦈↦⟨P, α⟩"
    hence B2: "Q ∈ ProcS" and B3: "P ∈ ProcT"
      using kinds_of_encoded_label(1, 3)[of Q β P α]
      by simp_all
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
      assume "⦇Q, β⦈↦⟨R, γ⟩"
      with noST have False
        using kinds_of_encoded_label(1, 3)[of Q β R γ]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        by simp
    next
      assume C: "¬⦇Q, β⦈↦⟨R, γ⟩"
      show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
        assume "⦇R, γ⦈↦⟨Q, β⟩"
        hence "Q ∈ ProcT"
          using kinds_of_encoded_label(3)[of R γ Q β]
          by simp
        with B2 have False
          by blast
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          by simp
      next
        assume "¬⦇R, γ⦈↦⟨Q, β⟩"
        with rel2 C have D1: "β = γ" and D2: "Q ∼ST R"
          using related_labels_get_condition(1)[of Q β R γ]
          by simp_all
        from B1 D1 have D3: "⦇Q, γ⦈↦⟨P, α⟩"
          by simp
        from B2 D2 have "R ∈ ProcS"
          by blast
        with B3 D3 have "⦇R, γ⦈↦⟨P, α⟩"
          using encoded_label_exchange_processes[of Q γ P α R P]
          by simp
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      qed
    qed
  next
    assume "¬⦇Q, β⦈↦⟨P, α⟩"
    with rel1 A have A1: "α = β" and A2: "P ∼ST Q"
      using related_labels_get_condition(1)[of P α Q β]
      by simp_all
    show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
    proof (cases "⦇Q, β⦈↦⟨R, γ⟩")
      assume "⦇Q, β⦈↦⟨R, γ⟩"
      with noST have False
        using kinds_of_encoded_label(1, 3)[of Q β R γ]
        by simp
      thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
        by simp
    next
      assume B: "¬⦇Q, β⦈↦⟨R, γ⟩"
      show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
      proof (cases "⦇R, γ⦈↦⟨Q, β⟩")
        assume C1: "⦇R, γ⦈↦⟨Q, β⟩"
        with A1 have C2: "⦇R, γ⦈↦⟨Q, α⟩"
          by simp
        from C1 have C3: "R ∈ ProcS"
          using kinds_of_encoded_label(1)[of R γ Q β]
          by simp
        from C1 have "Q ∈ ProcT"
          using kinds_of_encoded_label(3)[of R γ Q β]
          by simp
        with A2 have "P ∈ ProcT"
          by blast
        with C2 C3 have "⦇R, γ⦈↦⟨P, α⟩"
          using encoded_label_exchange_processes[of R γ Q α R P]
          by simp
        thus "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      next
        assume "¬⦇R, γ⦈↦⟨Q, β⟩"
        with rel2 B have C1: "β = γ" and C2: "Q ∼ST R"
          using related_labels_get_condition(1)[of Q β R γ]
          by simp_all
        from A1 C1 have "α = γ"
          by simp
        moreover from A2 C2 have "P ∼ST R"
          by blast
        ultimately show "⟨P, α⟩ ≡⦇⦈ ⟨R, γ⟩"
          unfolding related_labels_def
          by simp
      qed
    qed
  qed
qed

lemma related_words_trans_inj:
  fixes P Q R :: "('procS, 'procT) Proc"
    and w v y :: "('labS, 'labT) Lab list"
  assumes rel1: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and rel2: "⟨Q, v⟩ ≡⦇⦈* ⟨R, y⟩"
      and inj:  "inj encL"
    shows "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
proof (cases "⦇P, w⦈↦*⟨Q, v⟩")
  assume A1: "⦇P, w⦈↦*⟨Q, v⟩"
  hence A2: "P ∈ ProcS" and A3: "Q ∈ ProcT"
    using kinds_of_encoded_word(1, 3)[of P w Q v]
    by simp_all
  show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
  proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
    assume "⦇Q, v⦈↦*⟨R, y⟩"
    hence "Q ∈ ProcS"
      using kinds_of_encoded_word(1)[of Q v R y]
      by simp
    with A3 have False
      by blast
    thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      by simp
  next
    assume B: "¬⦇Q, v⦈↦*⟨R, y⟩"
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
      assume C1: "⦇R, y⦈↦*⟨Q, v⟩"
      with inj A1 have C2: "w = y"
        using encoded_word_unique_rev[of P w Q v R y]
        by simp
      from C1 have "R ∈ ProcS"
        using kinds_of_encoded_word(1)[of R y Q v]
        by simp
      with A2 have "P ∼ST R"
        by simp
      with C2 show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        unfolding related_words_def
        by simp
    next
      assume "¬⦇R, y⦈↦*⟨Q, v⟩"
      with rel2 B have C1: "v = y" and C2: "Q ∼ST R"
        using related_words_get_condition(1)[of Q v R y]
        by simp_all
      from A1 C1 have C3: "⦇P, w⦈↦*⟨Q, y⟩"
        by simp
      from A3 C2 have "R ∈ ProcT"
        by blast
      with A2 C3 have "⦇P, w⦈↦*⟨R, y⟩"
        using encoded_word_exchange_processes[of P w Q y P R]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        unfolding related_words_def
        by simp
    qed
  qed
next
  assume A: "¬⦇P, w⦈↦*⟨Q, v⟩"
  show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
  proof (cases "⦇Q, v⦈↦*⟨P, w⟩")
    assume B1: "⦇Q, v⦈↦*⟨P, w⟩"
    hence B2: "Q ∈ ProcS" and B3: "P ∈ ProcT"
      using kinds_of_encoded_word(1, 3)[of Q v P w]
      by simp_all
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
      assume C1: "⦇Q, v⦈↦*⟨R, y⟩"
      with inj B1 have C2: "w = y"
        using encoded_word_unique[of Q v P w R y]
        by simp
      from C1 have "R ∈ ProcT"
        using kinds_of_encoded_word(3)[of Q v R y]
        by simp
      with B3 have "P ∼ST R"
        by simp
      with C2 show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        unfolding related_words_def
        by simp
    next
      assume C: "¬⦇Q, v⦈↦*⟨R, y⟩"
      show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
        assume "⦇R, y⦈↦*⟨Q, v⟩"
        hence "Q ∈ ProcT"
          using kinds_of_encoded_word(3)[of R y Q v]
          by simp
        with B2 have False
          by blast
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          by simp
      next
        assume "¬⦇R, y⦈↦*⟨Q, v⟩"
        with rel2 C have D1: "v = y" and D2: "Q ∼ST R"
          using related_words_get_condition(1)[of Q v R y]
          by simp_all
        from B1 D1 have D3: "⦇Q, y⦈↦*⟨P, w⟩"
          by simp
        from B2 D2 have "R ∈ ProcS"
          by blast
        with B3 D3 have "⦇R, y⦈↦*⟨P, w⟩"
          using encoded_word_exchange_processes[of Q y P w R P]
          by simp
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      qed
    qed
  next
    assume "¬⦇Q, v⦈↦*⟨P, w⟩"
    with rel1 A have A1: "w = v" and A2: "P ∼ST Q"
      using related_words_get_condition(1)[of P w Q v]
      by simp_all
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
      assume B1: "⦇Q, v⦈↦*⟨R, y⟩"
      with A1 have B2: "⦇Q, w⦈↦*⟨R, y⟩"
        by simp
      from B1 have "Q ∈ ProcS"
        using kinds_of_encoded_word(1)[of Q v R y]
        by simp
      with A2 have B3: "P ∈ ProcS"
        by blast
      from B1 have "R ∈ ProcT"
        using kinds_of_encoded_word(3)[of Q v R y]
        by simp
      with B2 B3 have "⦇P, w⦈↦*⟨R, y⟩"
        using encoded_word_exchange_processes[of Q w R y P R]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        unfolding related_words_def
        by simp
    next
      assume B: "¬⦇Q, v⦈↦*⟨R, y⟩"
      show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
        assume C1: "⦇R, y⦈↦*⟨Q, v⟩"
        with A1 have C2: "⦇R, y⦈↦*⟨Q, w⟩"
          by simp
        from C1 have C3: "R ∈ ProcS"
          using kinds_of_encoded_word(1)[of R y Q v]
          by simp
        from C1 have "Q ∈ ProcT"
          using kinds_of_encoded_word(3)[of R y Q v]
          by simp
        with A2 have "P ∈ ProcT"
          by blast
        with C2 C3 have "⦇R, y⦈↦*⟨P, w⟩"
          using encoded_word_exchange_processes[of R y Q w R P]
          by simp
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      next
        assume "¬⦇R, y⦈↦*⟨Q, v⟩"
        with rel2 B have C1: "v = y" and C2: "Q ∼ST R"
          using related_words_get_condition(1)[of Q v R y]
          by simp_all
        from A1 C1 have "w = y"
          by simp
        moreover from A2 C2 have "P ∼ST R"
          by blast
        ultimately show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      qed
    qed
  qed
qed

lemma related_words_trans_no_T_to_S:
  fixes P Q R :: "('procS, 'procT) Proc"
    and w v y :: "('labS, 'labT) Lab list"
  assumes rel1: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and rel2: "⟨Q, v⟩ ≡⦇⦈* ⟨R, y⟩"
      and noTS: "¬(P ∈ ProcT ∧ Q ∈ ProcS) ∧ ¬(Q ∈ ProcT ∧ R ∈ ProcS)"
    shows "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
proof (cases "⦇P, w⦈↦*⟨Q, v⟩")
  assume A1: "⦇P, w⦈↦*⟨Q, v⟩"
  hence A2: "P ∈ ProcS" and A3: "Q ∈ ProcT"
    using kinds_of_encoded_word(1, 3)[of P w Q v]
    by simp_all
  show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
  proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
    assume "⦇Q, v⦈↦*⟨R, y⟩"
    hence "Q ∈ ProcS"
      using kinds_of_encoded_word(1)[of Q v R y]
      by simp
    with A3 have False
      by blast
    thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      by simp
  next
    assume B: "¬⦇Q, v⦈↦*⟨R, y⟩"
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
      assume "⦇R, y⦈↦*⟨Q, v⟩"
      with noTS have False
        using kinds_of_encoded_word(1, 3)[of R y Q v]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        by simp
    next
      assume "¬⦇R, y⦈↦*⟨Q, v⟩"
      with rel2 B have C1: "v = y" and C2: "Q ∼ST R"
        using related_words_get_condition(1)[of Q v R y]
        by simp_all
      from A1 C1 have C3: "⦇P, w⦈↦*⟨Q, y⟩"
        by simp
      from A3 C2 have "R ∈ ProcT"
        by blast
      with A2 C3 have "⦇P, w⦈↦*⟨R, y⟩"
        using encoded_word_exchange_processes[of P w Q y P R]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        unfolding related_words_def
        by simp
    qed
  qed
next
  assume A: "¬⦇P, w⦈↦*⟨Q, v⟩"
  show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
  proof (cases "⦇Q, v⦈↦*⟨P, w⟩")
    assume "⦇Q, v⦈↦*⟨P, w⟩"
    with noTS have False
      using kinds_of_encoded_word(1, 3)[of Q v P w]
      by simp
    thus  "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      by simp
  next
    assume "¬⦇Q, v⦈↦*⟨P, w⟩"
    with rel1 A have A1: "w = v" and A2: "P ∼ST Q"
      using related_words_get_condition(1)[of P w Q v]
      by simp_all
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
      assume B1: "⦇Q, v⦈↦*⟨R, y⟩"
      with A1 have B2: "⦇Q, w⦈↦*⟨R, y⟩"
        by simp
      from B1 have "Q ∈ ProcS"
        using kinds_of_encoded_word(1)[of Q v R y]
        by simp
      with A2 have B3: "P ∈ ProcS"
        by blast
      from B1 have "R ∈ ProcT"
        using kinds_of_encoded_word(3)[of Q v R y]
        by simp
      with B2 B3 have "⦇P, w⦈↦*⟨R, y⟩"
        using encoded_word_exchange_processes[of Q w R y P R]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        unfolding related_words_def
        by simp
    next
      assume B: "¬⦇Q, v⦈↦*⟨R, y⟩"
      show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
        assume "⦇R, y⦈↦*⟨Q, v⟩"
        with noTS have False
          using kinds_of_encoded_word(1, 3)[of R y Q v]
          by simp
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          by simp
      next
        assume "¬⦇R, y⦈↦*⟨Q, v⟩"
        with rel2 B have C1: "v = y" and C2: "Q ∼ST R"
          using related_words_get_condition(1)[of Q v R y]
          by simp_all
        from A1 C1 have "w = y"
          by simp
        moreover from A2 C2 have "P ∼ST R"
          by blast
        ultimately show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      qed
    qed
  qed
qed

lemma related_words_trans_no_S_to_T:
  fixes P Q R :: "('procS, 'procT) Proc"
    and w v y :: "('labS, 'labT) Lab list"
  assumes rel1: "⟨P, w⟩ ≡⦇⦈* ⟨Q, v⟩"
      and rel2: "⟨Q, v⟩ ≡⦇⦈* ⟨R, y⟩"
      and noST: "¬(P ∈ ProcS ∧ Q ∈ ProcT) ∧ ¬(Q ∈ ProcS ∧ R ∈ ProcT)"
    shows "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
proof (cases "⦇P, w⦈↦*⟨Q, v⟩")
  assume A1: "⦇P, w⦈↦*⟨Q, v⟩"
  with noST have False
    using kinds_of_encoded_word(1, 3)[of P w Q v]
    by simp
  thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    by simp
next
  assume A: "¬⦇P, w⦈↦*⟨Q, v⟩"
  show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
  proof (cases "⦇Q, v⦈↦*⟨P, w⟩")
    assume B1: "⦇Q, v⦈↦*⟨P, w⟩"
    hence B2: "Q ∈ ProcS" and B3: "P ∈ ProcT"
      using kinds_of_encoded_word(1, 3)[of Q v P w]
      by simp_all
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
      assume "⦇Q, v⦈↦*⟨R, y⟩"
      with noST have False
        using kinds_of_encoded_word(1, 3)[of Q v R y]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        by simp
    next
      assume C: "¬⦇Q, v⦈↦*⟨R, y⟩"
      show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
        assume "⦇R, y⦈↦*⟨Q, v⟩"
        hence "Q ∈ ProcT"
          using kinds_of_encoded_word(3)[of R y Q v]
          by simp
        with B2 have False
          by blast
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          by simp
      next
        assume "¬⦇R, y⦈↦*⟨Q, v⟩"
        with rel2 C have D1: "v = y" and D2: "Q ∼ST R"
          using related_words_get_condition(1)[of Q v R y]
          by simp_all
        from B1 D1 have D3: "⦇Q, y⦈↦*⟨P, w⟩"
          by simp
        from B2 D2 have "R ∈ ProcS"
          by blast
        with B3 D3 have "⦇R, y⦈↦*⟨P, w⟩"
          using encoded_word_exchange_processes[of Q y P w R P]
          by simp
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      qed
    qed
  next
    assume "¬⦇Q, v⦈↦*⟨P, w⟩"
    with rel1 A have A1: "w = v" and A2: "P ∼ST Q"
      using related_words_get_condition(1)[of P w Q v]
      by simp_all
    show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
    proof (cases "⦇Q, v⦈↦*⟨R, y⟩")
      assume "⦇Q, v⦈↦*⟨R, y⟩"
      with noST have False
        using kinds_of_encoded_word(1, 3)[of Q v R y]
        by simp
      thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
        by simp
    next
      assume B: "¬⦇Q, v⦈↦*⟨R, y⟩"
      show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
      proof (cases "⦇R, y⦈↦*⟨Q, v⟩")
        assume C1: "⦇R, y⦈↦*⟨Q, v⟩"
        with A1 have C2: "⦇R, y⦈↦*⟨Q, w⟩"
          by simp
        from C1 have C3: "R ∈ ProcS"
          using kinds_of_encoded_word(1)[of R y Q v]
          by simp
        from C1 have "Q ∈ ProcT"
          using kinds_of_encoded_word(3)[of R y Q v]
          by simp
        with A2 have "P ∈ ProcT"
          by blast
        with C2 C3 have "⦇R, y⦈↦*⟨P, w⟩"
          using encoded_word_exchange_processes[of R y Q w R P]
          by simp
        thus "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      next
        assume "¬⦇R, y⦈↦*⟨Q, v⟩"
        with rel2 B have C1: "v = y" and C2: "Q ∼ST R"
          using related_words_get_condition(1)[of Q v R y]
          by simp_all
        from A1 C1 have "w = y"
          by simp
        moreover from A2 C2 have "P ∼ST R"
          by blast
        ultimately show "⟨P, w⟩ ≡⦇⦈* ⟨R, y⟩"
          unfolding related_words_def
          by simp
      qed
    qed
  qed
qed

text ‹For a labelled semantics the internal label is of special relevance, since it is used to
      define weak notions of steps. We say that the encoding on labels preserves the internal if it
      translates the internal of the source to the internal of the target. It reflects the internal
      if the internal of the target is used as result of the encoding of labels only in the
      translation of the source internal label. Finally, an encoding on labels respects the
      internal if it preserves and reflects the internal.›

abbreviation encL_preserves_internal :: "bool" where
  "encL_preserves_internal ≡ ⦉τ-Source⦊ = τ-Target"

abbreviation encL_reflects_internal :: "bool" where
  "encL_reflects_internal ≡ ∀α. ⦉α⦊ = τ-Target ⟶ α = τ-Source"

abbreviation encL_respects_internal :: "bool" where
  "encL_respects_internal ≡ encL_preserves_internal ∧ encL_reflects_internal"

text ‹An injective label encoding that preserves the internal also respects the internal.›

lemma inj_preserves_is_respects_internal:
  assumes "inj encL"
      and "encL_preserves_internal"
    shows "encL_respects_internal"
  using assms
  unfolding inj_def
  by simp

text ‹If an encoding relates a source and a target step on internals, then the encoding preserves
      the internal.›

lemma related_labels_preserves_internal:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes rel:  "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, τ-STLCal⟩"
      and cond: "¬(P ∈ ProcS ⟷ Q ∈ ProcS)"
    shows "encL_preserves_internal"
  using assms
  unfolding related_labels_def encLST_def getSourceLabel_def getTargetLabel_def
  by blast

text ‹If the encoding of labels preserves the internal, then a source internal is related to an
      internal.›

lemma encL_preserves_internal_implies_source_internal_to_internal:
  fixes P Q :: "('procS, 'procT) Proc"
    and β   :: "('labS, 'labT) Lab"
  assumes rel:  "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
      and kind: "P ∈ ProcS"
      and pre:  "encL_preserves_internal"
    shows "β = τ-STLCal"
proof (cases "⦇P, τ-STLCal⦈↦⟨Q, β⟩")
  assume "⦇P, τ-STLCal⦈↦⟨Q, β⟩"
  then obtain α' β' where A1: "α' ∈SL ⟨P, τ-STLCal⟩" and A2: "β' ∈TL ⟨Q, β⟩" and A3: "⦉α'⦊ = β'"
    unfolding encLST_def
    by blast
  from A1 have "α' = τ-Source"
    unfolding getSourceLabel_def
    by simp
  with pre A3 have "β' = τ-Target"
    by simp
  with A2 show "β = τ-STLCal"
    unfolding getTargetLabel_def
    by simp
next
  assume A1: "¬⦇P, τ-STLCal⦈↦⟨Q, β⟩"
  from kind have "¬⦇Q, β⦈↦⟨P, τ-STLCal⟩"
    using kinds_of_encoded_label(3)[of Q β P "τ-STLCal"]
    by blast
  with rel A1 show "β = τ-STLCal"
    using related_labels_get_condition(1)[of P "τ-STLCal" Q β]
    by simp
qed

lemma encL_preserves_internal_implies_source_internal_to_internal_right:
  fixes P Q :: "('procS, 'procT) Proc"
    and α   :: "('labS, 'labT) Lab"
  assumes rel:  "⟨P, α⟩ ≡⦇⦈ ⟨Q, τ-STLCal⟩"
      and kind: "Q ∈ ProcS"
      and pre:  "encL_preserves_internal"
    shows "α = τ-STLCal"
proof (cases "⦇Q, τ-STLCal⦈↦⟨P, α⟩")
  assume "⦇Q, τ-STLCal⦈↦⟨P, α⟩"
  then obtain α' β' where A1: "β' ∈SL ⟨Q, τ-STLCal⟩" and A2: "α' ∈TL ⟨P, α⟩" and A3: "⦉β'⦊ = α'"
    unfolding encLST_def
    by blast
  from A1 have "β' = τ-Source"
    unfolding getSourceLabel_def
    by simp
  with pre A3 have "α' = τ-Target"
    by simp
  with A2 show "α = τ-STLCal"
    unfolding getTargetLabel_def
    by simp
next
  assume A1: "¬⦇Q, τ-STLCal⦈↦⟨P, α⟩"
  from kind have "¬⦇P, α⦈↦⟨Q, τ-STLCal⟩"
    using kinds_of_encoded_label(3)[of P α Q "τ-STLCal"]
    by blast
  with rel A1 show "α = τ-STLCal"
    using related_labels_get_condition(1)[of P α Q "τ-STLCal"]
    by simp
qed

text ‹If the encoding of labels reflects the internal, then a target internal is related to an
      internal.›

lemma encL_reflects_internal_implies_target_internal_to_internal:
  fixes P Q :: "('procS, 'procT) Proc"
    and β   :: "('labS, 'labT) Lab"
  assumes rel:  "⟨P, τ-STLCal⟩ ≡⦇⦈ ⟨Q, β⟩"
      and kind: "P ∈ ProcT"
      and ref:  "encL_reflects_internal"
    shows "β = τ-STLCal"
proof (cases "⦇Q, β⦈↦⟨P, τ-STLCal⟩")
  assume "⦇Q, β⦈↦⟨P, τ-STLCal⟩"
  then obtain α' β' where A1: "α' ∈TL ⟨P, τ-STLCal⟩" and A2: "β' ∈SL ⟨Q, β⟩" and A3: "⦉β'⦊ = α'"
    unfolding encLST_def
    by blast
  from A1 have "α' = τ-Target"
    unfolding getTargetLabel_def
    by simp
  with ref A3 have "β' = τ-Source"
    by simp
  with A2 show "β = τ-STLCal"
    unfolding getSourceLabel_def
    by simp
next
  assume A1: "¬⦇Q, β⦈↦⟨P, τ-STLCal⟩"
  from kind have "¬⦇P, τ-STLCal⦈↦⟨Q, β⟩"
    using kinds_of_encoded_label(1)[of P "τ-STLCal" Q β]
    by blast
  with rel A1 show "β = τ-STLCal"
    using related_labels_get_condition(1)[of P "τ-STLCal" Q β]
    by simp
qed

lemma encL_reflects_internal_implies_target_internal_to_internal_right:
  fixes P Q :: "('procS, 'procT) Proc"
    and α   :: "('labS, 'labT) Lab"
  assumes rel:  "⟨P, α⟩ ≡⦇⦈ ⟨Q, τ-STLCal⟩"
      and kind: "Q ∈ ProcT"
      and ref:  "encL_reflects_internal"
    shows "α = τ-STLCal"
proof (cases "⦇P, α⦈↦⟨Q, τ-STLCal⟩")
  assume "⦇P, α⦈↦⟨Q, τ-STLCal⟩"
  then obtain α' β' where A1: "α' ∈SL ⟨P, α⟩" and A2: "β' ∈TL ⟨Q, τ-STLCal⟩" and A3: "⦉α'⦊ = β'"
    unfolding encLST_def
    by blast
  from A2 have "β' = τ-Target"
    unfolding getTargetLabel_def
    by simp
  with ref A3 have "α' = τ-Source"
    by simp
  with A1 show "α = τ-STLCal"
    unfolding getSourceLabel_def
    by simp
next
  assume A1: "¬⦇P, α⦈↦⟨Q, τ-STLCal⟩"
  from kind have "¬⦇Q, τ-STLCal⦈↦⟨P, α⟩"
    using kinds_of_encoded_label(1)[of Q "τ-STLCal" P α]
    by blast
  with rel A1 show "α = τ-STLCal"
    using related_labels_get_condition(1)[of P α Q "τ-STLCal"]
    by simp
qed

text ‹If the encoding of labels respects the internal, then the related labels are either both the
      internal or none of them are internal.›

lemma encL_respects_internal_implies_iff_internal:
  fixes P Q :: "('procS, 'procT) Proc"
    and α β :: "('labS, 'labT) Lab"
  assumes "⟨P, α⟩ ≡⦇⦈ ⟨Q, β⟩"
      and "encL_respects_internal"
    shows "α = τ-STLCal ⟷ β = τ-STLCal"
  using assms
  unfolding encLST_def related_labels_def getSourceLabel_def getTargetLabel_def
  by fastforce

end

end