Theory Weak_Stat_Imp_Pres

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

context env begin

lemma weakStatImpInputPres:
  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: "⋀Ψ'. (Ψ ⊗ Ψ', M⦇λ*xvec N⦈.P, M⦇λ*xvec N⦈.Q) ∈ Rel"

  shows "Ψ ⊳ M⦇λ*xvec N⦈.P ⪅<Rel> M⦇λ*xvec N⦈.Q"
using assms
by(fastforce simp add: weakStatImp_def)

lemma weakStatImpOutputPres:
  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: "⋀Ψ'. (Ψ ⊗ Ψ', M⟨N⟩.P, M⟨N⟩.Q) ∈ Rel"

  shows "Ψ ⊳ M⟨N⟩.P ⪅<Rel> M⟨N⟩.Q"
using assms
by(fastforce simp add: weakStatImp_def)
(*
lemma weakStatImpCasePres:
  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 ∧ Eq P Q"
  and     Sim:   "⋀Ψ P Q. (Ψ, P, Q) ∈ Rel ⟹ Ψ ⊳ P ⪅<Rel> Q"
  and     EqRel: "⋀Ψ P Q. Eq P Q ⟹ (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ Cases CsP ⪅<Rel> Cases CsQ"
using assms
apply(auto simp add: weakStatImp_def)
apply(rule_tac x="Cases CsQ" in exI)
apply auto
apply(rule_tac x="Cases CsQ" in exI)
apply auto
apply blast
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from `bn α ♯* (Cases CsP)` have "bn α ♯* CsP" by auto
  from `Ψ ⊳ Cases CsQ ⟼α ≺ Q'`
  show ?case
  proof(induct rule: caseCases)
    case(cCase φ Q)
    from `(φ, Q) mem CsQ` obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq P Q"
      by(metis PRelQ)
    from `Eq P Q` have "Ψ ⊳ P ↝<Rel> Q" by(metis EqRel Sim)
    moreover note `Ψ ⊳ Q ⟼α ≺ Q'` `bn α ♯* Ψ`
    moreover from `bn α ♯* CsP` `(φ, P) mem CsP` have "bn α ♯* P" by(auto dest: memFreshChain)
    ultimately obtain P'' P' where PTrans: "Ψ : Q ⊳ P ⟹α ≺ P''"
                               and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ⟹⇧^⇩τ P'" and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
      using `α ≠ τ`
      by(blast dest: weakSimE)
    note PTrans `(φ, P) mem CsP` `Ψ ⊢ φ` `guarded P`
    moreover from `guarded Q` have "insertAssertion (extractFrame Q) Ψ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
      by(rule insertGuardedAssertion)
    hence "insertAssertion (extractFrame(Cases CsQ)) Ψ ↪⇩F insertAssertion (extractFrame Q) Ψ"
      by(auto simp add: FrameStatEq_def)
    moreover from Identity have "insertAssertion (extractFrame(Cases CsQ)) Ψ ↪⇩F ⟨ε, Ψ⟩"
      by(auto simp add: AssertionStatEq_def)
    ultimately have "Ψ : (Cases CsQ) ⊳ Cases CsP ⟹α ≺ P''"
      by(rule weakCase)
    with P''Chain P'RelQ' show ?case by blast
  qed
next
  case(cTau Q')
  from `Ψ ⊳ Cases CsQ ⟼τ ≺ Q'` show ?case
  proof(induct rule: caseCases)
    case(cCase φ Q)
    from `(φ, Q) mem CsQ` obtain P where "(φ, P) mem CsP" and "guarded P" and "Eq P Q"
      by(metis PRelQ)
    from `Eq P Q` `Ψ ⊳ Q ⟼τ ≺ Q'`
    obtain P' where PChain: "Ψ ⊳ P ⟹⇩τ P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
      by(blast dest: EqSim weakCongSimE)
    from PChain `(φ, P) mem CsP` `Ψ ⊢ φ` `guarded P` have "Ψ ⊳ Cases CsP ⟹⇩τ P'"
      by(rule tauStepChainCase)
    hence "Ψ ⊳ Cases CsP ⟹⇧^⇩τ P'" by(simp add: trancl_into_rtrancl)
    with P'RelQ' show ?case by blast
  qed
qed
*)
lemma weakStatImpResPres:
  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     C1: "⋀Ψ' R S y. ⟦(Ψ', R, S) ∈ Rel; y ♯ Ψ'⟧ ⟹ (Ψ', ⦇νy⦈R, ⦇νy⦈S) ∈ Rel'"

  shows   "Ψ ⊳ ⦇νx⦈P ⪅<Rel'> ⦇νx⦈Q"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  obtain y::name where "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ P" and "y ♯ Q" by(generate_fresh "name") auto
  from ‹eqvt Rel› ‹Ψ ⊳ P ⪅<Rel> Q›  have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P) ⪅<Rel> ([(x, y)] ∙ Q)" by(rule weakStatImpClosed)
  with ‹x ♯ Ψ› ‹y ♯ Ψ› have "Ψ ⊳ ([(x, y)] ∙ P) ⪅<Rel> ([(x, y)] ∙ Q)" by simp
  then obtain Q' Q'' where QChain: "Ψ ⊳ ([(x, y)] ∙ Q) ⟹⇧^⇩τ Q'"
                       and PimpQ': "insertAssertion (extractFrame ([(x, y)] ∙ P)) Ψ ↪⇩F insertAssertion (extractFrame Q') Ψ"
                       and Q'Chain: "Ψ ⊗ Ψ' ⊳ Q' ⟹⇧^⇩τ Q''" and "(Ψ ⊗ Ψ', ([(x, y)] ∙ P), Q'') ∈ Rel"
    by(rule weakStatImpE)
  from QChain ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈([(x, y)] ∙ Q) ⟹⇧^⇩τ ⦇νy⦈Q'" by(rule tauChainResPres)
  with ‹y ♯ Q› have "Ψ ⊳ ⦇νx⦈Q ⟹⇧^⇩τ ⦇νy⦈Q'" by(simp add: alphaRes)
  moreover from PimpQ' ‹y ♯ Ψ› have "insertAssertion (extractFrame(⦇νy⦈([(x, y)] ∙ P))) Ψ ↪⇩F insertAssertion (extractFrame(⦇νy⦈Q')) Ψ"
    by(force intro: frameImpResPres)
  with ‹y ♯ P› have "insertAssertion (extractFrame(⦇νx⦈P)) Ψ ↪⇩F insertAssertion (extractFrame(⦇νy⦈Q')) Ψ"
    by(simp add: alphaRes)
  moreover from Q'Chain ‹y ♯ Ψ› ‹y ♯ Ψ'› have "Ψ ⊗ Ψ' ⊳ ⦇νy⦈Q' ⟹⇧^⇩τ ⦇νy⦈Q''" by(rule_tac tauChainResPres) auto
  moreover from ‹(Ψ ⊗ Ψ', ([(x, y)] ∙ P), Q'') ∈ Rel› ‹y ♯ Ψ› ‹y ♯ Ψ'› have "(Ψ ⊗ Ψ', ⦇νy⦈([(x, y)] ∙ P), ⦇νy⦈Q'') ∈ Rel'" 
    by(blast intro: C1)
  with ‹y ♯ P› have "(Ψ ⊗ Ψ', ⦇νx⦈P, ⦇νy⦈Q'') ∈ Rel'" by(simp add: alphaRes)
  ultimately show ?case
    by blast
qed

lemma weakStatImpParPres:
  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 PStatImpQ: "⋀A⇩R Ψ⇩R. ⟦extractFrame R = ⟨A⇩R, Ψ⇩R⟩; A⇩R ♯* Ψ; A⇩R ♯* P; A⇩R ♯* Q⟧ ⟹ Ψ ⊗ Ψ⇩R ⊳ P ⪅<Rel> Q"
  and     "xvec ♯* Ψ"
  and     Eqvt:  "eqvt 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 yvec. ⟦(Ψ', S, T) ∈ Rel'; yvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*yvec⦈S, ⦇ν*yvec⦈T) ∈ Rel'"
  and     C3: "⋀Ψ' S T Ψ''. ⟦(Ψ', S, T) ∈ Rel; Ψ' ≃ Ψ''⟧ ⟹ (Ψ'', S, T) ∈ Rel"

  shows "Ψ ⊳ ⦇ν*xvec⦈(P ∥ R) ⪅<Rel'> ⦇ν*xvec⦈(Q ∥ R)"
proof(induct rule: weakStatImpI)
  case(cStatImp Ψ')
  obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* Ψ" and "A⇩R ♯* Ψ'" and "A⇩R ♯* P" and "A⇩R ♯* Q" and "A⇩R ♯* R" and "A⇩R ♯* xvec"
    by(rule_tac F="extractFrame R" and C="(xvec, Ψ, Ψ', P, Q, R, xvec)" in freshFrame) auto

  hence "Ψ ⊗ Ψ⇩R ⊳ P ⪅<Rel> Q" by(rule_tac PStatImpQ)
    
  obtain p::"name prm" where "(p ∙ xvec) ♯* P" and "(p ∙ xvec) ♯* Q" and "(p ∙ xvec) ♯* Ψ" and "(p ∙ xvec) ♯* Ψ'" and  "(p ∙ xvec) ♯* Ψ⇩R" 
                         and  "(p ∙ xvec) ♯* A⇩R" and "(p ∙ xvec) ♯* R" and "(p ∙ xvec) ♯* P"
                         and "distinctPerm p" and S: "set p ⊆ set xvec × set (p ∙ xvec)"
    by(rule_tac c="(P, Q, R, Ψ, Ψ', A⇩R, Ψ⇩R, P)" in name_list_avoiding) auto
    
  from FrR have "(p ∙ extractFrame R) = (p ∙ ⟨A⇩R, Ψ⇩R⟩)" by(rule pt_bij3)
  with ‹A⇩R ♯* xvec› ‹(p ∙ xvec) ♯* A⇩R› S have FrpR: "extractFrame(p ∙ R) = ⟨A⇩R, p ∙ Ψ⇩R⟩" by(simp add: eqvts)
  from ‹eqvt Rel› ‹Ψ ⊗ Ψ⇩R ⊳ P ⪅<Rel> Q› have "(p ∙ (Ψ ⊗ Ψ⇩R)) ⊳ (p ∙ P) ⪅<Rel> (p ∙ Q)" by(rule weakStatImpClosed)
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S have "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ (p ∙ P) ⪅<Rel> (p ∙ Q)" by(simp add: eqvts)
  then obtain Q' Q'' where QChain: "Ψ ⊗ (p ∙ Ψ⇩R) ⊳ (p ∙ Q) ⟹⇧^⇩τ Q'"
                       and PimpQ': "insertAssertion (extractFrame (p ∙ P)) (Ψ ⊗ (p ∙ Ψ⇩R)) ↪⇩F insertAssertion (extractFrame Q') (Ψ ⊗ (p ∙ Ψ⇩R))"
                       and Q'Chain: "(Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ' ⊳ Q' ⟹⇧^⇩τ Q''" and "((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ', (p ∙ P), Q'') ∈ Rel"
    by(rule weakStatImpE)
    
  from ‹A⇩R ♯* xvec› ‹(p ∙ xvec) ♯* A⇩R› ‹A⇩R ♯* Q› S have "A⇩R ♯* (p ∙ Q)" by(simp add: freshChainSimps)
  moreover from ‹(p ∙ xvec) ♯* Q› have "(p ∙ p ∙ xvec) ♯* (p ∙ Q)"
    by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  hence "xvec ♯* (p ∙ Q)" using ‹distinctPerm p› by simp
  ultimately have "A⇩R ♯* Q'" and "A⇩R ♯* Q''" and "xvec ♯* Q'" and "xvec ♯* Q''" using QChain Q'Chain
    by(metis tauChainFreshChain)+

  obtain A⇩P Ψ⇩P where FrP: "extractFrame(p ∙ P) = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" "A⇩P ♯* Ψ'" and "A⇩P ♯* A⇩R" and "A⇩P ♯* (p ∙ Ψ⇩R)"
    by(rule_tac C="(Ψ, Ψ', A⇩R, p ∙ Ψ⇩R)" in freshFrame) auto
  obtain A⇩Q' Ψ⇩Q' where FrQ': "extractFrame Q' = ⟨A⇩Q', Ψ⇩Q'⟩" and "A⇩Q' ♯* Ψ"and "A⇩Q' ♯* Ψ'" and "A⇩Q' ♯* A⇩R" and "A⇩Q' ♯* (p ∙ Ψ⇩R)"
    by(rule_tac C="(Ψ, Ψ', A⇩R, p ∙ Ψ⇩R)" in freshFrame) auto
  from ‹A⇩R ♯* xvec› ‹(p ∙ xvec) ♯* A⇩R› ‹A⇩R ♯* P› S have "A⇩R ♯* (p ∙ P)" by(simp add: freshChainSimps)
  with ‹A⇩R ♯* Q'› ‹A⇩P ♯* A⇩R› ‹A⇩Q' ♯* A⇩R› FrP FrQ' have "A⇩R ♯* Ψ⇩P" and  "A⇩R ♯* Ψ⇩Q'"
    by(force dest: extractFrameFreshChain)+

  from QChain FrpR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* (p ∙ Q)› have "Ψ ⊳ (p ∙ Q) ∥ (p ∙ R) ⟹⇧^⇩τ Q' ∥ (p ∙ R)" by(rule tauChainPar1)
  hence "(p ∙ Ψ) ⊳ (p ∙ ((p ∙ Q) ∥ (p ∙ R))) ⟹⇧^⇩τ p ∙ (Q' ∥ (p ∙ R))" by(rule eqvts)
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p› have "Ψ ⊳ Q ∥ R ⟹⇧^⇩τ (p ∙ Q') ∥ R" by(simp add: eqvts)
  hence "Ψ ⊳ ⦇ν*xvec⦈(Q ∥ R) ⟹⇧^⇩τ ⦇ν*xvec⦈((p ∙ Q') ∥ R)" using ‹xvec ♯* Ψ› by(rule tauChainResChainPres)
  moreover have "⟨(A⇩P@A⇩R), Ψ ⊗ Ψ⇩P ⊗ (p ∙ Ψ⇩R)⟩ ↪⇩F ⟨(A⇩Q'@A⇩R), Ψ ⊗ Ψ⇩Q' ⊗ (p ∙ Ψ⇩R)⟩"
  proof -
    have "⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ (p ∙ Ψ⇩R)⟩ ≃⇩F ⟨A⇩P, (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩P⟩"
      by(metis frameResChainPres frameNilStatEq Associativity Commutativity AssertionStatEqTrans Composition)
    moreover with FrP FrQ' PimpQ' ‹A⇩P ♯* Ψ› ‹A⇩P ♯* (p ∙ Ψ⇩R)› ‹A⇩Q' ♯* Ψ› ‹A⇩Q' ♯* (p ∙ Ψ⇩R)›
    have "⟨A⇩P, (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩P⟩ ↪⇩F ⟨A⇩Q', (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩Q'⟩"  using freshCompChain
      by simp
    moreover have "⟨A⇩Q', (Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ⇩Q'⟩ ≃⇩F ⟨A⇩Q', Ψ ⊗ Ψ⇩Q' ⊗ (p ∙ Ψ⇩R)⟩"
      by(metis frameResChainPres frameNilStatEq Associativity Commutativity AssertionStatEqTrans Composition)
    ultimately have "⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ (p ∙ Ψ⇩R)⟩ ↪⇩F ⟨A⇩Q', Ψ ⊗ Ψ⇩Q' ⊗ (p ∙ Ψ⇩R)⟩"
      by(rule FrameStatEqImpCompose)
    hence "⟨(A⇩R@A⇩P), Ψ ⊗ Ψ⇩P ⊗ (p ∙ Ψ⇩R)⟩ ↪⇩F ⟨(A⇩R@A⇩Q'), Ψ ⊗ Ψ⇩Q' ⊗ (p ∙ Ψ⇩R)⟩"
      by(drule_tac frameImpResChainPres) (simp add: frameChainAppend)
    thus ?thesis
      apply(simp add: frameChainAppend)
      by(metis frameImpChainComm FrameStatImpTrans)
  qed
  with FrP FrpR FrQ' ‹A⇩P ♯* A⇩R› ‹A⇩P ♯* (p ∙ Ψ⇩R)› ‹A⇩Q' ♯* A⇩R› ‹A⇩Q' ♯* (p ∙ Ψ⇩R)› ‹A⇩R ♯* Ψ⇩P› ‹A⇩R ♯* Ψ⇩Q'›
      ‹A⇩P ♯* Ψ› ‹A⇩Q' ♯* Ψ› ‹A⇩R ♯* Ψ›
  have "insertAssertion(extractFrame((p ∙ P) ∥ (p ∙ R))) Ψ ↪⇩F insertAssertion(extractFrame(Q' ∥ (p ∙ R))) Ψ"
    by simp
  hence "(p ∙ insertAssertion(extractFrame((p ∙ P) ∥ (p ∙ R))) Ψ) ↪⇩F (p ∙ insertAssertion(extractFrame(Q' ∥ (p ∙ R))) Ψ)"
    by(rule FrameStatImpClosed)
  with ‹xvec ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ› S ‹distinctPerm p›
  have "insertAssertion(extractFrame(P ∥ R)) Ψ ↪⇩F insertAssertion(extractFrame((p ∙ Q') ∥ R)) Ψ"
    by(simp add: eqvts)
  with ‹xvec ♯* Ψ› have "insertAssertion(extractFrame(⦇ν*xvec⦈(P ∥ R))) Ψ ↪⇩F insertAssertion(extractFrame(⦇ν*xvec⦈((p ∙ Q') ∥ R))) Ψ"
    by(force intro: frameImpResChainPres)
  moreover from Q'Chain have "(Ψ ⊗ Ψ') ⊗ (p ∙ Ψ⇩R) ⊳ Q' ⟹⇧^⇩τ Q''"
    by(rule tauChainStatEq) (metis Associativity AssertionStatEqTrans Commutativity Composition)
  hence "Ψ ⊗ Ψ' ⊳ Q' ∥ (p ∙ R) ⟹⇧^⇩τ Q'' ∥ (p ∙ R)" using FrpR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* Q'› ‹A⇩R ♯* xvec› ‹(p ∙ xvec) ♯* A⇩R› S
    by(force intro: tauChainPar1 simp add: freshChainSimps)
  hence "Ψ ⊗ Ψ' ⊳ ⦇ν*(p ∙ xvec)⦈(Q' ∥ (p ∙ R)) ⟹⇧^⇩τ ⦇ν*(p ∙ xvec)⦈(Q'' ∥ (p ∙ R))" using ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'›
    by(rule_tac tauChainResChainPres) auto
  hence "Ψ ⊗ Ψ' ⊳ ⦇ν*xvec⦈((p ∙ Q') ∥ R) ⟹⇧^⇩τ ⦇ν*xvec⦈((p ∙ Q'') ∥ R)" using ‹xvec ♯* Q'› ‹xvec ♯* Q''› ‹(p ∙ xvec) ♯* R› S ‹distinctPerm p›
    apply(subst resChainAlpha) apply(auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
    by(subst resChainAlpha[of _ xvec]) (auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  moreover from ‹((Ψ ⊗ (p ∙ Ψ⇩R)) ⊗ Ψ', (p ∙ P), Q'') ∈ Rel› have "((Ψ ⊗ Ψ') ⊗ (p ∙ Ψ⇩R), (p ∙ P),  Q'') ∈ Rel"
    by(rule C3) (metis Associativity AssertionStatEqTrans Commutativity Composition)
  hence "(Ψ ⊗ Ψ', (p ∙ P) ∥ (p ∙ R), Q'' ∥ (p ∙ R)) ∈ Rel'" 
    using FrpR ‹A⇩R ♯* Ψ› ‹A⇩R ♯* Ψ'› ‹A⇩R ♯* Q''› ‹A⇩R ♯* P› ‹A⇩R ♯* xvec› ‹(p ∙ xvec) ♯* A⇩R› S
    by(rule_tac C1) (auto simp add: freshChainSimps)
  hence "(Ψ ⊗ Ψ', ⦇ν*(p ∙ xvec)⦈((p ∙ P) ∥ (p ∙ R)), ⦇ν*(p ∙ xvec)⦈(Q'' ∥ (p ∙ R))) ∈ Rel'"  using ‹(p ∙ xvec) ♯* Ψ› ‹(p ∙ xvec) ♯* Ψ'›
    by(rule_tac C2) auto
  hence "(Ψ ⊗ Ψ', ⦇ν*xvec⦈(P ∥ R), ⦇ν*xvec⦈((p ∙ Q'') ∥ R)) ∈ Rel'" using ‹(p ∙ xvec) ♯* P› ‹xvec ♯* Q''› ‹(p ∙ xvec) ♯* R› S ‹distinctPerm p›
    apply(subst resChainAlpha[where p=p]) 
    apply simp
    apply simp
    apply(subst resChainAlpha[where xvec=xvec and p=p]) 
    by(auto simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
  ultimately show ?case 
    by blast
qed

end

end