Theory CombinedCriteria

theory CombinedCriteria
  imports DivergenceReflection SuccessSensitiveness FullAbstraction OperationalCorrespondence
begin

section ‹Combining Criteria›

text ‹So far we considered the effect of single criteria on encodings. Often the quality of an
        encoding is prescribed by a set of different criteria. In the following we analyse the
        combined effect of criteria. This way we can compare criteria as well as identify side
        effects that result from combinations of criteria. We start with some technical lemmata. To
        combine the effect of different criteria we combine the conditions they induce. If their
        effect can be described by a predicate on the pairs of the relation, as in the case of
        success sensitiveness or divergence reflection, combining the effects is simple.›

lemma (in encoding) criterion_iff_source_target_relation_impl_indRelR:
  fixes Cond :: "('procS ⇒ 'procT) ⇒ bool"
    and Pred :: "(('procS, 'procT) Proc × ('procS, 'procT) Proc) set ⇒ bool"
  assumes "Cond enc = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ Pred Rel)"
  shows "Cond enc = (∃Rel'. Pred (indRelR ∪ Rel'))"
proof (rule iffI)
  assume "Cond enc"
  with assms obtain Rel where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel" and A2: "Pred Rel"
    by blast
  from A1 have "Rel = indRelR ∪ (Rel - indRelR)"
    by (auto simp add: indRelR.simps)
  with A2 have "Pred (indRelR ∪ (Rel - indRelR))"
    by simp
  thus "∃Rel'. Pred (indRelR ∪ Rel')"
    by blast
next
  assume "∃Rel'. Pred (indRelR ∪ Rel')"
  from this obtain Rel' where "Pred (indRelR ∪ Rel')"
    by blast
  moreover have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ (indRelR ∪ Rel')"
    by (simp add: indRelR.encR)
  ultimately show "Cond enc"
      using assms
    by blast
qed

lemma (in encoding) combine_conditions_on_pairs_of_relations:
  fixes RelA RelB   :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set"
    and CondA CondB :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) ⇒ bool"
  assumes "∀(P, Q) ∈ RelA. CondA (P, Q)"
      and "∀(P, Q) ∈ RelB. CondB (P, Q)"
  shows "(∀(P, Q) ∈ RelA ∩ RelB. CondA (P, Q)) ∧ (∀(P, Q) ∈ RelA ∩ RelB. CondB (P, Q))"
      using assms
    by blast

lemma (in encoding) combine_conditions_on_sets_of_relations:
  fixes Rel RelA :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set"
    and Cond     :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set ⇒ bool"
    and CondA    :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) ⇒ bool"
  assumes "∀(P, Q) ∈ RelA. CondA (P, Q)"
      and "Cond Rel ∧ Rel ⊆ RelA"
  shows "Cond Rel ∧ (∀(P, Q) ∈ Rel. CondA (P, Q))"
      using assms
    by blast

lemma (in encoding) combine_conditions_on_sets_and_pairs_of_relations:
  fixes Rel RelA RelB :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set"
    and Cond          :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set ⇒ bool"
    and CondA CondB   :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) ⇒ bool"
  assumes "∀(P, Q) ∈ RelA. CondA (P, Q)"
      and "∀(P, Q) ∈ RelB. CondB (P, Q)"
      and "Cond Rel ∧ Rel ⊆ RelA ∧ Rel ⊆ RelB"
  shows "Cond Rel ∧ (∀(P, Q) ∈ Rel. CondA (P, Q)) ∧ (∀(P, Q) ∈ Rel. CondB (P, Q))"
      using assms
    by blast

text ‹We mapped several criteria on conditions on relations that relate at least all source terms
        and their literal translations. The following lemmata help us to combine such conditions by
        switching to the witness indRelR.›

lemma (in encoding) combine_conditions_on_relations_indRelR:
  fixes RelA RelB   :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set"
    and Cond        :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) set ⇒ bool"
    and CondA CondB :: "(('procS, 'procT) Proc ×('procS, 'procT) Proc) ⇒ bool"
  assumes A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ RelA"
      and A2: "∀(P, Q) ∈ RelA. CondA (P, Q)"
      and A3: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ RelB"
      and A4: "∀(P, Q) ∈ RelB. CondB (P, Q)"
  shows "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ (∀(P, Q) ∈ Rel. CondA (P, Q))
          ∧ (∀(P, Q) ∈ Rel. CondB (P, Q))"
    and "Cond indRelR ⟹ (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
         ∧ (∀(P, Q) ∈ Rel. CondA (P, Q)) ∧ (∀(P, Q) ∈ Rel. CondB (P, Q)) ∧ Cond Rel)"
proof -
  have A5: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ indRelR"
    by (simp add: indRelR.encR)
  moreover have A6: "indRelR ⊆ RelA"
  proof clarify
    fix P Q
    assume "(P, Q) ∈ indRelR"
    from this A1 show "(P, Q) ∈ RelA"
      by (induct, simp)
  qed
  moreover have A7: "indRelR ⊆ RelB"
  proof clarify
    fix P Q
    assume "(P, Q) ∈ indRelR"
    from this A3 show "(P, Q) ∈ RelB"
      by (induct, simp)
  qed
  ultimately show "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀(P, Q) ∈ Rel. CondA (P, Q)) ∧ (∀(P, Q) ∈ Rel. CondB (P, Q))"
      using combine_conditions_on_sets_and_pairs_of_relations[where RelA="RelA" and RelB="RelB"
            and CondA="CondA" and CondB="CondB" and Rel="indRelR"
            and Cond="λR. ∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ R"] A2 A4
    by blast
  from A2 A4 A5 A6 A7
  show "Cond indRelR ⟹ (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
        ∧ (∀(P, Q) ∈ Rel. CondA (P, Q)) ∧ (∀(P, Q) ∈ Rel. CondB (P, Q)) ∧ Cond Rel)"
      using combine_conditions_on_sets_and_pairs_of_relations[where RelA="RelA" and RelB="RelB"
            and CondA="CondA" and CondB="CondB" and Rel="indRelR"
            and Cond="λR. ∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ R ∧ Cond R"]
    by blast
qed

lemma (in encoding) indRelR_cond_respects_predA_and_reflects_predB:
  fixes PredA PredB :: "('procS, 'procT) Proc ⇒ bool"
  shows "((∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_respects_pred Rel PredA)
          ∧ (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_reflects_pred Rel PredB))
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_respects_pred Rel PredA
            ∧ rel_reflects_pred Rel PredB)"
proof (rule iffI, erule conjE)
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_respects_pred Rel PredA"
  from this obtain RelA where A1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ RelA"
                          and A2: "rel_respects_pred RelA PredA"
    by blast
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_reflects_pred Rel PredB"
  from this obtain RelB where A3: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ RelB"
                          and A4: "rel_reflects_pred RelB PredB"
    by blast
  from A2 have "∀(P, Q) ∈ RelA. PredA P ⟷ PredA Q"
    by blast
  moreover from A4 have "∀(P, Q) ∈ RelB. PredB Q ⟶ PredB P"
    by blast
  ultimately have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                   ∧ (∀(P, Q)∈Rel. PredA P = PredA Q) ∧ (∀(P, Q)∈Rel. PredB Q ⟶ PredB P)"
      using combine_conditions_on_relations_indRelR(1)[where RelA="RelA" and RelB="RelB" and
            CondA="λ(P, Q). PredA P ⟷ PredA Q" and CondB="λ(P, Q). PredB Q ⟶ PredB P"] A1 A3
    by simp
  thus "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_respects_pred Rel PredA
        ∧ rel_reflects_pred Rel PredB"
    by blast
next
  assume "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_respects_pred Rel PredA
          ∧ rel_reflects_pred Rel PredB"
  thus "(∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_respects_pred Rel PredA) ∧
        (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel) ∧ rel_reflects_pred Rel PredB)"
    by blast
qed

subsection ‹Divergence Reflection and Success Sensitiveness›

text ‹We combine results on divergence reflection and success sensitiveness to analyse their
        combined effect on an encoding function. An encoding is success sensitive and reflects
        divergence iff there exists a relation that relates source terms and their literal
        translations that reflects divergence and respects success.›

lemma (in encoding_wrt_barbs) WSS_DR_iff_source_target_rel:
  fixes success :: "'barbs"
  shows "(enc_weakly_respects_barb_set {success} ∧ enc_reflects_divergence)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
proof -
  have "∀Rel. rel_reflects_divergence Rel (STCal Source Target)
        = rel_reflects_pred Rel divergentST"
    by (simp add: divergentST_STCal_divergent)
  moreover have "∀Rel. (rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
                 = rel_respects_pred Rel (λP. P⇓.success))"
    by (simp add: STCalWB_reachesBarbST)
  ultimately show "(enc_weakly_respects_barb_set {success} ∧ enc_reflects_divergence)
    = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
       ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
       ∧ rel_reflects_divergence Rel (STCal Source Target))"
      using success_sensitive_iff_source_target_rel_weakly_respects_success(1)
            divergence_reflection_iff_source_target_rel_reflects_divergence
            indRelR_cond_respects_predA_and_reflects_predB[where
              PredA="λP. P⇓.success" and PredB="divergentST"]
    by simp
qed

lemma (in encoding_wrt_barbs) SS_DR_iff_source_target_rel:
  fixes success :: "'barbs"
  shows "(enc_respects_barb_set {success} ∧ enc_reflects_divergence)
         = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
            ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
proof -
  have "∀Rel. rel_reflects_divergence Rel (STCal Source Target)
        = rel_reflects_pred Rel divergentST"
    by (simp add: divergentST_STCal_divergent)
  moreover have "∀Rel. (rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
                 = rel_respects_pred Rel (λP. P↓.success))"
    by (simp add: STCalWB_hasBarbST)
  ultimately show "(enc_respects_barb_set {success} ∧ enc_reflects_divergence)
    = (∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
       ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
       ∧ rel_reflects_divergence Rel (STCal Source Target))"
      using success_sensitive_iff_source_target_rel_respects_success(1)
            divergence_reflection_iff_source_target_rel_reflects_divergence
            indRelR_cond_respects_predA_and_reflects_predB[where
              PredA="λP. P↓.success" and PredB="divergentST"]
    by simp
qed

subsection ‹Adding Operational Correspondence›

text ‹The effect of operational correspondence includes conditions (TRel is included,
        transitivity) that require a witness like indRelRTPO. In order to combine operational
        correspondence with success sensitiveness, we show that if the encoding and TRel (weakly)
        respects barbs than indRelRTPO (weakly) respects barbs. Since success is only a specific
        kind of barbs, the same holds for success sensitiveness.›

lemma (in encoding_wrt_barbs) enc_and_TRel_impl_indRelRTPO_weakly_respects_success:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  assumes encRS:  "enc_weakly_respects_barb_set {success}"
      and trelPS: "rel_weakly_preserves_barb_set TRel TWB {success}"
      and trelRS: "rel_weakly_reflects_barb_set TRel TWB {success}"
  shows "rel_weakly_respects_barb_set (indRelRTPO TRel) (STCalWB SWB TWB) {success}"
proof auto
  fix P Q P'
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "P ⟼(Calculus (STCalWB SWB TWB))* P'"
     and "P'↓<STCalWB SWB TWB>success"
  thus "Q⇓<STCalWB SWB TWB>success"
  proof (induct arbitrary: P')
    case (encR S)
    assume "SourceTerm S ⟼(Calculus (STCalWB SWB TWB))* P'" and "P'↓<STCalWB SWB TWB>success"
    hence "S⇓<SWB>success"
        using STCalWB_reachesBarbST
      by blast
    with encRS have "⟦S⟧⇓<TWB>success"
      by simp
    thus "TargetTerm (⟦S⟧)⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S ⟼(Calculus (STCalWB SWB TWB))* P'" and "P'↓<STCalWB SWB TWB>success"
    thus "SourceTerm S⇓<STCalWB SWB TWB>success"
      by blast
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T1 ⟼(Calculus (STCalWB SWB TWB))* P'"
                and "P'↓<STCalWB SWB TWB>success"
    hence "T1⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "T2⇓<TWB>success"
        using trelPS
      by simp
    thus "TargetTerm T2⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    case (trans P Q R)
    assume "P ⟼(Calculus (STCalWB SWB TWB))* P'" and "P'↓<STCalWB SWB TWB>success"
       and "⋀P'. P ⟼(Calculus (STCalWB SWB TWB))* P' ⟹ P'↓<STCalWB SWB TWB>success
            ⟹ Q⇓<STCalWB SWB TWB>success"
    hence "Q⇓<STCalWB SWB TWB>success"
      by simp
    moreover assume "⋀Q'. Q ⟼(Calculus (STCalWB SWB TWB))* Q' ⟹ Q'↓<STCalWB SWB TWB>success
                     ⟹ R⇓<STCalWB SWB TWB>success"
    ultimately show "R⇓<STCalWB SWB TWB>success"
      by blast
  qed
next
  fix P Q Q'
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "Q ⟼(Calculus (STCalWB SWB TWB))* Q'"
     and "Q'↓<STCalWB SWB TWB>success"
  thus "P⇓<STCalWB SWB TWB>success"
  proof (induct arbitrary: Q')
    case (encR S)
    assume "TargetTerm (⟦S⟧) ⟼(Calculus (STCalWB SWB TWB))* Q'"
       and "Q'↓<STCalWB SWB TWB>success"
    hence "⟦S⟧⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
    with encRS have "S⇓<SWB>success"
        by simp
    thus "SourceTerm S⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S ⟼(Calculus (STCalWB SWB TWB))* Q'" and "Q'↓<STCalWB SWB TWB>success"
    thus "SourceTerm S⇓<STCalWB SWB TWB>success"
      by blast
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T2 ⟼(Calculus (STCalWB SWB TWB))* Q'"
                and "Q'↓<STCalWB SWB TWB>success"
    hence "T2⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "T1⇓<TWB>success"
        using trelRS
      by blast
  thus "TargetTerm T1⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    case (trans P Q R R')
    assume "R ⟼(Calculus (STCalWB SWB TWB))* R'" and "R'↓<STCalWB SWB TWB>success"
       and "⋀R'. R ⟼(Calculus (STCalWB SWB TWB))* R' ⟹ R'↓<STCalWB SWB TWB>success
            ⟹ Q⇓<STCalWB SWB TWB>success"
    hence "Q⇓<STCalWB SWB TWB>success"
      by simp
    moreover assume "⋀Q'. Q ⟼(Calculus (STCalWB SWB TWB))* Q' ⟹ Q'↓<STCalWB SWB TWB>success
                     ⟹ P⇓<STCalWB SWB TWB>success"
    ultimately show "P⇓<STCalWB SWB TWB>success"
      by blast
  qed
qed

lemma (in encoding_wrt_barbs) enc_and_TRel_impl_indRelRTPO_weakly_respects_barbs:
  fixes TRel :: "('procT × 'procT) set"
  assumes encRS:  "enc_weakly_respects_barbs"
      and trelPS: "rel_weakly_preserves_barbs TRel TWB"
      and trelRS: "rel_weakly_reflects_barbs TRel TWB"
  shows "rel_weakly_respects_barbs (indRelRTPO TRel) (STCalWB SWB TWB)"
proof auto
  fix P Q x P'
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "P ⟼(Calculus (STCalWB SWB TWB))* P'"
     and "P'↓<STCalWB SWB TWB>x"
  thus "Q⇓<STCalWB SWB TWB>x"
  proof (induct arbitrary: P')
    case (encR S)
    assume "SourceTerm S ⟼(Calculus (STCalWB SWB TWB))* P'" and "P'↓<STCalWB SWB TWB>x"
    hence "S⇓<SWB>x"
        using STCalWB_reachesBarbST
      by blast
    with encRS have "⟦S⟧⇓<TWB>x"
      by simp
    thus "TargetTerm (⟦S⟧)⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S ⟼(Calculus (STCalWB SWB TWB))* P'" and "P'↓<STCalWB SWB TWB>x"
    thus "SourceTerm S⇓<STCalWB SWB TWB>x"
      by blast
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T1 ⟼(Calculus (STCalWB SWB TWB))* P'"
                and "P'↓<STCalWB SWB TWB>x"
    hence "T1⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "T2⇓<TWB>x"
        using trelPS
      by simp
    thus "TargetTerm T2⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    case (trans P Q R)
    assume "P ⟼(Calculus (STCalWB SWB TWB))* P'" and "P'↓<STCalWB SWB TWB>x"
       and "⋀P'. P ⟼(Calculus (STCalWB SWB TWB))* P' ⟹ P'↓<STCalWB SWB TWB>x
            ⟹ Q⇓<STCalWB SWB TWB>x"
    hence "Q⇓<STCalWB SWB TWB>x"
      by simp
    moreover assume "⋀Q'. Q ⟼(Calculus (STCalWB SWB TWB))* Q' ⟹ Q'↓<STCalWB SWB TWB>x
                     ⟹ R⇓<STCalWB SWB TWB>x"
    ultimately show "R⇓<STCalWB SWB TWB>x"
      by blast
  qed
next
  fix P Q x Q'
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "Q ⟼(Calculus (STCalWB SWB TWB))* Q'"
     and "Q'↓<STCalWB SWB TWB>x"
  thus "P⇓<STCalWB SWB TWB>x"
  proof (induct arbitrary: Q')
    case (encR S)
    assume "TargetTerm (⟦S⟧) ⟼(Calculus (STCalWB SWB TWB))* Q'"
       and "Q'↓<STCalWB SWB TWB>x"
    hence "⟦S⟧⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
    with encRS have "S⇓<SWB>x"
        by simp
    thus "SourceTerm S⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S ⟼(Calculus (STCalWB SWB TWB))* Q'" and "Q'↓<STCalWB SWB TWB>x"
    thus "SourceTerm S⇓<STCalWB SWB TWB>x"
      by blast
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T2 ⟼(Calculus (STCalWB SWB TWB))* Q'"
                and "Q'↓<STCalWB SWB TWB>x"
    hence "T2⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "T1⇓<TWB>x"
        using trelRS
      by blast
  thus "TargetTerm T1⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    case (trans P Q R R')
    assume "R ⟼(Calculus (STCalWB SWB TWB))* R'" and "R'↓<STCalWB SWB TWB>x"
       and "⋀R'. R ⟼(Calculus (STCalWB SWB TWB))* R' ⟹ R'↓<STCalWB SWB TWB>x
            ⟹ Q⇓<STCalWB SWB TWB>x"
    hence "Q⇓<STCalWB SWB TWB>x"
      by simp
    moreover assume "⋀Q'. Q ⟼(Calculus (STCalWB SWB TWB))* Q' ⟹ Q'↓<STCalWB SWB TWB>x
                     ⟹ P⇓<STCalWB SWB TWB>x"
    ultimately show "P⇓<STCalWB SWB TWB>x"
      by blast
  qed
qed

lemma (in encoding_wrt_barbs) enc_and_TRel_impl_indRelRTPO_respects_success:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  assumes encRS:  "enc_respects_barb_set {success}"
      and trelPS: "rel_preserves_barb_set TRel TWB {success}"
      and trelRS: "rel_reflects_barb_set TRel TWB {success}"
  shows "rel_respects_barb_set (indRelRTPO TRel) (STCalWB SWB TWB) {success}"
proof auto
  fix P Q
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "P↓<STCalWB SWB TWB>success"
  thus "Q↓<STCalWB SWB TWB>success"
  proof induct
    case (encR S)
    assume "SourceTerm S↓<STCalWB SWB TWB>success"
    hence "S↓<SWB>success"
        using STCalWB_hasBarbST
      by blast
    with encRS have "⟦S⟧↓<TWB>success"
      by simp
    thus "TargetTerm (⟦S⟧)↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S↓<STCalWB SWB TWB>success"
    thus "SourceTerm S↓<STCalWB SWB TWB>success"
      by simp
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T1↓<STCalWB SWB TWB>success"
    hence "T1↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
    ultimately have "T2↓<TWB>success"
        using trelPS
      by simp
    thus "TargetTerm T2↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
  next
    case (trans P Q R)
    assume "P↓<STCalWB SWB TWB>success"
       and "P↓<STCalWB SWB TWB>success ⟹ Q↓<STCalWB SWB TWB>success"
       and "Q↓<STCalWB SWB TWB>success ⟹ R↓<STCalWB SWB TWB>success"
    thus "R↓<STCalWB SWB TWB>success"
      by simp
  qed
next
  fix P Q
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "Q↓<STCalWB SWB TWB>success"
  thus "P↓<STCalWB SWB TWB>success"
  proof induct
    case (encR S)
    assume "TargetTerm (⟦S⟧)↓<STCalWB SWB TWB>success"
    hence "⟦S⟧↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
    with encRS have "S↓<SWB>success"
        by simp
    thus "SourceTerm S↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S↓<STCalWB SWB TWB>success"
    thus "SourceTerm S↓<STCalWB SWB TWB>success"
      by simp
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T2↓<STCalWB SWB TWB>success"
    hence "T2↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
    ultimately have "T1↓<TWB>success"
        using trelRS
      by blast
  thus "TargetTerm T1↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
  next
    case (trans P Q R)
    assume "R↓<STCalWB SWB TWB>success"
       and "R↓<STCalWB SWB TWB>success ⟹ Q↓<STCalWB SWB TWB>success"
       and "Q↓<STCalWB SWB TWB>success ⟹ P↓<STCalWB SWB TWB>success"
    thus "P↓<STCalWB SWB TWB>success"
      by simp
  qed
qed

lemma (in encoding_wrt_barbs) enc_and_TRel_impl_indRelRTPO_respects_barbs:
  fixes TRel    :: "('procT × 'procT) set"
  assumes encRS:  "enc_respects_barbs"
      and trelPS: "rel_preserves_barbs TRel TWB"
      and trelRS: "rel_reflects_barbs TRel TWB"
  shows "rel_respects_barbs (indRelRTPO TRel) (STCalWB SWB TWB)"
proof auto
  fix P Q x
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "P↓<STCalWB SWB TWB>x"
  thus "Q↓<STCalWB SWB TWB>x"
  proof induct
    case (encR S)
    assume "SourceTerm S↓<STCalWB SWB TWB>x"
    hence "S↓<SWB>x"
        using STCalWB_hasBarbST
      by blast
    with encRS have "⟦S⟧↓<TWB>x"
      by simp
    thus "TargetTerm (⟦S⟧)↓<STCalWB SWB TWB>x"
        using STCalWB_hasBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S↓<STCalWB SWB TWB>x"
    thus "SourceTerm S↓<STCalWB SWB TWB>x"
      by simp
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T1↓<STCalWB SWB TWB>x"
    hence "T1↓<TWB>x"
        using STCalWB_hasBarbST
      by blast
    ultimately have "T2↓<TWB>x"
        using trelPS
      by simp
    thus "TargetTerm T2↓<STCalWB SWB TWB>x"
        using STCalWB_hasBarbST
      by blast
  next
    case (trans P Q R)
    assume "P↓<STCalWB SWB TWB>x"
       and "P↓<STCalWB SWB TWB>x ⟹ Q↓<STCalWB SWB TWB>x"
       and "Q↓<STCalWB SWB TWB>x ⟹ R↓<STCalWB SWB TWB>x"
    thus "R↓<STCalWB SWB TWB>x"
      by simp
  qed
next
  fix P Q x
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "Q↓<STCalWB SWB TWB>x"
  thus "P↓<STCalWB SWB TWB>x"
  proof induct
    case (encR S)
    assume "TargetTerm (⟦S⟧)↓<STCalWB SWB TWB>x"
    hence "⟦S⟧↓<TWB>x"
        using STCalWB_hasBarbST
      by blast
    with encRS have "S↓<SWB>x"
        by simp
    thus "SourceTerm S↓<STCalWB SWB TWB>x"
        using STCalWB_hasBarbST
      by blast
  next
    case (source S)
    assume "SourceTerm S↓<STCalWB SWB TWB>x"
    thus "SourceTerm S↓<STCalWB SWB TWB>x"
      by simp
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T2↓<STCalWB SWB TWB>x"
    hence "T2↓<TWB>x"
        using STCalWB_hasBarbST
      by blast
    ultimately have "T1↓<TWB>x"
        using trelRS
      by blast
  thus "TargetTerm T1↓<STCalWB SWB TWB>x"
        using STCalWB_hasBarbST
      by blast
  next
    case (trans P Q R)
    assume "R↓<STCalWB SWB TWB>x"
       and "R↓<STCalWB SWB TWB>x ⟹ Q↓<STCalWB SWB TWB>x"
       and "Q↓<STCalWB SWB TWB>x ⟹ P↓<STCalWB SWB TWB>x"
    thus "P↓<STCalWB SWB TWB>x"
      by simp
  qed
qed

text ‹An encoding is success sensitive and operational corresponding w.r.t. a bisimulation TRel
        that respects success iff there exists a bisimultion that includes TRel and respects
        success. The same holds if we consider not only success sensitiveness but barb
        sensitiveness in general.›

lemma (in encoding_wrt_barbs) OC_SS_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(operational_corresponding (TRel⇧*)
          ∧ weak_reduction_bisimulation (TRel⇧+) Target
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def have B2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    by (simp add: indRelRTPO.target)
  from Rel_def have B3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by (simp add: indRelRTPO_to_TRel(4)[where TRel="TRel"])
  from Rel_def have B4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete (TRel⇧*)"
     and "operational_sound (TRel⇧*)"
     and "weak_reduction_simulation (TRel⇧+) Target"
     and "∀P Q Q'. (P, Q) ∈ TRel⇧+ ∧ Q ⟼Target* Q'
          ⟶ (∃P'. P ⟼Target* P' ∧ (P', Q') ∈ TRel⇧+)"
  with Rel_def have B5: "weak_reduction_bisimulation Rel (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  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)
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 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)
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and C2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and C3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and C4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
   and C5: "weak_reduction_bisimulation Rel (STCal Source Target)"
   and C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by auto
  from C1 C2 C3 C4 C5 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)"
    by blast
  hence "operational_corresponding (TRel⇧*)
        ∧ weak_reduction_bisimulation (TRel⇧+) Target"
      using OC_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by auto
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using C1 C6 by blast
  hence "enc_weakly_respects_barb_set {success}"
      using success_sensitive_iff_source_target_rel_weakly_respects_success
    by auto
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  ultimately show "operational_corresponding (TRel⇧*)
   ∧ weak_reduction_bisimulation (TRel⇧+) Target
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}"
    by fast
qed

lemma (in encoding_wrt_barbs) OC_SS_RB_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(operational_corresponding (TRel⇧*)
          ∧ weak_reduction_bisimulation (TRel⇧+) Target
          ∧ enc_weakly_respects_barbs ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barbs TRel TWB ∧ rel_weakly_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "rel_weakly_preserves_barbs TRel TWB" and A6: "rel_weakly_reflects_barbs TRel TWB"
     and A7: "enc_weakly_preserves_barbs" and A8: "enc_weakly_reflects_barbs"
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def have B2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    by (simp add: indRelRTPO.target)
  from Rel_def have B3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by (simp add: indRelRTPO_to_TRel(4)[where TRel="TRel"])
  from Rel_def have B4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete (TRel⇧*)"
     and "operational_sound (TRel⇧*)"
     and "weak_reduction_simulation (TRel⇧+) Target"
     and "∀P Q Q'. (P, Q) ∈ TRel⇧+ ∧ Q ⟼Target* Q' ⟶ (∃P'. P ⟼Target* P' ∧ (P', Q') ∈ TRel⇧+)"
  with Rel_def have B5: "weak_reduction_bisimulation Rel (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  from Rel_def A5 A6 A7 A8 have B7: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_barbs[where TRel="TRel"]
    by blast
  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)
        ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C: "(∀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)
          ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by auto
  hence C1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by simp
  from C have C2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    by simp
  from C have C3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by simp
  from C have C4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    by simp
  from C have C5: "weak_reduction_bisimulation Rel (STCal Source Target)"
    by simp
  from C have C7: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
    apply (rule conjE) apply (erule conjE)+ by blast
  from C have C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule conjE) apply (erule conjE)+ by blast
  from C1 C2 C3 C4 C5 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)"
    by blast
  hence "operational_corresponding (TRel⇧*)
        ∧ weak_reduction_bisimulation (TRel⇧+) Target"
      using OC_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by auto
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using C1 C6 by blast
  hence "enc_weakly_respects_barb_set {success}"
      using success_sensitive_iff_source_target_rel_weakly_respects_success
    by auto
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
    apply (rule exI) using C1 C7 by blast
  hence "enc_weakly_respects_barbs"
      using enc_weakly_respects_barbs_iff_source_target_rel
    by auto
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  moreover have "rel_weakly_respects_barbs TRel TWB"
  proof auto
    fix TP TQ x TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>x"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>x"
        using C7
      by blast
    thus "TQ⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ x TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>x"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>x"
        using C7
      by blast
    thus "TP⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
  qed
  ultimately show "operational_corresponding (TRel⇧*)
   ∧ weak_reduction_bisimulation (TRel⇧+) Target
   ∧ enc_weakly_respects_barbs ∧ enc_weakly_respects_barb_set {success}
   ∧ rel_weakly_respects_barbs TRel TWB ∧ rel_weakly_respects_barb_set TRel TWB {success}"
    by fast
qed

lemma (in encoding_wrt_barbs) OC_SS_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "preorder TRel"
  from A5 have A6: "TRel⇧+ = TRel"
      using trancl_id[of TRel] preorder_on_def
    by blast
  from A5 have A7: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding refl_on_def preorder_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A6 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A7 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete TRel" and "operational_sound TRel"
     and "weak_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target* Q' ⟶ (∃P'. P ⟼Target* P' ∧ (P', Q') ∈ TRel)"
  with Rel_def A6 A7 have B4: "weak_reduction_bisimulation Rel (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A5 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by blast
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  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)
        ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 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)
          ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "(∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)"
   and C4: "weak_reduction_bisimulation Rel (STCal Source Target)" and C5: "preorder Rel"
   and C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target"
      using OC_wrt_preorder_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using C1 C6 by blast
  hence "enc_weakly_respects_barb_set {success}"
      using success_sensitive_iff_source_target_rel_weakly_respects_success
    by simp
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  ultimately show "operational_corresponding TRel ∧ preorder TRel
   ∧ weak_reduction_bisimulation TRel Target
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}"
    by fast
qed

lemma (in encoding_wrt_barbs) OC_SS_RB_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target
          ∧ enc_weakly_respects_barbs ∧ rel_weakly_respects_barbs TRel TWB
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barbs TRel TWB" and A2: "rel_weakly_reflects_barbs TRel TWB"
     and A3: "enc_weakly_preserves_barbs" and A4: "enc_weakly_reflects_barbs"
     and A5: "preorder TRel"
  from A5 have A6: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A5 have A7: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A6 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A7 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete TRel" and "operational_sound TRel"
     and "weak_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target* Q' ⟶ (∃P'. P ⟼Target* P' ∧ (P', Q') ∈ TRel)"
  with Rel_def A6 A7 have B4: "weak_reduction_bisimulation Rel (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A5 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by blast
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_barbs[where TRel="TRel"]
    by blast
  hence B7: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by blast
  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)
        ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "(∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)"
   and C4: "weak_reduction_bisimulation Rel (STCal Source Target)" and C5: "preorder Rel"
   and C6: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target"
      using OC_wrt_preorder_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
    apply (rule exI) using C1 C6 by blast
  hence "enc_weakly_respects_barbs"
      using enc_weakly_respects_barbs_iff_source_target_rel
    by simp
  moreover hence "enc_weakly_respects_barb_set {success}"
    by simp
  moreover have "rel_weakly_respects_barbs TRel TWB"
  proof auto
    fix TP TQ x TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>x"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>x"
        using C6
      by blast
    thus "TQ⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ x TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>x"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>x"
        using C6
      by blast
    thus "TP⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
  qed
  moreover hence "rel_weakly_respects_barb_set TRel TWB {success}"
    by blast
  ultimately show "operational_corresponding TRel ∧ preorder TRel
   ∧ weak_reduction_bisimulation TRel Target
   ∧ enc_weakly_respects_barbs ∧ rel_weakly_respects_barbs TRel TWB 
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}"
    by fast
qed

text ‹An encoding is success sensitive and weakly operational corresponding w.r.t. a
        correspondence simulation TRel that respects success iff there exists a correspondence
        simultion that includes TRel and respects success. The same holds if we consider not only
        success sensitiveness but barb sensitiveness in general.›

lemma (in encoding_wrt_barbs) WOC_SS_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(weakly_operational_corresponding TRel ∧ preorder TRel
          ∧ weak_reduction_correspondence_simulation TRel Target
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "preorder TRel"
  from A5 have A6: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A5 A6 have A7: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A6 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A7 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete TRel" and "weakly_operational_sound TRel"
     and "weak_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target* Q'
          ⟶ (∃P'' Q''. P ⟼Target* P'' ∧ Q' ⟼Target* Q'' ∧ (P'', Q'') ∈ TRel)"
  with Rel_def A6 A7 have B4: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
      using WOC_iff_indRelRTPO_is_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  from Rel_def A5 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by blast
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  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)
        ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 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)
          ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "(∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)"
   and C4: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
   and C5: "preorder Rel" and C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "weakly_operational_corresponding TRel ∧ preorder TRel
         ∧ weak_reduction_correspondence_simulation TRel Target"
      using WOC_wrt_preorder_iff_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using C1 C6 by blast
  hence "enc_weakly_respects_barb_set {success}"
      using success_sensitive_iff_source_target_rel_weakly_respects_success
    by simp
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  ultimately show "weakly_operational_corresponding TRel ∧ preorder TRel
   ∧ weak_reduction_correspondence_simulation TRel Target
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}"
    by fast
qed

lemma (in encoding_wrt_barbs) WOC_SS_RB_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(weakly_operational_corresponding TRel ∧ preorder TRel
          ∧ weak_reduction_correspondence_simulation TRel Target
          ∧ enc_weakly_respects_barbs ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barbs TRel TWB ∧ rel_weakly_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "preorder TRel"
     and A1': "rel_weakly_preserves_barbs TRel TWB" and A2': "rel_weakly_reflects_barbs TRel TWB"
     and A3': "enc_weakly_preserves_barbs" and A4': "enc_weakly_reflects_barbs"
  from A5 have A6: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A5 A6 have A7: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A6 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A7 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete TRel" and "weakly_operational_sound TRel"
     and "weak_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target* Q'
          ⟶ (∃P'' Q''. P ⟼Target* P'' ∧ Q' ⟼Target* Q'' ∧ (P'', Q'') ∈ TRel)"
  with Rel_def A6 A7 have B4: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
      using WOC_iff_indRelRTPO_is_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  from Rel_def A5 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by blast
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  from Rel_def A1' A2' A3' A4' have B7: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_barbs[where TRel="TRel"]
    by blast
  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)
        ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "(∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)"
   and C4: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
   and C5: "preorder Rel" and C7: "rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "weakly_operational_corresponding TRel ∧ preorder TRel
         ∧ weak_reduction_correspondence_simulation TRel Target"
      using WOC_wrt_preorder_iff_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barbs Rel (STCalWB SWB TWB)"
    apply (rule exI) using C1 C7 by blast
  hence D1: "enc_weakly_respects_barbs"
      using enc_weakly_respects_barbs_iff_source_target_rel
    by simp
  moreover from D1 have "enc_weakly_respects_barb_set {success}"
    by simp
  moreover have D2: "rel_weakly_respects_barbs TRel TWB"
  proof auto
    fix TP TQ x TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>x"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>x"
        using C7
      by blast
    thus "TQ⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ x TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>x"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>x"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>x"
        using C7
      by blast
    thus "TP⇓<TWB>x"
        using STCalWB_reachesBarbST
      by blast
  qed
  moreover from D2 have "rel_weakly_respects_barb_set TRel TWB {success}"
    by blast
  ultimately show "weakly_operational_corresponding TRel ∧ preorder TRel
   ∧ weak_reduction_correspondence_simulation TRel Target
   ∧ enc_weakly_respects_barbs ∧ enc_weakly_respects_barb_set {success}
   ∧ rel_weakly_respects_barbs TRel TWB ∧ rel_weakly_respects_barb_set TRel TWB {success}"
    by fast
qed

text ‹An encoding is strongly success sensitive and strongly operational corresponding w.r.t. a
        strong bisimulation TRel that strongly respects success iff there exists a strong
        bisimultion that includes TRel and strongly respects success. The same holds if we consider
        not only strong success sensitiveness but strong barb sensitiveness in general.›

lemma (in encoding_wrt_barbs) SOC_SS_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(strongly_operational_corresponding TRel ∧ preorder TRel
          ∧ strong_reduction_bisimulation TRel Target
          ∧ enc_respects_barb_set {success} ∧ rel_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_preserves_barb_set TRel TWB {success}"
     and A2: "rel_reflects_barb_set TRel TWB {success}"
     and A3: "enc_preserves_barb_set {success}" and A4: "enc_reflects_barb_set {success}"
     and A5: "preorder TRel"
  from A5 have A6: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A5 A6 have A7: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A6 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A7 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "strongly_operational_complete TRel" and "strongly_operational_sound TRel"
     and "strong_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target Q' ⟶ (∃P'. P ⟼Target P' ∧ (P', Q') ∈ TRel)"
  with Rel_def A6 A7 have B4: "strong_reduction_bisimulation Rel (STCal Source Target)"
      using SOC_iff_indRelRTPO_is_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A5 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by blast
  from Rel_def A1 A2 A3 A4 have B6: "rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_respects_success[where TRel="TRel" and success="success"]
    by blast
  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)
        ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 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)
          ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "(∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)"
   and C4: "strong_reduction_bisimulation Rel (STCal Source Target)" and C5: "preorder Rel"
   and C6: "rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "strongly_operational_corresponding TRel ∧ preorder TRel
         ∧ strong_reduction_bisimulation TRel Target"
      using SOC_wrt_preorder_iff_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using C1 C6 by blast
  hence "enc_respects_barb_set {success}"
      using success_sensitive_iff_source_target_rel_respects_success
    by simp
  moreover have "rel_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP↓<TWB>success"
    hence "TargetTerm TP↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
    ultimately have "TargetTerm TQ↓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
  next
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ↓<TWB>success"
    hence "TargetTerm TQ↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
    ultimately have "TargetTerm TP↓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
  qed
  ultimately show "strongly_operational_corresponding TRel ∧ preorder TRel
   ∧ strong_reduction_bisimulation TRel Target
   ∧ enc_respects_barb_set {success} ∧ rel_respects_barb_set TRel TWB {success}"
    by fast
qed

lemma (in encoding_wrt_barbs) SOC_SS_RB_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(strongly_operational_corresponding TRel ∧ preorder TRel
          ∧ strong_reduction_bisimulation TRel Target
          ∧ enc_respects_barbs ∧ rel_respects_barbs TRel TWB
          ∧ enc_respects_barb_set {success} ∧ rel_respects_barb_set TRel TWB {success})
         = (∃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)
            ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_respects_barbs Rel (STCalWB SWB TWB)
            ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success})"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_preserves_barbs TRel TWB" and A2: "rel_reflects_barbs TRel TWB"
     and A3: "enc_preserves_barbs" and A4: "enc_reflects_barbs"
     and A5: "preorder TRel"
  from A5 have A6: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A5 have A7: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A6 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A7 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "strongly_operational_complete TRel" and "strongly_operational_sound TRel"
     and "strong_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target Q' ⟶ (∃P'. P ⟼Target P' ∧ (P', Q') ∈ TRel)"
  with Rel_def A6 A7 have B4: "strong_reduction_bisimulation Rel (STCal Source Target)"
      using SOC_iff_indRelRTPO_is_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A5 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by blast
  from Rel_def A1 A2 A3 A4 have B6: "rel_respects_barbs Rel (STCalWB SWB TWB)"
      using enc_and_TRel_impl_indRelRTPO_respects_barbs[where TRel="TRel"]
    by blast
  hence B7: "rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    by blast
  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)
        ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_respects_barbs Rel (STCalWB SWB TWB)
        ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 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)
          ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_respects_barbs Rel (STCalWB SWB TWB)
          ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
  from this obtain Rel where C1: "(∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "(∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel)"
   and C4: "strong_reduction_bisimulation Rel (STCal Source Target)" and C5: "preorder Rel"
   and C6: "rel_respects_barbs Rel (STCalWB SWB TWB)"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "strongly_operational_corresponding TRel ∧ preorder TRel
         ∧ strong_reduction_bisimulation TRel Target"
      using SOC_wrt_preorder_iff_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_respects_barbs Rel (STCalWB SWB TWB)"
    apply (rule exI) using C1 C6 by blast
  hence "enc_respects_barbs"
      using enc_respects_barbs_iff_source_target_rel
    by simp
  moreover hence "enc_respects_barb_set {success}"
    by simp
  moreover have "rel_respects_barbs TRel TWB"
  proof auto
    fix TP TQ x
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP↓<TWB>x"
    hence "TargetTerm TP↓<STCalWB SWB TWB>x"
        using STCalWB_hasBarbST
      by blast
    ultimately have "TargetTerm TQ↓<STCalWB SWB TWB>x"
        using C6
      by blast
    thus "TQ↓<TWB>x"
        using STCalWB_hasBarbST
      by blast
  next
    fix TP TQ x
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ↓<TWB>x"
    hence "TargetTerm TQ↓<STCalWB SWB TWB>x"
        using STCalWB_hasBarbST
      by blast
    ultimately have "TargetTerm TP↓<STCalWB SWB TWB>x"
        using C6
      by blast
    thus "TP↓<TWB>x"
        using STCalWB_hasBarbST
      by blast
  qed
  moreover hence "rel_respects_barb_set TRel TWB {success}"
    by blast
  ultimately show "strongly_operational_corresponding TRel ∧ preorder TRel
   ∧ strong_reduction_bisimulation TRel Target
   ∧ enc_respects_barbs ∧ rel_respects_barbs TRel TWB
   ∧ enc_respects_barb_set {success} ∧ rel_respects_barb_set TRel TWB {success}"
    by fast
qed

text ‹Next we also add divergence reflection to operational correspondence and success
        sensitiveness.›

lemma (in encoding) enc_and_TRelimpl_indRelRTPO_reflect_divergence:
  fixes TRel    :: "('procT × 'procT) set"
  assumes encRD:  "enc_reflects_divergence"
      and trelRD: "rel_reflects_divergence TRel Target"
  shows "rel_reflects_divergence (indRelRTPO TRel) (STCal Source Target)"
proof auto
  fix P Q
  assume "P ≲⟦⋅⟧RT<TRel> Q" and "Q ⟼(STCal Source Target)ω"
  thus "P ⟼(STCal Source Target)ω"
  proof induct
    case (encR S)
    assume "TargetTerm (⟦S⟧) ⟼(STCal Source Target)ω"
    hence "⟦S⟧ ⟼(Target)ω"
      by (simp add: STCal_divergent(2))
    with encRD have "S ⟼(Source)ω"
      by simp
    thus "SourceTerm S ⟼(STCal Source Target)ω"
      by (simp add: STCal_divergent(1))
  next
    case (source S)
    assume "SourceTerm S ⟼(STCal Source Target)ω"
    thus "SourceTerm S ⟼(STCal Source Target)ω"
      by simp
  next
    case (target T1 T2)
    assume "(T1, T2) ∈ TRel"
    moreover assume "TargetTerm T2 ⟼(STCal Source Target)ω"
    hence "T2 ⟼(Target)ω"
      by (simp add: STCal_divergent(2))
    ultimately have "T1 ⟼(Target)ω"
        using trelRD
      by blast
    thus "TargetTerm T1 ⟼(STCal Source Target)ω"
      by (simp add: STCal_divergent(2))
  next
    case (trans P Q R)
    assume "R ⟼(STCal Source Target)ω"
       and "R ⟼(STCal Source Target)ω ⟹ Q ⟼(STCal Source Target)ω"
       and "Q ⟼(STCal Source Target)ω ⟹ P ⟼(STCal Source Target)ω"
    thus "P ⟼(STCal Source Target)ω"
      by simp
  qed
qed

lemma (in encoding_wrt_barbs) OC_SS_DR_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(operational_corresponding (TRel⇧*)
          ∧ weak_reduction_bisimulation (TRel⇧+) Target
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success}
          ∧ enc_reflects_divergence ∧ rel_reflects_divergence 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)
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "rel_reflects_divergence TRel Target" and A6: "enc_reflects_divergence"
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def have B2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
    by (simp add: indRelRTPO.target)
  from Rel_def have B3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
    by (simp add: indRelRTPO_to_TRel(4)[where TRel="TRel"])
  from Rel_def have B4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete (TRel⇧*)"
     and "operational_sound (TRel⇧*)"
     and "weak_reduction_simulation (TRel⇧+) Target"
     and "∀P Q Q'. (P, Q) ∈ TRel⇧+ ∧ Q ⟼Target* Q'
          ⟶ (∃P'. P ⟼Target* P' ∧ (P', Q') ∈ TRel⇧+)"
  with Rel_def have B5: "weak_reduction_bisimulation Rel (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  from Rel_def A5 A6 have B7: "rel_reflects_divergence Rel (STCal Source Target)"
      using enc_and_TRelimpl_indRelRTPO_reflect_divergence[where TRel="TRel"]
    by blast
  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)
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
        ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
          ∧ rel_reflects_divergence Rel (STCal Source Target)"
  from this obtain Rel where C1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and C2: "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
   and C3: "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
   and C4: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
   and C5: "weak_reduction_bisimulation Rel (STCal Source Target)"
   and C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
   and C7: "rel_reflects_divergence Rel (STCal Source Target)"
    by auto
  from C1 C2 C3 C4 C5 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)"
    by blast
  hence "operational_corresponding (TRel⇧*)
        ∧ weak_reduction_bisimulation (TRel⇧+) Target"
      using OC_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by auto
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
                 ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using C1 C6 C7 by blast
  hence "enc_weakly_respects_barb_set {success} ∧ enc_reflects_divergence"
      using WSS_DR_iff_source_target_rel
    by auto
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  moreover from C2 C7 have "rel_reflects_divergence TRel Target"
      using STCal_divergent(2)
    by blast
  ultimately show "operational_corresponding (TRel⇧*)
   ∧ weak_reduction_bisimulation (TRel⇧+) Target
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}
   ∧ enc_reflects_divergence ∧ rel_reflects_divergence TRel Target"
    by fast
qed

lemma (in encoding_wrt_barbs) WOC_SS_DR_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(weakly_operational_corresponding TRel ∧ preorder TRel
          ∧ weak_reduction_correspondence_simulation TRel Target
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success}
          ∧ enc_reflects_divergence ∧ rel_reflects_divergence 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)
            ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "rel_reflects_divergence TRel Target" and A6: "enc_reflects_divergence"
     and A7: "preorder TRel"
  from A7 have A8: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A7 have A9: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A8 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A9 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete TRel" and "weakly_operational_sound TRel" and "preorder TRel"
     and "weak_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target* Q'
          ⟶ (∃P'' Q''. P ⟼Target* P'' ∧ Q' ⟼Target* Q'' ∧ (P'', Q'') ∈ TRel)"
  with Rel_def A8 A9 have B4: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
      using WOC_iff_indRelRTPO_is_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  from Rel_def A7 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by simp
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  from Rel_def A5 A6 have B7: "rel_reflects_divergence Rel (STCal Source Target)"
      using enc_and_TRelimpl_indRelRTPO_reflect_divergence[where TRel="TRel"]
    by blast
  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)
        ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
        ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ weak_reduction_correspondence_simulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
          ∧ rel_reflects_divergence Rel (STCal Source Target)"
  from this obtain Rel where C1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
   and C4: "weak_reduction_correspondence_simulation Rel (STCal Source Target)"
   and C5: "preorder Rel" and C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
   and C7: "rel_reflects_divergence Rel (STCal Source Target)"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "weakly_operational_corresponding TRel ∧ preorder TRel
         ∧ weak_reduction_correspondence_simulation TRel Target"
      using WOC_wrt_preorder_iff_reduction_correspondence_simulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
                 ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using C1 C6 C7 by blast
  hence "enc_weakly_respects_barb_set {success} ∧ enc_reflects_divergence"
      using WSS_DR_iff_source_target_rel
    by simp
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  moreover from C2 C7 have "rel_reflects_divergence TRel Target"
      using STCal_divergent(2)
    by blast
  ultimately
  show "weakly_operational_corresponding TRel ∧ preorder TRel
   ∧ weak_reduction_correspondence_simulation TRel Target
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}
   ∧ enc_reflects_divergence ∧ rel_reflects_divergence TRel Target"
    by fast
qed

lemma (in encoding_wrt_barbs) OC_SS_DR_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target
          ∧ enc_weakly_respects_barb_set {success}
          ∧ rel_weakly_respects_barb_set TRel TWB {success}
          ∧ enc_reflects_divergence ∧ rel_reflects_divergence 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)
            ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_weakly_preserves_barb_set TRel TWB {success}"
     and A2: "rel_weakly_reflects_barb_set TRel TWB {success}"
     and A3: "enc_weakly_preserves_barb_set {success}"
     and A4: "enc_weakly_reflects_barb_set {success}"
     and A5: "rel_reflects_divergence TRel Target" and A6: "enc_reflects_divergence"
     and A7: "preorder TRel"
  from A7 have A8: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A7 have A9: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A8 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A9 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "operational_complete TRel" and "operational_sound TRel" and "preorder TRel"
     and "weak_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target* Q' ⟶ (∃P'. P ⟼Target* P' ∧ (P', Q') ∈ TRel)"
  with Rel_def A8 A9 have B4: "weak_reduction_bisimulation Rel (STCal Source Target)"
      using OC_iff_indRelRTPO_is_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A7 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by simp
  from Rel_def A1 A2 A3 A4 have B6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_weakly_respects_success[where TRel="TRel"
            and success="success"]
    by blast
  from Rel_def A5 A6 have B7: "rel_reflects_divergence Rel (STCal Source Target)"
      using enc_and_TRelimpl_indRelRTPO_reflect_divergence[where TRel="TRel"]
    by blast
  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)
        ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
        ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ weak_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
          ∧ rel_reflects_divergence Rel (STCal Source Target)"
  from this obtain Rel where C1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
   and C4: "weak_reduction_bisimulation Rel (STCal Source Target)" and C5: "preorder Rel"
   and C6: "rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}"
   and C7: "rel_reflects_divergence Rel (STCal Source Target)"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target"
      using OC_wrt_preorder_iff_weak_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_weakly_respects_barb_set Rel (STCalWB SWB TWB) {success}
                 ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using C1 C6 C7 by blast
  hence "enc_weakly_respects_barb_set {success} ∧ enc_reflects_divergence"
      using WSS_DR_iff_source_target_rel
    by simp
  moreover have "rel_weakly_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ TP'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP ⟼(Calculus TWB)* TP'" and "TP'↓<TWB>success"
    hence "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  next
    fix TP TQ TQ'
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ ⟼(Calculus TWB)* TQ'" and "TQ'↓<TWB>success"
    hence "TargetTerm TQ⇓<STCalWB SWB TWB>success"
        using STCalWB_reachesBarbST
      by blast
    ultimately have "TargetTerm TP⇓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP⇓<TWB>success"
        using STCalWB_reachesBarbST
      by blast
  qed
  moreover from C2 C7 have "rel_reflects_divergence TRel Target"
      using STCal_divergent(2)
    by blast
  ultimately
  show "operational_corresponding TRel ∧ preorder TRel ∧ weak_reduction_bisimulation TRel Target
   ∧ enc_weakly_respects_barb_set {success} ∧ rel_weakly_respects_barb_set TRel TWB {success}
   ∧ enc_reflects_divergence ∧ rel_reflects_divergence TRel Target"
    by fast
qed

lemma (in encoding_wrt_barbs) SOC_SS_DR_wrt_preorder_iff_source_target_rel:
  fixes success :: "'barbs"
    and TRel    :: "('procT × 'procT) set"
  shows "(strongly_operational_corresponding TRel ∧ preorder TRel
          ∧ strong_reduction_bisimulation TRel Target
          ∧ enc_respects_barb_set {success} ∧ rel_respects_barb_set TRel TWB {success}
          ∧ enc_reflects_divergence ∧ rel_reflects_divergence 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)
            ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
            ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
            ∧ rel_reflects_divergence Rel (STCal Source Target))"
proof (rule iffI, (erule conjE)+)
  assume A1: "rel_preserves_barb_set TRel TWB {success}"
     and A2: "rel_reflects_barb_set TRel TWB {success}"
     and A3: "enc_preserves_barb_set {success}" and A4: "enc_reflects_barb_set {success}"
     and A5: "rel_reflects_divergence TRel Target" and A6: "enc_reflects_divergence"
     and A7: "preorder TRel"
  from A7 have A8: "TRel⇧+ = TRel"
      using trancl_id[of TRel]
      unfolding preorder_on_def
    by blast
  from A7 have A9: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding preorder_on_def refl_on_def
    by auto
  define Rel where "Rel = indRelRTPO TRel"
  hence B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
    by (simp add: indRelRTPO.encR)
  from Rel_def A8 have B2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
      using indRelRTPO_to_TRel(4)[where TRel="TRel"]
    by (auto simp add: indRelRTPO.target)
  from Rel_def A9 have B3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
      using indRelRTPO_to_TRel(2)[where TRel="TRel"]
            trans_closure_of_TRel_refl_cond[where TRel="TRel"]
    by simp
  assume "strongly_operational_complete TRel" and "strongly_operational_sound TRel"
     and "preorder TRel" and "strong_reduction_simulation TRel Target"
     and "∀P Q Q'. (P, Q) ∈ TRel ∧ Q ⟼Target Q' ⟶ (∃P'. P ⟼Target P' ∧ (P', Q') ∈ TRel)"
  with Rel_def A8 A9 have B4: "strong_reduction_bisimulation Rel (STCal Source Target)"
      using SOC_iff_indRelRTPO_is_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  from Rel_def A7 have B5: "preorder Rel"
      using indRelRTPO_is_preorder[where TRel="TRel"]
      unfolding preorder_on_def
    by simp
  from Rel_def A1 A2 A3 A4 have B6: "rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
      using enc_and_TRel_impl_indRelRTPO_respects_success[where TRel="TRel" and success="success"]
    by blast
  from Rel_def A5 A6 have B7: "rel_reflects_divergence Rel (STCal Source Target)"
      using enc_and_TRelimpl_indRelRTPO_reflect_divergence[where TRel="TRel"]
    by blast
  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)
        ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
        ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
        ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using B1 B2 B3 B4 B5 B6 B7 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)
          ∧ strong_reduction_bisimulation Rel (STCal Source Target) ∧ preorder Rel
          ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
          ∧ rel_reflects_divergence Rel (STCal Source Target)"
  from this obtain Rel where C1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
   and C2: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and C3: "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel"
   and C4: "strong_reduction_bisimulation Rel (STCal Source Target)" and C5: "preorder Rel"
   and C6: "rel_respects_barb_set Rel (STCalWB SWB TWB) {success}"
   and C7: "rel_reflects_divergence Rel (STCal Source Target)"
    by auto
  from C1 C2 C3 C4 C5 have "∃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)"
    by blast
  hence "strongly_operational_corresponding TRel ∧ preorder TRel
         ∧ strong_reduction_bisimulation TRel Target"
      using SOC_wrt_preorder_iff_strong_reduction_bisimulation[where TRel="TRel"]
    by simp
  moreover have "∃Rel. (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel)
                 ∧ rel_respects_barb_set Rel (STCalWB SWB TWB) {success}
                 ∧ rel_reflects_divergence Rel (STCal Source Target)"
    apply (rule exI) using C1 C6 C7 by blast
  hence "enc_respects_barb_set {success} ∧ enc_reflects_divergence"
      using SS_DR_iff_source_target_rel
    by simp
  moreover have "rel_respects_barb_set TRel TWB {success}"
  proof auto
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TP↓<TWB>success"
    hence "TargetTerm TP↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
    ultimately have "TargetTerm TQ↓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TQ↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
  next
    fix TP TQ
    assume "(TP, TQ) ∈ TRel"
    with C2 have "(TargetTerm TP, TargetTerm TQ) ∈ Rel"
      by simp
    moreover assume "TQ↓<TWB>success"
    hence "TargetTerm TQ↓<STCalWB SWB TWB>success"
        using STCalWB_hasBarbST
      by blast
    ultimately have "TargetTerm TP↓<STCalWB SWB TWB>success"
        using C6
      by blast
    thus "TP↓<TWB>success"
        using STCalWB_hasBarbST
      by blast
  qed
  moreover from C2 C7 have "rel_reflects_divergence TRel Target"
      using STCal_divergent(2)
    by blast
  ultimately show "strongly_operational_corresponding TRel ∧ preorder TRel
   ∧ strong_reduction_bisimulation TRel Target
   ∧ enc_respects_barb_set {success} ∧ rel_respects_barb_set TRel TWB {success}
   ∧ enc_reflects_divergence ∧ rel_reflects_divergence TRel Target"
    by fast
qed

subsection ‹Full Abstraction and Operational Correspondence›

text ‹To combine full abstraction and operational correspondence we consider a symmetric version
        of the induced relation and assume that the relations SRel and TRel are equivalences. Then
        an encoding is fully abstract w.r.t. SRel and TRel and operationally corresponding w.r.t.
        TRel such that TRel is a bisimulation iff the induced relation contains both SRel and TRel
        and is a transitive bisimulation.›

lemma (in encoding) FS_OC_modulo_equivalences_iff_source_target_relation:
  fixes SRel :: "('procS × 'procS) set"
    and TRel :: "('procT × 'procT) set"
  assumes eqS: "equivalence SRel"
      and eqT: "equivalence TRel"
  shows "fully_abstract SRel TRel
         ∧ operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target
         ⟷ (∃Rel.
         (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
         ∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
         ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
         ∧ trans Rel ∧ weak_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE, erule conjE)
  assume A1: "fully_abstract SRel TRel" and A2: "operational_corresponding TRel"
     and A3: "weak_reduction_bisimulation TRel Target"
  from eqT have A4: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding equiv_def refl_on_def
    by auto
  have A5:
   "∀S. SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧) ∧ TargetTerm (⟦S⟧) ∼⟦⋅⟧T<TRel> SourceTerm S"
    by (simp add: indRelTEQ.encR indRelTEQ.encL)
  moreover from A4 have A6: "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 A7: "trans (indRelTEQ TRel)"
      using indRelTEQ.trans[where TRel="TRel"]
      unfolding trans_def
    by blast
  moreover have "SRel = {(S1, S2). SourceTerm S1 ∼⟦⋅⟧T<TRel> SourceTerm S2}"
  proof -
    from A6 have "∀S1 S2. ((⟦S1⟧, ⟦S2⟧) ∈ TRel) = TargetTerm (⟦S1⟧) ∼⟦⋅⟧T<TRel> TargetTerm (⟦S2⟧)"
      by blast
    moreover have "indRelTEQ TRel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} = indRelTEQ TRel"
      by (auto simp add: indRelTEQ.encL)
    with A7 have "trans (indRelTEQ TRel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
        unfolding trans_def
      by blast
    ultimately show "SRel = {(S1, S2). SourceTerm S1 ∼⟦⋅⟧T<TRel> SourceTerm S2}"
        using A1 A5 full_abstraction_and_trans_relation_contains_TRel_impl_SRel[where
                    SRel="SRel" and TRel="TRel" and Rel="indRelTEQ TRel"]
      by blast
  qed
  moreover from eqT A2 A3 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)
         ∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ 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)
    ∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
    ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}
    ∧ trans Rel ∧ weak_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where
       B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
   and B2: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
   and B3: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}"
   and B4: "trans Rel" and B5: "weak_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  from B1 B2 B3 B4 have "fully_abstract SRel TRel"
      using trans_source_target_relation_impl_fully_abstract[where Rel="Rel" and SRel="SRel"
            and TRel="TRel"]
    by blast
  moreover have "operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
  proof -
    from eqT have C1: "TRel⇧+ = TRel"
        using trancl_id[of TRel]
        unfolding equiv_def
      by blast
    from eqT have C2: "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    from B1 have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover from B3 have "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
      by simp
    moreover from B3 C1 have "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
      by simp
    moreover have "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    proof clarify
      fix S T
      from B1 have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
        by simp
      moreover assume "(SourceTerm S, TargetTerm T) ∈ Rel"
      ultimately have "(TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel"
          using B4
          unfolding trans_def
        by blast
      with B3 C2 show "(⟦S⟧, T) ∈ TRel⇧*"
        by simp
    qed
    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 B5
         by blast
    with C1 C2 show "operational_corresponding TRel ∧ weak_reduction_bisimulation TRel Target"
        using OC_iff_weak_reduction_bisimulation[where TRel="TRel"]
      by auto
  qed
  ultimately show "fully_abstract SRel TRel ∧ operational_corresponding TRel
                   ∧ weak_reduction_bisimulation TRel Target"
    by simp
qed

lemma (in encoding) FA_SOC_modulo_equivalences_iff_source_target_relation:
  fixes SRel :: "('procS × 'procS) set"
    and TRel :: "('procT × 'procT) set"
  assumes eqS: "equivalence SRel"
      and eqT: "equivalence TRel"
  shows "fully_abstract SRel TRel ∧ strongly_operational_corresponding TRel
         ∧ strong_reduction_bisimulation TRel Target ⟷ (∃Rel.
         (∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel)
         ∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
         ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel} ∧ trans Rel
         ∧ strong_reduction_bisimulation Rel (STCal Source Target))"
proof (rule iffI, erule conjE, erule conjE)
  assume A1: "fully_abstract SRel TRel" and A2: "strongly_operational_corresponding TRel"
     and A3: "strong_reduction_bisimulation TRel Target"
  from eqT have A4: "TRel⇧* = TRel"
      using reflcl_trancl[of TRel] trancl_id[of TRel]
      unfolding equiv_def refl_on_def
    by auto
  have A5:
   "∀S. SourceTerm S ∼⟦⋅⟧T<TRel> TargetTerm (⟦S⟧) ∧ TargetTerm (⟦S⟧) ∼⟦⋅⟧T<TRel> SourceTerm S"
    by (simp add: indRelTEQ.encR indRelTEQ.encL)
  moreover from A4 have A6: "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 A7: "trans (indRelTEQ TRel)"
      using indRelTEQ.trans[where TRel="TRel"]
      unfolding trans_def
    by blast
  moreover have "SRel = {(S1, S2). SourceTerm S1 ∼⟦⋅⟧T<TRel> SourceTerm S2}"
  proof -
    from A6 have "∀S1 S2. ((⟦S1⟧, ⟦S2⟧) ∈ TRel) = TargetTerm (⟦S1⟧) ∼⟦⋅⟧T<TRel> TargetTerm (⟦S2⟧)"
      by blast
    moreover have "indRelTEQ TRel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q} = indRelTEQ TRel"
      by (auto simp add: indRelTEQ.encL)
    with A7 have "trans (indRelTEQ TRel ∪ {(P, Q). ∃S. ⟦S⟧ ∈T P ∧ S ∈S Q})"
        unfolding trans_def
      by blast
    ultimately show "SRel = {(S1, S2). SourceTerm S1 ∼⟦⋅⟧T<TRel> SourceTerm S2}"
        using A1 A5 full_abstraction_and_trans_relation_contains_TRel_impl_SRel[where
                    SRel="SRel" and TRel="TRel" and Rel="indRelTEQ TRel"]
      by blast
  qed
  moreover from eqT A2 A3 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)
         ∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ 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)
    ∧ SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}
    ∧ TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel} ∧ trans Rel
    ∧ strong_reduction_bisimulation Rel (STCal Source Target)"
  from this obtain Rel where
       B1: "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel ∧ (TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
   and B2: "SRel = {(S1, S2). (SourceTerm S1, SourceTerm S2) ∈ Rel}"
   and B3: "TRel = {(T1, T2). (TargetTerm T1, TargetTerm T2) ∈ Rel}" and B4: "trans Rel"
   and B5: "strong_reduction_bisimulation Rel (STCal Source Target)"
    by blast
  from B1 B2 B3 B4 have "fully_abstract SRel TRel"
      using trans_source_target_relation_impl_fully_abstract[where Rel="Rel" and SRel="SRel"
            and TRel="TRel"]
    by blast
  moreover
  have "strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target"
  proof -
    from eqT have C1: "TRel⇧+ = TRel"
        using trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by blast
    from eqT have C2: "TRel⇧* = TRel"
        using reflcl_trancl[of TRel] trancl_id[of TRel]
        unfolding equiv_def refl_on_def
      by auto
    from B1 have "∀S. (SourceTerm S, TargetTerm (⟦S⟧)) ∈ Rel"
      by simp
    moreover from B3 have "∀T1 T2. (T1, T2) ∈ TRel ⟶ (TargetTerm T1, TargetTerm T2) ∈ Rel"
      by simp
    moreover from B3 C1
    have "∀T1 T2. (TargetTerm T1, TargetTerm T2) ∈ Rel ⟶ (T1, T2) ∈ TRel⇧+"
      by simp
    moreover have "∀S T. (SourceTerm S, TargetTerm T) ∈ Rel ⟶ (⟦S⟧, T) ∈ TRel⇧*"
    proof clarify
      fix S T
      from B1 have "(TargetTerm (⟦S⟧), SourceTerm S) ∈ Rel"
        by simp
      moreover assume "(SourceTerm S, TargetTerm T) ∈ Rel"
      ultimately have "(TargetTerm (⟦S⟧), TargetTerm T) ∈ Rel"
          using B4
          unfolding trans_def
        by blast
      with B3 C2 show "(⟦S⟧, T) ∈ TRel⇧*"
        by simp
    qed
    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 B5
         by blast
    with C1 C2
    show "strongly_operational_corresponding TRel ∧ strong_reduction_bisimulation TRel Target"
        using SOC_iff_strong_reduction_bisimulation[where TRel="TRel"]
      by auto
  qed
  ultimately show "fully_abstract SRel TRel ∧ strongly_operational_corresponding TRel
                   ∧ strong_reduction_bisimulation TRel Target"
    by simp
qed

text ‹An encoding that is fully abstract w.r.t. the equivalences SRel and TRel and operationally
        corresponding w.r.t. TRel ensures that SRel is a bisimulation iff TRel is a bisimulation.
›

lemma (in encoding) FA_and_OC_and_TRel_impl_SRel_bisimulation:
  fixes SRel :: "('procS × 'procS) set"
    and TRel :: "('procT × 'procT) set"
  assumes fullAbs: "fully_abstract SRel TRel"
      and opCom:   "operational_complete TRel"
      and opSou:   "operational_sound TRel"
      and symmT:   "sym TRel"
      and transT:  "trans TRel"
      and bisimT:  "weak_reduction_bisimulation TRel Target"
  shows "weak_reduction_bisimulation SRel Source"
proof auto
  fix SP SQ SP'
  assume "SP ⟼Source* SP'"
  with opCom obtain TP' where A1: "⟦SP⟧ ⟼Target* TP'" and A2: "(⟦SP'⟧, TP') ∈ TRel"
    by blast
  assume "(SP, SQ) ∈ SRel"
  with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
    by simp
  with bisimT A1 obtain TQ' where A3: "⟦SQ⟧ ⟼Target* TQ'" and A4: "(TP', TQ') ∈ TRel"
    by blast
  from A3 opSou obtain SQ' where A5: "SQ ⟼Source* SQ'" and A6: "(⟦SQ'⟧, TQ') ∈ TRel"
    by blast
  from A2 A4 A6 symmT transT have "(⟦SP'⟧, ⟦SQ'⟧) ∈ TRel"
      unfolding trans_def sym_def
    by blast
  with fullAbs A5 show "∃SQ'. SQ ⟼Source* SQ' ∧ (SP', SQ') ∈ SRel"
    by blast
next
  fix SP SQ SQ'
  assume "SQ ⟼Source* SQ'"
  with opCom obtain TQ' where B1: "⟦SQ⟧ ⟼Target* TQ'" and B2: "(⟦SQ'⟧, TQ') ∈ TRel"
    by blast
  assume "(SP, SQ) ∈ SRel"
  with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
    by simp
  with bisimT B1 obtain TP' where B3: "⟦SP⟧ ⟼Target* TP'" and B4: "(TP', TQ') ∈ TRel"
    by blast
  from B3 opSou obtain SP' where B5: "SP ⟼Source* SP'" and B6: "(⟦SP'⟧, TP') ∈ TRel"
    by blast
  from B2 B4 B6 symmT transT have "(⟦SP'⟧, ⟦SQ'⟧) ∈ TRel"
      unfolding trans_def sym_def
    by blast
  with fullAbs B5 show "∃SP'. SP ⟼Source* SP' ∧ (SP', SQ') ∈ SRel"
    by blast
qed

lemma (in encoding) FA_and_SOC_and_TRel_impl_SRel_strong_bisimulation:
  fixes SRel :: "('procS × 'procS) set"
    and TRel :: "('procT × 'procT) set"
  assumes fullAbs: "fully_abstract SRel TRel"
      and opCom:   "strongly_operational_complete TRel"
      and opSou:   "strongly_operational_sound TRel"
      and symmT:   "sym TRel"
      and transT:  "trans TRel"
      and bisimT:  "strong_reduction_bisimulation TRel Target"
  shows "strong_reduction_bisimulation SRel Source"
proof auto
  fix SP SQ SP'
  assume "SP ⟼Source SP'"
  with opCom obtain TP' where A1: "⟦SP⟧ ⟼Target TP'" and A2: "(⟦SP'⟧, TP') ∈ TRel"
    by blast
  assume "(SP, SQ) ∈ SRel"
  with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
    by simp
  with bisimT A1 obtain TQ' where A3: "⟦SQ⟧ ⟼Target TQ'" and A4: "(TP', TQ') ∈ TRel"
    by blast
  from A3 opSou obtain SQ' where A5: "SQ ⟼Source SQ'" and A6: "(⟦SQ'⟧, TQ') ∈ TRel"
    by blast
  from A2 A4 A6 symmT transT have "(⟦SP'⟧, ⟦SQ'⟧) ∈ TRel"
      unfolding trans_def sym_def
    by blast
  with fullAbs A5 show "∃SQ'. SQ ⟼Source SQ' ∧ (SP', SQ') ∈ SRel"
    by blast
next
  fix SP SQ SQ'
  assume "SQ ⟼Source SQ'"
  with opCom obtain TQ' where B1: "⟦SQ⟧ ⟼Target TQ'" and B2: "(⟦SQ'⟧, TQ') ∈ TRel"
    by blast
  assume "(SP, SQ) ∈ SRel"
  with fullAbs have "(⟦SP⟧, ⟦SQ⟧) ∈ TRel"
    by simp
  with bisimT B1 obtain TP' where B3: "⟦SP⟧ ⟼Target TP'" and B4: "(TP', TQ') ∈ TRel"
    by blast
  from B3 opSou obtain SP' where B5: "SP ⟼Source SP'" and B6: "(⟦SP'⟧, TP') ∈ TRel"
    by blast
  from B2 B4 B6 symmT transT have "(⟦SP'⟧, ⟦SQ'⟧) ∈ TRel"
      unfolding trans_def sym_def
    by blast
  with fullAbs B5 show "∃SP'. SP ⟼Source SP' ∧ (SP', SQ') ∈ SRel"
    by blast
qed

lemma (in encoding) FA_and_OC_impl_SRel_iff_TRel_bisimulation:
  fixes SRel :: "('procS × 'procS) set"
    and TRel :: "('procT × 'procT) set"
  assumes fullAbs: "fully_abstract SRel TRel"
      and opCor:   "operational_corresponding TRel"
      and symmT:   "sym TRel"
      and transT:  "trans TRel"
      and surj:    "∀T. ∃S. T = ⟦S⟧"
  shows "weak_reduction_bisimulation SRel Source ⟷ weak_reduction_bisimulation TRel Target"
proof
  assume bisimS: "weak_reduction_bisimulation SRel Source"
  have "weak_reduction_simulation TRel Target"
  proof clarify
    fix TP TQ TP'
    from surj have "∃S. TP = ⟦S⟧"
      by simp
    from this obtain SP where A1: "⟦SP⟧ = TP"
      by blast
    from surj have "∃S. TQ = ⟦S⟧"
      by simp
    from this obtain SQ where A2: "⟦SQ⟧ = TQ"
      by blast
    assume "TP ⟼Target* TP'"
    with opCor A1 obtain SP' where A3: "SP ⟼Source* SP'" and A4: "(⟦SP'⟧, TP') ∈ TRel"
      by blast
    assume "(TP, TQ) ∈ TRel"
    with fullAbs A1 A2 have "(SP, SQ) ∈ SRel"
      by simp
    with bisimS A3 obtain SQ' where A5: "SQ ⟼Source* SQ'" and A6: "(SP', SQ') ∈ SRel"
      by blast
    from opCor A2 A5 obtain TQ' where A7: "TQ ⟼Target* TQ'" and A8: "(⟦SQ'⟧, TQ') ∈ TRel"
      by blast
    from symmT A4 have "(TP', ⟦SP'⟧) ∈ TRel"
        unfolding sym_def
      by simp
    moreover from fullAbs A6 have "(⟦SP'⟧, ⟦SQ'⟧) ∈ TRel"
      by simp
    ultimately have "(TP', TQ') ∈ TRel"
        using transT A8
        unfolding trans_def
      by blast
    with A7 show "∃TQ'. TQ ⟼Target* TQ' ∧ (TP', TQ') ∈ TRel"
      by blast
  qed
  with symmT show "weak_reduction_bisimulation TRel Target"
      using symm_weak_reduction_simulation_is_bisimulation[where Rel="TRel" and Cal="Target"]
    by blast
next
  assume "weak_reduction_bisimulation TRel Target"
  with fullAbs opCor symmT transT show "weak_reduction_bisimulation SRel Source"
      using FA_and_OC_and_TRel_impl_SRel_bisimulation[where SRel="SRel" and TRel="TRel"]
    by blast
qed

end