Theory Strong_Late_Sim_SC

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Strong_Late_Sim_SC
  imports Strong_Late_Sim
begin

(************** Zero **********************)

lemma nilSim[dest]:
  fixes a :: name
  and   b :: name
  and   x :: name
  and   P :: pi
  and   Q :: pi

  shows "𝟬 ↝[Rel] τ.(P) ⟹ False"
  and   "𝟬 ↝[Rel] a<x>.P ⟹ False"
  and   "𝟬 ↝[Rel] a{b}.P ⟹ False"
by(fastforce simp add: simulation_def intro: Tau Input Output)+

lemma nilSimRight:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  shows "P ↝[Rel] 𝟬"
by(auto simp add: simulation_def)

(************** Match *********************)

lemma matchIdLeft:
  fixes a   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes "Id ⊆ Rel"

  shows "[a⌢a]P ↝[Rel] P"
using assms
by(force simp add: simulation_def dest: Match derivativeReflexive)

lemma matchIdRight:
  fixes P   :: pi
  and   a   :: name
  and   Rel :: "(pi × pi) set"

  assumes IdRel: "Id ⊆ Rel"

  shows "P ↝[Rel] [a⌢a]P"
using assms
by(fastforce simp add: simulation_def elim: matchCases intro: derivativeReflexive)

lemma matchNilLeft:
  fixes a :: name
  and   b :: name
  and   P :: pi

  assumes "a ≠ b"
  
  shows "𝟬 ↝[Rel] [a⌢b]P"
using assms
by(auto simp add: simulation_def)

(************** Mismatch *********************)

lemma mismatchIdLeft:
  fixes a   :: name
  and   b   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes "Id ⊆ Rel"
  and     "a ≠ b"

  shows "[a≠b]P ↝[Rel] P"
using assms
by(fastforce simp add: simulation_def intro: Mismatch dest: derivativeReflexive)

lemma mismatchIdRight:
  fixes P   :: pi
  and   a   :: name
  and   b   :: name
  and   Rel :: "(pi × pi) set"

  assumes IdRel: "Id ⊆ Rel"
  and     aineqb: "a ≠ b"

  shows "P ↝[Rel] [a≠b]P"
using assms
by(fastforce simp add: simulation_def elim: mismatchCases intro: derivativeReflexive)

lemma mismatchNilLeft:
  fixes a :: name
  and   P :: pi
  
  shows "𝟬 ↝[Rel] [a≠a]P"
by(auto simp add: simulation_def)

(************** +-operator *****************)

lemma sumSym:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id: "Id ⊆ Rel"
  
  shows "P ⊕ Q ↝[Rel] Q ⊕ P"
using assms
by(fastforce simp add: simulation_def elim: sumCases intro: Sum1 Sum2 derivativeReflexive)

lemma sumIdempLeft:
  fixes P :: pi
  and Rel :: "(pi × pi) set"

  assumes "Id ⊆ Rel"

  shows "P ↝[Rel] P ⊕ P"
using assms
by(fastforce simp add: simulation_def elim: sumCases intro: derivativeReflexive)

lemma sumIdempRight:
  fixes P :: pi
  and Rel :: "(pi × pi) set"

  assumes I: "Id ⊆ Rel"

  shows "P ⊕ P ↝[Rel] P"
using assms
by(fastforce simp add: simulation_def intro: Sum1 derivativeReflexive)

lemma sumAssocLeft:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id: "Id ⊆ Rel"

  shows "(P ⊕ Q) ⊕ R ↝[Rel] P ⊕ (Q ⊕ R)"
using assms
by(fastforce simp add: simulation_def elim: sumCases intro: Sum1 Sum2 derivativeReflexive)

lemma sumAssocRight:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id: "Id ⊆ Rel"

  shows "P ⊕ (Q ⊕ R) ↝[Rel] (P ⊕ Q) ⊕ R"
using assms
by(fastforce simp add: simulation_def elim: sumCases intro: Sum1 Sum2 derivativeReflexive)

lemma sumZeroLeft:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id: "Id ⊆ Rel"

  shows "P ⊕ 𝟬 ↝[Rel] P"
using assms
by(fastforce simp add: simulation_def intro: Sum1 derivativeReflexive)

lemma sumZeroRight:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id: "Id ⊆ Rel"

  shows "P ↝[Rel] P ⊕ 𝟬"
using assms
by(fastforce simp add: simulation_def elim: sumCases intro: derivativeReflexive)

lemma sumResLeft:
  fixes x   :: name
  and   P   :: pi
  and   Q   :: pi

  assumes Id: "Id ⊆ Rel"
  and     Eqvt: "eqvt Rel"

  shows "(<νx>P) ⊕ (<νx>Q) ↝[Rel] <νx>(P ⊕ Q)"
using Eqvt
proof(induct rule: simCasesCont[where C="(x, P, Q)"])
  case(Bound a y PQ)
  from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by(simp add: fresh_prod)+
  hence "y ♯ P ⊕ Q" by simp
  with ‹<νx>(P ⊕ Q) ⟼a«y» ≺ PQ› ‹y ≠ x› show ?case
  proof(induct rule: resCasesB)
    case(cOpen a PQ)
    from ‹P ⊕ Q ⟼a[x] ≺ PQ› ‹y ♯ P› ‹y ♯ Q› have "y ♯ PQ" by(force dest: freshFreeDerivative)
    from ‹P ⊕ Q ⟼a[x] ≺ PQ› show ?case
    proof(induct rule: sumCases)
      case cSum1
      from ‹P ⟼a[x] ≺ PQ› ‹a ≠ x› have "<νx>P ⟼a<νx> ≺ PQ" by(rule Open)
      hence "(<νx>P) ⊕ (<νx>Q) ⟼a<νx> ≺ PQ" by(rule Sum1)
      with ‹y ♯ PQ› have "(<νx>P) ⊕ (<νx>Q) ⟼a<νy> ≺ ([(y, x)] ∙ PQ)" 
        by(simp add: alphaBoundResidual)
      moreover from Id have "derivative ([(y, x)] ∙ PQ) ([(y, x)] ∙ PQ) (BoundOutputS a) y Rel"
        by(force simp add: derivative_def)
      ultimately show ?case by blast
    next
      case cSum2
      from ‹Q ⟼a[x] ≺ PQ› ‹a ≠ x› have "<νx>Q ⟼a<νx> ≺ PQ" by(rule Open)
      hence "(<νx>P) ⊕ (<νx>Q) ⟼a<νx> ≺ PQ" by(rule Sum2)
      with ‹y ♯ PQ› have "(<νx>P) ⊕ (<νx>Q) ⟼a<νy> ≺ ([(y, x)] ∙ PQ)" 
        by(simp add: alphaBoundResidual)
      moreover from Id have "derivative ([(y, x)] ∙ PQ) ([(y, x)] ∙ PQ) (BoundOutputS a) y Rel"
        by(force simp add: derivative_def)
      ultimately show ?case by blast
    qed
  next
    case(cRes PQ)
    from ‹P ⊕ Q ⟼a«y» ≺ PQ› show ?case
    proof(induct rule: sumCases)
      case cSum1
      from ‹P ⟼a«y» ≺ PQ› ‹x ♯ a› ‹y ≠ x› have "<νx>P ⟼a«y» ≺ <νx>PQ" by(rule_tac ResB) auto
      hence "(<νx>P) ⊕ (<νx>Q) ⟼a«y» ≺ <νx>PQ" by(rule Sum1)
      moreover from Id have "derivative (<νx>PQ) (<νx>PQ) a y Rel"
        by(cases a) (auto simp add: derivative_def)
      ultimately show ?case by blast
    next
      case cSum2
      from ‹Q ⟼a«y» ≺ PQ› ‹x ♯ a› ‹y ≠ x› have "<νx>Q ⟼a«y» ≺ <νx>PQ" by(rule_tac ResB) auto
      hence "(<νx>P) ⊕ (<νx>Q) ⟼a«y» ≺ <νx>PQ" by(rule Sum2)
      moreover from Id have "derivative (<νx>PQ) (<νx>PQ) a y Rel"
        by(cases a) (auto simp add: derivative_def)
      ultimately show ?case by blast
    qed
  qed
next
  case(Free α PQ)
  from ‹<νx>(P ⊕ Q) ⟼α ≺ PQ› show ?case
  proof(induct rule: resCasesF)
    case(cRes PQ)
    from ‹P ⊕ Q ⟼α ≺ PQ› show ?case
    proof(induct rule: sumCases)
      case cSum1 
      from ‹P ⟼α ≺ PQ› ‹x ♯ α› have "<νx>P ⟼α ≺ <νx>PQ" by(rule ResF)
      hence "(<νx>P) ⊕ (<νx>Q) ⟼α ≺ <νx>PQ" by(rule Sum1)
      with Id show ?case by blast
    next
      case cSum2
      from ‹Q ⟼α ≺ PQ› ‹x ♯ α› have "<νx>Q ⟼α ≺ <νx>PQ" by(rule ResF)
      hence "(<νx>P) ⊕ (<νx>Q) ⟼α ≺ <νx>PQ" by(rule Sum2)
      with Id show ?case by blast
    qed
  qed
qed

lemma sumResRight:
  fixes x   :: name
  and   P   :: pi
  and   Q   :: pi

  assumes Id: "Id ⊆ Rel"
  and     Eqvt: "eqvt Rel"

  shows "<νx>(P ⊕ Q) ↝[Rel] (<νx>P) ⊕ (<νx>Q)"
using ‹eqvt Rel›
proof(induct rule: simCasesCont[where C="(x, P, Q)"])
  case(Bound a y PQ)
  from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by(simp add: fresh_prod)+
  from ‹(<νx>P) ⊕ (<νx>Q) ⟼a«y» ≺ PQ› show ?case
  proof(induct rule: sumCases)
    case cSum1
    from ‹<νx>P ⟼a«y» ≺ PQ› show ?case using ‹y ≠ x› ‹y ♯ P›
    proof(induct rule: resCasesB)
      case(cOpen a P')
      from ‹P ⟼a[x] ≺ P'› ‹y ♯ P› have "y ♯ P'" by(rule freshFreeDerivative)
      
      from ‹P ⟼a[x] ≺ P'› have "P ⊕ Q ⟼a[x] ≺ P'" by(rule Sum1)
      hence "<νx>(P ⊕ Q) ⟼a<νx> ≺ P'" using ‹a ≠ x› by(rule Open)
      with ‹y ♯ P'› have "<νx>(P ⊕ Q) ⟼a<νy> ≺ [(y, x)] ∙ P'" by(simp add: alphaBoundResidual)
      moreover from Id have "derivative ([(y, x)] ∙ P') ([(y, x)] ∙ P') (BoundOutputS a) y Rel"
        by(force simp add: derivative_def)
      ultimately show ?case by blast
    next
      case(cRes P')
      from ‹P ⟼a«y» ≺ P'› have "P ⊕ Q ⟼a«y» ≺ P'" by(rule Sum1)
      hence "<νx>(P ⊕ Q) ⟼a«y» ≺ <νx>P'" using ‹x ♯ a› ‹y ≠ x› by(rule_tac ResB) auto
      moreover from Id have "derivative (<νx>P') (<νx>P') a y Rel"
        by(cases a) (auto simp add: derivative_def)
      ultimately show ?case by blast
    qed
  next
    case cSum2
    from ‹<νx>Q ⟼a«y» ≺ PQ› show ?case using ‹y ≠ x› ‹y ♯ Q›
    proof(induct rule: resCasesB)
      case(cOpen a Q')
      from ‹Q ⟼a[x] ≺ Q'› ‹y ♯ Q› have "y ♯ Q'" by(rule freshFreeDerivative)
      
      from ‹Q ⟼a[x] ≺ Q'› have "P ⊕ Q ⟼a[x] ≺ Q'" by(rule Sum2)
      hence "<νx>(P ⊕ Q) ⟼a<νx> ≺ Q'" using ‹a ≠ x› by(rule Open)
      with ‹y ♯ Q'› have "<νx>(P ⊕ Q) ⟼a<νy> ≺ [(y, x)] ∙ Q'" by(simp add: alphaBoundResidual)
      moreover from Id have "derivative ([(y, x)] ∙ Q') ([(y, x)] ∙ Q') (BoundOutputS a) y Rel"
        by(force simp add: derivative_def)
      ultimately show ?case by blast
    next
      case(cRes Q')
      from ‹Q ⟼a«y» ≺ Q'› have "P ⊕ Q ⟼a«y» ≺ Q'" by(rule Sum2)
      hence "<νx>(P ⊕ Q) ⟼a«y» ≺ <νx>Q'" using ‹x ♯ a› ‹y ≠ x› by(rule_tac ResB) auto
      moreover from Id have "derivative (<νx>Q') (<νx>Q') a y Rel"
        by(cases a) (auto simp add: derivative_def)
      ultimately show ?case by blast
    qed
  qed
next
  case(Free α PQ)
  from ‹(<νx>P) ⊕ (<νx>Q) ⟼α ≺ PQ› show ?case
  proof(induct rule: sumCases)
    case cSum1
    from ‹<νx>P ⟼α ≺ PQ› show ?case
    proof(induct rule: resCasesF)
      case(cRes P')
      from ‹P ⟼α ≺ P'› have "P ⊕ Q ⟼α ≺ P'" by(rule Sum1)
      hence "<νx>(P ⊕ Q) ⟼α ≺ <νx>P'" using ‹x ♯ α› by(rule ResF)
      with Id show ?case by blast
    qed
  next
    case cSum2
    from ‹<νx>Q ⟼α ≺ PQ› show ?case
    proof(induct rule: resCasesF)
      case(cRes Q')
      from ‹Q ⟼α ≺ Q'› have "P ⊕ Q ⟼α ≺ Q'" by(rule Sum2)
      hence "<νx>(P ⊕ Q) ⟼α ≺ <νx>Q'" using ‹x ♯ α› by(rule ResF)
      with Id show ?case by blast
    qed
  qed
qed

(************** |-operator *************)

lemma parZeroLeft:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes ParZero: "⋀Q. (Q ∥ 𝟬, Q) ∈ Rel"

  shows "P ∥ 𝟬 ↝[Rel] P"
proof -
  {
    fix P Q a x
    from ParZero have "derivative (P ∥ 𝟬) P a x Rel"
      by(case_tac a) (auto simp add: derivative_def)
  }
  thus ?thesis using assms
    by(fastforce simp add: simulation_def intro: Par1B Par1F)
qed

lemma parZeroRight:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes ParZero: "⋀Q. (Q, Q ∥ 𝟬) ∈ Rel"

  shows "P ↝[Rel] P ∥ 𝟬"
proof -
  {
    fix P Q a x
    from ParZero have "derivative P (P ∥ 𝟬) a x Rel"
      by(case_tac a) (auto simp add: derivative_def)
  }
  thus ?thesis using assms
    by(fastforce simp add: simulation_def elim: parCasesF parCasesB)+
qed
  
lemma parSym:
  fixes P    :: pi
  and   Q    :: pi
  and   Rel  :: "(pi × pi) set"
  
  assumes Sym: "⋀R S. (R ∥ S, S ∥ R) ∈ Rel"
  and     Res: "⋀R S x. (R, S) ∈ Rel ⟹ (<νx>R, <νx>S) ∈ Rel"
  
  shows "P ∥ Q ↝[Rel] Q ∥ P"
proof(induct rule: simCases)
  case(Bound a x QP)
  from ‹x ♯ (P ∥ Q)› have "x ♯ Q" and "x ♯ P" by simp+
  with ‹Q ∥ P ⟼ a«x» ≺ QP› show ?case
  proof(induct rule: parCasesB)
    case(cPar1 Q')
    from ‹Q ⟼a«x» ≺ Q'› have "P ∥ Q ⟼a«x» ≺ P ∥ Q'" using ‹x ♯ P› by(rule Par2B)
    moreover have "derivative (P ∥ Q')  (Q' ∥ P) a x Rel"
      by(cases a, auto simp add: derivative_def intro: Sym)
    ultimately show ?case by blast
  next
    case(cPar2 P')
    from ‹P ⟼a«x» ≺ P'› have "P ∥ Q ⟼a«x» ≺ P' ∥ Q" using ‹x ♯ Q› by(rule Par1B)
    moreover have "derivative (P' ∥ Q)  (Q ∥ P') a x Rel"
      by(cases a, auto simp add: derivative_def intro: Sym)
    ultimately show ?case by blast
  qed
next
  case(Free α QP)
  from ‹Q ∥ P ⟼ α ≺ QP› show ?case
  proof(induct rule: parCasesF[where C="()"])
    case(cPar1 Q')
    from ‹Q ⟼ α ≺ Q'› have "P ∥ Q ⟼ α ≺ P ∥ Q'" by(rule Par2F)
    moreover have "(P ∥ Q', Q' ∥ P) ∈ Rel" by(rule Sym)
    ultimately show ?case by blast
  next
    case(cPar2 P')
    from ‹P ⟼ α ≺ P'› have "P ∥ Q ⟼ α ≺ P' ∥ Q" by(rule Par1F)
    moreover have "(P' ∥ Q, Q ∥ P') ∈ Rel" by(rule Sym)
    ultimately show ?case by blast
  next
    case(cComm1 Q' P' a b x)
    from ‹P ⟼a[b] ≺ P'› ‹Q ⟼a<x> ≺ Q'›
    have "P ∥ Q ⟼ τ ≺ P' ∥ (Q'[x::=b])" by(rule Comm2)
    moreover have "(P' ∥ Q'[x::=b], Q'[x::=b] ∥ P') ∈ Rel" by(rule Sym)
    ultimately show ?case by blast
  next
    case(cComm2 Q' P' a b x)
    from ‹P ⟼a<x> ≺ P'› ‹Q ⟼a[b] ≺ Q'›
    have "P ∥ Q ⟼ τ ≺ (P'[x::=b]) ∥ Q'" by(rule Comm1)
    moreover have "(P'[x::=b] ∥ Q', Q' ∥ P'[x::=b]) ∈ Rel" by(rule Sym)
    ultimately show ?case by blast
  next
    case(cClose1 Q' P' a x y)
    from ‹P ⟼ a<νy> ≺ P'› ‹Q ⟼ a<x> ≺ Q'› ‹y ♯ Q›
    have "P ∥ Q ⟼ τ ≺ <νy>(P' ∥ (Q'[x::=y]))" by(rule Close2)
    moreover have "(<νy>(P' ∥ Q'[x::=y]), <νy>(Q'[x::=y] ∥ P')) ∈ Rel" by(metis Res Sym)
    ultimately show ?case by blast
  next
    case(cClose2 Q' P' a x y)
    from ‹P ⟼ a<x> ≺ P'› ‹Q ⟼ a<νy> ≺ Q'› ‹y ♯ P›
    have "P ∥ Q ⟼ τ ≺ <νy>((P'[x::=y]) ∥ Q')" by(rule Close1)
    moreover have "(<νy>(P'[x::=y] ∥ Q'), <νy>(Q' ∥ P'[x::=y])) ∈ Rel" by(metis Res Sym)
    ultimately show ?case by blast
  qed
qed

lemma parAssocLeft:
  fixes P    :: pi
  and   Q    :: pi
  and   R    :: pi
  and   Rel  :: "(pi × pi) set"

  assumes Ass:       "⋀S T U. ((S ∥ T) ∥ U, S ∥ (T ∥ U)) ∈ Rel"
  and     Res:       "⋀S T x. (S, T) ∈ Rel ⟹ (<νx>S, <νx>T) ∈ Rel"
  and     FreshExt:  "⋀S T U x. x ♯ S ⟹ (<νx>((S ∥ T) ∥ U), S ∥ <νx>(T ∥ U)) ∈ Rel"
  and     FreshExt': "⋀S T U x. x ♯ U ⟹ ((<νx>(S ∥ T)) ∥ U, <νx>(S ∥ (T ∥ U))) ∈ Rel"

  shows "(P ∥ Q) ∥ R ↝[Rel] P ∥ (Q ∥ R)"
proof(induct rule: simCases)
  case(Bound a x PQR)
  from ‹x ♯ (P ∥ Q) ∥ R› have "x ♯ P" and "x ♯ Q" and "x ♯ R" by simp+
  hence "x ♯ (Q ∥ R)" by simp
  with ‹P ∥ (Q ∥ R) ⟼ a«x» ≺ PQR› ‹x ♯ P› show ?case
  proof(induct rule: parCasesB)
    case(cPar1 P')
    from ‹P ⟼ a«x» ≺ P'› have "P ∥ Q ⟼ a«x» ≺ P' ∥ Q" using ‹x ♯ Q› by(rule Par1B)
    hence "(P ∥ Q) ∥ R ⟼ a«x» ≺ (P' ∥ Q) ∥ R" using ‹x ♯ R› by(rule Par1B)
    moreover have "derivative ((P' ∥ Q) ∥ R) (P' ∥ (Q ∥ R)) a x Rel"
      by(cases a, auto intro: Ass simp add: derivative_def)
    ultimately show ?case by blast
  next
    case(cPar2 QR)
    from ‹Q ∥ R ⟼ a«x» ≺ QR› ‹x ♯ Q› ‹x ♯ R› show ?case
    proof(induct rule: parCasesB)
      case(cPar1 Q')
      from ‹Q ⟼ a«x» ≺ Q'› have "P ∥ Q ⟼ a«x» ≺ P ∥ Q'" using ‹x ♯ P› by(rule Par2B)
      hence "(P ∥ Q) ∥ R ⟼ a«x» ≺ (P ∥ Q') ∥ R" using ‹x ♯ R›by(rule Par1B)
      moreover have "derivative ((P ∥ Q') ∥ R) (P ∥ (Q' ∥ R)) a x Rel"
        by(cases a, auto intro: Ass simp add: derivative_def)
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹R ⟼ a«x» ≺ R'› have "(P ∥ Q) ∥ R ⟼ a«x» ≺ (P ∥ Q) ∥ R'" using ‹x ♯ P› ‹x ♯ Q› 
        by(rule_tac Par2B) auto
      moreover have "derivative ((P ∥ Q) ∥ R') (P ∥ (Q ∥ R')) a x Rel"
        by(cases a, auto intro: Ass simp add: derivative_def)
      ultimately show ?case by blast
    qed
  qed
next
  case(Free α PQR)
  from ‹P ∥ (Q ∥ R) ⟼ α ≺ PQR› show ?case
  proof(induct rule: parCasesF[where C="Q"])
    case(cPar1 P')
    from ‹P ⟼ α ≺ P'› have "P ∥ Q ⟼ α ≺ P' ∥ Q" by(rule Par1F)
    hence "(P ∥ Q) ∥ R ⟼ α ≺ (P' ∥ Q) ∥ R" by(rule Par1F)
    moreover from Ass have "((P' ∥ Q) ∥ R, P' ∥ (Q ∥ R)) ∈ Rel" by blast
    ultimately show ?case by blast
  next
    case(cPar2 QR)
    from ‹Q ∥ R ⟼ α ≺ QR› show ?case
    proof(induct rule: parCasesF[where C="P"])
      case(cPar1 Q')
      from ‹Q ⟼ α ≺ Q'› have "(P ∥ Q) ⟼ α ≺ P ∥ Q'" by(rule Par2F)
      hence "(P ∥ Q) ∥ R ⟼ α ≺ (P ∥ Q') ∥ R" by(rule Par1F)
      moreover from Ass have "((P ∥ Q') ∥ R, P ∥ (Q' ∥ R)) ∈ Rel" by blast
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹R ⟼ α ≺ R'› have "(P ∥ Q) ∥ R ⟼ α ≺ (P ∥ Q) ∥ R'" by(rule Par2F)
      moreover from Ass have "((P ∥ Q) ∥ R', P ∥ (Q ∥ R')) ∈ Rel" by blast
      ultimately show ?case by blast
    next
      case(cComm1 Q' R' a b x)
      from ‹Q ⟼a<x> ≺ Q'› ‹x ♯ P› have "P ∥ Q ⟼a<x> ≺ P ∥ Q'" by(rule Par2B)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P ∥ Q')[x::=b] ∥ R'" using ‹R ⟼a[b] ≺ R'› by(rule Comm1)
      with ‹x ♯ P› have "(P ∥ Q) ∥ R ⟼ τ ≺ (P ∥ (Q'[x::=b])) ∥ R'" by(simp add: forget)
      moreover from Ass have "((P ∥ (Q'[x::=b])) ∥ R', P ∥ (Q'[x::=b] ∥ R')) ∈ Rel" by blast
      ultimately show ?case by blast
    next
      case(cComm2 Q' R' a b x)
      from ‹Q ⟼a[b] ≺ Q'› have "P ∥ Q ⟼a[b] ≺ P ∥ Q'" by(rule Par2F)
      with ‹x ♯ P› ‹x ♯ Q› ‹R ⟼a<x> ≺ R'› have "(P ∥ Q) ∥ R ⟼ τ ≺ (P ∥ Q') ∥ R'[x::=b]"
        by(force intro: Comm2)
      moreover from Ass have "((P ∥ Q') ∥ R'[x::=b], P ∥ (Q' ∥ R'[x::=b])) ∈ Rel" by blast
      ultimately show ?case by blast
    next
      case(cClose1 Q' R' a x y)
      from ‹Q ⟼a<x> ≺ Q'› ‹x ♯ P› have "P ∥ Q ⟼a<x> ≺ P ∥ Q'" by(rule Par2B)
      with ‹y ♯ P› ‹y ♯ Q› ‹x ♯ P› ‹R ⟼a<νy> ≺ R'› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P ∥ Q')[x::=y] ∥ R')"
        by(rule_tac Close1) auto
      with ‹x ♯ P› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P ∥ (Q'[x::=y])) ∥ R')" by(simp add: forget)
      moreover from ‹y ♯ P› have "(<νy>((P ∥ Q'[x::=y]) ∥ R'), P ∥ <νy>(Q'[x::=y] ∥ R')) ∈ Rel"
        by(rule FreshExt)
      ultimately show ?case by blast
    next
      case(cClose2 Q' R' a x y)
      from ‹Q ⟼a<νy> ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼a<νy> ≺ P ∥ Q'" by(rule Par2B)
      hence Act: "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P ∥ Q') ∥ R'[x::=y])" using ‹R ⟼a<x> ≺ R'› ‹y ♯ R› by(rule Close2)
      moreover from ‹y ♯ P› have "(<νy>((P ∥ Q') ∥ R'[x::=y]), P ∥ <νy>(Q' ∥ R'[x::=y])) ∈ Rel"
        by(rule FreshExt)
      ultimately show ?case by blast
    qed
  next
    case(cComm1 P' QR a b x)
    from ‹Q ∥ R ⟼ a[b] ≺ QR› show ?case
    proof(induct rule: parCasesF[where C="()"])
      case(cPar1 Q')
      from ‹P ⟼a<x> ≺ P'› ‹Q ⟼a[b] ≺ Q'› have "P ∥ Q ⟼ τ ≺ P'[x::=b] ∥ Q'" by(rule Comm1)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P'[x::=b] ∥ Q') ∥ R" by(rule Par1F)
      moreover from Ass have "((P'[x::=b] ∥ Q') ∥ R, P'[x::=b] ∥ (Q' ∥ R)) ∈ Rel" by blast
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹P ⟼a<x> ≺ P'› ‹x ♯ Q› have "P ∥ Q ⟼ a<x> ≺ P' ∥ Q" by(rule Par1B)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P' ∥ Q)[x::=b] ∥ R'" using ‹R ⟼ a[b] ≺ R'› by(rule Comm1)
      with ‹x ♯ Q› have "(P ∥ Q) ∥ R ⟼ τ ≺ (P'[x::=b] ∥ Q) ∥ R'" by(simp add: forget)
      moreover from Ass have "((P'[x::=b] ∥ Q) ∥ R', P'[x::=b] ∥ (Q ∥ R')) ∈ Rel" by blast
      ultimately show ?case by blast
    next
      case(cComm1 Q' R')
      from ‹a[b] = τ› have False by simp thus ?case by simp
    next
      case(cComm2 Q' R')
      from ‹a[b] = τ› have False by simp thus ?case by simp
    next
      case(cClose1 Q' R')
      from ‹a[b] = τ› have False by simp thus ?case by simp
    next
      case(cClose2 Q' R')
      from ‹a[b] = τ› have False by simp thus ?case by simp
    qed
  next
    case(cComm2 P' QR a b x)
    from ‹x ♯ Q ∥ R› have "x ♯ Q" and "x ♯ R" by simp+
    with ‹Q ∥ R ⟼ a<x> ≺ QR› show ?case
    proof(induct rule: parCasesB)
      case(cPar1 Q')
      from ‹P ⟼a[b] ≺ P'› ‹Q ⟼ a<x> ≺ Q'› have "P ∥ Q ⟼ τ ≺ P' ∥ (Q'[x::=b])" by(rule Comm2)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P' ∥ Q'[x::=b]) ∥ R" by(rule Par1F)
      moreover from Ass have "((P' ∥ Q'[x::=b]) ∥ R, P' ∥ Q'[x::=b] ∥ R) ∈ Rel" by blast
      with ‹x ♯ R› have "((P' ∥ Q'[x::=b]) ∥ R, P' ∥ (Q' ∥ R)[x::=b]) ∈ Rel" by(force simp add: forget)
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹P ⟼a[b] ≺ P'› have "P ∥ Q ⟼ a[b] ≺ P' ∥ Q" by(rule Par1F)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (P' ∥ Q) ∥ (R'[x::=b])" using ‹R ⟼a<x> ≺ R'› by (rule Comm2)
      moreover from Ass have "((P' ∥ Q) ∥ R'[x::=b], P' ∥ Q ∥ (R'[x::=b])) ∈ Rel" by blast
      hence "((P' ∥ Q) ∥ R'[x::=b], P' ∥ (Q ∥ R')[x::=b]) ∈ Rel" using ‹x ♯ Q› by(force simp add: forget)
      ultimately show ?case by blast
    qed
  next
    case(cClose1 P' QR a x y)
    from ‹x ♯ Q ∥ R› have "x ♯ Q" by simp
    from ‹y ♯ Q ∥ R› have "y ♯ Q" and "y ♯ R" by simp+
    from ‹Q ∥ R ⟼ a<νy> ≺ QR› ‹y ♯ Q› ‹y ♯ R› show ?case
    proof(induct rule: parCasesB)
      case(cPar1 Q')
      from ‹P ⟼a<x> ≺ P'› ‹Q ⟼ a<νy> ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼ τ ≺ <νy>(P'[x::=y] ∥ Q')" by(rule Close1)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (<νy>(P'[x::=y] ∥ Q')) ∥ R" by(rule Par1F)
      moreover from ‹y ♯ R› have "((<νy>(P'[x::=y] ∥ Q')) ∥ R, <νy>(P'[x::=y] ∥ Q' ∥ R)) ∈ Rel"
        by(rule FreshExt')
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹P ⟼a<x> ≺ P'› ‹x ♯ Q› have "P ∥ Q ⟼ a<x> ≺ P' ∥ Q" by(rule Par1B)
      with ‹R ⟼ a<νy> ≺ R'› ‹y ♯ P› ‹y ♯ Q› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P' ∥ Q)[x::=y] ∥ R')"
        by(rule_tac Close1) auto
      with ‹x ♯ Q› have "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P'[x::=y] ∥ Q) ∥ R')" by(simp add: forget)
      moreover have "(<νy>((P'[x::=y] ∥ Q) ∥ R'), <νy>(P'[x::=y] ∥ (Q ∥ R'))) ∈ Rel" by(metis Ass Res)
      ultimately show ?case by blast
    qed
  next
    case(cClose2 P' QR a x y)
    from ‹y ♯ Q ∥ R› have "y ♯ Q" and "y ♯ R" by simp+
    from ‹x ♯ Q ∥ R› have "x ♯ Q" and "x ♯ R" by simp+
    with ‹Q ∥ R ⟼ a<x> ≺ QR› show ?case
    proof(induct rule: parCasesB)
      case(cPar1 Q')
      from ‹P ⟼a<νy> ≺ P'› ‹Q ⟼a<x> ≺ Q'› have "P ∥ Q ⟼ τ ≺ <νy>(P' ∥ Q'[x::=y])" using ‹y ♯ Q›
        by(rule Close2)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ (<νy>(P' ∥ Q'[x::=y])) ∥ R" by(rule Par1F)
      moreover from ‹y ♯ R› have "((<νy>(P' ∥ Q'[x::=y])) ∥ R, <νy>(P' ∥  (Q'[x::=y] ∥ R))) ∈ Rel"
        by(rule FreshExt')
      with ‹x ♯ R› have "((<νy>(P' ∥ Q'[x::=y])) ∥ R, <νy>(P' ∥  (Q' ∥ R)[x::=y])) ∈ Rel"
        by(simp add: forget)
      ultimately show ?case by blast
    next
      case(cPar2 R')
      from ‹P ⟼a<νy> ≺ P'› ‹y ♯ Q› have "P ∥ Q ⟼ a<νy> ≺ P' ∥ Q" by(rule Par1B)
      hence "(P ∥ Q) ∥ R ⟼ τ ≺ <νy>((P' ∥ Q) ∥ R'[x::=y])" using ‹R ⟼ a<x> ≺ R'› ‹y ♯ R› by(rule Close2)
      moreover have "((P' ∥ Q) ∥ R'[x::=y], P' ∥ (Q ∥ R'[x::=y])) ∈ Rel" by(rule Ass)
      hence "(<νy>((P' ∥ Q) ∥ R'[x::=y]), <νy>(P' ∥ (Q ∥ R'[x::=y]))) ∈ Rel" by(rule Res) 
      hence "(<νy>((P' ∥ Q) ∥ R'[x::=y]), <νy>(P' ∥ (Q ∥ R')[x::=y])) ∈ Rel" using ‹x ♯ Q›
        by(simp add: forget)
      ultimately show ?case by blast
    qed
  qed
qed

lemma substRes3:
  fixes a :: name
  and   P :: pi
  and   x :: name

  shows "(<νa>P)[x::=a] = <νx>([(x, a)] ∙ P)"
proof -
  have "a ♯ <νa>P" by(simp add: name_fresh_abs)
  hence "(<νa>P)[x::=a] = [(x, a)] ∙ <νa>P" by(rule injPermSubst[THEN sym])
  thus "(<νa>P)[x::=a] = <νx>([(x, a)] ∙ P)" by(simp add: name_calc)
qed

lemma scopeExtParLeft:
  fixes P   :: pi
  and   Q   :: pi
  and   a   :: name
  and   lst :: "name list"
  and   Rel :: "(pi × pi) set"

  assumes "x ♯ P"
  and     Id:         "Id ⊆ Rel"
  and     EqvtRel:    "eqvt Rel"
  and     Res:        "⋀R S y. y ♯ R ⟹ (<νy>(R ∥ S), R ∥ <νy>S) ∈ Rel"
  and     ScopeExt:   "⋀R S y z. y ♯ R ⟹ (<νy><νz>(R ∥ S), <νz>(R ∥ <νy>S)) ∈ Rel"

  shows "<νx>(P ∥ Q) ↝[Rel] P ∥ <νx>Q"
using ‹eqvt Rel›
proof(induct rule: simCasesCont[where C="(x, P, Q)"])
  case(Bound a y PxQ)
  from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by simp+
  hence "y ♯ P" and "y ♯ <νx>Q" by(simp add: abs_fresh)+
  with ‹P ∥ <νx>Q ⟼ a«y» ≺ PxQ› show ?case
  proof(induct rule: parCasesB)
    case(cPar1 P')
    from ‹P ⟼a«y» ≺ P'› ‹x ♯ P› ‹y ≠ x› have "x ♯ a" and "x ♯ P'"
      by(force intro: freshBoundDerivative)+

    from ‹P ⟼a«y» ≺ P'› ‹y ♯ Q› have "P ∥ Q ⟼a«y» ≺ P' ∥ Q" by(rule Par1B)
    with ‹x ♯ a› ‹y ≠ x› have "<νx>(P ∥ Q) ⟼ a«y» ≺ <νx>(P' ∥ Q)" by(rule_tac ResB) auto
    moreover have "derivative (<νx>(P' ∥ Q)) (P' ∥ <νx>Q) a y Rel"
    proof(cases a, auto simp add: derivative_def)
      fix u

      show "((<νx>(P' ∥ Q))[y::=u],  P'[y::=u] ∥  ((<νx>Q)[y::=u])) ∈ Rel"
      proof(cases "x=u")
        case True
        have "(<νx>(P' ∥ Q))[y::=x] = <νy>(([(y, x)] ∙ P') ∥ ([(y, x)] ∙ Q))"
          by(simp add: substRes3)
        moreover from ‹x ♯ P'› have "P'[y::=x] = [(y, x)] ∙ P'" by(rule injPermSubst[THEN sym])
        moreover have "(<νx>Q)[y::=x] = <νy>([(y, x)] ∙ Q)" by(rule substRes3)
        moreover from ‹x ♯ P'› ‹y ≠ x› have "y ♯ [(y, x)] ∙ P'" by(simp add: name_fresh_left name_calc)
        ultimately show ?thesis using ‹x = u›by(force intro: Res)
      next
        case False
        with ‹y ≠ x› have "(<νx>(P' ∥ Q))[y::=u] = <νx>(P'[y::=u] ∥ Q[y::=u])"
          by(simp add: fresh_prod name_fresh)
        moreover from ‹x ≠ u› ‹y ≠ x› have "(<νx>Q)[y::=u] = <νx>(Q[y::=u])"
          by(simp add: fresh_prod name_fresh)
        moreover from ‹x ♯ P'› ‹x ≠ u› have "x ♯ P'[y::=u]" by(simp add: fresh_fact1)
        ultimately show ?thesis by(force intro: Res)
      qed
    next
      from ‹x ♯ P'› show "(<νx>(P' ∥ Q), P' ∥ <νx>Q) ∈ Rel" by(rule Res)
    qed
    
    ultimately show ?case by blast
  next
    case(cPar2 xQ)
    from ‹<νx>Q ⟼a«y» ≺ xQ› ‹y ≠ x› ‹y ♯ Q› show ?case
    proof(induct rule: resCasesB)
      case(cOpen a Q')
      from ‹Q ⟼a[x] ≺ Q'› ‹y ♯ Q› have yFreshQ': "y ♯ Q'" by(force intro: freshFreeDerivative)

      from ‹Q ⟼ a[x] ≺ Q'› have "P ∥ Q ⟼ a[x] ≺ P ∥ Q'" by(rule Par2F)
      hence "<νx>(P ∥ Q) ⟼ a<νx> ≺ P ∥ Q'" using ‹a ≠ x› by(rule Open)
      with ‹y ♯ P› ‹y ♯ Q'› have "<νx>(P ∥ Q) ⟼ a<νy> ≺ [(x, y)] ∙ (P ∥ Q')"
        by(subst alphaBoundResidual[where x'=x]) (auto simp add: fresh_left calc_atm)
      with ‹y ♯ P› ‹x ♯ P› have "<νx>(P ∥ Q) ⟼ a<νy> ≺ P ∥ ([(x, y)] ∙ Q')"
        by(simp add: name_fresh_fresh)

      moreover have "derivative (P ∥ ([(x, y)] ∙ Q')) (P ∥ ([(y, x)] ∙ Q')) (BoundOutputS a) y Rel" using Id
        by(auto simp add: derivative_def name_swap)
         
      ultimately show ?case by blast
    next
      case(cRes Q')

      from ‹Q ⟼ a«y» ≺ Q'› ‹y ♯ P› have "P ∥ Q ⟼ a«y» ≺ P ∥ Q'" by(rule Par2B)
      hence "<νx>(P ∥ Q) ⟼ a«y» ≺ <νx>(P ∥ Q')" using ‹x ♯ a› ‹y ≠ x›
        by(rule_tac ResB) auto
      moreover have "derivative (<νx>(P ∥ Q')) (P ∥ <νx>Q') a y Rel"
      proof(cases a, auto simp add: derivative_def)
        fix u
        show "((<νx>(P ∥ Q'))[y::=u],  P[y::=u] ∥  (<νx>Q')[y::=u]) ∈ Rel"
        proof(cases "x=u")
          case True
          from ‹x ♯ P› ‹y ♯ P› have "(<νx>(P ∥ Q'))[y::=x] = <νy>(P ∥ ([(y, x)] ∙ Q'))"
            by(simp add: substRes3 perm_fresh_fresh)
          moreover from ‹y ♯ P› have "P[y::=x] = P" by(simp add: forget)
          moreover have "(<νx>Q')[y::=x] = <νy>([(y, x)] ∙ Q')" by(rule substRes3)
          ultimately show ?thesis using ‹x=u› ‹y ♯ P› by(force intro: Res)
        next
          case False
          with ‹y ≠ x› have "(<νx>(P ∥ Q'))[y::=u] = <νx>((P ∥ Q')[y::=u])"
            by(simp add: fresh_prod name_fresh)
          moreover from ‹y ≠ x› ‹x ≠ u› have "(<νx>Q')[y::=u] = <νx>(Q'[y::=u])"
            by(simp add: fresh_prod name_fresh)
          moreover from ‹x ♯ P› ‹x ≠ u› have "x ♯ P[y::=u]" by(force simp add: fresh_fact1)
          ultimately show ?thesis by(force intro: Res)
        qed
      next
        from ‹x ♯ P› show "(<νx>(P ∥ Q'), P ∥ <νx>Q') ∈ Rel" by(rule Res)
      qed
      ultimately show ?case by blast
    qed
  qed
next
  case(Free α PxQ)
  from ‹P ∥ <νx>Q ⟼α ≺ PxQ› show ?case
  proof(induct rule: parCasesF[where C="x"])
    case(cPar1 P')
    from ‹P ⟼ α ≺ P'› ‹x ♯ P›have "x ♯ α" and "x ♯ P'" by(force intro: freshFreeDerivative)+
    from ‹P ⟼ α ≺ P'› have "P ∥ Q ⟼ α ≺ P' ∥ Q" by(rule Par1F)
    hence "<νx>(P ∥ Q) ⟼ α ≺ <νx>(P' ∥ Q)" using ‹x ♯ α› by(rule ResF)
    moreover from ‹x ♯ P'› have "(<νx>(P' ∥ Q), P' ∥ <νx>Q) ∈ Rel" by(rule Res)
    ultimately show ?case by blast
  next
    case(cPar2 Q')
    from ‹<νx>Q ⟼ α ≺ Q'› show ?case
    proof(induct rule: resCasesF)
      case(cRes Q')
      from ‹Q ⟼ α ≺ Q'› have "P ∥ Q ⟼ α ≺ P ∥ Q'" by(rule Par2F)
      hence "<νx>(P ∥ Q) ⟼α ≺ <νx>(P ∥ Q')" using ‹x ♯ α›  by(rule ResF)
      moreover from ‹x ♯ P› have "(<νx>(P ∥ Q'), P ∥ <νx>Q') ∈ Rel" by(rule Res)
      ultimately show ?case by blast
    qed
  next
    case(cComm1 P' xQ a b y)
    from ‹y ♯ x› have "y ≠ x" by simp
    from ‹P ⟼ a<y> ≺ P'› ‹x ♯ P› ‹y ≠ x› have "x ♯ P'" by(force intro: freshBoundDerivative)
    from ‹<νx>Q ⟼a[b] ≺ xQ› show ?case
    proof(induct rule: resCasesF)
      case(cRes Q')
      from ‹x ♯ a[b]› have "x ≠ b" by simp
      from ‹P ⟼ a<y> ≺ P'› ‹Q ⟼ a[b] ≺ Q'› have "P ∥ Q ⟼ τ ≺ P'[y::=b] ∥ Q'" by(rule Comm1)
      hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx>(P'[y::=b] ∥ Q')" by(rule_tac ResF) auto
      moreover from ‹x ♯ P'› ‹x ≠ b› have "x ♯ P'[y::=b]" by(force intro: fresh_fact1)
      hence "(<νx>(P'[y::=b] ∥ Q'), P'[y::=b] ∥ <νx>Q') ∈ Rel" by(rule Res)
      ultimately show ?case by blast
    qed
  next
    case(cComm2 P' xQ a b y)
    from ‹y ♯ x› ‹y ♯ <νx>Q› have "y ≠ x" and "y ♯ Q" by(simp add: abs_fresh)+ 
    with ‹<νx>Q ⟼a<y> ≺ xQ› show ?case
    proof(induct rule: resCasesB)
      case(cOpen b Q')
      from ‹InputS a = BoundOutputS b› have False by simp
      thus ?case by simp
    next
      case(cRes Q')
      from ‹P ⟼a[b] ≺ P'› ‹Q ⟼a<y> ≺ Q'› have "P ∥ Q ⟼ τ ≺ P' ∥ Q'[y::=b]" by(rule Comm2)
      hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx>(P' ∥ Q'[y::=b])" by(rule_tac ResF) auto
      moreover from ‹P ⟼a[b] ≺ P'› ‹x ♯ P› have "x ♯ P'" and "x ≠ b" by(force dest: freshFreeDerivative)+
      from ‹x ♯ P'› have "(<νx>(P' ∥ Q'[y::=b]), P' ∥ <νx>(Q'[y::=b])) ∈ Rel" by(rule Res)
      with ‹y ≠ x› ‹x ≠ b› have "(<νx>(P' ∥ Q'[y::=b]), P' ∥ (<νx>Q')[y::=b]) ∈ Rel" by simp
      ultimately show ?case by blast
    qed
  next
    case(cClose1 P' Q' a y z)
    from ‹y ♯ x› have "y ≠ x" by simp
    from ‹z ♯ x› ‹z ♯ <νx>Q› have "z ♯ Q" and "z ≠ x" by(simp add: abs_fresh)+
    from ‹P ⟼a<y> ≺ P'› ‹z ♯ P› have "z ≠ a" by(force dest: freshBoundDerivative)
    from ‹<νx>Q ⟼ a<νz> ≺ Q'› ‹z ≠ x› ‹z ♯ Q› show ?case
    proof(induct rule: resCasesB)
      case(cOpen b Q')
      from ‹BoundOutputS a = BoundOutputS b› have "a = b" by simp
      with ‹Q ⟼ b[x] ≺ Q'› have "([(z, x)] ∙ Q) ⟼ [(z, x)] ∙ (a[x] ≺ Q')"
        by(rule_tac transitions.eqvt) simp
      with ‹b ≠ x› ‹z ≠ a› ‹a = b› ‹z ≠ x› have "([(z, x)] ∙ Q) ⟼ a[z] ≺ ([(z, x)] ∙ Q')"
        by(simp add: name_calc eqvts)
      with ‹P ⟼a<y> ≺ P'› have "P ∥ ([(z, x)] ∙ Q) ⟼τ ≺ P'[y::=z] ∥ ([(z, x)] ∙ Q')"
        by(rule Comm1)
      hence "<νz>(P ∥ ([(x, z)] ∙ Q)) ⟼ τ ≺ <νz>(P'[y::=z] ∥ ([(z, x)] ∙ Q'))"
        by(rule_tac ResF) auto
      hence "<νx>(P ∥ Q) ⟼ τ ≺ <νz>(P'[y::=z] ∥ ([(z, x)] ∙ Q'))" using ‹z ♯ P› ‹z ♯ Q› ‹x ♯ P›
        by(subst alphaRes[where c=z]) auto
      with Id show ?case by force
    next
      case(cRes Q')
      from ‹P ⟼a<y> ≺ P'› ‹Q ⟼a<νz> ≺ Q'› ‹z ♯ P› have "P ∥ Q ⟼ τ ≺ <νz>(P'[y::=z] ∥ Q')"
        by(rule Close1)
      hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx><νz>(P'[y::=z] ∥ Q')" by(rule_tac ResF) auto
      moreover from ‹P ⟼a<y> ≺ P'› ‹y ≠ x› ‹x ♯ P› have "x ♯ P'"
        by(force dest: freshBoundDerivative)
      with ‹z ≠ x› have "x ♯ P'[y::=z]" by(simp add: fresh_fact1)
      hence "(<νx><νz>(P'[y::=z] ∥ Q'), <νz>(P'[y::=z] ∥ <νx>Q')) ∈ Rel"
        by(rule ScopeExt)
      ultimately show ?case by blast
    qed
  next
    case(cClose2 P' xQ a y z)
    from ‹z ♯ x› ‹z ♯ <νx>Q› have "z ≠ x" and "z ♯ Q" by(auto simp add: abs_fresh)
    from ‹y ♯ x› ‹y ♯ <νx>Q› have "y ≠ x" and "y ♯ Q" by(auto simp add: abs_fresh)
    with ‹<νx>Q ⟼a<y> ≺ xQ› show ?case
    proof(induct rule: resCasesB)
      case(cOpen b Q')
      from ‹InputS a = BoundOutputS b› have False by simp
      thus ?case by simp
    next
      case(cRes Q')
      from ‹P ⟼a<νz> ≺ P'› ‹Q ⟼a<y> ≺ Q'› ‹z ♯ Q› have "P ∥ Q ⟼ τ ≺ <νz>(P' ∥ Q'[y::=z])"
        by(rule Close2)
      hence "<νx>(P ∥ Q) ⟼ τ ≺ <νx><νz>(P' ∥ (Q'[y::=z]))"
        by(rule_tac ResF) auto
      moreover from ‹P ⟼a<νz> ≺ P'› ‹x ♯ P› ‹z ≠ x› have "x ♯ P'" by(force dest: freshBoundDerivative)
      hence "(<νx><νz>(P' ∥ (Q'[y::=z])), <νz>(P' ∥ (<νx>(Q'[y::=z])))) ∈ Rel"
        by(rule ScopeExt)
      with ‹z ≠ x› ‹y ≠ x› have "(<νx><νz>(P' ∥ (Q'[y::=z])), <νz>(P' ∥ (<νx>Q')[y::=z])) ∈ Rel"
        by simp
      ultimately show ?case by blast
    qed
  qed
qed

lemma scopeExtParRight:
  fixes P   :: pi
  and   Q   :: pi
  and   a   :: name
  and   Rel :: "(pi × pi) set"

  assumes "x ♯ P"
  and     Id:         "Id ⊆ Rel"
  and     "eqvt Rel"
  and     Res:        "⋀R S y. y ♯ R ⟹ (R ∥ <νy>S, <νy>(R ∥ S)) ∈ Rel"
  and     ScopeExt:   "⋀R S y z. y ♯ R ⟹ (<νz>(R ∥ <νy>S), <νy><νz>(R ∥ S)) ∈ Rel"

  shows "P ∥ <νx>Q ↝[Rel] <νx>(P ∥ Q)"
using ‹eqvt Rel›
proof(induct rule: simCasesCont[where C="(x, P, Q)"])
  case(Bound a y xPQ)
  from ‹y ♯ (x, P, Q)› have "y ≠ x" and "y ♯ P" and "y ♯ Q" by simp+
  hence "y ≠ x" and "y ♯ P ∥ Q" by(auto simp add: abs_fresh)
  with ‹<νx>(P ∥ Q) ⟼a«y» ≺ xPQ› show ?case
  proof(induct rule: resCasesB)
    case(cOpen a PQ)
    from ‹P ∥ Q ⟼a[x] ≺ PQ› show ?case
    proof(induct rule: parCasesF[where C="()"])
      case(cPar1 P')
      from ‹P ⟼a[x] ≺ P'› ‹x ♯ P› have "x ≠ x" by(force dest: freshFreeDerivative)
      thus ?case by simp
    next
      case(cPar2 Q')
      from ‹Q ⟼a[x] ≺ Q'› ‹y ♯ Q› have "y ♯ Q'" by(force dest: freshFreeDerivative)
      from ‹Q ⟼a[x] ≺ Q'› ‹a ≠ x› have "<νx>Q ⟼a<νx> ≺ Q'" by(rule Open)
      hence "P ∥ <νx>Q ⟼a<νx> ≺ P ∥ Q'" using ‹x ♯ P› by(rule Par2B)
      with ‹y ♯ P› ‹y ♯ Q'› ‹x ♯ P› have "P ∥ <νx>Q ⟼a<νy> ≺ ([(y, x)] ∙ (P ∥ Q'))"
        by(subst alphaBoundResidual[where x'=x]) (auto simp add: fresh_left calc_atm)
      moreover with Id have "derivative ([(y, x)] ∙ (P ∥  Q'))
                                        ([(y, x)] ∙ (P ∥ Q')) (BoundOutputS a) y Rel"
        by(auto simp add: derivative_def)
      ultimately show ?case by blast
    next
      case(cComm1 P' Q' b c y)
      from ‹a[x] = τ› show ?case by simp
    next
      case(cComm2 P' Q' b c y)
      from ‹a[x] = τ› show ?case by simp
    next
      case(cClose1 P' Q' b y z)
      from ‹a[x] = τ› show ?case by simp
    next
      case(cClose2 P' Q' b y z)
      from ‹a[x] = τ› show ?case by simp
    qed
  next
    case(cRes PQ)
    from ‹P ∥ Q ⟼a«y» ≺ PQ› ‹y ♯ P› ‹y ♯ Q›
    show ?case
    proof(induct rule: parCasesB)
      case(cPar1 P')
      from ‹y ≠ x› ‹x ♯ P› ‹P ⟼a«y» ≺ P'› have "x ♯ P'" by(force dest: freshBoundDerivative)
      
      from ‹P ⟼a«y» ≺ P'› ‹y ♯ Q› have "P ∥ <νx>Q ⟼a«y» ≺ P' ∥ <νx>Q"
        by(rule_tac Par1B) (auto simp add: abs_fresh)
      moreover have "derivative (P' ∥ <νx>Q) (<νx>(P' ∥ Q)) a y Rel"
      proof(cases a, auto simp add: derivative_def)
        fix u::name
        obtain z::name where "z ♯ Q" and "y ≠ z" and "z ≠ u" and "z ♯ P" and "z ♯ P'"
          by(generate_fresh "name") auto
        thus "(P'[y::=u] ∥ (<νx>Q)[y::=u], (<νx>(P' ∥ Q))[y::=u]) ∈ Rel" using ‹x ♯ P'›
          by(subst alphaRes[where c=z and a=x], auto)
            (subst alphaRes[where c=z and a=x], auto intro: Res simp add: fresh_fact1)
      next
        from ‹x ♯ P'› show "(P' ∥ <νx>Q, <νx>(P' ∥ Q)) ∈ Rel"
          by(rule Res)
      qed

      ultimately show ?case by blast
    next
      case(cPar2 Q')
      from ‹Q ⟼a«y» ≺ Q'› have "<νx>Q ⟼a«y» ≺ <νx>Q'" using ‹x ♯ a› ‹y ≠ x› 
        by(rule_tac ResB) auto
      hence "P ∥ <νx>Q ⟼a«y» ≺ P ∥ <νx>Q'" using ‹y ♯ P› by(rule Par2B)
      
      moreover have "derivative (P ∥ <νx>Q') (<νx>(P ∥ Q')) a y Rel"
      proof(cases a, auto simp add: derivative_def)
        fix u::name
        obtain z::name where "z ♯ Q" and "z ≠ y" and "z ≠ u" and "z ♯ P" and "z ♯ Q'"
          by(generate_fresh "name") auto
        
        thus  "(P[y::=u] ∥ (<νx>Q')[y::=u], (<νx>(P ∥ Q'))[y::=u]) ∈ Rel" using ‹x ♯ P›
          by(subst alphaRes[where a=x and c=z], auto)
            (subst alphaRes[where a=x and c=z], auto intro: Res simp add: fresh_fact1)
      next
        from ‹x ♯ P› show "(P ∥ <νx>Q', <νx>(P ∥ Q')) ∈ Rel"
          by(rule Res)
      qed
      
      ultimately show ?case by blast
    qed
  qed
next
  case(Free α xPQ)
  from ‹<νx>(P ∥ Q) ⟼α ≺ xPQ› show ?case
  proof(induct rule: resCasesF)
    case(cRes PQ)
    from ‹P ∥ Q ⟼α ≺ PQ› show ?case
    proof(induct rule: parCasesF[where C="x"])
      case(cPar1 P')
      from ‹P ⟼α ≺ P'› have "P ∥ <νx>Q ⟼α ≺ P' ∥ <νx>Q" by(rule Par1F)
      moreover from ‹P ⟼α ≺ P'› ‹x ♯ P› have "x ♯ P'" by(rule freshFreeDerivative)
      hence "(P' ∥ <νx>Q, <νx>(P' ∥ Q)) ∈ Rel" by(rule Res)
      ultimately show ?case by blast
    next
      case(cPar2 Q')
      from ‹Q ⟼α ≺ Q'› ‹x ♯ α› have "<νx>Q ⟼α ≺ <νx>Q'" by(rule ResF)
      hence "P ∥ <νx>Q ⟼α ≺ P ∥ <νx>Q'" by(rule Par2F)
      moreover from ‹x ♯ P› have "(P ∥ <νx>Q', <νx>(P ∥ Q')) ∈ Rel" by(rule Res)
      ultimately show ?case by blast
    next
      case(cComm1 P' Q' a b y)
      from ‹x ♯ P› ‹y ♯ x› ‹P ⟼a<y> ≺ P'› have "x ≠ a" and "x ♯ P'" by(force dest: freshBoundDerivative)+
      show ?case
      proof(cases "b=x")
        case True
        from ‹Q ⟼a[b] ≺ Q'› ‹x ≠ a› ‹b = x› have "<νx>Q ⟼a<νx> ≺ Q'" by(rule_tac Open) auto
        with ‹P ⟼a<y> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ <νx>(P'[y::=x] ∥ Q')" using ‹x ♯ P› by(rule Close1)
        moreover from Id have "(<νx>(P'[y::=b] ∥ Q'), <νx>(P'[y::=b] ∥ Q')) ∈ Rel" by blast
        ultimately show ?thesis using ‹b=x› by blast
      next
        case False
        from ‹Q ⟼a[b] ≺ Q'› ‹x ≠ a› ‹b ≠ x› have "<νx>Q ⟼a[b] ≺ <νx>Q'" by(rule_tac ResF) auto
        with ‹P ⟼a<y> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ (P'[y::=b] ∥ <νx>Q')" by(rule Comm1)
        moreover from ‹x ♯ P'› ‹b ≠ x› have "(P'[y::=b] ∥ <νx>Q', <νx>(P'[y::=b] ∥ Q')) ∈ Rel"
          by(force intro: Res simp add: fresh_fact1)
        ultimately show ?thesis by blast
      qed
    next
      case(cComm2 P' Q' a b y)
      from ‹P ⟼a[b] ≺ P'› ‹x ♯ P› have "x ≠ a" and "x ≠ b" and "x ♯ P'" by(force dest: freshFreeDerivative)+
      from ‹Q ⟼a<y> ≺ Q'› ‹y ♯ x› ‹x ≠ a› have "<νx>Q ⟼a<y> ≺ <νx>Q'" by(rule_tac ResB) auto
      with ‹P ⟼a[b] ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ P' ∥ (<νx>Q')[y::=b]" by(rule Comm2)
      moreover from ‹x ♯ P'› have "(P' ∥ <νx>(Q'[y::=b]), <νx>(P' ∥ Q'[y::=b])) ∈ Rel" by(rule Res)
      ultimately show ?case using ‹y ♯ x› ‹x ≠ b› by force
    next
      case(cClose1 P' Q' a y z)
      from ‹P ⟼a<y> ≺ P'› ‹x ♯ P› ‹y ♯ x› have "x ≠ a" and "x ♯ P'" by(force dest: freshBoundDerivative)+
      from ‹Q ⟼a<νz> ≺ Q'› ‹z ♯ x› ‹x ≠ a› have "<νx>Q ⟼a<νz> ≺ <νx>Q'" by(rule_tac ResB) auto
      with ‹P ⟼a<y> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ <νz>(P'[y::=z] ∥ <νx>Q')" using ‹z ♯ P› by(rule Close1)
      moreover from ‹x ♯ P'› ‹z ♯ x› have "(<νz>(P'[y::=z] ∥ <νx>Q'), <νx>(<νz>(P'[y::=z] ∥ Q'))) ∈ Rel" 
        by(rule_tac ScopeExt) (auto simp add: fresh_fact1)
      ultimately show ?case by blast
    next
      case(cClose2 P' Q' a y z)
      from ‹P ⟼a<νz> ≺ P'› ‹x ♯ P› ‹z ♯ x› have "x ≠ a" and "x ♯ P'" by(force dest: freshBoundDerivative)+
      from ‹Q ⟼a<y> ≺ Q'› ‹y ♯ x› ‹x ≠ a› have "<νx>Q ⟼a<y> ≺ <νx>Q'" by(rule_tac ResB) auto
      with ‹P ⟼a<νz> ≺ P'› have "P ∥ <νx>Q ⟼τ ≺ <νz>(P' ∥ (<νx>Q')[y::=z])" using ‹z ♯ Q›
        by(rule_tac Close2) (auto simp add: abs_fresh)
      moreover from ‹x ♯ P'› have "(<νz>(P' ∥ <νx>(Q'[y::=z])), <νx><νz>(P' ∥ Q'[y::=z])) ∈ Rel" by(rule ScopeExt)
      ultimately show ?case using ‹z ♯ x› ‹y ♯ x› by force
    qed
  qed
qed

lemma resNilRight:
  fixes x   :: name
  and   Rel :: "(pi × pi) set"

  shows "𝟬 ↝[Rel] <νx>𝟬"
by(fastforce simp add: simulation_def pi.inject alpha' elim: resCasesB' resCasesF)

lemma resComm:
  fixes a   :: name
  and   b   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes ResComm: "⋀c d Q. (<νc><νd>Q, <νd><νc>Q) ∈ Rel"
  and     Id:      "Id ⊆ Rel"
  and     EqvtRel: "eqvt Rel"

  shows "<νa><νb>P ↝[Rel] <νb><νa>P"
proof(cases "a=b")
  assume "a=b"
  with Id show ?thesis by(force intro: Strong_Late_Sim.reflexive)
next
  assume aineqb: "a ≠ b"
  from EqvtRel show ?thesis
  proof(induct rule: simCasesCont[where C="(a, b, P)"])
    case(Bound c x baP)
    from ‹x ♯ (a, b, P)› have "x ≠ a" and "x ≠ b" and "x ♯ P" by simp+
    from ‹x ♯ P› have "x ♯ <νa>P" by(simp add: abs_fresh)
    with ‹<νb><νa>P ⟼ c«x» ≺ baP› ‹x ≠ b› show ?case
    proof(induct rule: resCasesB)
      case(cOpen c aP)
      from ‹<νa>P ⟼c[b] ≺ aP›
      show ?case
      proof(induct rule: resCasesF)
        case(cRes P')
        from ‹a ♯ c[b]› have "a ≠ c" and "a ≠ b" by simp+
        from ‹x ♯ P› ‹P ⟼c[b] ≺ P'› have "x ≠ c" and "x ♯ P'" by(force dest: freshFreeDerivative)+
        from ‹P ⟼ c[b] ≺ P'› have "([(x, b)] ∙ P) ⟼ [(x, b)] ∙ (c[b] ≺ P')" by(rule transitions.eqvt)
        with ‹x ≠ c› ‹c ≠ b› ‹x ≠ b› have "([(x, b)] ∙ P) ⟼ c[x] ≺ [(x, b)] ∙ P'" by(simp add: eqvts calc_atm)
        hence "<νx>([(x, b)] ∙ P) ⟼ c<νx> ≺ [(x, b)] ∙ P'" using ‹x ≠ c› by(rule_tac Open) auto
        with ‹x ♯ P› have "<νb>P ⟼ c<νx> ≺ [(x, b)] ∙ P'" by(simp add: alphaRes)
        hence "<νa><νb>P ⟼ c<νx> ≺ <νa>([(x, b)] ∙ P')" using ‹a ≠ c› ‹x ≠ a›
          by(rule_tac ResB) auto
        moreover from Id have "derivative (<νa>([(x, b)] ∙ P')) (<νa>([(x, b)] ∙ P')) (BoundOutputS c) x Rel"
          by(force simp add: derivative_def)
        ultimately show ?case using ‹a ≠ b› ‹x ≠ a› ‹a ≠ c› by(force simp add: eqvts calc_atm)
      qed
    next
      case(cRes aP)
      from ‹<νa>P ⟼ c«x» ≺ aP› ‹x ≠ a› ‹x ♯ P› ‹b ♯ c› show ?case
      proof(induct rule: resCasesB)
        case(cOpen c P')
        from ‹P ⟼c[a] ≺ P'› ‹x ♯ P› have "x ♯ P'" by(force intro: freshFreeDerivative)
        from ‹b ♯ BoundOutputS c› have "b ≠ c" by simp
        with ‹P ⟼c[a] ≺ P'› ‹a ≠ b› have "<νb>P ⟼ c[a] ≺ <νb>P'" by(rule_tac ResF) auto
        with ‹c ≠ a› have "<νa><νb>P ⟼ c<νa> ≺ <νb>P'" by(rule_tac Open) auto
        hence "<νa><νb>P ⟼c<νx> ≺ <νb>([(x, a)] ∙ P')" using ‹x ≠ b› ‹a ≠ b› ‹x ♯ P'›
          apply(subst alphaBoundResidual[where x'=a]) by(auto simp add: abs_fresh fresh_left calc_atm)
        moreover have "derivative (<νb>([(x, a)] ∙ P')) (<νb>([(x, a)] ∙ P')) (BoundOutputS c) x Rel" using Id
          by(force simp add: derivative_def)
        ultimately show ?case by blast
      next
        case(cRes P')
        from ‹P ⟼c«x» ≺ P'› ‹b ♯ c› ‹x ≠ b› have "<νb>P ⟼ c«x» ≺ <νb>P'" by(rule_tac ResB) auto
        hence "<νa><νb>P ⟼ c«x» ≺ <νa><νb>P'" using ‹a ♯ c› ‹x ≠ a› by(rule_tac ResB) auto
        moreover have "derivative (<νa><νb>P') (<νb><νa>P') c x Rel"
        proof(cases c, auto simp add: derivative_def)
          fix u::name
          show  "((<νa><νb>P')[x::=u],  (<νb><νa>P')[x::=u]) ∈ Rel"
          proof(cases "u=a")
            case True
            from ‹u = a› ‹a ≠ b› show ?thesis
              by(subst injPermSubst[symmetric], auto simp add: abs_fresh)
                (subst injPermSubst[symmetric], auto simp add: abs_fresh calc_atm intro: ResComm)
          next
            case False
            show ?thesis
            proof(cases "u=b")
              case True
              from ‹u = b› ‹u ≠ a› show ?thesis
              by(subst injPermSubst[symmetric], auto simp add: abs_fresh)
                (subst injPermSubst[symmetric], auto simp add: abs_fresh calc_atm intro: ResComm)
            next
              case False
              from ‹u ≠ a› ‹u ≠ b› ‹x ≠ a› ‹x ≠ b› show ?thesis by(auto intro: ResComm)
            qed
          qed
        next
          show "(<νa><νb>P', <νb><νa>P') ∈ Rel" by(rule ResComm)
        qed
        ultimately show ?case by blast
      qed
    qed
  next
    case(Free α baP)
    from ‹<νb><νa>P ⟼ α ≺ baP› show ?case
    proof(induct rule: resCasesF)
      case(cRes aP)
      from ‹<νa>P ⟼ α ≺ aP› show ?case
      proof(induct rule: resCasesF)
        case(cRes P')
        from ‹P ⟼ α ≺ P'› ‹b ♯ α› have "<νb>P ⟼ α ≺ <νb>P'" by(rule ResF)
        hence "<νa><νb>P ⟼ α ≺ <νa><νb>P'" using ‹a ♯ α› by(rule ResF)
        moreover have "(<νa><νb>P', <νb><νa>P') ∈ Rel" by(rule ResComm)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

(***************** !-operator ********************)

lemma bangLeftSC:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes "Id ⊆ Rel"

  shows "!P ↝[Rel] P ∥ !P"
using assms
by(force simp add: simulation_def dest: Bang derivativeReflexive)

lemma bangRightSC:
  fixes P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes IdRel: "Id ⊆ Rel"

  shows "P ∥ !P ↝[Rel] !P"
using assms
by(fastforce simp add: pi.inject simulation_def intro: derivativeReflexive elim: bangCases)

lemma resNilLeft:
  fixes x   :: name
  and   y   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"
  and   b   :: name

  shows "𝟬 ↝[Rel] <νx>(x<y>.P)"
  and   "𝟬 ↝[Rel] <νx>(x{b}.P)"
by(auto simp add: simulation_def)

lemma resInputLeft:
  fixes x :: name
  and   a :: name
  and   y :: name
  and   P :: pi
  and   Rel :: "(pi × pi) set"

  assumes xineqa: "x ≠ a"
  and     xineqy: "x ≠ y"
  and     Eqvt: "eqvt Rel"
  and     Id: "Id ⊆ Rel"

  shows "<νx>a<y>.P ↝[Rel] a<y>.(<νx>P)"
using Eqvt
proof(induct rule: simCasesCont[where C="(x, y, a, P)"])
  case(Bound b z P')
  from ‹z ♯ (x, y, a, P)› have "z ≠ x" and "z ≠ y" and "z ♯ P" and "z ≠ a"  by simp+
  from ‹z ♯ P› have "z ♯ <νx>P" by(simp add: abs_fresh)
  with ‹a<y>.(<νx>P) ⟼b«z» ≺ P'› ‹z ≠ a› ‹z ≠ y› show ?case
  proof(induct rule: inputCases)
    case cInput
    have "a<y>.P ⟼a<y> ≺ P" by(rule Input)
    with ‹x ≠ y› ‹x ≠ a› have "<νx>a<y>.P ⟼a<y> ≺ <νx>P" by(rule_tac ResB) auto
    hence "<νx>a<y>.P ⟼a<z> ≺ [(y,  z)] ∙ <νx>P" using ‹z ♯ P› 
      by(subst alphaBoundResidual[where x'=y]) (auto simp add: abs_fresh fresh_left calc_atm)
    moreover from Id have "derivative ([(y, z)] ∙ <νx>P) ([(y, z)] ∙ <νx>P) (InputS a) z Rel" 
      by(rule derivativeReflexive)
    ultimately show ?case by blast
  qed
next
  case(Free α P')
  from ‹a<y>.(<νx>P) ⟼α ≺ P'› have False by auto
  thus ?case by simp
qed

lemma resInputRight:
  fixes a :: name
  and   y :: name
  and   x :: name
  and   P :: pi
  and   Rel :: "(pi × pi) set"

  assumes xineqa: "x ≠ a"
  and     xineqy: "x ≠ y"
  and     Eqvt: "eqvt Rel"
  and     Id: "Id ⊆ Rel"

  shows "a<y>.(<νx>P) ↝[Rel] <νx>a<y>.P"
  using Eqvt
proof(induct rule: simCasesCont[where C="(x, y, a, P)"])
  case(Bound b z xP)
  from ‹z ♯ (x, y, a, P)› have "z ≠ x" and "z ≠ y" and "z ♯ P" and "z ≠ a" by simp+
  from ‹z ≠ a› ‹z ♯ P› have "z ♯ a<y>.P" by(simp add: abs_fresh)
  with ‹<νx>a<y>.P ⟼b«z» ≺ xP› ‹z ≠ x› show ?case
  proof(induct rule: resCasesB)
    case(cOpen b P')
    from ‹a<y>.P ⟼b[x] ≺ P'› have False by auto
    thus ?case by simp
  next
    case(cRes P')
    from ‹a<y>.P ⟼b«z» ≺ P'›‹z ≠ a› ‹z ≠ y› ‹z ♯ P› show ?case
    proof(induct rule: inputCases)
      case cInput
      have "a<y>.(<νx>P) ⟼a<y> ≺ (<νx>P)" by(rule Input)
      with ‹z ♯ P› ‹x ≠ y› ‹z ≠ x› have "a<y>.(<νx>P) ⟼a<z> ≺ (<νx>([(y, z)] ∙ P))"
        by(subst alphaBoundResidual[where x'=y]) (auto simp add: abs_fresh calc_atm fresh_left)
      moreover from Id have "derivative (<νx>([(y, z)] ∙ P)) (<νx>([(y, z)] ∙ P)) (InputS a) z Rel"
        by(rule derivativeReflexive)
      ultimately show ?case by blast
    qed
  qed
next
  case(Free α P')
  from ‹<νx>a<y>.P ⟼α ≺ P'› have False by auto
  thus ?case by simp
qed

lemma resOutputLeft:
  fixes x   :: name
  and   a   :: name
  and   b   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes xineqa: "x ≠ a"
  and     xineqb: "x ≠ b"
  and     Id: "Id ⊆ Rel"

  shows "<νx>a{b}.P ↝[Rel] a{b}.(<νx>P)"
using assms
by(fastforce simp add: simulation_def elim: outputCases intro: Output ResF)

lemma resOutputRight:
  fixes x   :: name
  and   a   :: name
  and   b   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes xineqa: "x ≠ a"
  and     xineqb: "x ≠ b"
  and     Id: "Id ⊆ Rel"
  and     Eqvt: "eqvt Rel"

  shows "a{b}.(<νx>P) ↝[Rel] <νx>a{b}.P"
using assms
by(erule_tac simCasesCont[where C=x])
  (force simp add: abs_fresh elim: resCasesB resCasesF outputCases intro: ResF Output)+

lemma resTauLeft:
  fixes x   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id: "Id ⊆ Rel"

  shows "<νx>(τ.(P)) ↝[Rel] τ.(<νx>P)"
using assms
by(force simp add: simulation_def elim: tauCases resCasesF intro: Tau ResF)

lemma resTauRight: 
  fixes x   :: name
  and   P   :: pi
  and   Rel :: "(pi × pi) set"

  assumes Id:   "Id ⊆ Rel"

  shows "τ.(<νx>P) ↝[Rel] <νx>(τ.(P))"
using assms
by(force simp add: simulation_def elim: tauCases resCasesF intro: Tau ResF)

end