Theory Weak_Sim_Pres

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Weak_Sim_Pres
  imports Sim_Pres Weak_Simulation Weak_Stat_Imp
begin

context env begin

lemma weakInputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a

  assumes PRelQ: "⋀Tvec Ψ'. length xvec = length Tvec ⟹ (Ψ ⊗ Ψ', P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel"

  shows "Ψ ⊳ M⦇λ*xvec N⦈.P ↝<Rel> M⦇λ*xvec N⦈.Q"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from ‹Ψ ⊳ M⦇λ*xvec N⦈.Q ⟼α ≺ Q'› show ?case
  proof(induct rule: inputCases)
    case(cInput K Tvec)
    from ‹Ψ ⊢ M ↔ K› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec› ‹distinct xvec›
    have "Ψ : (M⦇λ*xvec N⦈.Q) ⊳ M⦇λ*xvec N⦈.P ⟹K⦇(N[xvec::=Tvec])⦈ ≺ (P[xvec::=Tvec])"
      by(rule_tac weakInput) auto
    moreover have "Ψ ⊗ Ψ' ⊳ P[xvec::=Tvec] ⟹⇧^⇩τ  P[xvec::=Tvec]" by simp
    moreover from ‹length xvec = length Tvec› have "(Ψ ⊗ Ψ',  P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel"
      by(rule PRelQ)
    ultimately show ?case by blast
  qed
next
  case(cTau Q')
  from ‹Ψ ⊳ M⦇λ*xvec N⦈.Q ⟼τ ≺ Q'› have False by auto
  thus ?case by simp
qed

lemma weakOutputPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a

  assumes PRelQ: "⋀Ψ'. (Ψ ⊗ Ψ', P, Q) ∈ Rel"

  shows "Ψ ⊳ M⟨N⟩.P ↝<Rel> M⟨N⟩.Q"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from ‹Ψ ⊳ M⟨N⟩.Q ⟼α ≺ Q'› show ?case
  proof(induct rule: outputCases)
    case(cOutput K)
    from ‹Ψ ⊢ M ↔ K› 
    have "Ψ : (M⟨N⟩.Q) ⊳ M⟨N⟩.P ⟹K⟨N⟩ ≺ P" by(rule weakOutput) auto
    moreover have "Ψ ⊗ Ψ' ⊳ P ⟹⇧^⇩τ  P" by simp
    moreover have "(Ψ ⊗ Ψ',  P, Q) ∈ Rel" by(rule PRelQ)
    ultimately show ?case by blast
  qed
next
  case(cTau Q')
  from  ‹Ψ ⊳ M⟨N⟩.Q ⟼τ ≺ Q'› have False by auto
  thus ?case by simp
qed

lemma resTauCases[consumes 3, case_names cRes]:
  fixes Ψ    :: 'b
  and   x    :: name
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   C    :: "'d::fs_name"

  assumes Trans: "Ψ ⊳ ⦇νx⦈P ⟼τ ≺ P'"
  and     "x ♯ Ψ"
  and     "x ♯ P'"
  and     rScope:  "⋀P'. ⟦Ψ ⊳ P ⟼τ ≺ P'⟧ ⟹ Prop (⦇νx⦈P')"

  shows "Prop P'"
proof -
  note Trans ‹x ♯ Ψ›
  moreover have "x ♯ (τ)" by simp
  moreover note ‹x ♯ P'›
  moreover have "bn(τ) ♯* Ψ" and "bn(τ) ♯* P" and "bn(τ) ♯* subject(τ)" and "bn(τ) = []" by simp+
  ultimately show ?thesis
    by(induct rule: resCases) (auto intro: rScope)
qed

lemma weakResPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   x    :: name
  and   Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes PSimQ: "Ψ ⊳ P ↝<Rel> Q"
  and     "eqvt Rel'"
  and     "x ♯ Ψ"
  and     "Rel ⊆ Rel'"
  and     C1: "⋀Ψ' R S y. ⟦(Ψ', R, S) ∈ Rel; y ♯ Ψ'⟧ ⟹ (Ψ', ⦇νy⦈R, ⦇νy⦈S) ∈ Rel'"

  shows   "Ψ ⊳ ⦇νx⦈P ↝<Rel'> ⦇νx⦈Q"
proof -
  note ‹eqvt Rel'› ‹x ♯ Ψ›
  moreover have "x ♯ ⦇νx⦈P" and "x ♯ ⦇νx⦈Q" by(simp add: abs_fresh)+ 
  ultimately show ?thesis
  proof(induct rule: weakSimIFresh[of _ _ _ _ _ "()"])
    case(cAct α Q' Ψ')
    from ‹bn α ♯* ⦇νx⦈P› ‹bn α ♯* ⦇νx⦈Q› ‹x ♯ α› have "bn α ♯* P" and "bn α ♯* Q" by simp+
    from ‹Ψ ⊳ ⦇νx⦈Q ⟼α ≺ Q'› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* Q› ‹bn α ♯* subject α› ‹bn α ♯* P› ‹x ♯ α›
    show ?case
    proof(induct rule: resCases)
      case(cOpen M xvec1 xvec2 y N Q')
      from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* P› have "xvec1 ♯* P" and "xvec2 ♯* P" and "y ♯ P" by simp+
      from ‹x ♯ (M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩)› have "x ♯ xvec1" and "x ≠ y" and "x ♯ xvec2" and "x ♯ M" by simp+
      from PSimQ ‹Ψ ⊳ Q ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ Q')› ‹xvec1 ♯* Ψ› ‹xvec2 ♯* Ψ› ‹xvec1 ♯* P› ‹xvec2 ♯* P› ‹α ≠ τ›
      obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ P''"
                      and P''Chain: "Ψ ⊗ ([(x, y)] ∙ Ψ') ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ ([(x, y)] ∙ Ψ'), P', ([(x, y)] ∙ Q')) ∈ Rel"
        by (fastforce dest: weakSimE)
      from PTrans have "([(x, y)] ∙ Ψ) : ([(x, y)] ∙ Q) ⊳ ([(x, y)] ∙ P) ⟹([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩)) ≺ ([(x, y)] ∙ P'')"
        by(rule eqvts)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec1› ‹y ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec2›
      have "Ψ : ([(x, y)] ∙ Q) ⊳ ([(x, y)] ∙ P) ⟹M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ ([(x, y)] ∙ P'')"
        by(simp add: eqvts)
      hence "Ψ : ⦇νy⦈([(x, y)] ∙ Q) ⊳ ⦇νy⦈([(x, y)] ∙ P) ⟹M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ ([(x, y)] ∙ P'')"
        using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
        by(rule weakOpen)
      with ‹y ♯ P› ‹y ♯ Q› have "Ψ : ⦇νx⦈Q ⊳ ⦇νx⦈P ⟹M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ ([(x, y)] ∙ P'')"
        by(simp add: alphaRes)
      moreover from P''Chain have "([(x, y)] ∙ (Ψ ⊗ ([(x, y)] ∙ Ψ'))) ⊳ ([(x, y)] ∙ P'') ⟹⇧^⇩τ ([(x, y)] ∙ P')"
        by(rule eqvts)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ ⊗ Ψ' ⊳ ([(x, y)] ∙ P'') ⟹⇧^⇩τ ([(x, y)] ∙ P')" by(simp add: eqvts)
      moreover from P'RelQ' ‹Rel ⊆ Rel'› have "(Ψ ⊗ ([(x, y)] ∙ Ψ'), P', ([(x, y)] ∙ Q')) ∈ Rel'" by auto
      with ‹eqvt Rel'› have "([(x, y)] ∙ (Ψ ⊗ ([(x, y)] ∙ Ψ'), P', ([(x, y)] ∙ Q'))) ∈ Rel'" by(rule eqvtI)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› have " (Ψ ⊗ Ψ', [(x, y)] ∙ P', Q') ∈ Rel'" by(simp add: eqvts)
      ultimately show ?case by blast
    next
      case(cRes Q')
      from PSimQ ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹α ≠ τ›
      obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''"
                      and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
        by(blast dest: weakSimE)
      from PTrans ‹x ♯ Ψ› ‹x ♯ α›  have "Ψ : ⦇νx⦈Q ⊳ ⦇νx⦈P ⟹α ≺ ⦇νx⦈P''"
        by(rule_tac weakScope)
      moreover from P''Chain  ‹x ♯ Ψ› ‹x ♯ Ψ'› have "Ψ ⊗ Ψ' ⊳ ⦇νx⦈P'' ⟹⇧^⇩τ ⦇νx⦈P'"
        by(rule_tac tauChainResPres) auto
      moreover from P'RelQ' ‹x ♯ Ψ› ‹x ♯ Ψ'› have "(Ψ ⊗ Ψ', ⦇νx⦈P', ⦇νx⦈Q') ∈ Rel'" 
        apply(rule_tac C1) by(auto simp add: fresh_left calc_atm)
      ultimately show ?case by blast
    qed
  next
    case(cTau Q')
    from ‹Ψ ⊳ ⦇νx⦈Q ⟼τ ≺ Q'› ‹x ♯ Ψ› ‹x ♯ Q'›
    show ?case
    proof(induct rule: resTauCases)
      case(cRes Q')
      from PSimQ ‹Ψ ⊳ Q ⟼τ ≺ Q'› obtain P' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel" 
        by(blast dest: weakSimE)
      from PChain ‹x ♯ Ψ› have "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇νx⦈P'" by(rule tauChainResPres)
      moreover from P'RelQ' ‹x ♯ Ψ› have "(Ψ, ⦇νx⦈P', ⦇νx⦈Q') ∈ Rel'" by(rule C1)
      ultimately show ?case by blast
    qed
  qed
qed

lemma weakResChainPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes PSimQ: "Ψ ⊳ P ↝<Rel> Q"
  and     "eqvt Rel"
  and     "xvec ♯* Ψ"
  and     C1:    "⋀Ψ' R S yvec. ⟦(Ψ', R, S) ∈ Rel; yvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*yvec⦈R, ⦇ν*yvec⦈S) ∈ Rel"

  shows   "Ψ ⊳ ⦇ν*xvec⦈P ↝<Rel> ⦇ν*xvec⦈Q"
using ‹xvec ♯* Ψ›
proof(induct xvec)
  case Nil
  from PSimQ show ?case by simp
next
  case(Cons x xvec)
  from ‹(x#xvec) ♯* Ψ› have "x ♯ Ψ" and "xvec ♯* Ψ" by simp+
  from ‹xvec ♯* Ψ ⟹ Ψ ⊳ ⦇ν*xvec⦈P ↝<Rel> ⦇ν*xvec⦈Q› ‹xvec ♯* Ψ›
  have "Ψ ⊳ ⦇ν*xvec⦈P ↝<Rel> ⦇ν*xvec⦈Q" by simp
  moreover note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover have "Rel ⊆ Rel" by simp
  moreover have "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ Rel; x ♯ Ψ⟧ ⟹ (Ψ, ⦇ν*[x]⦈P, ⦇ν*[x]⦈Q) ∈ Rel"
    by(rule_tac yvec="[x]" in C1) auto
  hence "⋀Ψ P Q x. ⟦(Ψ, P, Q) ∈ Rel; x ♯ Ψ⟧ ⟹ (Ψ, ⦇νx⦈P, ⦇νx⦈Q) ∈ Rel"
    by simp
  ultimately have "Ψ ⊳ ⦇νx⦈(⦇ν*xvec⦈P) ↝<Rel> ⦇νx⦈(⦇ν*xvec⦈Q)"
    by(rule weakResPres)
  thus ?case by simp
qed

lemma parTauCases[consumes 1, case_names cPar1 cPar2 cComm1 cComm2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"
  and   C :: "'d::fs_name"

  assumes Trans: "Ψ ⊳ P ∥ Q ⟼τ ≺ R"
  and     rPar1: "⋀P' A⇩Q Ψ⇩Q. ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼τ ≺ P';  extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
                       A⇩Q ♯* Ψ; A⇩Q ♯* P; A⇩Q ♯* Q; A⇩Q ♯* C⟧ ⟹ Prop (P' ∥ Q)"
  and     rPar2: "⋀Q' A⇩P Ψ⇩P. ⟦Ψ ⊗ Ψ⇩P ⊳ Q ⟼τ ≺ Q'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
                       A⇩P ♯* Ψ; A⇩P ♯* P;  A⇩P ♯* Q; A⇩P ♯* C⟧ ⟹ Prop (P ∥ Q')"
  and     rComm1: "⋀Ψ⇩Q M N P' A⇩P Ψ⇩P K xvec Q' A⇩Q.
           ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼M⦇N⦈ ≺ P'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
            Ψ ⊗ Ψ⇩P ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
            Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K; distinct xvec;
            A⇩P ♯* Ψ;  A⇩P ♯* Ψ⇩Q;  A⇩P ♯* P;  A⇩P ♯* M;  A⇩P ♯* N;  A⇩P ♯* P';  A⇩P ♯* Q;  A⇩P ♯* xvec;  A⇩P ♯* Q'; A⇩P ♯* A⇩Q;  A⇩P ♯* C; 
            A⇩Q ♯* Ψ;  A⇩Q ♯* Ψ⇩P; A⇩Q ♯* P;  A⇩Q ♯* K;  A⇩Q ♯* N;  A⇩Q ♯* P';  A⇩Q ♯* Q;  A⇩Q ♯* xvec;  A⇩Q ♯* Q'; A⇩Q ♯* C; 
            xvec ♯* Ψ;  xvec ♯* Ψ⇩P; xvec ♯* P;  xvec ♯* M;  xvec ♯* K; xvec ♯* Q;  xvec ♯* Ψ⇩Q;  xvec ♯* C⟧ ⟹
            Prop (⦇ν*xvec⦈(P' ∥ Q'))"
  and     rComm2: "⋀Ψ⇩Q M xvec N P' A⇩P Ψ⇩P K Q' A⇩Q.
           ⟦Ψ ⊗ Ψ⇩Q ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'; extractFrame P = ⟨A⇩P, Ψ⇩P⟩; distinct A⇩P;
            Ψ ⊗ Ψ⇩P ⊳ Q ⟼K⦇N⦈ ≺ Q'; extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩; distinct A⇩Q;
            Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q ⊢ M ↔ K; distinct xvec;
            A⇩P ♯* Ψ;  A⇩P ♯* Ψ⇩Q;  A⇩P ♯* P;  A⇩P ♯* M;  A⇩P ♯* N;  A⇩P ♯* P';  A⇩P ♯* Q;  A⇩P ♯* xvec;  A⇩P ♯* Q'; A⇩P ♯* A⇩Q;  A⇩P ♯* C; 
            A⇩Q ♯* Ψ;  A⇩Q ♯* Ψ⇩P; A⇩Q ♯* P;  A⇩Q ♯* K;  A⇩Q ♯* N;  A⇩Q ♯* P';  A⇩Q ♯* Q;  A⇩Q ♯* xvec;  A⇩Q ♯* Q'; A⇩Q ♯* C; 
            xvec ♯* Ψ;  xvec ♯* Ψ⇩P; xvec ♯* P;  xvec ♯* M;  xvec ♯* K;  xvec ♯* Q;  xvec ♯* Ψ⇩Q;  xvec ♯* C⟧ ⟹
            Prop (⦇ν*xvec⦈(P' ∥ Q'))"

  shows "Prop R"
proof -
  from Trans obtain α where "Ψ ⊳ P ∥ Q ⟼α ≺ R" and "bn α ♯* Ψ" and "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* subject α" and "α = τ" by auto
  thus ?thesis using rPar1 rPar2 rComm1 rComm2
    by(induct rule: parCases[where C=C]) (auto simp add: residualInject)
qed

lemma weakParPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"
  and   Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  
  assumes PRelQ: "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q⟧ ⟹ (Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" 
  and     Eqvt:  "eqvt Rel"
  and     Eqvt': "eqvt Rel'"

  and     Sim:    "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ↝<Rel> T"
  and     Sym:    "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', T, S) ∈ Rel"
  and     Ext:    "⋀Ψ' S T Ψ'. ⟦(Ψ', S, T) ∈ Rel⟧ ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
  and     StatImp: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ⪅<Rel> T"
  and     C1: "⋀Ψ' S T A⇩U Ψ⇩U U. ⟦(Ψ' ⊗ Ψ⇩U, S, T) ∈ Rel; extractFrame U = ⟨A⇩U, Ψ⇩U⟩; A⇩U ♯* Ψ'; A⇩U ♯* S; A⇩U ♯* T⟧ ⟹ (Ψ', S ∥ U, T ∥ U) ∈ Rel'"
  and     C2: "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel'; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel'"
  and     C3: "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel"

  shows "Ψ ⊳ P ∥ R ↝<Rel'> Q ∥ R"
proof -
  from Eqvt' show ?thesis
  proof(induct rule: weakSimI[where C="()"])
    case(cAct Ψ' α QR)
    from ‹bn α ♯* (P ∥ R)› ‹bn α ♯* (Q ∥ R)›
    have "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* R"
      by simp+
    from ‹Ψ ⊳ Q ∥ R ⟼α ≺ QR› ‹bn α ♯* Ψ› ‹bn α ♯* Q›  ‹bn α ♯* R› ‹bn α ♯* subject α› ‹α ≠ τ› show ?case
    proof(induct rule: parCases[where C="(P, R, Ψ')"])
      case(cPar1 Q' A⇩R Ψ⇩R)
      from ‹A⇩R ♯* (P, R, Ψ')› have "A⇩R ♯* P" and "A⇩R ♯* Ψ'" by simp+
      have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
      from ‹A⇩R ♯* α› ‹bn α ♯* R› FrR
      have "bn α ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
      have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼α ≺ Q'" by fact
      from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "Ψ ⊗ Ψ⇩R ⊳ P ↝<Rel> Q"
        by(blast intro: PRelQ Sim)
      then obtain P'' P' where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹α ≺ P''"
                           and P''Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', P', Q') ∈ Rel"
        using QTrans ‹bn α ♯* Ψ› ‹bn α ♯* Ψ⇩R› ‹bn α ♯* P› ‹bn α ♯* R› ‹A⇩R ♯* α› ‹α ≠ τ›
        by(drule_tac Ψ'=Ψ' in weakSimE(1)) auto

      from PTrans QTrans ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)› 
      have "A⇩R ♯* P''" and "A⇩R ♯* Q'"
        by(fastforce dest: weakFreshChainDerivative freeFreshChainDerivative)+
      with P''Chain have "A⇩R ♯* P'" by(force dest: tauChainFreshChain)
      
      from PTrans FrR ‹bn α ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹A⇩R ♯* Q› 
      have "Ψ : Q ∥ R ⊳ P ∥ R ⟹α ≺ (P'' ∥ R)"
        by(rule_tac weakPar1)
      moreover from P''Chain have "(Ψ ⊗ Ψ') ⊗ Ψ⇩R ⊳ P'' ⟹⇧^⇩τ P'" 
        by(metis tauChainStatEq Associativity Commutativity Composition)
      with FrR have "Ψ ⊗ Ψ' ⊳ P'' ∥ R ⟹⇧^⇩τ P' ∥ R" using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* P''›
        by(rule_tac tauChainPar1) auto
      
      moreover from P'RelQ' have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R, P', Q') ∈ Rel" 
        by(metis C3 compositionSym Associativity Commutativity)
      hence "(Ψ ⊗ Ψ', P' ∥ R, Q' ∥ R) ∈ Rel'" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* P'› ‹A⇩R ♯* Q'›
        by(rule_tac C1) auto
      ultimately show ?case by blast
    next
      case(cPar2 R' A⇩Q Ψ⇩Q)
      from ‹A⇩Q ♯* (P, R, Ψ')› have "A⇩Q ♯* P" and "A⇩Q ♯* R" and "A⇩Q ♯* Ψ'" by simp+
      obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* (Ψ, A⇩Q, Ψ⇩Q, α, R)"
        by(rule freshFrame)
      hence "A⇩P ♯* Ψ" and "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* α" and "A⇩P ♯* R"
        by simp+

      have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
      from ‹A⇩Q ♯* P› FrP ‹A⇩P ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩P"
        by(drule_tac extractFrameFreshChain) auto

      from FrP FrQ ‹bn α ♯* P› ‹bn α ♯* Q› ‹A⇩P ♯* α› ‹A⇩Q ♯* α›
      have "bn α ♯* Ψ⇩P" and "bn α ♯* Ψ⇩Q"
        by(force dest: extractFrameFreshChain)+
      
      obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* (Ψ, P, Q, A⇩Q, A⇩P, Ψ⇩Q, Ψ⇩P, α, R, Ψ')" 
                      and "distinct A⇩R"
        by(rule freshFrame)
      then have "A⇩R ♯* Ψ" and "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* A⇩Q" and  "A⇩R ♯* A⇩P" and  "A⇩R ♯* Ψ⇩Q" and  "A⇩R ♯* Ψ⇩P"
            and "A⇩R ♯* α" and "A⇩R ♯* R" and "A⇩R ♯* Ψ'"
        by simp+

      from ‹A⇩Q ♯* R›  FrR ‹A⇩R ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
      from ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› FrR  have "A⇩P ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto

      moreover from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼α ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* α› ‹A⇩R ♯* Ψ'›
                 ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* Q› ‹bn α ♯* R› ‹bn α ♯* subject α› ‹distinct(bn α)›
      obtain p Ψ'' A⇩R' Ψ⇩R' where S: "set p ⊆ set(bn α) × set(bn(p ∙ α))" and "(p ∙ Ψ⇩R) ⊗ Ψ'' ≃ Ψ⇩R'"
                              and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
                              and "bn(p ∙ α) ♯* Ψ" and "bn(p ∙ α) ♯* P" and "bn(p ∙ α) ♯* Q"
                              and "A⇩R' ♯* Ψ" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ'" and "distinctPerm p"
        by(rule_tac C="(Ψ, Ψ', P, Q)" and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+

      from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q›
      have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule PRelQ)
      hence "(Ψ ⊗ Ψ⇩R, Q, P) ∈ Rel" by(rule Sym)
      hence "Ψ ⊗ Ψ⇩R ⊳ Q ⪅<Rel> P" by(rule StatImp)
      then obtain P' P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'"
                           and QimpP': "insertAssertion(extractFrame Q) (Ψ ⊗ Ψ⇩R) ↪⇩F insertAssertion(extractFrame P') (Ψ ⊗ Ψ⇩R)"
                          and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ ((p ∙ Ψ'') ⊗ (p ∙ Ψ')) ⊳ P' ⟹⇧^⇩τ P''"
                          and P'RelQ: "((Ψ ⊗ Ψ⇩R) ⊗ ((p ∙ Ψ'') ⊗ (p ∙ Ψ')), Q, P'') ∈ Rel"
        by(rule weakStatImpE)
      obtain A⇩P' Ψ⇩P' where FrP': "extractFrame P' = ⟨A⇩P', Ψ⇩P'⟩" and "A⇩P' ♯* Ψ" and "A⇩P' ♯* Ψ⇩R" and "A⇩P' ♯* Ψ⇩Q"
                        and "A⇩P' ♯* A⇩Q" and "A⇩P' ♯* R" and "A⇩P' ♯* A⇩R" and "A⇩P' ♯* α"
        by(rule_tac C="(Ψ, Ψ⇩R, Ψ⇩Q, A⇩Q, R, A⇩R, α)" in freshFrame) auto

      from PChain ‹A⇩R ♯* P› ‹A⇩Q ♯* P› ‹bn α ♯* P› have "A⇩Q ♯* P'" and "A⇩R ♯* P'" and "bn α ♯* P'"
        by(force intro: tauChainFreshChain)+
      from ‹A⇩R ♯* P'› ‹A⇩P' ♯* A⇩R› ‹A⇩Q ♯* P'› ‹A⇩P' ♯* A⇩Q› FrP' have "A⇩Q ♯* Ψ⇩P'" and "A⇩R ♯* Ψ⇩P'"
        by(force dest: extractFrameFreshChain)+

      from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ P' ∥ R" by(rule tauChainPar1)
      moreover have "insertAssertion (extractFrame(Q ∥ R)) Ψ ↪⇩F insertAssertion(extractFrame(P' ∥ R)) Ψ"
      proof -
        have "⟨A⇩Q, Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
          by(metis Associativity Composition Commutativity AssertionStatEqTrans AssertionStatEqSym frameNilStatEq frameResChainPres)
        moreover from QimpP' FrQ FrP' ‹A⇩Q ♯* Ψ⇩R› ‹A⇩P' ♯* Ψ⇩R› ‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ› 
        have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩" using freshCompChain by simp
        moreover have "⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩ ≃⇩F ⟨A⇩P', Ψ ⊗ Ψ⇩P' ⊗ Ψ⇩R⟩"
          by(metis Associativity Composition Commutativity AssertionStatEqTrans AssertionStatEqSym frameNilStatEq frameResChainPres)
        ultimately have "⟨A⇩Q, Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P', Ψ ⊗ Ψ⇩P' ⊗ Ψ⇩R⟩"
          by(rule FrameStatEqImpCompose)
        hence "⟨(A⇩R@A⇩Q), Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R⟩ ↪⇩F ⟨(A⇩R@A⇩P'), Ψ ⊗ Ψ⇩P' ⊗ Ψ⇩R⟩"
          by(force intro: frameImpResChainPres simp add: frameChainAppend)
        with FrQ FrR FrP' ‹A⇩R ♯* A⇩Q› ‹A⇩P' ♯* A⇩R› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩P' ♯* Ψ⇩R› 
                          ‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩R ♯* Ψ› 
        show ?thesis
          by(simp add: frameChainAppend) (metis frameImpChainComm FrameStatImpTrans)
      qed
      moreover have RTrans: "Ψ ⊗ Ψ⇩P' ⊳ R ⟼α ≺ R'"
      proof -
        have "Ψ ⊗ Ψ⇩Q ⊳ R ⟼α ≺ R'" by fact
        moreover have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩P') ⊗ Ψ⇩R⟩"
        proof -
          have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
            by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym FrameStatEqSym)
          moreover with FrP' FrQ QimpP' ‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P' ♯* Ψ⇩R› ‹A⇩Q ♯* Ψ⇩R›
          have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩" using freshCompChain
            by simp
          moreover have "⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩ ≃⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩P') ⊗ Ψ⇩R⟩"
            by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym frameIntAssociativity[THEN FrameStatEqSym])
          ultimately show ?thesis
            by(rule FrameStatEqImpCompose)
        qed
        ultimately show ?thesis
          using ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩P'› ‹A⇩P' ♯* R› ‹A⇩Q ♯* R› ‹A⇩P' ♯* α› ‹A⇩Q ♯* α›
                ‹A⇩P' ♯* A⇩R› ‹A⇩R ♯* A⇩Q› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩Q ♯* Ψ⇩P'› FrR ‹distinct A⇩R›
          by(force intro: transferFrame)
      qed
      hence "Ψ ⊳ P' ∥ R ⟼α ≺ (P' ∥ R')" using FrP' ‹bn α ♯* P'› ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* R› ‹A⇩P' ♯* α› ‹A⇩P' ♯* α›
        by(rule_tac Par2)
      ultimately have "Ψ : (Q ∥ R) ⊳ P ∥ R ⟹α ≺ (P' ∥ R')"
        by(rule_tac weakTransitionI)
      moreover from PChain P'Chain ‹bn α ♯* P'› ‹bn(p ∙ α) ♯* P› ‹A⇩R' ♯* P› 
      have "bn α ♯* P''" and "bn(p ∙ α) ♯* P'" and "bn(p ∙ α) ♯* P''" and "A⇩R' ♯* P'" and "A⇩R' ♯* P''" 
        by(metis tauChainFreshChain)+
      from P'Chain have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'') ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ P'')"
        by(rule eqvts)
      with ‹bn α ♯* Ψ› ‹bn(p ∙ α) ♯* Ψ› ‹bn α ♯* P'› ‹bn(p ∙ α) ♯* P'› ‹bn α ♯* P''› ‹bn(p ∙ α) ♯* P''›
            S ‹distinctPerm p›
      have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ'' ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''"
        by(simp add: eqvts)
      hence "(Ψ ⊗ Ψ') ⊗ (p ∙ Ψ⇩R) ⊗ Ψ'' ⊳ P' ⟹⇧^⇩τ P''" 
        by(rule tauChainStatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans)
      with ‹(p ∙ Ψ⇩R) ⊗ Ψ'' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ') ⊗ Ψ⇩R' ⊳ P' ⟹⇧^⇩τ P''" by(metis tauChainStatEq compositionSym)
      hence "Ψ ⊗ Ψ' ⊳ P' ∥ R' ⟹⇧^⇩τ P'' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* Ψ'› ‹A⇩R' ♯* P'› by(rule_tac tauChainPar1) auto
      moreover from P'RelQ have "((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'') ⊗ (p ∙ Ψ'), P'', Q) ∈ Rel" by(rule Sym)
      with ‹eqvt Rel› have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'') ⊗ (p ∙ Ψ'), P'', Q)) ∈ Rel" by(rule eqvtI)
      with ‹bn α ♯* Ψ› ‹bn(p ∙ α) ♯* Ψ› ‹bn α ♯* P''› ‹bn(p ∙ α) ♯* P''› ‹bn α ♯* Q› ‹bn(p ∙ α) ♯* Q› S ‹distinctPerm p›
      have "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ'' ⊗ Ψ', P'', Q) ∈ Rel" by(simp add: eqvts)
      with ‹(p ∙ Ψ⇩R) ⊗ Ψ'' ≃ Ψ⇩R'› have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R', P'', Q) ∈ Rel" 
        by(rule_tac C3, auto) (metis Associativity Commutativity Composition AssertionStatEqTrans)
      with FrR' ‹A⇩R' ♯* Ψ›  ‹A⇩R' ♯* Ψ'› ‹A⇩R' ♯* P''› ‹A⇩R' ♯* Q› 
      have "(Ψ ⊗ Ψ', P'' ∥ R', Q ∥ R') ∈ Rel'" by(rule_tac C1) auto
      ultimately show ?case by blast
    next
      case cComm1
      from ‹τ ≠ τ› have False by simp
      thus ?case by simp
    next
      case cComm2
      from ‹τ ≠ τ› have False by simp
      thus ?case by simp
    qed
  next
    case(cTau QR)
    from ‹Ψ ⊳ Q ∥ R ⟼τ ≺ QR› show ?case
    proof(induct rule: parTauCases[where C="(P, R)"])
      case(cPar1 Q' A⇩R Ψ⇩R)
      from ‹A⇩R ♯* (P, R)› have "A⇩R ♯* P"
        by simp+
      have FrR: " extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
      with ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "Ψ ⊗ Ψ⇩R ⊳ P ↝<Rel> Q"
        by(blast intro: PRelQ Sim)
      moreover have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼τ ≺ Q'" by fact
      ultimately obtain P' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ⇩R, P', Q') ∈ Rel"
        by(force dest: weakSimE)
      from PChain QTrans ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "A⇩R ♯* P'" and "A⇩R ♯* Q'"
        by(force dest: freeFreshChainDerivative tauChainFreshChain)+
      from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ (P' ∥ R)"
        by(rule tauChainPar1)
      moreover from P'RelQ' FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'› ‹A⇩R ♯* Q'› have "(Ψ, P' ∥ R, Q' ∥ R) ∈ Rel'" by(rule C1)
      ultimately show ?case by blast
    next
      case(cPar2 R' A⇩Q Ψ⇩Q)
      from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+
      obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* (Ψ, A⇩Q, Ψ⇩Q, R)"
        by(rule freshFrame)
      hence "A⇩P ♯* Ψ" and "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* R"
        by simp+
      
      have FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
      from ‹A⇩Q ♯* P› FrP ‹A⇩P ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩P"
        by(drule_tac extractFrameFreshChain) auto
      
      obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* (Ψ, P, Q, A⇩Q, A⇩P, Ψ⇩Q, Ψ⇩P, R)" and "distinct A⇩R"
        by(rule freshFrame)
      then have "A⇩R ♯* Ψ" and "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* A⇩Q" and  "A⇩R ♯* A⇩P" and  "A⇩R ♯* Ψ⇩Q" and  "A⇩R ♯* Ψ⇩P"
            and "A⇩R ♯* R"
        by simp+

      from ‹A⇩Q ♯* R›  FrR ‹A⇩R ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto
      from ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› FrR  have "A⇩P ♯* Ψ⇩R" by(drule_tac extractFrameFreshChain) auto

      moreover from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼τ ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* R›
      obtain Ψ' A⇩R' Ψ⇩R' where "Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'" and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
                           and "A⇩R' ♯* Ψ" and "A⇩R' ♯* P" and "A⇩R' ♯* Q"
        by(rule_tac C="(Ψ, P, Q, R)" in expandTauFrame) (assumption | simp)+

      from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q›
      obtain P' P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'"
                      and QimpP': "insertAssertion(extractFrame Q) (Ψ ⊗ Ψ⇩R) ↪⇩F insertAssertion(extractFrame P') (Ψ ⊗ Ψ⇩R)"
                      and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''"
                      and P'RelQ: "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', Q, P'') ∈ Rel"
        by(metis StatImp PRelQ Sym weakStatImpE)
      obtain A⇩P' Ψ⇩P' where FrP': "extractFrame P' = ⟨A⇩P', Ψ⇩P'⟩" and "A⇩P' ♯* Ψ" and "A⇩P' ♯* Ψ⇩R" and "A⇩P' ♯* Ψ⇩Q"
                        and "A⇩P' ♯* A⇩Q" and "A⇩P' ♯* R" and "A⇩P' ♯* A⇩R"
        by(rule_tac C="(Ψ, Ψ⇩R, Ψ⇩Q, A⇩Q, R, A⇩R)" in freshFrame) auto

      from PChain P'Chain ‹A⇩R ♯* P› ‹A⇩Q ♯* P› ‹A⇩R' ♯* P› have "A⇩Q ♯* P'" and "A⇩R ♯* P'" and "A⇩R' ♯* P'" and "A⇩R' ♯* P''"
        by(force intro: tauChainFreshChain)+
      from ‹A⇩R ♯* P'› ‹A⇩P' ♯* A⇩R› ‹A⇩Q ♯* P'› ‹A⇩P' ♯* A⇩Q› FrP' have "A⇩Q ♯* Ψ⇩P'" and "A⇩R ♯* Ψ⇩P'"
        by(force dest: extractFrameFreshChain)+
      
      from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ P' ∥ R" by(rule tauChainPar1)
      moreover have RTrans: "Ψ ⊗ Ψ⇩P' ⊳ R ⟼τ ≺ R'"
      proof -
        have "Ψ ⊗ Ψ⇩Q ⊳ R ⟼τ ≺ R'" by fact
        moreover have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩P') ⊗ Ψ⇩R⟩"
        proof -
          have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩"
            by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym FrameStatEqSym)
          moreover with FrP' FrQ QimpP' ‹A⇩P' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P' ♯* Ψ⇩R› ‹A⇩Q ♯* Ψ⇩R›
          have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩" using freshCompChain
            by simp
          moreover have "⟨A⇩P', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'⟩ ≃⇩F ⟨A⇩P', (Ψ ⊗ Ψ⇩P') ⊗ Ψ⇩R⟩"
            by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym frameIntAssociativity[THEN FrameStatEqSym])
          ultimately show ?thesis
            by(rule FrameStatEqImpCompose)
        qed
        ultimately show ?thesis
          using ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩P'› ‹A⇩P' ♯* R› ‹A⇩Q ♯* R› 
                ‹A⇩P' ♯* A⇩R› ‹A⇩R ♯* A⇩Q› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩R ♯* Ψ⇩Q› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩P'› ‹A⇩Q ♯* Ψ⇩P'› FrR ‹distinct A⇩R›
          by(force intro: transferTauFrame)
      qed
      hence "Ψ ⊳ P' ∥ R ⟼τ ≺ (P' ∥ R')" using FrP' ‹A⇩P' ♯* Ψ› ‹A⇩P' ♯* R›
        by(rule_tac Par2) auto
      moreover from P'Chain have "Ψ ⊗ Ψ⇩R ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ P''" 
        by(rule tauChainStatEq) (metis Associativity)
      with ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "Ψ ⊗ Ψ⇩R' ⊳ P' ⟹⇧^⇩τ P''" by(metis tauChainStatEq compositionSym)
      hence "Ψ ⊳ P' ∥ R' ⟹⇧^⇩τ P'' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› by(rule_tac tauChainPar1)
      ultimately have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ (P'' ∥ R')"
        by(fastforce dest: rtrancl_into_rtrancl)

      moreover from P'RelQ ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P'', Q) ∈ Rel" by(blast intro: C3 Associativity compositionSym Sym)
      with FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P''› ‹A⇩R' ♯* Q› have "(Ψ, P'' ∥ R', Q ∥ R') ∈ Rel'" by(rule_tac C1) 
      ultimately show ?case by blast
    next
      case(cComm1 Ψ⇩R M N Q' A⇩Q Ψ⇩Q K xvec R' A⇩R)
      have  FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
      from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+

      have  FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
      from ‹A⇩R ♯* (P, R)› have "A⇩R ♯* P" and "A⇩R ♯* R" by simp+
      from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+

      have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼M⦇N⦈ ≺ Q'" and RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'"
        and MeqK: "Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R ⊢ M ↔K" by fact+

      from RTrans FrR ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* xvec› ‹A⇩R ♯* N› ‹xvec ♯* R› ‹xvec ♯* Q› ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩Q› ‹A⇩R ♯* Q›
                      ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ⇩Q› ‹xvec ♯* K› ‹A⇩R ♯* K› ‹A⇩R ♯* R› ‹xvec ♯* R› ‹A⇩R ♯* P› ‹xvec ♯* P›
                       ‹A⇩Q ♯* A⇩R› ‹A⇩Q ♯* xvec› ‹xvec ♯* K› ‹distinct xvec› ‹A⇩R ♯* N›
      obtain p Ψ' A⇩R' Ψ⇩R' where S: "set p ⊆ set xvec × set(p ∙ xvec)" and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩"
                             and "(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ" and "(p ∙ xvec) ♯* Ψ"
                             and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ⇩Q" and "(p ∙ xvec) ♯* K" and "(p ∙ xvec) ♯* R"
                             and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* A⇩Q" and "A⇩R' ♯* P" and "A⇩R' ♯* N"
        by(rule_tac C="(Ψ, Q, Ψ⇩Q, K, R, P, A⇩Q)" and C'="(Ψ, Q, Ψ⇩Q, K, R, P, A⇩Q)" in expandFrame) (assumption | simp)+

      from ‹A⇩R ♯* Ψ› have "(p ∙ A⇩R) ♯* (p ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have "(p ∙ A⇩R) ♯* Ψ" by simp
      from ‹A⇩R ♯* P› have "(p ∙ A⇩R) ♯* (p ∙ P)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S have "(p ∙ A⇩R) ♯* P" by simp
      from ‹A⇩R ♯* Q› have "(p ∙ A⇩R) ♯* (p ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S have "(p ∙ A⇩R) ♯* Q" by simp
      from ‹A⇩R ♯* R› have "(p ∙ A⇩R) ♯* (p ∙ R)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have "(p ∙ A⇩R) ♯* R" by simp
      from ‹A⇩R ♯* K› have "(p ∙ A⇩R) ♯* (p ∙ K)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹xvec ♯* K› ‹(p ∙ xvec) ♯* K› S have "(p ∙ A⇩R) ♯* K" by simp

      from ‹A⇩Q ♯* xvec› ‹(p ∙ xvec) ♯* A⇩Q› ‹A⇩Q ♯* M› S have "A⇩Q ♯* (p ∙ M)" by(simp add: freshChainSimps)
      from ‹A⇩Q ♯* xvec› ‹(p ∙ xvec) ♯* A⇩Q› ‹A⇩Q ♯* A⇩R› S have "A⇩Q ♯* (p ∙ A⇩R)" by(simp add: freshChainSimps)

      from QTrans S ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› have "(p ∙ (Ψ ⊗ Ψ⇩R)) ⊳ Q ⟼ (p ∙ M)⦇N⦈ ≺ Q'"
        by(rule_tac inputPermFrameSubject) (assumption | auto simp add: fresh_star_def)+
      with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have QTrans: "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊳ Q ⟼ (p ∙ M)⦇N⦈ ≺ Q'"
        by(simp add: eqvts)
      from FrR have "(p ∙ extractFrame R) = p ∙ ⟨A⇩R, Ψ⇩R⟩" by simp
      with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have FrR: "extractFrame R = ⟨(p ∙ A⇩R), (p ∙ Ψ⇩R)⟩"
        by(simp add: eqvts)

      from MeqK have "(p ∙ (Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R)) ⊢ (p ∙ M) ↔ (p ∙ K)" by(rule chanEqClosed)
      with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* Ψ⇩Q› ‹(p ∙ xvec) ♯* Ψ⇩Q› ‹xvec ♯* K› ‹(p ∙ xvec) ♯* K› S
      have MeqK: "Ψ ⊗ Ψ⇩Q ⊗ (p ∙ Ψ⇩R) ⊢ (p ∙ M) ↔ K" by(simp add: eqvts)

      from FrR ‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P› ‹(p ∙ A⇩R) ♯* Q›
      have "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ P ↝<Rel> Q" by(force intro: Sim PRelQ)

      with QTrans obtain P' P'' where PTrans: "Ψ ⊗ (p ∙ Ψ⇩R) : Q ⊳ P ⟹(p ∙ M)⦇N⦈ ≺ P''"
                                  and P''Chain: "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'"
                                  and P'RelQ': "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ', P', Q') ∈ Rel"
        by(fastforce dest: weakSimE)
      from PTrans QTrans ‹A⇩R' ♯* P› ‹A⇩R' ♯* Q› ‹A⇩R' ♯* N› have "A⇩R' ♯* P''" and "A⇩R' ♯* Q'"
        by(auto dest: weakInputFreshChainDerivative inputFreshChainDerivative)

      from PTrans FrQ RTrans FrR MeqK ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* P› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* R› ‹A⇩Q ♯* (p ∙ M)› ‹A⇩Q ♯* (p ∙ A⇩R)›
           ‹(p ∙ A⇩R) ♯* Ψ› ‹(p ∙ A⇩R) ♯* P› ‹(p ∙ A⇩R) ♯* Q› ‹(p ∙ A⇩R) ♯* R› ‹(p ∙ A⇩R) ♯* K› ‹xvec ♯* P› ‹distinct A⇩R›
      have "Ψ ⊳ P ∥ R ⟹⇩τ ⦇ν*xvec⦈(P'' ∥ R')" apply(rule_tac weakComm1)
        by(assumption | simp)+

      moreover from P''Chain ‹A⇩R' ♯* P''› have "A⇩R' ♯* P'" by(rule tauChainFreshChain)
      from ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ≃ Ψ ⊗ Ψ⇩R'"
        by(metis Associativity AssertionStatEqTrans AssertionStatEqSym compositionSym)
      with P''Chain have "Ψ ⊗ Ψ⇩R' ⊳ P'' ⟹⇧^⇩τ P'" by(rule tauChainStatEq)
      hence "Ψ ⊳ P'' ∥ R' ⟹⇧^⇩τ P' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P''› by(rule tauChainPar1)
      hence "Ψ ⊳ ⦇ν*xvec⦈(P'' ∥ R') ⟹⇧^⇩τ ⦇ν*xvec⦈(P' ∥ R')" using ‹xvec ♯* Ψ› by(rule tauChainResChainPres)
      ultimately have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ ⦇ν*xvec⦈(P' ∥ R')"
        by auto
      moreover from P'RelQ' ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P', Q') ∈ Rel"  by(metis C3 Associativity compositionSym)
      with FrR' ‹A⇩R' ♯* P'› ‹A⇩R' ♯* Q'› ‹A⇩R' ♯* Ψ› have "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule_tac C1)
      with ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ R'), ⦇ν*xvec⦈(Q' ∥ R')) ∈ Rel'"
        by(rule_tac C2)
      ultimately show ?case by blast
    next
      case(cComm2 Ψ⇩R M xvec N Q' A⇩Q Ψ⇩Q K R' A⇩R)
      have  FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
      from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+

      have  FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
      from ‹A⇩R ♯* (P, R)› have "A⇩R ♯* P" and "A⇩R ♯* R" by simp+
      from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+

      have QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'" and RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼K⦇N⦈ ≺ R'"
        and MeqK: "Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩R ⊢ M ↔K" by fact+

      from RTrans FrR ‹distinct A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* Q'› ‹A⇩R ♯* N› ‹A⇩R ♯* P› ‹A⇩R ♯* xvec› ‹A⇩R ♯* K›
      obtain Ψ' A⇩R' Ψ⇩R' where  ReqR': "Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'" and FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩" 
                           and "A⇩R' ♯* Ψ" and "A⇩R' ♯* P" and "A⇩R' ♯* Q'" and "A⇩R' ♯* N" and "A⇩R' ♯* xvec"
        by(rule_tac C="(Ψ, P, Q', N, xvec)" and C'="(Ψ, P, Q', N, xvec)" in expandFrame) (assumption | simp)+

      from FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› have "Ψ ⊗ Ψ⇩R ⊳ P ↝<Rel> Q" by(force intro: Sim PRelQ)

      with QTrans ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩R› ‹xvec ♯* P›
      obtain P'' P' where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹M⦇ν*xvec⦈⟨N⟩ ≺ P''"
                      and P''Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'"
                      and P'RelQ': "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', P', Q') ∈ Rel"
        by(fastforce dest: weakSimE)
      from PTrans obtain P''' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P'''"
                                and QimpP''': "insertAssertion (extractFrame Q) (Ψ ⊗ Ψ⇩R) ↪⇩F insertAssertion (extractFrame P''') (Ψ ⊗ Ψ⇩R)"
                                and P'''Trans: "Ψ ⊗ Ψ⇩R ⊳ P''' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P''"
        by(rule weakTransitionE)
      
      from PChain ‹A⇩R ♯* P› have "A⇩R ♯* P'''" by(rule tauChainFreshChain)

      obtain A⇩P''' Ψ⇩P''' where FrP''': "extractFrame P''' = ⟨A⇩P''', Ψ⇩P'''⟩" and "A⇩P''' ♯* (Ψ, A⇩Q, Ψ⇩Q, A⇩R, Ψ⇩R, M, N, K, R, P''', xvec)" and "distinct A⇩P'''"
        by(rule freshFrame)
      hence "A⇩P''' ♯* Ψ" and "A⇩P''' ♯* A⇩Q" and "A⇩P''' ♯* Ψ⇩Q" and "A⇩P''' ♯* M" and "A⇩P''' ♯* R"
        and "A⇩P''' ♯* N" and "A⇩P''' ♯* K" and "A⇩P''' ♯* A⇩R" and "A⇩P''' ♯* P'''" and "A⇩P''' ♯* xvec" and "A⇩P''' ♯* Ψ⇩R"
        by simp+

      have "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩" 
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover with QimpP''' FrP''' FrQ ‹A⇩P''' ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩P''' ♯* Ψ⇩R› ‹A⇩Q ♯* Ψ⇩R›
      have "⟨A⇩Q, (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q⟩ ↪⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'''⟩" using freshCompChain
        by simp
      moreover have "⟨A⇩P''', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P'''⟩ ≃⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩P''') ⊗ Ψ⇩R⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately have QImpP''': "⟨A⇩Q, (Ψ ⊗ Ψ⇩Q) ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P''', (Ψ ⊗ Ψ⇩P''') ⊗ Ψ⇩R⟩"
        by(rule FrameStatEqImpCompose)

      from PChain FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ P''' ∥ R" by(rule tauChainPar1)
      moreover from RTrans FrR P'''Trans MeqK QImpP''' FrP''' FrQ ‹distinct A⇩P'''› ‹distinct A⇩R› ‹A⇩P''' ♯* A⇩R› ‹A⇩Q ♯* A⇩R›
        ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'''› ‹A⇩R ♯* Q› ‹A⇩R ♯* R› ‹A⇩R ♯* K› ‹A⇩P''' ♯* Ψ› ‹A⇩P''' ♯* R›
        ‹A⇩P''' ♯* P'''› ‹A⇩P''' ♯* M› ‹A⇩Q ♯* R›  ‹A⇩Q ♯* M› ‹A⇩R ♯* xvec› ‹xvec ♯* M›
      obtain K' where "Ψ ⊗ Ψ⇩P''' ⊳ R ⟼K'⦇N⦈ ≺ R'" and "Ψ ⊗ Ψ⇩P''' ⊗ Ψ⇩R ⊢ M ↔ K'" and "A⇩R ♯* K'"
        by(rule_tac comm2Aux) (assumption | simp)+

      with P'''Trans FrP''' have "Ψ ⊳ P''' ∥ R ⟼τ ≺ ⦇ν*xvec⦈(P'' ∥ R')" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'''› ‹A⇩R ♯* R›
          ‹xvec ♯* R› ‹A⇩P''' ♯* Ψ› ‹A⇩P''' ♯* P'''› ‹A⇩P''' ♯* R› ‹A⇩P''' ♯* M› ‹A⇩R ♯* K'› ‹A⇩P''' ♯* A⇩R›
        by(rule_tac Comm2)
      moreover from P'''Trans ‹A⇩R ♯* P'''› ‹A⇩R ♯* xvec› ‹xvec ♯* M› ‹distinct xvec› have "A⇩R ♯* P''"
        by(rule_tac outputFreshChainDerivative) auto

      from PChain ‹A⇩R' ♯* P› have "A⇩R' ♯* P'''" by(rule tauChainFreshChain)
      with P'''Trans have "A⇩R' ♯* P''" using ‹A⇩R' ♯* xvec› ‹xvec ♯* M› ‹distinct xvec›
        by(rule_tac outputFreshChainDerivative) auto

      with P''Chain have "A⇩R' ♯* P'" by(rule tauChainFreshChain)
      from ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ≃ Ψ ⊗ Ψ⇩R'"
        by(metis Associativity AssertionStatEqTrans AssertionStatEqSym compositionSym)
      with P''Chain have "Ψ ⊗ Ψ⇩R' ⊳ P'' ⟹⇧^⇩τ P'" by(rule tauChainStatEq)
      hence "Ψ ⊳ P'' ∥ R' ⟹⇧^⇩τ P' ∥ R'" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P''› 
        by(rule tauChainPar1)
      hence "Ψ ⊳ ⦇ν*xvec⦈(P'' ∥ R') ⟹⇧^⇩τ ⦇ν*xvec⦈(P' ∥ R')" 
        using ‹xvec ♯* Ψ› by(rule tauChainResChainPres)
      ultimately have "Ψ ⊳ P ∥ R ⟹⇧^⇩τ ⦇ν*xvec⦈(P' ∥ R')" by(drule_tac tauActTauChain) auto
      moreover from P'RelQ' ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', P', Q') ∈ Rel"  by(metis C3 Associativity compositionSym)
      with FrR' ‹A⇩R' ♯* P'› ‹A⇩R' ♯* Q'› ‹A⇩R' ♯* Ψ› have "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'" by(rule_tac C1)
      with ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ R'), ⦇ν*xvec⦈(Q' ∥ R')) ∈ Rel'"
        by(rule_tac C2)
      ultimately show ?case by blast
    qed
  qed
qed
unbundle no relcomp_syntax
lemma weakSimBangPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "(Ψ, P, Q) ∈ Rel"
  and     "eqvt Rel''"
  and     "guarded P"
  and     "guarded Q"
  and     Rel'Rel: "Rel' ⊆ Rel"

  and     FrameParPres: "⋀Ψ' Ψ⇩U S T U A⇩U. ⟦(Ψ' ⊗ Ψ⇩U, S, T) ∈ Rel; extractFrame U = ⟨A⇩U, Ψ⇩U⟩; A⇩U ♯* Ψ'; A⇩U ♯* S; A⇩U ♯* T⟧ ⟹
                                            (Ψ', U ∥ S, U ∥ T) ∈ Rel"
  and     C1: "⋀Ψ' S T U. ⟦(Ψ', S, T) ∈ Rel; guarded S; guarded T⟧ ⟹ (Ψ', U ∥ !S, U ∥ !T) ∈ Rel''"
  and     ResPres: "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel"
  and     ResPres': "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel'; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel'"

  and     Closed: "⋀Ψ' S T p. (Ψ', S, T) ∈ Rel ⟹ ((p::name prm) ∙ Ψ', p ∙ S, p ∙ T) ∈ Rel"
  and     Closed': "⋀Ψ' S T p. (Ψ', S, T) ∈ Rel' ⟹ ((p::name prm) ∙ Ψ', p ∙ S, p ∙ T) ∈ Rel'"
  and     StatEq: "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel"
  and     StatEq': "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel'; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel'"
  and     Trans: "⋀Ψ' S T U. ⟦(Ψ', S, T) ∈ Rel; (Ψ', T, U) ∈ Rel⟧ ⟹ (Ψ', S, U) ∈ Rel"
  and     Trans': "⋀Ψ' S T U. ⟦(Ψ', S, T) ∈ Rel'; (Ψ', T, U) ∈ Rel'⟧ ⟹ (Ψ', S, U) ∈ Rel'"

  and     cSim: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ Ψ' ⊳ S ↝<Rel> T"
  and     cExt: "⋀Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
  and     cExt': "⋀Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel' ⟹ (Ψ' ⊗ Ψ'', S, T) ∈ Rel'"
  and     cSym: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', T, S) ∈ Rel"
  and     cSym': "⋀Ψ' S T. (Ψ', S, T) ∈ Rel' ⟹ (Ψ', T, S) ∈ Rel'"

  and     ParPres: "⋀Ψ' S T U. (Ψ', S, T) ∈ Rel ⟹ (Ψ', S ∥ U, T ∥ U) ∈ Rel"
  and     ParPres2: "⋀Ψ' S T. (Ψ', S, T) ∈ Rel ⟹ (Ψ', S ∥ S, T ∥ T) ∈ Rel"
  and     ParPres': "⋀Ψ' S T U. (Ψ', S, T) ∈ Rel' ⟹ (Ψ', U ∥ S, U ∥ T) ∈ Rel'"

  and     Assoc: "⋀Ψ' S T U. (Ψ', S ∥ (T ∥ U), (S ∥ T) ∥ U) ∈ Rel"
  and     Assoc': "⋀Ψ' S T U. (Ψ', S ∥ (T ∥ U), (S ∥ T) ∥ U) ∈ Rel'"
  and     ScopeExt: "⋀xvec Ψ' T S. ⟦xvec ♯* Ψ'; xvec ♯* T⟧ ⟹ (Ψ', ⦇ν*xvec⦈(S ∥ T), (⦇ν*xvec⦈S) ∥ T) ∈ Rel"
  and     ScopeExt': "⋀xvec Ψ' T S. ⟦xvec ♯* Ψ'; xvec ♯* T⟧ ⟹ (Ψ', ⦇ν*xvec⦈(S ∥ T), (⦇ν*xvec⦈S) ∥ T) ∈ Rel'"

  and     Compose: "⋀Ψ' S T U O. ⟦(Ψ', S, T) ∈ Rel; (Ψ', T, U) ∈ Rel''; (Ψ', U, O) ∈ Rel'⟧ ⟹ (Ψ', S, O) ∈ Rel''"

  and     rBangActE: "⋀Ψ' S α S'. ⟦Ψ' ⊳ !S ⟼α ≺ S'; guarded S; bn α ♯* S; α ≠ τ; bn α ♯* subject α⟧ ⟹ ∃T. Ψ' ⊳ S ⟼α ≺ T ∧ (𝟭, S', T ∥ !S) ∈ Rel'"
  and     rBangTauE: "⋀Ψ' S S'. ⟦Ψ' ⊳ !S ⟼τ ≺ S'; guarded S⟧ ⟹ ∃T. Ψ' ⊳ S ∥ S ⟼τ ≺ T ∧ (𝟭, S', T ∥ !S) ∈ Rel'"
  and     rBangTauI: "⋀Ψ' S S'. ⟦Ψ' ⊳ S ∥ S ⟹⇧^⇩τ S'; guarded S⟧ ⟹ ∃T. Ψ' ⊳ !S ⟹⇧^⇩τ T ∧ (Ψ', T, S' ∥ !S) ∈ Rel'"
  shows "Ψ ⊳ R ∥ !P ↝<Rel''> R ∥ !Q"
using ‹eqvt Rel''›
proof(induct rule: weakSimI[where C="()"])
  case(cAct Ψ' α RQ')
  from ‹bn α ♯* (R ∥ !P)› ‹bn α ♯* (R ∥ !Q)› have "bn α ♯* P" and "bn α ♯* (!Q)" and "bn α ♯* Q" and "bn α ♯* R"
    by simp+
  from ‹Ψ ⊳ R ∥ !Q ⟼α ≺ RQ'› ‹bn α ♯* Ψ› ‹bn α ♯* R› ‹bn α ♯* !Q› ‹bn α ♯* subject α› ‹α ≠ τ› show ?case
  proof(induct rule: parCases[where C="(Ψ', P, Q, R)"])
    case(cPar1 R' A⇩Q Ψ⇩Q)
    from ‹extractFrame (!Q) = ⟨A⇩Q, Ψ⇩Q⟩› have "A⇩Q = []" and "Ψ⇩Q = SBottom'" by simp+
    with ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼α ≺ R'› ‹Ψ⇩Q = SBottom'› ‹bn α ♯* Ψ› ‹bn α ♯* P›
    have "Ψ ⊳ R ∥ !P ⟼α ≺ (R' ∥ !P)" by(rule_tac Par1) (assumption | simp)+
    hence "Ψ : R ∥ !Q ⊳ R ∥ !P ⟹α ≺ R' ∥ !P" by(rule_tac transitionWeakTransition) auto
    moreover have "Ψ ⊗ Ψ' ⊳ R' ∥ !P ⟹⇧^⇩τ R' ∥ !P" by auto
    moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule cExt)
    hence "(Ψ ⊗ Ψ', R' ∥ !P, R' ∥ !Q) ∈ Rel''" using ‹guarded P› ‹guarded Q› 
      by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 Q' A⇩R Ψ⇩R)
    from ‹A⇩R ♯* (Ψ', P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* Ψ'" and "A⇩R ♯* R" by simp+
    have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
    with ‹bn α ♯* R› ‹A⇩R ♯* α› have "bn α ♯* Ψ⇩R" by(auto dest: extractFrameFreshChain)
    
    obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ⇩R" and "A⇩Q ♯* A⇩R"
      by(rule_tac C="(Ψ, Ψ⇩R, A⇩R)" in freshFrame) auto
    from FrQ ‹guarded Q› have "Ψ⇩Q ≃ 𝟭" and "supp Ψ⇩Q = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "A⇩R ♯* Ψ⇩Q" and "A⇩Q ♯* Ψ⇩Q" by(auto simp add: fresh_star_def fresh_def)

    from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼α ≺ Q'› ‹guarded Q› ‹bn α ♯* Q› ‹α ≠ τ› ‹bn α ♯* subject α›
    obtain T where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼α ≺ T" and "(𝟭, Q', T ∥ !Q) ∈ Rel'" 
      by(blast dest: rBangActE)
    
    from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
    with QTrans ‹bn α ♯* Ψ› ‹bn α ♯* Ψ⇩R› ‹bn α ♯* P› ‹α ≠ τ›
    obtain P'' S where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹α ≺ P''" 
                   and P''Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ S"
                   and SRelT: "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', S, T) ∈ Rel"
      by(blast dest: cSim weakSimE)
    from PTrans have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 : Q ⊳ P ⟹α ≺ P''"
      by(metis weakTransitionStatEq Identity AssertionStatEqSym)
    hence "Ψ ⊗ Ψ⇩R : Q ∥ !P ⊳ P ∥ !P ⟹α ≺ P'' ∥ !P" using ‹bn α ♯* P›
      by(force intro: weakPar1) 
    hence "Ψ ⊗ Ψ⇩R : Q ∥ !P ⊳ !P ⟹α ≺ P'' ∥ !P" using ‹guarded P›
      by(rule weakBang)
    hence "Ψ : R ∥ (Q ∥ !P) ⊳ R ∥ !P ⟹α ≺ R ∥ (P'' ∥ !P)" 
      using FrR ‹bn α ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Q›‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹A⇩R ♯* α›
      by(rule_tac weakPar2) auto
    moreover have "insertAssertion (extractFrame(R ∥ !Q)) Ψ ↪⇩F insertAssertion (extractFrame(R ∥ (Q ∥ !P))) Ψ"
    proof -
      have "insertAssertion (extractFrame(R ∥ !P)) Ψ = ⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ 𝟭⟩" using FrR ‹A⇩R ♯* Ψ›
        by auto
      moreover from ‹Ψ⇩Q ≃ 𝟭› have "⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ 𝟭⟩ ≃⇩F ⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩"
        by(rule_tac frameResChainPres, auto) (metis Identity compositionSym AssertionStatEqTrans AssertionStatEqSym)
      moreover have "⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩ ≃⇩F ⦇ν*A⇩Q⦈(⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩)" using ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩R› ‹A⇩Q ♯* A⇩R› freshCompChain
        by(subst frameResFreshChain[where xvec=A⇩Q, THEN FrameStatEqSym]) auto
      moreover have "⦇ν*A⇩Q⦈(⟨A⇩R, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩) ≃⇩F ⦇ν*A⇩R⦈(⟨A⇩Q, Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩)"
        by(rule frameResChainComm)
      moreover have "insertAssertion (extractFrame(R ∥ (Q ∥ !P))) Ψ = ⟨(A⇩R@A⇩Q), Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊗ 𝟭⟩" 
        using FrR FrQ ‹A⇩R ♯* Ψ› ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* A⇩R› ‹A⇩Q ♯* Ψ⇩R›  ‹A⇩R ♯* Ψ⇩Q›  freshCompChain
        by auto
      ultimately have "insertAssertion (extractFrame(R ∥ !P)) Ψ ≃⇩F insertAssertion (extractFrame(R ∥ (Q ∥ !P))) Ψ"
        by(auto simp add: frameChainAppend) (blast dest: FrameStatEqTrans)
      thus ?thesis by(simp add: FrameStatEq_def)
    qed
    ultimately have "Ψ : R ∥ !Q ⊳ R ∥ !P ⟹α ≺ R ∥ (P'' ∥ !P)" 
      by(rule weakTransitionFrameImp)

    moreover from PTrans ‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)›
    have "A⇩R ♯* P''" by(force dest: weakFreshChainDerivative)
    with P''Chain have "A⇩R ♯* S" by(force dest: tauChainFreshChain)
    from ‹Ψ ⊗ Ψ⇩R ⊳ Q ⟼α ≺ T› ‹A⇩R ♯* Q› ‹A⇩R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)› have "A⇩R ♯* T"
      by(force dest: freeFreshChainDerivative)

    from P''Chain have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P'' ⟹⇧^⇩τ S" 
      by(rule tauChainStatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym Identity)
    hence "(Ψ ⊗ Ψ') ⊗ Ψ⇩R ⊳ P'' ∥ !P ⟹⇧^⇩τ S ∥ !P"
      by(rule_tac tauChainPar1) auto
    hence "Ψ ⊗ Ψ' ⊳ R ∥ (P'' ∥ !P) ⟹⇧^⇩τ R ∥ (S ∥ !P)" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* P''› ‹A⇩R ♯* P›
      by(rule_tac tauChainPar2) auto
    moreover have "(Ψ ⊗ Ψ', R ∥ (S ∥ !P), R ∥ Q') ∈ Rel''"
    proof -
      from ‹((Ψ ⊗ Ψ⇩R) ⊗ Ψ', S, T) ∈ Rel› have "((Ψ ⊗ Ψ') ⊗ Ψ⇩R, S, T) ∈ Rel"
        by(rule StatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
      with FrR ‹A⇩R ♯* Ψ›  ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* S› ‹A⇩R ♯* T› have "(Ψ ⊗ Ψ', R ∥ S, R ∥ T) ∈ Rel"
        by(rule_tac FrameParPres) auto
      hence "(Ψ ⊗ Ψ', R ∥ T, R ∥ S) ∈ Rel" by(rule cSym)
      hence "(Ψ ⊗ Ψ', (R ∥ T) ∥ !P, (R ∥ S) ∥ !P) ∈ Rel" by(rule ParPres)
      hence "(Ψ ⊗ Ψ', (R ∥ S) ∥ !P, (R ∥ T) ∥ !P) ∈ Rel" by(rule cSym)
      hence "(Ψ ⊗ Ψ', R ∥ (S ∥ !P), (R ∥ T) ∥ !P) ∈ Rel" by(metis Trans Assoc)
      moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule cExt)
      hence "(Ψ ⊗ Ψ', (R ∥ T) ∥ !P, (R ∥ T) ∥ !Q) ∈ Rel''" using ‹guarded P› ‹guarded Q› by(rule C1)
      moreover from ‹(𝟭, Q', T ∥ !Q) ∈ Rel'› have "(𝟭 ⊗ Ψ ⊗ Ψ', Q', T ∥ !Q) ∈ Rel'" by(rule cExt')
      hence "(Ψ ⊗ Ψ', Q', T ∥ !Q) ∈ Rel'" 
        by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
      hence "(Ψ ⊗ Ψ', R ∥ Q', R ∥ (T ∥ !Q)) ∈ Rel'" by(rule ParPres')
      hence "(Ψ ⊗ Ψ', R ∥ Q', (R ∥ T) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
      hence "(Ψ ⊗ Ψ', (R ∥ T) ∥ !Q, R ∥ Q') ∈ Rel'" by(rule cSym')
      ultimately show ?thesis by(rule_tac Compose)
    qed
    ultimately show ?case by blast
  next
    case cComm1
    from ‹τ ≠ τ› have False by simp
    thus ?case by simp
  next
    case cComm2
    from ‹τ ≠ τ› have False by simp
    thus ?case by simp
  qed
next
  case(cTau RQ')
  from ‹Ψ ⊳ R ∥ !Q ⟼τ ≺ RQ'› show ?case
  proof(induct rule: parTauCases[where C="(P, Q, R)"])
    case(cPar1 R' A⇩Q Ψ⇩Q)
    from ‹extractFrame (!Q) = ⟨A⇩Q, Ψ⇩Q⟩› have "A⇩Q = []" and "Ψ⇩Q = SBottom'" by simp+
    with ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼τ ≺ R'› ‹Ψ⇩Q = SBottom'›
    have "Ψ ⊳ R ∥ !P ⟼τ ≺ (R' ∥ !P)" by(rule_tac Par1) (assumption | simp)+
    hence "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ R' ∥ !P" by auto
    moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have "(Ψ, R' ∥ !P, R' ∥ !Q) ∈ Rel''"
      by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 Q' A⇩R Ψ⇩R)
    from ‹A⇩R ♯* (P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" by simp+
    have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
    
    obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Ψ⇩R" and "A⇩Q ♯* A⇩R"
      by(rule_tac C="(Ψ, Ψ⇩R, A⇩R)" in freshFrame) auto
    from FrQ ‹guarded Q› have "Ψ⇩Q ≃ 𝟭" and "supp Ψ⇩Q = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "A⇩R ♯* Ψ⇩Q" and "A⇩Q ♯* Ψ⇩Q" by(auto simp add: fresh_star_def fresh_def)

    from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼τ ≺ Q'› ‹guarded Q› 
    obtain T where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ∥ Q ⟼τ ≺ T" and "(𝟭, Q', T ∥ !Q) ∈ Rel'" 
      by(blast dest: rBangTauE)
    
    from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
    hence "(Ψ ⊗ Ψ⇩R, P ∥ P, Q ∥ Q) ∈ Rel" by(rule ParPres2)
    with QTrans 
    obtain S where PTrans: "Ψ ⊗ Ψ⇩R ⊳ P ∥ P ⟹⇧^⇩τ S" and SRelT: "(Ψ ⊗ Ψ⇩R, S, T) ∈ Rel"
      by(blast dest: cSim weakSimE)
    from PTrans ‹guarded P› obtain U where PChain: "Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇧^⇩τ U" and "(Ψ ⊗ Ψ⇩R, U, S ∥ !P) ∈ Rel'"
      by(blast dest: rBangTauI)
    from PChain ‹A⇩R ♯* P› have "A⇩R ♯* U" by(force dest: tauChainFreshChain)
    from ‹Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇧^⇩τ U› FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› have "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ R ∥ U"
      by(rule_tac tauChainPar2) auto
    moreover from PTrans ‹A⇩R ♯* P› have "A⇩R ♯* S" by(force dest: tauChainFreshChain)
    from QTrans ‹A⇩R ♯* Q› have "A⇩R ♯* T" by(force dest: tauFreshChainDerivative)
    have "(Ψ, R ∥ U, R ∥ Q') ∈ Rel''"
    proof -
      from ‹(Ψ ⊗ Ψ⇩R, U, S ∥ !P) ∈ Rel'› Rel'Rel have "(Ψ ⊗ Ψ⇩R, U, S ∥ !P) ∈ Rel"
        by auto
      hence "(Ψ, R ∥ U, R ∥ (S ∥ !P)) ∈ Rel" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* U› ‹A⇩R ♯* S› ‹A⇩R ♯* P›
        by(rule_tac FrameParPres) auto

      moreover from ‹(Ψ ⊗ Ψ⇩R, S, T) ∈ Rel› FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* S› ‹A⇩R ♯* T› have "(Ψ, R ∥ S, R ∥ T) ∈ Rel"
        by(rule_tac FrameParPres) auto
      hence "(Ψ, R ∥ T, R ∥ S) ∈ Rel" by(rule cSym)
      hence "(Ψ, (R ∥ T) ∥ !P, (R ∥ S) ∥ !P) ∈ Rel" by(rule ParPres)
      hence "(Ψ, (R ∥ S) ∥ !P, (R ∥ T) ∥ !P) ∈ Rel" by(rule cSym)
      hence "(Ψ, R ∥ (S ∥ !P), (R ∥ T) ∥ !P) ∈ Rel" by(metis Trans Assoc)
      ultimately have "(Ψ, R ∥ U, (R ∥ T) ∥ !P) ∈ Rel" by(rule Trans)
      moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ, (R ∥ T) ∥ !P, (R ∥ T) ∥ !Q) ∈ Rel''" using ‹guarded P› ‹guarded Q› by(rule C1)
      moreover from ‹(𝟭, Q', T ∥ !Q) ∈ Rel'› have "(𝟭 ⊗ Ψ, Q', T ∥ !Q) ∈ Rel'" by(rule cExt')
      hence "(Ψ, Q', T ∥ !Q) ∈ Rel'" 
        by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
      hence "(Ψ, R ∥ Q', R ∥ (T ∥ !Q)) ∈ Rel'" by(rule ParPres')
      hence "(Ψ, R ∥ Q', (R ∥ T) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
      hence "(Ψ, (R ∥ T) ∥ !Q, R ∥ Q') ∈ Rel'" by(rule cSym')
      ultimately show ?thesis by(rule_tac Compose)
    qed
    ultimately show ?case by blast
  next
    case(cComm1 Ψ⇩Q M N R' A⇩R Ψ⇩R K xvec Q' A⇩Q)
    from ‹A⇩R ♯* (P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" by simp+
    from ‹xvec ♯* (P, Q, R)› have "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* R" by simp+
    have FrQ: "extractFrame(!Q) = ⟨A⇩Q, Ψ⇩Q⟩" by fact
    have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
    from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* N› ‹A⇩R ♯* xvec› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* M›
    obtain A⇩R' Ψ⇩R' Ψ' where FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩" and "Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'" and "A⇩R' ♯* xvec" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ"
      by(rule_tac C="(Ψ, xvec, P, Q)" and C'="(Ψ, xvec, P, Q)" in expandFrame) auto
    from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
    moreover from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'› ‹guarded Q› ‹xvec ♯* Q› ‹xvec ♯* K›
    obtain S where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ S" and "(𝟭, Q', S ∥ !Q) ∈ Rel'"
      by(fastforce dest: rBangActE)
    ultimately obtain P' T where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹K⦇ν*xvec⦈⟨N⟩ ≺ P'" and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P' ⟹⇧^⇩τ T" and "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', T, S) ∈ Rel"
      using ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩R› ‹xvec ♯* P›
      by(fastforce dest: cSim weakSimE)

    from PTrans ‹A⇩R ♯* P› ‹A⇩R ♯* xvec› ‹A⇩R' ♯* P› ‹A⇩R' ♯* xvec› ‹xvec ♯* K› ‹distinct xvec›
    have "A⇩R ♯* P'" and  "A⇩R' ♯* P'"
      by(force dest: weakOutputFreshChainDerivative)+
    with P'Chain have "A⇩R' ♯* T" by(force dest: tauChainFreshChain)+
    from QTrans ‹A⇩R' ♯* Q› ‹A⇩R' ♯* xvec› ‹xvec ♯* K› ‹distinct xvec› 
    have "A⇩R' ♯* S" by(force dest: outputFreshChainDerivative)

    obtain A⇩Q' Ψ⇩Q' where FrQ': "extractFrame Q = ⟨A⇩Q', Ψ⇩Q'⟩" and "A⇩Q' ♯* Ψ" and "A⇩Q' ♯* Ψ⇩R" and "A⇩Q' ♯* A⇩R" and "A⇩Q' ♯* M" and "A⇩Q' ♯* R" and "A⇩Q' ♯* K"
      by(rule_tac C="(Ψ, Ψ⇩R, A⇩R, K, M, R)" in freshFrame) auto
    from FrQ' ‹guarded Q› have "Ψ⇩Q' ≃ 𝟭" and "supp Ψ⇩Q' = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "A⇩Q' ♯* Ψ⇩Q'" by(auto simp add: fresh_star_def fresh_def)

    from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P''"
                             and NilImpP'': "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩R)"
                             and P''Trans: "Ψ ⊗ Ψ⇩R ⊳ P'' ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'"
      using FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* Ψ⇩R› freshCompChain
      by(drule_tac weakTransitionE) auto

    from PChain have "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P))"
    proof(induct rule: tauChainCases)
      case TauBase
      from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'› FrQ have "Ψ ⊗ 𝟭 ⊳ R ⟼M⦇N⦈ ≺ R'" by simp
      moreover note FrR
      moreover from P''Trans ‹P = P''› have "Ψ ⊗ Ψ⇩R ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'" by simp
      hence "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'" by(rule statEqTransition) (metis Identity AssertionStatEqSym)
      hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ !P)" using ‹xvec ♯* Ψ› ‹xvec ♯* Ψ⇩R› ‹xvec ♯* P›
        by(force intro: Par1)
      hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ !P)" using ‹guarded P› by(rule Bang)
      moreover from ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› FrQ have "Ψ ⊗ Ψ⇩R ⊗ 𝟭 ⊢ M ↔ K" by simp
      ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P))" using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P› ‹A⇩R ♯* M› ‹xvec ♯* R›
        by(force intro: Comm1)
      thus ?case by(rule tauActTauChain)
    next
      case TauStep
      obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* Ψ" and "A⇩P'' ♯* K" and "A⇩P'' ♯* Ψ⇩R" and "A⇩P'' ♯* R" and "A⇩P'' ♯* P''" and "A⇩P'' ♯* P"
                          and "A⇩P'' ♯* A⇩R" and "distinct A⇩P''"
        by(rule_tac C="(Ψ, K, A⇩R, Ψ⇩R, R, P'', P)" in freshFrame) auto
      from PChain ‹A⇩R ♯* P› have "A⇩R ♯* P''" by(drule_tac tauChainFreshChain) auto
      with FrP'' ‹A⇩P'' ♯* A⇩R› have "A⇩R ♯* Ψ⇩P''" by(drule_tac extractFrameFreshChain) auto
      from ‹Ψ ⊗ Ψ⇩R ⊳ P ⟹⇩τ P''› have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟹⇩τ P''" by(rule tauStepChainStatEq) (metis Identity AssertionStatEqSym)
      hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟹⇩τ P'' ∥ !P" by(rule_tac tauStepChainPar1) auto
      hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇩τ P'' ∥ !P" using ‹guarded P› by(rule tauStepChainBang)
      hence  "Ψ ⊳ R ∥ !P ⟹⇩τ R ∥ (P'' ∥ !P)" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P›
        by(rule_tac tauStepChainPar2) auto
      moreover have "Ψ ⊳ R ∥ (P'' ∥ !P) ⟼τ ≺ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P))"
      proof -
        from FrQ ‹Ψ⇩Q' ≃ 𝟭› ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'› have "Ψ ⊗ Ψ⇩Q' ⊳ R ⟼M⦇N⦈ ≺ R'"
          by simp (metis statEqTransition AssertionStatEqSym compositionSym)
        moreover from P''Trans have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P'' ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'"
          by(rule statEqTransition) (metis Identity AssertionStatEqSym)
        hence P''PTrans: "Ψ ⊗ Ψ⇩R ⊳ P'' ∥ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ !P)" using ‹xvec ♯* P›
          by(rule_tac Par1) auto
        moreover from FrP'' have FrP''P: "extractFrame(P'' ∥ !P) = ⟨A⇩P'', Ψ⇩P'' ⊗ 𝟭⟩"
          by auto
        moreover from FrQ ‹Ψ⇩Q' ≃ 𝟭› ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› have "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ M ↔ K"
          by simp (metis statEqEnt Composition AssertionStatEqSym Commutativity)
        hence "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ K ↔ M" by(rule chanEqSym)
        moreover have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭)) ⊗ Ψ⇩R⟩"
        proof -
          have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩"
            by(rule_tac frameResChainPres, simp)
              (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
          moreover from NilImpP'' FrQ FrP'' ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩R› freshCompChain have "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩"
            by auto
          moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R⟩"
            by(rule frameResChainPres, simp) 
              (metis Identity AssertionStatEqSym Associativity Commutativity Composition AssertionStatEqTrans)
          ultimately show ?thesis by(rule FrameStatEqImpCompose)
        qed
        ultimately obtain M' where RTrans: "Ψ ⊗ Ψ⇩P'' ⊗ 𝟭 ⊳ R ⟼M'⦇N⦈ ≺ R'" and "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'" and "A⇩R ♯* M'"
          using FrR FrQ' ‹distinct A⇩R› ‹distinct A⇩P''› ‹A⇩P'' ♯* A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P''› ‹A⇩R ♯* Q› ‹A⇩R ♯* R›  ‹A⇩R ♯* M› ‹A⇩Q' ♯* R› ‹A⇩Q' ♯* K› ‹A⇩Q' ♯* A⇩R› ‹A⇩R ♯* P› ‹A⇩P'' ♯* P› ‹A⇩R ♯* xvec›
                     ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R›  ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* K› ‹xvec ♯* K› ‹distinct xvec›
          by(rule_tac A⇩Q="A⇩Q'" and Q="Q" in comm2Aux) (assumption | simp)+

        note RTrans FrR P''PTrans FrP''P
        moreover from ‹Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'› have "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ M' ↔ K" by(rule chanEqSym)
        hence "Ψ ⊗ Ψ⇩R ⊗ Ψ⇩P'' ⊗ 𝟭 ⊢ M' ↔ K" by(metis statEqEnt Composition AssertionStatEqSym Commutativity)
        ultimately show ?thesis using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P''› ‹A⇩R ♯* P› ‹A⇩R ♯* M'› ‹A⇩P'' ♯* A⇩R› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* P› ‹A⇩P'' ♯* K› ‹xvec ♯* R›
          by(rule_tac Comm1) (assumption | simp)+
      qed
      ultimately show ?thesis
        by(drule_tac tauActTauChain) auto
    qed

    moreover from P'Chain have "((Ψ ⊗ Ψ⇩R) ⊗ Ψ') ⊗ 𝟭 ⊳ P' ⟹⇧^⇩τ T"
      by(rule tauChainStatEq) (metis Identity AssertionStatEqSym)
    hence "(Ψ ⊗ Ψ⇩R) ⊗ Ψ' ⊳ P' ∥ !P ⟹⇧^⇩τ T ∥ !P"
      by(rule_tac tauChainPar1) auto
    hence "Ψ ⊗ Ψ⇩R ⊗ Ψ' ⊳ P' ∥ !P ⟹⇧^⇩τ T ∥ !P"
      by(rule tauChainStatEq) (metis Associativity)
    hence "Ψ ⊗ Ψ⇩R' ⊳ P' ∥ !P⟹⇧^⇩τ T ∥ !P" using ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'›
      by(rule_tac tauChainStatEq) (auto intro: compositionSym)
    hence "Ψ ⊳ R' ∥ (P' ∥ !P) ⟹⇧^⇩τ R' ∥ (T ∥ !P)" using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P› ‹A⇩R' ♯* P'›
      by(rule_tac tauChainPar2) auto
    hence "Ψ ⊳ ⦇ν*xvec⦈(R' ∥ (P' ∥ !P)) ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ (T ∥ !P))" using ‹xvec ♯* Ψ›
      by(rule tauChainResChainPres)
    ultimately have "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ (T ∥ !P))"
      by auto
    moreover have "(Ψ, ⦇ν*xvec⦈(R' ∥ (T ∥ !P)), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel''"
    proof -
      from ‹((Ψ ⊗ Ψ⇩R) ⊗ Ψ', T, S) ∈ Rel› have "(Ψ ⊗ Ψ⇩R ⊗ Ψ', T, S) ∈ Rel"
        by(rule StatEq) (metis Associativity)
      hence "(Ψ ⊗ Ψ⇩R', T, S) ∈ Rel" using ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'›
        by(rule_tac StatEq) (auto dest: compositionSym)

      with FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* S› ‹A⇩R' ♯* T› have "(Ψ, R' ∥ T, R' ∥ S) ∈ Rel"
        by(rule_tac FrameParPres) auto
      hence "(Ψ, (R' ∥ T) ∥ !P, (R' ∥ S) ∥ !P) ∈ Rel" by(rule ParPres)
      hence "(Ψ, ⦇ν*xvec⦈((R' ∥ T) ∥ !P), ⦇ν*xvec⦈((R' ∥ S) ∥ !P)) ∈ Rel" using ‹xvec ♯* Ψ›
        by(rule ResPres)
      hence "(Ψ, ⦇ν*xvec⦈(R' ∥ T) ∥ !P, (⦇ν*xvec⦈(R' ∥ S)) ∥ !P) ∈ Rel" using ‹xvec ♯* Ψ› ‹xvec ♯* P›
        by(force intro: Trans ScopeExt)
      hence "(Ψ, ⦇ν*xvec⦈(R' ∥ (T ∥ !P)), (⦇ν*xvec⦈(R' ∥ S)) ∥ !P) ∈ Rel" using ‹xvec ♯* Ψ›
        by(force intro: Trans ResPres Assoc)

      moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have "(Ψ, (⦇ν*xvec⦈(R' ∥ S)) ∥ !P, (⦇ν*xvec⦈(R' ∥ S)) ∥ !Q) ∈ Rel''"
        by(rule C1)
      moreover from ‹(𝟭, Q', S ∥ !Q) ∈ Rel'› have "(𝟭 ⊗ Ψ, Q', S ∥ !Q) ∈ Rel'" by(rule cExt')
      hence "(Ψ, Q', S ∥ !Q) ∈ Rel'" 
        by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
      hence "(Ψ, R' ∥ Q', R' ∥ (S ∥ !Q)) ∈ Rel'" by(rule ParPres')
      hence "(Ψ, R' ∥ Q', (R' ∥ S) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
      hence "(Ψ, (R' ∥ S) ∥ !Q, R' ∥ Q') ∈ Rel'" by(rule cSym')
      hence "(Ψ, ⦇ν*xvec⦈((R' ∥ S) ∥ !Q), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ›
        by(rule ResPres')
      hence "(Ψ, (⦇ν*xvec⦈(R' ∥ S)) ∥ !Q, ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ› ‹xvec ♯* Q›
        by(force intro: Trans' ScopeExt'[THEN cSym'])
      ultimately show ?thesis by(rule_tac Compose)
    qed
    ultimately show ?case by blast
  next
    case(cComm2 Ψ⇩Q M xvec N R' A⇩R Ψ⇩R K Q' A⇩Q)
    from ‹A⇩R ♯* (P, Q, R)› have "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" by simp+
    from ‹xvec ♯* (P, Q, R)› have "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* R" by simp+
    have FrQ: "extractFrame(!Q) = ⟨A⇩Q, Ψ⇩Q⟩" by fact
    have FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact
    from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*xvec⦈⟨N⟩ ≺ R'› FrR ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* N› ‹A⇩R ♯* xvec› ‹A⇩R ♯* P› ‹A⇩R ♯* Q› ‹A⇩R ♯* Ψ› ‹xvec ♯* R› ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* Q› ‹xvec ♯* M› ‹distinct xvec› ‹A⇩R ♯* M›
    obtain p A⇩R' Ψ⇩R' Ψ' where FrR': "extractFrame R' = ⟨A⇩R', Ψ⇩R'⟩" and "(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'" and "A⇩R' ♯* xvec" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "A⇩R' ♯* Ψ" and S: "set p ⊆ set xvec × set(p ∙ xvec)" and "distinctPerm p" and "(p ∙ xvec) ♯* N" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* R'" and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Ψ" and "A⇩R' ♯* N" and "A⇩R' ♯* xvec" and "A⇩R' ♯* (p ∙ xvec)"
      by(rule_tac C="(Ψ, P, Q)"  and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+

    from ‹Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*xvec⦈⟨N⟩ ≺ R'› S ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* R'›
    have  RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')"
      by(simp add: boundOutputChainAlpha'' residualInject)
    from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ⇩R, P, Q) ∈ Rel" by(rule cExt)
    moreover from ‹Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇N⦈ ≺ Q'› S ‹(p ∙ xvec) ♯* Q›  ‹xvec ♯* Q› ‹distinctPerm p›
    have "Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇(p ∙ N)⦈ ≺ (p ∙ Q')" 
      by(rule_tac inputAlpha) auto
    then obtain S where QTrans: "Ψ ⊗ Ψ⇩R ⊳ Q ⟼K⦇(p ∙ N)⦈ ≺ S" and "(𝟭, (p ∙ Q'), S ∥ !Q) ∈ Rel'" 
      using ‹guarded Q›
      by(fastforce dest: rBangActE)
    ultimately obtain P' T where PTrans: "Ψ ⊗ Ψ⇩R : Q ⊳ P ⟹K⦇(p ∙ N)⦈ ≺ P'" 
                             and P'Chain: "(Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ') ⊳ P' ⟹⇧^⇩τ T" 
                             and "((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'), T, S) ∈ Rel"
      by(fastforce dest: cSim weakSimE)

    from ‹A⇩R' ♯* N› ‹A⇩R' ♯* xvec› ‹A⇩R' ♯* (p ∙ xvec)› S have "A⇩R' ♯* (p ∙ N)"
      by(simp add: freshChainSimps)
    with PTrans ‹A⇩R' ♯* P› have "A⇩R' ♯* P'" by(force dest: weakInputFreshChainDerivative)
    with P'Chain have "A⇩R' ♯* T" by(force dest: tauChainFreshChain)+
    from QTrans ‹A⇩R' ♯* Q› ‹A⇩R' ♯* (p ∙ N)› have "A⇩R' ♯* S" by(force dest: inputFreshChainDerivative)

    obtain A⇩Q' Ψ⇩Q' where FrQ': "extractFrame Q = ⟨A⇩Q', Ψ⇩Q'⟩" and "A⇩Q' ♯* Ψ" and "A⇩Q' ♯* Ψ⇩R" and "A⇩Q' ♯* A⇩R" and "A⇩Q' ♯* M" and "A⇩Q' ♯* R" and "A⇩Q' ♯* K"
      by(rule_tac C="(Ψ, Ψ⇩R, A⇩R, K, M, R)" in freshFrame) auto
    from FrQ' ‹guarded Q› have "Ψ⇩Q' ≃ 𝟭" and "supp Ψ⇩Q' = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "A⇩Q' ♯* Ψ⇩Q'" by(auto simp add: fresh_star_def fresh_def)

    from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ⇩R ⊳ P ⟹⇧^⇩τ P''"
                             and NilImpP'': "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ⇩R)"
                             and P''Trans: "Ψ ⊗ Ψ⇩R ⊳ P'' ⟼K⦇(p ∙ N)⦈ ≺ P'"
      using FrQ' ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* Ψ⇩R› freshCompChain
      by(drule_tac weakTransitionE) auto

    from ‹(p ∙ xvec) ♯* P› ‹xvec ♯* P› PChain have "(p ∙ xvec) ♯* P''" and "xvec ♯* P''" 
      by(force dest: tauChainFreshChain)+
    from ‹(p ∙ xvec) ♯* N› ‹distinctPerm p› have "xvec ♯* (p ∙ N)"
      by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, where pi=p, symmetric]) simp
    with P''Trans ‹xvec ♯* P''› have "xvec ♯* P'" by(force dest: inputFreshChainDerivative)
    hence "(p ∙ xvec) ♯* (p ∙ P')" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])

    from PChain have "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ (P' ∥ !P))"
    proof(induct rule: tauChainCases)
      case TauBase
      from RTrans FrQ have "Ψ ⊗ 𝟭 ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')" by simp
      moreover note FrR
      moreover from P''Trans ‹P = P''› have "Ψ ⊗ Ψ⇩R ⊳ P ⟼K⦇(p ∙ N)⦈≺ P'" by simp
      hence "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟼K⦇(p ∙ N)⦈ ≺ P'" 
        by(rule statEqTransition) (metis Identity AssertionStatEqSym)
      hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟼K⦇(p ∙ N)⦈ ≺ (P' ∥ !P)" by(force intro: Par1)
      hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟼K⦇(p ∙ N)⦈ ≺ (P' ∥ !P)" using ‹guarded P› by(rule Bang)
      moreover from ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› FrQ have "Ψ ⊗ Ψ⇩R ⊗ 𝟭 ⊢ M ↔ K" by simp
      ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ (P' ∥ !P))" using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P› ‹A⇩R ♯* M› ‹(p ∙ xvec) ♯* P›
        by(force intro: Comm2)
      thus ?case by(rule tauActTauChain)
    next
      case TauStep
      obtain A⇩P'' Ψ⇩P'' where FrP'': "extractFrame P'' = ⟨A⇩P'', Ψ⇩P''⟩" and "A⇩P'' ♯* Ψ" and "A⇩P'' ♯* K" and "A⇩P'' ♯* Ψ⇩R" and "A⇩P'' ♯* R" and "A⇩P'' ♯* P''" and "A⇩P'' ♯* P"
                          and "A⇩P'' ♯* A⇩R" and "distinct A⇩P''"
        by(rule_tac C="(Ψ, K, A⇩R, Ψ⇩R, R, P'', P)" in freshFrame) auto
      from PChain ‹A⇩R ♯* P› have "A⇩R ♯* P''" by(drule_tac tauChainFreshChain) auto
      with FrP'' ‹A⇩P'' ♯* A⇩R› have "A⇩R ♯* Ψ⇩P''" by(drule_tac extractFrameFreshChain) auto
      from ‹Ψ ⊗ Ψ⇩R ⊳ P ⟹⇩τ P''› have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P ⟹⇩τ P''" by(rule tauStepChainStatEq) (metis Identity AssertionStatEqSym)
      hence "Ψ ⊗ Ψ⇩R ⊳ P ∥ !P ⟹⇩τ P'' ∥ !P" by(rule_tac tauStepChainPar1) auto
      hence "Ψ ⊗ Ψ⇩R ⊳ !P ⟹⇩τ P'' ∥ !P" using ‹guarded P› by(rule tauStepChainBang)
      hence  "Ψ ⊳ R ∥ !P ⟹⇩τ R ∥ (P'' ∥ !P)" using FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P›
        by(rule_tac tauStepChainPar2) auto
      moreover have "Ψ ⊳ R ∥ (P'' ∥ !P) ⟼τ ≺ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ (P' ∥ !P))"
      proof -
        from FrQ ‹Ψ⇩Q' ≃ 𝟭› RTrans have "Ψ ⊗ Ψ⇩Q' ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')"
          by simp (metis statEqTransition AssertionStatEqSym compositionSym)
        moreover from P''Trans have "(Ψ ⊗ Ψ⇩R) ⊗ 𝟭 ⊳ P'' ⟼K⦇(p ∙ N)⦈ ≺ P'"
          by(rule statEqTransition) (metis Identity AssertionStatEqSym)
        hence P''PTrans: "Ψ ⊗ Ψ⇩R ⊳ P'' ∥ !P ⟼K⦇(p ∙ N)⦈ ≺ (P' ∥ !P)"
          by(rule_tac Par1) auto
        moreover from FrP'' have FrP''P: "extractFrame(P'' ∥ !P) = ⟨A⇩P'', Ψ⇩P'' ⊗ 𝟭⟩"
          by auto
        moreover from FrQ ‹Ψ⇩Q' ≃ 𝟭› ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K› have "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ M ↔ K"
          by simp (metis statEqEnt Composition AssertionStatEqSym Commutativity)
        hence "Ψ ⊗ Ψ⇩Q' ⊗ Ψ⇩R ⊢ K ↔ M" by(rule chanEqSym)
        moreover have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭)) ⊗ Ψ⇩R⟩"
        proof -
          have "⟨A⇩Q', (Ψ ⊗ Ψ⇩Q') ⊗ Ψ⇩R⟩ ≃⇩F ⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩"
            by(rule_tac frameResChainPres, simp)
              (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
          moreover from NilImpP'' FrQ FrP'' ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* Ψ⇩R› freshCompChain have "⟨A⇩Q', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩Q'⟩ ↪⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩"
            by auto
          moreover have "⟨A⇩P'', (Ψ ⊗ Ψ⇩R) ⊗ Ψ⇩P''⟩ ≃⇩F ⟨A⇩P'', (Ψ ⊗ Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R⟩"
            by(rule frameResChainPres, simp) 
              (metis Identity AssertionStatEqSym Associativity Commutativity Composition AssertionStatEqTrans)
          ultimately show ?thesis by(rule FrameStatEqImpCompose)
        qed
        ultimately obtain M' where RTrans: "Ψ ⊗ Ψ⇩P'' ⊗ 𝟭 ⊳ R ⟼M'⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')" and "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'" and "A⇩R ♯* M'"
          using FrR FrQ' ‹distinct A⇩R› ‹distinct A⇩P''› ‹A⇩P'' ♯* A⇩R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P''› ‹A⇩R ♯* Q› ‹A⇩R ♯* R›  ‹A⇩R ♯* M› ‹A⇩Q' ♯* R› ‹A⇩Q' ♯* K› ‹A⇩Q' ♯* A⇩R› ‹A⇩R ♯* P› ‹A⇩P'' ♯* P›
                     ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R›  ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* K›
          by(rule_tac A⇩Q="A⇩Q'" and Q="Q" in comm1Aux) (assumption | simp)+

        note RTrans FrR P''PTrans FrP''P
        moreover from ‹Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ K ↔ M'› have "Ψ ⊗ (Ψ⇩P'' ⊗ 𝟭) ⊗ Ψ⇩R ⊢ M' ↔ K" by(rule chanEqSym)
        hence "Ψ ⊗ Ψ⇩R ⊗ Ψ⇩P'' ⊗ 𝟭 ⊢ M' ↔ K" by(metis statEqEnt Composition AssertionStatEqSym Commutativity)
        ultimately show ?thesis using ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* P''› ‹A⇩R ♯* P› ‹A⇩R ♯* M'› ‹A⇩P'' ♯* A⇩R› ‹A⇩P'' ♯* Ψ› ‹A⇩P'' ♯* R› ‹A⇩P'' ♯* P''› ‹A⇩P'' ♯* P› ‹A⇩P'' ♯* K› ‹(p ∙ xvec) ♯* P''› ‹(p ∙ xvec) ♯* P›
          by(rule_tac Comm2) (assumption | simp)+
      qed
      ultimately show ?thesis
        by(drule_tac tauActTauChain) auto
    qed
    hence "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ ((p ∙ P') ∥ !P))" 
      using ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* (p ∙ P')› ‹(p ∙ xvec) ♯* R'› S ‹distinctPerm p›
      by(subst resChainAlpha[where p=p]) auto
    moreover from P'Chain have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'))) ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ T)"
      by(rule tauChainEqvt)
    with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
    have "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ T)" by(simp add: eqvts)
    hence "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ') ⊗ 𝟭 ⊳ (p ∙ P') ⟹⇧^⇩τ (p ∙ T)"
      by(rule tauChainStatEq) (metis Identity AssertionStatEqSym)
    hence "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ (p ∙ P') ∥ !P ⟹⇧^⇩τ (p ∙ T) ∥ !P"
      by(rule_tac tauChainPar1) auto
    hence "Ψ ⊗ (p ∙ Ψ⇩R) ⊗ Ψ' ⊳ (p ∙ P') ∥ !P ⟹⇧^⇩τ (p ∙ T) ∥ !P"
      by(rule tauChainStatEq) (metis Associativity)
    hence "Ψ ⊗ Ψ⇩R' ⊳ (p ∙ P') ∥ !P ⟹⇧^⇩τ (p ∙ T) ∥ !P" using ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃  Ψ⇩R'›
      by(rule_tac tauChainStatEq) (auto intro: compositionSym)
    hence "Ψ ⊳ R' ∥ ((p ∙ P') ∥ !P) ⟹⇧^⇩τ R' ∥ ((p ∙ T) ∥ !P)" 
      using FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P› ‹A⇩R' ♯* P'› ‹A⇩R' ♯* xvec› ‹A⇩R' ♯* (p ∙ xvec)› S
      by(rule_tac tauChainPar2) (auto simp add: freshChainSimps)
    hence "Ψ ⊳ ⦇ν*xvec⦈(R' ∥ ((p ∙ P') ∥ !P)) ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P))" using ‹xvec ♯* Ψ›
      by(rule tauChainResChainPres)
    ultimately have "Ψ ⊳ R ∥ !P ⟹⇧^⇩τ ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P))"
      by auto
    moreover have "(Ψ, ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P)), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel''"
    proof -
      from ‹((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ'), T, S) ∈ Rel› 
      have "(p ∙ ((Ψ ⊗ Ψ⇩R) ⊗ (p ∙ Ψ')), (p ∙ T), (p ∙ S)) ∈ Rel"
        by(rule Closed)
      with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹distinctPerm p› S
      have "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ', p ∙ T, p ∙ S) ∈ Rel"
        by(simp add: eqvts)
      hence "(Ψ ⊗ (p ∙ Ψ⇩R) ⊗ Ψ', p ∙ T, p ∙ S) ∈ Rel"
        by(rule StatEq) (metis Associativity)
      hence "(Ψ ⊗ Ψ⇩R', p ∙ T, p ∙ S) ∈ Rel" using ‹(p ∙ Ψ⇩R) ⊗ Ψ' ≃ Ψ⇩R'›
        by(rule_tac StatEq) (auto dest: compositionSym)
      moreover from ‹A⇩R' ♯* S› ‹A⇩R' ♯* T› ‹A⇩R' ♯* xvec› ‹A⇩R' ♯* (p ∙ xvec)› S
      have "A⇩R' ♯* (p ∙ S)" and "A⇩R' ♯* (p ∙ T)"
        by(simp add: freshChainSimps)+
      ultimately have "(Ψ, R' ∥ (p ∙ T), R' ∥ (p ∙ S)) ∈ Rel" using FrR' ‹A⇩R' ♯* Ψ›
        by(rule_tac FrameParPres) auto
      hence "(Ψ, (R' ∥ (p ∙ T)) ∥ !P, (R' ∥ (p ∙ S)) ∥ !P) ∈ Rel" by(rule ParPres)
      hence "(Ψ, ⦇ν*xvec⦈((R' ∥ (p ∙ T)) ∥ !P), ⦇ν*xvec⦈((R' ∥ (p ∙ S)) ∥ !P)) ∈ Rel" 
        using ‹xvec ♯* Ψ›
        by(rule ResPres)
      hence "(Ψ, ⦇ν*xvec⦈(R' ∥ (p ∙ T)) ∥ !P, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !P) ∈ Rel" 
        using ‹xvec ♯* Ψ› ‹xvec ♯* P›
        by(force intro: Trans ScopeExt)
      hence "(Ψ, ⦇ν*xvec⦈(R' ∥ ((p ∙ T) ∥ !P)), (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !P) ∈ Rel"
        using ‹xvec ♯* Ψ›
        by(force intro: Trans ResPres Assoc)
      moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› 
      have "(Ψ, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !P, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !Q) ∈ Rel''"
        by(rule C1)
      moreover from ‹(𝟭, (p ∙ Q'), S ∥ !Q) ∈ Rel'› 
      have "(p ∙ 𝟭, p ∙ p ∙ Q', p ∙ (S ∥ !Q)) ∈ Rel'" by(rule Closed')
      with ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S ‹distinctPerm p› 
        have "(𝟭, Q', (p ∙ S) ∥ !Q) ∈ Rel'" by(simp add: eqvts)
      hence "(𝟭 ⊗ Ψ, Q', (p ∙ S) ∥ !Q) ∈ Rel'" by(rule cExt')
      hence "(Ψ, Q', (p ∙ S) ∥ !Q) ∈ Rel'" 
        by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
      hence "(Ψ, R' ∥ Q', R' ∥ ((p ∙ S) ∥ !Q)) ∈ Rel'" by(rule ParPres')
      hence "(Ψ, R' ∥ Q', (R' ∥ (p ∙ S)) ∥ !Q) ∈ Rel'" by(metis Trans' Assoc')
      hence "(Ψ, (R' ∥ (p ∙ S)) ∥ !Q, R' ∥ Q') ∈ Rel'" by(rule cSym')
      hence "(Ψ, ⦇ν*xvec⦈((R' ∥ (p ∙ S)) ∥ !Q), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ›
        by(rule ResPres')
      hence "(Ψ, (⦇ν*xvec⦈(R' ∥ (p ∙ S))) ∥ !Q, ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" using ‹xvec ♯* Ψ› ‹xvec ♯* Q›
        by(force intro: Trans' ScopeExt'[THEN cSym'])
      ultimately show ?thesis by(rule_tac Compose)
    qed
    ultimately show ?case by blast
  qed
qed
unbundle relcomp_syntax
end

end