Theory Weak_Sim_Pres

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

context env begin

lemma weakInputPres:
  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(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from Ψ  M⦇λ*xvec N⦈.Q α  Q' show ?case
  proof(induct rule: inputCases)
    case(cInput K Tvec)
    from Ψ  M  K set xvec  supp N length xvec = length Tvec distinct xvec
    have "Ψ : (M⦇λ*xvec N⦈.Q)  M⦇λ*xvec N⦈.P K(N[xvec::=Tvec])  (P[xvec::=Tvec])"
      by(rule_tac weakInput) auto
    moreover have "Ψ  Ψ'  P[xvec::=Tvec] ^τ  P[xvec::=Tvec]" by simp
    moreover from length xvec = length Tvec have "(Ψ  Ψ',  P[xvec::=Tvec], Q[xvec::=Tvec])  Rel"
      by(rule PRelQ)
    ultimately show ?case by blast
  qed
next
  case(cTau Q')
  from Ψ  M⦇λ*xvec N⦈.Q τ  Q' have False by auto
  thus ?case by simp
qed

lemma weakOutputPres:
  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 "Ψ  MN⟩.P ↝<Rel> MN⟩.Q"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from Ψ  MN⟩.Q α  Q' show ?case
  proof(induct rule: outputCases)
    case(cOutput K)
    from Ψ  M  K 
    have "Ψ : (MN⟩.Q)  MN⟩.P KN  P" by(rule weakOutput) auto
    moreover have "Ψ  Ψ'  P ^τ  P" by simp
    moreover have "(Ψ  Ψ',  P, Q)  Rel" by(rule PRelQ)
    ultimately show ?case by blast
  qed
next
  case(cTau Q')
  from  Ψ  MN⟩.Q τ  Q' have False by auto
  thus ?case by simp
qed

lemma resTauCases[consumes 3, case_names cRes]:
  fixes Ψ    :: 'b
  and   x    :: name
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   C    :: "'d::fs_name"

  assumes Trans: "Ψ  ⦇νxP τ  P'"
  and     "x  Ψ"
  and     "x  P'"
  and     rScope:  "P'. Ψ  P τ  P'  Prop (⦇νxP')"

  shows "Prop P'"
proof -
  note Trans x  Ψ
  moreover have "x  (τ)" by simp
  moreover note x  P'
  moreover have "bn(τ) ♯* Ψ" and "bn(τ) ♯* P" and "bn(τ) ♯* subject(τ)" and "bn(τ) = []" by simp+
  ultimately show ?thesis
    by(induct rule: resCases) (auto intro: rScope)
qed

lemma weakResPres:
  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  Ψ'  (Ψ', ⦇νyR, ⦇νyS)  Rel'"

  shows   "Ψ  ⦇νxP ↝<Rel'> ⦇νxQ"
proof -
  note eqvt Rel' x  Ψ
  moreover have "x  ⦇νxP" and "x  ⦇νxQ" by(simp add: abs_fresh)+ 
  ultimately show ?thesis
  proof(induct rule: weakSimIFresh[of _ _ _ _ _ "()"])
    case(cAct α Q' Ψ')
    from bn α ♯* ⦇νxP bn α ♯* ⦇νxQ x  α have "bn α ♯* P" and "bn α ♯* Q" by simp+
    from Ψ  ⦇νxQ α  Q' x  Ψ x  α x  Q' bn α ♯* Ψ bn α ♯* Q bn α ♯* subject α bn α ♯* P x  α
    show ?case
    proof(induct rule: resCases)
      case(cOpen M xvec1 xvec2 y N Q')
      from bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N) ♯* P have "xvec1 ♯* P" and "xvec2 ♯* P" and "y  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'' P' where PTrans: "Ψ : Q  P M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  P''"
                      and P''Chain: "Ψ  ([(x, y)]  Ψ')  P'' ^τ P'" and P'RelQ': "(Ψ  ([(x, y)]  Ψ'), P', ([(x, y)]  Q'))  Rel"
        by (fastforce dest: weakSimE)
      from PTrans have "([(x, y)]  Ψ) : ([(x, y)]  Q)  ([(x, y)]  P) ([(x, y)]  (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)))  ([(x, y)]  P'')"
        by(rule eqvts)
      with x  Ψ y  Ψ x  M y  M x  xvec1 y  xvec1 x  xvec2 y  xvec2
      have "Ψ : ([(x, y)]  Q)  ([(x, y)]  P) M⦇ν*(xvec1@xvec2)⦈⟨N  ([(x, y)]  P'')"
        by(simp add: eqvts)
      hence "Ψ : ⦇νy([(x, y)]  Q)  ⦇νy([(x, y)]  P) M⦇ν*(xvec1@y#xvec2)⦈⟨N  ([(x, y)]  P'')"
        using y  supp N y  Ψ y  M y  xvec1 y  xvec2
        by(rule weakOpen)
      with y  P y  Q have "Ψ : ⦇νxQ  ⦇νxP M⦇ν*(xvec1@y#xvec2)⦈⟨N  ([(x, y)]  P'')"
        by(simp add: alphaRes)
      moreover from P''Chain have "([(x, y)]  (Ψ  ([(x, y)]  Ψ')))  ([(x, y)]  P'') ^τ ([(x, y)]  P')"
        by(rule eqvts)
      with x  Ψ y  Ψ have "Ψ  Ψ'  ([(x, y)]  P'') ^τ ([(x, y)]  P')" by(simp add: eqvts)
      moreover from P'RelQ' Rel  Rel' have "(Ψ  ([(x, y)]  Ψ'), P', ([(x, y)]  Q'))  Rel'" by auto
      with eqvt Rel' have "([(x, y)]  (Ψ  ([(x, y)]  Ψ'), P', ([(x, y)]  Q')))  Rel'" by(rule eqvtI)
      with x  Ψ y  Ψ have " (Ψ  Ψ', [(x, y)]  P', Q')  Rel'" by(simp add: eqvts)
      ultimately show ?case by blast
    next
      case(cRes Q')
      from PSimQ Ψ  Q α  Q' bn α ♯* Ψ bn α ♯* P α  τ
      obtain P'' P' where PTrans: "Ψ : Q  P α  P''"
                      and P''Chain: "Ψ  Ψ'  P'' ^τ P'" and P'RelQ': "(Ψ  Ψ', P', Q')  Rel"
        by(blast dest: weakSimE)
      from PTrans x  Ψ x  α  have "Ψ : ⦇νxQ  ⦇νxP α  ⦇νxP''"
        by(rule_tac weakScope)
      moreover from P''Chain  x  Ψ x  Ψ' have "Ψ  Ψ'  ⦇νxP'' ^τ ⦇νxP'"
        by(rule_tac tauChainResPres) auto
      moreover from P'RelQ' x  Ψ x  Ψ' have "(Ψ  Ψ', ⦇νxP', ⦇νxQ')  Rel'" 
        apply(rule_tac C1) by(auto simp add: fresh_left calc_atm)
      ultimately show ?case by blast
    qed
  next
    case(cTau Q')
    from Ψ  ⦇νxQ τ  Q' x  Ψ x  Q'
    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: weakSimE)
      from PChain x  Ψ have "Ψ  ⦇νxP ^τ ⦇νxP'" by(rule tauChainResPres)
      moreover from P'RelQ' x  Ψ have "(Ψ, ⦇νxP', ⦇νxQ')  Rel'" by(rule C1)
      ultimately show ?case by blast
    qed
  qed
qed

lemma weakResChainPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes PSimQ: "Ψ  P ↝<Rel> Q"
  and     "eqvt Rel"
  and     "xvec ♯* Ψ"
  and     C1:    "Ψ' R S yvec. (Ψ', R, S)  Rel; yvec ♯* Ψ'  (Ψ', ⦇ν*yvecR, ⦇ν*yvecS)  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 yvec="[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 weakResPres)
  thus ?case by simp
qed

lemma parTauCases[consumes 1, case_names cPar1 cPar2 cComm1 cComm2]:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"
  and   C :: "'d::fs_name"

  assumes Trans: "Ψ  P  Q τ  R"
  and     rPar1: "P' AQ ΨQ. Ψ  ΨQ  P τ  P';  extractFrame Q = AQ, ΨQ; distinct AQ;
                       AQ ♯* Ψ; AQ ♯* P; AQ ♯* Q; AQ ♯* C  Prop (P'  Q)"
  and     rPar2: "Q' AP ΨP. Ψ  ΨP  Q τ  Q'; extractFrame P = AP, ΨP; distinct AP;
                       AP ♯* Ψ; AP ♯* P;  AP ♯* Q; AP ♯* C  Prop (P  Q')"
  and     rComm1: "ΨQ M N P' AP ΨP K xvec Q' AQ.
           Ψ  ΨQ  P MN  P'; extractFrame P = AP, ΨP; distinct AP;
            Ψ  ΨP  Q K⦇ν*xvec⦈⟨N  Q'; extractFrame Q = AQ, ΨQ; distinct AQ;
            Ψ  ΨP  ΨQ  M  K; distinct xvec;
            AP ♯* Ψ;  AP ♯* ΨQ;  AP ♯* P;  AP ♯* M;  AP ♯* N;  AP ♯* P';  AP ♯* Q;  AP ♯* xvec;  AP ♯* Q'; AP ♯* AQ;  AP ♯* C; 
            AQ ♯* Ψ;  AQ ♯* ΨP; AQ ♯* P;  AQ ♯* K;  AQ ♯* N;  AQ ♯* P';  AQ ♯* Q;  AQ ♯* xvec;  AQ ♯* Q'; AQ ♯* C; 
            xvec ♯* Ψ;  xvec ♯* ΨP; xvec ♯* P;  xvec ♯* M;  xvec ♯* K; xvec ♯* Q;  xvec ♯* ΨQ;  xvec ♯* C 
            Prop (⦇ν*xvec(P'  Q'))"
  and     rComm2: "ΨQ M xvec N P' AP ΨP K Q' AQ.
           Ψ  ΨQ  P M⦇ν*xvec⦈⟨N  P'; extractFrame P = AP, ΨP; distinct AP;
            Ψ  ΨP  Q KN  Q'; extractFrame Q = AQ, ΨQ; distinct AQ;
            Ψ  ΨP  ΨQ  M  K; distinct xvec;
            AP ♯* Ψ;  AP ♯* ΨQ;  AP ♯* P;  AP ♯* M;  AP ♯* N;  AP ♯* P';  AP ♯* Q;  AP ♯* xvec;  AP ♯* Q'; AP ♯* AQ;  AP ♯* C; 
            AQ ♯* Ψ;  AQ ♯* ΨP; AQ ♯* P;  AQ ♯* K;  AQ ♯* N;  AQ ♯* P';  AQ ♯* Q;  AQ ♯* xvec;  AQ ♯* Q'; AQ ♯* C; 
            xvec ♯* Ψ;  xvec ♯* ΨP; xvec ♯* P;  xvec ♯* M;  xvec ♯* K;  xvec ♯* Q;  xvec ♯* ΨQ;  xvec ♯* C 
            Prop (⦇ν*xvec(P'  Q'))"

  shows "Prop R"
proof -
  from Trans obtain α where "Ψ  P  Q α  R" and "bn α ♯* Ψ" and "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* subject α" and "α = τ" by auto
  thus ?thesis using rPar1 rPar2 rComm1 rComm2
    by(induct rule: parCases[where C=C]) (auto simp add: residualInject)
qed

lemma weakParPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   Rel  :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"
  and   Rel' :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  
  assumes PRelQ: "AR ΨR. extractFrame R = AR, ΨR; AR ♯* Ψ; AR ♯* P; AR ♯* Q  (Ψ  ΨR, P, Q)  Rel" 
  and     Eqvt:  "eqvt Rel"
  and     Eqvt': "eqvt Rel'"

  and     Sim:    "Ψ' S T. (Ψ', S, T)  Rel  Ψ'  S ↝<Rel> T"
  and     Sym:    "Ψ' S T. (Ψ', S, T)  Rel  (Ψ', T, S)  Rel"
  and     Ext:    "Ψ' S T Ψ'. (Ψ', S, T)  Rel  (Ψ'  Ψ'', S, T)  Rel"
  and     StatImp: "Ψ' S T. (Ψ', S, T)  Rel  Ψ'  S ⪅<Rel> T"
  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 -
  from Eqvt' show ?thesis
  proof(induct rule: weakSimI[where C="()"])
    case(cAct Ψ' α QR)
    from bn α ♯* (P  R) bn α ♯* (Q  R)
    have "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* R"
      by simp+
    from Ψ  Q  R α  QR bn α ♯* Ψ bn α ♯* Q  bn α ♯* R bn α ♯* subject α α  τ show ?case
    proof(induct rule: parCases[where C="(P, R, Ψ')"])
      case(cPar1 Q' AR ΨR)
      from AR ♯* (P, R, Ψ') have "AR ♯* P" and "AR ♯* Ψ'" by simp+
      have FrR: "extractFrame R = AR, ΨR" by fact
      from AR ♯* α bn α ♯* R FrR
      have "bn α ♯* ΨR" by(drule_tac extractFrameFreshChain) auto
      have QTrans: "Ψ  ΨR  Q α  Q'" by fact
      from FrR AR ♯* Ψ AR ♯* P AR ♯* Q have "Ψ  ΨR  P ↝<Rel> Q"
        by(blast intro: PRelQ Sim)
      then obtain P'' P' where PTrans: "Ψ  ΨR : Q  P α  P''"
                           and P''Chain: "(Ψ  ΨR)  Ψ'  P'' ^τ P'" and P'RelQ': "((Ψ  ΨR)  Ψ', P', Q')  Rel"
        using QTrans bn α ♯* Ψ bn α ♯* ΨR bn α ♯* P bn α ♯* R AR ♯* α α  τ
        by(drule_tac Ψ'=Ψ' in weakSimE(1)) auto

      from PTrans QTrans AR ♯* P AR ♯* Q AR ♯* α bn α ♯* subject α distinct(bn α) 
      have "AR ♯* P''" and "AR ♯* Q'"
        by(fastforce dest: weakFreshChainDerivative freeFreshChainDerivative)+
      with P''Chain have "AR ♯* P'" by(force dest: tauChainFreshChain)
      
      from PTrans FrR bn α ♯* R AR ♯* Ψ AR ♯* P AR ♯* α AR ♯* Q 
      have "Ψ : Q  R  P  R α  (P''  R)"
        by(rule_tac weakPar1)
      moreover from P''Chain have "(Ψ  Ψ')  ΨR  P'' ^τ P'" 
        by(metis tauChainStatEq Associativity Commutativity Composition)
      with FrR have "Ψ  Ψ'  P''  R ^τ P'  R" using AR ♯* Ψ AR ♯* Ψ' AR ♯* P''
        by(rule_tac tauChainPar1) auto
      
      moreover from P'RelQ' have "((Ψ  Ψ')  ΨR, P', Q')  Rel" 
        by(metis C3 compositionSym Associativity Commutativity)
      hence "(Ψ  Ψ', P'  R, Q'  R)  Rel'" using FrR AR ♯* Ψ AR ♯* Ψ' AR ♯* P' AR ♯* Q'
        by(rule_tac C1) auto
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ)
      from AQ ♯* (P, R, Ψ') have "AQ ♯* P" and "AQ ♯* R" and "AQ ♯* Ψ'" 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 ♯* α" 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

      from FrP FrQ bn α ♯* P bn α ♯* Q AP ♯* α AQ ♯* α
      have "bn α ♯* ΨP" and "bn α ♯* ΨQ"
        by(force dest: extractFrameFreshChain)+
      
      obtain AR ΨR where FrR: "extractFrame R = AR, ΨR" and "AR ♯* (Ψ, P, Q, AQ, AP, ΨQ, ΨP, α, R, Ψ')" 
                      and "distinct AR"
        by(rule freshFrame)
      then have "AR ♯* Ψ" and "AR ♯* P" and "AR ♯* Q" and "AR ♯* AQ" and  "AR ♯* AP" and  "AR ♯* ΨQ" and  "AR ♯* ΨP"
            and "AR ♯* α" and "AR ♯* R" and "AR ♯* Ψ'"
        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 AR ♯* α AR ♯* Ψ'
                 bn α ♯* Ψ bn α ♯* P bn α ♯* Q bn α ♯* R bn α ♯* subject α distinct(bn α)
      obtain p Ψ'' AR' ΨR' where S: "set p  set(bn α) × set(bn(p  α))" and "(p  ΨR)  Ψ''  ΨR'"
                              and FrR': "extractFrame R' = AR', ΨR'"
                              and "bn(p  α) ♯* Ψ" and "bn(p  α) ♯* P" and "bn(p  α) ♯* Q"
                              and "AR' ♯* Ψ" and "AR' ♯* P" and "AR' ♯* Q" and "AR' ♯* Ψ'" and "distinctPerm p"
        by(rule_tac C="(Ψ, Ψ', P, Q)" and C'="(Ψ, P, Q)" in expandFrame) (assumption | simp)+

      from FrR AR ♯* Ψ AR ♯* P AR ♯* Q
      have "(Ψ  ΨR, P, Q)  Rel" by(rule PRelQ)
      hence "(Ψ  ΨR, Q, P)  Rel" by(rule Sym)
      hence "Ψ  ΨR  Q ⪅<Rel> P" by(rule StatImp)
      then 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  Ψ'))  P' ^τ P''"
                          and P'RelQ: "((Ψ  ΨR)  ((p  Ψ'')  (p  Ψ')), Q, P'')  Rel"
        by(rule weakStatImpE)
      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" and "AP' ♯* α"
        by(rule_tac C="(Ψ, ΨR, ΨQ, AQ, R, AR, α)" in freshFrame) auto

      from PChain AR ♯* P AQ ♯* P bn α ♯* P have "AQ ♯* P'" and "AR ♯* P'" and "bn α ♯* 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 "insertAssertion (extractFrame(Q  R)) Ψ F insertAssertion(extractFrame(P'  R)) Ψ"
      proof -
        have "AQ, Ψ  ΨQ  ΨR F AQ, (Ψ  ΨR)  ΨQ"
          by(metis Associativity Composition Commutativity AssertionStatEqTrans AssertionStatEqSym frameNilStatEq frameResChainPres)
        moreover from QimpP' FrQ FrP' AQ ♯* ΨR AP' ♯* ΨR AP' ♯* Ψ AQ ♯* Ψ 
        have "AQ, (Ψ  ΨR)  ΨQ F AP', (Ψ  ΨR)  ΨP'" using freshCompChain by simp
        moreover have "AP', (Ψ  ΨR)  ΨP' F AP', Ψ  ΨP'  ΨR"
          by(metis Associativity Composition Commutativity AssertionStatEqTrans AssertionStatEqSym frameNilStatEq frameResChainPres)
        ultimately have "AQ, Ψ  ΨQ  ΨR F AP', Ψ  ΨP'  ΨR"
          by(rule FrameStatEqImpCompose)
        hence "(AR@AQ), Ψ  ΨQ  ΨR F (AR@AP'), Ψ  ΨP'  ΨR"
          by(force intro: frameImpResChainPres simp add: frameChainAppend)
        with FrQ FrR FrP' AR ♯* AQ AP' ♯* AR AQ ♯* ΨR AR ♯* ΨQ AR ♯* ΨP' AP' ♯* ΨR 
                          AP' ♯* Ψ AQ ♯* Ψ AR ♯* Ψ 
        show ?thesis
          by(simp add: frameChainAppend) (metis frameImpChainComm FrameStatImpTrans)
      qed
      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' ♯* α AQ ♯* α
                AP' ♯* AR AR ♯* AQ AR ♯* ΨP' AR ♯* ΨQ AR ♯* Ψ AR ♯* ΨP' AQ ♯* ΨP' FrR distinct AR
          by(force intro: transferFrame)
      qed
      hence "Ψ  P'  R α  (P'  R')" using FrP' bn α ♯* P' AP' ♯* Ψ AP' ♯* R AP' ♯* α AP' ♯* α
        by(rule_tac Par2)
      ultimately have "Ψ : (Q  R)  P  R α  (P'  R')"
        by(rule_tac weakTransitionI)
      moreover from PChain P'Chain bn α ♯* P' bn(p  α) ♯* P AR' ♯* P 
      have "bn α ♯* P''" and "bn(p  α) ♯* P'" and "bn(p  α) ♯* P''" and "AR' ♯* P'" and "AR' ♯* P''" 
        by(metis tauChainFreshChain)+
      from P'Chain have "(p  ((Ψ  ΨR)  (p  Ψ'')  (p  Ψ')))  (p  P') ^τ (p  P'')"
        by(rule eqvts)
      with bn α ♯* Ψ bn(p  α) ♯* Ψ bn α ♯* P' bn(p  α) ♯* P' bn α ♯* P'' bn(p  α) ♯* P''
            S distinctPerm p
      have "(Ψ  (p  ΨR))  Ψ''  Ψ'  P' ^τ P''"
        by(simp add: eqvts)
      hence "(Ψ  Ψ')  (p  ΨR)  Ψ''  P' ^τ P''" 
        by(rule tauChainStatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans)
      with (p  ΨR)  Ψ''  ΨR' have "(Ψ  Ψ')  ΨR'  P' ^τ P''" by(metis tauChainStatEq compositionSym)
      hence "Ψ  Ψ'  P'  R' ^τ P''  R'" using FrR' AR' ♯* Ψ AR' ♯* Ψ' AR' ♯* P' by(rule_tac tauChainPar1) auto
      moreover from P'RelQ have "((Ψ  ΨR)  (p  Ψ'')  (p  Ψ'), P'', Q)  Rel" by(rule Sym)
      with eqvt Rel have "(p  ((Ψ  ΨR)  (p  Ψ'')  (p  Ψ'), P'', Q))  Rel" by(rule eqvtI)
      with bn α ♯* Ψ bn(p  α) ♯* Ψ bn α ♯* P'' bn(p  α) ♯* P'' bn α ♯* Q bn(p  α) ♯* Q S distinctPerm p
      have "((Ψ  (p  ΨR))  Ψ''  Ψ', P'', Q)  Rel" by(simp add: eqvts)
      with (p  ΨR)  Ψ''  ΨR' have "((Ψ  Ψ')  ΨR', P'', Q)  Rel" 
        by(rule_tac C3, auto) (metis Associativity Commutativity Composition AssertionStatEqTrans)
      with FrR' AR' ♯* Ψ  AR' ♯* Ψ' AR' ♯* P'' AR' ♯* Q 
      have "(Ψ  Ψ', P''  R', Q  R')  Rel'" by(rule_tac C1) auto
      ultimately show ?case by blast
    next
      case cComm1
      from τ  τ have False by simp
      thus ?case by simp
    next
      case cComm2
      from τ  τ have False by simp
      thus ?case by simp
    qed
  next
    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(blast intro: PRelQ Sim)
      moreover have QTrans: "Ψ  ΨR  Q τ  Q'" by fact
      ultimately obtain P' where PChain: "Ψ  ΨR  P ^τ P'" and P'RelQ': "(Ψ  ΨR, P', Q')  Rel"
        by(force dest: weakSimE)
      from PChain QTrans AR ♯* P AR ♯* Q have "AR ♯* P'" and "AR ♯* Q'"
        by(force dest: freeFreshChainDerivative tauChainFreshChain)+
      from PChain FrR AR ♯* Ψ AR ♯* P have "Ψ  P  R ^τ (P'  R)"
        by(rule tauChainPar1)
      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)  Ψ', Q, P'')  Rel"
        by(metis StatImp PRelQ Sym weakStatImpE)
      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(rule tauChainStatEq) (metis Associativity)
      with ΨR  Ψ'  ΨR' have "Ψ  ΨR'  P' ^τ P''" by(metis tauChainStatEq compositionSym)
      hence "Ψ  P'  R' ^τ P''  R'" using FrR' AR' ♯* Ψ AR' ♯* P' by(rule_tac tauChainPar1)
      ultimately have "Ψ  P  R ^τ (P''  R')"
        by(fastforce dest: rtrancl_into_rtrancl)

      moreover from P'RelQ ΨR  Ψ'  ΨR' have "(Ψ  ΨR', P'', Q)  Rel" by(blast intro: C3 Associativity compositionSym Sym)
      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 AR ♯* N 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 xvec ♯* K distinct xvec AR ♯* N
      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)

      from FrR (p  AR) ♯* Ψ (p  AR) ♯* P (p  AR) ♯* Q
      have "Ψ  (p  ΨR)  P ↝<Rel> Q" by(force intro: Sim PRelQ)

      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(auto dest: weakInputFreshChainDerivative inputFreshChainDerivative)

      from PTrans FrQ RTrans FrR MeqK AQ ♯* Ψ AQ ♯* P AQ ♯* Q AQ ♯* R AQ ♯* (p  M) AQ ♯* (p  AR)
           (p  AR) ♯* Ψ (p  AR) ♯* P (p  AR) ♯* Q (p  AR) ♯* R (p  AR) ♯* K xvec ♯* P distinct AR
      have "Ψ  P  R τ ⦇ν*xvec(P''  R')" apply(rule_tac weakComm1)
        by(assumption | simp)+

      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 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) (assumption | simp)+

      from FrR AR ♯* Ψ AR ♯* P AR ♯* Q have "Ψ  ΨR  P ↝<Rel> Q" by(force intro: Sim PRelQ)

      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 have "AR' ♯* P''" using AR' ♯* xvec xvec ♯* M distinct 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 tauActTauChain) 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
qed
unbundle no relcomp_syntax
lemma weakSimBangPres:
  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 "(Ψ, P, Q)  Rel"
  and     "eqvt 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     ResPres: "Ψ' S T xvec. (Ψ', S, T)  Rel; xvec ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  Rel"
  and     ResPres': "Ψ' S T xvec. (Ψ', S, T)  Rel'; xvec ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  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     cSim: "Ψ' S T. (Ψ', S, T)  Rel  Ψ'  S ↝<Rel> T"
  and     cExt: "Ψ' S T Ψ''. (Ψ', S, T)  Rel  (Ψ'  Ψ'', S, T)  Rel"
  and     cExt': "Ψ' S T Ψ''. (Ψ', S, T)  Rel'  (Ψ'  Ψ'', S, T)  Rel'"
  and     cSym: "Ψ' S T. (Ψ', S, T)  Rel  (Ψ', T, S)  Rel"
  and     cSym': "Ψ' S T. (Ψ', S, T)  Rel'  (Ψ', T, S)  Rel'"

  and     ParPres: "Ψ' S T U. (Ψ', S, T)  Rel  (Ψ', S  U, T  U)  Rel"
  and     ParPres2: "Ψ' S T. (Ψ', S, T)  Rel  (Ψ', S  S, T  T)  Rel"
  and     ParPres': "Ψ' S T U. (Ψ', S, T)  Rel'  (Ψ', U  S, U  T)  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"
using eqvt Rel''
proof(induct rule: weakSimI[where C="()"])
  case(cAct Ψ' α 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, 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' bn α ♯* Ψ bn α ♯* P
    have "Ψ  R  !P α  (R'  !P)" by(rule_tac Par1) (assumption | simp)+
    hence "Ψ : R  !Q  R  !P α  R'  !P" by(rule_tac transitionWeakTransition) auto
    moreover have "Ψ  Ψ'  R'  !P ^τ R'  !P" by auto
    moreover from (Ψ, P, Q)  Rel have "(Ψ  Ψ', P, Q)  Rel" by(rule cExt)
    hence "(Ψ  Ψ', 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 ♯* Ψ'" and "AR ♯* R" by simp+
    have FrR: "extractFrame R = AR, ΨR" by fact
    with bn α ♯* R AR ♯* α have "bn α ♯* ΨR" by(auto dest: extractFrameFreshChain)
    
    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 bn α ♯* Q α  τ bn α ♯* subject α
    obtain T where QTrans: "Ψ  ΨR  Q α  T" and "(𝟭, Q', T  !Q)  Rel'" 
      by(blast dest: rBangActE)
    
    from (Ψ, P, Q)  Rel have "(Ψ  ΨR, P, Q)  Rel" by(rule cExt)
    with QTrans bn α ♯* Ψ bn α ♯* ΨR bn α ♯* P α  τ
    obtain P'' S where PTrans: "Ψ  ΨR : Q  P α  P''" 
                   and P''Chain: "(Ψ  ΨR)  Ψ'  P'' ^τ S"
                   and SRelT: "((Ψ  ΨR)  Ψ', S, T)  Rel"
      by(blast dest: cSim weakSimE)
    from PTrans have "(Ψ  ΨR)  𝟭 : Q  P α  P''"
      by(metis weakTransitionStatEq Identity AssertionStatEqSym)
    hence "Ψ  ΨR : Q  !P  P  !P α  P''  !P" using bn α ♯* P
      by(force intro: weakPar1) 
    hence "Ψ  ΨR : Q  !P  !P α  P''  !P" using guarded P
      by(rule weakBang)
    hence "Ψ : R  (Q  !P)  R  !P α  R  (P''  !P)" 
      using FrR bn α ♯* R AR ♯* Ψ AR ♯* QAR ♯* P AR ♯* α AR ♯* α
      by(rule_tac weakPar2) auto
    moreover have "insertAssertion (extractFrame(R  !Q)) Ψ F insertAssertion (extractFrame(R  (Q  !P))) Ψ"
    proof -
      have "insertAssertion (extractFrame(R  !P)) Ψ = AR, Ψ  ΨR  𝟭" using FrR AR ♯* Ψ
        by auto
      moreover from ΨQ  𝟭 have "AR, Ψ  ΨR  𝟭 F AR, Ψ  ΨR  ΨQ  𝟭"
        by(rule_tac frameResChainPres, auto) (metis Identity compositionSym AssertionStatEqTrans AssertionStatEqSym)
      moreover have "AR, Ψ  ΨR  ΨQ  𝟭 F ⦇ν*AQ(AR, Ψ  ΨR  ΨQ  𝟭)" using AQ ♯* Ψ AQ ♯* ΨQ AQ ♯* ΨR AQ ♯* AR freshCompChain
        by(subst frameResFreshChain[where xvec=AQ, THEN FrameStatEqSym]) auto
      moreover have "⦇ν*AQ(AR, Ψ  ΨR  ΨQ  𝟭) F ⦇ν*AR(AQ, Ψ  ΨR  ΨQ  𝟭)"
        by(rule frameResChainComm)
      moreover have "insertAssertion (extractFrame(R  (Q  !P))) Ψ = (AR@AQ), Ψ  ΨR  ΨQ  𝟭" 
        using FrR FrQ AR ♯* Ψ AQ ♯* Ψ AQ ♯* AR AQ ♯* ΨR  AR ♯* ΨQ  freshCompChain
        by auto
      ultimately have "insertAssertion (extractFrame(R  !P)) Ψ F insertAssertion (extractFrame(R  (Q  !P))) Ψ"
        by(auto simp add: frameChainAppend) (blast dest: FrameStatEqTrans)
      thus ?thesis by(simp add: FrameStatEq_def)
    qed
    ultimately have "Ψ : R  !Q  R  !P α  R  (P''  !P)" 
      by(rule weakTransitionFrameImp)

    moreover from PTrans AR ♯* P AR ♯* α bn α ♯* subject α distinct(bn α)
    have "AR ♯* P''" by(force dest: weakFreshChainDerivative)
    with P''Chain have "AR ♯* S" by(force dest: tauChainFreshChain)
    from Ψ  ΨR  Q α  T AR ♯* Q AR ♯* α bn α ♯* subject α distinct(bn α) have "AR ♯* T"
      by(force dest: freeFreshChainDerivative)

    from P''Chain have "((Ψ  Ψ')  ΨR)  𝟭  P'' ^τ S" 
      by(rule tauChainStatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym Identity)
    hence "(Ψ  Ψ')  ΨR  P''  !P ^τ S  !P"
      by(rule_tac tauChainPar1) auto
    hence "Ψ  Ψ'  R  (P''  !P) ^τ R  (S  !P)" using FrR AR ♯* Ψ AR ♯* Ψ' AR ♯* P'' AR ♯* P
      by(rule_tac tauChainPar2) auto
    moreover have "(Ψ  Ψ', R  (S  !P), R  Q')  Rel''"
    proof -
      from ((Ψ  ΨR)  Ψ', S, T)  Rel have "((Ψ  Ψ')  ΨR, S, T)  Rel"
        by(rule StatEq) (metis Associativity Commutativity Composition AssertionStatEqTrans AssertionStatEqSym)
      with FrR AR ♯* Ψ  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)
      moreover from (Ψ, P, Q)  Rel have "(Ψ  Ψ', P, Q)  Rel" by(rule cExt)
      hence "(Ψ  Ψ', (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(