Theory Sim_Pres

theory Sim_Pres
  imports Simulation
begin

text ‹This file is a (heavily modified) variant of the theory {\it Psi\_Calculi.Sim\_Pres}
from~\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: "⋀AR ΨR. ⟦extractFrame R = ⟨AR, ΨR⟩; AR ♯* Ψ; AR ♯* P; AR ♯* 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 AU ΨU U. ⟦(Ψ' ⊗ ΨU, S, T) ∈ Rel; extractFrame U = ⟨AU, ΨU⟩; AU ♯* Ψ'; AU ♯* S; AU ♯* 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' AR ΨR)
    from ‹AR ♯* (P, R)› have "AR ♯* P" by simp
    have FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact
    from ‹AR ♯* α› ‹bn α ♯* R› FrR have "bn α ♯* ΨR"
      by(auto dest: extractFrameFreshChain)
    from FrR ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* 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 ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* α› ‹bn α ♯* subject α› ‹distinct(bn α)› have "AR ♯* P'" and "AR ♯* Q'"
      by(blast dest: freeFreshChainDerivative)+
    from PTrans ‹bn α ♯* R› FrR  ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* α› have "Ψ ⊳ P ∥ R ⟼α ≺ (P' ∥ R)"
      by(metis Par1)
    moreover from P'RelQ' FrR ‹AR ♯* Ψ› ‹AR ♯* P'› ‹AR ♯* Q'› have "(Ψ, P' ∥ R, Q' ∥ R) ∈ Rel'" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 R' AQ ΨQ)
    from ‹AQ ♯* (P, R)› have "AQ ♯* P" and "AQ ♯* R" by simp+
    obtain AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* (Ψ, AQ, ΨQ, α, R)"
      by(rule freshFrame)
    then have "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* α" and "AP ♯* R"
      by simp+

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

    from FrP FrQ ‹bn α ♯* P› ‹bn α ♯* Q› ‹AP ♯* α› ‹AQ ♯* α›
    have "bn α ♯* ΨP" and "bn α ♯* ΨQ"
      by(force dest: extractFrameFreshChain)+

    obtain AR ΨR where FrR: "extractFrame R = ⟨AR, ΨR⟩" and "AR ♯* (Ψ, P, Q, AQ, AP, ΨQ, ΨP, α, R)" and "distinct AR"
      by(rule freshFrame)
    then have "AR ♯* Ψ" and "AR ♯* P" and "AR ♯* Q" and "AR ♯* AQ" and  "AR ♯* AP" and  "AR ♯* ΨQ" and  "AR ♯* ΨP" and "AR ♯* α" and "AR ♯* R"
      by simp+

    from ‹AQ ♯* R›  FrR ‹AR ♯* AQ› have "AQ ♯* ΨR"
      by(auto dest: extractFrameFreshChain)
    from ‹AP ♯* R› ‹AR ♯* AP› FrR  have "AP ♯* ΨR"
      by(auto dest: extractFrameFreshChain)

    have RTrans: "Ψ ⊗ ΨQ ⊳ R ⟼α ≺ R'" by fact
    moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ↪F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
    proof -
      have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ≃F ⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩"
        by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym FrameStatEqSym)
      moreover from FrR ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ ΨR)) ↪F (insertAssertion (extractFrame P) (Ψ ⊗ ΨR))"
        by(blast intro: PRelQ StatImp)
      with FrP FrQ ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* ΨR› ‹AQ ♯* ΨR›
      have "⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩ ↪F ⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩" using freshCompChain by auto
      moreover have "⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩ ≃F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
        by(metis frameIntAssociativity Commutativity FrameStatEqTrans frameIntCompositionSym frameIntAssociativity[THEN FrameStatEqSym])
      ultimately show ?thesis
        by(rule FrameStatEqImpCompose)
    qed

    ultimately have "Ψ ⊗ ΨP ⊳ R ⟼α ≺ R'"
      using ‹AP ♯* Ψ› ‹AP ♯* ΨQ› ‹AQ ♯* Ψ› ‹AQ ♯* ΨP› ‹AP ♯* R› ‹AQ ♯* R› ‹AP ♯* α› ‹AQ ♯* α›
        ‹AR ♯* AP› ‹AR ♯* AQ› ‹AR ♯* ΨP› ‹AR ♯* ΨQ› ‹AR ♯* Ψ› FrR ‹distinct AR›
      by(force intro: transferFrame)
    with ‹bn α ♯* P› ‹AP ♯* Ψ›  ‹AP ♯* R›  ‹AP ♯* α› FrP have "Ψ ⊳ P ∥ R ⟼α ≺ (P ∥ R')"
      by(force intro: Par2)
    moreover obtain AR' ΨR' where "extractFrame R' = ⟨AR', ΨR'⟩" and "AR' ♯* Ψ" and "AR' ♯* P" and "AR' ♯* Q"
      by(rule freshFrame[where C="(Ψ, P, Q)"]) auto

    moreover from RTrans FrR ‹distinct AR› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* R› ‹AR ♯* α› ‹bn α ♯* Ψ› ‹bn α  ♯* P› ‹bn α  ♯* Q› ‹bn α  ♯* R› ‹bn α ♯* subject α› ‹distinct(bn α)›
    obtain p Ψ' AR' ΨR' where S: "set p ⊆ set(bn α) × set(bn(p ∙ α))" and "(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'" and FrR': "extractFrame R' = ⟨AR', ΨR'⟩"
      and "bn(p ∙ α) ♯* R" and "bn(p ∙ α) ♯* Ψ" and "bn(p ∙ α) ♯* P" and "bn(p ∙ α) ♯* Q" and "bn(p ∙ α) ♯* R"
      and "AR' ♯* Ψ" and "AR' ♯* P" and "AR' ♯* Q"
      apply -
      apply (rule expandFrame[where C="(Ψ, P, Q, R)" and C'="(Ψ, P, Q, R)"])
                 apply simp+
      done

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

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

    with ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* 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' ‹AR' ♯* Ψ› ‹AR' ♯* P› ‹AR' ♯* Q› have "(Ψ, P ∥ R', Q ∥ R') ∈ Rel'"
      by(metis C1)
    ultimately show ?case by blast
  next
    case(cComm1 ΨR M N Q' AQ ΨQ K xvec R' AR)
    have  FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
    from ‹AQ ♯* (P, R)› have "AQ ♯* P" and "AQ ♯* R" by simp+

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

    from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+

    obtain AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* (Ψ, AQ, ΨQ, AR, M, N, K, R, P, xvec)" and "distinct AP"
      by(rule freshFrame)
    then have "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* M" and "AP ♯* R"
      and "AP ♯* N" and "AP ♯* K" and "AP ♯* AR" and "AP ♯* P" and "AP ♯* 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 ‹AQ ♯* P› ‹AP ♯* R› ‹AR ♯* P› ‹AP ♯* AQ› ‹AP ♯* AR› ‹AP ♯* xvec› ‹xvec ♯* P›
    have "AP ♯* ΨR" and "AQ ♯* ΨP" and  "AR ♯* ΨP" and "xvec ♯* ΨP"
      by(auto dest!: extractFrameFreshChain)+

    from RTrans FrR ‹distinct AR› ‹AR ♯* R› ‹AR ♯* xvec› ‹xvec ♯* R› ‹xvec ♯* Q› ‹xvec ♯* Ψ› ‹xvec ♯* ΨQ› ‹AR ♯* Q›
      ‹AR ♯* Ψ› ‹AR ♯* ΨQ› ‹xvec ♯* K› ‹AR ♯* K› ‹AR ♯* N› ‹AR ♯* R› ‹xvec ♯* R› ‹AR ♯* P› ‹xvec ♯* P› ‹AP ♯* AR› ‹AP ♯* xvec›
      ‹AQ ♯* AR› ‹AQ ♯* xvec› ‹AR ♯* ΨP› ‹xvec ♯* ΨP› ‹distinct xvec› ‹xvec ♯* M›
    obtain p Ψ' AR' ΨR' where S: "set p ⊆ set xvec × set(p ∙ xvec)" and FrR': "extractFrame R' = ⟨AR', ΨR'⟩"
      and "(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Q" and "AR' ♯* Ψ" 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) ♯* AP" and "(p ∙ xvec) ♯* AQ" and "(p ∙ xvec) ♯* ΨP"
      and "AR' ♯* P" and "AR' ♯* N"
      by (subst expandFrame[where C="(Ψ, Q, ΨQ, K, R, P, AP, AQ, ΨP)" and C'="(Ψ, Q, ΨQ, K, R, P, AP, AQ, ΨP)"]) simp+

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

    from ‹AP ♯* xvec› ‹(p ∙ xvec) ♯* AP› ‹AP ♯* M› S have "AP ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹AQ ♯* xvec› ‹(p ∙ xvec) ♯* AQ› ‹AQ ♯* M› S have "AQ ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹AP ♯* xvec› ‹(p ∙ xvec) ♯* AP› ‹AP ♯* AR› S have "(p ∙ AR) ♯* AP" by(simp add: freshChainSimps)
    from ‹AQ ♯* xvec› ‹(p ∙ xvec) ♯* AQ› ‹AQ ♯* AR› S have "(p ∙ AR) ♯* AQ" 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 ∙ ⟨AR, ΨR⟩" by simp
    with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have FrR: "extractFrame R = ⟨(p ∙ AR), (p ∙ ΨR)⟩"
      by(simp add: eqvts)

    note RTrans FrR
    moreover from FrR ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* 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 ‹AR' ♯* P› ‹AR' ♯* Q› ‹AR' ♯* N› have "AR' ♯* P'" and "AR' ♯* 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 "⟨AQ, (Ψ ⊗ ΨQ) ⊗ (p ∙ ΨR)⟩ ↪F ⟨AP, (Ψ ⊗ ΨP) ⊗ (p ∙ ΨR)⟩"
    proof -
      have "⟨AP, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨP⟩ ≃F ⟨AP, (Ψ ⊗ ΨP) ⊗ (p ∙ ΨR)⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ (p ∙ ΨR))) ↪F (insertAssertion (extractFrame P) (Ψ ⊗ (p ∙ ΨR)))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* ΨR› ‹AQ ♯* ΨR› ‹AP ♯* xvec› ‹(p ∙ xvec) ♯* AP› ‹AQ ♯* xvec› ‹(p ∙ xvec) ♯* AQ› S
      have "⟨AQ, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨQ⟩ ↪F ⟨AP, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨP⟩" using freshCompChain
        by(simp add: freshChainSimps)
      moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ (p ∙ ΨR)⟩ ≃F ⟨AQ, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨQ⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    moreover note FrP FrQ ‹distinct AP›
    moreover from ‹distinct AR› have "distinct(p ∙ AR)" by simp
    moreover note ‹(p ∙ AR) ♯* AP›  ‹(p ∙ AR) ♯* AQ› ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* Q› ‹(p ∙ AR) ♯* R› ‹(p ∙ AR) ♯* K›
      ‹AP ♯* Ψ› ‹AP ♯* R› ‹AP ♯* P› ‹AP ♯* (p ∙ M)› ‹AQ ♯* R› ‹AQ ♯* (p ∙ M)› ‹AP ♯* xvec› ‹xvec ♯* P› ‹AP ♯* R›
    ultimately obtain K' where "Ψ ⊗ ΨP ⊳ R ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ R'" and "Ψ ⊗ ΨP ⊗ (p ∙ ΨR) ⊢ (p ∙ M) ↔ K'" and "(p ∙ AR) ♯* K'"
      using comm1Aux by blast

    with PTrans FrP have "Ψ ⊳ P ∥ R ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ R')" using FrR ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* R›
        ‹xvec ♯* P› ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* R› ‹AP ♯* (p ∙ M)› ‹(p ∙ AR) ♯* K'› ‹(p ∙ AR) ♯* AP›
      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' ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Ψ› 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' AQ ΨQ K R' AR)
    have  FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
    from ‹AQ ♯* (P, R)› have "AQ ♯* P" and "AQ ♯* R" by simp+

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

    from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+

    obtain AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* (Ψ, AQ, ΨQ, AR, M, N, K, R, P, xvec)" and "distinct AP"
      by(rule freshFrame)
    then have "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* M" and "AP ♯* R"
      and "AP ♯* N" "AP ♯* K" and "AP ♯* AR" and "AP ♯* P"  and "AP ♯* xvec"
      by simp+

    from FrP FrR ‹AQ ♯* P› ‹AP ♯* R› ‹AR ♯* P› ‹AP ♯* AQ› ‹AP ♯* AR› ‹AP ♯* xvec› ‹xvec ♯* P›
    have "AP ♯* ΨR" and "AQ ♯* ΨP" and  "AR ♯* Ψ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 ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* 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 ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* xvec› ‹xvec ♯* M› ‹distinct xvec› have "AR ♯* P'" and "AR ♯* Q'"
      by(blast dest: outputFreshChainDerivative)+
    note PTrans ‹Ψ ⊗ ΨQ ⊗ ΨR ⊢ M ↔ K›
    moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ↪F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
    proof -
      have "⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩ ≃F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ ΨR)) ↪F (insertAssertion (extractFrame P) (Ψ ⊗ ΨR))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* ΨR› ‹AQ ♯* ΨR›
      have "⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩ ↪F ⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩" using freshCompChain by simp
      moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ≃F ⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    moreover note FrP FrQ ‹distinct AP› ‹distinct AR›
    moreover from ‹AP ♯* AR› ‹AQ ♯* AR› have "AR ♯* AP" and "AR ♯* AQ" by simp+
    moreover note ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* R› ‹AR ♯* K›  ‹AP ♯* Ψ› ‹AP ♯* P›
      ‹AP ♯* R› ‹AP ♯* M› ‹AQ ♯* R› ‹AQ ♯* M› ‹AR ♯* xvec› ‹xvec ♯* M›
    ultimately obtain K' where "Ψ ⊗ ΨP ⊳ R ⟼K'⦇N⦈ ≺ R'" and "Ψ ⊗ ΨP ⊗ ΨR ⊢ M ↔ K'" and "AR ♯* K'"
      using comm2Aux by blast

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

    moreover from ‹Ψ ⊗ ΨP ⊳ R ⟼K'⦇N⦈ ≺ R'› FrR ‹distinct AR› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* P'› ‹AR ♯* Q'› ‹AR ♯* N› ‹AR ♯* K'›
    obtain Ψ' AR' ΨR' where  ReqR': "ΨR ⊗ Ψ' ≃ ΨR'" and FrR': "extractFrame R' = ⟨AR', ΨR'⟩"
      and "AR' ♯* Ψ" and "AR' ♯* P'" and "AR' ♯* 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' ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Ψ› 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' AQ ΨQ R' AR)
    have  FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
    from ‹AQ ♯* (P, R)› have "AQ ♯* P" and "AQ ♯* R" by simp+

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

    obtain AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* (Ψ, AQ, ΨQ, AR, M, N, R, P)" and "distinct AP"
      by(rule freshFrame)
    then have "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* M" and "AP ♯* R"
      and "AP ♯* N" and "AP ♯* AR" and "AP ♯* P"
      by simp+

    from FrP FrR ‹AQ ♯* P› ‹AP ♯* R› ‹AR ♯* P› ‹AP ♯* AQ› ‹AP ♯* AR›
    have "AP ♯* ΨR" and "AQ ♯* ΨP" and  "AR ♯* Ψ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 ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* 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 ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* N› have "AR ♯* P'" and "AR ♯* Q'"
      by(blast dest: brinputFreshChainDerivative)+

    have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ↪F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
    proof -
      have "⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩ ≃F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ ΨR)) ↪F (insertAssertion (extractFrame P) (Ψ ⊗ ΨR))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* ΨR› ‹AQ ♯* ΨR›
      have "⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩ ↪F ⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩" using freshCompChain by simp
      moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ≃F ⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    with RTrans ‹extractFrame R = ⟨AR, ΨR⟩› ‹distinct AR› ‹AP ♯* AR› ‹AQ ♯* AR›
      ‹AR ♯* Ψ› ‹AR ♯* ΨP› ‹AR ♯* ΨQ› ‹AR ♯* R› ‹AR ♯* M› ‹AP ♯* R› ‹AP ♯* M› ‹AQ ♯* R› ‹AQ ♯* 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 ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* R›
        ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* R› ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* R› ‹AP ♯* AR› ‹AP ♯* M› ‹AR ♯* M›
      by(force intro: BrMerge)

    from ‹Ψ ⊗ ΨP ⊳ R ⟼¿M⦇N⦈ ≺ R'› FrR ‹distinct AR› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* P'› ‹AR ♯* Q'› ‹AR ♯* N› ‹AR ♯* M›
    obtain Ψ' AR' ΨR' where  ReqR': "ΨR ⊗ Ψ' ≃ ΨR'" and FrR': "extractFrame R' = ⟨AR', ΨR'⟩"
      and "AR' ♯* Ψ" and "AR' ♯* P'" and "AR' ♯* 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' ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Ψ› have Relation: "(Ψ, P' ∥ R', Q' ∥ R') ∈ Rel'"
      by(metis C1)
    show ?case using Transition Relation
      by blast
  next
    case(cBrComm1 ΨR M N Q' AQ ΨQ xvec R' AR)
    have  FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
    from ‹AQ ♯* (P, R)› have "AQ ♯* P" and "AQ ♯* R" by simp+

    have  FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact
    from ‹AR ♯* (P, R)› have "AR ♯* P" and "AR ♯* 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 AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* (Ψ, AQ, ΨQ, AR, M, N, R, P, xvec)" and "distinct AP"
      by(rule freshFrame)
    then have "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* M" and "AP ♯* R"
      and "AP ♯* N" and "AP ♯* AR" and "AP ♯* P" and "AP ♯* xvec"
      by simp+

    from FrP FrR ‹AQ ♯* P› ‹AP ♯* R› ‹AR ♯* P› ‹AP ♯* AQ› ‹AP ♯* AR›
    have "AP ♯* ΨR" and "AQ ♯* ΨP" and  "AR ♯* ΨP"
      by(auto dest: extractFrameFreshChain)+

    from ‹AP ♯* 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 AR› ‹AR ♯* R› ‹AR ♯* xvec› ‹xvec ♯* R› ‹xvec ♯* Q› ‹xvec ♯* Ψ› ‹xvec ♯* ΨQ› ‹AR ♯* Q›
      ‹AR ♯* Ψ› ‹AR ♯* ΨQ› ‹AR ♯* M› ‹AR ♯* N› ‹AR ♯* R› ‹xvec ♯* R› ‹AR ♯* P› ‹xvec ♯* P› ‹AP ♯* AR› ‹AP ♯* xvec›
      ‹AQ ♯* AR› ‹AQ ♯* xvec› ‹AR ♯* ΨP› ‹xvec ♯* ΨP› ‹distinct xvec› ‹xvec ♯* M›
    obtain p Ψ' AR' ΨR' where S: "set p ⊆ set xvec × set(p ∙ xvec)" and FrR': "extractFrame R' = ⟨AR', ΨR'⟩"
      and "(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Q" and "AR' ♯* Ψ" 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) ♯* AP" and "(p ∙ xvec) ♯* AQ" and "(p ∙ xvec) ♯* ΨP"
      and "AR' ♯* P" and "AR' ♯* N"
      by(auto intro: expandFrame[where C="(Ψ, Q, ΨQ, R, P, M, AP, AQ, ΨP)" and C'="(Ψ, Q, ΨQ, R, P, M, AP, AQ, ΨP)"])

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

    from ‹AP ♯* xvec› ‹(p ∙ xvec) ♯* AP› ‹AP ♯* M› S have "AP ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹AQ ♯* xvec› ‹(p ∙ xvec) ♯* AQ› ‹AQ ♯* M› S have "AQ ♯* (p ∙ M)" by(simp add: freshChainSimps)
    from ‹AP ♯* xvec› ‹(p ∙ xvec) ♯* AP› ‹AP ♯* AR› S have "(p ∙ AR) ♯* AP" by(simp add: freshChainSimps)
    from ‹AQ ♯* xvec› ‹(p ∙ xvec) ♯* AQ› ‹AQ ♯* AR› S have "(p ∙ AR) ♯* AQ" 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 ∙ ⟨AR, ΨR⟩" by simp
    with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have FrR: "extractFrame R = ⟨(p ∙ AR), (p ∙ ΨR)⟩"
      by(simp add: eqvts)

    from FrR ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* 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 ‹AR' ♯* P› ‹AR' ♯* Q› ‹AR' ♯* N› have "AR' ♯* P'" and "AR' ♯* Q'"
      by(blast dest: brinputFreshChainDerivative)+

    have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ (p ∙ ΨR)⟩ ↪F ⟨AP, (Ψ ⊗ ΨP) ⊗ (p ∙ ΨR)⟩"
    proof -
      have "⟨AP, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨP⟩ ≃F ⟨AP, (Ψ ⊗ ΨP) ⊗ (p ∙ ΨR)⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ (p ∙ ΨR))) ↪F (insertAssertion (extractFrame P) (Ψ ⊗ (p ∙ ΨR)))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* ΨR› ‹AQ ♯* ΨR› ‹AP ♯* xvec› ‹(p ∙ xvec) ♯* AP› ‹AQ ♯* xvec› ‹(p ∙ xvec) ♯* AQ› S
      have "⟨AQ, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨQ⟩ ↪F ⟨AP, (Ψ ⊗ (p ∙ ΨR)) ⊗ ΨP⟩" using freshCompChain
        by(simp add: freshChainSimps)
      moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ (p ∙ ΨR)⟩ ≃F ⟨AQ, (Ψ ⊗ (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 AP›
    moreover from ‹distinct AR› have "distinct(p ∙ AR)" by simp
    moreover note ‹(p ∙ AR) ♯* AP›  ‹(p ∙ AR) ♯* AQ› ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* ΨP› ‹(p ∙ AR) ♯* ΨQ› ‹(p ∙ AR) ♯* M› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* Q› ‹(p ∙ AR) ♯* R›
      ‹AP ♯* Ψ› ‹AP ♯* R› ‹AP ♯* P› ‹AP ♯* M› ‹AQ ♯* M› ‹AP ♯* (p ∙ M)› ‹AQ ♯* R› ‹AP ♯* xvec› ‹xvec ♯* P› ‹AP ♯* 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 ∙ AR) ♯* M› have "Ψ ⊳ P ∥ R ⟼¡(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ R')" using FrR ‹(p ∙ AR) ♯* Ψ› ‹(p ∙ AR) ♯* P› ‹(p ∙ AR) ♯* R›
        ‹xvec ♯* P› ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* R› ‹AP ♯* (p ∙ M)› ‹(p ∙ AR) ♯* AP›
      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' ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Ψ› 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' AQ ΨQ R' AR)
    have  FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
    from ‹AQ ♯* (P, R)› have "AQ ♯* P" and "AQ ♯* R" by simp+

    have  FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact
    from ‹AR ♯* (P, R)› have "AR ♯* P" and "AR ♯* 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 AP ΨP where FrP: "extractFrame P = ⟨AP, ΨP⟩" and "AP ♯* (Ψ, AQ, ΨQ, AR, M, N, R, P)" and "distinct AP"
      by(rule freshFrame)
    then have "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* M" and "AP ♯* R"
      and "AP ♯* N" and "AP ♯* AR" and "AP ♯* P"
      by simp+

    from FrP FrR ‹AQ ♯* P› ‹AP ♯* R› ‹AR ♯* P› ‹AP ♯* AQ› ‹AP ♯* AR›
    have "AP ♯* ΨR" and "AQ ♯* ΨP" and  "AR ♯* Ψ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 ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* 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 ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* N› ‹AR ♯* xvec› ‹xvec ♯* M› ‹distinct xvec› have "AR ♯* P'" and "AR ♯* Q'"
      by(blast dest: broutputFreshChainDerivative)+

    have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ↪F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
    proof -
      have "⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩ ≃F ⟨AP, (Ψ ⊗ ΨP) ⊗ ΨR⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      moreover from FrR ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q›
      have "(insertAssertion (extractFrame Q) (Ψ ⊗ ΨR)) ↪F (insertAssertion (extractFrame P) (Ψ ⊗ ΨR))"
        by(metis PRelQ StatImp)
      with FrP FrQ ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* ΨR› ‹AQ ♯* ΨR›
      have "⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩ ↪F ⟨AP, (Ψ ⊗ ΨR) ⊗ ΨP⟩" using freshCompChain by simp
      moreover have "⟨AQ, (Ψ ⊗ ΨQ) ⊗ ΨR⟩ ≃F ⟨AQ, (Ψ ⊗ ΨR) ⊗ ΨQ⟩"
        by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
      ultimately show ?thesis
        by(metis FrameStatEqImpCompose)
    qed
    with RTrans ‹extractFrame R = ⟨AR, ΨR⟩› ‹distinct AR› ‹AP ♯* AR› ‹AQ ♯* AR›
      ‹AR ♯* Ψ› ‹AR ♯* ΨP› ‹AR ♯* ΨQ› ‹AR ♯* R› ‹AR ♯* M› ‹AP ♯* R› ‹AP ♯* M› ‹AQ ♯* R› ‹AQ ♯* 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 ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* R›
        ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* R› ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* R› ‹AP ♯* AR› ‹AP ♯* M› ‹AR ♯* M› ‹xvec ♯* R›
      by(force intro: BrComm2)

    from ‹Ψ ⊗ ΨP ⊳ R ⟼¿M⦇N⦈ ≺ R'› FrR ‹distinct AR› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* P'› ‹AR ♯* Q'› ‹AR ♯* N› ‹AR ♯* M›
    obtain Ψ' AR' ΨR' where  ReqR': "ΨR ⊗ Ψ' ≃ ΨR'" and FrR': "extractFrame R' = ⟨AR', ΨR'⟩"
      and "AR' ♯* Ψ" and "AR' ♯* P'" and "AR' ♯* 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' ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Ψ› 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 AU. ⟦(Ψ' ⊗ ΨU, S, T) ∈ Rel; extractFrame U = ⟨AU, ΨU⟩; AU ♯* Ψ'; AU ♯* S; AU ♯* 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' AQ ΨQ)
    from ‹extractFrame (!Q) = ⟨AQ, ΨQ⟩› have "AQ = []" 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' AR ΨR)
    have QTrans: "Ψ ⊗ ΨR ⊳ !Q ⟼α ≺ Q'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
    with ‹bn α ♯* R› ‹AR ♯* α› have "bn α ♯* ΨR" by(force dest: extractFrameFreshChain)
    with QTrans ‹(Ψ, P, Q) ∈ Rel› ‹bn α ♯* Ψ›‹bn α ♯* P› ‹bn α ♯* Q› ‹guarded P› ‹bn α ♯* subject α›
    obtain P' S T where PTrans: "Ψ ⊗ ΨR ⊳ !P ⟼α ≺ P'" and "(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel"
      and "(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel" and "(Ψ ⊗ ΨR, S, T) ∈ Rel"
      and suppT: "((supp T)::name set) ⊆ supp P'" and suppS: "((supp S)::name set) ⊆ supp Q'"
      by(drule_tac cSym) (auto dest: Der cExt)
    from PTrans FrR ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* α› ‹bn α ♯* R› have "Ψ ⊳ R ∥ !P ⟼α ≺ (R ∥ P')"
      by(intro Par2) auto
    moreover
    {
      from ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* α› PTrans QTrans ‹bn α ♯* subject α› ‹distinct(bn α)› have "AR ♯* P'" and "AR ♯* Q'"
        by(force dest: freeFreshChainDerivative)+
      from ‹(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel› FrR ‹AR ♯* Ψ› ‹AR ♯* P'› ‹AR ♯* P› suppT have "(Ψ, R ∥ P', R ∥ (T ∥ !P)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(Ψ, R ∥ P', (R ∥ T) ∥ !P) ∈ Rel" by(blast intro: Assoc Trans)
      moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have "(Ψ, (R ∥ T) ∥ !P, (R ∥ T) ∥ !Q) ∈ Rel'"
        by(rule C1)
      moreover from ‹(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel› ‹(Ψ ⊗ ΨR, S, T) ∈ Rel› have "(Ψ ⊗ ΨR, Q', T ∥ !Q) ∈ Rel"
        by(blast intro: ParPres Trans)
      with FrR ‹AR ♯* Ψ› ‹AR ♯* P'› ‹AR ♯* Q'› ‹AR ♯* (!Q)› suppT suppS have "(Ψ, R ∥ Q', R ∥ (T ∥ !Q)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(Ψ, R ∥ Q', (R ∥ T) ∥ !Q) ∈ Rel" by(blast intro: Assoc Trans)
      ultimately have "(Ψ, R ∥ P', R ∥ Q') ∈ Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cComm1 ΨQ M N R' AR ΨR K xvec Q' AQ)
    from ‹extractFrame (!Q) = ⟨AQ, ΨQ⟩› have "AQ = []" and "ΨQ = SBottom'" by simp+
    have RTrans: "Ψ ⊗ ΨQ ⊳ R ⟼M⦇N⦈ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
    moreover have QTrans: "Ψ ⊗ ΨR ⊳ !Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'" by fact
    from FrR ‹xvec ♯* R› ‹AR ♯* xvec› have "xvec ♯* ΨR" by(force dest: extractFrameFreshChain)
    with QTrans ‹(Ψ, P, Q) ∈ Rel› ‹xvec ♯* Ψ›‹xvec ♯* P› ‹xvec ♯* (!Q)› ‹guarded P› ‹xvec ♯* K›
    obtain P' S T where PTrans: "Ψ ⊗ ΨR ⊳ !P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'" and "(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel"
      and "(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel" and "(Ψ ⊗ ΨR, S, T) ∈ Rel"
      and suppT: "((supp T)::name set) ⊆ supp P'" and suppS: "((supp S)::name set) ⊆ supp Q'"
      apply(drule_tac cSym)
      by (metis Der bn.simps(3) cExt freshCompChain(1) optionFreshChain(1) psiFreshVec(7) subject.simps(3))
    note ‹Ψ ⊗ ΨR ⊗ ΨQ ⊢ M ↔ K›
    ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*xvec⦈(R' ∥ P')"
      using PTrans ‹ΨQ = SBottom'› ‹xvec ♯* R› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* P›
      by(intro Comm1) (assumption | simp)+

    moreover from ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* xvec› PTrans QTrans ‹xvec ♯* K› ‹distinct xvec›
    have "AR ♯* P'" and "AR ♯* Q'" by(force dest: outputFreshChainDerivative)+
    moreover with RTrans FrR ‹distinct AR› ‹AR ♯* R› ‹AR ♯* N› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* M›
    obtain Ψ' AR' ΨR' where FrR': "extractFrame R' = ⟨AR', ΨR'⟩" and "ΨR ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Ψ"
      and "AR' ♯* P'" and "AR' ♯* Q'" and "AR' ♯* P" and "AR' ♯* Q"
      by(auto intro: expandFrame[where C="(Ψ, P, P', Q, Q')" and C'=Ψ])

    moreover
    {
      from ‹(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel› have "((Ψ ⊗ ΨR) ⊗ Ψ', P', T ∥ !P) ∈ Rel" by(rule cExt)
      with ‹ΨR ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', P', T ∥ !P) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* P› suppT have "(Ψ, R' ∥ P', R' ∥ (T ∥ !P)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(Ψ, R' ∥ P', (R' ∥ T) ∥ !P) ∈ Rel" by(blast intro: Assoc Trans)
      with ‹xvec ♯* Ψ› ‹xvec ♯* P› have "(Ψ, ⦇ν*xvec⦈(R' ∥ P'), (⦇ν*xvec⦈(R' ∥ T)) ∥ !P) ∈ Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have "(Ψ, (⦇ν*xvec⦈(R' ∥ T)) ∥ !P, (⦇ν*xvec⦈(R' ∥ T)) ∥ !Q) ∈ Rel'"
        by(rule C1)
      moreover from ‹(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel› ‹(Ψ ⊗ ΨR, S, T) ∈ Rel› have "(Ψ ⊗ ΨR, Q', T ∥ !Q) ∈ Rel"
        by(blast intro: ParPres Trans)
      then have "((Ψ ⊗ ΨR) ⊗ Ψ', Q', T ∥ !Q) ∈ Rel" by(rule cExt)
      with ‹ΨR ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', Q', T ∥ !Q) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Q› suppT suppS have "(Ψ, R' ∥ Q', R' ∥ (T ∥ !Q)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have "(Ψ, R' ∥ Q', (R' ∥ T) ∥ !Q) ∈ Rel" by(blast intro: Assoc Trans)
      with ‹xvec ♯* Ψ› ‹xvec ♯* (!Q)› have "(Ψ, ⦇ν*xvec⦈(R' ∥ Q'), (⦇ν*xvec⦈(R' ∥ T)) ∥ !Q) ∈ Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      ultimately have "(Ψ, ⦇ν*xvec⦈(R' ∥ P'), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cComm2 ΨQ M xvec N R' AR ΨR K Q' AQ)
    from ‹extractFrame (!Q) = ⟨AQ, ΨQ⟩› have "AQ = []" and "ΨQ = SBottom'" by simp+
    have RTrans: "Ψ ⊗ ΨQ ⊳ R ⟼M⦇ν*xvec⦈⟨N⟩ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
    then obtain p Ψ' AR' ΨR' where S: "set p ⊆ set xvec × set(p ∙ xvec)"
      and FrR': "extractFrame R' = ⟨AR', ΨR'⟩" and "(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Ψ"
      and "AR' ♯* N" and "AR' ♯* R'" and "AR' ♯* P" and "AR' ♯* Q" and "(p ∙ xvec) ♯* Ψ"
      and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "xvec ♯* AR'" and "(p ∙ xvec) ♯* AR'"
      and "distinctPerm p" and "(p ∙ xvec) ♯* R'" and "(p ∙ xvec) ♯* N"
      using ‹distinct AR› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* xvec› ‹AR ♯* N› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* (!Q)›
        ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* (!Q)› ‹xvec ♯* R› ‹xvec ♯* M› ‹distinct xvec›
      by(auto intro: expandFrame[where C="(Ψ, P, Q)" and C'="(Ψ, P, Q)"])

    from RTrans S ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* R'› have "Ψ ⊗ ΨQ ⊳ R ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')"
      apply(simp add: residualInject)
      by(subst boundOutputChainAlpha''[symmetric]) auto

    moreover have QTrans: "Ψ ⊗ ΨR ⊳ !Q ⟼K⦇N⦈ ≺ Q'" by fact
    with QTrans S ‹(p ∙ xvec) ♯* N› have "Ψ ⊗ ΨR ⊳ !Q ⟼K⦇(p ∙ N)⦈ ≺ (p ∙ Q')" using ‹distinctPerm p› ‹xvec ♯* (!Q)› ‹(p ∙ xvec) ♯* Q›
      by(intro inputAlpha) auto
    with ‹(Ψ, P, Q) ∈ Rel› ‹guarded P›
    obtain P' S T where PTrans: "Ψ ⊗ ΨR ⊳ !P ⟼K⦇(p ∙ N)⦈ ≺ P'" and "(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel"
      and "(Ψ ⊗ ΨR, (p ∙ Q'), S ∥ !Q) ∈ Rel" and "(Ψ ⊗ ΨR, S, T) ∈ Rel"
      and suppT: "((supp T)::name set) ⊆ supp P'" and suppS: "((supp S)::name set) ⊆ supp(p ∙ Q')"
      by(drule_tac cSym) (auto dest: Der cExt)
    note ‹Ψ ⊗ ΨR ⊗ ΨQ ⊢ M ↔ K›
    ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ P')"
      using PTrans FrR ‹ΨQ = SBottom'› ‹(p ∙ xvec) ♯* P› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* P›
      by(intro Comm2) (assumption | simp)+

    moreover from ‹AR' ♯* P› ‹AR' ♯* Q› ‹AR' ♯* N› S ‹xvec ♯* AR'› ‹(p ∙ xvec) ♯* AR'› PTrans QTrans ‹distinctPerm p› have "AR' ♯* P'" and "AR' ♯* 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 ‹AR' ♯* N› ‹AR' ♯* Q› inputFreshChainDerivative by force
    from ‹xvec ♯* P› ‹(p ∙ xvec) ♯* N› PTrans ‹distinctPerm p› have "(p ∙ xvec) ♯* (p ∙ 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 ‹(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel› have "(p ∙ (Ψ ⊗ ΨR), (p ∙ P'), p ∙ (T ∥ !P)) ∈ Rel"
        by(rule Closed)
      with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S have "(Ψ ⊗ (p ∙ ΨR), p ∙ P', (p ∙ T) ∥ !P) ∈ Rel"
        by(simp add: eqvts)
      then have "((Ψ ⊗ (p ∙ ΨR)) ⊗ Ψ', p ∙ P', (p ∙ T) ∥ !P) ∈ Rel" by(rule cExt)
      with ‹(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', (p ∙ P'), (p ∙ T) ∥ !P) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* P› ‹xvec ♯* AR'› ‹(p ∙ xvec) ♯* AR'› S ‹distinctPerm p› suppT
      have "(Ψ, R' ∥ (p ∙ P'), R' ∥ ((p ∙ T) ∥ !P)) ∈ Rel"
        apply(intro FrameParPres)
            apply(assumption | simp add: freshChainSimps)+
        by(auto simp add: fresh_star_def fresh_def)
      then have "(Ψ, R' ∥ (p ∙ P'), (R' ∥ (p ∙ T)) ∥ !P) ∈ Rel" by(blast intro: Assoc Trans)
      with ‹xvec ♯* Ψ› ‹xvec ♯* P› have "(Ψ, ⦇ν*xvec⦈(R' ∥ (p ∙ P')), (⦇ν*xvec⦈(R' ∥ (p ∙ T))) ∥ !P) ∈ Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      then have "(Ψ, ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ P'), (⦇ν*xvec⦈(R' ∥ (p ∙ T))) ∥ !P) ∈ Rel"
        using ‹(p ∙ xvec) ♯* R'› ‹(p ∙ xvec) ♯* (p ∙ P')› S ‹distinctPerm p›
        apply(erule_tac rev_mp)
        by(subst resChainAlpha[of p]) auto
      moreover from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have "(Ψ, (⦇ν*xvec⦈(R' ∥ (p ∙ T))) ∥ !P, (⦇ν*xvec⦈(R' ∥ (p ∙ T))) ∥ !Q) ∈ Rel'"
        by(rule C1)
      moreover from ‹(Ψ ⊗ ΨR, (p ∙ Q'), S ∥ !Q) ∈ Rel› ‹(Ψ ⊗ ΨR, S, T) ∈ Rel› have "(Ψ ⊗ ΨR, (p ∙ Q'), T ∥ !Q) ∈ Rel"
        by(blast intro: ParPres Trans)
      then have "(p ∙ (Ψ ⊗ ΨR), p ∙ p ∙ Q', p ∙ (T ∥ !Q)) ∈ Rel" by(rule Closed)
      with S ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* (!Q)› ‹(p ∙ xvec) ♯* Q› ‹distinctPerm p›
      have "(Ψ ⊗ (p ∙ ΨR), Q', (p ∙ T) ∥ !Q) ∈ Rel" by(simp add: eqvts)
      then have "((Ψ ⊗ (p ∙ ΨR)) ⊗ Ψ', Q', (p ∙ T) ∥ !Q) ∈ Rel" by(rule cExt)
      with ‹(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', Q', (p ∙ T) ∥ !Q) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Q› suppT suppS ‹xvec ♯* AR'› ‹(p ∙ xvec) ♯* AR'› S ‹distinctPerm p›
      have "(Ψ, R' ∥ Q', R' ∥ ((p ∙ T) ∥ !Q)) ∈ Rel"
        apply(intro FrameParPres)
            apply(assumption | simp)+
        apply(simp add: freshChainSimps)
        by(auto simp add: fresh_star_def fresh_def)
      then have "(Ψ, R' ∥ Q', (R' ∥ (p ∙ T)) ∥ !Q) ∈ Rel" by(blast intro: Assoc Trans)
      with ‹xvec ♯* Ψ› ‹xvec ♯* (!Q)› have "(Ψ, ⦇ν*xvec⦈(R' ∥ Q'), (⦇ν*xvec⦈(R' ∥ (p ∙ T))) ∥ !Q) ∈ Rel"
        by(metis ResPres psiFreshVec ScopeExt Trans)
      ultimately have "(Ψ, ⦇ν*(p ∙ xvec)⦈((p ∙ R') ∥ P'), ⦇ν*xvec⦈(R' ∥ Q')) ∈ Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cBrMerge ΨQ M N R' AR ΨR Q' AQ)
    from ‹extractFrame (!Q) = ⟨AQ, ΨQ⟩› have "AQ = []" and "ΨQ = SBottom'" by simp+
    have RTrans: "Ψ ⊗ ΨQ ⊳ R ⟼¿M⦇N⦈ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
    have QTrans: "Ψ ⊗ ΨR ⊳ !Q ⟼¿M⦇N⦈ ≺ Q'" by fact
    with ‹(Ψ, P, Q) ∈ Rel› ‹guarded P›
    obtain P' S T where PTrans: "Ψ ⊗ ΨR ⊳ !P ⟼¿M⦇N⦈ ≺ P'" and "(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel"
      and "(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel" and "(Ψ ⊗ ΨR, S, T) ∈ Rel"
      and suppT: "((supp T)::name set) ⊆ supp P'" and suppS: "((supp S)::name set) ⊆ supp Q'"
      by(drule_tac cSym) (auto dest: Der intro: cExt)
    with RTrans QTrans FrR have "Ψ ⊳ R ∥ !P ⟼¿M⦇N⦈ ≺ (R' ∥ P')"
      using PTrans ‹ΨQ = SBottom'› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* P›
      by(intro BrMerge) (assumption | simp)+

    moreover from ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* N› PTrans QTrans
    have "AR ♯* P'" and "AR ♯* Q'" by(force dest: brinputFreshChainDerivative)+
    moreover with RTrans FrR ‹distinct AR› ‹AR ♯* R› ‹AR ♯* N› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* M›
    obtain Ψ' AR' ΨR' where FrR': "extractFrame R' = ⟨AR', ΨR'⟩" and "ΨR ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Ψ"
      and "AR' ♯* P'" and "AR' ♯* Q'" and "AR' ♯* P" and "AR' ♯* Q"
      by(auto intro: expandFrame[where C="(Ψ, P, P', Q, Q')" and C'=Ψ])

    moreover
    {
      from ‹(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel› have "((Ψ ⊗ ΨR) ⊗ Ψ', P', T ∥ !P) ∈ Rel" by(rule cExt)
      with ‹ΨR ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', P', T ∥ !P) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* P› suppT have "(Ψ, R' ∥ P', R' ∥ (T ∥ !P)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have one: "(Ψ, R' ∥ P', (R' ∥ T) ∥ !P) ∈ Rel" by(blast intro: Assoc Trans)
      from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have two: "(Ψ, (R' ∥ T) ∥ !P, (R' ∥ T) ∥ !Q) ∈ Rel'"
        by(rule C1)
      from ‹(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel› ‹(Ψ ⊗ ΨR, S, T) ∈ Rel› have "(Ψ ⊗ ΨR, Q', T ∥ !Q) ∈ Rel"
        by(blast intro: ParPres Trans)
      then have "((Ψ ⊗ ΨR) ⊗ Ψ', Q', T ∥ !Q) ∈ Rel" by(rule cExt)
      with ‹ΨR ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', Q', T ∥ !Q) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Q› suppT suppS have "(Ψ, R' ∥ Q', R' ∥ (T ∥ !Q)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have three: "(Ψ, R' ∥ Q', (R' ∥ T) ∥ !Q) ∈ Rel" by(blast intro: Assoc Trans)
      from one two three have "(Ψ, (R' ∥ P'), (R' ∥ Q')) ∈ Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cBrComm1 ΨQ M N R' AR ΨR xvec Q' AQ)
    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+

    from ‹extractFrame (!Q) = ⟨AQ, ΨQ⟩› have "AQ = []" and "ΨQ = SBottom'" by simp+
    have RTrans: "Ψ ⊗ ΨQ ⊳ R ⟼¿M⦇N⦈ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
    moreover have QTrans: "Ψ ⊗ ΨR ⊳ !Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q'" by fact
    from FrR ‹xvec ♯* R› ‹AR ♯* xvec› have "xvec ♯* ΨR" by(force dest: extractFrameFreshChain)
    with QTrans ‹(Ψ, P, Q) ∈ Rel› ‹xvec ♯* Ψ›‹xvec ♯* P› ‹xvec ♯* (!Q)› ‹guarded P› ‹xvec ♯* M›
    obtain P' S T where PTrans: "Ψ ⊗ ΨR ⊳ !P ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ P'" and "(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel"
      and "(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel" and "(Ψ ⊗ ΨR, S, T) ∈ Rel"
      and suppT: "((supp T)::name set) ⊆ supp P'" and suppS: "((supp S)::name set) ⊆ supp Q'"
      apply(drule_tac cSym)
      by(metis Der ‹bn α ♯* Q› ‹xvec = bn α› cBrComm1.hyps(30) cExt cSim.hyps(6) freshCompChain(1))

    ultimately have "Ψ ⊳ R ∥ !P ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ (R' ∥ P')"
      using PTrans ‹ΨQ = SBottom'› ‹xvec ♯* R› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* P›
      by(intro BrComm1) (assumption | simp)+

    moreover from ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* xvec› PTrans QTrans ‹xvec ♯* M› ‹distinct xvec›
    have "AR ♯* P'" and "AR ♯* Q'" by(force dest: broutputFreshChainDerivative)+
    moreover with RTrans FrR ‹distinct AR› ‹AR ♯* R› ‹AR ♯* N› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* (!Q)› ‹AR ♯* M›
    obtain Ψ' AR' ΨR' where FrR': "extractFrame R' = ⟨AR', ΨR'⟩" and "ΨR ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Ψ"
      and "AR' ♯* P'" and "AR' ♯* Q'" and "AR' ♯* P" and "AR' ♯* Q"
      by(auto intro: expandFrame[where C="(Ψ, P, P', Q, Q')" and C'=Ψ])

    moreover
    {
      from ‹(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel› have "((Ψ ⊗ ΨR) ⊗ Ψ', P', T ∥ !P) ∈ Rel" by(rule cExt)
      with ‹ΨR ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', P', T ∥ !P) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* P› suppT have "(Ψ, R' ∥ P', R' ∥ (T ∥ !P)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have one: "(Ψ, R' ∥ P', (R' ∥ T) ∥ !P) ∈ Rel" by(blast intro: Assoc Trans)
      from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have two: "(Ψ, (R' ∥ T) ∥ !P, (R' ∥ T) ∥ !Q) ∈ Rel'"
        by(rule C1)
      from ‹(Ψ ⊗ ΨR, Q', S ∥ !Q) ∈ Rel› ‹(Ψ ⊗ ΨR, S, T) ∈ Rel› have "(Ψ ⊗ ΨR, Q', T ∥ !Q) ∈ Rel"
        by(blast intro: ParPres Trans)
      then have "((Ψ ⊗ ΨR) ⊗ Ψ', Q', T ∥ !Q) ∈ Rel" by(rule cExt)
      with ‹ΨR ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', Q', T ∥ !Q) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Q› suppT suppS have "(Ψ, R' ∥ Q', R' ∥ (T ∥ !Q)) ∈ Rel"
        by(intro FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      then have three: "(Ψ, R' ∥ Q', (R' ∥ T) ∥ !Q) ∈ Rel" by(blast intro: Assoc Trans)
      from one two three have "(Ψ, (R' ∥ P'), (R' ∥ Q')) ∈ Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  next
    case(cBrComm2 ΨQ M xvec N R' AR ΨR Q' AQ)
    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+

    from ‹extractFrame (!Q) = ⟨AQ, ΨQ⟩› have "AQ = []" and "ΨQ = SBottom'" by simp+
    have RTrans: "Ψ ⊗ ΨQ ⊳ R ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
    then obtain p Ψ' AR' ΨR' where S: "set p ⊆ set xvec × set(p ∙ xvec)"
      and FrR': "extractFrame R' = ⟨AR', ΨR'⟩" and "(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'" and "AR' ♯* Ψ"
      and "AR' ♯* N" and "AR' ♯* M" and "AR' ♯* R" and "AR' ♯* R'" and "AR' ♯* P" and "AR' ♯* Q" and "(p ∙ xvec) ♯* Ψ"
      and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "xvec ♯* AR'" and "(p ∙ xvec) ♯* AR'"
      and "distinctPerm p" and "(p ∙ xvec) ♯* R" and "(p ∙ xvec) ♯* R'" and "(p ∙ xvec) ♯* N" and "(p ∙ xvec) ♯* M"
      using ‹distinct AR› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* xvec› ‹AR ♯* N› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* (!Q)›
        ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* (!Q)› ‹xvec ♯* R› ‹xvec ♯* M› ‹distinct xvec›
      by(auto intro: expandFrame[where C="(Ψ, P, R, Q, M)" and C'="(Ψ, P, R, Q, M)"])

    from RTrans S ‹(p ∙ xvec) ♯* N› ‹(p ∙ xvec) ♯* R'› have "Ψ ⊗ ΨQ ⊳ R ⟼¡M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ R')"
      apply(simp add: residualInject)
      by(subst boundOutputChainAlpha''[symmetric]) auto

    moreover have QTrans: "Ψ ⊗ ΨR ⊳ !Q ⟼¿M⦇N⦈ ≺ Q'" by fact
    with QTrans S ‹(p ∙ xvec) ♯* N› have "Ψ ⊗ ΨR ⊳ !Q ⟼¿M⦇(p ∙ N)⦈ ≺ (p ∙ Q')" using ‹distinctPerm p› ‹xvec ♯* (!Q)› ‹(p ∙ xvec) ♯* Q›
      by(intro brinputAlpha) auto
    with ‹(Ψ, P, Q) ∈ Rel› ‹guarded P›
    obtain P' S T where PTrans: "Ψ ⊗ ΨR ⊳ !P ⟼¿M⦇(p ∙ N)⦈ ≺ P'" and "(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel"
      and "(Ψ ⊗ ΨR, (p ∙ Q'), S ∥ !Q) ∈ Rel" and "(Ψ ⊗ ΨR, S, T) ∈ Rel"
      and suppT: "((supp T)::name set) ⊆ supp P'" and suppS: "((supp S)::name set) ⊆ supp(p ∙ Q')"
      by(drule_tac cSym) (auto dest: Der cExt)
    ultimately have "Ψ ⊳ R ∥ !P ⟼¡M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ ((p ∙ R') ∥ P')"
      using PTrans FrR ‹ΨQ = SBottom'› ‹(p ∙ xvec) ♯* P› ‹AR ♯* Ψ› ‹AR ♯* R› ‹AR ♯* M› ‹AR ♯* P›
      by(intro BrComm2) (assumption | simp)+
    then have "p ∙ (Ψ ⊳ R ∥ !P ⟼¡M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ ((p ∙ R') ∥ P'))" by simp
    with ‹distinctPerm p› have "(p ∙ Ψ) ⊳ (p ∙ R) ∥ !(p ∙ P) ⟼¡(p ∙ M)⦇ν*xvec⦈⟨N⟩ ≺ (R' ∥ (p ∙ P'))"
      by(simp add: eqvts)
    with S ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R›
      ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› ‹xvec ♯* M› ‹(p ∙ xvec) ♯* M›
    have "Ψ ⊳ R ∥ !P ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ (R' ∥ (p ∙ P'))"
      by simp

    moreover from ‹AR' ♯* P› ‹AR' ♯* Q› ‹AR' ♯* N› S ‹xvec ♯* AR'› ‹(p ∙ xvec) ♯* AR'› PTrans QTrans ‹distinctPerm p› have "AR' ♯* P'" and "AR' ♯* 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 ‹AR' ♯* N› ‹AR' ♯* Q› brinputFreshChainDerivative by force
    from ‹xvec ♯* P› ‹(p ∙ xvec) ♯* N› PTrans ‹distinctPerm p› have "(p ∙ xvec) ♯* (p ∙ 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 ‹(Ψ ⊗ ΨR, P', T ∥ !P) ∈ Rel› have "(p ∙ (Ψ ⊗ ΨR), (p ∙ P'), p ∙ (T ∥ !P)) ∈ Rel"
        by(rule Closed)
      with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S have "(Ψ ⊗ (p ∙ ΨR), p ∙ P', (p ∙ T) ∥ !P) ∈ Rel"
        by(simp add: eqvts)
      then have "((Ψ ⊗ (p ∙ ΨR)) ⊗ Ψ', p ∙ P', (p ∙ T) ∥ !P) ∈ Rel"
        by(rule cExt)
      with ‹(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', (p ∙ P'), (p ∙ T) ∥ !P) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* P› ‹xvec ♯* AR'› ‹(p ∙ xvec) ♯* AR'› S ‹distinctPerm p› suppT
      have "(Ψ, R' ∥ (p ∙ P'), R' ∥ ((p ∙ T) ∥ !P)) ∈ Rel"
        apply(intro FrameParPres)
            apply(assumption | simp add: freshChainSimps)+
        by(auto simp add: fresh_star_def fresh_def)
      then have one: "(Ψ, R' ∥ (p ∙ P'), (R' ∥ (p ∙ T)) ∥ !P) ∈ Rel" by(blast intro: Assoc Trans)
      from ‹(Ψ, P, Q) ∈ Rel› ‹guarded P› ‹guarded Q› have two: "(Ψ, (R' ∥ (p ∙ T)) ∥ !P, (R' ∥ (p ∙ T)) ∥ !Q) ∈ Rel'"
        by(rule C1)
      from ‹(Ψ ⊗ ΨR, (p ∙ Q'), S ∥ !Q) ∈ Rel› ‹(Ψ ⊗ ΨR, S, T) ∈ Rel› have "(Ψ ⊗ ΨR, (p ∙ Q'), T ∥ !Q) ∈ Rel"
        by(blast intro: ParPres Trans)
      then have "(p ∙ (Ψ ⊗ ΨR), p ∙ p ∙ Q', p ∙ (T ∥ !Q)) ∈ Rel" by(rule Closed)
      with S ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› ‹xvec ♯* (!Q)› ‹(p ∙ xvec) ♯* Q› ‹distinctPerm p›
      have "(Ψ ⊗ (p ∙ ΨR), Q', (p ∙ T) ∥ !Q) ∈ Rel" by(simp add: eqvts)
      then have "((Ψ ⊗ (p ∙ ΨR)) ⊗ Ψ', Q', (p ∙ T) ∥ !Q) ∈ Rel" by(rule cExt)
      with ‹(p ∙ ΨR) ⊗ Ψ' ≃ ΨR'› have "(Ψ ⊗ ΨR', Q', (p ∙ T) ∥ !Q) ∈ Rel"
        by(metis Associativity StatEq compositionSym)
      with FrR' ‹AR' ♯* Ψ› ‹AR' ♯* P'› ‹AR' ♯* Q'› ‹AR' ♯* Q› suppT suppS ‹xvec ♯* AR'› ‹(p ∙ xvec) ♯* AR'› S ‹distinctPerm p›
      have "(Ψ, R' ∥ Q', R' ∥ ((p ∙ T) ∥ !Q)) ∈ Rel"
        apply(intro FrameParPres)
            apply(assumption | simp)+
        apply(simp add: freshChainSimps)
        by(auto simp add: fresh_star_def fresh_def)
      then have three: "(Ψ, R' ∥ Q', (R' ∥ (p ∙ T)) ∥ !Q) ∈ Rel" by(blast intro: Assoc Trans)
      from one two three have "(Ψ, (R' ∥ (p ∙ P')), (R' ∥ Q')) ∈ Rel'" by(blast intro: cSym Compose)
    }
    ultimately show ?case by blast
  qed
qed

unbundle relcomp_syntax

end

end