Quellcode-Bibliothek Sim_Pres.thy

theory Sim_Pres
  imports Simulation
begin

text ‹This file is a (heavily modified) variant of the theory {\it Psi\_Calculi.Sim\_Pres}
 ~\cite{DBLP:journals/afp/Bengtson12}.›

context env begin

lemma inputPres:
  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 -
  {
    fix α Q'
    assume "Ψ ⊳ M(λ*xvec N).Q ⟼α ≺ Q'"
    then have "∃P'. Ψ ⊳ M(λ*xvec N).P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
      by(induct rule: inputCases) (auto intro: Input BrInput PRelQ)
  }
  then show ?thesis
    by(auto simp add: simulation_def residual.inject psi.inject)
qed

lemma outputPres:
  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 -
  {
    fix α Q'
    assume "Ψ ⊳ M⟨N⟩.Q ⟼α ≺ Q'"
    then have "∃P'. Ψ ⊳ M⟨N⟩.P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
      by(induct rule: outputCases) (auto intro: Output BrOutput PRelQ)
  }
  then show ?thesis
    by(auto simp add: simulation_def residual.inject psi.inject)
qed

lemma casePres:
  fixes Ψ    :: 'b
    and CsP  :: "('c × ('a, 'b, 'c) psi) list"
    and Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
    and CsQ  :: "('c × ('a, 'b, 'c) psi) list"
    and M    :: 'a
    and N    :: 'a

assumes PRelQ: "∧φ Q. (φ, Q) ∈ set CsQ ==> ∃P. (φ, P) ∈ set CsP ∧ guarded P ∧ (Ψ, P, Q) ∈ Rel"
  and   Sim: "∧Ψ' R S. (Ψ', R, S) ∈ Rel ==> Ψ' ⊳ R ↝[Rel] S"
  and        "Rel ⊆ Rel'"

shows "Ψ ⊳ Cases CsP ↝[Rel'] Cases CsQ"
proof -
  {
    fix α Q'
    assume "Ψ ⊳ Cases CsQ ⟼α ≺ Q'" and "bn α ♯* CsP" and "bn α ♯* Ψ"
    then have "∃P'. Ψ ⊳ Cases CsP ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel'"
    proof(induct rule: caseCases)
      case(cCase φ Q)
      from ‹(φ, Q) ∈ set CsQ› obtain P where "(φ, P) ∈ set CsP" and "guarded P" and "(Ψ, P, Q) ∈ Rel"
        by(metis PRelQ)
      from ‹(Ψ, P, Q) ∈ Rel› have "Ψ ⊳ P ↝[Rel] Q"
        by(rule Sim)
      moreover from ‹bn α ♯* CsP› ‹(φ, P) ∈ set CsP› have "bn α ♯* P"
        by(auto dest: memFreshChain)
      moreover note ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ›
      ultimately obtain P' where PTrans: "Ψ ⊳ P ⟼α ≺ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
        by(blast dest: simE)
      from PTrans ‹(φ, P) ∈ set CsP› ‹Ψ ⊨ φ› ‹guarded P› have "Ψ ⊳ Cases CsP ⟼α ≺ P'"
        by(rule Case)
      moreover from P'RelQ' ‹Rel ⊆ Rel'› have "(Ψ, P', Q') ∈ Rel'"
        by blast
      ultimately show ?case
        by blast
    qed
  }
  then show ?thesis
    by(auto simp add: simulation_def residual.inject psi.inject)
qed

lemma resPres:
  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 yvec. [(Ψ', R, S) ∈ Rel; yvec ♯* Ψ'] ==> (Ψ', (ν*yvec)R, (ν*yvec)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: simIFresh[where C="()"])
    case(cSim α 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 α ♯* Ψ› ‹bn α ♯* P› ‹x ♯ α›
    show ?case
    proof(induct rule: resCases[where C="P"])
      case(cOpen M xvec1 xvec2 y N Q')
      from ‹bn (M(ν*(xvec1@y#xvec2))⟨N⟩) ♯* Ψ› have "xvec1 ♯* Ψ" and "y ♯ Ψ" and "xvec2 ♯* Ψ" by simp+
      from ‹bn (M(ν*(xvec1@y#xvec2))⟨N⟩) ♯* P› have "xvec1 ♯* P" and "y ♯ P" and "xvec2 ♯* 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' where PTrans: "Ψ ⊳ P ⟼M(ν*(xvec1@xvec2))⟨([(x, y)] ∙ N)⟩ ≺ P'" and P'RelQ': "(Ψ, P', ([(x, y)] ∙ Q')) ∈ Rel"
        by(force dest: simE)
      from ‹y ∈ supp N› ‹x ≠ y› have "x ∈ supp([(x, y)] ∙ N)"
        apply -
        apply(drule pt_set_bij2[OF pt_name_inst, OF at_name_inst, where pi="[(x, y)]"])
        by(simp add: eqvts calc_atm)
      with PTrans ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2›
      have "Ψ ⊳ (νx)P ⟼M(ν*(xvec1@x#xvec2))⟨([(x, y)] ∙ N)⟩ ≺ P'"
        by(metis Open)
      then have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ (νx)P) ⟼([(x, y)] ∙ (M(ν*(xvec1@x#xvec2))⟨([(x, y)] ∙ N)⟩ ≺ P'))"
        by(rule eqvts)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹y ♯ P› ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec1› ‹y ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec2› ‹x ≠ y›
      have "Ψ ⊳ (νx)P ⟼M(ν*(xvec1@y#xvec2))⟨N⟩ ≺ ([(x, y)] ∙ P')" by(simp add: eqvts calc_atm alphaRes)
      moreover from P'RelQ' ‹Rel ⊆ Rel'› ‹eqvt Rel'› have "([(y, x)] ∙ Ψ, [(y, x)] ∙ P', [(y, x)] ∙ [(x, y)] ∙ Q') ∈ Rel'"
        by(force simp add: eqvt_def)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› have "(Ψ, [(x, y)] ∙ P', Q') ∈ Rel'" by(simp add: name_swap)
      ultimately show ?case by blast
    next
      case(cBrOpen M xvec1 xvec2 y N Q')
      from ‹bn (🍋M(ν*(xvec1@y#xvec2))⟨N⟩) ♯* Ψ› have "xvec1 ♯* Ψ" and "y ♯ Ψ" and "xvec2 ♯* Ψ" by simp+
      from ‹bn (🍋M(ν*(xvec1@y#xvec2))⟨N⟩) ♯* P› have "xvec1 ♯* P" and "y ♯ P" and "xvec2 ♯* 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' where PTrans: "Ψ ⊳ P ⟼🍋M(ν*(xvec1@xvec2))⟨([(x, y)] ∙ N)⟩ ≺ P'" and P'RelQ': "(Ψ, P', ([(x, y)] ∙ Q')) ∈ Rel"
        by(force dest: simE)
      from ‹y ∈ supp N› ‹x ≠ y› have "x ∈ supp([(x, y)] ∙ N)"
        apply -
        apply(drule pt_set_bij2[OF pt_name_inst, OF at_name_inst, where pi="[(x, y)]"])
        by(simp add: eqvts calc_atm)
      with PTrans ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2›
      have "Ψ ⊳ (νx)P ⟼🍋M(ν*(xvec1@x#xvec2))⟨([(x, y)] ∙ N)⟩ ≺ P'"
        by(metis BrOpen)
      then have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ (νx)P) ⟼([(x, y)] ∙ (🍋M(ν*(xvec1@x#xvec2))⟨([(x, y)] ∙ N)⟩ ≺ P'))"
        by(rule eqvts)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹y ♯ P› ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec1› ‹y ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec2› ‹x ≠ y›
      have "Ψ ⊳ (νx)P ⟼🍋M(ν*(xvec1@y#xvec2))⟨N⟩ ≺ ([(x, y)] ∙ P')" by(simp add: eqvts calc_atm alphaRes)
      moreover from P'RelQ' ‹Rel ⊆ Rel'› ‹eqvt Rel'› have "([(y, x)] ∙ Ψ, [(y, x)] ∙ P', [(y, x)] ∙ [(x, y)] ∙ Q') ∈ Rel'"
        by(force simp add: eqvt_def)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› have "(Ψ, [(x, y)] ∙ P', Q') ∈ Rel'" by(simp add: name_swap)
      ultimately show ?case by blast
    next
      case(cRes Q')
      from PSimQ ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ› ‹bn α ♯* P›
      obtain P' where PTrans: "Ψ ⊳ P ⟼α ≺ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
        by(blast dest: simE)
      from PTrans ‹x ♯ Ψ› ‹x ♯ α› have "Ψ ⊳ (νx)P ⟼α ≺ (νx)P'"
        by(rule Scope)
      moreover from P'RelQ' ‹x ♯ Ψ› have "(Ψ, (ν*[x])P', (ν*[x])Q') ∈ Rel'"
        by(intro C1[where yvec="[x]"]) simp+
      moreover then have "(Ψ, (νx)P', (νx)Q') ∈ Rel'"
        by (metis resChain.base resChain.step)
      ultimately show ?case by blast
    next
      case(cBrClose M xvec N Q')
      from PSimQ ‹Ψ ⊳ Q ⟼ 🍋M(ν*xvec)⟨N⟩ ≺ Q'› ‹xvec ♯* Ψ› ‹xvec ♯* P›
      obtain P' where PTrans: "Ψ ⊳ P ⟼🍋M(ν*xvec)⟨N⟩ ≺ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
        by(force dest: simE)
      with ‹x ♯ Ψ› ‹xvec ♯* Ψ›
      have "(x#xvec) ♯* Ψ" by simp

      from P'RelQ'
      have "(Ψ, (ν*(x#xvec))P', (ν*(x#xvec))Q') ∈ Rel'"
        using ‹(x#xvec) ♯* Ψ›
        by(rule C1)
      then have "(Ψ, (νx)((ν*xvec)P'), (νx)((ν*xvec)Q')) ∈ Rel'"
        by simp

      moreover from ‹Ψ ⊳ P ⟼ 🍋M(ν*xvec)⟨N⟩ ≺ P'› ‹x ∈ supp M› ‹x ♯ Ψ›
      have "Ψ ⊳ (νx)P ⟼ τ ≺ (νx)((ν*xvec)P')"
        by(rule BrClose)
      ultimately show ?case
        by blast
    qed
  qed
qed

lemma resChainPres:
  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 ♯* Ψ› have "Ψ ⊳ (ν*xvec)P ↝[Rel] (ν*xvec)Q" by(rule Cons)
  moreover note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover have "Rel ⊆ Rel" by simp
  ultimately have "Ψ ⊳ (νx)((ν*xvec)P) ↝[Rel] (νx)((ν*xvec)Q)" using C1
    by(rule resPres)
  then show ?case by simp
qed

lemma parPres:
  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   StatImp: "∧Ψ' S T. (Ψ', S, T) ∈ Rel ==> insertAssertion (extractFrame T) Ψ' ↪_F insertAssertion (extractFrame S) Ψ'"
and   Sim:     "∧Ψ' S T. (Ψ', S, T) ∈ Rel ==> Ψ' ⊳ S ↝[Rel] T"
and   Ext: "∧Ψ' S T Ψ''. [(Ψ', S, T) ∈ Rel] ==> (Ψ' ⊗ Ψ'', S, T) ∈ Rel"


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"
  using Eqvt'
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α 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" by simp
    have FrR: "extractFrame R = ⟨A_R, Ψ_R⟩" by fact
    from ‹A_R ♯* α› ‹bn α ♯* R› FrR have "bn α ♯* Ψ_R"
      by(auto dest: extractFrameFreshChain)
    from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q› have "Ψ ⊗ Ψ_R ⊳ P ↝[Rel] Q"
      by(blast intro: Sim PRelQ)
    moreover have QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼α ≺ Q'" by fact
    ultimately obtain P' where PTrans: "Ψ ⊗ Ψ_R ⊳ P ⟼α ≺ P'"
      and P'RelQ': "(Ψ ⊗ Ψ_R, P', Q') ∈ Rel"
      using ‹bn α ♯* Ψ› ‹bn α ♯* Ψ_R› ‹bn α ♯* P›
      by(force dest: simE)
    from PTrans QTrans ‹A_R ♯* P› ‹A_R ♯* Q› ‹A_R ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)› have "A_R ♯* P'" and "A_R ♯* Q'"
      by(blast dest: freeFreshChainDerivative)+
    from PTrans ‹bn α ♯* R› FrR  ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* α› have "Ψ ⊳ P ∥ R ⟼α ≺ (P' ∥ R)"
      by(metis Par1)
    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)
    then have "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(auto dest: extractFrameFreshChain)

    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"
      by simp+

    from ‹A_Q ♯* R›  FrR ‹A_R ♯* A_Q› have "A_Q ♯* Ψ_R"
      by(auto dest: extractFrameFreshChain)
    from ‹A_P ♯* R› ‹A_R ♯* A_P› FrR  have "A_P ♯* Ψ_R"
      by(auto dest: extractFrameFreshChain)

    have RTrans: "Ψ ⊗ Ψ_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 from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ Ψ_R)) ↪_F (insertAssertion (extractFrame P) (Ψ ⊗ Ψ_R))"
        by(blast intro: PRelQ StatImp)
      with 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 auto
      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 have "Ψ ⊗ Ψ_P ⊳ R ⟼α ≺ R'"
      using ‹A_P ♯* Ψ› ‹A_P ♯* Ψ_Q› ‹A_Q ♯* Ψ› ‹A_Q ♯* Ψ_P› ‹A_P ♯* R› ‹A_Q ♯* R› ‹A_P ♯* α› ‹A_Q ♯* α›
        ‹A_R ♯* A_P› ‹A_R ♯* A_Q› ‹A_R ♯* Ψ_P› ‹A_R ♯* Ψ_Q› ‹A_R ♯* Ψ› FrR ‹distinct A_R›
      by(force intro: transferFrame)
    with ‹bn α ♯* P› ‹A_P ♯* Ψ›  ‹A_P ♯* R›  ‹A_P ♯* α› FrP have "Ψ ⊳ P ∥ R ⟼α ≺ (P ∥ R')"
      by(force intro: Par2)
    moreover obtain A_R' Ψ_R' where "extractFrame R' = ⟨A_R', Ψ_R'⟩" and "A_R' ♯* Ψ" and "A_R' ♯* P" and "A_R' ♯* Q"
      by(rule freshFrame[where C="(Ψ, P, Q)"]) auto

    moreover from RTrans FrR ‹distinct A_R› ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q› ‹A_R ♯* 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 ∙ α) ♯* R" and "bn(p ∙ α) ♯* Ψ" and "bn(p ∙ α) ♯* P" and "bn(p ∙ α) ♯* Q" and "bn(p ∙ α) ♯* R"
      and "A_R' ♯* Ψ" and "A_R' ♯* P" and "A_R' ♯* Q"
      apply -
      apply (rule expandFrame[where C="(Ψ, P, Q, R)" and C'="(Ψ, P, Q, R)"])
                 apply simp+
      done

    from ‹A_R ♯* Ψ› have "(p ∙ A_R) ♯* (p ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹bn α ♯* Ψ› ‹bn(p ∙ α) ♯* Ψ› 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 ‹bn α ♯* P› ‹bn(p ∙ α) ♯* 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 ‹bn α ♯* Q› ‹bn(p ∙ α) ♯* Q› S have "(p ∙ A_R) ♯* Q" by simp

    from FrR have "(p ∙ extractFrame R) = p ∙ ⟨A_R, Ψ_R⟩" by simp
    with ‹bn α ♯* R› ‹bn(p ∙ α) ♯* R› S have "extractFrame R = ⟨(p ∙ A_R), (p ∙ Ψ_R)⟩"
      by(simp add: eqvts)

    with ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q› have "(Ψ ⊗ (p ∙ Ψ_R), P, Q) ∈ Rel"
      by(metis PRelQ)

    then have "((Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ', P, Q) ∈ Rel" by(rule Ext)
    with ‹(p ∙ Ψ_R) ⊗ Ψ' ≃ Ψ_R'› have "(Ψ ⊗ Ψ_R', P, Q) ∈ Rel" by(blast intro: C3 Associativity compositionSym)
    with FrR' ‹A_R' ♯* Ψ› ‹A_R' ♯* P› ‹A_R' ♯* Q› have "(Ψ, P ∥ R', Q ∥ R') ∈ Rel'"
      by(metis 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+

    obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* (Ψ, A_Q, Ψ_Q, A_R, M, N, K, R, P, xvec)" and "distinct A_P"
      by(rule freshFrame)
    then have "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"
      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 FrP FrR ‹A_Q ♯* P› ‹A_P ♯* R› ‹A_R ♯* P› ‹A_P ♯* A_Q› ‹A_P ♯* A_R› ‹A_P ♯* xvec› ‹xvec ♯* P›
    have "A_P ♯* Ψ_R" and "A_Q ♯* Ψ_P" and  "A_R ♯* Ψ_P" and "xvec ♯* Ψ_P"
      by(auto dest!: extractFrameFreshChain)+

    from RTrans FrR ‹distinct A_R› ‹A_R ♯* R› ‹A_R ♯* xvec› ‹xvec ♯* R› ‹xvec ♯* Q› ‹xvec ♯* Ψ› ‹xvec ♯* Ψ_Q› ‹A_R ♯* Q›
      ‹A_R ♯* Ψ› ‹A_R ♯* Ψ_Q› ‹xvec ♯* K› ‹A_R ♯* K› ‹A_R ♯* N› ‹A_R ♯* R› ‹xvec ♯* R› ‹A_R ♯* P› ‹xvec ♯* P› ‹A_P ♯* A_R› ‹A_P ♯* xvec›
      ‹A_Q ♯* A_R› ‹A_Q ♯* xvec› ‹A_R ♯* Ψ_P› ‹xvec ♯* Ψ_P› ‹distinct xvec› ‹xvec ♯* M›
    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_P" and "(p ∙ xvec) ♯* A_Q" and "(p ∙ xvec) ♯* Ψ_P"
      and "A_R' ♯* P" and "A_R' ♯* N"
      by (subst expandFrame[where C="(Ψ, Q, Ψ_Q, K, R, P, A_P, A_Q, Ψ_P)" and C'="(Ψ, Q, Ψ_Q, K, R, P, A_P, A_Q, Ψ_P)"]) 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_P ♯* xvec› ‹(p ∙ xvec) ♯* A_P› ‹A_P ♯* M› S have "A_P ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹A_Q ♯* xvec› ‹(p ∙ xvec) ♯* A_Q› ‹A_Q ♯* M› S have "A_Q ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹A_P ♯* xvec› ‹(p ∙ xvec) ♯* A_P› ‹A_P ♯* A_R› S have "(p ∙ A_R) ♯* A_P" by(simp add: freshChainSimps)
    from ‹A_Q ♯* xvec› ‹(p ∙ xvec) ♯* A_Q› ‹A_Q ♯* A_R› S have "(p ∙ A_R) ♯* A_Q" by(simp add: freshChainSimps)

    from QTrans S ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› have "(p ∙ (Ψ ⊗ Ψ_R)) ⊳ Q ⟼ (p ∙ M)(N) ≺ Q'"
      using inputPermFrameSubject name_list_set_fresh by blast
    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)

    note RTrans FrR
    moreover from FrR ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q› have "Ψ ⊗ (p ∙ Ψ_R) ⊳ P ↝[Rel] Q"
      by(metis Sim PRelQ)
    with QTrans obtain P' where PTrans: "Ψ ⊗ (p ∙ Ψ_R) ⊳ P ⟼(p ∙ M)(N) ≺ P'" and P'RelQ': "(Ψ ⊗ (p ∙ Ψ_R), P', Q') ∈ Rel"
      by(force dest: simE)
    from PTrans QTrans ‹A_R' ♯* P› ‹A_R' ♯* Q› ‹A_R' ♯* N› have "A_R' ♯* P'" and "A_R' ♯* Q'"
      by(blast dest: inputFreshChainDerivative)+

    note PTrans
    moreover 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)

    moreover have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ (p ∙ Ψ_R)⟩ ↪_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ (p ∙ Ψ_R)⟩"
    proof -
      have "⟨A_P, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_P⟩ ≃_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ (p ∙ Ψ_R)⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ (p ∙ Ψ_R))) ↪_F (insertAssertion (extractFrame P) (Ψ ⊗ (p ∙ Ψ_R)))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹A_P ♯* Ψ› ‹A_Q ♯* Ψ› ‹A_P ♯* Ψ_R› ‹A_Q ♯* Ψ_R› ‹A_P ♯* xvec› ‹(p ∙ xvec) ♯* A_P› ‹A_Q ♯* xvec› ‹(p ∙ xvec) ♯* A_Q› S
      have "⟨A_Q, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_Q⟩ ↪_F ⟨A_P, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_P⟩" using freshCompChain
        by(simp add: freshChainSimps)
      moreover have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ (p ∙ Ψ_R)⟩ ≃_F ⟨A_Q, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_Q⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    moreover note FrP FrQ ‹distinct A_P›
    moreover from ‹distinct A_R› have "distinct(p ∙ A_R)" by simp
    moreover note ‹(p ∙ A_R) ♯* A_P›  ‹(p ∙ A_R) ♯* A_Q› ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q› ‹(p ∙ A_R) ♯* R› ‹(p ∙ A_R) ♯* K›
      ‹A_P ♯* Ψ› ‹A_P ♯* R› ‹A_P ♯* P› ‹A_P ♯* (p ∙ M)› ‹A_Q ♯* R› ‹A_Q ♯* (p ∙ M)› ‹A_P ♯* xvec› ‹xvec ♯* P› ‹A_P ♯* R›
    ultimately obtain K' where "Ψ ⊗ Ψ_P ⊳ R ⟼K'(ν*xvec)⟨N⟩ ≺ R'" and "Ψ ⊗ Ψ_P ⊗ (p ∙ Ψ_R) ⊨ (p ∙ M) ↔ K'" and "(p ∙ A_R) ♯* K'"
      using comm1Aux by blast

    with PTrans FrP have "Ψ ⊳ P ∥ R ⟼τ ≺ (ν*xvec)(P' ∥ R')" using FrR ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* R›
        ‹xvec ♯* P› ‹A_P ♯* Ψ› ‹A_P ♯* P› ‹A_P ♯* R› ‹A_P ♯* (p ∙ M)› ‹(p ∙ A_R) ♯* K'› ‹(p ∙ A_R) ♯* A_P›
      by (intro Comm1) (assumption | simp)+

    moreover from P'RelQ' have  "((Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ', P', Q') ∈ Rel" by(rule Ext)
    with ‹(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(metis C1)
    with ‹xvec ♯* Ψ› have "(Ψ, (ν*xvec)(P' ∥ R'), (ν*xvec)(Q' ∥ R')) ∈ Rel'"
      by(metis 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+

    obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* (Ψ, A_Q, Ψ_Q, A_R, M, N, K, R, P, xvec)" and "distinct A_P"
      by(rule freshFrame)
    then have "A_P ♯* Ψ" and "A_P ♯* A_Q" and "A_P ♯* Ψ_Q" and "A_P ♯* M" and "A_P ♯* R"
      and "A_P ♯* N" "A_P ♯* K" and "A_P ♯* A_R" and "A_P ♯* P"  and "A_P ♯* xvec"
      by simp+

    from FrP FrR ‹A_Q ♯* P› ‹A_P ♯* R› ‹A_R ♯* P› ‹A_P ♯* A_Q› ‹A_P ♯* A_R› ‹A_P ♯* xvec› ‹xvec ♯* P›
    have "A_P ♯* Ψ_R" and "A_Q ♯* Ψ_P" and  "A_R ♯* Ψ_P" and "xvec ♯* Ψ_P"
      by(auto dest!: extractFrameFreshChain)+

    have QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼M(ν*xvec)⟨N⟩ ≺ Q'" by fact

    note ‹Ψ ⊗ Ψ_Q ⊳ R ⟼K(N) ≺ R'› FrR ‹Ψ ⊗ Ψ_Q ⊗ Ψ_R ⊨ M ↔ K›
    moreover from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q› have "Ψ ⊗ Ψ_R ⊳ P ↝[Rel] Q" by(metis PRelQ Sim)
    with QTrans obtain P' where PTrans: "Ψ ⊗ Ψ_R ⊳ P ⟼M(ν*xvec)⟨N⟩ ≺ P'" and P'RelQ': "(Ψ ⊗ Ψ_R, P', Q') ∈ Rel"
      using ‹xvec ♯* Ψ› ‹xvec ♯* Ψ_R› ‹xvec ♯* P›
      by(force dest: simE)
    from PTrans QTrans ‹A_R ♯* P› ‹A_R ♯* Q› ‹A_R ♯* xvec› ‹xvec ♯* M› ‹distinct xvec› have "A_R ♯* P'" and "A_R ♯* Q'"
      by(blast dest: outputFreshChainDerivative)+
    note PTrans ‹Ψ ⊗ Ψ_Q ⊗ Ψ_R ⊨ M ↔ K›
    moreover have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ↪_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
    proof -
      have "⟨A_P, (Ψ ⊗ Ψ_R) ⊗ Ψ_P⟩ ≃_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ Ψ_R)) ↪_F (insertAssertion (extractFrame P) (Ψ ⊗ Ψ_R))"
        by(metis PRelQ StatImp)
      with 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_Q, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ≃_F ⟨A_Q, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    moreover note FrP FrQ ‹distinct A_P› ‹distinct A_R›
    moreover from ‹A_P ♯* A_R› ‹A_Q ♯* A_R› have "A_R ♯* A_P" and "A_R ♯* A_Q" by simp+
    moreover note ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q› ‹A_R ♯* R› ‹A_R ♯* K›  ‹A_P ♯* Ψ› ‹A_P ♯* P›
      ‹A_P ♯* R› ‹A_P ♯* M› ‹A_Q ♯* R› ‹A_Q ♯* M› ‹A_R ♯* xvec› ‹xvec ♯* M›
    ultimately obtain K' where "Ψ ⊗ Ψ_P ⊳ R ⟼K'(N) ≺ R'" and "Ψ ⊗ Ψ_P ⊗ Ψ_R ⊨ M ↔ K'" and "A_R ♯* K'"
      using comm2Aux by blast

    with PTrans FrP have "Ψ ⊳ P ∥ R ⟼τ ≺ (ν*xvec)(P' ∥ R')" using FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* R›
        ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* R› and ‹xvec ♯* R› ‹A_P ♯* Ψ› ‹A_P ♯* P› ‹A_P ♯* R› ‹A_P ♯* A_R› ‹A_P ♯* M› ‹A_R ♯* K'›
      by(force intro: Comm2)

    moreover from ‹Ψ ⊗ Ψ_P ⊳ R ⟼K'(N) ≺ R'› FrR ‹distinct A_R› ‹A_R ♯* Ψ› ‹A_R ♯* R› ‹A_R ♯* P'› ‹A_R ♯* Q'› ‹A_R ♯* N› ‹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'"
      by(auto intro: expandFrame[where C="(Ψ, P', Q')" and C'="Ψ"])

    from P'RelQ' have "((Ψ ⊗ Ψ_R) ⊗ Ψ', P', Q') ∈ Rel" by(rule Ext)
    with ReqR' 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(metis C1)
    with ‹xvec ♯* Ψ› have "(Ψ, (ν*xvec)(P' ∥ R'), (ν*xvec)(Q' ∥ R')) ∈ Rel'"
      by(metis C2)
    ultimately show ?case by blast
  next
    case(cBrMerge Ψ_R M N Q' A_Q Ψ_Q 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+

    obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* (Ψ, A_Q, Ψ_Q, A_R, M, N, R, P)" and "distinct A_P"
      by(rule freshFrame)
    then have "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 ♯* A_R" and "A_P ♯* P"
      by simp+

    from FrP FrR ‹A_Q ♯* P› ‹A_P ♯* R› ‹A_R ♯* P› ‹A_P ♯* A_Q› ‹A_P ♯* A_R›
    have "A_P ♯* Ψ_R" and "A_Q ♯* Ψ_P" and  "A_R ♯* Ψ_P"
      by(auto dest: extractFrameFreshChain)+

    have QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼🍋M(N) ≺ Q'" by fact

    have RTrans: "Ψ ⊗ Ψ_Q ⊳ R ⟼🍋M(N) ≺ R'" by fact

    from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q› have "Ψ ⊗ Ψ_R ⊳ P ↝[Rel] Q" by(metis PRelQ Sim)
    with QTrans obtain P' where PTrans: "Ψ ⊗ Ψ_R ⊳ P ⟼🍋M(N) ≺ P'" and P'RelQ': "(Ψ ⊗ Ψ_R, P', Q') ∈ Rel"
      by(force dest: simE)
    from PTrans QTrans ‹A_R ♯* P› ‹A_R ♯* Q› ‹A_R ♯* N› have "A_R ♯* P'" and "A_R ♯* Q'"
      by(blast dest: brinputFreshChainDerivative)+

    have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ↪_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
    proof -
      have "⟨A_P, (Ψ ⊗ Ψ_R) ⊗ Ψ_P⟩ ≃_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ Ψ_R)) ↪_F (insertAssertion (extractFrame P) (Ψ ⊗ Ψ_R))"
        by(metis PRelQ StatImp)
      with 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_Q, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ≃_F ⟨A_Q, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    with RTrans ‹extractFrame R = ⟨A_R, Ψ_R⟩› ‹distinct A_R› ‹A_P ♯* A_R› ‹A_Q ♯* A_R›
      ‹A_R ♯* Ψ› ‹A_R ♯* Ψ_P› ‹A_R ♯* Ψ_Q› ‹A_R ♯* R› ‹A_R ♯* M› ‹A_P ♯* R› ‹A_P ♯* M› ‹A_Q ♯* R› ‹A_Q ♯* M›
    have "Ψ ⊗ Ψ_P ⊳ R ⟼🍋M(N) ≺ R'"
      using brCommInAux freshChainSym by blast

    with PTrans FrP have Transition: "Ψ ⊳ P ∥ R ⟼🍋M(N) ≺ (P' ∥ R')" using FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* R›
        ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* R› ‹A_P ♯* Ψ› ‹A_P ♯* P› ‹A_P ♯* R› ‹A_P ♯* A_R› ‹A_P ♯* M› ‹A_R ♯* M›
      by(force intro: BrMerge)

    from ‹Ψ ⊗ Ψ_P ⊳ R ⟼🍋M(N) ≺ R'› FrR ‹distinct A_R› ‹A_R ♯* Ψ› ‹A_R ♯* R› ‹A_R ♯* P'› ‹A_R ♯* Q'› ‹A_R ♯* N› ‹A_R ♯* M›
    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'"
      by(auto intro: expandFrame[where C="(Ψ, P', Q')" and C'="Ψ"])

    from P'RelQ' have "((Ψ ⊗ Ψ_R) ⊗ Ψ', P', Q') ∈ Rel" by(rule Ext)
    with ReqR' have "(Ψ ⊗ Ψ_R', P', Q') ∈ Rel" by(metis C3 Associativity compositionSym)
    with FrR' ‹A_R' ♯* P'› ‹A_R' ♯* Q'› ‹A_R' ♯* Ψ› have Relation: "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'"
      by(metis C1)
    show ?case using Transition Relation
      by blast
  next
    case(cBrComm1 Ψ_R M N Q' A_Q Ψ_Q 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 ‹🍋M(ν*xvec)⟨N⟩ = α› have "xvec = bn α"
      by(auto simp add: action.inject)
    from ‹xvec = bn α› ‹bn α ♯* P› ‹bn α ♯* R›
    have "xvec ♯* P" and "xvec ♯* R" by simp+

    obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* (Ψ, A_Q, Ψ_Q, A_R, M, N, R, P, xvec)" and "distinct A_P"
      by(rule freshFrame)
    then have "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 ♯* A_R" and "A_P ♯* P" and "A_P ♯* xvec"
      by simp+

    from FrP FrR ‹A_Q ♯* P› ‹A_P ♯* R› ‹A_R ♯* P› ‹A_P ♯* A_Q› ‹A_P ♯* A_R›
    have "A_P ♯* Ψ_R" and "A_Q ♯* Ψ_P" and  "A_R ♯* Ψ_P"
      by(auto dest: extractFrameFreshChain)+

    from ‹A_P ♯* xvec› ‹xvec ♯* P› FrP have "xvec ♯* Ψ_P"
      by(auto dest: extractFrameFreshChain)

    have QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼🍋M(N) ≺ Q'" by fact

    have RTrans: "Ψ ⊗ Ψ_Q ⊳ R ⟼ 🍋M(ν*xvec)⟨N⟩ ≺ R'" by fact

    from RTrans FrR ‹distinct A_R› ‹A_R ♯* R› ‹A_R ♯* xvec› ‹xvec ♯* R› ‹xvec ♯* Q› ‹xvec ♯* Ψ› ‹xvec ♯* Ψ_Q› ‹A_R ♯* Q›
      ‹A_R ♯* Ψ› ‹A_R ♯* Ψ_Q› ‹A_R ♯* M› ‹A_R ♯* N› ‹A_R ♯* R› ‹xvec ♯* R› ‹A_R ♯* P› ‹xvec ♯* P› ‹A_P ♯* A_R› ‹A_P ♯* xvec›
      ‹A_Q ♯* A_R› ‹A_Q ♯* xvec› ‹A_R ♯* Ψ_P› ‹xvec ♯* Ψ_P› ‹distinct xvec› ‹xvec ♯* M›
    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) ♯* R" and "(p ∙ xvec) ♯* M"
      and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* A_P" and "(p ∙ xvec) ♯* A_Q" and "(p ∙ xvec) ♯* Ψ_P"
      and "A_R' ♯* P" and "A_R' ♯* N"
      by(auto intro: expandFrame[where C="(Ψ, Q, Ψ_Q, R, P, M, A_P, A_Q, Ψ_P)" and C'="(Ψ, Q, Ψ_Q, R, P, M, A_P, A_Q, Ψ_P)"])

    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 ♯* M› have "(p ∙ A_R) ♯* (p ∙ M)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹xvec ♯* M› ‹(p ∙ xvec) ♯* M› S have "(p ∙ A_R) ♯* M" 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_P ♯* xvec› ‹(p ∙ xvec) ♯* A_P› ‹A_P ♯* M› S have "A_P ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹A_Q ♯* xvec› ‹(p ∙ xvec) ♯* A_Q› ‹A_Q ♯* M› S have "A_Q ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹A_P ♯* xvec› ‹(p ∙ xvec) ♯* A_P› ‹A_P ♯* A_R› S have "(p ∙ A_R) ♯* A_P" by(simp add: freshChainSimps)
    from ‹A_Q ♯* xvec› ‹(p ∙ xvec) ♯* A_Q› ‹A_Q ♯* A_R› S have "(p ∙ A_R) ♯* A_Q" by(simp add: freshChainSimps)

    from QTrans S ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› have "(p ∙ (Ψ ⊗ Ψ_R)) ⊳ Q ⟼ 🍋(p ∙ M)(N) ≺ Q'"
      using brinputPermFrameSubject name_list_set_fresh by blast
    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 FrR ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q› have "Ψ ⊗ (p ∙ Ψ_R) ⊳ P ↝[Rel] Q"
      by(metis Sim PRelQ)
    with QTrans obtain P' where PTrans: "Ψ ⊗ (p ∙ Ψ_R) ⊳ P ⟼🍋(p ∙ M)(N) ≺ P'" and P'RelQ': "(Ψ ⊗ (p ∙ Ψ_R), P', Q') ∈ Rel"
      by(force dest: simE)
    with QTrans ‹A_R' ♯* P› ‹A_R' ♯* Q› ‹A_R' ♯* N› have "A_R' ♯* P'" and "A_R' ♯* Q'"
      by(blast dest: brinputFreshChainDerivative)+

    have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ (p ∙ Ψ_R)⟩ ↪_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ (p ∙ Ψ_R)⟩"
    proof -
      have "⟨A_P, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_P⟩ ≃_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ (p ∙ Ψ_R)⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ (p ∙ Ψ_R))) ↪_F (insertAssertion (extractFrame P) (Ψ ⊗ (p ∙ Ψ_R)))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹A_P ♯* Ψ› ‹A_Q ♯* Ψ› ‹A_P ♯* Ψ_R› ‹A_Q ♯* Ψ_R› ‹A_P ♯* xvec› ‹(p ∙ xvec) ♯* A_P› ‹A_Q ♯* xvec› ‹(p ∙ xvec) ♯* A_Q› S
      have "⟨A_Q, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_Q⟩ ↪_F ⟨A_P, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_P⟩" using freshCompChain
        by(simp add: freshChainSimps)
      moreover have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ (p ∙ Ψ_R)⟩ ≃_F ⟨A_Q, (Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ_Q⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    moreover note RTrans FrR FrP FrQ ‹distinct A_P›
    moreover from ‹distinct A_R› have "distinct(p ∙ A_R)" by simp
    moreover note ‹(p ∙ A_R) ♯* A_P›  ‹(p ∙ A_R) ♯* A_Q› ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* Ψ_P› ‹(p ∙ A_R) ♯* Ψ_Q› ‹(p ∙ A_R) ♯* M› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* Q› ‹(p ∙ A_R) ♯* R›
      ‹A_P ♯* Ψ› ‹A_P ♯* R› ‹A_P ♯* P› ‹A_P ♯* M› ‹A_Q ♯* M› ‹A_P ♯* (p ∙ M)› ‹A_Q ♯* R› ‹A_P ♯* xvec› ‹xvec ♯* P› ‹A_P ♯* R›
    ultimately have "Ψ ⊗ Ψ_P ⊳ R ⟼🍋M(ν*xvec)⟨N⟩ ≺ R'"
      using brCommOutAux by blast
    with S ‹xvec ♯* M› ‹(p ∙ xvec) ♯* M› have "Ψ ⊗ Ψ_P ⊳ R ⟼🍋(p ∙ M)(ν*xvec)⟨N⟩ ≺ R'" by simp

    with PTrans FrP S ‹xvec ♯* M› ‹(p ∙ xvec) ♯* M› ‹(p ∙ A_R) ♯* M› have "Ψ ⊳ P ∥ R ⟼🍋(p ∙ M)(ν*xvec)⟨N⟩ ≺ (P' ∥ R')" using FrR ‹(p ∙ A_R) ♯* Ψ› ‹(p ∙ A_R) ♯* P› ‹(p ∙ A_R) ♯* R›
        ‹xvec ♯* P› ‹A_P ♯* Ψ› ‹A_P ♯* P› ‹A_P ♯* R› ‹A_P ♯* (p ∙ M)› ‹(p ∙ A_R) ♯* A_P›
      by(intro BrComm1) (assumption | simp)+

    with S ‹xvec ♯* M› ‹(p ∙ xvec) ♯* M›
    have Transition: "Ψ ⊳ P ∥ R ⟼🍋M(ν*xvec)⟨N⟩ ≺ (P' ∥ R')" by simp

    from P'RelQ' have  "((Ψ ⊗ (p ∙ Ψ_R)) ⊗ Ψ', P', Q') ∈ Rel" by(rule Ext)
    with ‹(p ∙ Ψ_R) ⊗ Ψ' ≃ Ψ_R'› have "(Ψ ⊗ Ψ_R', P', Q') ∈ Rel" by(metis C3 Associativity compositionSym)
    with FrR' ‹A_R' ♯* P'› ‹A_R' ♯* Q'› ‹A_R' ♯* Ψ› have Relation: "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'"
      by(metis C1)

    show ?case using Transition Relation
      by blast
  next
    case(cBrComm2 Ψ_R M xvec N Q' A_Q Ψ_Q 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 ‹🍋M(ν*xvec)⟨N⟩ = α› have "xvec = bn α"
      by(auto simp add: action.inject)
    from ‹xvec = bn α› ‹bn α ♯* P› ‹bn α ♯* R›
    have "xvec ♯* P" and "xvec ♯* R" by simp+

    obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* (Ψ, A_Q, Ψ_Q, A_R, M, N, R, P)" and "distinct A_P"
      by(rule freshFrame)
    then have "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 ♯* A_R" and "A_P ♯* P"
      by simp+

    from FrP FrR ‹A_Q ♯* P› ‹A_P ♯* R› ‹A_R ♯* P› ‹A_P ♯* A_Q› ‹A_P ♯* A_R›
    have "A_P ♯* Ψ_R" and "A_Q ♯* Ψ_P" and  "A_R ♯* Ψ_P"
      by(auto dest: extractFrameFreshChain)+

    have QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼🍋M(ν*xvec)⟨N⟩ ≺ Q'" by fact

    have RTrans: "Ψ ⊗ Ψ_Q ⊳ R ⟼🍋M(N) ≺ R'" by fact

    from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q› have "Ψ ⊗ Ψ_R ⊳ P ↝[Rel] Q" by(metis PRelQ Sim)
    from ‹Ψ ⊗ Ψ_R ⊳ P ↝[Rel] Q› QTrans ‹xvec ♯* Ψ› ‹xvec ♯* Ψ_R› ‹xvec ♯* P›
    obtain P' where PTrans: "Ψ ⊗ Ψ_R ⊳ P ⟼🍋M(ν*xvec)⟨N⟩ ≺ P'" and P'RelQ': "(Ψ ⊗ Ψ_R, P', Q') ∈ Rel"
      by(force dest: simE)
    from PTrans QTrans ‹A_R ♯* P› ‹A_R ♯* Q› ‹A_R ♯* N› ‹A_R ♯* xvec› ‹xvec ♯* M› ‹distinct xvec› have "A_R ♯* P'" and "A_R ♯* Q'"
      by(blast dest: broutputFreshChainDerivative)+

    have "⟨A_Q, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ↪_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
    proof -
      have "⟨A_P, (Ψ ⊗ Ψ_R) ⊗ Ψ_P⟩ ≃_F ⟨A_P, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ Ψ_R)) ↪_F (insertAssertion (extractFrame P) (Ψ ⊗ Ψ_R))"
        by(metis PRelQ StatImp)
      with 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_Q, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ≃_F ⟨A_Q, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    with RTrans ‹extractFrame R = ⟨A_R, Ψ_R⟩› ‹distinct A_R› ‹A_P ♯* A_R› ‹A_Q ♯* A_R›
      ‹A_R ♯* Ψ› ‹A_R ♯* Ψ_P› ‹A_R ♯* Ψ_Q› ‹A_R ♯* R› ‹A_R ♯* M› ‹A_P ♯* R› ‹A_P ♯* M› ‹A_Q ♯* R› ‹A_Q ♯* M›
    have "Ψ ⊗ Ψ_P ⊳ R ⟼🍋M(N) ≺ R'"
      using brCommInAux freshChainSym by blast

    with PTrans FrP have Transition: "Ψ ⊳ P ∥ R ⟼🍋M(ν*xvec)⟨N⟩ ≺ (P' ∥ R')" using FrR ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* R›
        ‹A_R ♯* Ψ› ‹A_R ♯* P› ‹A_R ♯* R› ‹A_P ♯* Ψ› ‹A_P ♯* P› ‹A_P ♯* R› ‹A_P ♯* A_R› ‹A_P ♯* M› ‹A_R ♯* M› ‹xvec ♯* R›
      by(force intro: BrComm2)

    from ‹Ψ ⊗ Ψ_P ⊳ R ⟼🍋M(N) ≺ R'› FrR ‹distinct A_R› ‹A_R ♯* Ψ› ‹A_R ♯* R› ‹A_R ♯* P'› ‹A_R ♯* Q'› ‹A_R ♯* N› ‹A_R ♯* M›
    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'"
      by(auto intro: expandFrame[where C="(Ψ, P', Q')" and C'="Ψ"])

    from P'RelQ' have "((Ψ ⊗ Ψ_R) ⊗ Ψ', P', Q') ∈ Rel" by(rule Ext)
    with ReqR' have "(Ψ ⊗ Ψ_R', P', Q') ∈ Rel" by(metis C3 Associativity compositionSym)
    with FrR' ‹A_R' ♯* P'› ‹A_R' ♯* Q'› ‹A_R' ♯* Ψ› have Relation: "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'"
      by(metis C1)
    show ?case using Transition Relation
      by blast
  qed
qed

unbundle no relcomp_syntax

lemma bangPres:
  fixes Ψ   :: 'b
    and P    :: "('a, 'b, 'c) psi"
    and Q    :: "('a, 'b, 'c) psi"
    and R    :: "('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"

assumes "(Ψ, P, Q) ∈ Rel"
  and   "eqvt Rel'"
  and   "guarded P"
  and   "guarded Q"
  and   cSim: "∧Ψ' S T. (Ψ', S, T) ∈ Rel ==> Ψ' ⊳ S ↝[Rel] T"
  and   cExt: "∧Ψ' S T Ψ''. (Ψ', S, T) ∈ Rel ==> (Ψ' ⊗ Ψ'', S, T) ∈ Rel"
  and   cSym: "∧Ψ' S T. (Ψ', S, T) ∈ Rel ==> (Ψ', T, S) ∈ Rel"
  and   StatEq: "∧Ψ' S T Ψ''. [(Ψ', S, T) ∈ Rel; Ψ' ≃ Ψ''] ==> (Ψ'', S, T) ∈ Rel"
  and   Closed: "∧Ψ' S T p. (Ψ', S, T) ∈ Rel ==> ((p::name prm) ∙ Ψ', p ∙ S, p ∙ T) ∈ Rel"
  and   Assoc: "∧Ψ' S T U. (Ψ', S ∥ (T ∥ U), (S ∥ T) ∥ U) ∈ Rel"
  and   ParPres: "∧Ψ' S T U. (Ψ', S, T) ∈ Rel ==> (Ψ', S ∥ U, T ∥ U) ∈ 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   ResPres: "∧Ψ' S T xvec. [(Ψ', S, T) ∈ Rel; xvec ♯* Ψ'] ==> (Ψ', (ν*xvec)S, (ν*xvec)T) ∈ Rel"
  and   ScopeExt: "∧xvec Ψ' S T. [xvec ♯* Ψ'; xvec ♯* T] ==> (Ψ', (ν*xvec)(S ∥ T), ((ν*xvec)S) ∥ T) ∈ Rel"
  and   Trans: "∧Ψ' S T U. [(Ψ', S, T) ∈ Rel; (Ψ', T, U) ∈ Rel] ==> (Ψ', S, U) ∈ Rel"
  and   Compose: "∧Ψ' S T U O. [(Ψ', S, T) ∈ Rel; (Ψ', T, U) ∈ Rel'; (Ψ', U, O) ∈ Rel] ==> (Ψ', S, O) ∈ Rel'"
  and   C1: "∧Ψ S T U. [(Ψ, S, T) ∈ Rel; guarded S; guarded T] ==> (Ψ, U ∥ !S, U ∥ !T) ∈ Rel'"
  and   Der: "∧Ψ' S α S' T. [Ψ' ⊳ !S ⟼α ≺ S'; (Ψ', S, T) ∈ Rel; bn α ♯* Ψ'; bn α ♯* S; bn α ♯* T; guarded T; bn α ♯* subject α] ==>
                                      ∃T' U O. Ψ' ⊳ !T ⟼α ≺ T' ∧ (Ψ', S', U ∥ !S) ∈ Rel ∧ (Ψ', T', O ∥ !T) ∈ Rel ∧
                                                (Ψ', U, O) ∈ Rel ∧ ((supp U)::name set) ⊆ supp S' ∧
                                                 ((supp O)::name set) ⊆ supp T'"

shows "Ψ ⊳ R ∥ !P ↝[Rel'] R ∥ !Q"
  using ‹eqvt Rel'›
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α 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])
    case(cPar1 R' A_Q Ψ_Q)
    from ‹extractFrame (!Q) = ⟨A_Q, Ψ_Q⟩› have "A_Q = []" and "Ψ_Q = SBottom'" by simp+
    with ‹Ψ ⊗ Ψ_Q ⊳ R ⟼α ≺ R'› ‹bn α ♯* P› have "Ψ ⊳ R ∥ !P ⟼α ≺ (R' ∥ !P)"
      by(intro Par1) (assumption | simp)+
    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)
    have QTrans: "Ψ ⊗ Ψ_R ⊳ !Q ⟼α ≺ Q'" and FrR: "extractFrame R = ⟨A_R, Ψ_R⟩" by fact+
    with ‹bn α ♯* R› ‹A_R ♯* α› have "bn α ♯* Ψ_R" by(force dest: extractFrameFreshChain)
    with QTrans ‹(Ψ, P, Q) ∈ Rel› ‹bn α ♯* Ψ›\<open>bn α ♯* P› ‹bn α ♯* Q› ‹guarded P› ‹bn α ♯* subject α›
    obtain P' S T where PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !P \<longmapsto>\<alpha> \<prec> P'" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel"
      and "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel"
      and suppT: "((supp T)::name set) \<subseteq> supp P'" and suppS: "((supp S)::name set) \<subseteq> supp Q'"
      by(drule_tac cSym) (auto dest: Der cExt)
    from PTrans FrR \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* \<alpha>\<close> \<open>bn \<alpha> \<sharp>* R\<close> have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<alpha> \<prec> (R \<parallel> P')"
      by(intro Par2) auto
    moreover
    {
      from \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* \<alpha>\<close> PTrans QTrans \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>distinct(bn \<alpha>)\<close> have "A\<^sub>R \<sharp>* P'" and "A\<^sub>R \<sharp>* Q'"
        by(force dest: freeFreshChainDerivative)+
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel\<close> FrR \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P'\<close> \<open>A\<^sub>R \<sharp>* P\<close> suppT have "(\<Psi>, R \<parallel> P', R \<parallel> (T \<parallel> !P)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(\<Psi>, R \<parallel> P', (R \<parallel> T) \<parallel> !P) \<in> Rel" by(blast intro: Assoc Trans)
      moreover from \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close> \<open>guarded Q\<close> have "(\<Psi>, (R \<parallel> T) \<parallel> !P, (R \<parallel> T) \<parallel> !Q) \<in> Rel'"
        by(rule C1)
      moreover from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel\<close> \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', T \<parallel> !Q) \<in> Rel"
        by(blast intro: ParPres Trans)
      with FrR \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P'\<close> \<open>A\<^sub>R \<sharp>* Q'\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> suppT suppS have "(\<Psi>, R \<parallel> Q', R \<parallel> (T \<parallel> !Q)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(\<Psi>, R \<parallel> Q', (R \<parallel> T) \<parallel> !Q) \<in> Rel" by(blast intro: Assoc Trans)
      ultimately have "(\<Psi>, R \<parallel> P', R \<parallel> Q') \<in> Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cComm1 \<Psi>\<^sub>Q M N R' A\<^sub>R \<Psi>\<^sub>R K xvec Q' A\<^sub>Q)
    from \<open>extractFrame (!Q) = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> have "A\<^sub>Q = []" and "\<Psi>\<^sub>Q = SBottom'" by simp+
    have RTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>M\<lparr>N\<rparr> \<prec> R'" and FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>" by fact+
    moreover have QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'" by fact
    from FrR \<open>xvec \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* xvec\<close> have "xvec \<sharp>* \<Psi>\<^sub>R" by(force dest: extractFrameFreshChain)
    with QTrans \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>xvec \<sharp>* \<Psi>\<close>\<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>guarded P\<close> \<open>xvec \<sharp>* K\<close>
    obtain P' S T where PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !P \<longmapsto>K\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel"
      and "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel"
      and suppT: "((supp T)::name set) \<subseteq> supp P'" and suppS: "((supp S)::name set) \<subseteq> supp Q'"
      apply(drule_tac cSym)
      by (metis Der bn.simps(3) cExt freshCompChain(1) optionFreshChain(1) psiFreshVec(7) subject.simps(3))
    note \<open>\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K\<close>
    ultimately have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<tau> \<prec> \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> P')"
      using PTrans \<open>\<Psi>\<^sub>Q = SBottom'\<close> \<open>xvec \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* P\<close>
      by(intro Comm1) (assumption | simp)+

    moreover from \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* xvec\<close> PTrans QTrans \<open>xvec \<sharp>* K\<close> \<open>distinct xvec\<close>
    have "A\<^sub>R \<sharp>* P'" and "A\<^sub>R \<sharp>* Q'" by(force dest: outputFreshChainDerivative)+
    moreover with RTrans FrR \<open>distinct A\<^sub>R\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* N\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* M\<close>
    obtain \<Psi>' A\<^sub>R' \<Psi>\<^sub>R' where FrR': "extractFrame R' = \<langle>A\<^sub>R', \<Psi>\<^sub>R'\<rangle>" and "\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'" and "A\<^sub>R' \<sharp>* \<Psi>"
      and "A\<^sub>R' \<sharp>* P'" and "A\<^sub>R' \<sharp>* Q'" and "A\<^sub>R' \<sharp>* P" and "A\<^sub>R' \<sharp>* Q"
      by(auto intro: expandFrame[where C="(\<Psi>, P, P', Q, Q')" and C'=\<Psi>])

    moreover
    {
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel\<close> have "((\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>', P', T \<parallel> !P) \<in> Rel" by(rule cExt)
      with \<open>\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', P', T \<parallel> !P) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* P\<close> suppT have "(\<Psi>, R' \<parallel> P', R' \<parallel> (T \<parallel> !P)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(\<Psi>, R' \<parallel> P', (R' \<parallel> T) \<parallel> !P) \<in> Rel" by(blast intro: Assoc Trans)
      with \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> have "(\<Psi>, \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> P'), (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> T)) \<parallel> !P) \<in> Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      moreover from \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close> \<open>guarded Q\<close> have "(\<Psi>, (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> T)) \<parallel> !P, (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> T)) \<parallel> !Q) \<in> Rel'"
        by(rule C1)
      moreover from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel\<close> \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', T \<parallel> !Q) \<in> Rel"
        by(blast intro: ParPres Trans)
      then have "((\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>', Q', T \<parallel> !Q) \<in> Rel" by(rule cExt)
      with \<open>\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', Q', T \<parallel> !Q) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* Q'\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> suppT suppS have "(\<Psi>, R' \<parallel> Q', R' \<parallel> (T \<parallel> !Q)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(\<Psi>, R' \<parallel> Q', (R' \<parallel> T) \<parallel> !Q) \<in> Rel" by(blast intro: Assoc Trans)
      with \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* (!Q)\<close> have "(\<Psi>, \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> Q'), (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> T)) \<parallel> !Q) \<in> Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      ultimately have "(\<Psi>, \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> P'), \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> Q')) \<in> Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cComm2 \<Psi>\<^sub>Q M xvec N R' A\<^sub>R \<Psi>\<^sub>R K Q' A\<^sub>Q)
    from \<open>extractFrame (!Q) = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> have "A\<^sub>Q = []" and "\<Psi>\<^sub>Q = SBottom'" by simp+
    have RTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> R'" and FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>" by fact+
    then obtain p \<Psi>' A\<^sub>R' \<Psi>\<^sub>R' where S: "set p \<subseteq> set xvec \<times> set(p \<bullet> xvec)"
      and FrR': "extractFrame R' = \<langle>A\<^sub>R', \<Psi>\<^sub>R'\<rangle>" and "(p \<bullet> \<Psi>\<^sub>R) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'" and "A\<^sub>R' \<sharp>* \<Psi>"
      and "A\<^sub>R' \<sharp>* N" and "A\<^sub>R' \<sharp>* R'" and "A\<^sub>R' \<sharp>* P" and "A\<^sub>R' \<sharp>* Q" and "(p \<bullet> xvec) \<sharp>* \<Psi>"
      and "(p \<bullet> xvec) \<sharp>* P" and "(p \<bullet> xvec) \<sharp>* Q" and "xvec \<sharp>* A\<^sub>R'" and "(p \<bullet> xvec) \<sharp>* A\<^sub>R'"
      and "distinctPerm p" and "(p \<bullet> xvec) \<sharp>* R'" and "(p \<bullet> xvec) \<sharp>* N"
      using \<open>distinct A\<^sub>R\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* xvec\<close> \<open>A\<^sub>R \<sharp>* N\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close>
        \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>xvec \<sharp>* R\<close> \<open>xvec \<sharp>* M\<close> \<open>distinct xvec\<close>
      by(auto intro: expandFrame[where C="(\<Psi>, P, Q)" and C'="(\<Psi>, P, Q)"])

    from RTrans S \<open>(p \<bullet> xvec) \<sharp>* N\<close> \<open>(p \<bullet> xvec) \<sharp>* R'\<close> have "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> R')"
      apply(simp add: residualInject)
      by(subst boundOutputChainAlpha''[symmetric]) auto

    moreover have QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>K\<lparr>N\<rparr> \<prec> Q'" by fact
    with QTrans S \<open>(p \<bullet> xvec) \<sharp>* N\<close> have "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>K\<lparr>(p \<bullet> N)\<rparr> \<prec> (p \<bullet> Q')" using \<open>distinctPerm p\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close>
      by(intro inputAlpha) auto
    with \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close>
    obtain P' S T where PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !P \<longmapsto>K\<lparr>(p \<bullet> N)\<rparr> \<prec> P'" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel"
      and "(\<Psi> \<otimes> \<Psi>\<^sub>R, (p \<bullet> Q'), S \<parallel> !Q) \<in> Rel" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel"
      and suppT: "((supp T)::name set) \<subseteq> supp P'" and suppS: "((supp S)::name set) \<subseteq> supp(p \<bullet> Q')"
      by(drule_tac cSym) (auto dest: Der cExt)
    note \<open>\<Psi> \<otimes> \<Psi>\<^sub>R \<otimes> \<Psi>\<^sub>Q \<turnstile> M \<leftrightarrow> K\<close>
    ultimately have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<tau> \<prec> \<lparr>\<nu>*(p \<bullet> xvec)\<rparr>((p \<bullet> R') \<parallel> P')"
      using PTrans FrR \<open>\<Psi>\<^sub>Q = SBottom'\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* P\<close>
      by(intro Comm2) (assumption | simp)+

    moreover from \<open>A\<^sub>R' \<sharp>* P\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> \<open>A\<^sub>R' \<sharp>* N\<close> S \<open>xvec \<sharp>* A\<^sub>R'\<close> \<open>(p \<bullet> xvec) \<sharp>* A\<^sub>R'\<close> PTrans QTrans \<open>distinctPerm p\<close> have "A\<^sub>R' \<sharp>* P'" and "A\<^sub>R' \<sharp>* Q'"
       apply(drule_tac inputFreshChainDerivative)
         apply simp
        apply(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ _ p], simp)
       apply fastforce
      using QTrans \<open>A\<^sub>R' \<sharp>* N\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> inputFreshChainDerivative by force
    from \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* N\<close> PTrans \<open>distinctPerm p\<close> have "(p \<bullet> xvec) \<sharp>* (p \<bullet> P')"
      apply(drule_tac inputFreshChainDerivative)
        apply simp
      by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ _ p], simp)+

    {
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel\<close> have "(p \<bullet> (\<Psi> \<otimes> \<Psi>\<^sub>R), (p \<bullet> P'), p \<bullet> (T \<parallel> !P)) \<in> Rel"
        by(rule Closed)
      with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> S have "(\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R), p \<bullet> P', (p \<bullet> T) \<parallel> !P) \<in> Rel"
        by(simp add: eqvts)
      then have "((\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R)) \<otimes> \<Psi>', p \<bullet> P', (p \<bullet> T) \<parallel> !P) \<in> Rel" by(rule cExt)
      with \<open>(p \<bullet> \<Psi>\<^sub>R) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', (p \<bullet> P'), (p \<bullet> T) \<parallel> !P) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* P\<close> \<open>xvec \<sharp>* A\<^sub>R'\<close> \<open>(p \<bullet> xvec) \<sharp>* A\<^sub>R'\<close> S \<open>distinctPerm p\<close> suppT
      have "(\<Psi>, R' \<parallel> (p \<bullet> P'), R' \<parallel> ((p \<bullet> T) \<parallel> !P)) \<in> Rel"
        apply(intro FrameParPres)
            apply(assumption | simp add: freshChainSimps)+
        by(auto simp add: fresh_star_def fresh_def)
      then have "(\<Psi>, R' \<parallel> (p \<bullet> P'), (R' \<parallel> (p \<bullet> T)) \<parallel> !P) \<in> Rel" by(blast intro: Assoc Trans)
      with \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> have "(\<Psi>, \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> (p \<bullet> P')), (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> (p \<bullet> T))) \<parallel> !P) \<in> Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      then have "(\<Psi>, \<lparr>\<nu>*(p \<bullet> xvec)\<rparr>((p \<bullet> R') \<parallel> P'), (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> (p \<bullet> T))) \<parallel> !P) \<in> Rel"
        using \<open>(p \<bullet> xvec) \<sharp>* R'\<close> \<open>(p \<bullet> xvec) \<sharp>* (p \<bullet> P')\<close> S \<open>distinctPerm p\<close>
        apply(erule_tac rev_mp)
        by(subst resChainAlpha[of p]) auto
      moreover from \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close> \<open>guarded Q\<close> have "(\<Psi>, (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> (p \<bullet> T))) \<parallel> !P, (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> (p \<bullet> T))) \<parallel> !Q) \<in> Rel'"
        by(rule C1)
      moreover from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, (p \<bullet> Q'), S \<parallel> !Q) \<in> Rel\<close> \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R, (p \<bullet> Q'), T \<parallel> !Q) \<in> Rel"
        by(blast intro: ParPres Trans)
      then have "(p \<bullet> (\<Psi> \<otimes> \<Psi>\<^sub>R), p \<bullet> p \<bullet> Q', p \<bullet> (T \<parallel> !Q)) \<in> Rel" by(rule Closed)
      with S \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close> \<open>distinctPerm p\<close>
      have "(\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R), Q', (p \<bullet> T) \<parallel> !Q) \<in> Rel" by(simp add: eqvts)
      then have "((\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R)) \<otimes> \<Psi>', Q', (p \<bullet> T) \<parallel> !Q) \<in> Rel" by(rule cExt)
      with \<open>(p \<bullet> \<Psi>\<^sub>R) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', Q', (p \<bullet> T) \<parallel> !Q) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* Q'\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> suppT suppS \<open>xvec \<sharp>* A\<^sub>R'\<close> \<open>(p \<bullet> xvec) \<sharp>* A\<^sub>R'\<close> S \<open>distinctPerm p\<close>
      have "(\<Psi>, R' \<parallel> Q', R' \<parallel> ((p \<bullet> T) \<parallel> !Q)) \<in> Rel"
        apply(intro FrameParPres)
            apply(assumption | simp)+
        apply(simp add: freshChainSimps)
        by(auto simp add: fresh_star_def fresh_def)
      then have "(\<Psi>, R' \<parallel> Q', (R' \<parallel> (p \<bullet> T)) \<parallel> !Q) \<in> Rel" by(blast intro: Assoc Trans)
      with \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* (!Q)\<close> have "(\<Psi>, \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> Q'), (\<lparr>\<nu>*xvec\<rparr>(R' \<parallel> (p \<bullet> T))) \<parallel> !Q) \<in> Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      ultimately have "(\<Psi>, \<lparr>\<nu>*(p \<bullet> xvec)\<rparr>((p \<bullet> R') \<parallel> P'), \<lparr>\<nu>*xvec\<rparr>(R' \<parallel> Q')) \<in> Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cBrMerge \<Psi>\<^sub>Q M N R' A\<^sub>R \<Psi>\<^sub>R Q' A\<^sub>Q)
    from \<open>extractFrame (!Q) = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> have "A\<^sub>Q = []" and "\<Psi>\<^sub>Q = SBottom'" by simp+
    have RTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>\<questiondown>M\<lparr>N\<rparr> \<prec> R'" and FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>" by fact+
    have QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>\<questiondown>M\<lparr>N\<rparr> \<prec> Q'" by fact
    with \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close>
    obtain P' S T where PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !P \<longmapsto>\<questiondown>M\<lparr>N\<rparr> \<prec> P'" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel"
      and "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel"
      and suppT: "((supp T)::name set) \<subseteq> supp P'" and suppS: "((supp S)::name set) \<subseteq> supp Q'"
      by(drule_tac cSym) (auto dest: Der intro: cExt)
    with RTrans QTrans FrR have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<questiondown>M\<lparr>N\<rparr> \<prec> (R' \<parallel> P')"
      using PTrans \<open>\<Psi>\<^sub>Q = SBottom'\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* P\<close>
      by(intro BrMerge) (assumption | simp)+

    moreover from \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* N\<close> PTrans QTrans
    have "A\<^sub>R \<sharp>* P'" and "A\<^sub>R \<sharp>* Q'" by(force dest: brinputFreshChainDerivative)+
    moreover with RTrans FrR \<open>distinct A\<^sub>R\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* N\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* M\<close>
    obtain \<Psi>' A\<^sub>R' \<Psi>\<^sub>R' where FrR': "extractFrame R' = \<langle>A\<^sub>R', \<Psi>\<^sub>R'\<rangle>" and "\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'" and "A\<^sub>R' \<sharp>* \<Psi>"
      and "A\<^sub>R' \<sharp>* P'" and "A\<^sub>R' \<sharp>* Q'" and "A\<^sub>R' \<sharp>* P" and "A\<^sub>R' \<sharp>* Q"
      by(auto intro: expandFrame[where C="(\<Psi>, P, P', Q, Q')" and C'=\<Psi>])

    moreover
    {
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel\<close> have "((\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>', P', T \<parallel> !P) \<in> Rel" by(rule cExt)
      with \<open>\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', P', T \<parallel> !P) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* P\<close> suppT have "(\<Psi>, R' \<parallel> P', R' \<parallel> (T \<parallel> !P)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have one: "(\<Psi>, R' \<parallel> P', (R' \<parallel> T) \<parallel> !P) \<in> Rel" by(blast intro: Assoc Trans)
      from \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close> \<open>guarded Q\<close> have two: "(\<Psi>, (R' \<parallel> T) \<parallel> !P, (R' \<parallel> T) \<parallel> !Q) \<in> Rel'"
        by(rule C1)
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel\<close> \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', T \<parallel> !Q) \<in> Rel"
        by(blast intro: ParPres Trans)
      then have "((\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>', Q', T \<parallel> !Q) \<in> Rel" by(rule cExt)
      with \<open>\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', Q', T \<parallel> !Q) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* Q'\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> suppT suppS have "(\<Psi>, R' \<parallel> Q', R' \<parallel> (T \<parallel> !Q)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have three: "(\<Psi>, R' \<parallel> Q', (R' \<parallel> T) \<parallel> !Q) \<in> Rel" by(blast intro: Assoc Trans)
      from one two three have "(\<Psi>, (R' \<parallel> P'), (R' \<parallel> Q')) \<in> Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cBrComm1 \<Psi>\<^sub>Q M N R' A\<^sub>R \<Psi>\<^sub>R xvec Q' A\<^sub>Q)
    from \<open>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> = \<alpha>\<close> have "xvec=bn \<alpha>"
      by(auto simp add: action.inject)
    from \<open>xvec = bn \<alpha>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* R\<close>
    have "xvec \<sharp>* P" and "xvec \<sharp>* R" by simp+

    from \<open>extractFrame (!Q) = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> have "A\<^sub>Q = []" and "\<Psi>\<^sub>Q = SBottom'" by simp+
    have RTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>\<questiondown>M\<lparr>N\<rparr> \<prec> R'" and FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>" by fact+
    moreover have QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'" by fact
    from FrR \<open>xvec \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* xvec\<close> have "xvec \<sharp>* \<Psi>\<^sub>R" by(force dest: extractFrameFreshChain)
    with QTrans \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>xvec \<sharp>* \<Psi>\<close>\<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>guarded P\<close> \<open>xvec \<sharp>* M\<close>
    obtain P' S T where PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !P \<longmapsto>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel"
      and "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel"
      and suppT: "((supp T)::name set) \<subseteq> supp P'" and suppS: "((supp S)::name set) \<subseteq> supp Q'"
      apply(drule_tac cSym)
      by(metis Der \<open>bn \<alpha> \<sharp>* Q\<close> \<open>xvec = bn \<alpha>\<close> cBrComm1.hyps(30) cExt cSim.hyps(6) freshCompChain(1))

    ultimately have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (R' \<parallel> P')"
      using PTrans \<open>\<Psi>\<^sub>Q = SBottom'\<close> \<open>xvec \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* P\<close>
      by(intro BrComm1) (assumption | simp)+

    moreover from \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* xvec\<close> PTrans QTrans \<open>xvec \<sharp>* M\<close> \<open>distinct xvec\<close>
    have "A\<^sub>R \<sharp>* P'" and "A\<^sub>R \<sharp>* Q'" by(force dest: broutputFreshChainDerivative)+
    moreover with RTrans FrR \<open>distinct A\<^sub>R\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* N\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close> \<open>A\<^sub>R \<sharp>* M\<close>
    obtain \<Psi>' A\<^sub>R' \<Psi>\<^sub>R' where FrR': "extractFrame R' = \<langle>A\<^sub>R', \<Psi>\<^sub>R'\<rangle>" and "\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'" and "A\<^sub>R' \<sharp>* \<Psi>"
      and "A\<^sub>R' \<sharp>* P'" and "A\<^sub>R' \<sharp>* Q'" and "A\<^sub>R' \<sharp>* P" and "A\<^sub>R' \<sharp>* Q"
      by(auto intro: expandFrame[where C="(\<Psi>, P, P', Q, Q')" and C'=\<Psi>])

    moreover
    {
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel\<close> have "((\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>', P', T \<parallel> !P) \<in> Rel" by(rule cExt)
      with \<open>\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', P', T \<parallel> !P) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* P\<close> suppT have "(\<Psi>, R' \<parallel> P', R' \<parallel> (T \<parallel> !P)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have one: "(\<Psi>, R' \<parallel> P', (R' \<parallel> T) \<parallel> !P) \<in> Rel" by(blast intro: Assoc Trans)
      from \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close> \<open>guarded Q\<close> have two: "(\<Psi>, (R' \<parallel> T) \<parallel> !P, (R' \<parallel> T) \<parallel> !Q) \<in> Rel'"
        by(rule C1)
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', S \<parallel> !Q) \<in> Rel\<close> \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R, Q', T \<parallel> !Q) \<in> Rel"
        by(blast intro: ParPres Trans)
      then have "((\<Psi> \<otimes> \<Psi>\<^sub>R) \<otimes> \<Psi>', Q', T \<parallel> !Q) \<in> Rel" by(rule cExt)
      with \<open>\<Psi>\<^sub>R \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', Q', T \<parallel> !Q) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* Q'\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> suppT suppS have "(\<Psi>, R' \<parallel> Q', R' \<parallel> (T \<parallel> !Q)) \<in> Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have three: "(\<Psi>, R' \<parallel> Q', (R' \<parallel> T) \<parallel> !Q) \<in> Rel" by(blast intro: Assoc Trans)
      from one two three have "(\<Psi>, (R' \<parallel> P'), (R' \<parallel> Q')) \<in> Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cBrComm2 \<Psi>\<^sub>Q M xvec N R' A\<^sub>R \<Psi>\<^sub>R Q' A\<^sub>Q)
    from \<open>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> = \<alpha>\<close> have "xvec = bn \<alpha>"
      by(auto simp add: action.inject)
    from \<open>xvec = bn \<alpha>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* R\<close>
    have "xvec \<sharp>* P" and "xvec \<sharp>* R" by simp+

    from \<open>extractFrame (!Q) = \<langle>A\<^sub>Q, \<Psi>\<^sub>Q\<rangle>\<close> have "A\<^sub>Q = []" and "\<Psi>\<^sub>Q = SBottom'" by simp+
    have RTrans: "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> R'" and FrR: "extractFrame R = \<langle>A\<^sub>R, \<Psi>\<^sub>R\<rangle>" by fact+
    then obtain p \<Psi>' A\<^sub>R' \<Psi>\<^sub>R' where S: "set p \<subseteq> set xvec \<times> set(p \<bullet> xvec)"
      and FrR': "extractFrame R' = \<langle>A\<^sub>R', \<Psi>\<^sub>R'\<rangle>" and "(p \<bullet> \<Psi>\<^sub>R) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'" and "A\<^sub>R' \<sharp>* \<Psi>"
      and "A\<^sub>R' \<sharp>* N" and "A\<^sub>R' \<sharp>* M" and "A\<^sub>R' \<sharp>* R" and "A\<^sub>R' \<sharp>* R'" and "A\<^sub>R' \<sharp>* P" and "A\<^sub>R' \<sharp>* Q" and "(p \<bullet> xvec) \<sharp>* \<Psi>"
      and "(p \<bullet> xvec) \<sharp>* P" and "(p \<bullet> xvec) \<sharp>* Q" and "xvec \<sharp>* A\<^sub>R'" and "(p \<bullet> xvec) \<sharp>* A\<^sub>R'"
      and "distinctPerm p" and "(p \<bullet> xvec) \<sharp>* R" and "(p \<bullet> xvec) \<sharp>* R'" and "(p \<bullet> xvec) \<sharp>* N" and "(p \<bullet> xvec) \<sharp>* M"
      using \<open>distinct A\<^sub>R\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* xvec\<close> \<open>A\<^sub>R \<sharp>* N\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* (!Q)\<close>
        \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>xvec \<sharp>* R\<close> \<open>xvec \<sharp>* M\<close> \<open>distinct xvec\<close>
      by(auto intro: expandFrame[where C="(\<Psi>, P, R, Q, M)" and C'="(\<Psi>, P, R, Q, M)"])

    from RTrans S \<open>(p \<bullet> xvec) \<sharp>* N\<close> \<open>(p \<bullet> xvec) \<sharp>* R'\<close> have "\<Psi> \<otimes> \<Psi>\<^sub>Q \<rhd> R \<longmapsto>\<exclamdown>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> R')"
      apply(simp add: residualInject)
      by(subst boundOutputChainAlpha''[symmetric]) auto

    moreover have QTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>\<questiondown>M\<lparr>N\<rparr> \<prec> Q'" by fact
    with QTrans S \<open>(p \<bullet> xvec) \<sharp>* N\<close> have "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !Q \<longmapsto>\<questiondown>M\<lparr>(p \<bullet> N)\<rparr> \<prec> (p \<bullet> Q')" using \<open>distinctPerm p\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close>
      by(intro brinputAlpha) auto
    with \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close>
    obtain P' S T where PTrans: "\<Psi> \<otimes> \<Psi>\<^sub>R \<rhd> !P \<longmapsto>\<questiondown>M\<lparr>(p \<bullet> N)\<rparr> \<prec> P'" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel"
      and "(\<Psi> \<otimes> \<Psi>\<^sub>R, (p \<bullet> Q'), S \<parallel> !Q) \<in> Rel" and "(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel"
      and suppT: "((supp T)::name set) \<subseteq> supp P'" and suppS: "((supp S)::name set) \<subseteq> supp(p \<bullet> Q')"
      by(drule_tac cSym) (auto dest: Der cExt)
    ultimately have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<exclamdown>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> ((p \<bullet> R') \<parallel> P')"
      using PTrans FrR \<open>\<Psi>\<^sub>Q = SBottom'\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> \<open>A\<^sub>R \<sharp>* \<Psi>\<close> \<open>A\<^sub>R \<sharp>* R\<close> \<open>A\<^sub>R \<sharp>* M\<close> \<open>A\<^sub>R \<sharp>* P\<close>
      by(intro BrComm2) (assumption | simp)+
    then have "p \<bullet> (\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<exclamdown>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> ((p \<bullet> R') \<parallel> P'))" by simp
    with \<open>distinctPerm p\<close> have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> R) \<parallel> !(p \<bullet> P) \<longmapsto>\<exclamdown>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (R' \<parallel> (p \<bullet> P'))"
      by(simp add: eqvts)
    with S \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* R\<close> \<open>(p \<bullet> xvec) \<sharp>* R\<close>
      \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> \<open>xvec \<sharp>* M\<close> \<open>(p \<bullet> xvec) \<sharp>* M\<close>
    have "\<Psi> \<rhd> R \<parallel> !P \<longmapsto>\<exclamdown>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (R' \<parallel> (p \<bullet> P'))"
      by simp

    moreover from \<open>A\<^sub>R' \<sharp>* P\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> \<open>A\<^sub>R' \<sharp>* N\<close> S \<open>xvec \<sharp>* A\<^sub>R'\<close> \<open>(p \<bullet> xvec) \<sharp>* A\<^sub>R'\<close> PTrans QTrans \<open>distinctPerm p\<close> have "A\<^sub>R' \<sharp>* P'" and "A\<^sub>R' \<sharp>* Q'"
       apply(drule_tac brinputFreshChainDerivative, simp)
        apply(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ _ p], simp)
       apply force
      using QTrans \<open>A\<^sub>R' \<sharp>* N\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> brinputFreshChainDerivative by force
    from \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* N\<close> PTrans \<open>distinctPerm p\<close> have "(p \<bullet> xvec) \<sharp>* (p \<bullet> P')"
      apply(drule_tac brinputFreshChainDerivative, simp)
       apply(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ _ p], simp)
      by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ _ p], simp)

    {
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, P', T \<parallel> !P) \<in> Rel\<close> have "(p \<bullet> (\<Psi> \<otimes> \<Psi>\<^sub>R), (p \<bullet> P'), p \<bullet> (T \<parallel> !P)) \<in> Rel"
        by(rule Closed)
      with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> S have "(\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R), p \<bullet> P', (p \<bullet> T) \<parallel> !P) \<in> Rel"
        by(simp add: eqvts)
      then have "((\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R)) \<otimes> \<Psi>', p \<bullet> P', (p \<bullet> T) \<parallel> !P) \<in> Rel"
        by(rule cExt)
      with \<open>(p \<bullet> \<Psi>\<^sub>R) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', (p \<bullet> P'), (p \<bullet> T) \<parallel> !P) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* P\<close> \<open>xvec \<sharp>* A\<^sub>R'\<close> \<open>(p \<bullet> xvec) \<sharp>* A\<^sub>R'\<close> S \<open>distinctPerm p\<close> suppT
      have "(\<Psi>, R' \<parallel> (p \<bullet> P'), R' \<parallel> ((p \<bullet> T) \<parallel> !P)) \<in> Rel"
        apply(intro FrameParPres)
            apply(assumption | simp add: freshChainSimps)+
        by(auto simp add: fresh_star_def fresh_def)
      then have one: "(\<Psi>, R' \<parallel> (p \<bullet> P'), (R' \<parallel> (p \<bullet> T)) \<parallel> !P) \<in> Rel" by(blast intro: Assoc Trans)
      from \<open>(\<Psi>, P, Q) \<in> Rel\<close> \<open>guarded P\<close> \<open>guarded Q\<close> have two: "(\<Psi>, (R' \<parallel> (p \<bullet> T)) \<parallel> !P, (R' \<parallel> (p \<bullet> T)) \<parallel> !Q) \<in> Rel'"
        by(rule C1)
      from \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, (p \<bullet> Q'), S \<parallel> !Q) \<in> Rel\<close> \<open>(\<Psi> \<otimes> \<Psi>\<^sub>R, S, T) \<in> Rel\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R, (p \<bullet> Q'), T \<parallel> !Q) \<in> Rel"
        by(blast intro: ParPres Trans)
      then have "(p \<bullet> (\<Psi> \<otimes> \<Psi>\<^sub>R), p \<bullet> p \<bullet> Q', p \<bullet> (T \<parallel> !Q)) \<in> Rel" by(rule Closed)
      with S \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* (!Q)\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close> \<open>distinctPerm p\<close>
      have "(\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R), Q', (p \<bullet> T) \<parallel> !Q) \<in> Rel" by(simp add: eqvts)
      then have "((\<Psi> \<otimes> (p \<bullet> \<Psi>\<^sub>R)) \<otimes> \<Psi>', Q', (p \<bullet> T) \<parallel> !Q) \<in> Rel" by(rule cExt)
      with \<open>(p \<bullet> \<Psi>\<^sub>R) \<otimes> \<Psi>' \<simeq> \<Psi>\<^sub>R'\<close> have "(\<Psi> \<otimes> \<Psi>\<^sub>R', Q', (p \<bullet> T) \<parallel> !Q) \<in> Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' \<open>A\<^sub>R' \<sharp>* \<Psi>\<close> \<open>A\<^sub>R' \<sharp>* P'\<close> \<open>A\<^sub>R' \<sharp>* Q'\<close> \<open>A\<^sub>R' \<sharp>* Q\<close> suppT suppS \<open>xvec \<sharp>* A\<^sub>R'\<close> \<open>(p \<bullet> xvec) \<sharp>* A\<^sub>R'\<close> S \<open>distinctPerm p\<close>
      have "(\<Psi>, R' \<parallel> Q', R' \<parallel> ((p \<bullet> T) \<parallel> !Q)) \<in> Rel"
        apply(intro FrameParPres)
            apply(assumption | simp)+
        apply(simp add: freshChainSimps)
        by(auto simp add: fresh_star_def fresh_def)
      then have three: "(\<Psi>, R' \<parallel> Q', (R' \<parallel> (p \<bullet> T)) \<parallel> !Q) \<in> Rel" by(blast intro: Assoc Trans)
      from one two three have "(\<Psi>, (R' \<parallel> (p \<bullet> P')), (R' \<parallel> Q')) \<in> Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  qed
qed

unbundle relcomp_syntax

end

end