Theory Sim_Pres

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

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(auto simp add: simulation_def residual.inject psi.inject)
  fix α Q'
  assume "Ψ ⊳ M⦇λ*xvec N⦈.Q ⟼α ≺ Q'"
  thus "∃P'. Ψ ⊳ M⦇λ*xvec N⦈.P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
    by(induct rule: inputCases) (auto intro: Input PRelQ)
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(auto simp add: simulation_def residual.inject psi.inject)
  fix α Q'
  assume "Ψ ⊳ M⟨N⟩.Q ⟼α ≺ Q'"
  thus "∃P'. Ψ ⊳ M⟨N⟩.P ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel"
    by(induct rule: outputCases) (auto intro: Output PRelQ)
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) mem CsQ ⟹ ∃P. (φ, P) mem 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(auto simp add: simulation_def residual.inject psi.inject)
  fix α Q'
  assume "Ψ ⊳ Cases CsQ ⟼α ≺ Q'" and "bn α ♯* CsP" and "bn α ♯* Ψ"
  thus "∃P'. Ψ ⊳ Cases CsP ⟼α ≺ P' ∧ (Ψ, P', Q') ∈ Rel'"
  proof(induct rule: caseCases)
    case(cCase φ Q)
    from ‹(φ, Q) mem CsQ› obtain P where "(φ, P) mem 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) mem 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) mem 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
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 y. ⟦(Ψ', R, S) ∈ Rel; y ♯ Ψ'⟧ ⟹ (Ψ', ⦇νy⦈R, ⦇νy⦈S) ∈ Rel'"

  shows   "Ψ ⊳ ⦇νx⦈P ↝[Rel'] ⦇νx⦈Q"
proof -
  note ‹eqvt Rel'› ‹x ♯ Ψ›
  moreover have "x ♯ ⦇νx⦈P" and "x ♯ ⦇νx⦈Q" by(simp add: abs_fresh)+
  ultimately show ?thesis
  proof(induct rule: 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)
      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)" 
        by(drule_tac pt_set_bij2[OF pt_name_inst, OF at_name_inst, where pi="[(x, y)]"]) (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(rule_tac Open)
      hence "([(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(rule C1)
      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 y. ⟦(Ψ', R, S) ∈ Rel; y ♯ Ψ'⟧ ⟹ (Ψ', ⦇νy⦈R, ⦇νy⦈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)
  thus ?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(drule_tac extractFrameFreshChain) auto
    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(rule_tac 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)
    hence "A⇩P ♯* Ψ" and "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* α" and "A⇩P ♯* R"
      by simp+

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

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


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

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

    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_tac 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"
      by(rule_tac C="(Ψ, P, Q, R)" and C'="(Ψ, P, Q, R)" in expandFrame) (assumption | simp)+

    from ‹A⇩R ♯* Ψ› have "(p ∙ A⇩R) ♯* (p ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    with ‹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(rule_tac PRelQ)

    hence "((Ψ ⊗ (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(rule_tac C1) 
    ultimately show ?case by blast
  next
    case(cComm1 Ψ⇩R M N Q' A⇩Q Ψ⇩Q K xvec R' A⇩R)
    have  FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
    from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+

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

    from ‹xvec ♯* (P, R)› have "xvec ♯* P" and "xvec ♯* R" by simp+
  
    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)
    hence "A⇩P ♯* Ψ" and "A⇩P ♯* A⇩Q" and "A⇩P ♯* Ψ⇩Q" and "A⇩P ♯* M" and "A⇩P ♯* R"
      and "A⇩P ♯* N" and "A⇩P ♯* K" and "A⇩P ♯* A⇩R" and "A⇩P ♯* P" and "A⇩P ♯* xvec"
      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(fastforce 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(rule_tac C="(Ψ, Q, Ψ⇩Q, K, R, P, A⇩P, A⇩Q, Ψ⇩P)" and C'="(Ψ, Q, Ψ⇩Q, K, R, P, A⇩P, A⇩Q, Ψ⇩P)" in expandFrame) 
      (assumption | simp)+

  from ‹A⇩R ♯* Ψ› have "(p ∙ A⇩R) ♯* (p ∙ Ψ)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have "(p ∙ A⇩R) ♯* Ψ" by simp
  from ‹A⇩R ♯* P› have "(p ∙ A⇩R) ♯* (p ∙ P)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  with ‹xvec ♯* P› ‹(p ∙ xvec) ♯* P› S have "(p ∙ A⇩R) ♯* P" by simp
  from ‹A⇩R ♯* Q› have "(p ∙ A⇩R) ♯* (p ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  with ‹xvec ♯* Q› ‹(p ∙ xvec) ♯* Q› S have "(p ∙ A⇩R) ♯* Q" by simp
  from ‹A⇩R ♯* R› have "(p ∙ A⇩R) ♯* (p ∙ R)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  with ‹xvec ♯* R› ‹(p ∙ xvec) ♯* R› S have "(p ∙ A⇩R) ♯* R" by simp
  from ‹A⇩R ♯* K› have "(p ∙ A⇩R) ♯* (p ∙ K)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  with ‹xvec ♯* K› ‹(p ∙ xvec) ♯* K› S have "(p ∙ A⇩R) ♯* K" by simp
  
  from ‹A⇩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'"
    by(rule_tac inputPermFrameSubject) (assumption | auto simp add: fresh_star_def)+
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have QTrans: "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊳ Q ⟼ (p ∙ M)⦇N⦈ ≺ Q'"
    by(simp add: eqvts)

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

  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(rule_tac 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'"
    by(rule_tac comm1Aux)

  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(rule_tac 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(rule_tac C1)
  with ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ R'), ⦇ν*xvec⦈(Q' ∥ R')) ∈ Rel'" by(rule_tac C2)
  ultimately show ?case by blast
next
    case(cComm2 Ψ⇩R M xvec N Q' A⇩Q Ψ⇩Q K R' A⇩R)
    have  FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" by fact
    from ‹A⇩Q ♯* (P, R)› have "A⇩Q ♯* P" and "A⇩Q ♯* R" by simp+

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

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

    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)
    hence "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(fastforce 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(rule_tac 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'"
      by(rule_tac comm2Aux) assumption+

    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(rule_tac C="(Ψ, P', Q')" and C'="Ψ" in expandFrame) auto

    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(rule_tac C1)
    with ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ R'), ⦇ν*xvec⦈(Q' ∥ R')) ∈ Rel'" by(rule_tac C2)
    ultimately show ?case 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(rule_tac 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 α ♯* Ψ›‹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 ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* α› ‹bn α ♯* R› have "Ψ ⊳ R ∥ !P ⟼α ≺ (R ∥ P')"
      by(rule_tac Par2) auto
    moreover 
    { 
      from ‹A⇩R ♯* P› ‹A⇩R ♯* (!Q)› ‹A⇩R ♯* α› PTrans QTrans ‹bn α ♯* subject α› ‹distinct(bn α)› have "A⇩R ♯* P'" and "A⇩R ♯* Q'"
        by(force dest: freeFreshChainDerivative)+
      from ‹(Ψ ⊗ Ψ⇩R, P', T ∥ !P) ∈ Rel› FrR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'› ‹A⇩R ♯* P› suppT have "(Ψ, R ∥ P', R ∥ (T ∥ !P)) ∈ Rel"
        by(rule_tac FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      hence "(Ψ, 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 ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P'› ‹A⇩R ♯* Q'› ‹A⇩R ♯* (!Q)› suppT suppS have "(Ψ, R ∥ Q', R ∥ (T ∥ !Q)) ∈ Rel"
        by(rule_tac FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      hence "(Ψ, 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' A⇩R Ψ⇩R K xvec Q' A⇩Q)
    from ‹extractFrame (!Q) = ⟨A⇩Q, Ψ⇩Q⟩› have "A⇩Q = []" and "Ψ⇩Q = SBottom'" by simp+
    have RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇N⦈ ≺ R'" and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact+
    moreover have QTrans: "Ψ ⊗ Ψ⇩R ⊳ !Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'" by fact
    from FrR ‹xvec ♯* R› ‹A⇩R ♯* 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'"
      by(drule_tac cSym) (fastforce dest: Der intro: cExt)
    note ‹Ψ ⊗ Ψ⇩R ⊗ Ψ⇩Q ⊢ M ↔ K›
    ultimately have "Ψ ⊳ R ∥ !P ⟼τ ≺ ⦇ν*xvec⦈(R' ∥ P')" 
      using PTrans ‹Ψ⇩Q = SBottom'› ‹xvec ♯* R› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* M› ‹A⇩R ♯* P›
      by(rule_tac Comm1) (assumption | simp)+

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

    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' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› ‹A⇩R' ♯* P› suppT have "(Ψ, R' ∥ P', R' ∥ (T ∥ !P)) ∈ Rel"
        by(rule_tac FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      hence "(Ψ, 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)
      hence "((Ψ ⊗ Ψ⇩R) ⊗ Ψ', Q', T ∥ !Q) ∈ Rel" by(rule cExt)
      with ‹Ψ⇩R ⊗ Ψ' ≃ Ψ⇩R'› have "(Ψ ⊗ Ψ⇩R', Q', T ∥ !Q) ∈ Rel"
        by(metis Associativity StatEq compositionSym) 
      with FrR' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› ‹A⇩R' ♯* Q'› ‹A⇩R' ♯* Q› suppT suppS have "(Ψ, R' ∥ Q', R' ∥ (T ∥ !Q)) ∈ Rel"
        by(rule_tac FrameParPres) (auto simp add: fresh_star_def fresh_def psi.supp)
      hence "(Ψ, 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' A⇩R Ψ⇩R K Q' A⇩Q)
    from ‹extractFrame (!Q) = ⟨A⇩Q, Ψ⇩Q⟩› have "A⇩Q = []" and "Ψ⇩Q = SBottom'" by simp+
    have RTrans: "Ψ ⊗ Ψ⇩Q ⊳ R ⟼M⦇ν*xvec⦈⟨N⟩ ≺ R'" and FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" by fact+
    then 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' ♯* Ψ"
                                and "A⇩R' ♯* N" and "A⇩R' ♯* R'" and "A⇩R' ♯* P" and "A⇩R' ♯* Q" and "(p ∙ xvec) ♯* Ψ"
                                and "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "xvec ♯* A⇩R'" and "(p ∙ xvec) ♯* A⇩R'"
                                and "distinctPerm p" and "(p ∙ xvec) ♯* R'" and "(p ∙ xvec) ♯* N" 
      using ‹distinct A⇩R› ‹A⇩R ♯* R› ‹A⇩R ♯* M› ‹A⇩R ♯* xvec› ‹A⇩R ♯* N› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* P› ‹A⇩R ♯* (!Q)›
            ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* (!Q)› ‹xvec ♯* R› ‹xvec ♯* M› ‹distinct xvec›
     by(rule_tac C="(Ψ, P, Q)" and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+

    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(rule_tac 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› ‹A⇩R ♯* Ψ› ‹A⇩R ♯* R› ‹A⇩R ♯* M› ‹A⇩R ♯* P›
      by(rule_tac Comm2) (assumption | simp)+

    moreover from ‹A⇩R' ♯* P› ‹A⇩R' ♯* Q› ‹A⇩R' ♯* N› S ‹xvec ♯* A⇩R'› ‹(p ∙ xvec) ♯* A⇩R'› PTrans QTrans ‹distinctPerm p› have "A⇩R' ♯* P'" and "A⇩R' ♯* Q'"
      apply -
      apply(drule_tac inputFreshChainDerivative, auto)
      apply(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, symmetric, of _ _ p], simp)
      by(force dest: inputFreshChainDerivative)+
    from ‹xvec ♯* P› ‹(p ∙ xvec) ♯* N› PTrans ‹distinctPerm p› have "(p ∙ xvec) ♯* (p ∙ P')"
      apply(drule_tac inputFreshChainDerivative, 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)     
      hence "((Ψ ⊗ (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' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› ‹A⇩R' ♯* P› ‹xvec ♯* A⇩R'› ‹(p ∙ xvec) ♯* A⇩R'› S ‹distinctPerm p› suppT
      have "(Ψ, R' ∥ (p ∙ P'), R' ∥ ((p ∙ T) ∥ !P)) ∈ Rel"
        apply(rule_tac FrameParPres)
        apply(assumption | simp add: freshChainSimps)+
        by(auto simp add: fresh_star_def fresh_def)
      hence "(Ψ, 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)
      hence "(Ψ, ⦇ν*(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)
      hence "(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)
      hence "((Ψ ⊗ (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' ‹A⇩R' ♯* Ψ› ‹A⇩R' ♯* P'› ‹A⇩R' ♯* Q'› ‹A⇩R' ♯* Q› suppT suppS ‹xvec ♯* A⇩R'› ‹(p ∙ xvec) ♯* A⇩R'› S ‹distinctPerm p› 
      have "(Ψ, R' ∥ Q', R' ∥ ((p ∙ T) ∥ !Q)) ∈ Rel"
        apply(rule_tac FrameParPres)
        apply(assumption | simp)+
        apply(simp add: freshChainSimps)
        by(auto simp add: fresh_star_def fresh_def)
      hence "(Ψ, 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
  qed
qed
unbundle relcomp_syntax
end

end