Theory Weak_Cong_Sim_Pres

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

context env begin

lemma caseWeakSimPres:
  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"
  and     EqSim: "Ψ' P Q. Eq Ψ' P Q  Ψ'  P ↝«Rel» Q"

  shows "Ψ  Cases CsP ↝<Rel> Cases CsQ"
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 weakCongSimCasePres:
  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     EqSim: "Ψ' P Q. Eq Ψ' P Q  Ψ'  P ↝«Rel» Q"

  shows "Ψ  Cases CsP ↝«Rel» Cases CsQ"
proof(induct rule: weakCongSimI)
  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)
    with P'RelQ' show ?case by blast
  qed
qed

lemma weakCongSimResPres:
  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 x. (Ψ', R, S)  Rel; x  Ψ'  (Ψ', ⦇νxR, ⦇νxS)  Rel'"

  shows   "Ψ  ⦇νxP ↝«Rel'» ⦇νxQ"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from Ψ  ⦇νxQ τ  Q' have "x  Q'" by(auto dest: tauFreshDerivative simp add: abs_fresh) 
  with  Ψ  ⦇νxQ τ  Q' x  Ψ show ?case
  proof(induct rule: resTauCases)
    case(cRes Q')
    from PSimQ Ψ  Q τ  Q' obtain P' where PChain: "Ψ  P τ P'" and P'RelQ': "(Ψ, P', Q')  Rel" 
      by(blast dest: weakCongSimE)
    from PChain x  Ψ have "Ψ  ⦇νxP τ ⦇νxP'" by(rule tauStepChainResPres)
    moreover from P'RelQ' x  Ψ have "(Ψ, ⦇νxP', ⦇νxQ')  Rel'" by(rule C1)
    ultimately show ?case by blast
  qed
qed

lemma weakCongSimResChainPres:
  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 xvec. (Ψ', R, S)  Rel; xvec ♯* Ψ'  (Ψ', ⦇ν*xvecR, ⦇ν*xvecS)  Rel"

  shows   "Ψ  ⦇ν*xvecP ↝«Rel» ⦇ν*xvecQ"
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 ♯* Ψ  Ψ  ⦇ν*xvecP ↝«Rel» ⦇ν*xvecQ xvec ♯* Ψ
  have "Ψ  ⦇ν*xvecP ↝«Rel» ⦇ν*xvecQ" by simp
  moreover note eqvt Rel x  Ψ
  moreover have "Rel  Rel" by simp
  moreover have "Ψ P Q x. (Ψ, P, Q)  Rel; x  Ψ  (Ψ, ⦇ν*[x]P, ⦇ν*[x]Q)  Rel"
    by(rule_tac xvec="[x]" in C1) auto
  hence "Ψ P Q x. (Ψ, P, Q)  Rel; x  Ψ  (Ψ, ⦇νxP, ⦇νxQ)  Rel"
    by simp
  ultimately have "Ψ  ⦇νx(⦇ν*xvecP) ↝«Rel» ⦇νx(⦇ν*xvecQ)"
    by(rule weakCongSimResPres)
  thus ?case by simp
qed

lemma weakCongSimParPres:
  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 PSimQ: "Ψ'. Ψ'  P ↝«Rel» Q"
  and     PSimQ': "Ψ'. Ψ'  P ↝<Rel> Q"
  and     StatImp: "Ψ'. Ψ'  Q ⪅<Rel> P"

  and            "eqvt Rel"
  and            "eqvt Rel'"

  and     Sym:    "Ψ' S T. (Ψ', S, T)  Rel  (Ψ', T, S)  Rel"
  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 ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  Rel'"
  and     C3: "Ψ' S T Ψ''. (Ψ', S, T)  Rel; Ψ'  Ψ''  (Ψ'', S, T)  Rel"

  shows "Ψ  P  R ↝«Rel'» Q  R"
proof(induct rule: weakCongSimI)
  case(cTau QR)
  from Ψ  Q  R τ  QR show ?case
  proof(induct rule: parTauCases[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
    with AR ♯* Ψ AR ♯* P AR ♯* Q have "Ψ  ΨR  P ↝«Rel» Q"
      by(rule_tac PSimQ)
    moreover have QTrans: "Ψ  ΨR  Q τ  Q'" by fact
    ultimately obtain P' where PChain: "Ψ  ΨR  P τ P'" and P'RelQ': "(Ψ  ΨR, P', Q')  Rel"
      by(rule weakCongSimE)
    from PChain QTrans AR ♯* P AR ♯* Q have "AR ♯* P'" and "AR ♯* Q'"
      by(force dest: freeFreshChainDerivative tauStepChainFreshChain)+
    from PChain FrR AR ♯* Ψ AR ♯* P have "Ψ  P  R τ (P'  R)"
      by(rule tauStepChainPar1)
    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)
    hence "AP ♯* Ψ" and "AP ♯* AQ" and "AP ♯* ΨQ" and "AP ♯* R"
      by simp+
    
    have FrQ: "extractFrame Q = AQ, ΨQ" by fact
    from AQ ♯* P FrP AP ♯* AQ have "AQ ♯* ΨP"
      by(drule_tac extractFrameFreshChain) auto
      
    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 ♯* R"
      by simp+
    
    from AQ ♯* R  FrR AR ♯* AQ have "AQ ♯* ΨR" by(drule_tac extractFrameFreshChain) auto
    from AP ♯* R AR ♯* AP FrR  have "AP ♯* ΨR" by(drule_tac extractFrameFreshChain) auto
    
    moreover from Ψ  ΨQ  R τ  R' FrR distinct AR AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R
    obtain Ψ' AR' ΨR' where "ΨR  Ψ'  ΨR'" and FrR': "extractFrame R' = AR', ΨR'"
                         and "AR' ♯* Ψ" and "AR' ♯* P" and "AR' ♯* Q"
      by(rule_tac C="(Ψ, P, Q, R)" in expandTauFrame) (assumption | simp)+

    from FrR AR ♯* Ψ AR ♯* P AR ♯* Q
    obtain P' P'' where PChain: "Ψ  ΨR  P ^τ P'"
                    and QimpP': "insertAssertion(extractFrame Q) (Ψ  ΨR) F insertAssertion(extractFrame P') (Ψ  ΨR)"
                    and P'Chain: "(Ψ  ΨR)  Ψ'  P' ^τ P''"
                    and P'RelQ: "((Ψ  ΨR)  Ψ', P'', Q)  Rel"
      by(metis StatImp weakStatImp_def Sym)
    obtain AP' ΨP' where FrP': "extractFrame P' = AP', ΨP'" and "AP' ♯* Ψ" and "AP' ♯* ΨR" and "AP' ♯* ΨQ"
                      and "AP' ♯* AQ" and "AP' ♯* R" and "AP' ♯* AR"
      by(rule_tac C="(Ψ, ΨR, ΨQ, AQ, R, AR)" in freshFrame) auto

    from PChain P'Chain AR ♯* P AQ ♯* P AR' ♯* P have "AQ ♯* P'" and "AR ♯* P'" and "AR' ♯* P'" and "AR' ♯* P''"
      by(force intro: tauChainFreshChain)+
    from AR ♯* P' AP' ♯* AR AQ ♯* P' AP' ♯* AQ FrP' have "AQ ♯* ΨP'" and "AR ♯* ΨP'"
      by(force dest: extractFrameFreshChain)+
      
    from PChain FrR AR ♯* Ψ AR ♯* P have "Ψ  P  R ^τ P'  R" by(rule tauChainPar1)
    moreover have RTrans: "Ψ  ΨP'  R τ  R'"
    proof -
      have "Ψ  Ψ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 with FrP' FrQ QimpP' AP' ♯* Ψ AQ ♯* Ψ AP' ♯* ΨR AQ ♯* ΨR
        have "AQ, (Ψ  ΨR)  ΨQ F AP', (Ψ  ΨR)  ΨP'" using freshCompChain
          by simp
        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 show ?thesis
        using AP' ♯* Ψ AP' ♯* ΨQ AQ ♯* Ψ AQ ♯* ΨP' AP' ♯* R AQ ♯* R 
              AP' ♯* AR AR ♯* AQ AR ♯* ΨP' AR ♯* ΨQ AR ♯* Ψ AR ♯* ΨP' AQ ♯* ΨP' FrR distinct AR
        by(force intro: transferTauFrame)
    qed
    hence "Ψ  P'  R τ  (P'  R')" using FrP' AP' ♯* Ψ AP' ♯* R
      by(rule_tac Par2) auto
    moreover from P'Chain have "Ψ  ΨR  Ψ'  P' ^τ P''"
      by(metis tauChainStatEq Associativity)
    with ΨR  Ψ'  ΨR' have "Ψ  ΨR'  P' ^τ P''" 
      by(rule_tac tauChainStatEq, auto) (metis compositionSym)
    hence "Ψ  P'  R' ^τ P''  R'" using FrR' AR' ♯* Ψ AR' ♯* P' by(rule_tac tauChainPar1)
    ultimately have "Ψ  P  R τ (P''  R')"
      by(drule_tac tauActTauStepChain) auto
    
    moreover from P'RelQ Ψ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(rule_tac 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+
    
    have QTrans: "Ψ  ΨR  Q MN  Q'" and RTrans: "Ψ  ΨQ  R K⦇ν*xvec⦈⟨N  R'"
      and MeqK: "Ψ  ΨQ  ΨR  M K" by fact+

    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 ♯* R xvec ♯* R AR ♯* P xvec ♯* P
                     AQ ♯* AR AQ ♯* xvec AR ♯* K AR ♯* N xvec ♯* K distinct xvec
    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) ♯* AQ" and "AR' ♯* P" and "AR' ♯* N"
      by(rule_tac C="(Ψ, Q, ΨQ, K, R, P, AQ)"  and C'="(Ψ, Q, ΨQ, K, R, P, AQ)" in expandFrame) (assumption | 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 AQ ♯* xvec (p  xvec) ♯* AQ AQ ♯* M S have "AQ ♯* (p  M)" by(simp add: freshChainSimps)
    from AQ ♯* xvec (p  xvec) ♯* AQ AQ ♯* AR S have "AQ ♯* (p  AR)" 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  AR, ΨR" by simp
    with xvec ♯* R (p  xvec) ♯* R S have FrR: "extractFrame R = (p  AR), (p  ΨR)"
      by(simp add: eqvts)
    
    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)
    
    have "Ψ  (p  ΨR)  P ↝<Rel> Q" by(rule PSimQ')

    with QTrans obtain P' P'' where PTrans: "Ψ  (p  ΨR) : Q  P (p  M)N  P''"
                                and P''Chain: "(Ψ  (p  ΨR))  Ψ'  P'' ^τ P'"
                                and P'RelQ': "((Ψ  (p  ΨR))  Ψ', P', Q')  Rel"
      by(fastforce dest: weakSimE)
    from PTrans QTrans AR' ♯* P AR' ♯* Q AR' ♯* N have "AR' ♯* P''" and "AR' ♯* Q'"
      by(blast dest: weakInputFreshChainDerivative inputFreshChainDerivative)+

    from PTrans obtain P''' where PChain: "Ψ  (p  ΨR)  P ^τ P'''"
                              and QimpP''': "insertAssertion (extractFrame Q) (Ψ  (p  ΨR)) F insertAssertion (extractFrame P''') (Ψ  (p  ΨR))"
                              and P'''Trans: "Ψ  (p  ΨR)  P''' (p  M)N  P''"
      by(rule weakTransitionE)
    
    from PChain xvec ♯* P (p  AR) ♯* P AR' ♯* P have "xvec ♯* P'''" and "(p  AR) ♯* P'''" and "AR' ♯* P'''"
      by(force intro: tauChainFreshChain)+
    from P'''Trans AR' ♯* P''' AR' ♯* N have "AR' ♯* P''" by(force dest: inputFreshChainDerivative)
    
    obtain AP''' ΨP''' where FrP''': "extractFrame P''' = AP''', ΨP'''" and "AP''' ♯* (Ψ, AQ, ΨQ, p  AR, p  ΨR, p  M, N, K, R, P''', xvec)" and "distinct AP'''"
      by(rule freshFrame)
    hence "AP''' ♯* Ψ" and "AP''' ♯* AQ" and "AP''' ♯* ΨQ" and "AP''' ♯* (p  M)" and "AP''' ♯* R"
      and "AP''' ♯* N" and "AP''' ♯* K" and "AP''' ♯* (p  AR)" and "AP''' ♯* P'''" and "AP''' ♯* xvec" and "AP''' ♯* (p  ΨR)"
      by simp+

    have "AQ, (Ψ  ΨQ)  (p  ΨR) F AQ, (Ψ  (p  ΨR))  ΨQ" 
      by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
    moreover with QimpP''' FrP''' FrQ AP''' ♯* Ψ AQ ♯* Ψ AP''' ♯* (p  ΨR) AQ ♯* ΨR AQ ♯* xvec (p  xvec) ♯* AQ S
    have "AQ, (Ψ  (p  ΨR))  ΨQ F AP''', (Ψ  (p  ΨR))  ΨP'''" using freshCompChain
      by(simp add: freshChainSimps)
    moreover have "AP''', (Ψ  (p  ΨR))  ΨP''' F AP''', (Ψ  ΨP''')  (p  ΨR)"
      by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
    ultimately have QImpP''': "AQ, (Ψ  ΨQ)  (p  ΨR) F AP''', (Ψ  ΨP''')  (p  ΨR)"
      by(rule FrameStatEqImpCompose)
      
    from PChain FrR (p  AR) ♯* Ψ (p  AR) ♯* P have "Ψ  P  R ^τ P'''  R" by(rule tauChainPar1)
    moreover from RTrans FrR P'''Trans MeqK QImpP''' FrP''' FrQ distinct AP''' distinct AR AP''' ♯* (p  AR) AQ ♯* (p  AR)
      (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) 
    obtain K' where "Ψ  ΨP'''  R K'⦇ν*xvec⦈⟨N  R'" and "Ψ  ΨP'''  (p  ΨR)  (p  M)  K'" and "(p  AR) ♯* K'"
      by(rule_tac comm1Aux) (assumption | simp)+
    
    with P'''Trans 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' AP''' ♯* (p  AR)
      by(rule_tac Comm1)
    
    moreover from P''Chain AR' ♯* P'' have "AR' ♯* P'" by(rule tauChainFreshChain)
    from (p  ΨR)  Ψ'  ΨR' have "(Ψ  (p  ΨR))  Ψ'  Ψ  ΨR'"
      by(metis Associativity AssertionStatEqTrans AssertionStatEqSym compositionSym)
    with P''Chain have "Ψ  ΨR'  P'' ^τ P'" by(rule tauChainStatEq)
    hence "Ψ  P''  R' ^τ P'  R'" using FrR' AR' ♯* Ψ AR' ♯* P'' by(rule tauChainPar1)
    hence "Ψ  ⦇ν*xvec(P''  R') ^τ ⦇ν*xvec(P'  R')" using xvec ♯* Ψ by(rule tauChainResChainPres)
    ultimately have "Ψ  P  R τ ⦇ν*xvec(P'  R')"
      by(drule_tac tauActTauStepChain) auto
    moreover from P'RelQ' (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(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' 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+
    
    have QTrans: "Ψ  ΨR  Q M⦇ν*xvec⦈⟨N  Q'" and RTrans: "Ψ  ΨQ  R KN  R'"
     and MeqK: "Ψ  ΨQ  ΨR  M K" by fact+

    from RTrans FrR distinct AR AR ♯* Ψ AR ♯* R AR ♯* Q' AR ♯* N AR ♯* P AR ♯* xvec AR ♯* K
    obtain Ψ' AR' ΨR' where  ReqR': "ΨR  Ψ'  ΨR'" and FrR': "extractFrame R' = AR', ΨR'" 
                         and "AR' ♯* Ψ" and "AR' ♯* P" and "AR' ♯* Q'" and "AR' ♯* N" and "AR' ♯* xvec"
      by(rule_tac C="(Ψ, P, Q', N, xvec)" and C'="(Ψ, P, Q', N, xvec)" in expandFrame) auto
    
    have "Ψ  ΨR  P ↝<Rel> Q" by(rule PSimQ')
    
    with QTrans xvec ♯* Ψ xvec ♯* ΨR xvec ♯* P
    obtain P'' P' where PTrans: "Ψ  ΨR : Q  P M⦇ν*xvec⦈⟨N  P''"
                    and P''Chain: "(Ψ  ΨR)  Ψ'  P'' ^τ P'"
                    and P'RelQ': "((Ψ  ΨR)  Ψ', P', Q')  Rel"
      by(fastforce dest: weakSimE)

    from PTrans obtain P''' where PChain: "Ψ  ΨR  P ^τ P'''"
                              and QimpP''': "insertAssertion (extractFrame Q) (Ψ  ΨR) F insertAssertion (extractFrame P''') (Ψ  ΨR)"
                              and P'''Trans: "Ψ  ΨR  P''' M⦇ν*xvec⦈⟨N  P''"
      by(rule weakTransitionE)
      
    from PChain AR ♯* P have "AR ♯* P'''" by(rule tauChainFreshChain)

    obtain AP''' ΨP''' where FrP''': "extractFrame P''' = AP''', ΨP'''" and "AP''' ♯* (Ψ, AQ, ΨQ, AR, ΨR, M, N, K, R, P''', xvec)" and "distinct AP'''"
      by(rule freshFrame)
    hence "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" and "AP''' ♯* ΨR"
      by simp+

    have "AQ, (Ψ  ΨQ)  ΨR F AQ, (Ψ  ΨR)  ΨQ" 
      by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
    moreover with QimpP''' FrP''' FrQ AP''' ♯* Ψ AQ ♯* Ψ AP''' ♯* ΨR AQ ♯* ΨR
    have "AQ, (Ψ  ΨR)  ΨQ F AP''', (Ψ  ΨR)  ΨP'''" using freshCompChain
      by simp
    moreover have "AP''', (Ψ  ΨR)  ΨP''' F AP''', (Ψ  ΨP''')  ΨR"
      by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
    ultimately have QImpP''': "AQ, (Ψ  ΨQ)  ΨR F AP''', (Ψ  ΨP''')  ΨR"
      by(rule FrameStatEqImpCompose)

    from PChain FrR AR ♯* Ψ AR ♯* P have "Ψ  P  R ^τ P'''  R" by(rule tauChainPar1)
    moreover from RTrans FrR P'''Trans MeqK QImpP''' FrP''' FrQ distinct AP''' distinct AR AP''' ♯* AR AQ ♯* AR
      AR ♯* Ψ AR ♯* P''' AR ♯* Q AR ♯* R AR ♯* K AP''' ♯* Ψ AP''' ♯* R
      AP''' ♯* P''' AP''' ♯* M AQ ♯* R  AQ ♯* M AR ♯* xvec xvec ♯* M
    obtain K' where "Ψ  ΨP'''  R K'N  R'" and "Ψ  ΨP'''  ΨR  M  K'" and "AR ♯* K'"
      by(rule_tac comm2Aux) (assumption | simp)+
    
    with P'''Trans FrP''' have "Ψ  P'''  R τ  ⦇ν*xvec(P''  R')" using FrR AR ♯* Ψ AR ♯* P''' AR ♯* R
      xvec ♯* R AP''' ♯* Ψ AP''' ♯* P''' AP''' ♯* R AP''' ♯* M AR ♯* K' AP''' ♯* AR
      by(rule_tac Comm2)
    moreover from P'''Trans AR ♯* P''' AR ♯* xvec xvec ♯* M distinct xvec have "AR ♯* P''"
      by(rule_tac outputFreshChainDerivative) auto

    from PChain AR' ♯* P have "AR' ♯* P'''" by(rule tauChainFreshChain)
    with P'''Trans xvec ♯* M distinct xvec have "AR' ♯* P''" using AR' ♯* xvec
      by(rule_tac outputFreshChainDerivative) auto
    
    with P''Chain have "AR' ♯* P'" by(rule tauChainFreshChain)
    from ΨR  Ψ'  ΨR' have "(Ψ  ΨR)  Ψ'  Ψ  ΨR'"
      by(metis Associativity AssertionStatEqTrans AssertionStatEqSym compositionSym)
    with P''Chain have "Ψ  ΨR'  P'' ^τ P'" by(rule tauChainStatEq)
    hence "Ψ  P''  R' ^τ P'  R'" using FrR' AR' ♯* Ψ AR' ♯* P'' 
      by(rule tauChainPar1)
    hence "Ψ  ⦇ν*xvec(P''  R') ^τ ⦇ν*xvec(P'  R')" 
      using xvec ♯* Ψ by(rule tauChainResChainPres)
    ultimately have "Ψ  P  R τ ⦇ν*xvec(P'  R')" by(drule_tac tauActTauStepChain) auto
    moreover from P'RelQ' Ψ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(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 weakCongSimBangPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('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"
  and   Rel'' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes PEqQ:   "Eq P Q"
  and     PRelQ: "(Ψ, P, Q)  Rel"
  and     "guarded P"
  and     "guarded Q"
  and     Rel'Rel: "Rel'  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     C1: "Ψ' S T U. (Ψ', S, T)  Rel; guarded S; guarded T  (Ψ', U  !S, U  !T)  Rel''"
  and     Closed: "Ψ' S T p. (Ψ', S, T)  Rel  ((p::name prm)  Ψ', p  S, p  T)  Rel"
  and     Closed': "Ψ' S T p. (Ψ', S, T)  Rel'  ((p::name prm)  Ψ', p  S, p  T)  Rel'"
  and     StatEq: "Ψ' S T Ψ''. (Ψ', S, T)  Rel; Ψ'  Ψ''  (Ψ'', S, T)  Rel"
  and     StatEq': "Ψ' S T Ψ''. (Ψ', S, T)  Rel'; Ψ'  Ψ''  (Ψ'', S, T)  Rel'"
  and     Trans: "Ψ' S T U. (Ψ', S, T)  Rel; (Ψ', T, U)  Rel  (Ψ', S, U)  Rel"
  and     Trans': "Ψ' S T U. (Ψ', S, T)  Rel'; (Ψ', T, U)  Rel'  (Ψ', S, U)  Rel'"
  and     EqSim: "Ψ' S T. Eq S T  Ψ'  S ↝«Rel» T"
  and     cSim: "Ψ' S T. (Ψ', S, T)  Rel  Ψ'  S ↝<Rel> T"
  and     cSym: "Ψ' S T. (Ψ', S, T)  Rel  (Ψ', T, S)  Rel"
  and     cSym': "Ψ' S T. (Ψ', S, T)  Rel'  (Ψ', T, S)  Rel'"
  and     cExt: "Ψ' S T Ψ''. (Ψ', S, T)  Rel  (Ψ'  Ψ'', S, T)  Rel"
  and     cExt': "Ψ' S T Ψ''. (Ψ', S, T)  Rel'  (Ψ'  Ψ'', S, T)  Rel'"
  and     ParPres: "Ψ' S T U. (Ψ', S, T)  Rel  (Ψ', S  U, T  U)  Rel"
  and     ParPres': "Ψ' S T U. (Ψ', S, T)  Rel'  (Ψ', U  S, U  T)  Rel'"
  and     ParPres2: "Ψ' S T. Eq S T  Eq (S  S) (T  T)"
  and     ResPres: "Ψ' S T xvec. (Ψ', S, T)  Rel; xvec ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  Rel"
  and     ResPres': "Ψ' S T xvec. (Ψ', S, T)  Rel'; xvec ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  Rel'"
  and     Assoc: "Ψ' S T U. (Ψ', S  (T  U), (S  T)  U)  Rel"
  and     Assoc': "Ψ' S T U. (Ψ', S  (T  U), (S  T)  U)  Rel'"
  and     ScopeExt: "xvec Ψ' T S. xvec ♯* Ψ'; xvec ♯* T  (Ψ', ⦇ν*xvec(S  T), (⦇ν*xvecS)  T)  Rel"
  and     ScopeExt': "xvec Ψ' T S. xvec ♯* Ψ'; xvec ♯* T  (Ψ', ⦇ν*xvec(S  T), (⦇ν*xvecS)  T)  Rel'"
  and     Compose: "Ψ' S T U O. (Ψ', S, T)  Rel; (Ψ', T, U)  Rel''; (Ψ', U, O)  Rel'  (Ψ', S, O)  Rel''"
  and     rBangActE: "Ψ' S α S'. Ψ'  !S α  S'; guarded S; bn α ♯* S; α  τ; bn α ♯* subject α  T. Ψ'  S α  T  (𝟭, S', T  !S)  Rel'"
  and     rBangTauE: "Ψ' S S'. Ψ'  !S τ  S'; guarded S  T. Ψ'  S  S τ  T  (𝟭, S', T  !S)  Rel'"
  and     rBangTauI: "Ψ' S S'. Ψ'  S  S τ S'; guarded S  T. Ψ'  !S τ T  (Ψ', T, S'  !S)  Rel'"
  shows "Ψ  R  !P ↝«Rel''» R  !Q"
proof(induct rule: weakCongSimI)
  case(cTau RQ')
  from Ψ  R  !Q τ  RQ' show ?case
  proof(induct rule: parTauCases[where C="(P, Q, R)"])
    case(cPar1 R' AQ ΨQ)
    from extractFrame (!Q) = AQ, ΨQ have "AQ = []" and "ΨQ = SBottom'" by simp+
    with Ψ  ΨQ  R τ  R' ΨQ = SBottom'
    have "Ψ  R  !P τ  (R'  !P)" by(rule_tac Par1) (assumption | simp)+
    hence "Ψ  R  !P τ R'  !P" by auto
    moreover from (Ψ, P, Q)  Rel have "(Ψ, R'  !P, R'  !Q)  Rel''" using guarded P guarded Q 
      by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 Q' AR ΨR)
    from AR ♯* (P, Q, R) have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" by simp+
    have FrR: "extractFrame R = AR, ΨR" by fact
    
    obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "AQ ♯* ΨR" and "AQ ♯* AR"
      by(rule_tac C="(Ψ, ΨR, AR)" in freshFrame) auto
    from FrQ guarded Q have "ΨQ  𝟭" and "supp ΨQ = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "AR ♯* ΨQ" and "AQ ♯* ΨQ" by(auto simp add: fresh_star_def fresh_def)

    from Ψ  ΨR  !Q τ  Q' guarded Q 
    obtain T where QTrans: "Ψ  ΨR  Q  Q τ  T" and "(𝟭, Q', T  !Q)  Rel'" 
      by(blast dest: rBangTauE)
    
    from Eq P Q have "Eq (P  P) (Q  Q)" by(rule ParPres2)
    with QTrans 
    obtain S where PTrans: "Ψ  ΨR  P  P τ S" and SRelT: "(Ψ  ΨR, S, T)  Rel"
      by(blast dest: EqSim weakCongSimE)
    from PTrans guarded P obtain U where PChain: "Ψ  ΨR  !P τ U" and "(Ψ  ΨR, U, S  !P)  Rel'"
      by(blast dest: rBangTauI)
    from PChain AR ♯* P have "AR ♯* U" by(force dest: tauStepChainFreshChain)
    from Ψ  ΨR  !P τ U FrR AR ♯* Ψ AR ♯* P have "Ψ  R  !P τ R  U"
      by(rule_tac tauStepChainPar2) auto
    moreover from PTrans AR ♯* P have "AR ♯* S" by(force dest: tauStepChainFreshChain)
    from QTrans AR ♯* Q have "AR ♯* T" by(force dest: tauFreshChainDerivative)
    have "(Ψ, R  U, R  Q')  Rel''"
    proof -
      from (Ψ  ΨR, U, S  !P)  Rel' Rel'Rel have "(Ψ  ΨR, U, S  !P)  Rel"
        by auto
      hence "(Ψ, R  U, R  (S  !P))  Rel" using FrR AR ♯* Ψ AR ♯* U AR ♯* S AR ♯* P
        by(rule_tac FrameParPres) auto

      moreover from (Ψ  ΨR, S, T)  Rel FrR AR ♯* Ψ AR ♯* S AR ♯* T have "(Ψ, R  S, R  T)  Rel"
        by(rule_tac FrameParPres) auto
      hence "(Ψ, R  T, R  S)  Rel" by(rule cSym)
      hence "(Ψ, (R  T)  !P, (R  S)  !P)  Rel" by(rule ParPres)
      hence "(Ψ, (R  S)  !P, (R  T)  !P)  Rel" by(rule cSym)
      hence "(Ψ, R  (S  !P), (R  T)  !P)  Rel" by(metis Trans Assoc)
      ultimately have "(Ψ, R  U, (R  T)  !P)  Rel" by(rule Trans)
      moreover from (Ψ, P, Q)  Rel have "(Ψ, (R  T)  !P, (R  T)  !Q)  Rel''" using guarded P guarded Q by(rule C1)
      moreover from (𝟭, Q', T  !Q)  Rel' have "(𝟭  Ψ, Q', T  !Q)  Rel'" by(rule cExt')
      hence "(Ψ, Q', T  !Q)  Rel'" 
        by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
      hence "(Ψ, R  Q', R  (T  !Q))  Rel'" by(rule ParPres')
      hence "(Ψ, R  Q', (R  T)  !Q)  Rel'" by(metis Trans' Assoc')
      hence "(Ψ, (R  T)  !Q, R  Q')  Rel'" by(rule cSym')
      ultimately show ?thesis by(rule_tac Compose)
    qed
    ultimately show ?case by blast
  next
    case(cComm1 ΨQ M N R' AR ΨR K xvec Q' AQ)
    from AR ♯* (P, Q, R) have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" by simp+
    from xvec ♯* (P, Q, R) have "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* R" by simp+
    have FrQ: "extractFrame(!Q) = AQ, ΨQ" by fact
    have FrR: "extractFrame R = AR, ΨR" by fact
    from Ψ  ΨQ  R MN  R' FrR distinct AR AR ♯* R AR ♯* N AR ♯* xvec AR ♯* P AR ♯* Q AR ♯* Ψ AR ♯* M
    obtain AR' ΨR' Ψ' where FrR': "extractFrame R' = AR', ΨR'" and "ΨR  Ψ'  ΨR'" and "AR' ♯* xvec" and "AR' ♯* P" and "AR' ♯* Q" and "AR' ♯* Ψ"
      by(rule_tac C="(Ψ, xvec, P, Q)" and C'="(Ψ, xvec, P, Q)" in expandFrame) auto
    from (Ψ, P, Q)  Rel have "(Ψ  ΨR, P, Q)  Rel" by(rule cExt)
    moreover from Ψ  ΨR  !Q K⦇ν*xvec⦈⟨N  Q' guarded Q xvec ♯* Q xvec ♯* K
    obtain S where QTrans: "Ψ  ΨR  Q K⦇ν*xvec⦈⟨N  S" and "(𝟭, Q', S  !Q)  Rel'"
      by(fastforce dest: rBangActE)
    ultimately obtain P' T where PTrans: "Ψ  ΨR : Q  P K⦇ν*xvec⦈⟨N  P'" and P'Chain: "(Ψ  ΨR)  Ψ'  P' ^τ T" and "((Ψ  ΨR)  Ψ', T, S)  Rel"
      using xvec ♯* Ψ xvec ♯* ΨR xvec ♯* P
      by(fastforce dest: cSim weakSimE)

    from PTrans AR ♯* P AR ♯* xvec AR' ♯* P AR' ♯* xvec xvec ♯* K distinct xvec
    have "AR ♯* P'" and  "AR' ♯* P'"
      by(force dest: weakOutputFreshChainDerivative)+
    with P'Chain have "AR' ♯* T" by(force dest: tauChainFreshChain)+
    from QTrans AR' ♯* Q AR' ♯* xvec xvec ♯* K distinct xvec 
    have "AR' ♯* S" by(force dest: outputFreshChainDerivative)

    obtain AQ' ΨQ' where FrQ': "extractFrame Q = AQ', ΨQ'" and "AQ' ♯* Ψ" and "AQ' ♯* ΨR" and "AQ' ♯* AR" and "AQ' ♯* M" and "AQ' ♯* R" and "AQ' ♯* K"
      by(rule_tac C="(Ψ, ΨR, AR, K, M, R)" in freshFrame) auto
    from FrQ' guarded Q have "ΨQ'  𝟭" and "supp ΨQ' = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "AQ' ♯* ΨQ'" by(auto simp add: fresh_star_def fresh_def)

    from PTrans obtain P'' where PChain: "Ψ  ΨR  P ^τ P''"
                             and NilImpP'': "AQ', (Ψ  ΨR)  ΨQ' F insertAssertion (extractFrame P'') (Ψ  ΨR)"
                             and P''Trans: "Ψ  ΨR  P'' K⦇ν*xvec⦈⟨N  P'"
      using FrQ' AQ' ♯* Ψ AQ' ♯* ΨR freshCompChain
      by(drule_tac weakTransitionE) auto

    from PChain have "Ψ  R  !P τ ⦇ν*xvec(R'  (P'  !P))"
    proof(induct rule: tauChainCases)
      case TauBase
      from Ψ  ΨQ  R MN  R' FrQ have "Ψ  𝟭  R MN  R'" by simp
      moreover note FrR
      moreover from P''Trans P = P'' have "Ψ  ΨR  P K⦇ν*xvec⦈⟨N  P'" by simp
      hence "(Ψ  ΨR)  𝟭  P K⦇ν*xvec⦈⟨N  P'" by(rule statEqTransition) (metis Identity AssertionStatEqSym)
      hence "Ψ  ΨR  P  !P K⦇ν*xvec⦈⟨N  (P'  !P)" using xvec ♯* Ψ xvec ♯* ΨR xvec ♯* P
        by(force intro: Par1)
      hence "Ψ  ΨR  !P K⦇ν*xvec⦈⟨N  (P'  !P)" using guarded P by(rule Bang)
      moreover from Ψ  ΨR  ΨQ  M  K FrQ have "Ψ  ΨR  𝟭  M  K" by simp
      ultimately have "Ψ  R  !P τ  ⦇ν*xvec(R'  (P'  !P))" using AR ♯* Ψ AR ♯* R AR ♯* P AR ♯* M xvec ♯* R
        by(force intro: Comm1)
      thus ?case by(rule tauActTauStepChain)
    next
      case TauStep
      obtain AP'' ΨP'' where FrP'': "extractFrame P'' = AP'', ΨP''" and "AP'' ♯* Ψ" and "AP'' ♯* K" and "AP'' ♯* ΨR" and "AP'' ♯* R" and "AP'' ♯* P''" and "AP'' ♯* P"
                          and "AP'' ♯* AR" and "distinct AP''"
        by(rule_tac C="(Ψ, K, AR, ΨR, R, P'', P)" in freshFrame) auto
      from PChain AR ♯* P have "AR ♯* P''" by(drule_tac tauChainFreshChain) auto
      with FrP'' AP'' ♯* AR have "AR ♯* ΨP''" by(drule_tac extractFrameFreshChain) auto
      from Ψ  ΨR  P τ P'' have "(Ψ  ΨR)  𝟭  P τ P''" by(rule tauStepChainStatEq) (metis Identity AssertionStatEqSym)
      hence "Ψ  ΨR  P  !P τ P''  !P" by(rule_tac tauStepChainPar1) auto
      hence "Ψ  ΨR  !P τ P''  !P" using guarded P by(rule tauStepChainBang)
      hence  "Ψ  R  !P τ R  (P''  !P)" using FrR AR ♯* Ψ AR ♯* P
        by(rule_tac tauStepChainPar2) auto
      moreover have "Ψ  R  (P''  !P) τ  ⦇ν*xvec(R'  (P'  !P))"
      proof -
        from FrQ ΨQ'  𝟭 Ψ  ΨQ  R MN  R' have "Ψ  ΨQ'  R MN  R'"
          by simp (metis statEqTransition AssertionStatEqSym compositionSym)
        moreover from P''Trans have "(Ψ  ΨR)  𝟭  P'' K⦇ν*xvec⦈⟨N  P'"
          by(rule statEqTransition) (metis Identity AssertionStatEqSym)
        hence P''PTrans: "Ψ  ΨR  P''  !P K⦇ν*xvec⦈⟨N  (P'  !P)" using xvec ♯* P
          by(rule_tac Par1) auto
        moreover from FrP'' have FrP''P: "extractFrame(P''  !P) = AP'', ΨP''  𝟭"
          by auto
        moreover from FrQ ΨQ'  𝟭 Ψ  ΨR  ΨQ  M  K have "Ψ  ΨQ'  ΨR  M  K"
          by simp (metis statEqEnt Composition AssertionStatEqSym Commutativity)
        hence "Ψ  ΨQ'  ΨR  K  M" by(rule chanEqSym)
        moreover have "AQ', (Ψ  ΨQ')  ΨR F AP'', (Ψ  (ΨP''  𝟭))  ΨR"
        proof -
          have "AQ', (Ψ  ΨQ')  ΨR F AQ', (Ψ  ΨR)  ΨQ'"
            by(rule_tac frameResChainPres, simp)
              (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
          moreover from NilImpP'' FrQ FrP'' AP'' ♯* Ψ AP'' ♯* ΨR freshCompChain have "AQ', (Ψ  ΨR)  ΨQ' F AP'', (Ψ  ΨR)  ΨP''"
            by auto
          moreover have "AP'', (Ψ  ΨR)  ΨP'' F AP'', (Ψ  ΨP''  𝟭)  ΨR"
            by(rule frameResChainPres, simp) 
              (metis Identity AssertionStatEqSym Associativity Commutativity Composition AssertionStatEqTrans)
          ultimately show ?thesis by(rule FrameStatEqImpCompose)
        qed
        ultimately obtain M' where RTrans: "Ψ  ΨP''  𝟭  R M'N  R'" and "Ψ  (ΨP''  𝟭)  ΨR  K  M'" and "AR ♯* M'"
          using FrR FrQ' distinct AR distinct AP'' AP'' ♯* AR AR ♯* Ψ AR ♯* P'' AR ♯* Q AR ♯* R  AR ♯* M AQ' ♯* R AQ' ♯* K AQ' ♯* AR AR ♯* P AP'' ♯* P AR ♯* xvec
                     AP'' ♯* Ψ AP'' ♯* R  AP'' ♯* P'' AP'' ♯* K xvec ♯* K distinct xvec
          by(rule_tac AQ="AQ'" and Q="Q" in comm2Aux) (assumption | simp)+

        note RTrans FrR P''PTrans FrP''P
        moreover from Ψ  (ΨP''  𝟭)  ΨR  K  M' have "Ψ  (ΨP''  𝟭)  ΨR  M'  K" by(rule chanEqSym)
        hence "Ψ  ΨR  ΨP''  𝟭  M'  K" by(metis statEqEnt Composition AssertionStatEqSym Commutativity)
        ultimately show ?thesis using AR ♯* Ψ AR ♯* R AR ♯* P'' AR ♯* P AR ♯* M' AP'' ♯* AR AP'' ♯* Ψ AP'' ♯* R AP'' ♯* P'' AP'' ♯* P AP'' ♯* K xvec ♯* R
          by(rule_tac Comm1) (assumption | simp)+
      qed
      ultimately show ?thesis
        by(drule_tac tauActTauStepChain) auto
    qed

    moreover from P'Chain have "((Ψ  ΨR)  Ψ')  𝟭  P' ^τ T"
      by(rule tauChainStatEq) (metis Identity AssertionStatEqSym)
    hence "(Ψ  ΨR)  Ψ'  P'  !P ^τ T  !P"
      by(rule_tac tauChainPar1) auto
    hence "Ψ  ΨR  Ψ'  P'  !P ^τ T  !P"
      by(rule tauChainStatEq) (metis Associativity)
    hence "Ψ  ΨR'  P'  !P^τ T  !P" using ΨR  Ψ'  ΨR'
      by(rule_tac tauChainStatEq) (auto intro: compositionSym)
    hence "Ψ  R'  (P'  !P) ^τ R'  (T  !P)" using FrR' AR' ♯* Ψ AR' ♯* P AR' ♯* P'
      by(rule_tac tauChainPar2) auto
    hence "Ψ  ⦇ν*xvec(R'  (P'  !P)) ^τ ⦇ν*xvec(R'  (T  !P))" using xvec ♯* Ψ
      by(rule tauChainResChainPres)
    ultimately have "Ψ  R  !P τ ⦇ν*xvec(R'  (T  !P))"
      by auto
    moreover have "(Ψ, ⦇ν*xvec(R'  (T  !P)), ⦇ν*xvec(R'  Q'))  Rel''"
    proof -
      from ((Ψ  ΨR)  Ψ', T, S)  Rel have "(Ψ  ΨR  Ψ', T, S)  Rel"
        by(rule StatEq) (metis Associativity)
      hence "(Ψ  ΨR', T, S)  Rel" using ΨR  Ψ'  ΨR'
        by(rule_tac StatEq) (auto dest: compositionSym)

      with FrR' AR' ♯* Ψ AR' ♯* S AR' ♯* T have "(Ψ, R'  T, R'  S)  Rel"
        by(rule_tac FrameParPres) auto
      hence "(Ψ, (R'  T)  !P, (R'  S)  !P)  Rel" by(rule ParPres)
      hence "(Ψ, ⦇ν*xvec((R'  T)  !P), ⦇ν*xvec((R'  S)  !P))  Rel" using xvec ♯* Ψ
        by(rule ResPres)
      hence "(Ψ, ⦇ν*xvec(R'  T)  !P, (⦇ν*xvec(R'  S))  !P)  Rel" using xvec ♯* Ψ xvec ♯* P
        by(force intro: Trans ScopeExt)
      hence "(Ψ, ⦇ν*xvec(R'  (T  !P)), (⦇ν*xvec(R'  S))  !P)  Rel" using xvec ♯* Ψ
        by(force intro: Trans ResPres Assoc)

      moreover from (Ψ, P, Q)  Rel guarded P guarded Q have "(Ψ, (⦇ν*xvec(R'  S))  !P, (⦇ν*xvec(R'  S))  !Q)  Rel''"
        by(rule C1)
      moreover from (𝟭, Q', S  !Q)  Rel' have "(𝟭  Ψ, Q', S  !Q)  Rel'" by(rule cExt')
      hence "(Ψ, Q', S  !Q)  Rel'" 
        by(rule StatEq') (metis Identity AssertionStatEqSym Commutativity AssertionStatEqTrans)
      hence "(Ψ, R'  Q', R'  (S  !Q))  Rel'" by(rule ParPres')
      hence "(Ψ, R'  Q', (R'  S)  !Q)  Rel'" by(metis Trans' Assoc')
      hence "(Ψ, (R'  S)  !Q, R'  Q')  Rel'" by(rule cSym')
      hence "(Ψ, ⦇ν*xvec((R'  S)  !Q), ⦇ν*xvec(R'  Q'))  Rel'" using xvec ♯* Ψ
        by(rule ResPres')
      hence "(Ψ, (⦇ν*xvec(R'  S))  !Q, ⦇ν*xvec(R'  Q'))  Rel'" using xvec ♯* Ψ xvec ♯* Q
        by(force intro: Trans' ScopeExt'[THEN cSym'])
      ultimately show ?thesis by(rule_tac Compose)
    qed
    ultimately show ?case by blast
  next
    case(cComm2 ΨQ M xvec N R' AR ΨR K Q' AQ)
    from AR ♯* (P, Q, R) have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" by simp+
    from xvec ♯* (P, Q, R) have "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* R" by simp+
    have FrQ: "extractFrame(!Q) = AQ, ΨQ" by fact
    have FrR: "extractFrame R = AR, ΨR" by fact
    from Ψ  ΨQ  R M⦇ν*xvec⦈⟨N  R' FrR distinct AR AR ♯* R AR ♯* N AR ♯* xvec AR ♯* P AR ♯* Q AR ♯* Ψ xvec ♯* R xvec ♯* Ψ xvec ♯* P xvec ♯* Q xvec ♯* M distinct xvec AR ♯* M
    obtain p AR' ΨR' Ψ' where FrR': "extractFrame R' = AR', ΨR'" and "(p  ΨR)  Ψ'  ΨR'" and "AR' ♯* xvec" and "AR' ♯* P" and "AR' ♯* Q" and "AR' ♯* Ψ" and S: "set p  set xvec × set(p  xvec)" and "distinctPerm p" and "(p  xvec) ♯* N" and "(p  xvec) ♯* Q" and "(p  xvec) ♯* R'" and "(p  xvec) ♯* P" and "(p  xvec) ♯* Ψ" and "AR' ♯* N" and "AR' ♯* xvec" and "AR' ♯* (p  xvec)"
      by(rule_tac C="(Ψ, P, Q)"  and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+

    from Ψ  ΨQ  R M⦇ν*xvec⦈⟨N  R' S (p  xvec) ♯* N (p  xvec) ♯* R'
    have  RTrans: "Ψ  ΨQ  R M⦇ν*(p  xvec)⦈⟨(p  N)  (p  R')"
      by(simp add: boundOutputChainAlpha'' residualInject)
    from (Ψ, P, Q)  Rel have "(Ψ  ΨR, P, Q)  Rel" by(rule cExt)
    moreover from Ψ  ΨR  !Q KN  Q' S (p  xvec) ♯* Q xvec ♯* Q distinctPerm p
    have "Ψ  ΨR  !Q K(p  N)  (p  Q')" by(rule_tac inputAlpha) auto
    then obtain S where QTrans: "Ψ  ΨR  Q K(p  N)  S" and "(𝟭, (p  Q'), S  !Q)  Rel'" 
      using guarded Q
      by(fastforce dest: rBangActE)
    ultimately obtain P' T where PTrans: "Ψ  ΨR : Q  P K(p  N)  P'" 
                             and P'Chain: "(Ψ  ΨR)  (p  Ψ')  P' ^τ T" 
                             and "((Ψ  ΨR)  (p  Ψ'), T, S)  Rel"
      by(fastforce dest: cSim weakSimE)

    from AR' ♯* N AR' ♯* xvec AR' ♯* (p  xvec) S have "AR' ♯* (p  N)"
      by(simp add: freshChainSimps)
    with PTrans AR' ♯* P have "AR' ♯* P'" by(force dest: weakInputFreshChainDerivative)
    with P'Chain have "AR' ♯* T" by(force dest: tauChainFreshChain)+
    from QTrans AR' ♯* Q AR' ♯* (p  N) have "AR' ♯* S" by(force dest: inputFreshChainDerivative)

    obtain AQ' ΨQ' where FrQ': "extractFrame Q = AQ', ΨQ'" and "AQ' ♯* Ψ" and "AQ' ♯* ΨR" and "AQ' ♯* AR" and "AQ' ♯* M" and "AQ' ♯* R" and "AQ' ♯* K"
      by(rule_tac C="(Ψ, ΨR, AR, K, M, R)" in freshFrame) auto
    from FrQ' guarded Q have "ΨQ'  𝟭" and "supp ΨQ' = ({}::name set)" by(blast dest: guardedStatEq)+
    hence "AQ' ♯* ΨQ'" by(auto simp add: fresh_star_def fresh_def)

    from PTrans obtain P'' where PChain: "Ψ  ΨR  P ^τ P''"
                             and NilImpP'': "AQ', (Ψ  ΨR)  ΨQ' F insertAssertion (extractFrame P'') (Ψ  ΨR)"
                             and P''Trans: "Ψ  ΨR  P'' K(p  N)  P'"
      using FrQ' AQ' ♯* Ψ AQ' ♯* ΨR freshCompChain
      by(drule_tac weakTransitionE) auto

    from (p  xvec) ♯* P xvec ♯* P PChain have "(p  xvec) ♯* P''" and "xvec ♯* P''" 
      by(force dest: tauChainFreshChain)+
    from (p  xvec) ♯* N distinctPerm p have "xvec ♯* (p  N)"
      by(subst pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst, where pi=p, symmetric]) simp
    with P''Trans xvec ♯* P'' have "xvec ♯* P'" by(force dest: inputFreshChainDerivative)
    hence "(p  xvec) ♯* (p  P')" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])

    from PChain have "Ψ  R  !P τ ⦇ν*(p  xvec)((p  R')  (P'  !P))"
    proof(induct rule: tauChainCases)
      case TauBase
      from RTrans FrQ have "Ψ  𝟭  R M⦇ν*(p  xvec)⦈⟨(p  N)  (p  R')" by simp
      moreover note FrR
      moreover from P''Trans P = P'' have "Ψ  ΨR  P K(p  N) P'" by simp
      hence "(Ψ  ΨR)  𝟭  P K(p  N)  P'" 
        by(rule statEqTransition) (metis Identity AssertionStatEqSym)
      hence "Ψ  ΨR  P  !P K(p  N)  (P'  !P)" by(force intro: Par1)
      hence "Ψ  ΨR  !P K(p  N)  (P'  !P)" using guarded P by(rule Bang)
      moreover from Ψ  ΨR  ΨQ  M  K FrQ have "Ψ  ΨR  𝟭  M  K" by simp
      ultimately have "Ψ  R  !P τ  ⦇ν*(p  xvec)((p  R')  (P'  !P))" using AR ♯* Ψ AR ♯* R AR ♯* P AR ♯* M (p  xvec) ♯* P
        by(force intro: Comm2)
      thus ?case by(rule tauActTauStepChain)
    next
      case TauStep
      obtain AP'' ΨP'' where FrP'': "extractFrame P'' = AP'', ΨP''" and "AP'' ♯* Ψ" and "AP'' ♯* K" and "AP'' ♯* ΨR" and "AP'' ♯* R" and "AP'' ♯* P''" and "AP'' ♯* P"
                          and "AP'' ♯* AR" and "distinct AP''"
        by(rule_tac C="(Ψ, K, AR, ΨR, R, P'', P)" in freshFrame) auto
      from PChain AR ♯* P have "AR ♯* P''" by(drule_tac tauChainFreshChain) auto
      with FrP'' AP'' ♯* AR have "AR ♯* ΨP''" by(drule_tac extractFrameFreshChain) auto
      from Ψ  ΨR  P τ P'' have "(Ψ  ΨR)  𝟭  P τ P''" by(rule tauStepChainStatEq) (metis Identity AssertionStatEqSym)
      hence "Ψ  ΨR  P  !P τ P''  !P" by(rule_tac tauStepChainPar1) auto
      hence "Ψ  ΨR  !P τ P''  !P" using guarded P by(rule tauStepChainBang)
      hence  "Ψ  R  !P τ R  (P''  !P)" using FrR AR ♯* Ψ AR ♯* P
        by(rule_tac tauStepChainPar2) auto
      moreover have "Ψ  R  (P''  !P) τ  ⦇ν*(p  xvec)((p  R')  (P'  !P))"
      proof -
        from FrQ ΨQ'  𝟭 RTrans have "Ψ  ΨQ'  R M⦇ν*(p  xvec)⦈⟨(p  N)  (p  R')"
          by simp (metis statEqTransition AssertionStatEqSym compositionSym)
        moreover from P''Trans have "(Ψ  ΨR)  𝟭  P'' K(p  N)  P'"
          by(rule statEqTransition) (metis Identity AssertionStatEqSym)
        hence P''PTrans: "Ψ  ΨR  P''  !P K(p  N)  (P'  !P)"
          by(rule_tac Par1) auto
        moreover from FrP'' have FrP''P: "extractFrame(P''  !P) =