Theory Bisim_Struct_Cong

(* 
   Title: Psi-calculi   
   Author/Maintainer: Jesper Bengtson (jebe@itu.dk), 2012
*)
theory Bisim_Struct_Cong
  imports Bisim_Pres Sim_Struct_Cong Structural_Congruence
begin

context env begin

lemma bisimParComm:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  
  shows "Ψ  P  Q  Q  P"
proof -
  let ?X = "{((Ψ::'b), ⦇ν*xvec((P::('a, 'b, 'c) psi)  Q), ⦇ν*xvec(Q  P)) | xvec Ψ P Q. xvec ♯* Ψ}"
  
  have "eqvt ?X"
    by(force simp add: eqvt_def pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst] eqvts)

  have "(Ψ, P  Q, Q  P)  ?X"
    apply auto by(rule_tac x="[]" in exI) auto
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ PQ QP)
    from (Ψ, PQ, QP)  ?X
    obtain xvec P Q where PFrQ: "PQ = ⦇ν*xvec(P  Q)" and QFrP: "QP = ⦇ν*xvec(Q  P)" and "xvec ♯* Ψ"
      by auto

    obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" and "AP ♯* Q"
      by(rule_tac C="(Ψ, Q)" in freshFrame) auto
    obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "AQ ♯* AP" and "AQ ♯* ΨP"
      by(rule_tac C="(Ψ, AP, ΨP)" in freshFrame) auto
    from FrQ AQ ♯* AP AP ♯* Q have "AP ♯* ΨQ" by(force dest: extractFrameFreshChain)
    have "(xvec@AP@AQ), Ψ  ΨP  ΨQ F (xvec@AQ@AP), Ψ  ΨQ  ΨP"
      by(simp add: frameChainAppend)
        (metis frameResChainPres frameResChainComm frameNilStatEq compositionSym Associativity Commutativity FrameStatEqTrans)
    with FrP FrQ PFrQ QFrP AP ♯* ΨQ AQ ♯* ΨP AQ ♯* AP xvec ♯* Ψ AP ♯* Ψ AQ ♯* Ψ
    show ?case by(auto simp add: frameChainAppend)
  next
    case(cSim Ψ PQ QP)
    from (Ψ, PQ, QP)  ?X    
    obtain xvec P Q where PFrQ: "PQ = ⦇ν*xvec(P  Q)" and QFrP: "QP = ⦇ν*xvec(Q  P)"
                      and "xvec ♯* Ψ"
      by auto
    moreover have "Ψ  ⦇ν*xvec(P  Q) ↝[?X] ⦇ν*xvec(Q  P)"
    proof -
      have "Ψ  P  Q ↝[?X] Q  P"
      proof -
        note eqvt ?X
        moreover have "Ψ P Q. (Ψ, P  Q, Q  P)  ?X"
          apply auto by(rule_tac x="[]" in exI) auto
        moreover have "Ψ P Q xvec. (Ψ, P, Q)  ?X; xvec ♯* Ψ  (Ψ, ⦇ν*xvecP, ⦇ν*xvecQ)  ?X"
          apply(induct xvec, auto)
          by(rule_tac x="xvec@xveca" in exI) (auto simp add: resChainAppend)
        ultimately show ?thesis by(rule simParComm) 
      qed
      moreover note eqvt ?X xvec ♯* Ψ
      moreover have "Ψ P Q x. (Ψ, P, Q)  ?X; x  Ψ  (Ψ, ⦇νxP, ⦇νxQ)  ?X"
        apply auto
        by(rule_tac x="x#xvec" in exI) auto
      ultimately show ?thesis by(rule resChainPres) 
    qed
    ultimately show ?case by simp
  next
    case(cExt Ψ PQ QP Ψ')
    from (Ψ, PQ, QP)  ?X
    obtain xvec P Q where PFrQ: "PQ = ⦇ν*xvec(P  Q)" and QFrP: "QP = ⦇ν*xvec(Q  P)"
                      and "xvec ♯* Ψ"
      by auto
    
    obtain p where "(p  xvec) ♯* Ψ"
               and "(p  xvec) ♯* P"
               and "(p  xvec) ♯* Q"
               and "(p  xvec) ♯* Ψ'"
               and S: "(set p)  (set xvec) × (set(p  xvec))" and "distinctPerm p"
      by(rule_tac c="(Ψ, P, Q, Ψ')" in name_list_avoiding) auto

    from (p  xvec) ♯* P (p  xvec) ♯* Q S have "⦇ν*xvec(P  Q) = ⦇ν*(p  xvec)(p  (P  Q))"
      by(subst resChainAlpha) auto
    hence PQAlpha: "⦇ν*xvec(P  Q) = ⦇ν*(p  xvec)((p  P)  (p  Q))"
      by(simp add: eqvts)

    from (p  xvec) ♯* P (p  xvec) ♯* Q S have "⦇ν*xvec(Q  P) = ⦇ν*(p  xvec)(p  (Q  P))"
      by(subst resChainAlpha) auto
    hence QPAlpha: "⦇ν*xvec(Q  P) = ⦇ν*(p  xvec)((p  Q)  (p  P))"
      by(simp add: eqvts)

    from (p  xvec) ♯* Ψ (p  xvec) ♯* Ψ' have "(Ψ  Ψ', ⦇ν*(p  xvec)((p  P)  (p  Q)), ⦇ν*(p  xvec)((p  Q)  (p  P)))  ?X"
      by auto
    with PFrQ QFrP PQAlpha QPAlpha show ?case by simp
  next
    case(cSym Ψ PR QR)
    thus ?case by blast
  qed
qed

lemma bisimResComm:
  fixes x :: name
  and   Ψ :: 'b
  and   y :: name
  and   P :: "('a, 'b, 'c) psi"

  shows "Ψ  ⦇νx(⦇νyP)  ⦇νy(⦇νxP)"
proof(cases "x=y")
  case True
  thus ?thesis by(blast intro: bisimReflexive)
next
  case False
  {
    fix x::name and y::name and P::"('a, 'b, 'c) psi"
    assume "x  Ψ" and "y  Ψ"
    let ?X = "{((Ψ::'b), ⦇νx(⦇νy(P::('a, 'b, 'c) psi)), ⦇νy(⦇νxP)) | Ψ x y P. x  Ψ  y  Ψ}"
    from x  Ψ y  Ψ have "(Ψ, ⦇νx(⦇νyP), ⦇νy(⦇νxP))  ?X" by auto
    hence "Ψ  ⦇νx(⦇νyP)  ⦇νy(⦇νxP)"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ xyP yxP)
      from (Ψ, xyP, yxP)  ?X obtain x y P where "x  Ψ" and "y  Ψ" and "xyP = ⦇νx(⦇νyP)" and "yxP = ⦇νy(⦇νxP)" by auto
      moreover obtain AP ΨP where "extractFrame P = AP, ΨP" and "AP ♯* Ψ" and "x  AP" and "y  AP"
        by(rule_tac C="(x, y, Ψ)" in freshFrame) auto
      ultimately show ?case by(force intro: frameResComm FrameStatEqTrans)
    next
      case(cSim Ψ xyP yxP)
      from (Ψ, xyP, yxP)  ?X obtain x y P where "x  Ψ" and "y  Ψ" and "xyP = ⦇νx(⦇νyP)" and "yxP = ⦇νy(⦇νxP)" by auto
      note x  Ψ y  Ψ
      moreover have "eqvt ?X" by(force simp add: eqvt_def pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
      hence "eqvt(?X  bisim)" by auto
      moreover have "Ψ P. (Ψ, P, P)  ?X  bisim" by(blast intro: bisimReflexive)
      moreover have "Ψ x y P. x  Ψ; y  Ψ  (Ψ, ⦇νx(⦇νyP), ⦇νy(⦇νxP))  ?X  bisim" by auto
      ultimately have "Ψ  ⦇νx(⦇νyP) ↝[(?X  bisim)] ⦇νy(⦇νxP)" by(rule resComm)
      with xyP = ⦇νx(⦇νyP) yxP = ⦇νy(⦇νxP) show ?case
        by simp
    next
      case(cExt Ψ xyP yxP Ψ')
      from (Ψ, xyP, yxP)  ?X obtain x y P where "x  Ψ" and "y  Ψ" and xyPeq: "xyP = ⦇νx(⦇νyP)" and yxPeq: "yxP = ⦇νy(⦇νxP)" by auto
      show ?case
      proof(case_tac "x=y")
        assume "x = y"
        with xyPeq yxPeq show ?case
          by(blast intro: bisimReflexive)
      next
        assume "x  y"
        obtain x' where "x'  Ψ" and "x'  Ψ'" and "x'  x" and "x'  y" and "x'  P" by(generate_fresh "name") (auto simp add: fresh_prod)
        obtain y' where "y'  Ψ" and "y'  Ψ'" and "y'  x" and "x'  y'" and "y'  y" and "y'  P" by(generate_fresh "name") (auto simp add: fresh_prod)
        with xyPeq y'  P x'  P x  y x'  y y'  x have "⦇νx(⦇νyP) = ⦇νx'(⦇νy'([(x, x')]  [(y, y')]  P))"
          apply(subst alphaRes[of x']) apply(simp add: abs_fresh) by(subst alphaRes[of y' _ y]) (auto simp add: eqvts calc_atm)
        moreover with yxPeq y'  P x'  P x  y x'  y y'  x x'  y' have "⦇νy(⦇νxP) = ⦇νy'(⦇νx'([(y, y')]  [(x, x')]  P))"
          apply(subst alphaRes[of y']) apply(simp add: abs_fresh) by(subst alphaRes[of x' _ x]) (auto simp add: eqvts calc_atm)
        with x  y x'  y y'  y x'  x y'  x x'  y' have "⦇νy(⦇νxP) = ⦇νy'(⦇νx'([(x, x')]  [(y, y')]  P))"
          by(subst perm_compose) (simp add: calc_atm)
        moreover from x'  Ψ x'  Ψ' y'  Ψ y'  Ψ' have "(Ψ  Ψ', ⦇νx'(⦇νy'([(x, x')]  [(y, y')]  P)), ⦇νy'(⦇νx'([(x, x')]  [(y, y')]  P)))  ?X"
          by auto
        ultimately show ?case using xyPeq yxPeq by simp
      qed
    next
      case(cSym Ψ xyP yxP)
      thus ?case by auto
    qed
  }
  moreover obtain x'::name where "x'  Ψ" and "x'  P" and "x'  x" and "x'  y"
    by(generate_fresh "name") auto
  moreover obtain y'::name where "y'  Ψ" and "y'  P" and "y'  x" and "y'  y" and "y'  x'"
    by(generate_fresh "name") auto
  ultimately have "Ψ  ⦇νx'(⦇νy'([(y, y'), (x, x')]  P))  ⦇νy'(⦇νx'([(y, y'), (x, x')]  P))" by auto
  thus ?thesis using x'  P x'  x x'  y y'  P y'  x y'  y y'  x' x  y
    apply(subst alphaRes[where x=x and y=x' and P=P], auto)
    apply(subst alphaRes[where x=y and y=y' and P=P], auto)
    apply(subst alphaRes[where x=x and y=x' and P="⦇νy'([(y, y')]  P)"], auto simp add: abs_fresh fresh_left)
    apply(subst alphaRes[where x=y and y=y' and P="⦇νx'([(x, x')]  P)"], auto simp add: abs_fresh fresh_left)
    by(subst perm_compose) (simp add: eqvts calc_atm)
qed

lemma bisimResComm':
  fixes x    :: name
  and   Ψ   :: 'b
  and   xvec :: "name list"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "x  Ψ"
  and     "xvec ♯* Ψ"

  shows "Ψ  ⦇νx(⦇ν*xvecP)  ⦇ν*xvec(⦇νxP)"
using assms
by(induct xvec) (auto intro: bisimResComm bisimReflexive bisimResPres bisimTransitive)

lemma bisimScopeExt:
  fixes x :: name
  and   Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "x  P"

  shows "Ψ  ⦇νx(P  Q)  P  ⦇νxQ"
proof -
  {
    fix x::name and Q :: "('a, 'b, 'c) psi"
    assume "x  Ψ" and "x  P"
    let ?X1 = "{((Ψ::'b), ⦇ν*xvec(⦇νx((P::('a, 'b, 'c) psi)  Q)), ⦇ν*xvec(P  ⦇νxQ)) | Ψ xvec x P Q. x  Ψ  x  P  xvec ♯* Ψ}"
    let ?X2 = "{((Ψ::'b), ⦇ν*xvec((P::('a, 'b, 'c) psi)  ⦇νxQ), ⦇ν*xvec(⦇νx(P  Q))) | Ψ xvec x P Q. x  Ψ  x  P  xvec ♯* Ψ}"
    let ?X = "?X1  ?X2"

    from x  Ψ x  P have "(Ψ, ⦇νx(P  Q), P  ⦇νxQ)  ?X"
      by(auto, rule_tac x="[]" in exI) (auto simp add: fresh_list_nil)
    moreover have "eqvt ?X"
      by(rule eqvtUnion)
    (fastforce simp add: eqvt_def eqvts pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst] pt_fresh_bij[OF pt_name_inst, OF at_name_inst])+
    ultimately have "Ψ  ⦇νx(P  Q)  P  ⦇νxQ"
    proof(coinduct rule: transitiveCoinduct)
      case(cStatEq Ψ R T)
      show ?case
      proof(case_tac "(Ψ, R, T)  ?X1")
        assume "(Ψ, R, T)  ?X1"
        then obtain xvec x P Q where "R = ⦇ν*xvec(⦇νx(P  Q))" and "T = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
          by auto
        moreover obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" and "x  AP" and "AP ♯* Q"
          by(rule_tac C="(Ψ, x, Q)" in freshFrame) auto
        moreover obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "x  AQ" and "AQ ♯* AP" and "AQ ♯* ΨP"
          by(rule_tac C="(Ψ, x, AP, ΨP)" in freshFrame) auto
        moreover from FrQ AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
          by(drule_tac extractFrameFreshChain) auto
        moreover from x  P x  AP FrP have "x  ΨP" by(drule_tac extractFrameFresh) auto
        ultimately show ?case
          by(force simp add: frameChainAppend intro: frameResComm' FrameStatEqTrans frameResChainPres)
      next
        assume "(Ψ, R, T)  ?X1"
        with (Ψ, R, T)  ?X have "(Ψ, R, T)  ?X2" by blast
        then obtain xvec x P Q where "T = ⦇ν*xvec(⦇νx(P  Q))" and "R = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
          by auto
        moreover obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" and "x  AP" and "AP ♯* Q"
          by(rule_tac C="(Ψ, x, Q)" in freshFrame) auto
        moreover obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "x  AQ" and "AQ ♯* AP" and "AQ ♯* ΨP"
          by(rule_tac C="(Ψ, x, AP, ΨP)" in freshFrame) auto
        moreover from FrQ AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
          by(drule_tac extractFrameFreshChain) auto
        moreover from x  P x  AP FrP have "x  ΨP" by(drule_tac extractFrameFresh) auto
        ultimately show ?case
          apply auto
          by(force simp add: frameChainAppend intro: frameResComm' FrameStatEqTrans frameResChainPres FrameStatEqSym)
      qed
    next
      case(cSim Ψ R T)
      let ?Y = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ  P  P'  ((Ψ, P', Q')  ?X  Ψ  P'  Q')  Ψ  Q'  Q}"
      from eqvt ?X have "eqvt ?Y" by blast
      have C1: "Ψ R T y. (Ψ, R, T)  ?Y; (y::name)  Ψ  (Ψ, ⦇νyR, ⦇νyT)  ?Y"
      proof -
        fix Ψ R T y
        assume "(Ψ, R, T)  ?Y"
        then obtain R' T' where "Ψ  R  R'" and "(Ψ, R', T')  (?X  bisim)" and "Ψ  T'  T" by fastforce
        assume "(y::name)  Ψ" 
        show "(Ψ, ⦇νyR, ⦇νyT)  ?Y"
        proof(case_tac "(Ψ, R', T')  ?X")
          assume "(Ψ, R', T')  ?X"
          show ?thesis
          proof(case_tac "(Ψ, R', T')  ?X1")
            assume "(Ψ, R', T')  ?X1"
            then obtain xvec x P Q where R'eq: "R' = ⦇ν*xvec(⦇νx(P  Q))" and T'eq: "T' = ⦇ν*xvec(P  ⦇νxQ)"
                                     and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
              by auto
            from Ψ  R  R' y  Ψ have "Ψ  ⦇νyR  ⦇νyR'" by(rule bisimResPres)
            moreover from xvec ♯* Ψ y  Ψ x  P x  Ψ have "(Ψ, ⦇ν*(y#xvec)⦇νx(P  Q), ⦇ν*(y#xvec)(P  ⦇νxQ))  ?X1"
              by(force simp del: resChain.simps)
            with R'eq T'eq have "(Ψ, ⦇νyR', ⦇νyT')  ?X  bisim" by simp
            moreover from Ψ  T'  T y  Ψ have "Ψ  ⦇νyT'  ⦇νyT" by(rule bisimResPres)
            ultimately show ?thesis by blast
          next
            assume "(Ψ, R', T')  ?X1"
            with (Ψ, R', T')  ?X have "(Ψ, R', T')  ?X2" by blast
            then obtain xvec x P Q where T'eq: "T' = ⦇ν*xvec(⦇νx(P  Q))" and R'eq: "R' = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
              by auto
            from Ψ  R  R' y  Ψ have "Ψ  ⦇νyR  ⦇νyR'" by(rule bisimResPres)
            moreover from xvec ♯* Ψ y  Ψ x  P x  Ψ have "(Ψ, ⦇ν*(y#xvec)(P  ⦇νxQ), ⦇ν*(y#xvec)(⦇νx(P  Q)))  ?X2"
              by(force simp del: resChain.simps)
            with R'eq T'eq have "(Ψ, ⦇νyR', ⦇νyT')  ?X  bisim" by simp
            moreover from Ψ  T'  T y  Ψ have "Ψ  ⦇νyT'  ⦇νyT" by(rule bisimResPres)
            ultimately show ?thesis by blast
          qed
        next
          assume "(Ψ, R', T')  ?X"
          with (Ψ, R', T')  ?X  bisim have "Ψ  R'  T'" by blast
          with Ψ  R  R' Ψ  T'  T y  Ψ show ?thesis
            by(blast dest: bisimResPres)
        qed
      qed
      
      show ?case
      proof(case_tac "(Ψ, R, T)  ?X1")
        assume "(Ψ, R, T)  ?X1"
        then obtain xvec x P Q where Req: "R = ⦇ν*xvec(⦇νx(P  Q))" and Teq: "T = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
          by auto
        have "Ψ  ⦇ν*xvec(⦇νx(P  Q)) ↝[?Y] ⦇ν*xvec(P  ⦇νxQ)"
        proof -
          have "Ψ  ⦇νx(P  Q) ↝[?Y] P  ⦇νxQ"
          proof -
            note x  P x  Ψ eqvt ?Y
            moreover have "Ψ P. (Ψ, P, P)  ?Y" by(blast intro: bisimReflexive)
            moreover have "x Ψ P Q xvec. x  Ψ; x  P; xvec ♯* Ψ  (Ψ, ⦇νx(⦇ν*xvec(P  Q)), ⦇ν*xvec(P  ⦇νxQ))  ?Y"
            proof -
              fix x Ψ P Q xvec
              assume "(x::name)  (Ψ::'b)" and "x  (P::('a, 'b, 'c) psi)" and "(xvec::name list) ♯* Ψ"
              from x  Ψ xvec ♯* Ψ have "Ψ  ⦇νx(⦇ν*xvec(P  Q))  ⦇ν*xvec(⦇νx(P  Q))"
                by(rule bisimResComm')
              moreover from xvec ♯* Ψ x  Ψ x  P have "(Ψ, ⦇ν*xvec(⦇νx(P  Q)), ⦇ν*xvec(P  ⦇νxQ))  ?X  bisim"
                by blast
              ultimately show "(Ψ, ⦇νx(⦇ν*xvec(P  Q)), ⦇ν*xvec(P  ⦇νxQ))  ?Y" 
                by(blast intro: bisimReflexive)
            qed
            moreover have "Ψ xvec P x. x  Ψ; xvec ♯* Ψ  (Ψ, ⦇νx(⦇ν*xvecP), ⦇ν*xvec(⦇νxP))  ?Y"
              by(blast intro: bisimResComm' bisimReflexive)
            ultimately show ?thesis by(rule scopeExtLeft)
          qed
          thus ?thesis using eqvt ?Y xvec ♯* Ψ C1 
            by(rule resChainPres)
        qed
        with Req Teq show ?case by simp
      next
        assume "(Ψ, R, T)  ?X1"
        with (Ψ, R, T)  ?X have "(Ψ, R, T)  ?X2" by blast
        then obtain xvec x P Q where Teq: "T = ⦇ν*xvec(⦇νx(P  Q))" and Req: "R = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
          by auto
        have "Ψ  ⦇ν*xvec(P  ⦇νxQ) ↝[?Y] ⦇ν*xvec(⦇νx(P  Q))"
        proof -
          have "Ψ  P  ⦇νxQ ↝[?Y] ⦇νx(P  Q)"
          proof -
            note x  P x  Ψ eqvt ?Y
            moreover have "Ψ P. (Ψ, P, P)  ?Y" by(blast intro: bisimReflexive)
            moreover have "x Ψ P Q xvec. x  Ψ; x  P; xvec ♯* Ψ  (Ψ, ⦇ν*xvec(P  ⦇νxQ), ⦇νx(⦇ν*xvec(P  Q)))  ?Y"
            proof -
              fix x Ψ P Q xvec
              assume "(x::name)  (Ψ::'b)" and "x  (P::('a, 'b, 'c) psi)" and "(xvec::name list) ♯* Ψ"
              from xvec ♯* Ψ x  Ψ x  P have "(Ψ, ⦇ν*xvec(P  ⦇νxQ), ⦇ν*xvec(⦇νx(P  Q)))  ?X  bisim"
                by blast
              moreover from x  Ψ xvec ♯* Ψ have "Ψ  ⦇ν*xvec(⦇νx(P  Q))  ⦇νx(⦇ν*xvec(P  Q))"
                by(blast intro: bisimResComm' bisimE)
              ultimately show "(Ψ, ⦇ν*xvec(P  ⦇νxQ), ⦇νx(⦇ν*xvec(P  Q)))  ?Y" 
                by(blast intro: bisimReflexive)
            qed
            ultimately show ?thesis by(rule scopeExtRight)
          qed
          thus ?thesis using eqvt ?Y xvec ♯* Ψ C1 
            by(rule resChainPres)
        qed
        with Req Teq show ?case by simp
      qed
    next
      case(cExt Ψ R T Ψ')
      show ?case
      proof(case_tac "(Ψ, R, T)  ?X1")
        assume "(Ψ, R, T)  ?X1"
        then obtain xvec x P Q where Req: "R = ⦇ν*xvec(⦇νx(P  Q))" and Teq: "T = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
          by auto
        obtain y::name where "y  P" and "y  Q" and "y  xvec" and "y  Ψ" and "y  Ψ'"
          by(generate_fresh "name", auto simp add: fresh_prod)

        obtain p where "(p  xvec) ♯* Ψ" and "(p  xvec) ♯* P" and "(p  xvec) ♯* Q" and "(p  xvec) ♯* Ψ'"
                  and "x  (p  xvec)" and "y  (p  xvec)"
                   and S: "(set p)  (set xvec) × (set(p  xvec))" and "distinctPerm p"
          by(rule_tac c="(Ψ, P, Q, x, y, Ψ')" in name_list_avoiding) auto
        
        
        from y  P have "(p  y)  (p  P)" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
        with S y  xvec y  (p  xvec) have "y  (p  P)" by simp
        with (p  xvec) ♯* Ψ y  Ψ (p  xvec) ♯* Ψ' y  Ψ'
        have "(Ψ  Ψ', ⦇ν*(p  xvec)(⦇νy((p  P)  (p  [(x, y)]  Q))), ⦇ν*(p  xvec)((p  P)  (⦇νy(p  [(x, y)]  Q))))  ?X"
          by auto
        moreover from Req (p  xvec) ♯* P (p  xvec) ♯* Q y  xvec y  (p  xvec) x  (p  xvec) y  P y  Q x  P S
        have "R = ⦇ν*(p  xvec)(⦇νy((p  P)  (p  [(x, y)]  Q)))"
          apply(erule_tac rev_mp)
          apply(subst alphaRes[of y])
          apply(clarsimp simp add: eqvts)
          apply(subst resChainAlpha[of p])
          by(auto simp add: eqvts)
        moreover from Teq (p  xvec) ♯* P (p  xvec) ♯* Q y  xvec y  (p  xvec) x  (p  xvec) y  P y  Q x  P S
        have "T = ⦇ν*(p  xvec)((p  P)  ⦇νy(p  [(x, y)]  Q))"
          apply(erule_tac rev_mp)
          apply(subst alphaRes[of y])
          apply(clarsimp simp add: eqvts)
          apply(subst resChainAlpha[of p])
          by(auto simp add: eqvts)
        ultimately show ?case
          by blast
      next
        assume "(Ψ, R, T)  ?X1"
        with (Ψ, R, T)  ?X have "(Ψ, R, T)  ?X2" by blast
        then obtain xvec x P Q where Teq: "T = ⦇ν*xvec(⦇νx(P  Q))" and Req: "R = ⦇ν*xvec(P  ⦇νxQ)" and "xvec ♯* Ψ" and "x  P" and "x  Ψ"
          by auto
        obtain y::name where "y  P" and "y  Q" and "y  xvec" and "y  Ψ" and "y  Ψ'"
          by(generate_fresh "name", auto simp add: fresh_prod)

        obtain p where "(p  xvec) ♯* Ψ" and "(p  xvec) ♯* P" and "(p  xvec) ♯* Q" and "(p  xvec) ♯* Ψ'"
                   and "x  (p  xvec)" and "y  (p  xvec)"
                   and S: "(set p)  (set xvec) × (set(p  xvec))" and "distinctPerm p"
          by(rule_tac c="(Ψ, P, Q, x, y, Ψ')" in name_list_avoiding) auto
        
        from y  P have "(p  y)  (p  P)" by(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
        with S y  xvec y  (p  xvec) have "y  (p  P)" by simp
        with (p  xvec) ♯* Ψ y  Ψ (p  xvec) ♯* Ψ' y  Ψ'
        have "(Ψ  Ψ', ⦇ν*(p  xvec)((p  P)  ⦇νy(p  [(x, y)]  Q)), ⦇ν*(p  xvec)(⦇νy((p  P)  (p  [(x, y)]  Q))))  ?X2"
          by auto
        moreover from Teq (p  xvec) ♯* P (p  xvec) ♯* Q y  xvec y  (p  xvec) x  (p  xvec) y  P y  Q x  P S
        have "T = ⦇ν*(p  xvec)(⦇νy((p  P)  (p  [(x, y)]  Q)))"
          apply(erule_tac rev_mp)
          apply(subst alphaRes[of y])
          apply(clarsimp simp add: eqvts)
          apply(subst resChainAlpha[of p])
          by(auto simp add: eqvts)
        moreover from Req (p  xvec) ♯* P (p  xvec) ♯* Q y  xvec y  (p  xvec) x  (p  xvec) y  P y  Q x  P S
        have "R = ⦇ν*(p  xvec)((p  P)  ⦇νy(p  [(x, y)]  Q))"
          apply(erule_tac rev_mp)
          apply(subst alphaRes[of y])
          apply(clarsimp simp add: eqvts)
          apply(subst resChainAlpha[of p])
          by(auto simp add: eqvts)
        ultimately show ?case
          by blast
      qed
    next
      case(cSym Ψ P Q)
      thus ?case
        by(blast dest: bisimE)
    qed
  }
  moreover obtain y::name where "y  Ψ" and "y  P" "y  Q"
    by(generate_fresh "name") auto
  ultimately have "Ψ  ⦇νy(P  ([(x, y)]  Q))  P  ⦇νy([(x, y)]  Q)" by auto
  thus ?thesis using assms y  P y  Q
    apply(subst alphaRes[where x=x and y=y and P=Q], auto)
    by(subst alphaRes[where x=x and y=y and P="P  Q"]) auto
qed

lemma bisimScopeExtChain:
  fixes xvec :: "name list"
  and   Ψ    :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "xvec ♯* Ψ"
  and     "xvec ♯* P"

  shows "Ψ  ⦇ν*xvec(P  Q)  P  (⦇ν*xvecQ)"
using assms
by(induct xvec) (auto intro: bisimScopeExt bisimReflexive bisimTransitive bisimResPres) 

lemma bisimParAssoc:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  shows "Ψ  (P  Q)  R  P  (Q  R)"
proof -
  let ?X = "{(Ψ, ⦇ν*xvec((P  Q)  R), ⦇ν*xvec(P  (Q  R))) | Ψ xvec P Q R. xvec ♯* Ψ}"
  let ?Y = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ  P  P'  (Ψ, P', Q')  ?X  Ψ  Q'  Q}"

  have "(Ψ, (P  Q)  R, P  (Q  R))  ?X"
    by(auto, rule_tac x="[]" in exI) auto
  moreover have "eqvt ?X" by(force simp add: eqvt_def simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst] eqvts)
  ultimately show ?thesis
  proof(coinduct rule: weakTransitiveCoinduct')
    case(cStatEq Ψ PQR PQR')
    from (Ψ, PQR, PQR')  ?X obtain xvec P Q R where "xvec ♯* Ψ" and "PQR = ⦇ν*xvec((P  Q)  R)" and "PQR' = ⦇ν*xvec(P  (Q  R))"
      by auto
    moreover obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" and "AP ♯* Q" and "AP ♯* R"
      by(rule_tac C="(Ψ, Q, R)" in freshFrame) auto
    moreover obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "AQ ♯* AP" and "AQ ♯* ΨP" and "AQ ♯* R"
      by(rule_tac C="(Ψ, AP, ΨP, R)" in freshFrame) auto
    moreover obtain AR ΨR where FrR: "extractFrame R = AR, ΨR" and "AR ♯* Ψ" and "AR ♯* AP" and "AR ♯* ΨP" and "AR ♯* AQ" and "AR ♯* ΨQ"
      by(rule_tac C="(Ψ, AP, ΨP, AQ, ΨQ)" in freshFrame) auto
    moreover from FrQ AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
      by(drule_tac extractFrameFreshChain) auto
    moreover from FrR AP ♯* R AR ♯* AP have "AP ♯* ΨR"
      by(drule_tac extractFrameFreshChain) auto
    moreover from FrR AQ ♯* R AR ♯* AQ have "AQ ♯* ΨR"
      by(drule_tac extractFrameFreshChain) auto
    ultimately show ?case using freshCompChain
      by auto (metis frameChainAppend compositionSym Associativity frameNilStatEq frameResChainPres)
  next
    case(cSim Ψ T S)
    from (Ψ, T, S)  ?X obtain xvec P Q R where "xvec ♯* Ψ" and TEq: "T = ⦇ν*xvec((P  Q)  R)"
                                               and SEq: "S = ⦇ν*xvec(P  (Q  R))"
      by auto
    from eqvt ?Xhave "eqvt ?Y" by blast
    have C1: "Ψ T S yvec. (Ψ, T, S)  ?Y; yvec ♯* Ψ  (Ψ, ⦇ν*yvecT, ⦇ν*yvecS)  ?Y"
    proof -
      fix Ψ T S yvec
      assume "(Ψ, T, S)  ?Y"
      then obtain T' S' where "Ψ  T  T'" and "(Ψ, T', S')  ?X" and "Ψ  S'  S" by fastforce
      assume "(yvec::name list) ♯* Ψ" 
      from (Ψ, T', S')  ?X obtain xvec P Q R where T'eq: "T' = ⦇ν*xvec((P  Q)  R)" and S'eq: "S' = ⦇ν*xvec(P  (Q  R))"
                                                  and "xvec ♯* Ψ"
        by auto
      from Ψ  T  T' yvec ♯* Ψ have "Ψ  ⦇ν*yvecT  ⦇ν*yvecT'" by(rule bisimResChainPres)
      moreover from xvec ♯* Ψ yvec ♯* Ψ have "(Ψ, ⦇ν*(yvec@xvec)((P  Q)  R), ⦇ν*(yvec@xvec)(P  (Q  R)))  ?X"
        by force
      with T'eq S'eq have "(Ψ, ⦇ν*yvecT', ⦇ν*yvecS')  ?X" by(simp add: resChainAppend)
      moreover from Ψ  S'  S yvec ♯* Ψ have "Ψ  ⦇ν*yvecS'  ⦇ν*yvecS" by(rule bisimResChainPres)
      ultimately show "(Ψ, ⦇ν*yvecT, ⦇ν*yvecS)  ?Y" by blast
    qed
    have C2: "Ψ T S y. (Ψ, T, S)  ?Y; y  Ψ  (Ψ, ⦇νyT, ⦇νyS)  ?Y"
      by(drule_tac yvec2="[y]" in C1) auto

    have "Ψ  ⦇ν*xvec((P  Q)  R) ↝[?Y] ⦇ν*xvec(P  (Q  R))"
    proof -
      have "Ψ  (P  Q)  R ↝[?Y] P  (Q  R)" 
      proof -
        note eqvt ?Y
        moreover have "Ψ P Q R. (Ψ, (P  Q)  R, P  (Q  R))  ?Y"
        proof -
          fix Ψ P Q R
          have "(Ψ::'b, ((P::('a, 'b, 'c) psi)  Q)  R, P  (Q  R))  ?X"
            by(auto, rule_tac x="[]" in exI) auto
          thus "(Ψ, (P  Q)  R, P  (Q  R))  ?Y"
            by(blast intro: bisimReflexive)
        qed
        moreover have "xvec Ψ P Q R. xvec ♯* Ψ; xvec ♯* P  (Ψ, ⦇ν*xvec((P  Q)  R), P  (⦇ν*xvec(Q  R)))  ?Y"
        proof -
          fix xvec Ψ P Q R
          assume "(xvec::name list) ♯* (Ψ::'b)" and "xvec ♯* (P::('a, 'b, 'c) psi)"
          from xvec ♯* Ψ have "(Ψ, ⦇ν*xvec((P  Q)  R), ⦇ν*xvec(P  (Q  R)))  ?X" by blast
          moreover from xvec ♯* Ψ xvec ♯* P have "Ψ  ⦇ν*xvec(P  (Q  R))  P  (⦇ν*xvec(Q  R))"
            by(rule bisimScopeExtChain)
          ultimately show "(Ψ, ⦇ν*xvec((P  Q)  R), P  (⦇ν*xvec(Q  R)))  ?Y"
            by(blast intro: bisimReflexive)
        qed
        moreover have "xvec Ψ P Q R. xvec ♯* Ψ; xvec ♯* R  (Ψ, (⦇ν*xvec(P  Q))  R, ⦇ν*xvec(P  (Q  R)))  ?Y"
        proof -
          fix xvec Ψ P Q R
          assume "(xvec::name list) ♯* (Ψ::'b)" and "xvec ♯* (R::('a, 'b, 'c) psi)"
          have "Ψ  (⦇ν*xvec(P  Q))  R  R  (⦇ν*xvec(P  Q))" by(rule bisimParComm)
          moreover from xvec ♯* Ψ xvec ♯* R have "Ψ  ⦇ν*xvec(R  (P  Q))  R  (⦇ν*xvec(P  Q))" by(rule bisimScopeExtChain)
          hence "Ψ  R  (⦇ν*xvec(P  Q))  ⦇ν*xvec(R  (P  Q))" by(rule bisimE)
          moreover from xvec ♯* Ψ have "Ψ  ⦇ν*xvec(R  (P  Q))  ⦇ν*xvec((P  Q)  R)"
            by(metis bisimResChainPres bisimParComm)
          moreover from xvec ♯* Ψ have "(Ψ, ⦇ν*xvec((P  Q)  R), ⦇ν*xvec(P  (Q  R)))  ?X" by blast
          ultimately show "(Ψ, (⦇ν*xvec(P  Q))  R, ⦇ν*xvec(P  (Q  R)))  ?Y"  by(blast dest: bisimTransitive intro: bisimReflexive)
        qed
        ultimately show ?thesis using C1
          by(rule parAssocLeft)
      qed
      thus ?thesis using eqvt ?Y xvec ♯* Ψ C2
        by(rule resChainPres)
    qed
    with TEq SEq show ?case by simp
  next
    case(cExt Ψ T S Ψ')
    from (Ψ, T, S)  ?X obtain xvec P Q R where "xvec ♯* Ψ" and TEq: "T = ⦇ν*xvec((P  Q)  R)"
                                               and SEq: "S = ⦇ν*xvec(P  (Q  R))"
      by auto
    obtain p where "(p  xvec) ♯* Ψ" and "(p  xvec) ♯* P" and "(p  xvec) ♯* Q" and "(p  xvec) ♯* R" and "(p  xvec) ♯* Ψ'"
               and S: "(set p)  (set xvec) × (set(p  xvec))" and "distinctPerm p"
      by(rule_tac c="(Ψ, P, Q, R, Ψ')" in name_list_avoiding) auto

    from (p  xvec) ♯* Ψ (p  xvec) ♯* Ψ' have "(Ψ  Ψ', ⦇ν*(p  xvec)(((p  P)  (p  Q))  (p  R)), ⦇ν*(p  xvec)((p  P)  ((p  Q)  (p  R))))  ?X"
      by auto
    moreover from TEq (p  xvec) ♯* P (p  xvec) ♯* Q (p  xvec) ♯* R S have "T = ⦇ν*(p  xvec)(((p  P)  (p  Q))  (p  R))"
      apply auto by(subst resChainAlpha[of p]) auto
    moreover from SEq (p  xvec) ♯* P (p  xvec) ♯* Q (p  xvec) ♯* R S have "S = ⦇ν*(p  xvec)((p  P)  ((p  Q)  (p  R)))"
      apply auto by(subst resChainAlpha[of p]) auto
    ultimately show ?case by simp
  next
    case(cSym Ψ T S)
    from (Ψ, T, S)  ?X obtain xvec P Q R where "xvec ♯* Ψ" and TEq: "T = ⦇ν*xvec((P  Q)  R)"
                                               and SEq: "⦇ν*xvec(P  (Q  R)) = S"
      by auto
    
    from xvec ♯* Ψ have "Ψ  ⦇ν*xvec(P  (Q  R))  ⦇ν*xvec((R  Q)  P)"
      by(metis bisimParComm bisimParPres bisimTransitive bisimResChainPres)
    moreover from xvec ♯* Ψ have "(Ψ, ⦇ν*xvec((R  Q)  P), ⦇ν*xvec(R  (Q  P)))  ?X" by blast
    moreover from xvec ♯* Ψ have "Ψ  ⦇ν*xvec(R  (Q  P))  ⦇ν*xvec((P  Q)  R)"
      by(metis bisimParComm bisimParPres bisimTransitive bisimResChainPres)
    ultimately show ?case using TEq SEq by(blast dest: bisimTransitive)
  qed
qed    

lemma bisimParNil:
  fixes P :: "('a, 'b, 'c) psi"

  shows "Ψ  P  𝟬  P"
proof -
  let ?X1 = "{(Ψ, P  𝟬, P) | Ψ P. True}"
  let ?X2 = "{(Ψ, P, P  𝟬) | Ψ P. True}"
  let ?X = "?X1  ?X2"
  have "eqvt ?X" by(auto simp add: eqvt_def)
  have "(Ψ, P  𝟬, P)  ?X" by simp
  thus ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ Q R)
    show ?case
    proof(case_tac "(Ψ, Q, R)  ?X1")
      assume "(Ψ, Q, R)  ?X1"
      then obtain P where "Q = P  𝟬" and "R = P" by auto
      moreover obtain AP ΨP where "extractFrame P = AP, ΨP" and "AP ♯* Ψ"
        by(rule freshFrame)
      ultimately show ?case
        apply auto by(metis frameResChainPres frameNilStatEq Identity Associativity AssertionStatEqTrans Commutativity)
    next
      assume "(Ψ, Q, R)  ?X1"
      with (Ψ, Q, R)  ?X have "(Ψ, Q, R)  ?X2" by blast
      then obtain P where "Q = P" and "R = P  𝟬" by auto
      moreover obtain AP ΨP where "extractFrame P = AP, ΨP" and "AP ♯* Ψ"
        by(rule freshFrame)
      ultimately show ?case
        apply auto by(metis frameResChainPres frameNilStatEq Identity Associativity AssertionStatEqTrans AssertionStatEqSym Commutativity)
    qed
  next
    case(cSim Ψ Q R)
    thus ?case using eqvt ?X
      by(auto intro: parNilLeft parNilRight)
  next
    case(cExt Ψ Q R Ψ')
    thus ?case by auto
  next
    case(cSym Ψ Q R)
    thus ?case by auto
  qed
qed

lemma bisimResNil:
  fixes x :: name
  and   Ψ :: 'b
  
  shows "Ψ  ⦇νx𝟬  𝟬"
proof -
  {
    fix x::name
    assume "x  Ψ"
    have "Ψ  ⦇νx𝟬  𝟬"
    proof -
      let ?X1 = "{(Ψ, ⦇νx𝟬, 𝟬) | Ψ x. x  Ψ}"
      let ?X2 = "{(Ψ, 𝟬, ⦇νx𝟬) | Ψ x. x  Ψ}"
      let ?X = "?X1  ?X2"

      from x  Ψ have "(Ψ, ⦇νx𝟬, 𝟬)  ?X" by auto
      thus ?thesis
      proof(coinduct rule: bisimWeakCoinduct)
        case(cStatEq Ψ P Q)
        thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
      next
        case(cSim Ψ P Q)
        thus ?case
          by(force intro: resNilLeft resNilRight)
      next
        case(cExt Ψ P Q Ψ')
        obtain y where "y  Ψ" and "y  Ψ'" and "y  x"
          by(generate_fresh "name") (auto simp add: fresh_prod)
        show ?case
        proof(case_tac "(Ψ, P, Q)  ?X1")
          assume "(Ψ, P, Q)  ?X1"
          then obtain x where "P = ⦇νx𝟬" and "Q = 𝟬" by auto
          moreover have "⦇νx𝟬 = ⦇νy 𝟬" by(subst alphaRes) auto
          ultimately show ?case using y  Ψ y  Ψ' by auto
        next
          assume "(Ψ, P, Q)  ?X1"
          with (Ψ, P, Q)  ?X have "(Ψ, P, Q)  ?X2" by auto
          then obtain x where "Q = ⦇νx𝟬" and "P = 𝟬" by auto
          moreover have "⦇νx𝟬 = ⦇νy 𝟬" by(subst alphaRes) auto
          ultimately show ?case using y  Ψ y  Ψ' by auto
        qed
      next
        case(cSym Ψ P Q)
        thus ?case by auto
      qed
    qed
  }
  moreover obtain y::name where "y  Ψ" by(generate_fresh "name") auto
  ultimately have "Ψ  ⦇νy𝟬  𝟬" by auto
  thus ?thesis by(subst alphaRes[where x=x and y=y]) auto
qed

lemma bisimOutputPushRes:
  fixes x :: name
  and   Ψ :: 'b
  and   M :: 'a
  and   N :: 'a
  and   P :: "('a, 'b, 'c) psi"

  assumes "x  M"
  and     "x  N"

  shows "Ψ  ⦇νx(MN⟩.P)  MN⟩.⦇νxP"
proof -
  {
    fix x::name and P::"('a, 'b, 'c) psi"
    assume "x  Ψ" and "x  M" and "x  N"
    let ?X1 = "{(Ψ, ⦇νx(MN⟩.P), MN⟩.⦇νxP) | Ψ x M N P. x  Ψ  x  M  x  N}"
    let ?X2 = "{(Ψ, MN⟩.⦇νxP, ⦇νx(MN⟩.P)) | Ψ x M N P. x  Ψ  x  M  x  N}"
    let ?X = "?X1  ?X2"
  
    have "eqvt ?X" by(rule_tac eqvtUnion) (force simp add: eqvt_def pt_fresh_bij[OF pt_name_inst, OF at_name_inst] eqvts)+
    from x  Ψ x  M x  N  have "(Ψ, ⦇νx(MN⟩.P), MN⟩.⦇νxP)  ?X" by auto
    hence "Ψ  ⦇νx(MN⟩.P)  MN⟩.⦇νxP"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ Q R)
      thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
    next
      case(cSim Ψ Q R)
      thus ?case using eqvt ?X
        by(fastforce intro: outputPushResLeft outputPushResRight bisimReflexive)
    next
      case(cExt Ψ Q R Ψ')
      show ?case
      proof(case_tac "(Ψ, Q, R)  ?X1")
        assume "(Ψ, Q, R)  ?X1"
        then obtain x M N P where Qeq: "Q = ⦇νx(MN⟩.P)" and Req: "R = MN⟩.⦇νxP" and "x  Ψ" and "x  M" and "x  N" by auto
        obtain y::name where "y  Ψ" and "y  Ψ'" and "y  M" and "y  N" and "y  P"
          by(generate_fresh "name") (auto simp add: fresh_prod)
        
        moreover hence "(Ψ  Ψ', ⦇νy(MN⟩.([(x, y)]  P)), MN⟩.⦇νy([(x, y)]  P))  ?X" by auto
        moreover from Qeq x  M y  M x  N y  N y  P have "Q = ⦇νy(MN⟩.([(x, y)]  P))"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Req y  P have "R = MN⟩.⦇νy([(x, y)]  P)"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        ultimately show ?case by blast
      next
        assume "(Ψ, Q, R)  ?X1"
        with (Ψ, Q, R)  ?X have "(Ψ, Q, R)  ?X2" by blast
        then obtain x M N P where Req: "R = ⦇νx(MN⟩.P)" and Qeq: "Q = MN⟩.⦇νxP" and "x  Ψ" and "x  M" and "x  N" by auto
        obtain y::name where "y  Ψ" and "y  Ψ'" and "y  M" and "y  N" and "y  P"
          by(generate_fresh "name") (auto simp add: fresh_prod)
        
        moreover hence "(Ψ  Ψ', ⦇νy(MN⟩.([(x, y)]  P)), MN⟩.⦇νy([(x, y)]  P))  ?X" by auto
        moreover from Req x  M y  M x  N y  N y  P have "R = ⦇νy(MN⟩.([(x, y)]  P))"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Qeq y  P have "Q = MN⟩.⦇νy([(x, y)]  P)"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        ultimately show ?case by blast
      qed
    next
      case(cSym Ψ R Q)
      thus ?case by blast
    qed
  }
  moreover obtain y::name where "y  Ψ" and "y  M" and "y  N" "y  P"
    by(generate_fresh "name") auto
  ultimately have "Ψ  ⦇νy(MN⟩.([(x, y)]  P))  MN⟩.⦇νy([(x, y)]  P)" by auto
  thus ?thesis using assms y  P y  M y  N
    apply(subst alphaRes[where x=x and y=y and P=P], auto)
    by(subst alphaRes[where x=x and y=y and P="MN⟩.P"]) auto
qed

lemma bisimInputPushRes:
  fixes x    :: name
  and   Ψ    :: 'b
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "x  M"
  and     "x  xvec"
  and     "x  N"

  shows "Ψ  ⦇νx(M⦇λ*xvec N⦈.P)  M⦇λ*xvec N⦈.⦇νxP"
proof -
  {
    fix x::name and P::"('a, 'b, 'c) psi"
    assume "x  Ψ" and "x  M" and "x  N" and "x  xvec"
    let ?X1 = "{(Ψ, ⦇νx(M⦇λ*xvec N⦈.P), M⦇λ*xvec N⦈.⦇νxP) | Ψ x M xvec N P. x  Ψ  x  M  x  xvec  x  N}"
    let ?X2 = "{(Ψ, M⦇λ*xvec N⦈.⦇νxP, ⦇νx(M⦇λ*xvec N⦈.P)) | Ψ x M xvec N P. x  Ψ  x  M  x  xvec  x  N}"
    let ?X = "?X1  ?X2"
  
    have "eqvt ?X" by(rule_tac eqvtUnion) (force simp add: eqvt_def pt_fresh_bij[OF pt_name_inst, OF at_name_inst] eqvts)+

    from x  Ψ x  M x  xvec x  N have "(Ψ, ⦇νx(M⦇λ*xvec N⦈.P), M⦇λ*xvec N⦈.⦇νxP)  ?X" by blast
    hence "Ψ  ⦇νx(M⦇λ*xvec N⦈.P)  M⦇λ*xvec N⦈.⦇νxP"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ Q R)
      thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
    next
      case(cSim Ψ Q R)
      thus ?case using eqvt ?X
        by(fastforce intro: inputPushResLeft inputPushResRight bisimReflexive)
    next
      case(cExt Ψ Q R Ψ')
      show ?case
      proof(case_tac "(Ψ, Q, R)  ?X1")
        assume "(Ψ, Q, R)  ?X1"
        then obtain x M xvec N P where Qeq: "Q = ⦇νx(M⦇λ*xvec N⦈.P)" and Req: "R = M⦇λ*xvec N⦈.⦇νxP" and "x  Ψ"
                                   and "x  M" and "x  xvec" and "x  N" by auto
        obtain y::name where "y  Ψ" and "y  Ψ'" and "y  M" and "y  N" and "y  P" and "y  xvec"
          by(generate_fresh "name") (auto simp add: fresh_prod)
        
        moreover hence "(Ψ  Ψ', ⦇νy(M⦇λ*xvec N⦈.([(x, y)]  P)), M⦇λ*xvec N⦈.⦇νy([(x, y)]  P))  ?X" by fastforce
        moreover from Qeq x  M y  M x  xvec y  xvec x  N y  N y  P have "Q = ⦇νy(M⦇λ*xvec N⦈.([(x, y)]  P))"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts inputChainFresh)
        moreover from Req y  P have "R = M⦇λ*xvec N ⦈.⦇νy([(x, y)]  P)"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        ultimately show ?case by blast
      next
        assume "(Ψ, Q, R)  ?X1"
        with (Ψ, Q, R)  ?X have "(Ψ, Q, R)  ?X2" by blast
        then obtain x M xvec N P where Req: "R = ⦇νx(M⦇λ*xvec N⦈.P)" and Qeq: "Q = M⦇λ*xvec N⦈.⦇νxP" and "x  Ψ"
                                   and "x  M" and "x  xvec" and "x  N" by auto
        obtain y::name where "y  Ψ" and "y  Ψ'" and "y  M" and "y  N" and "y  P" and "y  xvec"
          by(generate_fresh "name") (auto simp add: fresh_prod)

        moreover hence "(Ψ  Ψ', ⦇νy(M⦇λ*xvec N⦈.([(x, y)]  P)), M⦇λ*xvec N⦈.⦇νy([(x, y)]  P))  ?X" by fastforce
        moreover from Req x  M y  M x  xvec y  xvec x  N y  N y  P have "R = ⦇νy(M⦇λ*xvec N⦈.([(x, y)]  P))"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts inputChainFresh)
        moreover from Qeq y  P have "Q = M⦇λ*xvec N ⦈.⦇νy([(x, y)]  P)"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        ultimately show ?case by blast
      qed
    next
      case(cSym Ψ R Q)
      thus ?case by blast
    qed
  }
  moreover obtain y::name where "y  Ψ" and "y  M" and "y  N" and "y  P" and "y  xvec"
    by(generate_fresh "name") auto
  ultimately have "Ψ  ⦇νy(M⦇λ*xvec N⦈.([(x, y)]  P))  M⦇λ*xvec N⦈.⦇νy([(x, y)]  P)" by auto
  thus ?thesis using assms y  P y  M y  N y  xvec
    apply(subst alphaRes[where x=x and y=y and P=P], auto)
    by(subst alphaRes[where x=x and y=y and P="M⦇λ*xvec N⦈.P"]) (auto simp add: inputChainFresh eqvts)
qed

lemma bisimCasePushRes:
  fixes x  :: name
  and   Ψ  :: 'b
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "x  (map fst Cs)"

  shows "Ψ  ⦇νx(Cases Cs)  Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)"
proof -
  {
    fix x::name and Cs::"('c × ('a, 'b, 'c) psi) list"
    assume "x  Ψ" and "x  (map fst Cs)"
    let ?X1 = "{(Ψ, ⦇νx(Cases Cs), Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)) | Ψ x Cs. x  Ψ  x  (map fst Cs)}"
    let ?X2 = "{(Ψ, Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs), ⦇νx(Cases Cs)) | Ψ x Cs. x  Ψ  x  (map fst Cs)}"
    let ?X = "?X1  ?X2"
  
    have "eqvt ?X" apply(rule_tac eqvtUnion) 
      apply(auto simp add: eqvt_def eqvts)
      apply(rule_tac x="p  x" in exI)
      apply(rule_tac x="p  Cs" in exI)
      apply(perm_extend_simp)
      apply(auto simp add: eqvts)
      apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
      apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
      apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
      apply(simp add: eqvts)
      apply(perm_extend_simp)
      apply(simp add: eqvts)
      apply(rule_tac x="p  x" in exI)
      apply(rule_tac x="p  Cs" in exI)
      apply auto
      apply(perm_extend_simp)
      apply(simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
      apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
      apply(drule_tac pi=p in pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
      apply(simp add: eqvts)
      apply(perm_extend_simp)
      by(simp add: eqvts)    
    
    from x  Ψ x  map fst Cs have "(Ψ, ⦇νx(Cases Cs), Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs))  ?X" by auto
    hence "Ψ  ⦇νx(Cases Cs)  Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ Q R)
      thus ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
    next
      case(cSim Ψ Q R)
      thus ?case using eqvt ?X
        by(fastforce intro: casePushResLeft casePushResRight bisimReflexive)
    next
      case(cExt Ψ Q R Ψ')
      show ?case
      proof(case_tac "(Ψ, Q, R)  ?X1")
        assume "(Ψ, Q, R)  ?X1"
        then obtain x Cs where Qeq: "Q = ⦇νx(Cases Cs)" and Req: "R = Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)"
                           and "x  Ψ" and "x  (map fst Cs)" by blast
        obtain y::name where "y  Ψ" and "y  Ψ'" and "y  Cs"
          by(generate_fresh "name") (auto simp add: fresh_prod)
        from y  Cs x  (map fst Cs) have "y  map fst ([(x, y)]  Cs)" by(induct Cs) (auto simp add: fresh_list_cons fresh_list_nil)

        moreover with y  Ψ y  Ψ' have "(Ψ  Ψ', ⦇νy(Cases ([(x, y)]  Cs)), Cases(map (λ(φ, P). (φ, ⦇νyP)) ([(x, y)]  Cs)))  ?X"
          by auto
        moreover from Qeq y  Cs have "Q = ⦇νy(Cases([(x, y)]  Cs))"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Req y  Cs x  (map fst Cs) have "R = Cases(map (λ(φ, P). (φ, ⦇νyP)) ([(x, y)]  Cs))" 
          by(induct Cs arbitrary: R) (auto simp add: fresh_list_cons fresh_prod alphaRes)
        ultimately show ?case by blast
      next
        assume "(Ψ, Q, R)  ?X1"
        with (Ψ, Q, R)  ?X have "(Ψ, Q, R)  ?X2" by blast
        then obtain x Cs where Req: "R = ⦇νx(Cases Cs)" and Qeq: "Q = Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)"
                           and "x  Ψ" and "x  (map fst Cs)" by blast
        obtain y::name where "y  Ψ" and "y  Ψ'" and "y  Cs"
          by(generate_fresh "name") (auto simp add: fresh_prod)
        from y  Cs x  (map fst Cs) have "y  map fst ([(x, y)]  Cs)" by(induct Cs) (auto simp add: fresh_list_cons fresh_list_nil)
        
        moreover with y  Ψ y  Ψ' have "(Ψ  Ψ', ⦇νy(Cases ([(x, y)]  Cs)), Cases(map (λ(φ, P). (φ, ⦇νyP)) ([(x, y)]  Cs)))  ?X"
          by auto
        moreover from Req y  Cs have "R = ⦇νy(Cases([(x, y)]  Cs))"
          apply auto by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Qeq y  Cs x  (map fst Cs) have "Q = Cases(map (λ(φ, P). (φ, ⦇νyP)) ([(x, y)]  Cs))" 
          by(induct Cs arbitrary: Q) (auto simp add: fresh_list_cons fresh_prod alphaRes)
        ultimately show ?case by blast
      qed
    next
      case(cSym Ψ R Q)
      thus ?case by blast
    qed
  }
  moreover obtain y::name where "y  Ψ" and "y  Cs" by(generate_fresh "name") auto
  moreover from x  map fst Cs have "y  map fst([(x, y)]  Cs)" 
    by(induct Cs) (auto simp add: fresh_left calc_atm)
  ultimately have "Ψ  ⦇νy(Cases ([(x, y)]  Cs))  Cases(map (λ(φ, P). (φ, ⦇νyP)) ([(x, y)]  Cs))"
    by auto
  moreover from y  Cs have "⦇νy(Cases ([(x, y)]  Cs)) =  ⦇νx(Cases Cs)"
    by(simp add: alphaRes eqvts)
  moreover from x  map fst Cs y  Cs have "Cases(map (λ(φ, P). (φ, ⦇νyP)) ([(x, y)]  Cs)) = Cases(map (λ(φ, P). (φ, ⦇νxP)) Cs)"
    by(induct Cs) (auto simp add: alphaRes)
  ultimately show ?thesis by auto
qed

lemma bangExt:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  
  assumes "guarded P"

  shows "Ψ  !P  P  !P"
proof -
  let ?X = "{(Ψ, !P, P  !P) | Ψ P. guarded P}  {(Ψ, P  !P, !P) | Ψ P. guarded P}"
  from guarded P have "(Ψ, !P, P  !P)  ?X" by auto
  thus ?thesis
  proof(coinduct rule: bisimCoinduct)
    case(cStatEq Ψ Q R)
    from (Ψ, Q, R)  ?X obtain P where Eq: "(Q = !P  R = P  !P)  (Q = P  !P  R = !P)" and "guarded P"
      by auto
    obtain AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" by(rule freshFrame)
    from FrP guarded P have "ΨP  SBottom'" by(blast dest: guardedStatEq)
    from ΨP  SBottom' have "Ψ  SBottom'  Ψ  ΨP  SBottom'" by(metis Identity Composition AssertionStatEqTrans Commutativity AssertionStatEqSym)
    hence "AP, Ψ  SBottom' F AP, Ψ  ΨP  SBottom'"
      by(force intro: frameResChainPres)
    moreover from AP ♯* Ψ have "⟨ε, Ψ  SBottom' F AP, Ψ  SBottom'"
      by(rule_tac FrameStatEqSym) (fastforce intro: frameResFreshChain)
    ultimately show ?case using Eq AP ♯* Ψ FrP
      by auto (blast dest: FrameStatEqTrans FrameStatEqSym)+
  next
    case(cSim Ψ Q R)
    thus ?case by(auto intro: bangExtLeft bangExtRight bisimReflexive)
  next
    case(cExt Ψ Q R)
    thus ?case by auto
  next
    case(cSym Ψ Q R)
    thus ?case by auto
  qed
qed
  
lemma bisimParPresSym:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "Ψ  P  Q"

  shows "Ψ  R  P  R  Q"
using assms
by(metis bisimParComm bisimParPres bisimTransitive)

lemma bisimScopeExtSym:
  fixes x :: name
  and   Q :: "('a, 'b, 'c) psi"
  and   P :: "('a, 'b, 'c) psi"

  assumes "x  Ψ"
  and     "x  Q"

  shows "Ψ  ⦇νx(P  Q)  (⦇νxP)  Q"
using assms
by(metis bisimScopeExt bisimTransitive bisimParComm bisimSymmetric bisimResPres)

lemma bisimScopeExtChainSym:
  fixes xvec :: "name list"
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "xvec ♯* Ψ"
  and     "xvec ♯* Q"

  shows "Ψ  ⦇ν*xvec(P  Q)  (⦇ν*xvecP)  Q"
using assms
by(induct xvec) (auto intro: bisimScopeExtSym bisimReflexive bisimTransitive bisimResPres)

lemma bisimParPresAuxSym:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"
  and   R :: "('a, 'b, 'c) psi"

  assumes "Ψ  ΨR  P  Q"
  and     "extractFrame R = AR, ΨR"
  and     "AR ♯* Ψ"
  and     "AR ♯* P"
  and     "AR ♯* Q"

  shows "Ψ  R  P  R  Q"
using assms
by(metis bisimParComm bisimParPresAux bisimTransitive)

lemma bangDerivative:
  fixes Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "Ψ  !P α  P'"
  and     "Ψ  P  Q"
  and     "bn α ♯* Ψ"
  and     "bn α ♯* P"
  and     "bn α ♯* Q"
  and     "bn α ♯* subject α"
  and     "guarded Q"

  obtains Q' R T where "Ψ  !Q α  Q'" and "Ψ  P'  R  !P" and "Ψ  Q'  T  !Q" and "Ψ  R  T"
                   and "((supp R)::name set)  supp P'" and "((supp T)::name set)  supp Q'"
proof -
  from Ψ  !P α  P' have "guarded P" apply - by(ind_cases "Ψ  !P α  P'") (auto simp add: psi.inject)
  assume "Q' R T. Ψ  !Q α  Q'; Ψ  P'  R  !P; Ψ  Q'  T  !Q; Ψ  R  T; ((supp R)::name set)  supp P';
                    ((supp T)::name set)  supp Q'  thesis"
  moreover from Ψ  !P α  P' bn α ♯* subject α bn α ♯* Ψ bn α ♯* P bn α ♯* Q Ψ  P  Q guarded Q 
  have "Q' T R . Ψ  !Q α   Q'  Ψ  P'  R  !P  Ψ  Q'  T  !Q  Ψ  R  T 
                  ((supp R)::name set)  supp P'  ((supp T)::name set)  supp Q'"
  proof(nominal_induct avoiding: Q rule: bangInduct')
    case(cAlpha α P' p Q)
    then obtain Q' T R where QTrans: "Ψ  !Q α  Q'" and "Ψ  P'  R  (P  !P)" and "Ψ  Q'  T  !Q" and "Ψ  R  T"
                         and suppR: "((supp R)::name set)  supp P'" and suppT: "((supp T)::name set)  supp Q'"
      by blast
    from QTrans have "distinct(bn α)" by(rule boundOutputDistinct)
    have S: "set p  set(bn α) × set(bn(p  α))" by fact
    from QTrans bn(p  α) ♯* Q bn(p  α) ♯* α bn α ♯* subject α distinct(bn α) have "bn(p  α) ♯* Q'"
      by(drule_tac freeFreshChainDerivative) simp+
    with QTrans bn(p  α) ♯* α S bn α ♯* subject α have "Ψ  !Q (p  α)  (p  Q')"
      by(force simp add: residualAlpha)
    moreover from Ψ  P'  R  (P  !P) have "(p  Ψ)  (p  P')  (p  (R  (P  !P)))"
      by(rule bisimClosed)
    with bn α ♯* Ψ bn α ♯* P bn(p  α) ♯* Ψ bn(p  α) ♯* P S have "Ψ  (p  P')  (p  R)  (P  !P)"
      by(simp add: eqvts)
    moreover from Ψ  Q'  T  !Q have "(p  Ψ)  (p  Q')  (p  (T  !Q))"
      by(rule bisimClosed)
    with bn α ♯* Ψ bn α ♯* Q bn(p  α) ♯* Ψ bn(p  α) ♯* Q S have "Ψ  (p  Q')  (p  T)  !Q"
      by(simp add: eqvts)
    moreover from Ψ  R  T have "(p  Ψ)  (p  R)  (p  T)"
      by(rule bisimClosed)
    with bn α ♯* Ψ bn(p  α) ♯* Ψ S have "Ψ  (p  R)  (p  T)"
      by(simp add: eqvts)
    moreover from suppR have "((supp(p  R))::name set)  supp(p  P')"
      apply(erule_tac rev_mp)
      by(subst subsetClosed[of p, symmetric]) (simp add: eqvts)
    moreover from suppT have "((supp(p  T))::name set)  supp(p  Q')"
      apply(erule_tac rev_mp)
      by(subst subsetClosed[of p, symmetric]) (simp add: eqvts)
    ultimately show ?case by blast
  next
    case(cPar1 α P' Q)
    from Ψ  P  Q Ψ  P α  P' bn α ♯* Ψ bn α ♯* Q 
    obtain Q' where QTrans: "Ψ  Q α  Q'" and "Ψ  P'  Q'"
      by(blast dest: bisimE simE)
    from QTrans have "Ψ  SBottom'  Q α  Q'" by(metis statEqTransition Identity AssertionStatEqSym)
    hence "Ψ  Q  !Q α  (Q'  !Q)" using bn α ♯* Q by(rule_tac Par1) (assumption | simp)+
    hence "Ψ  !Q α  (Q'  !Q)" using guarded Q by(rule Bang)
    moreover from guarded P have "Ψ  P'  !P  P'  (P  !P)" by(metis bangExt bisimParPresSym)
    moreover have "Ψ  Q'  !Q  Q'  !Q" by(rule bisimReflexive)
    ultimately show ?case using Ψ  P'  Q' by(force simp add: psi.supp)
  next
    case(cPar2 α P' Q)
    then obtain Q' T R where QTrans: "Ψ  !Q α  Q'" and "Ψ  P'  R  !P" and "Ψ  Q'  T  !Q" and "Ψ  R  T"
                         and suppR: "((supp R)::name set)  supp P'" and suppT: "((supp T)::name set)  supp Q'"
      by blast
    note QTrans
    from Ψ  P'  R  !P have "Ψ  P  P'  R  (P  !P)"
      by(metis bisimParPresSym bisimParComm bisimTransitive bisimParAssoc)
    with QTrans show ?case using Ψ  Q'  T  !Q Ψ  R  T suppR suppT
      by(force simp add: psi.supp)
  next
    case(cComm1 M N P' K xvec P'' Q)
    from Ψ  P  Q have "Ψ  Q ↝[bisim] P" by(metis bisimE)
    with Ψ  P MN  P' obtain Q' where QTrans: "Ψ  Q MN  Q'" and "Ψ  Q'  P'"
      by(force dest: simE)
    from QTrans have "Ψ  SBottom'  Q MN  Q'" by(metis statEqTransition Identity AssertionStatEqSym)
    moreover obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "AQ ♯* Q" and "AQ ♯* M" 
      by(rule_tac C="(Ψ, Q, M)" in freshFrame) auto
    note FrQ
    moreover from FrQ guarded Q have "ΨQ  SBottom'" by(blast dest: guardedStatEq)
    from Ψ  !P K⦇ν*xvec⦈⟨N  P'' xvec ♯* K Ψ  P  Q xvec ♯* Ψ xvec ♯* P xvec ♯* Q guarded Q
    obtain Q'' T R where QTrans': "Ψ  !Q K⦇ν*xvec⦈⟨N  Q''" and "Ψ  P''  R  !P" and "Ψ  Q''  T  !Q" and "Ψ  R  T"
                     and suppR: "((supp R)::name set)  supp P''" and suppT: "((supp T)::name set)  supp Q''" using cComm1
      by fastforce
    from QTrans' ΨQ  SBottom' have "Ψ  ΨQ  !Q K⦇ν*xvec⦈⟨N  Q''" 
      by(metis statEqTransition Identity compositionSym AssertionStatEqSym)
    moreover from Ψ  M  K ΨQ  SBottom' have "Ψ  ΨQ  SBottom'  M  K" by(metis statEqEnt Identity compositionSym AssertionStatEqSym)
    ultimately have "Ψ  Q  !Q τ  (⦇ν*xvec(Q'  Q''))" using AQ ♯* Ψ AQ ♯* Q AQ ♯* M xvec ♯* Q
      by(rule_tac Comm1) (assumption | simp)+
    hence "Ψ  !Q τ  (⦇ν*xvec(Q'  Q''))" using guarded Q by(rule Bang)
    moreover from Ψ  P''  R  !P guarded P xvec ♯* Ψ have "Ψ  ⦇ν*xvec(P'  P'')  ⦇ν*xvec((P'  R)  (P  !P))"
      by(metis bisimParPresSym bangExt bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres)
    with xvec ♯* Ψ xvec ♯* P have "Ψ  ⦇ν*xvec(P'  P'')  (⦇ν*xvec(P'  R))  (P  !P)"
      by(metis bisimScopeExtChainSym bisimTransitive psiFreshVec)
    moreover from Ψ  Q''  T  !Q xvec ♯* Ψ xvec ♯* Q have "Ψ  ⦇ν*xvec(Q'  Q'')  (⦇ν*xvec(Q'  T))  !Q"
      by(metis bisimParPresSym bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres bisimScopeExtChainSym psiFreshVec)
    moreover from Ψ  R  T Ψ  Q'  P' xvec ♯* Ψ have "Ψ  ⦇ν*xvec(P'  R)  ⦇ν*xvec(Q'  T)"
      by(metis bisimParPresSym bisimTransitive bisimResChainPres bisimParComm bisimE(4))
    moreover from suppR have "((supp(⦇ν*xvec(P'  R)))::name set)   supp((⦇ν*xvec(P'  P'')))"
      by(auto simp add: psi.supp resChainSupp)
    moreover from suppT have "((supp(⦇ν*xvec(Q'  T)))::name set)   supp((⦇ν*xvec(Q'  Q'')))"
      by(auto simp add: psi.supp resChainSupp)
    ultimately show ?case by blast
  next
    case(cComm2 M xvec N P' K P'' Q)
    from Ψ  P  Q Ψ  P M⦇ν*xvec⦈⟨N  P' xvec ♯* Ψ xvec ♯* Q 
    obtain Q' where QTrans: "Ψ  Q M⦇ν*xvec⦈⟨N  Q'" and "Ψ  P'  Q'"
      by(metis bisimE simE bn.simps)
    from QTrans have "Ψ  SBottom'  Q M⦇ν*xvec⦈⟨N  Q'" by(metis statEqTransition Identity AssertionStatEqSym)
    moreover obtain AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "AQ ♯* Q" and "AQ ♯* M" 
      by(rule_tac C="(Ψ, Q, M)" in freshFrame) auto
    note FrQ
    moreover from FrQ guarded Q have "ΨQ  SBottom'" by(blast dest: guardedStatEq)
    from Ψ  !P KN  P'' Ψ  P  Q guarded Q
   obtain Q'' T R where QTrans': "Ψ  !Q KN  Q''" and "Ψ  P''  R  !P" and "Ψ  Q''  T  !Q" and "Ψ  R  T"
                    and suppR: "((supp R)::name set)  supp P''" and suppT: "((supp T)::name set)  supp Q''" using cComm2
     by fastforce
    from QTrans' ΨQ  SBottom' have "Ψ  ΨQ  !Q KN  Q''" 
      by(metis statEqTransition Identity compositionSym AssertionStatEqSym)
    moreover from Ψ  M  K ΨQ  SBottom' have "Ψ  ΨQ  SBottom'  M  K" by(metis statEqEnt Identity compositionSym AssertionStatEqSym)
    ultimately have "Ψ  Q  !Q τ  (⦇ν*xvec(Q'  Q''))" using AQ ♯* Ψ AQ ♯* Q AQ ♯* M xvec ♯* Q
      by(rule_tac Comm2) (assumption | simp)+
    hence "Ψ  !Q τ  (⦇ν*xvec(Q'  Q''))" using guarded Q by(rule Bang)
    moreover from Ψ  P''  R  !P guarded P xvec ♯* Ψ have "Ψ  ⦇ν*xvec(P'  P'')  ⦇ν*xvec((P'  R)  (P  !P))"
      by(metis bisimParPresSym bangExt bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres)
    with xvec ♯* Ψ xvec ♯* P have "Ψ  ⦇ν*xvec(P'  P'')  (⦇ν*xvec(P'  R))  (P  !P)"
      by(metis bisimScopeExtChainSym bisimTransitive psiFreshVec)
    moreover from Ψ  Q''  T  !Q xvec ♯* Ψ xvec ♯* Q have "Ψ  ⦇ν*xvec(Q'  Q'')  (⦇ν*xvec(Q'  T))  !Q"
      by(metis bisimParPresSym bisimTransitive bisimParAssoc bisimSymmetric bisimResChainPres bisimScopeExtChainSym psiFreshVec)
    moreover from Ψ  R  T Ψ  P'  Q' xvec ♯* Ψ have "Ψ  ⦇ν*xvec(P'  R)  ⦇ν*xvec(Q'  T)"
      by(metis bisimParPresSym bisimTransitive bisimResChainPres bisimParComm)
    moreover from suppR have "((supp(⦇ν*xvec(P'  R)))::name set)   supp((⦇ν*xvec(P'  P'')))"
      by(auto simp add: psi.supp resChainSupp)
    moreover from suppT have "((supp(⦇ν*xvec(Q'  T)))::name set)   supp((⦇ν*xvec(Q'  Q'')))"
      by(auto simp add: psi.supp resChainSupp)
    ultimately show ?case by blast
  next
    case(cBang α P' Q)
    then obtain Q' T R where QTrans: "Ψ  !Q α  Q'" and "Ψ  P'  R  (P  !P)" and "Ψ  Q'  T  !Q" and "Ψ  R  T"
                         and suppR: "((supp R)::name set)  supp P'" and suppT: "((supp T)::name set)  supp Q'"
      by blast
    from Ψ  P'  R  (P  !P) guarded P have "Ψ  P'  R  !P" by(metis bangExt bisimParPresSym bisimTransitive bisimSymmetric)
    with QTrans show ?case using Ψ  Q'  T  !Q Ψ  R  T suppR suppT
      by blast
  qed
  ultimately show ?thesis by blast
qed

lemma structCongBisim:
  fixes P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "P s Q"

  shows "P  Q"
using assms
by(induct rule: structCong.induct)
  (auto intro: bisimReflexive bisimSymmetric bisimTransitive bisimParComm bisimParAssoc bisimParNil bisimResNil bisimResComm bisimScopeExt bisimCasePushRes bisimInputPushRes bisimOutputPushRes bangExt)

lemma bisimBangPres:
  fixes Ψ :: 'b
  and   P :: "('a, 'b, 'c) psi"
  and   Q :: "('a, 'b, 'c) psi"

  assumes "Ψ  P  Q"
  and     "guarded P"
  and     "guarded Q"

  shows "Ψ  !P  !Q"
proof -
  let ?X = "{(Ψ, R  !P, R  !Q) | Ψ P Q R. Ψ  P  Q  guarded P  guarded Q}"
  let ?Y = "{(Ψ, P, Q) | Ψ P P' Q' Q. Ψ  P  P'  (Ψ, P', Q')  ?X  Ψ  Q'  Q}"
  from assms have "(Ψ, 𝟬  !P, 𝟬  !Q)  ?X" by(blast intro: bisimReflexive)

  moreover have "eqvt ?X" 
    apply(auto simp add: eqvt_def)
    apply(drule_tac p=p in bisimClosed)
    by fastforce
  ultimately have "Ψ  𝟬  !P  𝟬  !Q"
  proof(coinduct rule: weakTransitiveCoinduct)
    case(cStatEq Ψ P Q)
    thus ?case by auto
  next
    case(cSim Ψ RP RQ)
    from (Ψ, RP, RQ)  ?X obtain P Q R where "Ψ  P  Q" and "guarded P" and "guarded Q"
                                           and "RP = R  !P" and "RQ = R  !Q"
      by auto
    note Ψ  P  Q 
    moreover from eqvt ?X have "eqvt ?Y" by blast
    moreover note guarded P guarded Q bisimE(2) bisimE(3) bisimE(4) statEqBisim bisimClosed bisimParAssoc[THEN bisimSymmetric] 
                  bisimParPres bisimParPresAuxSym bisimResChainPres bisimScopeExtChainSym bisimTransitive
    moreover have "Ψ P Q R T. Ψ  P  Q; (Ψ, Q, R)  ?Y; Ψ  R  T  (Ψ, P, T)  ?Y"
      by auto (metis bisimTransitive)
    moreover have "Ψ P Q R. Ψ  P  Q; guarded P; guarded Q  (Ψ, R  !P, R  !Q)  ?Y" by(blast intro: bisimReflexive)
    moreover have "Ψ P α P' Q. Ψ  !P α  P'; Ψ  P  Q; bn α ♯* Ψ;  bn α ♯* P;  bn α ♯* Q; guarded Q; bn α ♯* subject α 
                                         Q' R T.  Ψ  !Q α  Q'  Ψ  P'  R  !P   Ψ  Q'  T  !Q 
                                                   Ψ  R  T  ((supp R)::name set)  supp P'  
                                                   ((supp T)::name set)  supp Q'"
      by(blast elim: bangDerivative)
    ultimately have "Ψ  R  !P ↝[?Y] R  !Q"
      by(rule bangPres)
    with RP = R  !P RQ = R  !Q show ?case
      by blast
  next
    case(cExt Ψ RP RQ Ψ')
    thus ?case by(blast dest: bisimE)
  next
    case(cSym Ψ RP RQ)
    thus ?case by(blast dest: bisimE)
  qed
  thus ?thesis
    by(metis bisimTransitive bisimParNil bisimSymmetric bisimParComm)
qed

end

end