(* 
   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