Theory Bisim_Struct_Cong

theory Bisim_Struct_Cong
  imports Bisim_Pres Sim_Struct_Cong "Psi_Calculi.Structural_Congruence"
begin

text ‹This file is a (heavily modified) variant of the theory {\it Psi\_Calculi.Bisim\_Struct\_Cong}
from~\cite{DBLP:journals/afp/Bengtson12}.›

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"
    using resChain.base by(smt (verit) freshSets(1) mem_Collect_eq)
  then show ?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 A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* Q"
      by(rule freshFrame[where C="(Ψ, Q)"]) auto
    obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P"
      by(rule freshFrame[where C="(Ψ, A⇩P, Ψ⇩P)"]) auto
    from FrQ ‹A⇩Q ♯* A⇩P› ‹A⇩P ♯* Q› have "A⇩P ♯* Ψ⇩Q" by(force dest: extractFrameFreshChain)
    have "⟨(xvec@A⇩P@A⇩Q), Ψ ⊗ Ψ⇩P ⊗ Ψ⇩Q⟩ ≃⇩F ⟨(xvec@A⇩Q@A⇩P), Ψ ⊗ Ψ⇩Q ⊗ Ψ⇩P⟩"
      by(simp add: frameChainAppend)
        (metis frameResChainPres frameResChainComm frameNilStatEq compositionSym Associativity Commutativity FrameStatEqTrans)
    with FrP FrQ PFrQ QFrP ‹A⇩P ♯* Ψ⇩Q› ‹A⇩Q ♯* Ψ⇩P› ‹A⇩Q ♯* A⇩P› ‹xvec ♯* Ψ› ‹A⇩P ♯* Ψ› ‹A⇩Q ♯* Ψ›
    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"
          using resChain.base by(smt (verit) freshSets(1) mem_Collect_eq)
        moreover have "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X"
        proof (induct xvec)
          case Nil
          then show ?case
            by (smt (verit, ccfv_threshold) Pair_inject freshChainAppend mem_Collect_eq resChainAppend)
        next
          case (Cons a xvec)
          then show ?case
            by blast
        qed
        ultimately show ?thesis by(rule simParComm)
      qed
      moreover note ‹eqvt ?X› ‹xvec ♯* Ψ›
      moreover have "⋀Ψ P Q xvec. ⟦(Ψ, P, Q) ∈ ?X; xvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*xvec⦈P, ⦇ν*xvec⦈Q) ∈ ?X"
        using resChainAppend[symmetric] freshChainAppend by blast
      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 name_list_avoiding[where c="(Ψ, P, Q, Ψ')"]) auto

    from ‹(p ∙ xvec) ♯* P› ‹(p ∙ xvec) ♯* Q› S have "⦇ν*xvec⦈(P ∥ Q) = ⦇ν*(p ∙ xvec)⦈(p ∙ (P ∥ Q))"
      by(subst resChainAlpha) auto
    then have 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
    then have 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)
    then show ?case by blast
  qed
qed

inductive_set resCommRel :: "('b × ('a,'b,'c) psi × ('a,'b,'c) psi) set"
  where
    resCommRel_refl : "(Ψ,P,P) ∈ resCommRel"
  | resCommRel_swap : "⟦a ♯ Ψ; b ♯ Ψ⟧ ⟹ (Ψ,⦇νa⦈(⦇νb⦈P),⦇νb⦈(⦇νa⦈P)) ∈ resCommRel"
  | resCommRel_res : "⟦(Ψ,P,Q) ∈ resCommRel; a ♯ Ψ⟧ ⟹ (Ψ,⦇νa⦈P,⦇νa⦈Q) ∈ resCommRel"

lemma eqvtResCommRel: "eqvt resCommRel"
proof -
  {
    fix Ψ P Q
      and p::"name prm"
    assume "(Ψ,P,Q) ∈ resCommRel"
    then have "(p∙Ψ,p∙P,p∙Q) ∈ resCommRel"
    proof(induct rule: resCommRel.inducts)
      case resCommRel_refl then show ?case by(rule resCommRel.intros)
    next
      case(resCommRel_swap a Ψ b P)
      then have "(p∙a) ♯ p∙Ψ" and "(p∙b) ♯ p∙Ψ"
         apply -
        by(subst (asm) (1 2) perm_bool[where pi=p,symmetric], simp add: eqvts)+
      then show ?case unfolding eqvts
        by(rule resCommRel.intros)
    next
      case(resCommRel_res Ψ P Q a)
      from ‹a ♯ Ψ› have "(p∙a) ♯ p∙Ψ"
        apply -
        by(subst (asm) perm_bool[where pi=p,symmetric], simp add: eqvts)
      then show ?case using ‹(p ∙ Ψ, p ∙ P, p ∙ Q) ∈ resCommRel›
        unfolding eqvts
        by(intro resCommRel.intros)
    qed
  }
  then show ?thesis unfolding eqvt_def
    by auto
qed

lemma resCommRelStarRes:
  assumes "(Ψ,P,Q) ∈ resCommRel⇧⋆"
    and   "a ♯ Ψ"
  shows   "(Ψ,⦇νa⦈P,⦇νa⦈Q) ∈ resCommRel⇧⋆"
  using assms
proof(induct rule: rel_trancl.induct)
  case r_into_rel_trancl then show ?case by(auto intro: resCommRel_res)
next
  case(rel_trancl_into_rel_trancl Ψ P Q R)
  then show ?case
    by(auto dest: resCommRel_res intro: rel_trancl.intros)
qed

lemma resCommRelStarResChain:
  assumes "(Ψ,P,Q) ∈ resCommRel⇧⋆"
    and   "xvec ♯* Ψ"
  shows   "(Ψ,⦇ν*xvec⦈P,⦇ν*xvec⦈Q) ∈ resCommRel⇧⋆"
  using assms
  by(induct xvec) (auto simp add: resCommRelStarRes)

lemma length_induct1[consumes 0, case_names Nil Cons]:
  assumes b: "P []"
    and   s: "⋀ x xvec. ⟦⋀ yvec. length xvec=length yvec⟹P yvec⟧ ⟹ P(x#xvec)"
  shows   "P xvec"
proof(induct xvec rule: length_induct)
  case(1 xvec)
  then show ?case
  proof(cases xvec)
    case Nil then show ?thesis by(simp add: b)
  next
    case(Cons y yvec)
    with ‹∀ys. length ys < length xvec ⟶ P ys› have "∀ys. length ys = length yvec ⟶ P ys" by simp
    then show ?thesis unfolding Cons
      using s by auto
  qed
qed

lemma oneStepPerm_in_rel:
  assumes "xvec ♯* Ψ"
  shows "(Ψ,⦇ν*xvec⦈P,⦇ν*(rotate1 xvec)⦈P) ∈ resCommRel⇧⋆"
  using assms
proof(induct xvec rule: length_induct1)
  case Nil then show ?case by(auto intro: resCommRel_refl)
next
  case(Cons x xvec)
  note Cons1 = this
  show ?case
  proof(cases xvec)
    case Nil then show ?thesis
      by(auto intro: resCommRel_refl)
  next
    case(Cons y yvec)
    then have "x ♯ Ψ" and "y ♯ Ψ" and "xvec ♯* Ψ" using ‹(x # xvec) ♯* Ψ›
      by simp+
    have "(Ψ, ⦇ν*(x#y#yvec)⦈P, ⦇ν*(y#x#yvec)⦈P) ∈ resCommRel⇧⋆" using ‹x ♯ Ψ› ‹y ♯ Ψ›
      by(auto intro: resCommRel_swap)
    moreover have "(Ψ, ⦇ν*(y#x#yvec)⦈P, ⦇ν*(y#rotate1(x#yvec))⦈P) ∈ resCommRel⇧⋆"
    proof -
      have "(Ψ, ⦇ν*(x#yvec)⦈P, ⦇ν*rotate1(x#yvec)⦈P) ∈ resCommRel⇧⋆" using ‹xvec ♯* Ψ› Cons ‹x ♯ Ψ›
        by(intro Cons1) auto
      then show ?thesis using ‹y ♯ Ψ›
        unfolding resChain.simps
        by(rule resCommRelStarRes)
    qed
    ultimately show ?thesis unfolding Cons
      by(auto intro: rel_trancl_transitive)
  qed
qed

lemma fresh_same_multiset:
  fixes xvec::"name list"
    and yvec::"name list"
  assumes "mset xvec = mset yvec"
    and   "xvec ♯* X"
  shows   "yvec ♯* X"
proof -
  from ‹mset xvec = mset yvec› have "set xvec = set yvec"
    using mset_eq_setD by blast
  then show ?thesis using ‹xvec ♯* X›
    unfolding fresh_def fresh_star_def name_list_supp
    by auto
qed

lemma nStepPerm_in_rel:
  assumes "xvec ♯* Ψ"
  shows "(Ψ,⦇ν*xvec⦈P,⦇ν*(rotate n xvec)⦈P) ∈ resCommRel⇧⋆"
  using assms
proof(induct n)
  case 0 then show ?case by(auto intro: resCommRel_refl)
next
  case(Suc n)
  then have "(Ψ, ⦇ν*xvec⦈P, ⦇ν*rotate n xvec⦈P) ∈ resCommRel⇧⋆"
    by simp
  moreover have "(Ψ, ⦇ν*rotate n xvec⦈P,⦇ν*rotate (Suc n) xvec⦈P) ∈ resCommRel⇧⋆"
  proof -
    {
      fix xvec::"name list"
      assume "xvec ♯* Ψ"
      have "rotate1 xvec ♯* Ψ" using ‹xvec ♯* Ψ›
      proof(induct xvec)
        case Nil then show ?case by simp
      next
        case Cons then show ?case by simp
      qed
    }
    note f1 = this
    have "rotate n xvec ♯* Ψ" using ‹xvec ♯* Ψ›
      by(induct n) (auto simp add: f1)
    then show ?thesis
      by(auto simp add: oneStepPerm_in_rel)
  qed
  ultimately show ?case
    by(rule rel_trancl_transitive)
qed

lemma any_perm_in_rel:
  assumes "xvec ♯* Ψ"
    and   "mset xvec = mset yvec"
  shows "(Ψ,⦇ν*xvec⦈P,⦇ν*yvec⦈P) ∈ resCommRel⇧⋆"
  using assms
proof(induct xvec arbitrary: yvec rule: length_induct1)
  case Nil then show ?case by(auto intro: resCommRel.intros)
next
  case(Cons x xvec)
  obtain yvec1 yvec2 where yveceq: "yvec=yvec1@x#yvec2"
  proof -
    assume 1: "⋀yvec1 yvec2. yvec = yvec1 @ x # yvec2 ⟹ thesis"
    {
      note ‹mset (x # xvec) = mset yvec›
      then have "∃ yvec1 yvec2. yvec=yvec1@x#yvec2"
      proof(induct xvec arbitrary: yvec rule: length_induct1)
        case Nil
        from ‹mset [x] = mset yvec› have "yvec = [x]"
          apply(induct yvec)
           apply simp
          apply(simp add: single_is_union)
          done
        then show ?case by blast
      next
        case(Cons x' xvec)
        have less: "{#x'#} ⊆# mset yvec" unfolding ‹mset (x # x' # xvec) = mset yvec›[symmetric]
          by simp
        from ‹mset (x # x' # xvec) = mset yvec›
        have "mset (x # xvec) = mset (remove1 x' yvec)"
          by (metis mset_remove1 remove1.simps(2))
        then have "∃yvec1 yvec2. (remove1 x' yvec) = yvec1 @ x # yvec2"
          by(intro Cons) simp+
        then obtain yvec1 yvec2 where "(remove1 x' yvec) = yvec1 @ x # yvec2"
          by blast
        then show ?case
        proof(induct yvec arbitrary: yvec1 yvec2)
          case Nil then show ?case by simp
        next
          case(Cons y yvec) then show ?case
          proof(cases "x'=y")
            case True
            with ‹remove1 x' (y # yvec) = yvec1 @ x # yvec2›
            have "yvec = yvec1 @ x # yvec2"
              by simp
            then show ?thesis
              by (metis append_Cons)
          next
            case False
            then have "remove1 x' (y#yvec) = y # remove1 x' (yvec)"
              by simp
            note Cons2=Cons
            show ?thesis
            proof(cases yvec1)
              case Nil
              then show ?thesis using Cons2 False
                by auto
            next
              case(Cons y1 yvec1a)
              from ‹remove1 x' (y # yvec) = yvec1 @ x # yvec2› ‹yvec1 = y1 # yvec1a› False have "y1=y"
                by simp
              from ‹remove1 x' (y # yvec) = yvec1 @ x # yvec2›
              have "remove1 x' yvec = yvec1a @ x # yvec2" unfolding Cons ‹y1=y› using False
                by simp
              then have "∃yvec1 yvec2. yvec = yvec1 @ x # yvec2"
                by(rule Cons2)
              then obtain yvec1 yvec2 where "yvec = yvec1 @ x # yvec2"
                by blast
              then show ?thesis
                by (metis append_Cons)
            qed
          qed
        qed
      qed
    }
    then show ?thesis using 1
      by blast
  qed
  from ‹(x # xvec) ♯* Ψ› have "x ♯ Ψ" and "xvec ♯* Ψ" by auto
  have "mset (x # xvec) = mset(yvec1 @ x # yvec2)"
    unfolding yveceq[symmetric] by fact
  then have "mset (xvec) = mset(yvec1 @ yvec2)"
    by(subst add_right_cancel[symmetric,where a="{#x#}"]) (simp add: add.assoc)
  then have "(Ψ, ⦇ν*xvec⦈P, ⦇ν*(yvec1@yvec2)⦈P) ∈ resCommRel⇧⋆" using ‹xvec ♯* Ψ›
    by(intro Cons) auto
  moreover have "(Ψ, ⦇ν*(yvec1@yvec2)⦈P, ⦇ν*(yvec2@yvec1)⦈P) ∈ resCommRel⇧⋆"
  proof -
    have e: "yvec2 @ yvec1 = rotate (length yvec1) (yvec1@yvec2)"
      apply(cases yvec2)
       apply simp
      apply(simp add: rotate_drop_take)
      done
    have "(yvec1@yvec2) ♯* Ψ" using ‹mset (xvec) = mset(yvec1 @ yvec2)› ‹xvec ♯* Ψ›
      by(rule fresh_same_multiset)
    then show ?thesis unfolding e
      by(rule nStepPerm_in_rel)
  qed
  ultimately have "(Ψ, ⦇ν*xvec⦈P, ⦇ν*(yvec2 @ yvec1)⦈P) ∈ resCommRel⇧⋆"
    by(rule rel_trancl_transitive)
  then have "(Ψ, ⦇ν*(x#xvec)⦈P, ⦇ν*(x # yvec2 @ yvec1)⦈P) ∈ resCommRel⇧⋆"
    unfolding resChain.simps using ‹x ♯ Ψ›
    by(rule resCommRelStarRes)
  moreover have "(Ψ, ⦇ν*(x # yvec2 @ yvec1)⦈P, ⦇ν*(yvec1 @ x # yvec2)⦈P) ∈ resCommRel⇧⋆"
  proof -
    have e: "yvec1 @ x # yvec2 = rotate (1+length yvec2) (x#yvec2@yvec1)"
      apply(simp add: rotate_drop_take)
      apply(cases yvec1)
      by simp+
    have "(yvec1 @ x # yvec2) ♯* Ψ" using ‹mset (x # xvec) = mset(yvec1 @ x # yvec2)› ‹(x#xvec) ♯* Ψ›
      by(rule fresh_same_multiset)
    then have "(x # yvec2 @ yvec1) ♯* Ψ" by simp
    then show ?thesis unfolding e
      by(rule nStepPerm_in_rel)
  qed
  ultimately show ?case unfolding yveceq
    by(rule rel_trancl_transitive)
qed

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

shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ∼ ⦇νy⦈(⦇νx⦈P)"
proof(cases "x=y")
  case True
  then show ?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 = resCommRel
    from ‹x ♯ Ψ› ‹y ♯ Ψ› have "(Ψ, ⦇νx⦈(⦇νy⦈P), ⦇νy⦈(⦇νx⦈P)) ∈ ?X"
      by(rule resCommRel_swap)
    then have "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ∼ ⦇νy⦈(⦇νx⦈P)" using eqvtResCommRel
    proof(coinduct rule: bisimStarWeakCoinduct)
      case(cStatEq Ψ R S)
      then show ?case
      proof(induct rule: resCommRel.induct)
        case resCommRel_refl then show ?case by(rule FrameStatEqRefl)
      next
        case(resCommRel_swap x Ψ y P)
        moreover obtain A⇩P Ψ⇩P where "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "x ♯ A⇩P" and "y ♯ A⇩P"
          by(rule freshFrame[where C="(x, y, Ψ)"]) auto
        ultimately show ?case by(force intro: frameResComm FrameStatEqTrans)
      next
        case(resCommRel_res Ψ P Q a)
        then show ?case by(auto intro: frameResPres)
      qed
    next
      case(cSim Ψ R S)
      have "eqvt(resCommRel⇧⋆)"
        by(rule rel_trancl_eqvt) (rule eqvtResCommRel)
      from cSim show ?case
      proof(induct rule: resCommRel.induct)
        case(resCommRel_refl Ψ P)
        then show ?case
          by(rule simI[OF ‹eqvt(resCommRel⇧⋆)›]) (blast intro: resCommRel.intros)
      next
        case(resCommRel_swap a Ψ b P)
        show ?case
          by(rule resComm) (fact|auto intro: resCommRel.intros any_perm_in_rel)+
      next
        case(resCommRel_res Ψ P Q a)
        show ?case
          by(rule resPres[where Rel="resCommRel⇧⋆"]) (fact|simp add: resCommRelStarResChain)+
      qed
    next
      case(cExt Ψ R S Ψ') then show ?case
      proof(induct arbitrary: Ψ' rule: resCommRel.induct)
        case resCommRel_refl then show ?case by(rule resCommRel_refl)
      next
        case(resCommRel_swap a Ψ b P)
        then show ?case
        proof(cases "a=b")
          case True show ?thesis unfolding ‹a=b› by(rule resCommRel_refl)
        next
          case False
          obtain x::name and y::name where "x≠y" and "x ♯ Ψ" and "x ♯ Ψ'" and "x ♯ P" and "x ≠ a" and "x≠b" and "y ♯ Ψ" and "y ♯ Ψ'" and "y ♯ P" and "y ≠ a" and "y≠b"
            apply(generate_fresh "name")
            apply(generate_fresh "name")
            by force
          then show ?thesis using False
            apply(subst (1 2) alphaRes[where x=a and y=x])
              apply assumption
             apply(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
            apply(subst (1 2) alphaRes[where x=b and y=y])
              apply(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp] fresh_left)
             apply assumption
            unfolding eqvts
            apply(subst (1) cp1[OF cp_pt_inst, OF pt_name_inst, OF at_name_inst])
            by(auto simp add: eqvts swap_simps intro: resCommRel.intros)
        qed
      next
        case(resCommRel_res Ψ P Q a)
        obtain b::name where "b ♯ Ψ" and "b ≠ a" and "b ♯ P" and "b ♯ Q" and "b ♯ Ψ'"
          by(generate_fresh "name") auto
        have "(Ψ ⊗ ([(a,b)]∙Ψ'), P, Q) ∈ resCommRel" by fact
        moreover from ‹b ♯ Ψ'› have "a ♯ ([(a, b)] ∙ Ψ')" by(simp add: fresh_left swap_simps)
        with ‹a ♯ Ψ› have "a ♯ Ψ ⊗ ([(a,b)]∙Ψ')" by force
        ultimately have "(Ψ ⊗ ([(a,b)]∙Ψ'), ⦇νa⦈P, ⦇νa⦈Q) ∈ resCommRel"
          by(rule resCommRel.intros)
        then have "([(a,b)]∙(Ψ ⊗ ([(a,b)]∙Ψ'), ⦇νa⦈P, ⦇νa⦈Q)) ∈ resCommRel" using eqvtResCommRel
          by(intro eqvtI)
        then have "(Ψ ⊗ Ψ', ⦇νb⦈([(a,b)]∙P), ⦇νb⦈([(a,b)]∙Q)) ∈ resCommRel" using ‹a ♯ Ψ› ‹b ♯ Ψ›
          by(simp add: eqvts swap_simps)
        then show ?case using ‹b ♯ Q› ‹b ♯ P›
          apply(subst (1 2) alphaRes[where x=a and y=b])
          by(assumption|simp only: eqvts)+
      qed
    next
      case(cSym Ψ R S) then show ?case
        by(induct rule: resCommRel.inducts) (auto intro: resCommRel.intros)
    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
  then show ?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⦈(⦇ν*xvec⦈P) ∼ ⦇ν*xvec⦈(⦇νx⦈P)"
  using assms
  by(induct xvec) (auto intro: bisimResComm bisimReflexive bisimResPres bisimTransitive)

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 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 ∥ ⦇νx⦈Q"
proof -
  {
    fix x::name and Q :: "('a, 'b, 'c) psi"
    assume "x ♯ Ψ" and "x ♯ P"
    let ?X1 = "{((Ψ::'b), ⦇ν*xvec⦈(⦇ν*yvec⦈((P::('a, 'b, 'c) psi) ∥ Q)), ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))) | Ψ xvec yvec P Q. yvec ♯* Ψ ∧ yvec ♯* P ∧ xvec ♯* Ψ}"
    let ?X2 = "{((Ψ::'b), ⦇ν*xvec⦈((P::('a, 'b, 'c) psi) ∥ (⦇ν*yvec⦈Q)), ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))) | Ψ xvec yvec P Q. yvec ♯* Ψ ∧ yvec ♯* P ∧ xvec ♯* Ψ}"
    let ?X = "?X1 ∪ ?X2"
    from ‹x ♯ Ψ› ‹x ♯ P› have "(Ψ, ⦇νx⦈(P ∥ Q), P ∥ ⦇νx⦈Q) ∈ ?X"
    proof -
      from ‹x ♯ Ψ› ‹x ♯ P› have "(Ψ, ⦇νx⦈(P ∥ Q), P ∥ ⦇νx⦈Q) ∈ ?X1"
        by (smt (verit, del_insts) mem_Collect_eq freshSets(1) freshSets(5) resChain.base resChain.step)
      then show ?thesis by auto
    qed
    moreover have "eqvt ?X"
      by (rule eqvtUnion) (clarsimp simp add: eqvt_def eqvts, metis fresh_star_bij(2))+
    ultimately have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ∼ P ∥ ⦇νx⦈Q"
    proof(coinduct rule: transitiveStarCoinduct)
      case(cStatEq Ψ R T)
      then have "(Ψ, R, T) ∈ ?X1 ∨ (Ψ, R, T) ∈ ?X2"
        by blast
      then show ?case
      proof(rule disjE)
        assume "(Ψ, R, T) ∈ ?X1"
        then obtain xvec yvec P Q where "R = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and "T = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
          by auto
        moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "yvec ♯* A⇩P" and "A⇩P ♯* Q"
          by(rule freshFrame[where C="(Ψ, yvec, Q)"]) auto
        moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "yvec ♯* A⇩Q" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P"
          by(rule freshFrame[where C="(Ψ, yvec, A⇩P, Ψ⇩P)"]) auto
        moreover from FrQ ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
          by(auto dest: extractFrameFreshChain)
        moreover from ‹yvec ♯* P› ‹yvec ♯* A⇩P› FrP have "yvec ♯* Ψ⇩P"
          by(drule_tac extractFrameFreshChain) auto
        ultimately show ?case
          by(auto simp add: frameChainAppend[symmetric] freshChainAppend) (auto simp add: frameChainAppend intro: frameResChainPres frameResChainComm)
      next
        assume "(Ψ, R, T) ∈ ?X2"
        then obtain xvec yvec P Q where "T = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and "R = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
          by auto
        moreover obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "yvec ♯* A⇩P" and "A⇩P ♯* Q"
          by(rule freshFrame[where C="(Ψ, yvec, Q)"]) auto
        moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "yvec ♯* A⇩Q" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P"
          by(rule freshFrame[where C="(Ψ, yvec, A⇩P, Ψ⇩P)"]) auto
        moreover from FrQ ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
          by(auto dest: extractFrameFreshChain)
        moreover from ‹yvec ♯* P› ‹yvec ♯* A⇩P› FrP have "yvec ♯* Ψ⇩P"
          by(drule_tac extractFrameFreshChain) auto
        ultimately show ?case
          by(auto simp add: frameChainAppend[symmetric] freshChainAppend) (auto simp add: frameChainAppend intro: frameResChainPres frameResChainComm)
      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) ♯ Ψ⟧ ⟹ (Ψ, ⦇νy⦈R, ⦇νy⦈T) ∈ ?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 force
        assume "(y::name) ♯ Ψ"
        show "(Ψ, ⦇νy⦈R, ⦇νy⦈T) ∈ ?Y"
        proof(cases "(Ψ, R', T') ∈ ?X")
          assume "(Ψ, R', T') ∈ ?X"
          show ?thesis
          proof(cases "(Ψ, R', T') ∈ ?X1")
            assume "(Ψ, R', T') ∈ ?X1"
            then obtain xvec yvec P Q where R'eq: "R' = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and T'eq: "T' = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))"
              and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
              by auto
            from ‹Ψ ⊳ R ∼ R'› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈R ∼ ⦇νy⦈R'" by(rule bisimResPres)
            moreover from ‹xvec ♯* Ψ› ‹y ♯ Ψ› ‹yvec ♯* P› ‹yvec ♯* Ψ› have "(Ψ, ⦇ν*(y#xvec)⦈⦇ν*yvec⦈(P ∥ Q), ⦇ν*(y#xvec)⦈(P ∥ (⦇ν*yvec⦈Q))) ∈ ?X1"
              by(force simp del: resChain.simps)
            with R'eq T'eq have "(Ψ, ⦇νy⦈R', ⦇νy⦈T') ∈ ?X ∪ bisim" by simp
            moreover from ‹Ψ ⊳ T' ∼ T› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈T' ∼ ⦇νy⦈T" 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 yvec P Q where T'eq: "T' = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and R'eq: "R' = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
              by auto
            from ‹Ψ ⊳ R ∼ R'› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈R ∼ ⦇νy⦈R'" by(rule bisimResPres)
            moreover from ‹xvec ♯* Ψ› ‹y ♯ Ψ› ‹yvec ♯* P› ‹yvec ♯* Ψ› have "(Ψ, ⦇ν*(y#xvec)⦈(P ∥ (⦇ν*yvec⦈Q)), ⦇ν*(y#xvec)⦈(⦇ν*yvec⦈(P ∥ Q))) ∈ ?X2"
              by(force simp del: resChain.simps)
            with R'eq T'eq have "(Ψ, ⦇νy⦈R', ⦇νy⦈T') ∈ ?X ∪ bisim" by simp
            moreover from ‹Ψ ⊳ T' ∼ T› ‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈T' ∼ ⦇νy⦈T" 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
      have C1': "⋀Ψ R T y. ⟦(Ψ, R, T) ∈ ?Y⇧⋆; (y::name) ♯ Ψ⟧ ⟹ (Ψ, ⦇νy⦈R, ⦇νy⦈T) ∈ ?Y⇧⋆"
      proof -
        fix Ψ R
          and T::"('a,'b,'c) psi"
          and y::name
        assume "(Ψ, R, T) ∈ ?Y⇧⋆"
          and  "y ♯ Ψ"
        then show "(Ψ, ⦇νy⦈R, ⦇νy⦈T) ∈ ?Y⇧⋆"
        proof(induct rule: rel_trancl.induct)
          case(r_into_rel_trancl Ψ P Q)
          then show ?case
            by (intro rel_trancl.intros(1)) (rule C1)
        next
          case(rel_trancl_into_rel_trancl Ψ P Q R)
          then show ?case
            using rel_trancl.intros(2) C1 by meson
        qed
      qed
      have C1'': "⋀Ψ R T yvec. ⟦(Ψ, R, T) ∈ ?Y⇧⋆; (yvec::name list) ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*yvec⦈R, ⦇ν*yvec⦈T) ∈ ?Y⇧⋆"
      proof -
        fix Ψ R T
          and yvec::"name list"
        assume "(Ψ, R, T) ∈ ?Y⇧⋆"
          and  "yvec ♯* Ψ"
        then show "(Ψ, ⦇ν*yvec⦈R, ⦇ν*yvec⦈T) ∈ ?Y⇧⋆"
          apply(induct yvec)
           apply simp
          unfolding resChain.simps
          by(rule C1') simp+
      qed
      have C2: "⋀y Ψ' R S zvec. ⟦y ♯ Ψ'; y ♯ R; zvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇νy⦈(⦇ν*zvec⦈(R ∥ S)), ⦇ν*zvec⦈(R ∥ ⦇νy⦈S)) ∈ ?Y⇧⋆"
      proof -
        fix   y::name
          and Ψ::'b
          and R::"('a,'b,'c) psi"
          and S::"('a,'b,'c) psi"
          and zvec::"name list"
        assume "y ♯ Ψ"
          and  "y ♯ R"
          and  "zvec ♯* Ψ"
        have "Ψ ⊳ ⦇νy⦈(⦇ν*zvec⦈(R ∥ S)) ∼ (⦇ν*zvec⦈(⦇νy⦈(R ∥ S)))"
          by(rule bisimResComm') fact+
        moreover have "(Ψ, (⦇ν*zvec⦈(⦇νy⦈(R ∥ S))), ⦇ν*zvec⦈(R ∥ ⦇νy⦈S)) ∈ ?X" using ‹y ♯ Ψ› ‹y ♯ R› ‹zvec ♯* Ψ›
          apply clarsimp
          apply(rule exI[where x=zvec])
          apply(rule exI[where x="[y]"])
          by auto
        moreover have "Ψ ⊳ ⦇ν*zvec⦈(R ∥ ⦇νy⦈S) ∼ ⦇ν*zvec⦈(R ∥ ⦇νy⦈S)"
          by(rule bisimReflexive)
        ultimately show "(Ψ, ⦇νy⦈(⦇ν*zvec⦈(R ∥ S)), ⦇ν*zvec⦈(R ∥ ⦇νy⦈S)) ∈ ?Y⇧⋆"
          by blast
      qed
      have C2': "⋀y Ψ' R S zvec. ⟦y ♯ Ψ'; y ♯ R; zvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*zvec⦈(R ∥ ⦇νy⦈S), ⦇νy⦈(⦇ν*zvec⦈(R ∥ S))) ∈ ?Y⇧⋆"
      proof -
        fix   y::name
          and Ψ::'b
          and R::"('a,'b,'c) psi"
          and S::"('a,'b,'c) psi"
          and zvec::"name list"
        assume "y ♯ Ψ"
          and  "y ♯ R"
          and  "zvec ♯* Ψ"
        have "Ψ ⊳ (⦇ν*zvec⦈(⦇νy⦈(R ∥ S))) ∼ ⦇νy⦈(⦇ν*zvec⦈(R ∥ S))"
          by(rule bisimSymmetric[OF bisimResComm']) fact+
        moreover have "(Ψ, ⦇ν*zvec⦈(R ∥ ⦇νy⦈S), (⦇ν*zvec⦈(⦇νy⦈(R ∥ S)))) ∈ ?X" using ‹y ♯ Ψ› ‹y ♯ R› ‹zvec ♯* Ψ›
          apply(intro UnI2)
          apply clarsimp
          apply(rule exI[where x=zvec])
          apply(rule exI[where x="[y]"])
          by auto
        moreover have "Ψ ⊳ ⦇ν*zvec⦈(R ∥ ⦇νy⦈S) ∼ ⦇ν*zvec⦈(R ∥ ⦇νy⦈S)"
          by(rule bisimReflexive)
        ultimately show "(Ψ, ⦇ν*zvec⦈(R ∥ ⦇νy⦈S), ⦇νy⦈(⦇ν*zvec⦈(R ∥ S))) ∈ ?Y⇧⋆"
          by blast
      qed
      have C3: "⋀Ψ' zvec R y. ⟦y ♯ Ψ'; zvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇νy⦈(⦇ν*zvec⦈R), ⦇ν*zvec⦈(⦇νy⦈R)) ∈ ?Y⇧⋆"
      proof -
        fix   y::name
          and Ψ::'b
          and R::"('a,'b,'c) psi"
          and zvec::"name list"
        assume "y ♯ Ψ"
          and  "zvec ♯* Ψ"
        then have "Ψ ⊳ ⦇νy⦈(⦇ν*zvec⦈R) ∼ ⦇ν*zvec⦈(⦇νy⦈R)"
          by(rule bisimResComm')
        then show "(Ψ, ⦇νy⦈(⦇ν*zvec⦈R), ⦇ν*zvec⦈(⦇νy⦈R)) ∈ ?Y⇧⋆"
          by(blast intro: bisimReflexive)
      qed
      have C4: "⋀Ψ' R S zvec. ⟦zvec ♯* R; zvec ♯* Ψ'⟧ ⟹ (Ψ', (⦇ν*zvec⦈(R ∥ S)), (R ∥ (⦇ν*zvec⦈S))) ∈ ?Y⇧⋆"
      proof -
        fix   Ψ::'b
          and R::"('a,'b,'c) psi"
          and S::"('a,'b,'c) psi"
          and zvec::"name list"
        assume "zvec ♯* R"
          and  "zvec ♯* Ψ"
        then have "(Ψ, (⦇ν*zvec⦈(R ∥ S)), (R ∥ (⦇ν*zvec⦈S))) ∈ ?X"
          apply clarsimp
          apply(rule exI[where x="[]"])
          apply(rule exI[where x=zvec])
          by auto
        then show "(Ψ, (⦇ν*zvec⦈(R ∥ S)), (R ∥ (⦇ν*zvec⦈S))) ∈ ?Y⇧⋆"
          by(blast intro: bisimReflexive)
      qed
      have C4': "⋀Ψ' R S zvec. ⟦zvec ♯* R; zvec ♯* Ψ'⟧ ⟹ (Ψ', (R ∥ (⦇ν*zvec⦈S)), (⦇ν*zvec⦈(R ∥ S))) ∈ ?Y⇧⋆"
      proof -
        fix   Ψ::'b
          and R::"('a,'b,'c) psi"
          and S::"('a,'b,'c) psi"
          and zvec::"name list"
        assume "zvec ♯* R"
          and  "zvec ♯* Ψ"
        then have "(Ψ, (R ∥ (⦇ν*zvec⦈S)), (⦇ν*zvec⦈(R ∥ S))) ∈ ?X"
          apply(intro UnI2)
          apply clarsimp
          apply(rule exI[where x="[]"])
          apply(rule exI[where x=zvec])
          by auto
        then show "(Ψ, (R ∥ (⦇ν*zvec⦈S)), (⦇ν*zvec⦈(R ∥ S))) ∈ ?Y⇧⋆"
          by(blast intro: bisimReflexive)
      qed
      {
        fix Ψ P Q R
        assume "Ψ ⊳ P ↝[?Y⇧⋆] Q"
          and  "Ψ ⊳ Q ↝[?Y⇧⋆] R"
        moreover note rel_trancl_eqvt[OF ‹eqvt ?Y›]
        moreover have "{(Ψ, P, R) | Ψ P R. ∃Q. (Ψ, P, Q) ∈ ?Y⇧⋆ ∧ (Ψ, Q, R) ∈ ?Y⇧⋆} ⊆ ?Y⇧⋆"
          by(auto intro: rel_trancl_transitive)
        ultimately have  "Ψ ⊳ P ↝[?Y⇧⋆] R"
          by(rule transitive)
      }
      note trans = this

      show ?case
      proof(cases "(Ψ, R, T) ∈ ?X1")
        assume "(Ψ, R, T) ∈ ?X1"
        then obtain xvec yvec P Q where Req: "R = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and Teq: "T = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
          by auto
        have "Ψ ⊳ ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q)) ↝[?Y⇧⋆] ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))"
        proof -
          have "Ψ ⊳ ⦇ν*yvec⦈(P ∥ Q) ↝[?Y⇧⋆] P ∥ (⦇ν*yvec⦈Q)" using ‹yvec ♯* Ψ› ‹yvec ♯* P›
          proof(induct yvec arbitrary: Q)
            case Nil show ?case
              unfolding resChain.simps
              by(rule monotonic[where A="?Y"]) (blast intro: reflexive bisimReflexive)+
          next
            case(Cons y yvec)
            then have "yvec ♯* P" and "yvec ♯* Ψ" and "y ♯ Ψ" and "y ♯ P"
              by simp+
            have "Ψ ⊳ ⦇ν*(y#yvec)⦈P ∥ Q ↝[?Y⇧⋆] ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q))"
            proof -
              have "Ψ ⊳ ⦇ν*(y#yvec)⦈P ∥ Q ↝[bisim] ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q))"
                unfolding resChain.simps
                apply(rule bisimE)
                apply(rule bisimResComm')
                by fact+
              then have "Ψ ⊳ ⦇ν*(y#yvec)⦈P ∥ Q ↝[?Y] ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q))"
                apply -
                apply(drule monotonic[where B="?Y"])
                by auto (blast intro: bisimTransitive bisimReflexive)
              then show ?thesis
                apply -
                apply(drule monotonic[where B="?Y⇧⋆"])
                by blast
            qed
            moreover have "Ψ ⊳ ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q)) ↝[?Y⇧⋆] ⦇ν*yvec⦈(P ∥ ⦇νy⦈Q)"
            proof -
              have "Ψ ⊳ ⦇νy⦈(P ∥ Q) ↝[?Y⇧⋆] P ∥ ⦇νy⦈Q"
                apply(rule scopeExtLeft)
                      apply fact
                     apply fact
                    apply(rule rel_trancl_eqvt)
                    apply fact
                   apply(blast intro: bisimReflexive)
                by fact+
              then show ?thesis using ‹yvec ♯* Ψ›
              proof(induct yvec)
                case Nil then show ?case by simp
              next
                case(Cons y' yvec)
                then show ?case
                  unfolding resChain.simps
                  apply -
                  apply(rule resPres[where Rel="?Y⇧⋆" and Rel'="?Y⇧⋆"])
                      apply simp
                     apply(rule rel_trancl_eqvt[OF ‹eqvt ?Y›])
                    apply simp
                   apply simp
                  by(rule C1'')
              qed
            qed
            moreover have "Ψ ⊳ ⦇ν*yvec⦈(P ∥ ⦇νy⦈Q) ↝[?Y⇧⋆] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
              by(rule Cons) fact+
            moreover have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[?Y⇧⋆] P ∥ (⦇ν*(y#yvec)⦈Q)"
            proof -
              have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[bisim] P ∥ (⦇ν*(y#yvec)⦈Q)"
                unfolding resChain.simps
                apply(rule bisimE)
                apply(rule bisimParPresSym)
                apply(rule bisimSymmetric[OF bisimResComm'])
                by fact+
              then have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[?Y] P ∥ (⦇ν*(y#yvec)⦈Q)"
                apply -
                apply(drule monotonic[where B="?Y"])
                by auto (blast intro: bisimTransitive bisimReflexive)
              then show ?thesis
                apply -
                apply(drule monotonic[where B="?Y⇧⋆"])
                by blast
            qed
            moreover have "Ψ ⊳ ⦇ν*yvec⦈P ∥ ⦇νy⦈Q ↝[?Y⇧⋆] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
              by(rule Cons) fact+
            moreover have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[?Y⇧⋆] P ∥ (⦇ν*(y#yvec)⦈Q)"
            proof -
              have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[bisim] P ∥ (⦇νy⦈(⦇ν*yvec⦈Q))"
                apply(rule bisimE)
                apply(rule bisimParPresSym)
                apply(rule bisimSymmetric[OF bisimResComm'])
                by fact+
              then have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[?Y] P ∥ (⦇νy⦈(⦇ν*yvec⦈Q))"
                apply -
                apply(drule monotonic[where B="?Y"])
                by auto (blast intro: bisimTransitive bisimReflexive)
              then show ?thesis
                unfolding resChain.simps
                apply -
                apply(drule monotonic[where B="?Y⇧⋆"])
                by blast
            qed
            ultimately show ?case
              by(blast dest: trans)
          qed
          then show ?thesis using ‹xvec ♯* Ψ›
            apply(induct xvec)
             apply simp
            unfolding resChain.simps
            apply(rule resPres)
                apply simp
               apply(rule rel_trancl_eqvt[OF ‹eqvt ?Y›])
              apply simp
             apply simp
            apply(rule C1'')
             apply simp
            by assumption
        qed
        then show ?case unfolding Req Teq
          by -
      next
        assume "(Ψ, R, T) ∉ ?X1"
        then have "(Ψ, R, T) ∈ ?X2" using ‹(Ψ, R, T) ∈ ?X› by blast
        then obtain xvec yvec P Q where Teq: "T = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and Req: "R = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
          by auto
        have "Ψ ⊳ ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q)) ↝[?Y⇧⋆] ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))"
        proof -
          have "Ψ ⊳ P ∥ (⦇ν*yvec⦈Q) ↝[?Y⇧⋆] ⦇ν*yvec⦈(P ∥ Q)" using ‹yvec ♯* P› ‹yvec ♯* Ψ›
          proof(induct yvec arbitrary: Q)
            case Nil show ?case
              unfolding resChain.simps
              by(rule monotonic[where A="?Y"]) (blast intro: reflexive bisimReflexive)+
          next
            case(Cons y yvec)
            then have "yvec ♯* P" and "yvec ♯* Ψ" and "y ♯ Ψ" and "y ♯ P"
              by simp+
            have "Ψ ⊳ ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q)) ↝[?Y⇧⋆] ⦇ν*(y#yvec)⦈P ∥ Q"
            proof -
              have "Ψ ⊳ ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q)) ↝[bisim] ⦇ν*(y#yvec)⦈P ∥ Q"
                unfolding resChain.simps
                apply(rule bisimE)
                apply(rule bisimSymmetric[OF bisimResComm'])
                by fact+
              then have "Ψ ⊳ ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q)) ↝[?Y] ⦇ν*(y#yvec)⦈P ∥ Q"
                apply -
                apply(drule monotonic[where B="?Y"])
                by auto (blast intro: bisimTransitive bisimReflexive)
              then show ?thesis
                apply -
                apply(drule monotonic[where B="?Y⇧⋆"])
                by blast
            qed
            moreover have "Ψ ⊳ ⦇ν*yvec⦈(P ∥ ⦇νy⦈Q) ↝[?Y⇧⋆] ⦇ν*yvec⦈(⦇νy⦈(P ∥ Q))"
            proof -
              have "Ψ ⊳ P ∥ ⦇νy⦈Q ↝[?Y⇧⋆] ⦇νy⦈(P ∥ Q)"
                apply(rule scopeExtRight)
                     apply fact
                    apply fact
                   apply(rule rel_trancl_eqvt)
                   apply fact
                  apply(blast intro: bisimReflexive)
                by fact+
              then show ?thesis using ‹yvec ♯* Ψ›
              proof(induct yvec)
                case Nil then show ?case by simp
              next
                case(Cons y' yvec)
                then show ?case
                  unfolding resChain.simps
                  apply -
                  apply(rule resPres[where Rel="?Y⇧⋆" and Rel'="?Y⇧⋆"])
                      apply simp
                     apply(rule rel_trancl_eqvt[OF ‹eqvt ?Y›])
                    apply simp
                   apply simp
                  by(rule C1'')
              qed
              moreover have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[?Y⇧⋆] ⦇ν*yvec⦈(P ∥ ⦇νy⦈Q)"
                by(rule Cons) fact+
              moreover have "Ψ ⊳ P ∥ (⦇ν*(y#yvec)⦈Q) ↝[?Y⇧⋆] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
              proof -
                have "Ψ ⊳ P ∥ (⦇ν*(y#yvec)⦈Q) ↝[bisim] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
                  unfolding resChain.simps
                  apply(rule bisimE)
                  apply(rule bisimParPresSym)
                  apply(rule bisimResComm')
                  by fact+
                then have "Ψ ⊳ P ∥ (⦇ν*(y#yvec)⦈Q) ↝[?Y] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
                  apply -
                  apply(drule monotonic[where B="?Y"])
                  by auto (blast intro: bisimTransitive bisimReflexive)
                then show ?thesis
                  apply -
                  apply(drule monotonic[where B="?Y⇧⋆"])
                  by blast
              qed
            qed
            moreover have "Ψ ⊳ P ∥ (⦇ν*yvec⦈(⦇νy⦈Q)) ↝[?Y⇧⋆] ⦇ν*yvec⦈P ∥ ⦇νy⦈Q"
              by(rule Cons) fact+
            moreover have "Ψ ⊳ P ∥ (⦇ν*(y#yvec)⦈Q) ↝[?Y⇧⋆] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
            proof -
              have "Ψ ⊳ P ∥ (⦇νy⦈(⦇ν*yvec⦈Q)) ↝[bisim] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
                apply(rule bisimE)
                apply(rule bisimParPresSym)
                apply(rule bisimResComm')
                by fact+
              then have "Ψ ⊳ P ∥ (⦇νy⦈(⦇ν*yvec⦈Q)) ↝[?Y] P ∥ (⦇ν*yvec⦈(⦇νy⦈Q))"
                apply -
                apply(drule monotonic[where B="?Y"])
                by auto (blast intro: bisimTransitive bisimReflexive)
              then show ?thesis
                unfolding resChain.simps
                apply -
                apply(drule monotonic[where B="?Y⇧⋆"])
                by blast
            qed
            ultimately show ?case
              by(blast dest: trans)
          qed
          then show ?thesis using ‹xvec ♯* Ψ›
            apply(induct xvec)
             apply simp
            unfolding resChain.simps
            apply(rule resPres)
                apply simp
               apply(rule rel_trancl_eqvt[OF ‹eqvt ?Y›])
              apply simp
             apply simp
            apply(rule C1'')
             apply simp
            by assumption
        qed
        then show ?case unfolding Req Teq
          by -
      qed
    next
      case(cExt Ψ R T Ψ')
      show ?case
      proof(cases "(Ψ, R, T) ∈ ?X1")
        assume "(Ψ, R, T) ∈ ?X1"
        then obtain xvec yvec P Q where Req: "R = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and Teq: "T = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
          by auto
        obtain p where "(p ∙ yvec) ♯* Ψ" and "(p ∙ yvec) ♯* P" and "(p ∙ yvec) ♯* Q" and "(p ∙ yvec) ♯* Ψ'" and "(p ∙ yvec) ♯* xvec"
          and S: "(set p) ⊆ (set yvec) × (set(p ∙ yvec))" and "distinctPerm p"
          by(rule name_list_avoiding[where c="(Ψ, P, Q, xvec, Ψ')"]) auto
        obtain q where "(q ∙ xvec) ♯* Ψ" and "(q ∙ xvec) ♯* Ψ'" and "(q ∙ xvec) ♯* P"  and "(q ∙ xvec) ♯* yvec" and "(q ∙ xvec) ♯* Q" and "(q ∙ xvec) ♯* (p∙P)" and "(q ∙ xvec) ♯* (p∙Q)" and "distinctPerm q" and T: "(set q) ⊆ (set xvec) × (set(q∙xvec))" and "(q ∙ xvec) ♯* (p∙yvec)"
          by(rule name_list_avoiding[where c="(Ψ, P, Q, yvec, p∙yvec, Ψ',p∙P,p∙Q)"]) auto
        note ‹(p ∙ yvec) ♯* Q› ‹set p ⊆ set yvec × set (p ∙ yvec)›
        moreover have "(p ∙ yvec) ♯* (P ∥ Q)" using ‹(p ∙ yvec) ♯* Q› ‹(p ∙ yvec) ♯* P›
          by simp
        moreover have "(Ψ ⊗ Ψ', ⦇ν*xvec⦈⦇ν*p ∙ yvec⦈p ∙ P ∥ Q, ⦇ν*xvec⦈P ∥ (⦇ν*p ∙ yvec⦈p ∙ Q)) ∈ ?X"
        proof -
          have Pdef: "(p ∙ P) = P" using ‹set p ⊆ set yvec × set(p∙yvec)› ‹yvec ♯* P› ‹(p∙yvec) ♯* P›
            by simp
          have yvecdef: "(q ∙ p ∙ yvec) = (p∙ yvec)" using ‹set q ⊆ set xvec × set(q∙xvec)› ‹(p∙yvec) ♯* xvec› ‹(q∙xvec) ♯* (p∙yvec)›
            by simp
          have "(q ∙ xvec) ♯* (P ∥ (⦇ν*p ∙ yvec⦈p ∙ Q))" using ‹(q ∙ xvec) ♯* P› ‹(q ∙ xvec) ♯* (p∙Q)› ‹(q ∙ xvec) ♯* (p∙yvec)›
            by simp
          moreover have "(q ∙ xvec) ♯* (⦇ν*p ∙ yvec⦈p ∙ P ∥ Q)"
            unfolding eqvts Pdef
            using ‹(q ∙ xvec) ♯* P› ‹(q ∙ xvec) ♯* (p∙Q)› ‹(q ∙ xvec) ♯* (p∙yvec)›
            by simp
          moreover note ‹set q ⊆ set xvec × set (q ∙ xvec)›
          moreover have "(Ψ ⊗ Ψ', ⦇ν*q ∙ xvec⦈q ∙ ⦇ν*p ∙ yvec⦈p ∙ P ∥ Q,
            ⦇ν*q ∙ xvec⦈q ∙ P ∥ (⦇ν*p ∙ yvec⦈p ∙ Q)) ∈ ?X"
          proof -
            have "(p∙yvec) ♯* (Ψ⊗Ψ')" using ‹(p∙yvec) ♯* Ψ› ‹(p∙yvec) ♯* Ψ'›
              by auto
            moreover have "(p∙yvec) ♯* (q∙P)" using ‹(p∙yvec) ♯* P›
              apply(subst yvecdef[symmetric])
              by(subst fresh_star_bij)
            moreover have "(q∙xvec) ♯* (Ψ⊗Ψ')" using ‹(q∙xvec) ♯* Ψ› ‹(q∙xvec) ♯* Ψ'›
              by auto
            ultimately show ?thesis
              unfolding Pdef eqvts yvecdef
              by blast
          qed
          ultimately show ?thesis
            by(subst (1 2) resChainAlpha[where p=q and xvec=xvec])
        qed
        ultimately show ?case unfolding Req Teq
          apply(intro disjI1)
          by(subst (1 2) resChainAlpha[where p=p and xvec=yvec])
      next
        assume "(Ψ, R, T) ∉ ?X1"
        then have "(Ψ, R, T) ∈ ?X2" using ‹(Ψ,R,T) ∈ ?X›
          by blast
        then obtain xvec yvec P Q where Teq: "T = ⦇ν*xvec⦈(⦇ν*yvec⦈(P ∥ Q))" and Req: "R = ⦇ν*xvec⦈(P ∥ (⦇ν*yvec⦈Q))" and "xvec ♯* Ψ" and "yvec ♯* P" and "yvec ♯* Ψ"
          by auto
        obtain p where "(p ∙ yvec) ♯* Ψ" and "(p ∙ yvec) ♯* P" and "(p ∙ yvec) ♯* Q" and "(p ∙ yvec) ♯* Ψ'" and "(p ∙ yvec) ♯* xvec"
          and S: "(set p) ⊆ (set yvec) × (set(p ∙ yvec))" and "distinctPerm p"
          by(rule name_list_avoiding[where c="(Ψ, P, Q, xvec, Ψ')"]) auto
        obtain q where "(q ∙ xvec) ♯* Ψ" and "(q ∙ xvec) ♯* Ψ'" and "(q ∙ xvec) ♯* P"  and "(q ∙ xvec) ♯* yvec" and "(q ∙ xvec) ♯* Q" and "(q ∙ xvec) ♯* (p∙P)" and "(q ∙ xvec) ♯* (p∙Q)" and "distinctPerm q" and T: "(set q) ⊆ (set xvec) × (set(q∙xvec))" and "(q ∙ xvec) ♯* (p∙yvec)"
          by(rule name_list_avoiding[where c="(Ψ, P, Q, yvec, p∙yvec, Ψ',p∙P,p∙Q)"]) auto
        note ‹(p ∙ yvec) ♯* Q› ‹set p ⊆ set yvec × set (p ∙ yvec)›
        moreover have "(p ∙ yvec) ♯* (P ∥ Q)" using ‹(p ∙ yvec) ♯* Q› ‹(p ∙ yvec) ♯* P›
          by simp
        moreover have "(Ψ ⊗ Ψ', ⦇ν*xvec⦈P ∥ (⦇ν*p ∙ yvec⦈p ∙ Q), ⦇ν*xvec⦈⦇ν*p ∙ yvec⦈p ∙ P ∥ Q) ∈ ?X"
        proof -
          have Pdef: "(p ∙ P) = P" using ‹set p ⊆ set yvec × set(p∙yvec)› ‹yvec ♯* P› ‹(p∙yvec) ♯* P›
            by simp
          have yvecdef: "(q ∙ p ∙ yvec) = (p∙ yvec)" using ‹set q ⊆ set xvec × set(q∙xvec)› ‹(p∙yvec) ♯* xvec› ‹(q∙xvec) ♯* (p∙yvec)›
            by simp
          have "(q ∙ xvec) ♯* (P ∥ (⦇ν*p ∙ yvec⦈p ∙ Q))" using ‹(q ∙ xvec) ♯* P› ‹(q ∙ xvec) ♯* (p∙Q)› ‹(q ∙ xvec) ♯* (p∙yvec)›
            by simp
          moreover have "(q ∙ xvec) ♯* (⦇ν*p ∙ yvec⦈p ∙ P ∥ Q)"
            unfolding eqvts Pdef
            using ‹(q ∙ xvec) ♯* P› ‹(q ∙ xvec) ♯* (p∙Q)› ‹(q ∙ xvec) ♯* (p∙yvec)›
            by simp
          moreover note ‹set q ⊆ set xvec × set (q ∙ xvec)›
          moreover have "(Ψ ⊗ Ψ', ⦇ν*q ∙ xvec⦈q ∙ P ∥ (⦇ν*p ∙ yvec⦈p ∙ Q), ⦇ν*q ∙ xvec⦈q ∙ ⦇ν*p ∙ yvec⦈p ∙ P ∥ Q) ∈ ?X"
          proof -
            have "(p∙yvec) ♯* (Ψ⊗Ψ')" using ‹(p∙yvec) ♯* Ψ› ‹(p∙yvec) ♯* Ψ'›
              by auto
            moreover have "(p∙yvec) ♯* (q∙P)" using ‹(p∙yvec) ♯* P›
              apply(subst yvecdef[symmetric])
              by(subst fresh_star_bij)
            moreover have "(q∙xvec) ♯* (Ψ⊗Ψ')" using ‹(q∙xvec) ♯* Ψ› ‹(q∙xvec) ♯* Ψ'›
              by auto
            ultimately show ?thesis
              unfolding Pdef eqvts yvecdef
              by blast
          qed
          ultimately show ?thesis
            by(subst (1 2) resChainAlpha[where p=q and xvec=xvec])
        qed
        ultimately show ?case unfolding Req Teq
          apply(intro disjI1)
          by(subst (1 2) resChainAlpha[where p=p and xvec=yvec])
      qed
    next
      case(cSym Ψ P Q)
      then show ?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
  then show ?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 ∥ (⦇ν*xvec⦈Q)"
  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(clarsimp, rule exI[where x="[]"]) 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 A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" and "A⇩P ♯* Q" and "A⇩P ♯* R"
      by(rule freshFrame[where C="(Ψ, Q, R)"]) auto
    moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* A⇩P" and "A⇩Q ♯* Ψ⇩P" and "A⇩Q ♯* R"
      by(rule freshFrame[where C="(Ψ, A⇩P, Ψ⇩P, R)"]) auto
    moreover obtain A⇩R Ψ⇩R where FrR: "extractFrame R = ⟨A⇩R, Ψ⇩R⟩" and "A⇩R ♯* Ψ" and "A⇩R ♯* A⇩P" and "A⇩R ♯* Ψ⇩P" and "A⇩R ♯* A⇩Q" and "A⇩R ♯* Ψ⇩Q"
      by(rule freshFrame[where C="(Ψ, A⇩P, Ψ⇩P, A⇩Q, Ψ⇩Q)"]) auto
    moreover from FrQ ‹A⇩P ♯* Q› ‹A⇩Q ♯* A⇩P› have "A⇩P ♯* Ψ⇩Q"
      by(auto dest: extractFrameFreshChain)
    moreover from FrR ‹A⇩P ♯* R› ‹A⇩R ♯* A⇩P› have "A⇩P ♯* Ψ⇩R"
      by(auto dest: extractFrameFreshChain)
    moreover from FrR ‹A⇩Q ♯* R› ‹A⇩R ♯* A⇩Q› have "A⇩Q ♯* Ψ⇩R"
      by(auto dest: extractFrameFreshChain)
    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 ?X›have "eqvt ?Y" by blast
    have C1: "⋀Ψ T S yvec. ⟦(Ψ, T, S) ∈ ?Y; yvec ♯* Ψ⟧ ⟹ (Ψ, ⦇ν*yvec⦈T, ⦇ν*yvec⦈S) ∈ ?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 force
      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 "Ψ ⊳ ⦇ν*yvec⦈T ∼ ⦇ν*yvec⦈T'" 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 "(Ψ, ⦇ν*yvec⦈T', ⦇ν*yvec⦈S') ∈ ?X" by(simp add: resChainAppend)
      moreover from ‹Ψ ⊳ S' ∼ S› ‹yvec ♯* Ψ› have "Ψ ⊳ ⦇ν*yvec⦈S' ∼ ⦇ν*yvec⦈S" by(rule bisimResChainPres)
      ultimately show "(Ψ, ⦇ν*yvec⦈T, ⦇ν*yvec⦈S) ∈ ?Y" by blast
    qed

    {
      fix y
      have "⋀Ψ T S. ⟦(Ψ, T, S) ∈ ?Y; y ♯ Ψ⟧ ⟹ (Ψ, ⦇νy⦈T, ⦇νy⦈S) ∈ ?Y"
        by(drule C1[where yvec2="[y]"]) auto
    }
    note C2 = this

    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(clarsimp, rule exI[where x="[]"]) auto
          then show "(Ψ, (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)
          then have "Ψ ⊳ 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
      then show ?thesis using ‹eqvt ?Y› ‹xvec ♯* Ψ› C1
        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 name_list_avoiding[where c="(Ψ, P, Q, R, Ψ')"]) 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 clarsimp 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 clarsimp 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
  then show ?thesis
  proof(coinduct rule: bisimWeakCoinduct)
    case(cStatEq Ψ Q R)
    show ?case
    proof(cases "(Ψ, Q, R) ∈ ?X1")
      assume "(Ψ, Q, R) ∈ ?X1"
      then obtain P where "Q = P ∥ 𝟬" and "R = P" by auto
      moreover obtain A⇩P Ψ⇩P where "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ"
        by(rule freshFrame)
      ultimately show ?case
        apply clarsimp 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 A⇩P Ψ⇩P where "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ"
        by(rule freshFrame)
      ultimately show ?case
        apply clarsimp by(metis frameResChainPres frameNilStatEq Identity Associativity AssertionStatEqTrans AssertionStatEqSym Commutativity)
    qed
  next
    case(cSim Ψ Q R)
    then show ?case using ‹eqvt ?X›
      by(auto intro: parNilLeft parNilRight)
  next
    case(cExt Ψ Q R Ψ')
    then show ?case by auto
  next
    case(cSym Ψ Q R)
    then show ?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
      then show ?thesis
      proof(coinduct rule: bisimWeakCoinduct)
        case(cStatEq Ψ P Q)
        then show ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
      next
        case(cSim Ψ P Q)
        then show ?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(cases "(Ψ, 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)
        then show ?case by auto
      qed
    qed
  }
  moreover obtain y::name where "y ♯ Ψ" by(generate_fresh "name") auto
  ultimately have "Ψ ⊳ ⦇νy⦈𝟬 ∼ 𝟬" by auto
  then show ?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⦈(M⟨N⟩.P) ∼ M⟨N⟩.⦇νx⦈P"
proof -
  {
    fix x::name and P::"('a, 'b, 'c) psi"
    assume "x ♯ Ψ" and "x ♯ M" and "x ♯ N"
    let ?X1 = "{(Ψ, ⦇νx⦈(M⟨N⟩.P), M⟨N⟩.⦇νx⦈P) | Ψ x M N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ N}"
    let ?X2 = "{(Ψ, M⟨N⟩.⦇νx⦈P, ⦇νx⦈(M⟨N⟩.P)) | Ψ x M N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ N}"
    let ?X = "?X1 ∪ ?X2"

    have "eqvt ?X"
      by(rule 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⦈(M⟨N⟩.P), M⟨N⟩.⦇νx⦈P) ∈ ?X"
      by auto
    then have "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ∼ M⟨N⟩.⦇νx⦈P"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ Q R)
      then show ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
    next
      case(cSim Ψ Q R)
      then show ?case using ‹eqvt ?X›
        by(auto intro!: outputPushResLeft outputPushResRight bisimReflexive)
    next
      case(cExt Ψ Q R Ψ')
      show ?case
      proof(cases "(Ψ, Q, R) ∈ ?X1")
        assume "(Ψ, Q, R) ∈ ?X1"
        then obtain x M N P where Qeq: "Q = ⦇νx⦈(M⟨N⟩.P)" and Req: "R = M⟨N⟩.⦇νx⦈P" 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 then have "(Ψ ⊗ Ψ', ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P)), M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by auto
        moreover from Qeq ‹x ♯ M› ‹y ♯ M› ‹x ♯ N› ‹y ♯ N› ‹y ♯ P› have "Q = ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P))"
          apply clarsimp by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Req ‹y ♯ P› have "R = M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)"
          apply clarsimp 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⦈(M⟨N⟩.P)" and Qeq: "Q = M⟨N⟩.⦇νx⦈P" 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 then have "(Ψ ⊗ Ψ', ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P)), M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by auto
        moreover from Req ‹x ♯ M› ‹y ♯ M› ‹x ♯ N› ‹y ♯ N› ‹y ♯ P› have "R = ⦇νy⦈(M⟨N⟩.([(x, y)] ∙ P))"
          apply clarsimp by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Qeq ‹y ♯ P› have "Q = M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)"
          apply clarsimp by(subst alphaRes[of y]) (auto simp add: eqvts)
        ultimately show ?case by blast
      qed
    next
      case(cSym Ψ R Q)
      then show ?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⦈(M⟨N⟩.([(x, y)] ∙ P)) ∼ M⟨N⟩.⦇νy⦈([(x, y)] ∙ P)" by auto
  then show ?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="M⟨N⟩.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⦈.⦇νx⦈P"
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⦈.⦇νx⦈P) | Ψ x M xvec N P. x ♯ Ψ ∧ x ♯ M ∧ x ♯ xvec ∧ x ♯ N}"
    let ?X2 = "{(Ψ, M⦇λ*xvec N⦈.⦇νx⦈P, ⦇ν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 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⦈.⦇νx⦈P) ∈ ?X"
      by blast
    then have "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ∼ M⦇λ*xvec N⦈.⦇νx⦈P"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ Q R)
      then show ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
    next
      case(cSim Ψ Q R)
      then show ?case using ‹eqvt ?X›
        by(auto intro!: inputPushResLeft inputPushResRight bisimReflexive)
    next
      case(cExt Ψ Q R Ψ')
      show ?case
      proof(cases "(Ψ, 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⦈.⦇νx⦈P" 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 then have "(Ψ ⊗ Ψ', ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P)), M⦇λ*xvec N⦈.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by force
        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 clarsimp 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 clarsimp 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⦈.⦇νx⦈P" 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 then have "(Ψ ⊗ Ψ', ⦇νy⦈(M⦇λ*xvec N⦈.([(x, y)] ∙ P)), M⦇λ*xvec N⦈.⦇νy⦈([(x, y)] ∙ P)) ∈ ?X" by force
        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 clarsimp 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 clarsimp by(subst alphaRes[of y]) (auto simp add: eqvts)
        ultimately show ?case by blast
      qed
    next
      case(cSym Ψ R Q)
      then show ?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
  then show ?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). (φ, ⦇νx⦈P)) 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). (φ, ⦇νx⦈P)) Cs)) | Ψ x Cs. x ♯ Ψ ∧ x ♯ (map fst Cs)}"
    let ?X2 = "{(Ψ, Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs), ⦇νx⦈(Cases Cs)) | Ψ x Cs. x ♯ Ψ ∧ x ♯ (map fst Cs)}"
    let ?X = "?X1 ∪ ?X2"

    have "eqvt ?X"
    proof
      show "eqvt ?X1"
        apply(clarsimp simp add: eqvt_def eqvts)
        apply (rule exI)
        apply (rule exI)
        apply (rule conjI)
         apply (rule refl)
        apply(perm_extend_simp)
          apply(clarsimp simp add: eqvts)
         apply (simp add: fresh_bij)
        apply(drule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
        apply(drule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
       apply(simp add: eqvts)
        apply(perm_extend_simp)
        apply(simp add: eqvts)
        done
    next
      show "eqvt ?X2"
        apply(clarsimp simp add: eqvt_def eqvts)
        apply (rule exI)
        apply (rule exI)
        apply (subst conj_commute)
        apply (rule conjI)
        apply (rule conjI)
          apply (rule refl)
         apply(perm_extend_simp)
          apply (simp add: fresh_bij)
         apply(drule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
         apply(drule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
         apply(simp add: eqvts)
         apply(perm_extend_simp)
         apply(simp add: eqvts)
        apply(perm_extend_simp)
        apply(clarsimp simp add: eqvts)
        done
    qed

    from ‹x ♯ Ψ› ‹x ♯ map fst Cs› have "(Ψ, ⦇νx⦈(Cases Cs), Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) ∈ ?X" by auto
    then have "Ψ ⊳ ⦇νx⦈(Cases Cs) ∼ Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
    proof(coinduct rule: bisimCoinduct)
      case(cStatEq Ψ Q R)
      then show ?case using freshComp by(force intro: frameResFresh FrameStatEqSym)
    next
      case(cSim Ψ Q R)
      then show ?case using ‹eqvt ?X›
        by(auto intro!: casePushResLeft casePushResRight bisimReflexive)
    next
      case(cExt Ψ Q R Ψ')
      show ?case
      proof(cases "(Ψ, Q, R) ∈ ?X1")
        assume "(Ψ, Q, R) ∈ ?X1"
        then obtain x Cs where Qeq: "Q = ⦇νx⦈(Cases Cs)" and Req: "R = Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) 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). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))) ∈ ?X"
          by auto
        moreover from Qeq ‹y ♯ Cs› have "Q = ⦇νy⦈(Cases([(x, y)] ∙ Cs))"
          apply clarsimp by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Req ‹y ♯ Cs› ‹x ♯ (map fst Cs)› have "R = Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(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). (φ, ⦇νx⦈P)) 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). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs))) ∈ ?X"
          by auto
        moreover from Req ‹y ♯ Cs› have "R = ⦇νy⦈(Cases([(x, y)] ∙ Cs))"
          apply clarsimp by(subst alphaRes[of y]) (auto simp add: eqvts)
        moreover from Qeq ‹y ♯ Cs› ‹x ♯ (map fst Cs)› have "Q = Cases(map (λ(φ, P). (φ, ⦇νy⦈P)) ([(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)
      then show ?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). (φ, ⦇νy⦈P)) ([(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). (φ, ⦇νy⦈P)) ([(x, y)] ∙ Cs)) = Cases(map (λ(φ, P). (φ, ⦇νx⦈P)) 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
  then show ?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 A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" 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)
    then have "⟨A⇩P, Ψ ⊗ SBottom'⟩ ≃⇩F ⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ SBottom'⟩"
      by(force intro: frameResChainPres)
    moreover from ‹A⇩P ♯* Ψ› have "⟨ε, Ψ ⊗ SBottom'⟩ ≃⇩F ⟨A⇩P, Ψ ⊗ SBottom'⟩"
      apply -
      by(rule FrameStatEqSym) (simp add: frameResFreshChain freshCompChain(1))
    ultimately show ?case using Eq ‹A⇩P ♯* Ψ› FrP
      by auto (blast dest: FrameStatEqTrans FrameStatEqSym)+
  next
    case(cSim Ψ Q R)
    then show ?case by(auto intro: bangExtLeft bangExtRight bisimReflexive)
  next
    case(cExt Ψ Q R)
    then show ?case by auto
  next
    case(cSym Ψ Q R)
    then show ?case by auto
  qed
qed

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) ∼ (⦇νx⦈P) ∥ 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) ∼ (⦇ν*xvec⦈P) ∥ 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 = ⟨A⇩R, Ψ⇩R⟩"
  and   "A⇩R ♯* Ψ"
  and   "A⇩R ♯* P"
  and   "A⇩R ♯* 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)
    then have "Ψ ⊳ Q ∥ !Q ⟼α ≺ (Q' ∥ !Q)"
      using ‹bn α ♯* Q› by(intro Par1) (assumption | simp)+
    then have "Ψ ⊳ !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 ⟼M⦇N⦈ ≺ P'› obtain Q' where QTrans: "Ψ ⊳ Q ⟼M⦇N⦈ ≺ Q'" and "Ψ ⊳ Q' ∼ P'"
      by(force dest: simE)
    from QTrans have "Ψ ⊗ SBottom' ⊳ Q ⟼M⦇N⦈ ≺ Q'"
      by(metis statEqTransition Identity AssertionStatEqSym)
    moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
      by(rule freshFrame[where C="(Ψ, Q, M)"]) 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 force
    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 ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* M› ‹xvec ♯* Q›
      by(intro Comm1) (assumption | simp)+
    then have "Ψ ⊳ !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 A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
      by(rule freshFrame[where C="(Ψ, Q, M)"]) auto
    note FrQ
    moreover from FrQ ‹guarded Q› have "Ψ⇩Q ≃ SBottom'"
      by(blast dest: guardedStatEq)
    from ‹Ψ ⊳ !P ⟼K⦇N⦈ ≺ P''› ‹Ψ ⊳ P ∼ Q› ‹guarded Q›
    obtain Q'' T R where QTrans': "Ψ ⊳ !Q ⟼K⦇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 cComm2
      by force
    from QTrans' ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊳ !Q ⟼K⦇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 ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* M› ‹xvec ♯* Q›
      by(intro Comm2) (assumption | simp)+
    then have "Ψ ⊳ !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
  next
    case(cBrMerge M N P' P'' Q)
    then obtain Q' T R where "Ψ ⊳ !Q ⟼ ¿M⦇N⦈ ≺ Q'" and
      p''eq: "Ψ ⊳ P'' ∼ R ∥ !P" and
      "Ψ ⊳ Q' ∼ T ∥ !Q" and "Ψ ⊳ R ∼ T" and
      "supp R ⊆ (supp P''::name set)" and
      "supp T ⊆ (supp Q'::name set)"
      by blast
    obtain Q'' where "Ψ ⊳ Q ⟼ ¿M⦇N⦈ ≺ Q''" and "Ψ ⊳ Q'' ∼ P'"
    proof -
      assume g: "(⋀Q''. ⟦Ψ ⊳ Q ⟼ ¿M⦇N⦈ ≺ Q''; Ψ ⊳ Q'' ∼ P'⟧ ⟹ thesis)"
      have "∃Q'. Ψ ⊳ Q ⟼ ¿M⦇N⦈ ≺ Q' ∧ (Ψ, Q', P') ∈ bisim"
        apply(rule simE)
           apply(rule bisimE)
           apply(rule bisimSymmetric)
        by fact+
      then show thesis
        using g by blast
    qed
    have "Ψ ⊗ 𝟭 ⊳ Q ⟼ ¿M⦇N⦈ ≺ Q''" using ‹Ψ ⊳ Q ⟼ ¿M⦇N⦈ ≺ Q''›
      by(rule statEqTransition) (rule AssertionStatEqSym[OF Identity])
    obtain A⇩Q Ψ⇩Q where "extractFrame Q = ⟨A⇩Q,Ψ⇩Q⟩" and "distinct A⇩Q" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
      by(rule freshFrame[where C="(Ψ,Q,M)"]) force
    then have "Ψ⇩Q ≃ 𝟭" using ‹guarded Q›
      by(auto dest: guardedStatEq)
    have "Ψ ⊗ Ψ⇩Q ⊳ !Q ⟼ ¿M⦇N⦈ ≺ Q'" using ‹Ψ ⊳ !Q ⟼ ¿M⦇N⦈ ≺ Q'›
      by(rule statEqTransition) (metis ‹Ψ⇩Q ≃ 𝟭› AssertionStatEqTrans AssertionStatEqSym Identity compositionSym)
    have "Ψ ⊳ !Q ⟼ ¿M⦇N⦈ ≺ Q'' ∥ Q'"
      by(rule Bang) (rule BrMerge|fact|simp)+
    moreover have "Ψ ⊳ P' ∥ P'' ∼ (P' ∥ R) ∥ (P ∥ !P)"
      apply(rule bisimTransitive[OF bisimParPresSym, OF p''eq])
      apply(rule bisimTransitive[OF bisimSymmetric, OF bisimParAssoc])
      apply(rule bisimParPresSym)
      apply(rule bangExt[OF ‹guarded P›])
      done
    moreover have "Ψ ⊳ Q'' ∥ Q' ∼ Q'' ∥ T ∥ !Q" using ‹Ψ ⊳ Q' ∼ T ∥ !Q›
      by(metis bisimTransitive bisimParAssoc bisimParComm bisimParPres bisimSymmetric)
    moreover have "Ψ ⊳ (P' ∥ R) ∼ Q'' ∥ T" using ‹Ψ ⊳ R ∼ T› and ‹Ψ ⊳ Q'' ∼ P'›
      apply -
      apply(erule bisimTransitive[OF bisimParPres, OF bisimSymmetric])
      apply(erule bisimTransitive[OF bisimParPresSym])
      by(rule bisimReflexive)
    moreover have "supp(P' ∥ R) ⊆ (supp(P'∥P'')::name set)"
      using ‹supp R ⊆ (supp P''::name set)› by(auto simp add: psi.supp)
    moreover have "supp(Q'' ∥ T) ⊆ (supp(Q'' ∥ Q')::name set)"
      using ‹supp T ⊆ (supp Q'::name set)› by(auto simp add: psi.supp)
    ultimately show ?case
      by blast
  next
    case(cBrComm1 M N P' xvec P'' Q)
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ Q ↝[bisim] P" by(metis bisimE)
    with ‹Ψ ⊳ P ⟼¿M⦇N⦈ ≺ P'› obtain Q' where QTrans: "Ψ ⊳ Q ⟼¿M⦇N⦈ ≺ Q'" and "Ψ ⊳ Q' ∼ P'"
      by(force dest: simE)
    from QTrans have "Ψ ⊗ SBottom' ⊳ Q ⟼¿M⦇N⦈ ≺ Q'"
      by(metis statEqTransition Identity AssertionStatEqSym)
    moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
      by(rule freshFrame[where C="(Ψ, Q, M)"]) auto
    note FrQ
    moreover from FrQ ‹guarded Q› have "Ψ⇩Q ≃ SBottom'"
      by(blast dest: guardedStatEq)
    from ‹Ψ ⊳ !P ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ P''› ‹Ψ ⊳ P ∼ Q› ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* Q› ‹guarded Q›
    obtain Q'' T R where QTrans': "Ψ ⊳ !Q ⟼¡M⦇ν*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 cBrComm1 by force
    from QTrans' ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊳ !Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q''"
      by(metis statEqTransition Identity compositionSym AssertionStatEqSym)
    ultimately have "Ψ ⊳ Q ∥ !Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q' ∥ Q''"
      using ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* M› ‹xvec ♯* Q› by(intro BrComm1) (assumption | simp)+
    then have "Ψ ⊳ !Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q' ∥ Q''"
      using ‹guarded Q› by(rule Bang)
    moreover from ‹Ψ ⊳ P'' ∼ R ∥ !P› ‹guarded P› ‹xvec ♯* Ψ› have "Ψ ⊳ P' ∥ P'' ∼ (P' ∥ R) ∥ (P ∥ !P)"
      by(metis bisimParPresSym bangExt bisimTransitive bisimParAssoc bisimSymmetric)
    moreover from ‹Ψ ⊳ Q'' ∼ T ∥ !Q› ‹xvec ♯* Ψ› ‹xvec ♯* Q› have "Ψ ⊳ Q' ∥ Q'' ∼ (Q' ∥ T) ∥ !Q"
      by(metis bisimParPresSym bisimTransitive bisimParAssoc bisimSymmetric)
    moreover from ‹Ψ ⊳ R ∼ T› ‹Ψ ⊳ Q' ∼ P'› ‹xvec ♯* Ψ› have "Ψ ⊳ P' ∥ R ∼ Q' ∥ T"
      by(metis bisimParPresSym bisimTransitive bisimParComm bisimE(4))
    moreover from suppR have "((supp(P' ∥ R))::name set) ⊆  supp((P' ∥ P''))"
      by(auto simp add: psi.supp resChainSupp)
    moreover from suppT have "((supp(Q' ∥ T))::name set) ⊆  supp((Q' ∥ Q''))"
      by(auto simp add: psi.supp resChainSupp)
    ultimately show ?case by blast
  next
    case(cBrComm2 M N P' xvec P'' Q)
    from ‹Ψ ⊳ P ∼ Q› have "Ψ ⊳ Q ↝[bisim] P" by(metis bisimE)
    with ‹Ψ ⊳ P ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ P'› obtain Q' where QTrans: "Ψ ⊳ Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q'" and "Ψ ⊳ Q' ∼ P'"
      using ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* Q› by(auto dest: simE)
    from QTrans have "Ψ ⊗ SBottom' ⊳ Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q'"
      by(metis statEqTransition Identity AssertionStatEqSym)
    moreover obtain A⇩Q Ψ⇩Q where FrQ: "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩" and "A⇩Q ♯* Ψ" and "A⇩Q ♯* Q" and "A⇩Q ♯* M"
      by(rule freshFrame[where C="(Ψ, Q, M)"]) auto
    note FrQ
    moreover from FrQ ‹guarded Q› have "Ψ⇩Q ≃ SBottom'" by(blast dest: guardedStatEq)
    from ‹Ψ ⊳ !P ⟼¿M⦇N⦈ ≺ P''› ‹Ψ ⊳ P ∼ Q› ‹xvec ♯* Ψ› ‹xvec ♯* P› ‹xvec ♯* Q› ‹guarded Q›
    obtain Q'' T R where QTrans': "Ψ ⊳ !Q ⟼¿M⦇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 cBrComm2 by force
    from QTrans' ‹Ψ⇩Q ≃ SBottom'› have "Ψ ⊗ Ψ⇩Q ⊳ !Q ⟼¿M⦇N⦈ ≺ Q''"
      by(metis statEqTransition Identity compositionSym AssertionStatEqSym)
    ultimately have "Ψ ⊳ Q ∥ !Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q' ∥ Q''"
      using ‹A⇩Q ♯* Ψ› ‹A⇩Q ♯* Q› ‹A⇩Q ♯* M› ‹xvec ♯* Q› by(intro BrComm2) (assumption | simp)+
    then have "Ψ ⊳ !Q ⟼¡M⦇ν*xvec⦈⟨N⟩ ≺ Q' ∥ Q''"
      using ‹guarded Q› by(rule Bang)
    moreover from ‹Ψ ⊳ P'' ∼ R ∥ !P› ‹guarded P› ‹xvec ♯* Ψ› have "Ψ ⊳ P' ∥ P'' ∼ (P' ∥ R) ∥ (P ∥ !P)"
      by(metis bisimParPresSym bangExt bisimTransitive bisimParAssoc bisimSymmetric)
    moreover from ‹Ψ ⊳ Q'' ∼ T ∥ !Q› ‹xvec ♯* Ψ› ‹xvec ♯* Q› have "Ψ ⊳ Q' ∥ Q'' ∼ (Q' ∥ T) ∥ !Q"
      by(metis bisimParPresSym bisimTransitive bisimParAssoc bisimSymmetric)
    moreover from ‹Ψ ⊳ R ∼ T› ‹Ψ ⊳ Q' ∼ P'› ‹xvec ♯* Ψ› have "Ψ ⊳ P' ∥ R ∼ Q' ∥ T"
      by(metis bisimParPresSym bisimTransitive bisimParComm bisimE(4))
    moreover from suppR have "((supp(P' ∥ R))::name set) ⊆  supp((P' ∥ P''))"
      by(auto simp add: psi.supp resChainSupp)
    moreover from suppT have "((supp(Q' ∥ T))::name set) ⊆  supp((Q' ∥ Q''))"
      by(auto simp add: psi.supp resChainSupp)
    ultimately show ?case 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(clarsimp simp add: eqvt_def)
    apply(drule bisimClosed)
    by force
  ultimately have "Ψ ⊳ 𝟬 ∥ !P ∼ 𝟬 ∥ !Q"
  proof(coinduct rule: weakTransitiveCoinduct)
    case(cStatEq Ψ P Q)
    then show ?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 Ψ')
    then show ?case by(blast dest: bisimE)
  next
    case(cSym Ψ RP RQ)
    then show ?case by(blast dest: bisimE)
  qed
  then show ?thesis
    by(metis bisimTransitive bisimParNil bisimSymmetric bisimParComm)
qed

end

end