Theory OperationalCorrespondence

theory OperationalCorrespondence
  imports SourceTargetRelation
begin

section ‹Operational Correspondence›

text ‹We consider different variants of operational correspondence. This criterion consists of a
        completeness and a soundness condition and is often defined with respect to a relation TRel
        on target terms. Operational completeness modulo TRel ensures that an encoding preserves
        source term behaviour modulo TRel by requiring that each sequence of source term steps can
        be mimicked by its translation such that the respective derivatives are related by TRel.›

abbreviation (in encoding) operational_complete :: "('procT × 'procT) set ⇒ bool" where
  "operational_complete TRel ≡
   ∀S S'. S ⟼Source* S' ⟶ (∃T. ⟦S⟧ ⟼Target* T ∧ (⟦S'⟧, T) ∈ TRel)"

text ‹We call an encoding strongly operational complete modulo TRel if each source term step has
        to be mimicked by single target term step of its translation.›

abbreviation (in encoding) strongly_operational_complete :: "('procT × 'procT) set ⇒ bool" where
  "strongly_operational_complete TRel ≡
   ∀S S'. S ⟼Source S' ⟶ (∃T. ⟦S⟧ ⟼Target T ∧ (⟦S'⟧, T) ∈ TRel)"

text ‹Operational soundness ensures that the encoding does not introduce new behaviour. An
        encoding is weakly operational sound modulo TRel if each sequence of target term steps is
        part of the translation of a sequence of source term steps such that the derivatives are
        related by TRel. It allows for intermediate states on the translation of source term step
        that are not the result of translating a source term.›

abbreviation (in encoding) weakly_operational_sound :: "('procT × 'procT) set ⇒ bool" where
  "weakly_operational_sound TRel ≡
   ∀S T. ⟦S⟧ ⟼Target* T ⟶ (∃S' T'. S ⟼Source* S' ∧ T ⟼Target* T' ∧ (⟦S'⟧, T') ∈ TRel)"

text ‹And encoding is operational sound modulo TRel if each sequence of target term steps is the
        translation of a sequence of source term steps such that the derivatives are related by
        TRel. This criterion does not allow for intermediate states, i.e., does not allow to a
        reach target term from an encoded source term that is not related by TRel to the
        translation of a source term.›

abbreviation (in encoding) operational_sound :: "('procT × 'procT) set ⇒ bool" where
  "operational_sound TRel ≡ ∀S T. ⟦S⟧ ⟼Target* T ⟶ (∃S'. S ⟼Source* S' ∧ (⟦S'⟧, T) ∈ TRel)"

text ‹Strong operational soundness modulo TRel is a stricter variant of operational soundness,
        where a single target term step has to be mapped on a single source term step.›

abbreviation (in encoding) strongly_operational_sound :: "('procT × 'procT) set ⇒ bool" where
  "strongly_operational_sound TRel ≡
   ∀S T. ⟦S⟧ ⟼Target T ⟶ (∃S'. S ⟼Source S' ∧ (⟦S'⟧, T) ∈ TRel)"

text ‹An encoding is weakly operational corresponding modulo TRel if it is operational complete
        and weakly operational sound modulo TRel.›

abbreviation (in encoding) weakly_operational_corresponding
    :: "('procT × 'procT) set ⇒ bool"
  where
  "weakly_operational_corresponding TRel ≡
   operational_complete TRel ∧ weakly_operational_sound TRel"

text ‹Operational correspondence modulo is the combination of operational completeness and
        operational soundness modulo TRel.›

abbreviation (in encoding) operational_corresponding :: "('procT × 'procT) set ⇒ bool" where
  "operational_corresponding TRel ≡ operational_complete TRel ∧ operational_sound TRel"

text ‹An encoding is strongly operational corresponding modulo TRel if it is strongly operational
        complete and strongly operational sound modulo TRel.›

abbreviation (in encoding) strongly_operational_corresponding
    :: "('procT × 'procT) set ⇒ bool"
  where
  "strongly_operational_corresponding TRel ≡
   strongly_operational_complete TRel ∧ strongly_operational_sound TRel"

subsection ‹Trivial Operational Correspondence Results›

text ‹Every encoding is (weakly) operational corresponding modulo the all relation on target
        terms.›

lemma (in encoding) operational_correspondence_modulo_all_relation:
  shows "operational_complete {(T1, T2). True}"
    and "weakly_operational_sound {(T1, T2). True}"
    and "operational_sound {(T1, T2). True}"
      using steps_refl[where Cal="Source"] steps_refl[where Cal="Target"]
    by blast+

lemma all_relation_is_weak_reduction_bisimulation:
  fixes Cal :: "'a processCalculus"
  shows "weak_reduction_bisimulation {(a, b). True} Cal"
      using steps_refl[where Cal="Cal"]
    by blast

lemma (in encoding) operational_correspondence_modulo_some_target_relation:
  shows "∃TRel. weakly_operational_corresponding TRel"
    and "∃TRel. operational_corresponding TRel"
    and "∃TRel. weakly_operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
    and "∃TRel. operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
      using operational_correspondence_modulo_all_relation
            all_relation_is_weak_reduction_bisimulation[where Cal="Target"]
    by blast+

text ‹Strong operational correspondence requires that source can perform a step iff their
        translations can perform a step.›

lemma (in encoding) strong_operational_correspondence_modulo_some_target_relation:
  shows "(∃TRel. strongly_operational_corresponding TRel)
         = (∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T))"
    and "(∃TRel. strongly_operational_corresponding TRel
          ∧ weak_reduction_bisimulation TRel Target)
         = (∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T))"
proof -
  have A1: "∃TRel. strongly_operational_corresponding TRel
            ⟹ ∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T)"
    by blast
  moreover have A2: "∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T)
                     ⟹ ∃TRel. strongly_operational_corresponding TRel
                          ∧ weak_reduction_bisimulation TRel Target"
  proof -
    assume "∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T)"
    hence "strongly_operational_corresponding {(T1, T2). True}"
      by simp
    thus "∃TRel. strongly_operational_corresponding TRel
          ∧ weak_reduction_bisimulation TRel Target"
        using all_relation_is_weak_reduction_bisimulation[where Cal="Target"]
      by blast
  qed
  ultimately show "(∃TRel. strongly_operational_corresponding TRel
                    ∧ weak_reduction_bisimulation TRel Target)
                   = (∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T))"
    by blast
  from A1 A2 show "(∃TRel. strongly_operational_corresponding TRel)
                   = (∀S. (∃S'. S ⟼Source S') ⟷ (∃T. ⟦S⟧ ⟼Target T))"
    by blast
qed

subsection ‹(Strong) Operational Completeness vs (Strong) Simulation›

text ‹An encoding is operational complete modulo a weak simulation on target terms TRel iff there
        is a relation, like indRelRTPO, that relates at least all source terms to their literal
        translations, includes TRel, and is a weak simulation.›

lemma (in encoding) weak_reduction_simulation_impl_OCom:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      and A2: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      and A3: "weak_reduction_simulation Rel (STCal Source Target)"
  shows "operational_complete (TRel⇧*)"
proof clarify
  fix S S'
  from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by simp
  moreover assume "S ⟼Source* S'"
  hence "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
    by (simp add: STCal_steps(1))
  ultimately obtain Q' where A5: "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q'"
                         and A6: "(SourceTerm S', Q') ∈ Rel"
      using A3
    by blast
  from A5 obtain T where A7: "T ∈T Q'" and A8: "⟦S⟧ ⟼Target* T"
    by (auto simp add: STCal_steps(2))
  from A2 A6 A7 have "(⟦S'⟧, T) ∈ TRel⇧*"
    by simp
  with A8 show "∃T. ⟦S⟧ ⟼Target* T ∧ (⟦S'⟧, T) ∈ TRel⇧*"
    by blast
qed

lemma (in encoding) OCom_iff_indRelRTPO_is_weak_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_complete (TRel⇧*)
         ∧ weak_reduction_simulation (TRel⇧+) Target)
         = weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume oc:  "operational_complete (TRel⇧*)"
     and sim: "weak_reduction_simulation (TRel⇧+) Target"
  show "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
  proof clarify
    fix P Q P'
    assume "P ≲⟦⋅⟧RT<TRel> Q" and "P ⟼(STCal Source Target)* P'"
    thus "∃Q'. Q ⟼(STCal Source Target)* Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
    proof (induct arbitrary: P')
      case (encR S)
      assume "SourceTerm S ⟼(STCal Source Target)* P'"
      from this obtain S' where A1: "S' ∈S P'" and A2: "S ⟼Source* S'"
        by (auto simp add: STCal_steps(1))
      from oc A2 obtain T where A3: "⟦S⟧ ⟼Target* T" and A4: "(⟦S'⟧, T) ∈ TRel⇧*"
        by blast
      from A3 have "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
        by (simp add: STCal_steps(2))
      moreover have "P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
      proof -
        from A4 have "⟦S'⟧ = T ∨ (⟦S'⟧, T) ∈ TRel⇧+"
            using rtrancl_eq_or_trancl[of "⟦S'⟧" T TRel]
          by blast
        moreover from A1 have A5: "P' ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelRTPO.encR)
        hence "⟦S'⟧ = T ⟹ P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
          by simp
        moreover have "(⟦S'⟧, T) ∈ TRel⇧+ ⟹ P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
        proof -
          assume "(⟦S'⟧, T) ∈ TRel⇧+"
          hence "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm T"
          proof induct
            fix T
            assume "(⟦S'⟧, T) ∈ TRel"
            thus "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm T"
              by (rule indRelRTPO.target)
          next
            case (step TQ TR)
            assume "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
            moreover assume "(TQ, TR) ∈ TRel"
            hence "TargetTerm TQ ≲⟦⋅⟧RT<TRel> TargetTerm TR"
              by (rule indRelRTPO.target)
            ultimately show "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm TR"
              by (rule indRelRTPO.trans)
          qed
          with A5 show "P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
            by (rule indRelRTPO.trans)
        qed
        ultimately show "P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
          by blast
      qed
      ultimately
      show "∃Q'. TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
    next
      case (source S)
      then obtain S' where B1: "S' ∈S P'"
        by (auto simp add: STCal_steps(1))
      hence "P' ≲⟦⋅⟧RT<TRel> P'"
        by (simp add: indRelRTPO.source)
      with source show "∃Q'. SourceTerm S ⟼(STCal Source Target)* Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T1 ⟼(STCal Source Target)* P'"
      from this obtain T1' where C1: "T1' ∈T P'" and C2: "T1 ⟼Target* T1'"
        by (auto simp add: STCal_steps(2))
      assume "(T1, T2) ∈ TRel"
      hence "(T1, T2) ∈ TRel⇧+"
        by simp
      with C2 sim obtain T2' where C3: "T2 ⟼Target* T2'"
                               and C4: "(T1', T2') ∈ TRel⇧+"
        by blast
      from C3 have "TargetTerm T2 ⟼(STCal Source Target)* (TargetTerm T2')"
        by (simp add: STCal_steps(2))
      moreover from C4 have "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
      proof induct
        fix T2'
        assume "(T1', T2') ∈ TRel"
        thus "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
          by (rule indRelRTPO.target)
      next
        case (step TQ TR)
        assume "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
        moreover assume "(TQ, TR) ∈ TRel"
        hence "TargetTerm TQ ≲⟦⋅⟧RT<TRel> TargetTerm TR"
          by (rule indRelRTPO.target)
        ultimately show "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm TR"
          by (rule indRelRTPO.trans)
      qed
      with C1 have "P' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
        by simp
      ultimately show "∃Q'. TargetTerm T2 ⟼(STCal Source Target)* Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
    next
      case (trans P Q R)
      assume "P ⟼(STCal Source Target)* P'"
         and "⋀P'. P ⟼(STCal Source Target)* P'
              ⟹ ∃Q'. Q ⟼(STCal Source Target)* Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
      from this obtain Q' where D1: "Q ⟼(STCal Source Target)* Q'"
                            and D2: "P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target)* Q'
              ⟹ ∃R'. R ⟼(STCal Source Target)* R' ∧ Q' ≲⟦⋅⟧RT<TRel> R'"
      with D1 obtain R' where D3: "R ⟼(STCal Source Target)* R'"
                          and D4: "Q' ≲⟦⋅⟧RT<TRel> R'"
        by blast
      from D2 D4 have "P' ≲⟦⋅⟧RT<TRel> R'"
        by (rule indRelRTPO.trans)
      with D3 show "∃R'. R ⟼(STCal Source Target)* R' ∧ P' ≲⟦⋅⟧RT<TRel> R'"
        by blast
    qed
  qed
next
  have "∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume sim: "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
  ultimately have "operational_complete (TRel⇧*)"
      using weak_reduction_simulation_impl_OCom[where Rel="indRelRTPO TRel" and TRel="TRel"]
    by simp
  moreover from sim have "weak_reduction_simulation (TRel⇧+) Target"
      using indRelRTPO_impl_TRel_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "operational_complete (TRel⇧*)
                   ∧ weak_reduction_simulation (TRel⇧+) Target"
    by simp
qed

lemma (in encoding) OCom_iff_weak_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_complete (TRel⇧*)
         ∧ weak_reduction_simulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ weak_reduction_simulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "operational_complete (TRel⇧*)"
              and "weak_reduction_simulation (TRel⇧+) Target"
  hence "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
      using OCom_iff_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ weak_reduction_simulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ weak_reduction_simulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    and A5: "weak_reduction_simulation Rel (STCal Source Target)"
    by blast
  from A1 A4 A5 have "operational_complete (TRel⇧*)"
      using weak_reduction_simulation_impl_OCom[where Rel="Rel" and TRel="TRel"]
    by simp
  moreover from A2 A3 A5 have "weak_reduction_simulation (TRel⇧+) Target"
      using rel_with_target_impl_transC_TRel_is_weak_reduction_simulation[where Rel="Rel" and
             TRel="TRel"]
    by simp
  ultimately show "operational_complete (TRel⇧*)
                   ∧ weak_reduction_simulation (TRel⇧+) Target"
    by simp
qed

text ‹An encoding is strong operational complete modulo a strong simulation on target terms TRel
        iff there is a relation, like indRelRTPO, that relates at least all source terms to their
        literal translations, includes TRel, and is a strong simulation.›

lemma (in encoding) strong_reduction_simulation_impl_SOCom:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      and A2: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      and A3: "strong_reduction_simulation Rel (STCal Source Target)"
  shows "strongly_operational_complete (TRel⇧*)"
proof clarify
  fix S S'
  from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by simp
  moreover assume "S ⟼Source S'"
  hence "SourceTerm S ⟼(STCal Source Target) (SourceTerm S')"
    by (simp add: STCal_step(1))
  ultimately obtain Q' where A5: "TargetTerm (⟦S⟧) ⟼(STCal Source Target) Q'"
                         and A6: "(SourceTerm S', Q') ∈ Rel"
      using A3
    by blast
  from A5 obtain T where A7: "T ∈T Q'" and A8: "⟦S⟧ ⟼Target T"
    by (auto simp add: STCal_step(2))
  from A2 A6 A7 have "(⟦S'⟧, T) ∈ TRel⇧*"
    by simp
  with A8 show "∃T. ⟦S⟧ ⟼Target T ∧ (⟦S'⟧, T) ∈ TRel⇧*"
    by blast
qed

lemma (in encoding) SOCom_iff_indRelRTPO_is_strong_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_complete (TRel⇧*)
         ∧ strong_reduction_simulation (TRel⇧+) Target)
         = strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume soc: "strongly_operational_complete (TRel⇧*)"
     and sim: "strong_reduction_simulation (TRel⇧+) Target"
  show "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
  proof clarify
    fix P Q P'
    assume "P ≲⟦⋅⟧RT<TRel> Q" and "P ⟼(STCal Source Target) P'"
    thus "∃Q'. Q ⟼(STCal Source Target) Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
    proof (induct arbitrary: P')
      case (encR S)
      assume "SourceTerm S ⟼(STCal Source Target) P'"
      from this obtain S' where A1: "S' ∈S P'" and A2: "S ⟼Source S'"
        by (auto simp add: STCal_step(1))
      from soc A2 obtain T where A3: "⟦S⟧ ⟼Target T" and A4: "(⟦S'⟧, T) ∈ TRel⇧*"
        by blast
      from A3 have "TargetTerm (⟦S⟧) ⟼(STCal Source Target) (TargetTerm T)"
        by (simp add: STCal_step(2))
      moreover have "P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
      proof -
        from A4 have "⟦S'⟧ = T ∨ (⟦S'⟧, T) ∈ TRel⇧+"
            using rtrancl_eq_or_trancl[of "⟦S'⟧" T TRel]
          by blast
        moreover from A1 have A5: "P' ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelRTPO.encR)
        hence "⟦S'⟧ = T ⟹ P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
          by simp
        moreover have "(⟦S'⟧, T) ∈ TRel⇧+ ⟹ P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
        proof -
          assume "(⟦S'⟧, T) ∈ TRel⇧+"
          hence "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm T"
          proof induct
            fix TQ
            assume "(⟦S'⟧, TQ) ∈ TRel"
            thus "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
              by (rule indRelRTPO.target)
          next
            case (step TQ TR)
            assume "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
            moreover assume "(TQ, TR) ∈ TRel"
            hence "TargetTerm TQ ≲⟦⋅⟧RT<TRel> TargetTerm TR"
              by (rule indRelRTPO.target)
            ultimately show "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm TR"
              by (rule indRelRTPO.trans)
          qed
          with A5 show "P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
            by (rule indRelRTPO.trans)
        qed
        ultimately show "P' ≲⟦⋅⟧RT<TRel> TargetTerm T"
          by blast
      qed
      ultimately
      show "∃Q'. TargetTerm (⟦S⟧) ⟼(STCal Source Target) Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
    next
      case (source S)
      then obtain S' where B1: "S' ∈S P'"
        by (auto simp add: STCal_step(1))
      hence "P' ≲⟦⋅⟧RT<TRel> P'"
        by (simp add: indRelRTPO.source)
      with source show "∃Q'. SourceTerm S ⟼(STCal Source Target) Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T1 ⟼(STCal Source Target) P'"
      from this obtain T1' where C1: "T1' ∈T P'" and C2: "T1 ⟼Target T1'"
        by (auto simp add: STCal_step(2))
      assume "(T1, T2) ∈ TRel"
      hence "(T1, T2) ∈ TRel⇧+"
        by simp
      with C2 sim obtain T2' where C3: "T2 ⟼Target T2'" and C4: "(T1', T2') ∈ TRel⇧+"
        by blast
      from C3 have "TargetTerm T2 ⟼(STCal Source Target) (TargetTerm T2')"
        by (simp add: STCal_step(2))
      moreover from C4 have "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
      proof induct
        fix T2'
        assume "(T1', T2') ∈ TRel"
        thus "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
          by (rule indRelRTPO.target)
      next
        case (step TQ TR)
        assume "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
        moreover assume "(TQ, TR) ∈ TRel"
        hence "TargetTerm TQ ≲⟦⋅⟧RT<TRel> TargetTerm TR"
          by (rule indRelRTPO.target)
        ultimately show "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm TR"
          by (rule indRelRTPO.trans)
      qed
      with C1 have "P' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
        by simp
      ultimately show "∃Q'. TargetTerm T2 ⟼(STCal Source Target) Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
    next
      case (trans P Q R)
      assume "P ⟼(STCal Source Target) P'"
         and "⋀P'. P ⟼(STCal Source Target) P'
              ⟹ ∃Q'. Q ⟼(STCal Source Target) Q' ∧ P' ≲⟦⋅⟧RT<TRel> Q'"
      from this obtain Q' where D1: "Q ⟼(STCal Source Target) Q'"
                            and D2: "P' ≲⟦⋅⟧RT<TRel> Q'"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target) Q'
              ⟹ ∃R'. R ⟼(STCal Source Target) R' ∧ Q' ≲⟦⋅⟧RT<TRel> R'"
      with D1 obtain R' where D3: "R ⟼(STCal Source Target) R'"
                          and D4: "Q' ≲⟦⋅⟧RT<TRel> R'"
        by blast
      from D2 D4 have "P' ≲⟦⋅⟧RT<TRel> R'"
        by (rule indRelRTPO.trans)
      with D3 show "∃R'. R ⟼(STCal Source Target) R' ∧ P' ≲⟦⋅⟧RT<TRel> R'"
        by blast
    qed
  qed
next
  have "∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume sim: "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
  ultimately have "strongly_operational_complete (TRel⇧*)"
      using strong_reduction_simulation_impl_SOCom[where Rel="indRelRTPO TRel" and TRel="TRel"]
    by simp
  moreover from sim have "strong_reduction_simulation (TRel⇧+) Target"
      using indRelRTPO_impl_TRel_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "strongly_operational_complete (TRel⇧*)
                   ∧ strong_reduction_simulation (TRel⇧+) Target"
    by simp
qed

lemma (in encoding) SOCom_iff_strong_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_complete (TRel⇧*)
         ∧ strong_reduction_simulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ strong_reduction_simulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "strongly_operational_complete (TRel⇧*)"
              and "strong_reduction_simulation (TRel⇧+) Target"
  hence "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
      using SOCom_iff_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ strong_reduction_simulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ strong_reduction_simulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    and A5: "strong_reduction_simulation Rel (STCal Source Target)"
    by blast
  from A1 A4 A5 have "strongly_operational_complete (TRel⇧*)"
      using strong_reduction_simulation_impl_SOCom[where Rel="Rel" and TRel="TRel"]
    by simp
  moreover from A2 A3 A5 have "strong_reduction_simulation (TRel⇧+) Target"
      using rel_with_target_impl_transC_TRel_is_strong_reduction_simulation[where Rel="Rel" and
             TRel="TRel"]
    by simp
  ultimately show "strongly_operational_complete (TRel⇧*)
                   ∧ strong_reduction_simulation (TRel⇧+) Target"
    by simp
qed

lemma (in encoding) target_relation_from_source_target_relation:
  fixes Rel :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
  assumes stre: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
                 ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧="
  shows "∃TRel. (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)"
proof -
  define TRel where "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
  from TRel_def have "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    by simp
  moreover from TRel_def
  have "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by blast
  moreover from stre TRel_def
  have "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    by blast
  ultimately show ?thesis
    by blast
qed

lemma (in encoding) SOCom_modulo_TRel_iff_strong_reduction_simulation:
  shows "(∃TRel. strongly_operational_complete (TRel⇧*)
         ∧ strong_reduction_simulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
           ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
           ∧ strong_reduction_simulation Rel (STCal Source Target))"
proof (rule iffI)
  assume "∃TRel. strongly_operational_complete (TRel⇧*)
          ∧ strong_reduction_simulation (TRel⇧+) Target"
  from this obtain TRel where "strongly_operational_complete (TRel⇧*)"
                          and "strong_reduction_simulation (TRel⇧+) Target"
    by blast
  hence "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
      using SOCom_iff_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  moreover have "∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T
                 ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ (indRelRTPO TRel)⇧="
      using indRelRTPO_relates_source_target[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
                      ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
                   ∧ strong_reduction_simulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
          ∧ strong_reduction_simulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
                         and A2: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
                                  ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)"
                         and A3: "strong_reduction_simulation Rel (STCal Source Target)"
    by blast
  from A2 obtain TRel where "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using target_relation_from_source_target_relation[where Rel="Rel"]
    by blast
  with A1 A3 have "strongly_operational_complete (TRel⇧*)
                   ∧ strong_reduction_simulation (TRel⇧+) Target"
      using SOCom_iff_strong_reduction_simulation[where TRel="TRel"]
    by blast
  thus "∃TRel. strongly_operational_complete (TRel⇧*)
        ∧ strong_reduction_simulation (TRel⇧+) Target"
    by blast
qed

subsection ‹Weak Operational Soundness vs Contrasimulation›

text ‹If the inverse of a relation that includes TRel and relates source terms and their literal
        translations is a contrasimulation, then the encoding is weakly operational sound.›

lemma (in encoding) weak_reduction_contrasimulation_impl_WOSou:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      and A2: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      and A3: "weak_reduction_contrasimulation (Rel¯) (STCal Source Target)"
  shows "weakly_operational_sound (TRel⇧*)"
proof clarify
  fix S T
  from A1 have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel¯"
    by simp
  moreover assume "⟦S⟧ ⟼Target* T"
  hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
    by (simp add: STCal_steps(2))
  ultimately obtain Q' where A5: "SourceTerm S ⟼(STCal Source Target)* Q'"
                         and A6: "(Q', TargetTerm T) ∈ Rel¯"
      using A3
    by blast
  from A5 obtain S' where A7: "S' ∈S Q'" and A8: "S ⟼Source* S'"
    by (auto simp add: STCal_steps(1))
  have "Q' ⟼(STCal Source Target)* Q'"
    by (simp add: steps_refl)
  with A6 A3 obtain P'' where A9:  "TargetTerm T ⟼(STCal Source Target)* P''"
                          and A10: "(P'', Q') ∈ Rel¯"
    by blast
  from A9 obtain T' where A11: "T' ∈T P''" and A12: "T ⟼Target* T'"
    by (auto simp add: STCal_steps(2))
  from A10 have "(Q', P'') ∈ Rel"
    by induct
  with A2 A7 A11 have "(⟦S'⟧, T') ∈ TRel⇧*"
    by simp
  with A8 A12 show "∃S' T'. S ⟼Source* S' ∧ T ⟼Target* T' ∧ (⟦S'⟧, T') ∈ TRel⇧*"
    by blast
qed

subsection ‹(Strong) Operational Soundness vs (Strong) Simulation›

text ‹An encoding is operational sound modulo a relation TRel whose inverse is a weak reduction
        simulation on target terms iff there is a relation, like indRelRTPO, that relates at least
        all source terms to their literal translations, includes TRel, and whose inverse is a weak
        simulation.›

lemma (in encoding) weak_reduction_simulation_impl_OSou:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      and A2: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      and A3: "weak_reduction_simulation (Rel¯) (STCal Source Target)"
  shows "operational_sound (TRel⇧*)"
proof clarify
  fix S T
  from A1 have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel¯"
    by simp
  moreover assume "⟦S⟧ ⟼Target* T"
  hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
    by (simp add: STCal_steps(2))
  ultimately obtain Q' where A5: "SourceTerm S ⟼(STCal Source Target)* Q'"
                         and A6: "(TargetTerm T, Q') ∈ Rel¯"
      using A3
    by blast
  from A5 obtain S' where A7: "S' ∈S Q'" and A8: "S ⟼Source* S'"
    by (auto simp add: STCal_steps(1))
  from A6 have "(Q', TargetTerm T) ∈ Rel"
    by induct
  with A2 A7 have "(⟦S'⟧, T) ∈ TRel⇧*"
    by simp
  with A8 show "∃S'. S ⟼Source* S' ∧ (⟦S'⟧, T) ∈ TRel⇧*"
    by blast
qed

lemma (in encoding) OSou_iff_inverse_of_indRelRTPO_is_weak_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_sound (TRel⇧*)
         ∧ weak_reduction_simulation ((TRel⇧+)¯) Target)
         = weak_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume os:  "operational_sound (TRel⇧*)"
     and sim: "weak_reduction_simulation ((TRel⇧+)¯) Target"
  show "weak_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
  proof clarify
    fix P Q P'
    assume "Q ≲⟦⋅⟧RT<TRel> P" and "P ⟼(STCal Source Target)* P'"
    thus "∃Q'. Q ⟼(STCal Source Target)* Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
    proof (induct arbitrary: P')
      case (encR S)
      assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* P'"
      from this obtain T where A1: "T ∈T P'" and A2: "⟦S⟧ ⟼Target* T"
        by (auto simp add: STCal_steps(2))
      from os A2 obtain S' where A3: "S ⟼Source* S'" and A4: "(⟦S'⟧, T) ∈ TRel⇧*"
        by blast
      from A3 have "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
        by (simp add: STCal_steps(1))
      moreover have "SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
      proof -
        from A4 have "⟦S'⟧ = T ∨ (⟦S'⟧, T) ∈ TRel⇧+"
            using rtrancl_eq_or_trancl[of "⟦S'⟧" T TRel]
          by blast
        moreover have A5: "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelRTPO.encR)
        with A1 have "⟦S'⟧ = T ⟹ SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
          by simp
        moreover have "(⟦S'⟧, T) ∈ TRel⇧+ ⟹ SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
        proof -
          assume "(⟦S'⟧, T) ∈ TRel⇧+"
          hence "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm T"
            by (rule transitive_closure_of_TRel_to_indRelRTPO)
          with A5 have "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T"
            by (rule indRelRTPO.trans)
          with A1 show "SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
            by simp
        qed
        ultimately show "SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
          by blast
      qed
      hence "(P', SourceTerm S') ∈ (indRelRTPO TRel)¯"
        by simp
      ultimately
      show "∃Q'. SourceTerm S ⟼(STCal Source Target)* Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
        by blast
    next
      case (source S)
      then obtain S' where B1: "S' ∈S P'"
        by (auto simp add: STCal_steps(1))
      hence "(P', P') ∈ (indRelRTPO TRel)¯"
        by (simp add: indRelRTPO.source)
      with source
      show "∃Q'. SourceTerm S ⟼(STCal Source Target)* Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T2 ⟼(STCal Source Target)* P'"
      from this obtain T2' where C1: "T2' ∈T P'" and C2: "T2 ⟼Target* T2'"
        by (auto simp add: STCal_steps(2))
      assume "(T1, T2) ∈ TRel"
      hence "(T2, T1) ∈ (TRel⇧+)¯"
        by simp
      with C2 sim obtain T1' where C3: "T1 ⟼Target* T1'" and C4: "(T2', T1') ∈ (TRel⇧+)¯"
        by blast
      from C3 have "TargetTerm T1 ⟼(STCal Source Target)* (TargetTerm T1')"
        by (simp add: STCal_steps(2))
      moreover from C4 have "(T1', T2') ∈ TRel⇧+"
        by induct
      hence "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
        by (rule transitive_closure_of_TRel_to_indRelRTPO)
      with C1 have "(P', TargetTerm T1') ∈ (indRelRTPO TRel)¯"
        by simp
      ultimately
      show "∃Q'. TargetTerm T1 ⟼(STCal Source Target)* Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
        by blast
    next
      case (trans P Q R R')
      assume "R ⟼(STCal Source Target)* R'"
         and "⋀R'. R ⟼(STCal Source Target)* R'
              ⟹ ∃Q'. Q ⟼(STCal Source Target)* Q' ∧ (R', Q') ∈ (indRelRTPO TRel)¯"
      from this obtain Q' where D1: "Q ⟼(STCal Source Target)* Q'"
                            and D2: "(R', Q') ∈ (indRelRTPO TRel)¯"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target)* Q'
              ⟹ ∃P'. P ⟼(STCal Source Target)* P' ∧ (Q', P') ∈ (indRelRTPO TRel)¯"
      with D1 obtain P' where D3: "P ⟼(STCal Source Target)* P'"
                          and D4: "(Q', P') ∈ (indRelRTPO TRel)¯"
        by blast
      from D4 D2 have "(R', P') ∈ (indRelRTPO TRel)¯"
        by (simp add: indRelRTPO.trans[where P="P'" and Q="Q'" and R="R'"])
      with D3 show "∃P'. P ⟼(STCal Source Target)* P' ∧ (R', P') ∈ (indRelRTPO TRel)¯"
        by blast
    qed
  qed
next
  have "∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover
  assume sim: "weak_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
  ultimately have "operational_sound (TRel⇧*)"
      using weak_reduction_simulation_impl_OSou[where Rel="indRelRTPO TRel" and TRel="TRel"]
    by simp
  moreover from sim have "weak_reduction_simulation ((TRel⇧+)¯) Target"
      using indRelRTPO_impl_TRel_is_weak_reduction_simulation_rev[where TRel="TRel"]
    by simp
  ultimately show "operational_sound (TRel⇧*) ∧ weak_reduction_simulation ((TRel⇧+)¯) Target"
    by simp
qed

lemma (in encoding) OSou_iff_weak_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_sound (TRel⇧*)
         ∧ weak_reduction_simulation ((TRel⇧+)¯) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ weak_reduction_simulation (Rel¯) (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "operational_sound (TRel⇧*)"
              and "weak_reduction_simulation ((TRel⇧+)¯) Target"
  hence "weak_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using OSou_iff_inverse_of_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ weak_reduction_simulation (Rel¯) (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ weak_reduction_simulation (Rel¯) (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    and A5: "weak_reduction_simulation (Rel¯) (STCal Source Target)"
    by blast
  from A1 A4 A5 have "operational_sound (TRel⇧*)"
      using weak_reduction_simulation_impl_OSou[where Rel="Rel" and TRel="TRel"]
    by simp
  moreover from A2 A3 A5 have "weak_reduction_simulation ((TRel⇧+)¯) Target"
      using rel_with_target_impl_transC_TRel_is_weak_reduction_simulation_rev[where Rel="Rel" and
             TRel="TRel"]
    by simp
  ultimately show "operational_sound (TRel⇧*) ∧ weak_reduction_simulation ((TRel⇧+)¯) Target"
    by simp
qed

text ‹An encoding is strongly operational sound modulo a relation TRel whose inverse is a strong
        reduction simulation on target terms iff there is a relation, like indRelRTPO, that relates
        at least all source terms to their literal translations, includes TRel, and whose inverse
        is a strong simulation.›

lemma (in encoding) strong_reduction_simulation_impl_SOSou:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      and A2: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      and A3: "strong_reduction_simulation (Rel¯) (STCal Source Target)"
  shows "strongly_operational_sound (TRel⇧*)"
proof clarify
  fix S T
  from A1 have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel¯"
    by simp
  moreover assume "⟦S⟧ ⟼Target T"
  hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target) (TargetTerm T)"
    by (simp add: STCal_step(2))
  ultimately obtain Q' where A5: "SourceTerm S ⟼(STCal Source Target) Q'"
                         and A6: "(TargetTerm T, Q') ∈ Rel¯"
      using A3
    by blast
  from A5 obtain S' where A7: "S' ∈S Q'" and A8: "S ⟼Source S'"
    by (auto simp add: STCal_step(1))
  from A6 have "(Q', TargetTerm T) ∈ Rel"
    by induct
  with A2 A7 have "(⟦S'⟧, T) ∈ TRel⇧*"
    by simp
  with A8 show "∃S'. S ⟼Source S' ∧ (⟦S'⟧, T) ∈ TRel⇧*"
    by blast
qed

lemma (in encoding) SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_sound (TRel⇧*)
         ∧ strong_reduction_simulation ((TRel⇧+)¯) Target)
         = strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume os:  "strongly_operational_sound (TRel⇧*)"
     and sim: "strong_reduction_simulation ((TRel⇧+)¯) Target"
  show "strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
  proof clarify
    fix P Q P'
    assume "Q ≲⟦⋅⟧RT<TRel> P"
    moreover assume "P ⟼(STCal Source Target) P'"
    ultimately
    show "∃Q'. Q ⟼(STCal Source Target) Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
    proof (induct arbitrary: P')
      case (encR S)
      assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target) P'"
      from this obtain T where A1: "T ∈T P'" and A2: "⟦S⟧ ⟼Target T"
        by (auto simp add: STCal_step(2))
      from os A2 obtain S' where A3: "S ⟼Source S'" and A4: "(⟦S'⟧, T) ∈ TRel⇧*"
        by blast
      from A3 have "SourceTerm S ⟼(STCal Source Target) (SourceTerm S')"
        by (simp add: STCal_step(1))
      moreover have "SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
      proof -
        from A4 have "⟦S'⟧ = T ∨ (⟦S'⟧, T) ∈ TRel⇧+"
            using rtrancl_eq_or_trancl[of "⟦S'⟧" T TRel]
          by blast
        moreover have A5: "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelRTPO.encR)
        with A1 have "⟦S'⟧ = T ⟹ SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
          by simp
        moreover have "(⟦S'⟧, T) ∈ TRel⇧+ ⟹ SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
        proof -
          assume "(⟦S'⟧, T) ∈ TRel⇧+"
          hence "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm T"
            by (rule transitive_closure_of_TRel_to_indRelRTPO)
          with A5 have "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T"
            by (rule indRelRTPO.trans)
          with A1 show "SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
            by simp
        qed
        ultimately show "SourceTerm S' ≲⟦⋅⟧RT<TRel> P'"
          by blast
      qed
      hence "(P', SourceTerm S') ∈ (indRelRTPO TRel)¯"
        by simp
      ultimately
      show "∃Q'. SourceTerm S ⟼(STCal Source Target) Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
        by blast
    next
      case (source S)
      then obtain S' where B1: "S' ∈S P'"
        by (auto simp add: STCal_step(1))
      hence "(P', P') ∈ (indRelRTPO TRel)¯"
        by (simp add: indRelRTPO.source)
      with source
      show "∃Q'. SourceTerm S ⟼(STCal Source Target) Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T2 ⟼(STCal Source Target) P'"
      from this obtain T2' where C1: "T2' ∈T P'" and C2: "T2 ⟼Target T2'"
        by (auto simp add: STCal_step(2))
      assume "(T1, T2) ∈ TRel"
      hence "(T2, T1) ∈ (TRel⇧+)¯"
        by simp
      with C2 sim obtain T1' where C3: "T1 ⟼Target T1'" and C4: "(T2', T1') ∈ (TRel⇧+)¯"
        by blast
      from C3 have "TargetTerm T1 ⟼(STCal Source Target) (TargetTerm T1')"
        by (simp add: STCal_step(2))
      moreover from C4 have "(T1', T2') ∈ TRel⇧+"
        by induct
      hence "TargetTerm T1' ≲⟦⋅⟧RT<TRel> TargetTerm T2'"
        by (rule transitive_closure_of_TRel_to_indRelRTPO)
      with C1 have "(P', TargetTerm T1') ∈ (indRelRTPO TRel)¯"
        by simp
      ultimately
      show "∃Q'. TargetTerm T1 ⟼(STCal Source Target) Q' ∧ (P', Q') ∈ (indRelRTPO TRel)¯"
        by blast
    next
      case (trans P Q R R')
      assume "R ⟼(STCal Source Target) R'"
         and "⋀R'. R ⟼(STCal Source Target) R'
              ⟹ ∃Q'. Q ⟼(STCal Source Target) Q' ∧ (R', Q') ∈ (indRelRTPO TRel)¯"
      from this obtain Q' where D1: "Q ⟼(STCal Source Target) Q'"
                            and D2: "(R', Q') ∈ (indRelRTPO TRel)¯"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target) Q'
              ⟹ ∃P'. P ⟼(STCal Source Target) P' ∧ (Q', P') ∈ (indRelRTPO TRel)¯"
      with D1 obtain P' where D3: "P ⟼(STCal Source Target) P'"
                          and D4: "(Q', P') ∈ (indRelRTPO TRel)¯"
        by blast
      from D4 D2 have "(R', P') ∈ (indRelRTPO TRel)¯"
        by (simp add: indRelRTPO.trans[where P="P'" and Q="Q'" and R="R'"])
      with D3 show "∃P'. P ⟼(STCal Source Target) P' ∧ (R', P') ∈ (indRelRTPO TRel)¯"
        by blast
    qed
  qed
next
  have "∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover
  assume sim: "strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
  ultimately have "strongly_operational_sound (TRel⇧*)"
      using strong_reduction_simulation_impl_SOSou[where Rel="indRelRTPO TRel" and TRel="TRel"]
    by simp
  moreover from sim have "strong_reduction_simulation ((TRel⇧+)¯) Target"
      using indRelRTPO_impl_TRel_is_strong_reduction_simulation_rev[where TRel="TRel"]
    by simp
  ultimately
  show "strongly_operational_sound (TRel⇧*) ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
    by simp
qed

lemma (in encoding) SOSou_iff_strong_reduction_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_sound (TRel⇧*) ∧ strong_reduction_simulation ((TRel⇧+)¯) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ strong_reduction_simulation (Rel¯) (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "strongly_operational_sound (TRel⇧*)"
              and "strong_reduction_simulation ((TRel⇧+)¯) Target"
  hence "strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ strong_reduction_simulation (Rel¯) (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ strong_reduction_simulation (Rel¯) (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    and A5: "strong_reduction_simulation (Rel¯) (STCal Source Target)"
    by blast
  from A1 A4 A5 have "strongly_operational_sound (TRel⇧*)"
      using strong_reduction_simulation_impl_SOSou[where Rel="Rel" and TRel="TRel"]
    by simp
  moreover from A2 A3 A5 have "strong_reduction_simulation ((TRel⇧+)¯) Target"
      using rel_with_target_impl_transC_TRel_is_strong_reduction_simulation_rev[where Rel="Rel" and
             TRel="TRel"]
    by simp
  ultimately
  show "strongly_operational_sound (TRel⇧*) ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
    by simp
qed

lemma (in encoding) SOSou_modulo_TRel_iff_strong_reduction_simulation:
  shows "(∃TRel. strongly_operational_sound (TRel⇧*)
         ∧ strong_reduction_simulation ((TRel⇧+)¯) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
           ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
           ∧ strong_reduction_simulation (Rel¯) (STCal Source Target))"
proof (rule iffI)
  assume "∃TRel. strongly_operational_sound (TRel⇧*)
          ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
  from this obtain TRel where "strongly_operational_sound (TRel⇧*)"
                          and "strong_reduction_simulation ((TRel⇧+)¯) Target"
    by blast
  hence "strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  moreover have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. (SourceTerm S, TargetTerm T) ∈ indRelRTPO TRel
                 ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ (indRelRTPO TRel)⇧="
      using indRelRTPO_relates_source_target[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
                      ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
                   ∧ strong_reduction_simulation (Rel¯) (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
             ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
          ∧ strong_reduction_simulation (Rel¯) (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and A2: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
            ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)"
   and A3: "strong_reduction_simulation (Rel¯) (STCal Source Target)"
    by blast
  from A2 obtain TRel where "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using target_relation_from_source_target_relation[where Rel="Rel"]
    by blast
  with A1 A3
  have "strongly_operational_sound (TRel⇧*) ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
      using SOSou_iff_strong_reduction_simulation[where TRel="TRel"]
    by blast
  thus "∃TRel. strongly_operational_sound (TRel⇧*) ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
    by blast
qed

subsection ‹Weak Operational Correspondence vs Correspondence Similarity›

text ‹If there exists a relation that relates at least all source terms and their literal
        translations, includes TRel, and is a correspondence simulation then the encoding is weakly
        operational corresponding w.r.t. TRel.›

lemma (in encoding) weak_reduction_correspondence_simulation_impl_WOC:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes enc:  "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      and tRel: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)"
      and cs:   "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
  shows "weakly_operational_corresponding (TRel⇧*)"
proof
  from enc tRel cs show "operational_complete (TRel⇧*)"
      using weak_reduction_simulation_impl_OCom[where TRel="TRel"]
    by simp
next
  show "weakly_operational_sound (TRel⇧*)"
  proof clarify
    fix S T
    from enc have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover assume "⟦S⟧ ⟼Target* T"
    hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
      by (simp add: STCal_steps(2))
    ultimately obtain P' Q' where A1: "SourceTerm S ⟼(STCal Source Target)* P'"
     and A2: "TargetTerm T ⟼(STCal Source Target)* Q'" and A3: "(P', Q') ∈ Rel"
        using cs
      by blast
    from A1 obtain S' where A4: "S' ∈S P'" and A5: "S ⟼Source* S'"
      by (auto simp add: STCal_steps(1))
    from A2 obtain T' where A6: "T' ∈T Q'" and A7: "T ⟼Target* T'"
      by (auto simp: STCal_steps(2))
    from tRel A3 A4 A6 have "(⟦S'⟧, T') ∈ TRel⇧*"
      by simp
    with A5 A7 show "∃S' T'. S ⟼Source* S' ∧ T ⟼Target* T' ∧ (⟦S'⟧, T') ∈ TRel⇧*"
      by blast
  qed
qed

text ‹An encoding is weakly operational corresponding w.r.t. a correspondence simulation on
        target terms TRel iff there exists a relation, like indRelRTPO, that relates at least all
        source terms and their literal translations, includes TRel, and is a correspondence
        simulation.›

lemma (in encoding) WOC_iff_indRelRTPO_is_reduction_correspondence_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(weakly_operational_corresponding (TRel⇧*)
         ∧ weak_reduction_correspondence_simulation (TRel⇧+) Target)
         = weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume woc: "weakly_operational_corresponding (TRel⇧*)"
     and csi: "weak_reduction_correspondence_simulation (TRel⇧+) Target"
  show "weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
  proof
    from woc csi show sim: "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
        using OCom_iff_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
      by simp
    show "∀P Q Q'. P ≲⟦⋅⟧RT<TRel> Q ∧ Q ⟼(STCal Source Target)* Q'
          ⟶ (∃P'' Q''. P ⟼(STCal Source Target)* P'' ∧ Q' ⟼(STCal Source Target)* Q''
          ∧ P'' ≲⟦⋅⟧RT<TRel> Q'')"
    proof clarify
      fix P Q Q'
      assume "P ≲⟦⋅⟧RT<TRel> Q" and "Q ⟼(STCal Source Target)* Q'"
      thus "∃P'' Q''. P ⟼(STCal Source Target)* P'' ∧ Q' ⟼(STCal Source Target)* Q''
            ∧ P'' ≲⟦⋅⟧RT<TRel> Q''"
      proof (induct arbitrary: Q')
        case (encR S)
        assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q'"
        from this obtain T where A1: "T ∈T Q'" and A2: "⟦S⟧ ⟼Target* T"
          by (auto simp add: STCal_steps(2))
        from A2 woc obtain S' T' where A3: "S ⟼Source* S'" and A4: "T ⟼Target* T'"
                                   and A5: "(⟦S'⟧, T') ∈ TRel⇧*"
          by blast
        from A3 have "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
          by (simp add: STCal_steps(1))
        moreover from A4 have "TargetTerm T ⟼(STCal Source Target)* (TargetTerm T')"
          by (simp add: STCal_steps(2))
        moreover have "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T'"
        proof -
          have A6: "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S'⟧)"
            by (rule indRelRTPO.encR)
          from A5 have "⟦S'⟧ = T' ∨ (⟦S'⟧, T') ∈ TRel⇧+"
              using rtrancl_eq_or_trancl[of "⟦S'⟧" T' TRel]
            by blast
          moreover from A6 have "⟦S'⟧ = T' ⟹ SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T'"
            by simp
          moreover have "(⟦S'⟧, T') ∈ TRel⇧+ ⟹ SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T'"
          proof -
            assume "(⟦S'⟧, T') ∈ TRel⇧+"
            hence "TargetTerm (⟦S'⟧) ≲⟦⋅⟧RT<TRel> TargetTerm T'"
              by (simp add: transitive_closure_of_TRel_to_indRelRTPO[where TRel="TRel"])
            with A6 show "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T'"
              by (rule indRelRTPO.trans)
          qed
          ultimately show "SourceTerm S' ≲⟦⋅⟧RT<TRel> TargetTerm T'"
            by blast
        qed
        ultimately show "∃P'' Q''. SourceTerm S ⟼(STCal Source Target)* P''
                         ∧ Q' ⟼(STCal Source Target)* Q'' ∧ P'' ≲⟦⋅⟧RT<TRel> Q''"
            using A1
          by blast
      next
        case (source S)
        assume B1: "SourceTerm S ⟼(STCal Source Target)* Q'"
        moreover have "Q' ⟼(STCal Source Target)* Q'"
          by (rule steps_refl)
        moreover from B1 obtain S' where "S' ∈S Q'"
          by (auto simp add: STCal_steps(1))
        hence "Q' ≲⟦⋅⟧RT<TRel> Q'"
          by (simp add: indRelRTPO.source)
        ultimately show "∃P'' Q''. SourceTerm S ⟼(STCal Source Target)* P''
                         ∧ Q' ⟼(STCal Source Target)* Q'' ∧ P'' ≲⟦⋅⟧RT<TRel> Q''"
          by blast
      next
        case (target T1 T2)
        assume "TargetTerm T2 ⟼(STCal Source Target)* Q'"
        from this obtain T2' where C1: "T2' ∈T Q'" and C2: "T2 ⟼Target* T2'"
          by (auto simp add: STCal_steps(2))
        assume "(T1, T2) ∈ TRel"
        hence "(T1, T2) ∈ TRel⇧+"
          by simp
        with C2 csi obtain T1' T2'' where C3: "T1 ⟼Target* T1'" and C4: "T2' ⟼Target* T2''"
                                      and C5: "(T1', T2'') ∈ TRel⇧+"
          by blast
        from C3 have "TargetTerm T1 ⟼(STCal Source Target)* (TargetTerm T1')"
          by (simp add: STCal_steps(2))
        moreover from C1 C4 have "Q' ⟼(STCal Source Target)* (TargetTerm T2'')"
          by (simp add: STCal_steps(2))
        moreover from C5 have "TargetTerm T1' ≲⟦⋅⟧RT<TRel> (TargetTerm T2'')"
          by (simp add: transitive_closure_of_TRel_to_indRelRTPO)
        ultimately show "∃P'' Q''. TargetTerm T1 ⟼(STCal Source Target)* P''
                         ∧ Q' ⟼(STCal Source Target)* Q'' ∧ P'' ≲⟦⋅⟧RT<TRel> Q''"
          by blast
      next
        case (trans P Q R R')
        assume "R ⟼(STCal Source Target)* R'"
           and "⋀R'. R ⟼(STCal Source Target)* R' ⟹ ∃Q'' R''. Q ⟼(STCal Source Target)* Q''
                ∧ R' ⟼(STCal Source Target)* R'' ∧ Q'' ≲⟦⋅⟧RT<TRel> R''"
           and "⋀Q'. Q ⟼(STCal Source Target)* Q' ⟹ ∃P'' Q''. P ⟼(STCal Source Target)* P''
                ∧ Q' ⟼(STCal Source Target)* Q'' ∧ P'' ≲⟦⋅⟧RT<TRel> Q''"
        moreover have "trans (indRelRTPO TRel)"
            using indRelRTPO.trans
            unfolding trans_def
          by blast
        ultimately show ?case
            using sim reduction_correspondence_simulation_condition_trans[where P="P" and
                   Rel="indRelRTPO TRel" and Cal="STCal Source Target" and Q="Q" and R="R"]
          by blast
      qed
    qed
  qed
next
  assume csi: "weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
  show "weakly_operational_corresponding (TRel⇧*)
        ∧ weak_reduction_correspondence_simulation (TRel⇧+) Target"
  proof
    have " ∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
      by (simp add: indRelRTPO.encR)
    moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
        using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
      by simp
    ultimately show "weakly_operational_corresponding (TRel⇧*)"
        using weak_reduction_correspondence_simulation_impl_WOC[where Rel="indRelRTPO TRel" and
               TRel="TRel"] csi
      by simp
  next
    from csi show "weak_reduction_correspondence_simulation (TRel⇧+) Target"
        using indRelRTPO_impl_TRel_is_weak_reduction_correspondence_simulation[where TRel="TRel"]
      by simp
  qed
qed

lemma (in encoding) WOC_iff_reduction_correspondence_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(weakly_operational_corresponding (TRel⇧*)
         ∧ weak_reduction_correspondence_simulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "weakly_operational_corresponding (TRel⇧*)"
              and "weak_reduction_correspondence_simulation (TRel⇧+) Target"
  hence "weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
      using WOC_iff_indRelRTPO_is_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
   and A5: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
    by blast
  from A1 A4 A5 have "weakly_operational_corresponding (TRel⇧*)"
      using weak_reduction_correspondence_simulation_impl_WOC[where Rel="Rel" and TRel="TRel"]
    by simp
  moreover from A2 A3 A5 have "weak_reduction_correspondence_simulation (TRel⇧+) Target"
      using rel_with_target_impl_transC_TRel_is_weak_reduction_correspondence_simulation
    by simp
  ultimately show "weakly_operational_corresponding (TRel⇧*)
                   ∧ weak_reduction_correspondence_simulation (TRel⇧+) Target"
    by simp
qed

lemma rel_includes_TRel_modulo_preorder:
  fixes Rel  :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set"
    and TRel :: "('procT × 'procT) set"
  assumes transT: "trans TRel"
  shows "((∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+))
         = (TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel})"
proof (rule iffI, erule conjE)
  assume "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
     and "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
  with transT show "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using trancl_id[of TRel]
    by blast
next
  assume A: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
  hence "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    by simp
  moreover from transT A
  have "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
      using trancl_id[of TRel]
    by blast
  ultimately show "(∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)"
    by simp
qed

lemma (in encoding) WOC_wrt_preorder_iff_reduction_correspondence_simulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(weakly_operational_corresponding TRel ∧ preorder TRel
         ∧ weak_reduction_correspondence_simulation TRel Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
            ∧ preorder Rel
            ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE, erule conjE, erule conjE)
  assume A1: "operational_complete TRel" and A2: "weakly_operational_sound TRel"
     and A3:"preorder TRel" and A4: "weak_reduction_correspondence_simulation TRel Target"
  from A3 have A5: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  with A3 have "TRel⇧* = TRel"
      using trancl_id[of TRel] reflcl_trancl[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  with A1 A2 have "weakly_operational_corresponding (TRel⇧*)"
    by simp
  moreover from A4 A5 have "weak_reduction_correspondence_simulation (TRel⇧+) Target"
    by simp
  ultimately
  have "weak_reduction_correspondence_simulation (indRelRTPO TRel) (STCal Source Target)"
      using WOC_iff_indRelRTPO_is_reduction_correspondence_simulation[where TRel="TRel"]
    by blast
  moreover have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover
  have "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ indRelRTPO TRel}"
  proof auto
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    thus "TargetTerm TP ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
      by (rule indRelRTPO.target)
  next
    fix TP TQ
    assume "TargetTerm TP ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
    with A3 show "(TP, TQ) ∈ TRel"
        using indRelRTPO_to_TRel(4)[where TRel="TRel"] trancl_id[of TRel]
        unfolding preorder_on_def
      by blast
  qed
  moreover from A3
  have "∀S T. (SourceTerm S, TargetTerm T) ∈ indRelRTPO TRel ⟶ (⟦S⟧, T) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] reflcl_trancl[of TRel]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      unfolding preorder_on_def refl_on_def
    by blast
  with A3 have "∀S T. (SourceTerm S, TargetTerm T) ∈ indRelRTPO TRel ⟶ (⟦S⟧, T) ∈ TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  moreover from A3 have "refl (indRelRTPO TRel)"
      using indRelRTPO_refl[of TRel]
      unfolding preorder_on_def
    by simp
  moreover have "trans (indRelRTPO TRel)"
      using indRelRTPO.trans
      unfolding trans_def
    by blast
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
                   ∧ preorder Rel
                   ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target)"
      unfolding preorder_on_def
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
          ∧ preorder Rel
          ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target)"
  from this obtain Rel where B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel" and B4: "preorder Rel"
   and B5: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
    by blast
  from B2 B4 have B6: "refl TRel"
      unfolding preorder_on_def refl_on_def
    by blast
  from B2 B4 have B7: "trans TRel"
      unfolding trans_def preorder_on_def
    by blast
  hence B8: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
    by simp
  with B6 have "TRel⇧* = TRel"
      using reflcl_trancl[of TRel]
      unfolding refl_on_def
    by blast
  with B1 B3 B5 have "weakly_operational_corresponding TRel"
      using weak_reduction_correspondence_simulation_impl_WOC[where Rel="Rel" and TRel="TRel"]
    by simp
  moreover from B6 B7 have "preorder TRel"
      unfolding preorder_on_def
    by blast
  moreover from B2 B5 B7 B8 have "weak_reduction_correspondence_simulation TRel Target"
      using rel_includes_TRel_modulo_preorder[where Rel="Rel" and TRel="TRel"]
            rel_with_target_impl_transC_TRel_is_weak_reduction_correspondence_simulation[where
               Rel="Rel" and TRel="TRel"]
      by fast
  ultimately show "weakly_operational_corresponding TRel ∧ preorder TRel
                   ∧ weak_reduction_correspondence_simulation TRel Target"
    by blast
qed

subsection ‹(Strong) Operational Correspondence vs (Strong) Bisimilarity›

text ‹An encoding is operational corresponding w.r.t a weak bisimulation on target terms TRel iff
        there exists a relation, like indRelRTPO, that relates at least all source terms and their
        literal translations, includes TRel, and is a weak bisimulation. Thus this variant of
        operational correspondence ensures that source terms and their translations are weak
        bisimilar.›

lemma (in encoding) OC_iff_indRelRTPO_is_weak_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_corresponding (TRel⇧*)
         ∧ weak_reduction_bisimulation (TRel⇧+) Target)
         = weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume ocorr: "operational_corresponding (TRel⇧*)"
     and bisim: "weak_reduction_bisimulation (TRel⇧+) Target"
  hence "weak_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
      using OCom_iff_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  moreover from bisim have "weak_reduction_simulation ((TRel⇧+)¯) Target"
      using weak_reduction_bisimulations_impl_inverse_is_simulation[where Rel="TRel⇧+"]
    by simp
  with ocorr have "weak_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using OSou_iff_inverse_of_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using weak_reduction_simulations_impl_bisimulation[where Rel="indRelRTPO TRel"]
    by simp
next
  assume bisim: "weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
  hence "operational_complete (TRel⇧*) ∧ weak_reduction_simulation (TRel⇧+) Target"
      using OCom_iff_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  moreover from bisim
  have "weak_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using weak_reduction_bisimulations_impl_inverse_is_simulation[where Rel="indRelRTPO TRel"]
    by simp
  hence "operational_sound (TRel⇧*) ∧ weak_reduction_simulation ((TRel⇧+)¯) Target"
      using OSou_iff_inverse_of_indRelRTPO_is_weak_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "operational_corresponding (TRel⇧*) ∧ weak_reduction_bisimulation (TRel⇧+) Target"
      using weak_reduction_simulations_impl_bisimulation[where Rel="TRel⇧+"]
    by simp
qed

lemma (in encoding) OC_iff_weak_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_corresponding (TRel⇧*) ∧ weak_reduction_bisimulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ weak_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "operational_corresponding (TRel⇧*)"
              and "weak_reduction_bisimulation (TRel⇧+) Target"
  hence "weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
   and A5: "weak_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  hence "operational_complete (TRel⇧*)
         ∧ weak_reduction_simulation (TRel⇧+) Target"
      using OCom_iff_weak_reduction_simulation[where TRel="TRel"]
    by blast
  moreover from A5 have "weak_reduction_simulation (Rel¯) (STCal Source Target)"
      using weak_reduction_bisimulations_impl_inverse_is_simulation[where Rel="Rel"]
    by simp
  with A1 A2 A3 A4 have "operational_sound (TRel⇧*)
                         ∧ weak_reduction_simulation ((TRel⇧+)¯) Target"
      using OSou_iff_weak_reduction_simulation[where TRel="TRel"]
    by blast
  ultimately show "operational_corresponding (TRel⇧*)
                   ∧ weak_reduction_bisimulation (TRel⇧+) Target"
      using weak_reduction_simulations_impl_bisimulation[where Rel="TRel⇧+"]
    by simp
qed

lemma (in encoding) OC_wrt_preorder_iff_weak_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(operational_corresponding TRel ∧ preorder TRel
         ∧ weak_reduction_bisimulation TRel Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
            ∧ preorder Rel
            ∧ weak_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE, erule conjE, erule conjE)
  assume A1: "operational_complete TRel" and A2: "operational_sound TRel"
     and A3:"preorder TRel" and A4: "weak_reduction_bisimulation TRel Target"
  from A3 have A5: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  with A3 have "TRel⇧* = TRel"
      using reflcl_trancl[of TRel]
      unfolding preorder_on_def refl_on_def
    by blast
  with A1 A2 have "operational_corresponding (TRel⇧*)"
    by simp
  moreover from A4 A5 have "weak_reduction_bisimulation (TRel⇧+) Target"
    by simp
  ultimately
  have "weak_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by blast
  moreover have "∀S. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm (⟦S⟧)"
    by (simp add: indRelRTPO.encR)
  moreover
  have "TRel = {(T1, T2). TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2}"
  proof auto
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    thus "TargetTerm TP ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
      by (rule indRelRTPO.target)
  next
    fix TP TQ
    assume "TargetTerm TP ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
    with A3 show "(TP, TQ) ∈ TRel"
        using indRelRTPO_to_TRel(4)[where TRel="TRel"] trancl_id[of TRel]
        unfolding preorder_on_def
      by blast
  qed
  moreover from A3
  have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] reflcl_trancl[of TRel]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      unfolding preorder_on_def refl_on_def
    by auto
  with A3 have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  moreover from A3 have "refl (indRelRTPO TRel)"
      unfolding preorder_on_def
    by (simp add: indRelRTPO_refl)
  moreover have "trans (indRelRTPO TRel)"
      using indRelRTPO.trans
      unfolding trans_def
    by blast
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
                   ∧ preorder Rel
                   ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
      unfolding preorder_on_def
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
          ∧ preorder Rel
          ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel" and B4: "preorder Rel"
   and B5: "weak_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  from B2 B4 have B6: "refl TRel"
      unfolding preorder_on_def refl_on_def
    by blast
  from B2 B4 have B7: "trans TRel"
      unfolding trans_def preorder_on_def
    by blast
  hence B8: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
    by simp
  with B6 have B9: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel]
      unfolding refl_on_def
    by blast
  with B3 have "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    by simp
  moreover from B2 B8 have "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by auto
  ultimately have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
   ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
      using B1 B5
    by blast
  hence "operational_corresponding (TRel⇧*)
         ∧ weak_reduction_bisimulation (TRel⇧+) Target"
      using OC_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  with B8 B9 have "operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
    by simp
  moreover from B6 B7 have "preorder TRel"
      unfolding preorder_on_def
    by blast
  ultimately show "operational_corresponding TRel ∧ preorder TRel
                   ∧ weak_reduction_bisimulation TRel Target"
    by blast
qed

lemma (in encoding) OC_wrt_equivalence_iff_indRelTEQ_weak_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  assumes eqT: "equivalence TRel"
  shows "(operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target) ⟷
         weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume oc: "operational_corresponding TRel" and bisimT: "weak_reduction_bisimulation TRel Target"
  show "weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
  proof auto
    fix P Q P'
    assume "P ∼⟦⋅⟧T<TRel> Q" and "P ⟼(STCal Source Target)* P'"
    thus "∃Q'. Q ⟼(STCal Source Target)* Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
    proof (induct arbitrary: P')
      case (encR S)
      assume "SourceTerm S ⟼(STCal Source Target)* P'"
      from this obtain S' where A1: "S ⟼Source* S'" and A2: "S' ∈S P'"
        by (auto simp add: STCal_steps(1))
      from A1 oc obtain T where A3: "⟦S⟧ ⟼Target* T" and A4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from A3 have "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
        by (simp add: STCal_steps(2))
      moreover have "P' ∼⟦⋅⟧T<TRel> TargetTerm T"
      proof -
        from A2 have "P' ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelTEQ.encR)
        moreover from A4 have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> TargetTerm T"
          by (rule indRelTEQ.target)
        ultimately show "P' ∼⟦⋅⟧T<TRel> TargetTerm T"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃Q'. TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (encL S)
      assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* P'"
      from this obtain T where B1: "⟦S⟧ ⟼Target* T" and B2: "T ∈T P'"
        by (auto simp add: STCal_steps(2))
      from B1 oc obtain S' where B3: "S ⟼Source* S'" and B4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from B3 have "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
        by (simp add: STCal_steps(1))
      moreover have "P' ∼⟦⋅⟧T<TRel> SourceTerm S'"
      proof -
        from B4 eqT have "(T, ⟦S'⟧) ∈ TRel"
            unfolding equiv_def sym_def
          by blast
        with B2 have "P' ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelTEQ.target)
        moreover have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> SourceTerm S'"
          by (rule indRelTEQ.encL)
        ultimately show "P' ∼⟦⋅⟧T<TRel> SourceTerm S'"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃Q'. SourceTerm S ⟼(STCal Source Target)* Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T1 ⟼(STCal Source Target)* P'"
      from this obtain T1' where C1: "T1 ⟼Target* T1'" and C2: "T1' ∈T P'"
        by (auto simp add: STCal_steps(2))
      assume "(T1, T2) ∈ TRel"
      with C1 bisimT obtain T2' where C3: "T2 ⟼Target* T2'" and C4: "(T1', T2') ∈ TRel"
        by blast
      from C3 have "TargetTerm T2 ⟼(STCal Source Target)* (TargetTerm T2')"
        by (simp add: STCal_steps(2))
      moreover from C2 C4 have "P' ∼⟦⋅⟧T<TRel> TargetTerm T2'"
        by (simp add: indRelTEQ.target)
      ultimately show "∃Q'. TargetTerm T2 ⟼(STCal Source Target)* Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (trans P Q R)
      assume "P ⟼(STCal Source Target)* P'"
         and "⋀P'. P ⟼(STCal Source Target)* P'
              ⟹ ∃Q'. Q ⟼(STCal Source Target)* Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
      from this obtain Q' where D1: "Q ⟼(STCal Source Target)* Q'" and D2: "P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target)* Q'
              ⟹ ∃R'. R ⟼(STCal Source Target)* R' ∧ Q' ∼⟦⋅⟧T<TRel> R'"
      with D1 obtain R' where D3: "R ⟼(STCal Source Target)* R'" and D4: "Q' ∼⟦⋅⟧T<TRel> R'"
        by blast
      from D2 D4 have "P' ∼⟦⋅⟧T<TRel> R'"
        by (rule indRelTEQ.trans)
      with D3 show "∃R'. R ⟼(STCal Source Target)* R' ∧ P' ∼⟦⋅⟧T<TRel> R'"
        by blast
    qed
  next
    fix P Q Q'
    assume "P ∼⟦⋅⟧T<TRel> Q" and "Q ⟼(STCal Source Target)* Q'"
    thus "∃P'. P ⟼(STCal Source Target)* P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
    proof (induct arbitrary: Q')
      case (encR S)
      assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q'"
      from this obtain T where E1: "⟦S⟧ ⟼Target* T" and E2: "T ∈T Q'"
        by (auto simp add: STCal_steps(2))
      from E1 oc obtain S' where E3: "S ⟼Source* S'" and E4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from E3 have "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
        by (simp add: STCal_steps(1))
      moreover have "SourceTerm S' ∼⟦⋅⟧T<TRel> Q'"
      proof -
        have "SourceTerm S' ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (rule indRelTEQ.encR)
        moreover from E2 E4 have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> Q'"
          by (simp add: indRelTEQ.target)
        ultimately show "SourceTerm S' ∼⟦⋅⟧T<TRel> Q'"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃P'. SourceTerm S ⟼(STCal Source Target)* P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (encL S)
      assume "SourceTerm S ⟼(STCal Source Target)* Q'"
      from this obtain S' where F1: "S ⟼Source* S'" and F2: "S' ∈S Q'"
        by (auto simp add: STCal_steps(1))
      from F1 oc obtain T where F3: "⟦S⟧ ⟼Target* T" and F4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from F3 have "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
        by (simp add: STCal_steps(2))
      moreover have "TargetTerm T ∼⟦⋅⟧T<TRel> Q'"
      proof -
        from F4 eqT have "(T, ⟦S'⟧) ∈ TRel"
            unfolding equiv_def sym_def
          by blast
        hence "TargetTerm T ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (rule indRelTEQ.target)
        moreover from F2 have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> Q'"
          by (simp add: indRelTEQ.encL)
        ultimately show "TargetTerm T ∼⟦⋅⟧T<TRel> Q'"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃P'. TargetTerm (⟦S⟧) ⟼(STCal Source Target)* P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T2 ⟼(STCal Source Target)* Q'"
      from this obtain T2' where G1: "T2 ⟼Target* T2'" and G2: "T2' ∈T Q'"
        by (auto simp add: STCal_steps(2))
      assume "(T1, T2) ∈ TRel"
      with G1 bisimT obtain T1' where G3: "T1 ⟼Target* T1'" and G4: "(T1', T2') ∈ TRel"
        by blast
      from G3 have "TargetTerm T1 ⟼(STCal Source Target)* (TargetTerm T1')"
        by (simp add: STCal_steps(2))
      moreover from G2 G4 have "TargetTerm T1' ∼⟦⋅⟧T<TRel> Q'"
        by (simp add: indRelTEQ.target)
      ultimately show "∃P'. TargetTerm T1 ⟼(STCal Source Target)* P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (trans P Q R R')
      assume "R ⟼(STCal Source Target)* R'"
         and "⋀R'. R ⟼(STCal Source Target)* R'
              ⟹ ∃Q'. Q ⟼(STCal Source Target)* Q' ∧ Q' ∼⟦⋅⟧T<TRel> R'"
      from this obtain Q' where H1: "Q ⟼(STCal Source Target)* Q'" and H2: "Q' ∼⟦⋅⟧T<TRel> R'"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target)* Q'
              ⟹ ∃P'. P ⟼(STCal Source Target)* P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
      with H1 obtain P' where H3: "P ⟼(STCal Source Target)* P'" and H4: "P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
      from H4 H2 have "P' ∼⟦⋅⟧T<TRel> R'"
        by (rule indRelTEQ.trans)
      with H3 show "∃P'. P ⟼(STCal Source Target)* P' ∧ P' ∼⟦⋅⟧T<TRel> R'"
        by blast
    qed
  qed
next
  assume bisim: "weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
  have "operational_corresponding TRel"
  proof auto
    fix S S'
    have "SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧)"
      by (rule indRelTEQ.encR)
    moreover assume "S ⟼Source* S'"
    hence "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
      by (simp add: STCal_steps(1))
    ultimately obtain Q' where I1: "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q'"
                           and I2: "SourceTerm S' ∼⟦⋅⟧T<TRel> Q'"
        using bisim
      by blast
    from I1 obtain T where I3: "⟦S⟧ ⟼Target* T" and I4: "T ∈T Q'"
      by (auto simp add: STCal_steps(2))
    from eqT have "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    with I2 I4 have "(⟦S'⟧, T) ∈ TRel"
        using indRelTEQ_to_TRel(2)[where TRel="TRel"]
              trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      by simp
    with I3 show "∃T. ⟦S⟧ ⟼Target* T ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  next
    fix S T
    have "SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧)"
      by (rule indRelTEQ.encR)
    moreover assume "⟦S⟧ ⟼Target* T"
    hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
      by (simp add: STCal_steps(2))
    ultimately obtain Q' where J1: "SourceTerm S ⟼(STCal Source Target)* Q'"
                           and J2: "Q' ∼⟦⋅⟧T<TRel> TargetTerm T"
        using bisim
      by blast
    from J1 obtain S' where J3: "S ⟼Source* S'" and J4: "S' ∈S Q'"
      by (auto simp add: STCal_steps(1))
    from eqT have "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    with J2 J4 have "(⟦S'⟧, T) ∈ TRel"
        using indRelTEQ_to_TRel(2)[where TRel="TRel"]
              trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      by blast
    with J3 show "∃S'. S ⟼Source* S' ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  qed
  moreover have "weak_reduction_bisimulation TRel Target"
  proof -
    from eqT have "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    with bisim show "weak_reduction_bisimulation TRel Target"
        using indRelTEQ_impl_TRel_is_weak_reduction_bisimulation[where TRel="TRel"]
      by simp
  qed
  ultimately show "operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
    by simp
qed

lemma (in encoding) OC_wrt_equivalence_iff_weak_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  assumes eqT: "equivalence TRel"
  shows "(operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target) ⟷ (∃Rel.
         (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
         ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
         ∧ trans Rel ∧ weak_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  assume oc: "operational_corresponding TRel" and bisimT: "weak_reduction_bisimulation TRel Target"
  from eqT have rt: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding equiv_def refl_on_def
    by auto
  have "∀S. SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧) ∧ TargetTerm (⟦S⟧) ∼⟦⋅⟧T<TRel> SourceTerm S"
    by (simp add: indRelTEQ.encR indRelTEQ.encL)
  moreover from rt have "TRel = {(T1, T2). TargetTerm T1 ∼⟦⋅⟧T<TRel> TargetTerm T2}"
      using indRelTEQ_to_TRel(4)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by (auto simp add: indRelTEQ.target)
  moreover have "trans (indRelTEQ TRel)"
      using indRelTEQ.trans[where TRel="TRel"]
      unfolding trans_def
    by blast
  moreover from eqT oc bisimT
  have "weak_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
      using OC_wrt_equivalence_iff_indRelTEQ_weak_reduction_bisimulation[where TRel="TRel"]
    by blast
  ultimately
  show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
        ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel} ∧ trans Rel
        ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
                 ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
          ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel} ∧ trans Rel
          ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
                                  ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
   and A2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}" and A3: "trans Rel"
   and A4: "weak_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  have "operational_corresponding TRel"
  proof auto
    fix S S'
    from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover assume "S ⟼Source* S'"
    hence "SourceTerm S ⟼(STCal Source Target)* (SourceTerm S')"
      by (simp add: STCal_steps(1))
    ultimately obtain Q' where B1: "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* Q'"
                           and B2: "(SourceTerm S', Q') ∈ Rel"
        using A4
      by blast
    from B1 obtain T where B3: "⟦S⟧ ⟼Target* T" and B4: "T ∈T Q'"
      by (auto simp add: STCal_steps(2))
    from A1 have "(TargetTerm (⟦S'⟧), SourceTerm S') ∈ Rel"
      by simp
    with B2 A3 have "(TargetTerm (⟦S'⟧), Q') ∈ Rel"
        unfolding trans_def
      by blast
    with B4 A2 have "(⟦S'⟧, T) ∈ TRel"
      by simp
    with B3 show "∃T. ⟦S⟧ ⟼Target* T ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  next
    fix S T
    from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover assume "⟦S⟧ ⟼Target* T"
    hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target)* (TargetTerm T)"
      by (simp add: STCal_steps(2))
    ultimately obtain P' where C1: "SourceTerm S ⟼(STCal Source Target)* P'"
                           and C2: "(P', TargetTerm T) ∈ Rel"
        using A4
      by blast
    from C1 obtain S' where C3: "S ⟼Source* S'" and C4: "S' ∈S P'"
      by (auto simp add: STCal_steps(1))
    from A1 C4 have "(TargetTerm (⟦S'⟧), P') ∈ Rel"
      by simp
    from A3 this C2 have "(TargetTerm (⟦S'⟧), TargetTerm T) ∈ Rel"
        unfolding trans_def
      by blast
    with A2 have "(⟦S'⟧, T) ∈ TRel"
      by simp
    with C3 show "∃S'. S ⟼Source* S' ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  qed
  moreover have "weak_reduction_bisimulation TRel Target"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with A2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼Target* TP'"
    hence "TargetTerm TP ⟼(STCal Source Target)* (TargetTerm TP')"
      by (simp add: STCal_steps(2))
    ultimately obtain Q' where D1: "TargetTerm TQ ⟼(STCal Source Target)* Q'"
                           and D2: "(TargetTerm TP', Q') ∈ Rel"
        using A4
      by blast
    from D1 obtain TQ' where D3: "TQ ⟼Target* TQ'" and D4: "TQ' ∈T Q'"
      by (auto simp add: STCal_steps(2))
    from A2 D2 D4 have "(TP', TQ') ∈ TRel"
      by simp
    with D3 show "∃TQ'. TQ ⟼Target* TQ' ∧ (TP', TQ') ∈ TRel"
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with A2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼Target* TQ'"
    hence "TargetTerm TQ ⟼(STCal Source Target)* (TargetTerm TQ')"
      by (simp add: STCal_steps(2))
    ultimately obtain P' where E1: "TargetTerm TP ⟼(STCal Source Target)* P'"
                           and E2: "(P', TargetTerm TQ') ∈ Rel"
        using A4
      by blast
    from E1 obtain TP' where E3: "TP ⟼Target* TP'" and E4: "TP' ∈T P'"
      by (auto simp add: STCal_steps(2))
    from A2 E2 E4 have "(TP', TQ') ∈ TRel"
      by simp
    with E3 show "∃TP'. TP ⟼Target* TP' ∧ (TP', TQ') ∈ TRel"
      by blast
  qed
  ultimately show "operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
    by simp
qed

text ‹An encoding is strong operational corresponding w.r.t a strong bisimulation on target terms
        TRel iff there exists a relation, like indRelRTPO, that relates at least all source terms
        and their literal translations, includes TRel, and is a strong bisimulation. Thus this
        variant of operational correspondence ensures that source terms and their translations are
        strong bisimilar.›

lemma (in encoding) SOC_iff_indRelRTPO_is_strong_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_corresponding (TRel⇧*)
         ∧ strong_reduction_bisimulation (TRel⇧+) Target)
         = strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume ocorr: "strongly_operational_corresponding (TRel⇧*)"
     and bisim: "strong_reduction_bisimulation (TRel⇧+) Target"
  hence "strong_reduction_simulation (indRelRTPO TRel) (STCal Source Target)"
      using SOCom_iff_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  moreover from bisim have "strong_reduction_simulation ((TRel⇧+)¯) Target"
      using strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="TRel⇧+"]
    by simp
  with ocorr
  have "strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using strong_reduction_simulations_impl_bisimulation[where Rel="indRelRTPO TRel"]
    by simp
next
  assume bisim: "strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
  hence "strongly_operational_complete (TRel⇧*) ∧ strong_reduction_simulation (TRel⇧+) Target"
      using SOCom_iff_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  moreover from bisim
  have "strong_reduction_simulation ((indRelRTPO TRel)¯) (STCal Source Target)"
      using strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="indRelRTPO TRel"]
    by simp
  hence "strongly_operational_sound (TRel⇧*) ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
      using SOSou_iff_inverse_of_indRelRTPO_is_strong_reduction_simulation[where TRel="TRel"]
    by simp
  ultimately show "strongly_operational_corresponding (TRel⇧*)
                   ∧ strong_reduction_bisimulation (TRel⇧+) Target"
      using strong_reduction_simulations_impl_bisimulation[where Rel="TRel⇧+"]
    by simp
qed

lemma (in encoding) SOC_iff_strong_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_corresponding (TRel⇧*)
         ∧ strong_reduction_bisimulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
            ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
            ∧ strong_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀T1 T2. (T1, T2) ∈ TRel ⟶ TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2"
    by (simp add: indRelRTPO.target)
  moreover have "∀T1 T2. TargetTerm T1 ≲⟦⋅⟧RT<TRel> TargetTerm T2 ⟶ (T1, T2) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by simp
  moreover have "∀S T. SourceTerm S ≲⟦⋅⟧RT<TRel> TargetTerm T ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] trans_closure_of_TRel_refl_cond
    by simp
  moreover assume "strongly_operational_corresponding (TRel⇧*)"
              and "strong_reduction_bisimulation (TRel⇧+) Target"
  hence "strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using SOC_iff_indRelRTPO_is_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
          ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
          ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and A2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and A3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and A4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
   and A5: "strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  hence "strongly_operational_complete (TRel⇧*)
         ∧ strong_reduction_simulation (TRel⇧+) Target"
      using SOCom_iff_strong_reduction_simulation[where TRel="TRel"]
    by blast
  moreover from A5 have "strong_reduction_simulation (Rel¯) (STCal Source Target)"
      using strong_reduction_bisimulations_impl_inverse_is_simulation[where Rel="Rel"]
    by simp
  with A1 A2 A3 A4 have "strongly_operational_sound (TRel⇧*)
                         ∧ strong_reduction_simulation ((TRel⇧+)¯) Target"
      using SOSou_iff_strong_reduction_simulation[where TRel="TRel"]
    by blast
  ultimately show "strongly_operational_corresponding (TRel⇧*)
                   ∧ strong_reduction_bisimulation (TRel⇧+) Target"
      using strong_reduction_simulations_impl_bisimulation[where Rel="TRel⇧+"]
    by simp
qed

lemma (in encoding) SOC_wrt_preorder_iff_strong_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  shows "(strongly_operational_corresponding TRel ∧ preorder TRel
         ∧ strong_reduction_bisimulation TRel Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
            ∧ preorder Rel
            ∧ strong_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE, erule conjE, erule conjE)
  assume A1: "strongly_operational_complete TRel" and A2: "strongly_operational_sound TRel"
     and A3:"preorder TRel" and A4: "strong_reduction_bisimulation TRel Target"
  from A3 have A5: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  with A3 have "TRel⇧* = TRel"
      using reflcl_trancl[of TRel]
      unfolding preorder_on_def refl_on_def
    by blast
  with A1 A2 have "strongly_operational_corresponding (TRel⇧*)"
    by simp
  moreover from A4 A5 have "strong_reduction_bisimulation (TRel⇧+) Target"
    by simp
  ultimately
  have "strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using SOC_iff_indRelRTPO_is_strong_reduction_bisimulation[where TRel="TRel"]
    by blast
  moreover have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover
  have "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ indRelRTPO TRel}"
  proof auto
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    thus "TargetTerm TP ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
      by (rule indRelRTPO.target)
  next
    fix TP TQ
    assume "TargetTerm TP ≲⟦⋅⟧RT<TRel> TargetTerm TQ"
    with A3 show "(TP, TQ) ∈ TRel"
        using indRelRTPO_to_TRel(4)[where TRel="TRel"] trancl_id[of TRel]
        unfolding preorder_on_def
      by blast
  qed
  moreover from A3
  have "∀S T. (SourceTerm S, TargetTerm T) ∈ indRelRTPO TRel ⟶ (⟦S⟧, T) ∈ TRel⇧+"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"] reflcl_trancl[of TRel]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      unfolding preorder_on_def refl_on_def
    by blast
  with A3 have "∀S T. (SourceTerm S, TargetTerm T) ∈ indRelRTPO TRel ⟶ (⟦S⟧, T) ∈ TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  moreover from A3 have "refl (indRelRTPO TRel)"
      unfolding preorder_on_def
    by (simp add: indRelRTPO_refl)
  moreover have "trans (indRelRTPO TRel)"
      using indRelRTPO.trans
      unfolding trans_def
    by blast
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
                   ∧ preorder Rel
                   ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
      unfolding preorder_on_def
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
          ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
          ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)
          ∧ preorder Rel
          ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel" and B4: "preorder Rel"
   and B5: "strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  from B2 B4 have B6: "refl TRel"
      unfolding preorder_on_def refl_on_def
    by blast
  from B2 B4 have B7: "trans TRel"
      unfolding trans_def preorder_on_def
    by blast
  hence B8: "TRel⇧+ = TRel"
    by (rule trancl_id)
  with B6 have B9: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel]
      unfolding refl_on_def
    by blast
  with B3 have "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    by simp
  moreover from B2 B8 have "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by auto
  ultimately have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
   ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
      using B1 B5
    by blast
  hence "strongly_operational_corresponding (TRel⇧*) ∧ strong_reduction_bisimulation (TRel⇧+) Target"
      using SOC_iff_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  with B8 B9
  have "strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target"
    by simp
  moreover from B6 B7 have "preorder TRel"
      unfolding preorder_on_def
    by blast
  ultimately show "strongly_operational_corresponding TRel ∧ preorder TRel
                   ∧ strong_reduction_bisimulation TRel Target"
    by blast
qed

lemma (in encoding) SOC_wrt_TRel_iff_strong_reduction_bisimulation:
  shows "(∃TRel. strongly_operational_corresponding (TRel⇧*)
         ∧ strong_reduction_bisimulation (TRel⇧+) Target)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
               ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
            ∧ strong_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI)
  assume "∃TRel. strongly_operational_corresponding (TRel⇧*)
          ∧ strong_reduction_bisimulation (TRel⇧+) Target"
  from this obtain TRel where "strongly_operational_corresponding (TRel⇧*)"
                          and "strong_reduction_bisimulation (TRel⇧+) Target"
    by blast
  hence "strong_reduction_bisimulation (indRelRTPO TRel) (STCal Source Target)"
      using SOC_iff_indRelRTPO_is_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelRTPO TRel"
    by (simp add: indRelRTPO.encR)
  moreover have "∀S T. (SourceTerm S, TargetTerm T) ∈ (indRelRTPO TRel)
                 ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ (indRelRTPO TRel)⇧="
      using indRelRTPO_relates_source_target[where TRel="TRel"]
    by simp
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
   ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧=)
   ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
                         and A2: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel
                                  ⟶ (TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel⇧="
                         and A3: "strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  from A2 obtain TRel where "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using target_relation_from_source_target_relation[where Rel="Rel"]
    by blast
  with A1 A3 have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel)
                   ∧ (∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+)
                   ∧ (∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*)
                   ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  hence "strongly_operational_corresponding (TRel⇧*)
         ∧ strong_reduction_bisimulation (TRel⇧+) Target"
      using SOC_iff_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  thus "∃TRel. strongly_operational_corresponding (TRel⇧*)
        ∧ strong_reduction_bisimulation (TRel⇧+) Target"
    by blast
qed

lemma (in encoding) SOC_wrt_equivalence_iff_indRelTEQ_strong_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  assumes eqT: "equivalence TRel"
  shows "(strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target)
         ⟷ strong_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
proof (rule iffI, erule conjE)
  assume oc:     "strongly_operational_corresponding TRel"
     and bisimT: "strong_reduction_bisimulation TRel Target"
  show "strong_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
  proof auto
    fix P Q P'
    assume "P ∼⟦⋅⟧T<TRel> Q" and "P ⟼(STCal Source Target) P'"
    thus "∃Q'. Q ⟼(STCal Source Target) Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
    proof (induct arbitrary: P')
      case (encR S)
      assume "SourceTerm S ⟼(STCal Source Target) P'"
      from this obtain S' where A1: "S ⟼Source S'" and A2: "S' ∈S P'"
        by (auto simp add: STCal_step(1))
      from A1 oc obtain T where A3: "⟦S⟧ ⟼Target T" and A4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from A3 have "TargetTerm (⟦S⟧) ⟼(STCal Source Target) (TargetTerm T)"
        by (simp add: STCal_step(2))
      moreover have "P' ∼⟦⋅⟧T<TRel> TargetTerm T"
      proof -
        from A2 have "P' ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelTEQ.encR)
        moreover from A4 have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> TargetTerm T"
          by (rule indRelTEQ.target)
        ultimately show "P' ∼⟦⋅⟧T<TRel> TargetTerm T"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃Q'. TargetTerm (⟦S⟧) ⟼(STCal Source Target) Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (encL S)
      assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target) P'"
      from this obtain T where B1: "⟦S⟧ ⟼Target T" and B2: "T ∈T P'"
        by (auto simp add: STCal_step(2))
      from B1 oc obtain S' where B3: "S ⟼Source S'" and B4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from B3 have "SourceTerm S ⟼(STCal Source Target) (SourceTerm S')"
        by (simp add: STCal_step(1))
      moreover have "P' ∼⟦⋅⟧T<TRel> SourceTerm S'"
      proof -
        from B4 eqT have "(T, ⟦S'⟧) ∈ TRel"
            unfolding equiv_def sym_def
          by blast
        with B2 have "P' ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (simp add: indRelTEQ.target)
        moreover have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> SourceTerm S'"
          by (rule indRelTEQ.encL)
        ultimately show "P' ∼⟦⋅⟧T<TRel> SourceTerm S'"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃Q'. SourceTerm S ⟼(STCal Source Target) Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T1 ⟼(STCal Source Target) P'"
      from this obtain T1' where C1: "T1 ⟼Target T1'" and C2: "T1' ∈T P'"
        by (auto simp add: STCal_step(2))
      assume "(T1, T2) ∈ TRel"
      with C1 bisimT obtain T2' where C3: "T2 ⟼Target T2'" and C4: "(T1', T2') ∈ TRel"
        by blast
      from C3 have "TargetTerm T2 ⟼(STCal Source Target) (TargetTerm T2')"
        by (simp add: STCal_step(2))
      moreover from C2 C4 have "P' ∼⟦⋅⟧T<TRel> TargetTerm T2'"
        by (simp add: indRelTEQ.target)
      ultimately show "∃Q'. TargetTerm T2 ⟼(STCal Source Target) Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (trans P Q R)
      assume "P ⟼(STCal Source Target) P'"
         and "⋀P'. P ⟼(STCal Source Target) P'
              ⟹ ∃Q'. Q ⟼(STCal Source Target) Q' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
      from this obtain Q' where D1: "Q ⟼(STCal Source Target) Q'" and D2: "P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target) Q'
              ⟹ ∃R'. R ⟼(STCal Source Target) R' ∧ Q' ∼⟦⋅⟧T<TRel> R'"
      with D1 obtain R' where D3: "R ⟼(STCal Source Target) R'" and D4: "Q' ∼⟦⋅⟧T<TRel> R'"
        by blast
      from D2 D4 have "P' ∼⟦⋅⟧T<TRel> R'"
        by (rule indRelTEQ.trans)
      with D3 show "∃R'. R ⟼(STCal Source Target) R' ∧ P' ∼⟦⋅⟧T<TRel> R'"
        by blast
    qed
  next
    fix P Q Q'
    assume "P ∼⟦⋅⟧T<TRel> Q" and "Q ⟼(STCal Source Target) Q'"
    thus "∃P'. P ⟼(STCal Source Target) P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
    proof (induct arbitrary: Q')
      case (encR S)
      assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target) Q'"
      from this obtain T where E1: "⟦S⟧ ⟼Target T" and E2: "T ∈T Q'"
        by (auto simp add: STCal_step(2))
      from E1 oc obtain S' where E3: "S ⟼Source S'" and E4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from E3 have "SourceTerm S ⟼(STCal Source Target) (SourceTerm S')"
        by (simp add: STCal_step(1))
      moreover have "SourceTerm S' ∼⟦⋅⟧T<TRel> Q'"
      proof -
        have "SourceTerm S' ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (rule indRelTEQ.encR)
        moreover from E2 E4 have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> Q'"
          by (simp add: indRelTEQ.target)
        ultimately show "SourceTerm S' ∼⟦⋅⟧T<TRel> Q'"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃P'. SourceTerm S ⟼(STCal Source Target) P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (encL S)
      assume "SourceTerm S ⟼(STCal Source Target) Q'"
      from this obtain S' where F1: "S ⟼Source S'" and F2: "S' ∈S Q'"
        by (auto simp add: STCal_step(1))
      from F1 oc obtain T where F3: "⟦S⟧ ⟼Target T" and F4: "(⟦S'⟧, T) ∈ TRel"
        by blast
      from F3 have "TargetTerm (⟦S⟧) ⟼(STCal Source Target) (TargetTerm T)"
        by (simp add: STCal_step(2))
      moreover have "TargetTerm T ∼⟦⋅⟧T<TRel> Q'"
      proof -
        from F4 eqT have "(T, ⟦S'⟧) ∈ TRel"
            unfolding equiv_def sym_def
          by blast
        hence "TargetTerm T ∼⟦⋅⟧T<TRel> TargetTerm (⟦S'⟧)"
          by (rule indRelTEQ.target)
        moreover from F2 have "TargetTerm (⟦S'⟧) ∼⟦⋅⟧T<TRel> Q'"
          by (simp add: indRelTEQ.encL)
        ultimately show "TargetTerm T ∼⟦⋅⟧T<TRel> Q'"
          by (rule indRelTEQ.trans)
      qed
      ultimately show "∃P'. TargetTerm (⟦S⟧) ⟼(STCal Source Target) P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (target T1 T2)
      assume "TargetTerm T2 ⟼(STCal Source Target) Q'"
      from this obtain T2' where G1: "T2 ⟼Target T2'" and G2: "T2' ∈T Q'"
        by (auto simp add: STCal_step(2))
      assume "(T1, T2) ∈ TRel"
      with G1 bisimT obtain T1' where G3: "T1 ⟼Target T1'" and G4: "(T1', T2') ∈ TRel"
        by blast
      from G3 have "TargetTerm T1 ⟼(STCal Source Target) (TargetTerm T1')"
        by (simp add: STCal_step(2))
      moreover from G2 G4 have "TargetTerm T1' ∼⟦⋅⟧T<TRel> Q'"
        by (simp add: indRelTEQ.target)
      ultimately show "∃P'. TargetTerm T1 ⟼(STCal Source Target) P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
    next
      case (trans P Q R R')
      assume "R ⟼(STCal Source Target) R'"
         and "⋀R'. R ⟼(STCal Source Target) R'
              ⟹ ∃Q'. Q ⟼(STCal Source Target) Q' ∧ Q' ∼⟦⋅⟧T<TRel> R'"
      from this obtain Q' where H1: "Q ⟼(STCal Source Target) Q'" and H2: "Q' ∼⟦⋅⟧T<TRel> R'"
        by blast
      assume "⋀Q'. Q ⟼(STCal Source Target) Q'
              ⟹ ∃P'. P ⟼(STCal Source Target) P' ∧ P' ∼⟦⋅⟧T<TRel> Q'"
      with H1 obtain P' where H3: "P ⟼(STCal Source Target) P'" and H4: "P' ∼⟦⋅⟧T<TRel> Q'"
        by blast
      from H4 H2 have "P' ∼⟦⋅⟧T<TRel> R'"
        by (rule indRelTEQ.trans)
      with H3 show "∃P'. P ⟼(STCal Source Target) P' ∧ P' ∼⟦⋅⟧T<TRel> R'"
        by blast
    qed
  qed
next
  assume bisim: "strong_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
  have "strongly_operational_corresponding TRel"
  proof auto
    fix S S'
    have "SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧)"
      by (rule indRelTEQ.encR)
    moreover assume "S ⟼Source S'"
    hence "SourceTerm S ⟼(STCal Source Target) (SourceTerm S')"
      by (simp add: STCal_step(1))
    ultimately obtain Q' where I1: "TargetTerm (⟦S⟧) ⟼(STCal Source Target) Q'"
                           and I2: "SourceTerm S' ∼⟦⋅⟧T<TRel> Q'"
        using bisim
      by blast
    from I1 obtain T where I3: "⟦S⟧ ⟼Target T" and I4: "T ∈T Q'"
      by (auto simp add: STCal_step(2))
    from eqT have "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    with I2 I4 have "(⟦S'⟧, T) ∈ TRel"
        using indRelTEQ_to_TRel(2)[where TRel="TRel"]
              trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      by simp
    with I3 show "∃T. ⟦S⟧ ⟼Target T ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  next
    fix S T
    have "SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧)"
      by (rule indRelTEQ.encR)
    moreover assume "⟦S⟧ ⟼Target T"
    hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target) (TargetTerm T)"
      by (simp add: STCal_step(2))
    ultimately obtain Q' where J1: "SourceTerm S ⟼(STCal Source Target) Q'"
                           and J2: "Q' ∼⟦⋅⟧T<TRel> TargetTerm T"
        using bisim
      by blast
    from J1 obtain S' where J3: "S ⟼Source S'" and J4: "S' ∈S Q'"
      by (auto simp add: STCal_step(1))
    from eqT have "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    with J2 J4 have "(⟦S'⟧, T) ∈ TRel"
        using indRelTEQ_to_TRel(2)[where TRel="TRel"]
              trans_closure_of_TRel_refl_cond[where TRel="TRel"]
      by blast
    with J3 show "∃S'. S ⟼Source S' ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  qed
  moreover have "strong_reduction_bisimulation TRel Target"
  proof -
    from eqT have "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    with bisim show "strong_reduction_bisimulation TRel Target"
        using indRelTEQ_impl_TRel_is_strong_reduction_bisimulation[where TRel="TRel"]
      by simp
  qed
  ultimately
  show "strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target"
    by simp
qed

lemma (in encoding) SOC_wrt_equivalence_iff_strong_reduction_bisimulation:
  fixes TRel :: "('procT × 'procT) set"
  assumes eqT: "equivalence TRel"
  shows "(strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target)
         ⟷ (∃Rel.
         (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
         ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
         ∧ trans Rel ∧ strong_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE)
  assume oc:     "strongly_operational_corresponding TRel"
     and bisimT: "strong_reduction_bisimulation TRel Target"
  from eqT have rt: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding equiv_def refl_on_def
    by auto
  have "∀S. SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧) ∧ TargetTerm (⟦S⟧) ∼⟦⋅⟧T<TRel> SourceTerm S"
    by (simp add: indRelTEQ.encR indRelTEQ.encL)
  moreover from rt have "TRel = {(T1, T2). TargetTerm T1 ∼⟦⋅⟧T<TRel> TargetTerm T2}"
      using indRelTEQ_to_TRel(4)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by (auto simp add: indRelTEQ.target)
  moreover have "trans (indRelTEQ TRel)"
      using indRelTEQ.trans[where TRel="TRel"]
      unfolding trans_def
    by blast
  moreover from eqT oc bisimT
  have "strong_reduction_bisimulation (indRelTEQ TRel) (STCal Source Target)"
      using SOC_wrt_equivalence_iff_indRelTEQ_strong_reduction_bisimulation[where TRel="TRel"]
    by blast
  ultimately
  show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
        ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel} ∧ trans Rel
        ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
                 ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
          ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel} ∧ trans Rel
          ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel
                                  ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
   and A2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}" and A3: "trans Rel"
   and A4: "strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  have "strongly_operational_corresponding TRel"
  proof auto
    fix S S'
    from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover assume "S ⟼Source S'"
    hence "SourceTerm S ⟼(STCal Source Target) (SourceTerm S')"
      by (simp add: STCal_step(1))
    ultimately obtain Q' where B1: "TargetTerm (⟦S⟧) ⟼(STCal Source Target) Q'"
                           and B2: "(SourceTerm S', Q') ∈ Rel"
        using A4
      by blast
    from B1 obtain T where B3: "⟦S⟧ ⟼Target T" and B4: "T ∈T Q'"
      by (auto simp add: STCal_step(2))
    from A1 have "(TargetTerm (⟦S'⟧), SourceTerm S') ∈ Rel"
      by simp
    with B2 A3 have "(TargetTerm (⟦S'⟧), Q') ∈ Rel"
        unfolding trans_def
      by blast
    with B4 A2 have "(⟦S'⟧, T) ∈ TRel"
      by simp
    with B3 show "∃T. ⟦S⟧ ⟼Target T ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  next
    fix S T
    from A1 have "(SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover assume "⟦S⟧ ⟼Target T"
    hence "TargetTerm (⟦S⟧) ⟼(STCal Source Target) (TargetTerm T)"
      by (simp add: STCal_step(2))
    ultimately obtain P' where C1: "SourceTerm S ⟼(STCal Source Target) P'"
                           and C2: "(P', TargetTerm T) ∈ Rel"
        using A4
      by blast
    from C1 obtain S' where C3: "S ⟼Source S'" and C4: "S' ∈S P'"
      by (auto simp add: STCal_step(1))
    from A1 C4 have "(TargetTerm (⟦S'⟧), P') ∈ Rel"
      by simp
    from A3 this C2 have "(TargetTerm (⟦S'⟧), TargetTerm T) ∈ Rel"
        unfolding trans_def
      by blast
    with A2 have "(⟦S'⟧, T) ∈ TRel"
      by simp
    with C3 show "∃S'. S ⟼Source S' ∧ (⟦S'⟧, T) ∈ TRel"
      by blast
  qed
  moreover have "strong_reduction_bisimulation TRel Target"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with A2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼Target TP'"
    hence "TargetTerm TP ⟼(STCal Source Target) (TargetTerm TP')"
      by (simp add: STCal_step(2))
    ultimately obtain Q' where D1: "TargetTerm TQ ⟼(STCal Source Target) Q'"
                           and D2: "(TargetTerm TP', Q') ∈ Rel"
        using A4
      by blast
    from D1 obtain TQ' where D3: "TQ ⟼Target TQ'" and D4: "TQ' ∈T Q'"
      by (auto simp add: STCal_step(2))
    from A2 D2 D4 have "(TP', TQ') ∈ TRel"
      by simp
    with D3 show "∃TQ'. TQ ⟼Target TQ' ∧ (TP', TQ') ∈ TRel"
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with A2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼Target TQ'"
    hence "TargetTerm TQ ⟼(STCal Source Target) (TargetTerm TQ')"
      by (simp add: STCal_step(2))
    ultimately obtain P' where E1: "TargetTerm TP ⟼(STCal Source Target) P'"
                           and E2: "(P', TargetTerm TQ') ∈ Rel"
        using A4
      by blast
    from E1 obtain TP' where E3: "TP ⟼Target TP'" and E4: "TP' ∈T P'"
      by (auto simp add: STCal_step(2))
    from A2 E2 E4 have "(TP', TQ') ∈ TRel"
      by simp
    with E3 show "∃TP'. TP ⟼Target TP' ∧ (TP', TQ') ∈ TRel"
      by blast
  qed
  ultimately
  show "strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target"
    by simp
qed

end