Theory Sim_Struct_Cong

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

lemma partitionListLeft:
  assumes "xs@ys=xs'@y#ys'"
  and     "y mem xs"
  and     "distinct(xs@ys)"

  obtains zs where "xs = xs'@y#zs" and "ys'=zs@ys"
using assms
by(auto simp add: append_eq_append_conv2 append_eq_Cons_conv)

lemma partitionListRight: 
  assumes "xs@ys=xs'@y#ys'"
  and     "y mem ys"
  and     "distinct(xs@ys)"

  obtains zs where "xs' = xs@zs" and "ys=zs@y#ys'"
using assms
by(force simp add: append_eq_append_conv2 append_eq_Cons_conv)

context env begin

lemma resComm:
  fixes Ψ   :: 'b
  and   x   :: name
  and   y   :: name
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  and   P   :: "('a, 'b, 'c) psi"
  
  assumes "x ♯ Ψ"
  and     "y ♯ Ψ"
  and     "eqvt Rel"
  and     R1: "⋀Ψ' Q. (Ψ', Q, Q) ∈ Rel"
  and     R2: "⋀Ψ' a b Q. ⟦a ♯ Ψ'; b ♯ Ψ'⟧ ⟹ (Ψ', ⦇νa⦈(⦇νb⦈Q), ⦇νb⦈(⦇νa⦈Q)) ∈ Rel"

  shows "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ↝[Rel] ⦇νy⦈(⦇νx⦈P)"
proof(case_tac "x=y")
  assume "x = y"
  thus ?thesis using R1
    by(force intro: reflexive)
next
  assume "x ≠ y"
  note ‹eqvt Rel›
  moreover from ‹x ♯ Ψ› ‹y ♯ Ψ› have "[x, y] ♯* Ψ" by(simp add: fresh_star_def)
  moreover have "[x, y] ♯* ⦇νx⦈(⦇νy⦈P)" by(simp add: abs_fresh)
  moreover have "[x, y] ♯* ⦇νy⦈(⦇νx⦈P)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIChainFresh[where C="(x, y)"])
    case(cSim α P')
    from ‹bn α ♯* (x, y)› ‹bn α ♯* (⦇νx⦈(⦇νy⦈P))› have "x ♯ bn α" and "y ♯ bn α" and "bn α ♯* P" by simp+
    from ‹[x, y] ♯* α› have "x ♯ α" and "y ♯ α" by simp+
    from ‹[x, y] ♯* P'› have "x ♯ P'" and "y ♯ P'" by simp+
    from ‹bn α ♯* P› ‹x ♯ α› have "bn α ♯* ⦇νx⦈P" by(simp add: abs_fresh)
    with ‹Ψ ⊳ ⦇νy⦈(⦇νx⦈P) ⟼α ≺ P'› ‹y ♯ Ψ› ‹y ♯ α› ‹y ♯ P'› ‹bn α ♯* Ψ›
    show ?case using ‹bn α ♯* subject α› ‹x ♯ α› ‹x ♯ P'› ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* subject α› ‹y ♯ α›
    proof(induct rule: resCases')
      case(cOpen M yvec1 yvec2 y' N P')
      from ‹yvec1 ♯* yvec2› ‹distinct yvec1› ‹distinct yvec2› have "distinct(yvec1@yvec2)" by auto
      from ‹x ♯ M⦇ν*(yvec1 @ y' # yvec2)⦈⟨N⟩› have "x ♯ M" and "x ♯ yvec1" and "x ≠ y'" and "x ♯ yvec2" and "x ♯ N"
        by simp+
      from ‹y ♯ M⦇ν*(yvec1 @ y' # yvec2)⦈⟨N⟩› have "y ♯ M" and "y ♯ yvec1" and "y ♯ yvec2"
        by simp+
      from ‹Ψ ⊳ ([(y, y')] ∙ ⦇νx⦈P) ⟼M⦇ν*(yvec1@yvec2)⦈⟨N⟩ ≺ P'› ‹x ≠ y› ‹x ≠ y'›
      have "Ψ ⊳ ⦇νx⦈([(y, y')] ∙ P) ⟼M⦇ν*(yvec1@yvec2)⦈⟨N⟩ ≺ P'" by(simp add: eqvts)
      moreover note ‹x ♯ Ψ›
      moreover from ‹x ♯ N› ‹x ♯ yvec1› ‹x ♯ yvec2› ‹x ♯ M› have "x ♯ M⦇ν*(yvec1@yvec2)⦈⟨N⟩" by simp
      moreover note ‹x ♯ P'›
      moreover from ‹yvec1 ♯* Ψ› ‹yvec2 ♯* Ψ› have "bn(M⦇ν*(yvec1@yvec2)⦈⟨N⟩) ♯* Ψ" by simp
      moreover from ‹yvec1 ♯* ⦇νx⦈P› ‹yvec2 ♯* ⦇νx⦈P› ‹y ♯ yvec1› ‹y' ♯ yvec1› ‹y ♯ yvec2› ‹y' ♯ yvec2› ‹x ♯ yvec1› ‹x ♯ yvec2›
      have "bn(M⦇ν*(yvec1@yvec2)⦈⟨N⟩) ♯* ([(y, y')] ∙ P)" by simp
      moreover from ‹yvec1 ♯* M› ‹yvec2 ♯* M› have "bn(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) ♯* subject(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩)"
        by simp
      moreover have "bn(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) = yvec1@yvec2" by simp
      moreover have "subject(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) = Some M" by simp
      moreover have "object(M⦇ν*(yvec1 @ yvec2)⦈⟨N⟩) = Some N" by simp
      ultimately show ?case 
      proof(induct rule: resCases')
        case(cOpen M' xvec1 xvec2 x' N' P')
        from ‹bn(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N'⟩) = yvec1 @ yvec2› have "yvec1@yvec2 = xvec1@x'#xvec2" by simp
        from ‹subject(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N'⟩) = Some M› have "M = M'" by simp
        from ‹object(M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N'⟩) = Some N› have "N = N'" by simp
        from ‹x ♯ yvec1› ‹x ♯ yvec2› ‹y' ♯ yvec1› ‹y' ♯ yvec2› ‹y ♯ yvec1› ‹y ♯ yvec2›
        have "x ♯ (yvec1@yvec2)" and "y ♯ (yvec1@yvec2)" and "y' ♯ (yvec1@yvec2)" by simp+
        with ‹yvec1@yvec2 = xvec1@x'#xvec2›
        have "x ♯ xvec1" and "x ≠ x'" and "x ♯ xvec2" and "y ♯ xvec1" and "y ≠ x'" and "y ♯ xvec2"
          and "y' ♯ xvec1" and "x' ≠ y'" and "y' ♯ xvec2"
          by auto

        show ?case
        proof(case_tac "x' mem yvec1")
          assume "x' mem yvec1"
        
          with ‹yvec1@yvec2 = xvec1@x'#xvec2› ‹distinct (yvec1@yvec2)›
          obtain xvec2' where Eq1: "yvec1=xvec1@x'#xvec2'"
                          and Eq: "xvec2=xvec2'@yvec2"
            by(rule_tac partitionListLeft)
          from ‹Ψ ⊳ ([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*(xvec1@xvec2)⦈⟨N'⟩ ≺ P'› ‹y' ∈ supp N› ‹y' ♯ Ψ› ‹y' ♯ M› ‹y' ♯ xvec1› ‹y' ♯ xvec2› Eq ‹M=M'› ‹N = N'›
          have "Ψ ⊳ ⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*((xvec1@xvec2')@y'#yvec2)⦈⟨N'⟩ ≺ P'" 
            by(rule_tac Open) auto
          then have "Ψ ⊳ ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P)) ⟼M⦇ν*(xvec1@x'#xvec2'@y'#yvec2)⦈⟨N⟩ ≺ P'" 
            using ‹x' ∈ supp N'› ‹x' ♯ Ψ› ‹x' ♯ M'› ‹x' ♯ xvec1› ‹x' ♯ xvec2› ‹x' ≠ y'› Eq ‹M=M'› ‹N=N'›
            by(rule_tac Open) auto
          with ‹x' ≠ y'› ‹x ≠ y'› ‹x' ♯ [(y, y')] ∙ P›
          have "Ψ ⊳ ⦇νx⦈(⦇νy'⦈([(y, y')] ∙ P)) ⟼M⦇ν*(xvec1@x'#xvec2'@y'#yvec2)⦈⟨N⟩ ≺ P'"
            by(subst alphaRes[where y=x']) (simp add: calc_atm eqvts abs_fresh)+
          with Eq1 ‹y' ♯ ⦇νx⦈P› ‹x ≠ y'› R1 show ?case
            by(fastforce simp add: alphaRes abs_fresh)
        next
          assume "¬x' mem yvec1"
          hence "x' ♯ yvec1" by(simp add: fresh_def)
          from ‹¬x' mem yvec1› ‹yvec1@yvec2 = xvec1@x'#xvec2›
          have "x' mem yvec2"
            by(fastforce simp add: append_eq_append_conv2 append_eq_Cons_conv
                                  fresh_list_append fresh_list_cons)
          with ‹yvec1@yvec2 = xvec1@x'#xvec2› ‹distinct (yvec1@yvec2)›
          obtain xvec2' where Eq: "xvec1=yvec1@xvec2'"
                          and Eq1: "yvec2=xvec2'@x'#xvec2"
            by(rule_tac partitionListRight)
          from ‹Ψ ⊳ ([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*(xvec1@xvec2)⦈⟨N'⟩ ≺ P'› ‹y' ∈ supp N› ‹y' ♯ Ψ› ‹y' ♯ M› ‹y' ♯ xvec1› ‹y' ♯ xvec2› Eq ‹M=M'› ‹N = N'›
          have "Ψ ⊳ ⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P) ⟼M'⦇ν*(yvec1@y'#xvec2'@xvec2)⦈⟨N'⟩ ≺ P'" 
            by(rule_tac Open) (assumption | simp)+
          then have "Ψ ⊳ ⦇νx'⦈(⦇νy'⦈([(x, x')] ∙ [(y, y')] ∙ P)) ⟼M⦇ν*((yvec1@y'#xvec2')@x'#xvec2)⦈⟨N⟩ ≺ P'" 
            using ‹x' ∈ supp N'› ‹x' ♯ Ψ› ‹x' ♯ M'› ‹x' ♯ xvec1› ‹x' ♯ xvec2› ‹x' ≠ y'› Eq ‹M=M'› ‹N=N'›
            by(rule_tac Open) auto
          with ‹x' ≠ y'› ‹x ≠ y'› ‹x' ♯ [(y, y')] ∙ P›
          have "Ψ ⊳ ⦇νx⦈(⦇νy'⦈([(y, y')] ∙ P)) ⟼M⦇ν*((yvec1@y'#xvec2')@x'#xvec2)⦈⟨N⟩ ≺ P'"
            by(subst alphaRes[where y=x']) (simp add: calc_atm eqvts abs_fresh)+
          with Eq1 ‹y' ♯ ⦇νx⦈P› ‹x ≠ y'› R1 show ?case
            by(fastforce simp add: alphaRes abs_fresh)
        qed
      next
        case(cRes P')
        from ‹Ψ ⊳ ([(y, y')] ∙ P) ⟼M⦇ν*(yvec1@yvec2)⦈⟨N⟩ ≺ P'› ‹y' ∈ supp N› ‹y' ♯ Ψ› ‹y' ♯ M› ‹y' ♯ yvec1› ‹y' ♯ yvec2›
        have "Ψ ⊳ ⦇νy'⦈([(y, y')] ∙ P) ⟼M⦇ν*(yvec1@y'#yvec2)⦈⟨N⟩ ≺ P'" by(rule Open)
        with ‹y' ♯ ⦇νx⦈P› ‹x ≠ y'›have "Ψ ⊳ ⦇νy⦈P ⟼M⦇ν*(yvec1@y'#yvec2)⦈⟨N⟩ ≺ P'" by(simp add: alphaRes abs_fresh)
        hence "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ⟼M⦇ν*(yvec1@y'#yvec2)⦈⟨N⟩ ≺ ⦇νx⦈P'" using ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ yvec1› ‹x ≠ y'› ‹x ♯ yvec2› ‹x ♯ N›
          by(rule_tac Scope) auto
        moreover have "(Ψ, ⦇νx⦈P', ⦇νx⦈P') ∈ Rel" by(rule R1)
        ultimately show ?case by blast
      qed
    next
      case(cRes P')
      from ‹x ♯ ⦇νy⦈P'› ‹x ≠ y› have "x ♯ P'" by(simp add: abs_fresh)
      with ‹Ψ ⊳ ⦇νx⦈P ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α›
      show ?case using ‹bn α ♯* Ψ› ‹bn α ♯* P› ‹bn α ♯* subject α› ‹y ♯ α›
      proof(induct rule: resCases')
        case(cOpen M xvec1 xvec2 x' N P')
        from ‹y ♯ M⦇ν*(xvec1@x'#xvec2)⦈⟨N⟩› have "y ≠ x'" and "y ♯ M⦇ν*(xvec1@xvec2)⦈⟨N⟩" by simp+
        from ‹Ψ ⊳ ([(x, x')] ∙ P) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'› ‹y ♯ Ψ› ‹y ♯ M⦇ν*(xvec1@xvec2)⦈⟨N⟩›
        have "Ψ ⊳ ⦇νy⦈([(x, x')] ∙ P) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ ⦇νy⦈P'" 
          by(rule Scope)
        hence "Ψ ⊳ ⦇νx'⦈(⦇νy⦈([(x, x')] ∙ P)) ⟼M⦇ν*(xvec1@x'#xvec2)⦈⟨N⟩ ≺ ⦇νy⦈P'" 
          using ‹x' ∈ supp N› ‹x' ♯ Ψ› ‹x' ♯ M› ‹x' ♯ xvec1› ‹x' ♯ xvec2›
          by(rule Open)
        with ‹y ≠ x'› ‹x ≠ y› ‹x' ♯ P› have "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ⟼M⦇ν*(xvec1@x'#xvec2)⦈⟨N⟩ ≺ ⦇νy⦈P'"
          by(subst alphaRes[where y=x']) (simp add: abs_fresh eqvts calc_atm)+
        moreover have "(Ψ, ⦇νy⦈P', ⦇νy⦈P') ∈ Rel" by(rule R1)
        ultimately show ?case by blast
      next
        case(cRes P')
        from ‹Ψ ⊳ P ⟼α ≺ P'› ‹y ♯ Ψ› ‹y ♯ α›
        have "Ψ ⊳ ⦇νy⦈P ⟼α ≺ ⦇νy⦈P'" by(rule Scope)
        hence "Ψ ⊳ ⦇νx⦈(⦇νy⦈P) ⟼α ≺ ⦇νx⦈(⦇νy⦈P')" using ‹x ♯ Ψ› ‹x ♯ α›
          by(rule Scope)
        moreover from ‹x ♯ Ψ› ‹y ♯ Ψ› have "(Ψ, ⦇νx⦈(⦇νy⦈P'), ⦇νy⦈(⦇νx⦈P')) ∈ Rel"
          by(rule R2)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

lemma parAssocLeft:
  fixes Ψ   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   R   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  assumes "eqvt Rel"
  and     C1: "⋀Ψ' S T U. (Ψ, (S ∥ T) ∥ U, S ∥ (T ∥ U)) ∈ Rel"
  and     C2: "⋀xvec Ψ' S T U. ⟦xvec ♯* Ψ'; xvec ♯* S⟧ ⟹ (Ψ', ⦇ν*xvec⦈((S ∥ T) ∥ U), S ∥ (⦇ν*xvec⦈(T ∥ U))) ∈ Rel"
  and     C3: "⋀xvec Ψ' S T U. ⟦xvec ♯* Ψ'; xvec ♯* U⟧ ⟹ (Ψ', (⦇ν*xvec⦈(S ∥ T)) ∥ U, ⦇ν*xvec⦈(S ∥ (T ∥ U))) ∈ Rel"
  and     C4: "⋀Ψ' S T xvec. ⟦(Ψ', S, T) ∈ Rel; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈S, ⦇ν*xvec⦈T) ∈ Rel"

  shows "Ψ ⊳ (P ∥ Q) ∥ R ↝[Rel] P ∥ (Q ∥ R)"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α PQR) 
  from ‹bn α ♯* (P ∥ Q ∥ R)› have "bn α ♯* P" and "bn α ♯* Q" and "bn α ♯* R" by simp+
  hence "bn α ♯* (Q ∥ R)" by simp
  with ‹Ψ ⊳ P ∥ (Q ∥ R) ⟼α ≺ PQR› ‹bn α ♯* Ψ› ‹bn α ♯* P›
  show ?case using ‹bn α ♯* subject α›
  proof(induct rule: parCases[where C = "(Ψ, P, Q, R, α)"])
    case(cPar1 P' AQR ΨQR)
    from ‹AQR ♯* (Ψ, P, Q, R, α)› have "AQR ♯* Q" and  "AQR ♯* R"
      by simp+
    with ‹extractFrame(Q ∥ R) = ⟨AQR, ΨQR⟩› ‹distinct AQR›
    obtain AQ ΨQ AR ΨR where "AQR = AQ@AR" and "ΨQR = ΨQ ⊗ ΨR" and FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" and  FrR: "extractFrame R = ⟨AR, ΨR⟩"
                           and "AQ ♯* ΨR" and "AR ♯* ΨQ"
      by(rule_tac mergeFrameE) (auto dest: extractFrameFreshChain)

    from ‹AQR = AQ@AR› ‹AQR ♯* Ψ› ‹AQR ♯* P› ‹AQR ♯* Q› ‹AQR ♯* α›
    have "AQ ♯* Ψ" and "AR ♯* Ψ" and "AQ ♯* P" and "AR ♯* P" and "AQ ♯* Q" and "AR ♯* Q" and "AQ ♯* α" and "AR ♯* α"
      by simp+

    from ‹Ψ ⊗ ΨQR ⊳ P ⟼α ≺ P'› ‹ΨQR = ΨQ ⊗ ΨR› have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼α ≺ P'"
      by(metis statEqTransition Associativity Commutativity Composition)
    hence "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼α ≺ (P' ∥ Q)" using FrQ ‹bn α ♯* Q› ‹AQ ♯* Ψ› ‹AQ ♯* ΨR› ‹AQ ♯* P› ‹AQ ♯* α›
      by(rule_tac Par1) auto
    hence "Ψ ⊳ (P ∥ Q) ∥ R ⟼α ≺ ((P' ∥ Q) ∥ R)" using FrR ‹bn α ♯* R› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* α›
      by(rule_tac Par1) auto
    moreover have "(Ψ, (P' ∥ Q) ∥ R, P' ∥ (Q ∥ R)) ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 QR AP ΨP)
    from ‹AP ♯* (Ψ, P, Q, R, α)› have "AP ♯* Q" and "AP ♯* R" and "AP ♯* α"
      by simp+
    have FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact
    with ‹bn α ♯* P› ‹AP ♯* α› have "bn α ♯* ΨP" by(auto dest: extractFrameFreshChain)
    with ‹bn α ♯* Ψ› have "bn α ♯* (Ψ ⊗ ΨP)" by force
    with ‹Ψ ⊗ ΨP ⊳ Q ∥ R ⟼α ≺ QR›
    show ?case using ‹bn α ♯* Q› ‹bn α ♯* R› ‹bn α ♯* subject α› ‹AP ♯* Q› ‹AP ♯* R›
    proof(induct rule: parCasesSubject[where C = "(AP, ΨP, P, Q, R, Ψ)"])
      case(cPar1 Q' AR ΨR)
      from ‹AR ♯* (AP, ΨP, P, Q, R, Ψ)› have "AR ♯* AP" and "AR ♯* P" and "AR ♯* Q" and "AR ♯* ΨP" and "AR ♯* Ψ"
        by simp+
      from ‹AP ♯* R› ‹extractFrame R = ⟨AR, ΨR⟩› ‹AR ♯* AP› have "AP ♯* ΨR"
        by(drule_tac extractFrameFreshChain) auto
      from ‹(Ψ ⊗ ΨP) ⊗ ΨR ⊳ Q ⟼α ≺ Q'› have "(Ψ ⊗ ΨR) ⊗ ΨP ⊳ Q ⟼α ≺ Q'" 
        by(metis statEqTransition Associativity Commutativity Composition)
      hence "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼α ≺ (P ∥ Q')"
        using FrP ‹bn α ♯* P› ‹AP ♯* Ψ› ‹AP ♯* ΨR› ‹AP ♯* Q› ‹AP ♯* α›
        by(rule_tac Par2) (assumption | force)+
      hence "Ψ ⊳ (P ∥ Q) ∥ R ⟼α ≺ ((P ∥ Q') ∥ R)"
        using ‹extractFrame R = ⟨AR, ΨR⟩› ‹bn α ♯* R› ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* α›
        by(rule_tac Par1) (assumption | simp)+
      moreover have "(Ψ, (P ∥ Q') ∥ R, P ∥ (Q' ∥ R)) ∈ Rel" by(rule C1)
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ)
      from ‹AQ ♯* (AP, ΨP, P, Q, R, Ψ)› have "AQ ♯* AP" and "AQ ♯* R" and "AQ ♯* ΨP" and "AQ ♯* Ψ"
        by simp+
      have FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
      from ‹AP ♯* Q› FrQ ‹AQ ♯* AP› have "AP ♯* ΨQ"
        by(drule_tac extractFrameFreshChain) auto
      from ‹(Ψ ⊗ ΨP) ⊗ ΨQ ⊳ R ⟼α ≺ R'›
      have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊳ R ⟼α ≺ R'"
        by(blast intro: statEqTransition Associativity)
      moreover from FrP FrQ ‹AQ ♯* AP› ‹AP ♯* ΨQ›  ‹AQ ♯* ΨP› 
      have "extractFrame(P ∥ Q) = ⟨(AP@AQ), ΨP ⊗ ΨQ⟩ " by simp
      moreover from ‹bn α ♯* P› ‹bn α ♯* Q› have "bn α ♯* (P ∥ Q)" by simp
      moreover from ‹AP ♯* Ψ› ‹AQ ♯* Ψ› have "(AP@AQ) ♯* Ψ" by simp
      moreover from ‹AP ♯* R› ‹AQ ♯* R› have "(AP@AQ) ♯* R" by simp
      moreover from ‹AP ♯* α› ‹AQ ♯* α› have "(AP@AQ) ♯* α" by simp
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼α ≺ ((P ∥ Q) ∥ R')"
        by(rule Par2) 
      moreover have "(Ψ, (P ∥ Q) ∥ R', P ∥ (Q ∥ R')) ∈ Rel" by(rule C1)
      ultimately show ?case by blast
    next
      case(cComm1 ΨR M N Q' AQ ΨQ K xvec R' AR) 
      from ‹AQ ♯* (AP, ΨP, P, Q, R, Ψ)›
      have "AQ ♯* P" and "AQ ♯* Q" and "AQ ♯* R" and "AQ ♯* AP" and "AQ ♯* ΨP"  and "AQ ♯* Ψ" by simp+
      from ‹AR ♯* (AP, ΨP, P, Q, R, Ψ)› have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" and "AR ♯* AP"  and "AR ♯* Ψ" by simp+
      from ‹xvec ♯* (AP,  ΨP, P, Q, R, Ψ)› have "xvec ♯* AP" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* Ψ" by simp+

      have FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
      with ‹AP ♯* Q› ‹AQ ♯* AP› have "AP ♯* ΨQ"
        by(drule_tac extractFrameFreshChain) auto
      have FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact
      with ‹AP ♯* R› ‹AR ♯* AP› have "AP ♯* ΨR"
        by(drule_tac extractFrameFreshChain) auto
      from ‹(Ψ ⊗ ΨP) ⊗ ΨQ ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'› ‹AP ♯* R› ‹xvec ♯* AP› ‹xvec ♯* K› ‹distinct xvec› have "AP ♯* N" 
        by(rule_tac outputFreshChainDerivative) auto

      from ‹(Ψ ⊗ ΨP) ⊗ ΨR ⊳ Q ⟼M⦇N⦈ ≺ Q'› have "(Ψ ⊗ ΨR) ⊗ ΨP ⊳ Q ⟼M⦇N⦈ ≺ Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      hence "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼M⦇N⦈ ≺ (P ∥ Q')" using FrP ‹AP ♯* Ψ› ‹AP ♯* ΨR› ‹AP ♯* Q› ‹AP ♯* M› ‹AP ♯* N›
        by(rule_tac Par2) auto
      moreover from FrP FrQ ‹AP ♯* ΨQ› ‹AQ ♯* AP› ‹AQ ♯* ΨP› have "extractFrame(P ∥ Q) = ⟨(AP@AQ), ΨP ⊗ ΨQ⟩"
        by simp
      moreover from  ‹(Ψ ⊗ ΨP) ⊗ ΨQ ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'› have "Ψ ⊗ ΨP ⊗ ΨQ ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'"
        by(metis statEqTransition Associativity)
      moreover note ‹extractFrame R = ⟨AR, ΨR⟩›
      moreover from ‹(Ψ ⊗ ΨP) ⊗ ΨQ ⊗ ΨR ⊢ M ↔ K› have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊗ ΨR ⊢ M ↔ K"
        by(metis statEqEnt Associativity Commutativity Composition)
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P ∥ Q') ∥ R')"
        using ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AR ♯* Ψ› ‹AP ♯* P› ‹AQ ♯* P› ‹AR ♯* P› ‹AP ♯* Q› ‹AQ ♯* Q› ‹AR ♯* Q› ‹AP ♯* R› ‹AQ ♯* R› ‹AR ♯* R›
              ‹AP ♯* M› ‹AQ ♯* M› ‹AR ♯* K› ‹AR ♯* AP› ‹AQ ♯* AR› ‹xvec ♯* P› ‹xvec ♯* Q›
        by(rule_tac Comm1) (assumption | simp)+
      moreover from ‹xvec ♯* Ψ› ‹xvec ♯* P› have "(Ψ, ⦇ν*xvec⦈((P ∥ Q') ∥ R'), P ∥ (⦇ν*xvec⦈(Q' ∥ R'))) ∈ Rel"
        by(rule C2)
      ultimately show ?case by blast
    next
      case(cComm2 ΨR M xvec N Q' AQ ΨQ K R' AR) 
      from ‹AQ ♯* (AP,  ΨP, P, Q, R, Ψ)›
      have "AQ ♯* P" and "AQ ♯* Q" and "AQ ♯* R" and "AQ ♯* AP" and "AQ ♯* Ψ" and "AQ ♯* ΨP" by simp+
      from ‹AR ♯* (AP,  ΨP, P, Q, R, Ψ)› have "AR ♯* P" and "AR ♯* Q" and "AR ♯* R" and "AR ♯* AP"and "AR ♯* Ψ" by simp+
      from ‹xvec ♯* (AP,  ΨP, P, Q, R, Ψ)› have "xvec ♯* AP" and "xvec ♯* P" and "xvec ♯* Q" and "xvec ♯* Ψ" by simp+

      have FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact
      with ‹AP ♯* Q› ‹AQ ♯* AP› have "AP ♯* ΨQ"
        by(drule_tac extractFrameFreshChain) auto
      have FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact
      with ‹AP ♯* R› ‹AR ♯* AP› have "AP ♯* ΨR"
        by(drule_tac extractFrameFreshChain) auto

      from ‹(Ψ ⊗ ΨP) ⊗ ΨR ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› ‹AP ♯* Q› ‹xvec ♯* AP› ‹xvec ♯* M› ‹distinct xvec› have "AP ♯* N" 
        by(rule_tac outputFreshChainDerivative) auto

      from ‹(Ψ ⊗ ΨP) ⊗ ΨR ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› have "(Ψ ⊗ ΨR) ⊗ ΨP ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      hence "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ (P ∥ Q')" using FrP ‹AP ♯* Ψ› ‹AP ♯* ΨR› ‹AP ♯* Q› ‹AP ♯* M› ‹AP ♯* N› ‹xvec ♯* P› ‹xvec ♯* AP›
        by(rule_tac Par2) auto
      moreover from FrP FrQ ‹AP ♯* ΨQ› ‹AQ ♯* AP› ‹AQ ♯* ΨP› have "extractFrame(P ∥ Q) = ⟨(AP@AQ), ΨP ⊗ ΨQ⟩"
        by simp+
      moreover from  ‹(Ψ ⊗ ΨP) ⊗ ΨQ ⊳ R ⟼K⦇N⦈ ≺ R'› have "Ψ ⊗ ΨP ⊗ ΨQ ⊳ R ⟼K⦇N⦈ ≺ R'"
        by(metis statEqTransition Associativity)
      moreover note ‹extractFrame R = ⟨AR, ΨR⟩›
      moreover from ‹(Ψ ⊗ ΨP) ⊗ ΨQ ⊗ ΨR ⊢ M ↔ K› have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊗ ΨR ⊢ M ↔ K"
        by(metis statEqEnt Associativity Commutativity Composition)
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P ∥ Q') ∥ R')"
        using ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AR ♯* Ψ› ‹AP ♯* P› ‹AQ ♯* P› ‹AR ♯* P› ‹AP ♯* Q› ‹AQ ♯* Q› ‹AR ♯* Q› ‹AP ♯* R› ‹AQ ♯* R› ‹AR ♯* R›
              ‹AP ♯* M› ‹AQ ♯* M› ‹AR ♯* K› ‹AR ♯* AP› ‹AQ ♯* AR› ‹xvec ♯* R›
        by(rule_tac Comm2) (assumption | simp)+
      moreover from ‹xvec ♯* Ψ› ‹xvec ♯* P› have "(Ψ, ⦇ν*xvec⦈((P ∥ Q') ∥ R'), P ∥ (⦇ν*xvec⦈(Q' ∥ R'))) ∈ Rel"
        by(rule C2)
      ultimately show ?case by blast
    qed
  next
    case(cComm1 ΨQR M N P' AP ΨP K xvec QR' AQR)
    from ‹xvec ♯* (Ψ, P, Q, R, α)› have "xvec ♯* Q" and "xvec ♯* R" by simp+
    from ‹AQR ♯* (Ψ, P, Q, R, α)› have "AQR ♯* Q" and "AQR ♯* R" and "AQR ♯* Ψ" by simp+
    from ‹AP ♯* (Q ∥ R)› have "AP ♯* Q" and "AP ♯* R" by simp+
    have PTrans: "Ψ ⊗ ΨQR ⊳ P ⟼M⦇N⦈ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" and MeqK: "Ψ ⊗ ΨP ⊗ ΨQR ⊢ M ↔ K" by fact+
    note ‹Ψ ⊗ ΨP ⊳ Q ∥ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ QR'›  
    moreover from ‹xvec ♯* Ψ› ‹xvec ♯* ΨP› have "xvec ♯* (Ψ ⊗ ΨP)" by force
    moreover note ‹xvec ♯* Q›‹xvec ♯* R› ‹xvec ♯* K›
         ‹extractFrame(Q ∥ R) = ⟨AQR, ΨQR⟩› ‹distinct AQR› 
    moreover from ‹AQR ♯* Ψ› ‹AQR ♯* ΨP› have "AQR ♯* (Ψ ⊗ ΨP)" by force
    ultimately show ?case using ‹AQR ♯* Q› ‹AQR ♯* R› ‹AQR ♯* K›
    proof(induct rule: parCasesOutputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ ⊗ ΨR" by fact+
      from PTrans Ψeq have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼M⦇N⦈ ≺ P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from ‹(Ψ ⊗ ΨP) ⊗ ΨR ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'› have "(Ψ ⊗ ΨR) ⊗ ΨP ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note ‹extractFrame Q = ⟨AQ, ΨQ⟩›
      moreover from MeqK Ψeq have "(Ψ ⊗ ΨR) ⊗ ΨP ⊗ ΨQ ⊢ M ↔ K"
        by(metis statEqEnt Associativity Commutativity Composition)
      moreover from ‹AP ♯* R› ‹AP ♯* AQR› Aeq ‹extractFrame R = ⟨AR, ΨR⟩› have "AP ♯* AQ" and "AP ♯* ΨR"
        by(auto dest:  extractFrameFreshChain)
      moreover from ‹AQR ♯* P› ‹AQR ♯* Ψ› Aeq have "AQ ♯* P" and "AQ ♯* Ψ" by simp+
      ultimately have "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')"
        using ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* Q› ‹AP ♯* M› ‹AP ♯* AQ› ‹AQ ♯* Ψ› ‹AQ ♯* ΨR› ‹AQ ♯* P› ‹AQ ♯* Q› ‹AQ ♯* K› ‹xvec ♯* P›
        by(rule_tac Comm1) (assumption | force)+
      moreover from ‹AQR ♯* Ψ› Aeq have "AR ♯* Ψ" by simp
      moreover from ‹AQR ♯* P› Aeq have "AR ♯* P" by simp
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ (⦇ν*xvec⦈(P' ∥ Q')) ∥ R" using ‹extractFrame R = ⟨AR, ΨR⟩› ‹AR ♯* Q›
        by(rule_tac Par1) (assumption | simp)+
      moreover from ‹xvec ♯* Ψ› ‹xvec ♯* R› have "(Ψ, (⦇ν*xvec⦈(P' ∥ Q')) ∥ R, ⦇ν*xvec⦈(P' ∥ (Q' ∥ R))) ∈ Rel"
        by(rule C3)
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ ⊗ ΨR" by fact+
      from ‹AQR ♯* Ψ› ‹AQR ♯* P› ‹AQR ♯* ΨP› ‹AP ♯* AQR› Aeq have "AR ♯* Ψ" and "AR ♯* ΨP" and "AP ♯* AR" and "AP ♯* AQ" and "AR ♯* P" by simp+
      from ‹AQR ♯* Ψ› Aeq have "AQ ♯* Ψ" by simp
      from ‹AQR ♯* P› ‹AP ♯* AQR› Aeq FrP have "AQ ♯* ΨP" by(auto dest: extractFrameFreshChain)
      from ‹AP ♯* AQR› ‹extractFrame R = ⟨AR, ΨR⟩› ‹extractFrame Q = ⟨AQ, ΨQ⟩› Aeq ‹AP ♯* Q› ‹AP ♯* R› have "AP ♯* ΨQ" and  "AP ♯* ΨR" by(auto dest: extractFrameFreshChain)
      have RTrans: "(Ψ ⊗ ΨP) ⊗ ΨQ ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
      then obtain K' where KeqK': "((Ψ ⊗ ΨP) ⊗ ΨQ) ⊗ ΨR ⊢ K ↔ K'" and "AP ♯* K'" and "AQ ♯* K'"
      using ‹AP ♯* R› ‹AQ ♯* R› ‹AR ♯* Ψ› ‹AR ♯* ΨP› ‹AR ♯* ΨQ› ‹AQ ♯* AR› ‹AP ♯* AR› ‹AR ♯* R› ‹AR ♯* R› ‹AR ♯* K› ‹distinct AR› ‹xvec ♯* K› ‹distinct xvec›
        by(rule_tac B="AP@AQ" in obtainPrefix) (assumption | force)+
      from PTrans Ψeq have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼M⦇N⦈ ≺ P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from MeqK KeqK' Ψeq have MeqK': "((Ψ ⊗ ΨR) ⊗ ΨQ) ⊗ ΨP ⊢ M ↔ K'"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans)
      ultimately have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼K'⦇N⦈ ≺ P'" using FrP ‹distinct AP› ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* M› ‹AP ♯* K'› ‹AP ♯* ΨQ› ‹AP ♯* ΨR›
        by(rule_tac inputRenameSubject) auto
      moreover from ‹AQR ♯* P› ‹AQR ♯* N› Aeq have "AQ ♯* P" and "AQ ♯* N" by simp+
      ultimately have "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼K'⦇N⦈ ≺ P' ∥ Q" using ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹AQ ♯* ΨR› ‹AQ ♯* K'› ‹AQ ♯* Ψ›
        by(rule_tac Par1) (assumption | force)+
      moreover from FrP ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹AP ♯* AQ› ‹AP ♯* ΨQ› ‹AQ ♯* ΨP›
      have "extractFrame(P ∥ Q) = ⟨(AP@AQ), ΨP ⊗ ΨQ⟩" by simp+
      moreover from RTrans have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊳ R ⟼K⦇ν*xvec⦈⟨N⟩ ≺ R'" by(metis Associativity statEqTransition)
      moreover note FrR
      moreover from MeqK' KeqK' have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊗ ΨR ⊢ K' ↔ K"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans chanEqSym)
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P' ∥ Q) ∥ R')"
        using ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* P› ‹AQ ♯* P› ‹AP ♯* Q› ‹AQ ♯* Q› ‹AP ♯* R› ‹AQ ♯* R› ‹AP ♯* K'› ‹AQ ♯* K'› ‹AP ♯* AR› ‹AQ ♯* AR›
              ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* R› ‹AR ♯* K› ‹xvec ♯* P› ‹xvec ♯* Q›
        by(rule_tac Comm1) (assumption | simp)+
      moreover from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((P' ∥ Q) ∥ R'), ⦇ν*xvec⦈(P' ∥ (Q ∥ R'))) ∈ Rel"
        by(metis C1 C4)
      ultimately show ?case by blast
    qed
  next
    case(cComm2 ΨQR M xvec N P' AP ΨP K QR' AQR)
    from ‹AQR ♯* (Ψ, P, Q, R, α)› have "AQR ♯* Q" and "AQR ♯* R" and "AQR ♯* Ψ" by simp+
    from ‹AP ♯* (Q ∥ R)› ‹xvec ♯* (Q ∥ R)› have "AP ♯* Q" and "AP ♯* R" and "xvec ♯* Q" and "xvec ♯* R" by simp+
    have PTrans: "Ψ ⊗ ΨQR ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" and MeqK: "Ψ ⊗ ΨP ⊗ ΨQR ⊢ M ↔ K" by fact+
    note ‹Ψ ⊗ ΨP ⊳ Q ∥ R ⟼K⦇N⦈ ≺ QR'› ‹extractFrame(Q ∥ R) = ⟨AQR, ΨQR⟩› ‹distinct AQR› 
    moreover from ‹AQR ♯* Ψ› ‹AQR ♯* ΨP› have "AQR ♯* (Ψ ⊗ ΨP)" by force
    ultimately show ?case using ‹AQR ♯* Q› ‹AQR ♯* R› ‹AQR ♯* K›
    proof(induct rule: parCasesInputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ ⊗ ΨR" by fact+
      from PTrans Ψeq have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from ‹(Ψ ⊗ ΨP) ⊗ ΨR ⊳ Q ⟼K⦇N⦈ ≺ Q'› have "(Ψ ⊗ ΨR) ⊗ ΨP ⊳ Q ⟼K⦇N⦈ ≺ Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note ‹extractFrame Q = ⟨AQ, ΨQ⟩›
      moreover from MeqK Ψeq have "(Ψ ⊗ ΨR) ⊗ ΨP ⊗ ΨQ ⊢ M ↔ K"
        by(metis statEqEnt Associativity Commutativity Composition)
      moreover from ‹AP ♯* Q› ‹AP ♯* R› ‹AP ♯* AQR› Aeq ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹extractFrame R = ⟨AR, ΨR⟩›
      have "AP ♯* AQ" and "AP ♯* ΨR" by(auto dest: extractFrameFreshChain)
      moreover from ‹AQR ♯* Ψ›  ‹AQR ♯* P› Aeq have "AQ ♯* Ψ" and "AQ ♯* P" by simp+
      ultimately have "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')"
        using ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* Q› ‹AP ♯* M› ‹AP ♯* AQ› ‹AQ ♯* Ψ› ‹AQ ♯* ΨR› ‹AQ ♯* P› ‹AQ ♯* Q› ‹AQ ♯* K› ‹xvec ♯* Q›
        by(rule_tac Comm2) (assumption | force)+
      moreover from ‹AQR ♯* Ψ› ‹AQR ♯* P› Aeq have "AR ♯* Ψ" and "AR ♯* P" by simp+
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ (⦇ν*xvec⦈(P' ∥ Q')) ∥ R" using ‹extractFrame R = ⟨AR, ΨR⟩› ‹AR ♯* Q›
        by(rule_tac Par1) (assumption | simp)+
      moreover from ‹xvec ♯* Ψ› ‹xvec ♯* R› have "(Ψ, (⦇ν*xvec⦈(P' ∥ Q')) ∥ R, ⦇ν*xvec⦈(P' ∥ (Q' ∥ R))) ∈ Rel"
        by(rule C3)
      ultimately show ?case by blast
    next
      case(cPar2 R' AQ ΨQ AR ΨR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ ⊗ ΨR" by fact+
      from ‹AQR ♯* Ψ› ‹AQR ♯* P› ‹AQR ♯* ΨP› ‹AP ♯* AQR› Aeq 
      have "AR ♯* Ψ" and "AR ♯* ΨP" and "AP ♯* AR" and "AP ♯* AQ" and "AR ♯* P" and "AQ ♯* Ψ" and "AQ ♯* ΨP" by simp+
      have RTrans: "(Ψ ⊗ ΨP) ⊗ ΨQ ⊳ R ⟼K⦇N⦈ ≺ R'" and FrR: "extractFrame R = ⟨AR, ΨR⟩" by fact+
      then obtain K' where KeqK': "((Ψ ⊗ ΨP) ⊗ ΨQ) ⊗ ΨR ⊢ K ↔ K'" and "AP ♯* K'" and "AQ ♯* K'"
      using ‹AP ♯* R› ‹AQ ♯* R› ‹AR ♯* Ψ› ‹AR ♯* ΨP› ‹AR ♯* ΨQ› ‹AQ ♯* AR› ‹AP ♯* AR› ‹AR ♯* R› ‹AR ♯* R› ‹AR ♯* K› ‹distinct AR›
        by(rule_tac B="AP@AQ" in obtainPrefix) (assumption | force)+
      from PTrans Ψeq have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from MeqK KeqK' Ψeq have MeqK': "((Ψ ⊗ ΨR) ⊗ ΨQ) ⊗ ΨP ⊢ M ↔ K'"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans)
      moreover from ‹AP ♯* R› ‹AP ♯* Q› ‹AP ♯* AQR› FrR ‹extractFrame Q = ⟨AQ, ΨQ⟩› Aeq have "AP ♯* ΨQ" and "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)
      ultimately have "(Ψ ⊗ ΨR) ⊗ ΨQ ⊳ P ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ P'" using FrP ‹distinct AP› ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* M› ‹AP ♯* K'›
        by(rule_tac outputRenameSubject) auto
      moreover from ‹AQR ♯* P› ‹AQR ♯* N› ‹AQR ♯* xvec› Aeq have "AQ ♯* P" and "AQ ♯* N" and "AQ ♯* xvec" by simp+
      ultimately have "Ψ ⊗ ΨR ⊳ P ∥ Q ⟼K'⦇ν*xvec⦈⟨N⟩ ≺ (P' ∥ Q)" using ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹AQ ♯* ΨR› ‹AQ ♯* K'› ‹xvec ♯* Q› ‹AQ ♯* Ψ›
        by(rule_tac Par1) (assumption | force)+
      moreover from FrP ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹AP ♯* AQ› ‹AP ♯* ΨQ› ‹AQ ♯* ΨP›
      have "extractFrame(P ∥ Q) = ⟨(AP@AQ), ΨP ⊗ ΨQ⟩" by simp+
      moreover from RTrans have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊳ R ⟼K⦇N⦈ ≺ R'" by(metis Associativity statEqTransition)
      moreover note FrR
      moreover from MeqK' KeqK' have "Ψ ⊗ (ΨP ⊗ ΨQ) ⊗ ΨR ⊢ K' ↔ K"
        by(metis statEqEnt Associativity Commutativity Composition chanEqTrans chanEqSym)
      ultimately have "Ψ ⊳ (P ∥ Q) ∥ R ⟼τ ≺ ⦇ν*xvec⦈((P' ∥ Q) ∥ R')"
        using ‹AP ♯* Ψ› ‹AQ ♯* Ψ› ‹AP ♯* P› ‹AQ ♯* P› ‹AP ♯* Q› ‹AQ ♯* Q› ‹AP ♯* R› ‹AQ ♯* R› ‹AP ♯* K'› ‹AQ ♯* K'› ‹AP ♯* AR› ‹AQ ♯* AR›
              ‹AR ♯* Ψ› ‹AR ♯* P› ‹AR ♯* Q› ‹AR ♯* R› ‹AR ♯* K› ‹xvec ♯* R›
        by(rule_tac Comm2) (assumption | simp)+
      moreover from ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈((P' ∥ Q) ∥ R'), ⦇ν*xvec⦈(P' ∥ (Q ∥ R'))) ∈ Rel"
        by(metis C1 C4)
      ultimately show ?case by blast
    qed
  qed
qed

lemma parNilLeft:
  fixes Ψ :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"  

  assumes "eqvt Rel"
  and     C1: "⋀Q. (Ψ, Q ∥ 𝟬, Q) ∈ Rel"

  shows "Ψ ⊳ (P ∥ 𝟬) ↝[Rel] P"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α P')
  from ‹Ψ ⊳ P ⟼α ≺ P'› have "Ψ ⊗ SBottom' ⊳ P ⟼α ≺ P'"
    by(metis statEqTransition Identity AssertionStatEqSym)
  hence "Ψ ⊳ (P ∥ 𝟬) ⟼α ≺ (P' ∥ 𝟬)"
    by(rule_tac Par1) auto
  moreover have "(Ψ, P' ∥ 𝟬, P') ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

lemma parNilRight:
  fixes Ψ :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"  

  assumes "eqvt Rel"
  and     C1: "⋀Q. (Ψ, Q, (Q ∥ 𝟬)) ∈ Rel"

  shows "Ψ ⊳ P ↝[Rel] (P ∥ 𝟬)"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α P')
  note ‹Ψ ⊳ P ∥ 𝟬 ⟼α ≺ P'› ‹bn α ♯* Ψ› ‹bn α ♯* P›
  moreover have "bn α ♯* 𝟬" by simp
  ultimately show ?case using ‹bn α ♯* subject α›
  proof(induct rule: parCases[where C="()"])
    case(cPar1 P' AQ ΨQ)
    from ‹extractFrame(𝟬) = ⟨AQ, ΨQ⟩› have "ΨQ = SBottom'" by auto
    with ‹Ψ ⊗ ΨQ ⊳ P ⟼α ≺ P'› have "Ψ ⊳ P ⟼α ≺ P'"
      by(metis statEqTransition Identity)
    moreover have "(Ψ, P', P' ∥ 𝟬) ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 Q' AP ΨP)
    from ‹Ψ ⊗ ΨP ⊳ 𝟬 ⟼α ≺ Q'› have False
      by auto
    thus ?case by simp
  next
    case(cComm1 ΨQ M N P' AP ΨP K xvec Q' AQ)
    from ‹Ψ ⊗ ΨP ⊳ 𝟬 ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'› have False by auto
    thus ?case by simp
  next
    case(cComm2 ΨQ M xvec N P' AP ΨP K Q' AQ)
    from ‹Ψ ⊗ ΨP ⊳ 𝟬 ⟼K⦇N⦈ ≺ Q'› have False
      by auto
    thus ?case by simp
  qed
qed

lemma resNilLeft:
  fixes x   :: name
  and   Ψ   :: 'b
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  shows "Ψ ⊳ ⦇νx⦈𝟬 ↝[Rel] 𝟬"
by(auto simp add: simulation_def)

lemma resNilRight:
  fixes x   :: name
  and   Ψ   :: 'b
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"

  shows "Ψ ⊳ 𝟬 ↝[Rel] ⦇νx⦈𝟬"
apply(auto simp add: simulation_def)
by(cases rule: semantics.cases) (auto simp add: psi.inject alpha')

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

  assumes "eqvt Rel"
  and     "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ xvec"
  and     "x ♯ N"
  and     C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"

  shows "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ↝[Rel] M⦇λ*xvec N⦈.⦇νx⦈P"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover have "x ♯ ⦇νx⦈(M⦇λ*xvec N⦈.P)" by(simp add: abs_fresh)
  moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⦇λ*xvec N⦈.⦇νx⦈P"
    by(auto simp add: inputChainFresh abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    from ‹Ψ ⊳ M⦇λ*xvec N⦈.⦇νx⦈P ⟼α ≺ P'› ‹x ♯ α› show ?case
    proof(induct rule: inputCases)
      case(cInput K Tvec)
      from ‹x ♯ K⦇N[xvec::=Tvec]⦈› have "x ♯ K" and "x ♯ N[xvec::=Tvec]" by simp+
      from ‹Ψ ⊢ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
      have "Ψ ⊳ M⦇λ*xvec N⦈.P ⟼K⦇(N[xvec::=Tvec])⦈ ≺ P[xvec::=Tvec]"
        by(rule Input)
      hence "Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ⟼K⦇(N[xvec::=Tvec])⦈ ≺ ⦇νx⦈(P[xvec::=Tvec])" using ‹x ♯ Ψ› ‹x ♯ K› ‹x ♯ N[xvec::=Tvec]›
        by(rule_tac Scope) auto
      moreover from ‹length xvec = length Tvec› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹x ♯ N[xvec::=Tvec]› have "x ♯ Tvec"
        by(rule substTerm.subst3)
      with ‹x ♯ xvec› have "(Ψ, ⦇νx⦈(P[xvec::=Tvec]), (⦇νx⦈P)[xvec::=Tvec]) ∈ Rel"
        by(force intro: C1)
      ultimately show ?case by blast
    qed
  qed
qed
 
lemma inputPushResRight:
  fixes Ψ   :: 'b
  and   x    :: name
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "eqvt Rel"
  and     "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ xvec"
  and     "x ♯ N"
  and     C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"

  shows "Ψ ⊳ M⦇λ*xvec N⦈.⦇νx⦈P ↝[Rel] ⦇νx⦈(M⦇λ*xvec N⦈.P)"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⦇λ*xvec N⦈.⦇νx⦈P"
    by(auto simp add: inputChainFresh abs_fresh)
  moreover have "x ♯ ⦇νx⦈(M⦇λ*xvec N⦈.P)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    note ‹Ψ ⊳ ⦇νx⦈(M⦇λ*xvec N⦈.P) ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P'› ‹bn α ♯* Ψ› 
    moreover from ‹bn α ♯* (⦇νx⦈(M⦇λ*xvec N⦈.P))› ‹x ♯ α› have  "bn α ♯* (M⦇λ*xvec N⦈.P)"
      by simp
    ultimately show ?case using ‹bn α ♯* subject α›
    proof(induct rule: resCases)
      case(cRes P')
      from ‹Ψ ⊳ M⦇λ*xvec N⦈.P ⟼α ≺ P'› ‹x ♯ α› show ?case
      proof(induct rule: inputCases)
        case(cInput K Tvec)
        from ‹x ♯ K⦇N[xvec::=Tvec]⦈› have "x ♯ K" and "x ♯ N[xvec::=Tvec]" by simp+
        from ‹Ψ ⊢ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
        have "Ψ ⊳ M⦇λ*xvec N⦈.(⦇νx⦈P) ⟼K⦇(N[xvec::=Tvec])⦈ ≺ (⦇νx⦈P)[xvec::=Tvec]"
          by(rule Input)
        moreover from ‹length xvec = length Tvec› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹x ♯ N[xvec::=Tvec]› have "x ♯ Tvec"
          by(rule substTerm.subst3)
        with ‹x ♯ xvec› have "(Ψ, (⦇νx⦈P)[xvec::=Tvec], ⦇νx⦈(P[xvec::=Tvec])) ∈ Rel"
          by(force intro: C1)
        ultimately show ?case by blast
      qed
    next
      case cOpen
      then have False by auto
      thus ?case by simp
    qed
  qed
qed

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

  assumes "eqvt Rel"
  and     "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ N"
  and     C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"

  shows "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ↝[Rel] M⟨N⟩.⦇νx⦈P"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover have "x ♯ ⦇νx⦈(M⟨N⟩.P)" by(simp add: abs_fresh)
  moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⟨N⟩.⦇νx⦈P"
    by(auto simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    from ‹Ψ ⊳ M⟨N⟩.⦇νx⦈P ⟼α ≺ P'› ‹x ♯ α›
    show ?case
    proof(induct rule: outputCases)
      case(cOutput K)
      from ‹Ψ ⊢ M ↔ K› have "Ψ ⊳ M⟨N⟩.P ⟼K⟨N⟩ ≺ P"
        by(rule Output)
      hence "Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ⟼K⟨N⟩ ≺ ⦇νx⦈P" using ‹x ♯ Ψ› ‹x ♯ K⟨N⟩›
        by(rule Scope)
      moreover have "(Ψ, ⦇νx⦈P, ⦇νx⦈P) ∈ Rel" by(rule C1)
      ultimately show ?case by blast
    qed
  qed
qed
 
lemma outputPushResRight:
  fixes Ψ   :: 'b
  and   x    :: name
  and   M    :: 'a
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"

  assumes "eqvt Rel"
  and     "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ N"
  and     C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"

  shows "Ψ ⊳ M⟨N⟩.⦇νx⦈P ↝[Rel] ⦇νx⦈(M⟨N⟩.P)"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover from ‹x ♯ M› ‹x ♯ N› have "x ♯ M⟨N⟩.⦇νx⦈P"
    by(auto simp add: abs_fresh)
  moreover have "x ♯ ⦇νx⦈(M⟨N⟩.P)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "(M, N)"])
    case(cSim α P')
    note ‹Ψ ⊳ ⦇νx⦈(M⟨N⟩.P) ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P'› ‹bn α ♯* Ψ›
    moreover from ‹bn α ♯* (⦇νx⦈(M⟨N⟩.P))› ‹x ♯ α› have "bn α ♯* (M⟨N⟩.P)" by simp
    ultimately show ?case using ‹bn α ♯* subject α› ‹bn α ♯* (M, N)› ‹x ♯ α›
    proof(induct rule: resCases)
      case(cOpen K xvec1 xvec2 y N' P')
      from ‹bn(K⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) ♯* (M, N)› have "y ♯ N" by simp+
      from ‹Ψ ⊳ M⟨N⟩.P ⟼K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N')⟩ ≺ ([(x, y)] ∙ P')›
      have "N = ([(x, y)] ∙ N')"
        apply -
        by(ind_cases "Ψ ⊳ M⟨N⟩.P ⟼K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N')⟩ ≺ ([(x, y)] ∙ P')")
          (auto simp add: residualInject psi.inject)
      with ‹x ♯ N› ‹y ♯ N› ‹x ≠ y› have "N = N'"
        by(subst pt_bij[OF pt_name_inst, OF at_name_inst, symmetric, where pi="[(x, y)]"])
          (simp add: fresh_left calc_atm)
      with ‹y ∈ supp N'› ‹y ♯ N› have False by(simp add: fresh_def)
      thus ?case by simp
    next
      case(cRes P')
      from ‹Ψ ⊳ M⟨N⟩.P ⟼α ≺ P'› show ?case
      proof(induct rule: outputCases)
        case(cOutput K)
        from ‹Ψ ⊢ M ↔ K› have "Ψ ⊳ M⟨N⟩.(⦇νx⦈P) ⟼K⟨N⟩ ≺ ⦇νx⦈P"
          by(rule Output)
        moreover have "(Ψ, ⦇νx⦈P, ⦇νx⦈P) ∈ Rel" by(rule C1)
        ultimately show ?case by force
      qed
    qed
  qed
qed

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

  assumes "eqvt Rel"
  and     "x ♯ Ψ"
  and     "x ♯ map fst Cs"
  and     C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"

  shows "Ψ ⊳ ⦇νx⦈(Cases Cs) ↝[Rel] Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover have "x ♯ ⦇νx⦈(Cases Cs)" by(simp add: abs_fresh)
  moreover from ‹x ♯ map fst Cs› have "x ♯ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
    by(induct Cs) (auto simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ Cs])
    case(cSim α P'')
    from ‹Ψ ⊳ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs) ⟼α ≺ P''› 
    show ?case
    proof(induct rule: caseCases)
      case(cCase φ P')
      from ‹(φ, P') mem (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)› 
      obtain P where "(φ, P) mem Cs" and "P' = ⦇νx⦈P" 
        by(induct Cs) auto
      from ‹guarded P'› ‹P' = ⦇νx⦈P› have "guarded P" by simp
      from ‹Ψ ⊳ P' ⟼α ≺ P''› ‹P' = ⦇νx⦈P› have "Ψ ⊳ ⦇νx⦈P ⟼α ≺ P''"
        by simp
      moreover note ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P''› ‹bn α ♯* Ψ› 
      moreover from ‹bn α ♯* Cs› ‹(φ, P) mem Cs›
      have "bn α ♯* P" by(auto dest: memFreshChain)
      ultimately show ?case using ‹bn α ♯* subject α› ‹x ♯ α› ‹bn α ♯* Cs›
      proof(induct rule: resCases)
        case(cOpen M xvec1 xvec2 y N P')
        from ‹x ♯ M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩› have "x ♯ xvec1" and "x ♯ xvec2" and "x ♯ M" by simp+
        from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* Cs› have "y ♯ Cs" by simp
        from ‹Ψ ⊳ P ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')› ‹(φ, P) mem Cs› ‹Ψ ⊢ φ› ‹guarded P›
        have "Ψ ⊳ Cases Cs ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')" by(rule Case)
        hence "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ (Cases Cs))  ⟼([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')))"
          by(rule semantics.eqvt)
        with ‹x ♯ Ψ› ‹x ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2› ‹y ♯ Ψ› ‹y ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2›
        have "Ψ ⊳ ([(x, y)] ∙ (Cases Cs))  ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'" by(simp add: eqvts)
        hence "Ψ ⊳ ⦇νy⦈([(x, y)] ∙ (Cases Cs))  ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
          by(rule Open)
        hence "Ψ ⊳ ⦇νx⦈(Cases Cs)  ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ♯ Cs›
          by(simp add: alphaRes)
        moreover have "(Ψ, P', P') ∈ Rel" by(rule C1)
        ultimately show ?case by blast
      next
        case(cRes P')
        from ‹Ψ ⊳ P ⟼α ≺ P'› ‹(φ, P) mem Cs› ‹Ψ ⊢ φ› ‹guarded P›
        have "Ψ ⊳ Cases Cs ⟼α ≺ P'" by(rule Case)
        hence "Ψ ⊳ ⦇νx⦈(Cases Cs) ⟼α ≺ ⦇νx⦈P'" using ‹x ♯ Ψ› ‹x ♯ α›
          by(rule Scope)
        moreover have "(Ψ, ⦇νx⦈P', ⦇νx⦈P') ∈ Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    qed
  qed
qed
 
lemma casePushResRight:
  fixes Ψ  :: 'b
  and   x  :: name
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "eqvt Rel"
  and     "x ♯ Ψ"
  and     "x ♯ map fst Cs"
  and     C1: "⋀Q. (Ψ, Q, Q) ∈ Rel"

  shows "Ψ ⊳ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs) ↝[Rel] ⦇νx⦈(Cases Cs)"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover from ‹x ♯ map fst Cs› have "x ♯ Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
    by(induct Cs) (auto simp add: abs_fresh)
  moreover have "x ♯ ⦇νx⦈(Cases Cs)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ Cs])
    case(cSim α P'')
    note ‹Ψ ⊳ ⦇νx⦈(Cases Cs) ⟼α ≺ P''› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ P''› ‹bn α ♯* Ψ›
    moreover from ‹bn α ♯* ⦇νx⦈(Cases Cs)› ‹x ♯ α› have "bn α ♯* (Cases Cs)" by simp
    ultimately show ?case using ‹bn α ♯* subject α› ‹x ♯ α› ‹bn α ♯* Cs›
    proof(induct rule: resCases)
      case(cOpen M xvec1 xvec2 y N P')
      from ‹x ♯ M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩› have "x ♯ xvec1" and "x ♯ xvec2" and "x ♯ M" by simp+
      from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* Cs› have "y ♯ Cs" by simp
      from ‹Ψ ⊳ Cases Cs ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')›
      show ?case
      proof(induct rule: caseCases)
        case(cCase φ P)
        from ‹Ψ ⊳ P ⟼M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')›
        have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ P)  ⟼([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ P')))"
          by(rule semantics.eqvt)
        with ‹x ♯ Ψ› ‹x ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2› ‹y ♯ Ψ› ‹y ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2›
        have "Ψ ⊳ ([(x, y)] ∙ P)  ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'" by(simp add: eqvts)
        hence "Ψ ⊳ ⦇νy⦈([(x, y)] ∙ P)  ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
          by(rule Open)
        hence "Ψ ⊳ ⦇νx⦈P  ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'" using ‹y ♯ Cs› ‹(φ, P) mem Cs›
          by(subst alphaRes, auto dest: memFresh)
        moreover from ‹(φ, P) mem Cs› have "(φ, ⦇νx⦈P) mem (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
          by(induct Cs) auto
        moreover note ‹Ψ ⊢ φ›
        moreover from ‹guarded P› have "guarded(⦇νx⦈P)" by simp
        ultimately have "Ψ ⊳ (Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ P'"
          by(rule Case)
        moreover have "(Ψ, P', P') ∈ Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    next
      case(cRes P')
      from ‹Ψ ⊳ Cases Cs ⟼α ≺ P'›
      show ?case
      proof(induct rule: caseCases)
        case(cCase φ P)
        from ‹Ψ ⊳ P ⟼α ≺ P'› ‹x ♯ Ψ› ‹x ♯ α›
        have "Ψ ⊳ ⦇νx⦈P ⟼α ≺ ⦇νx⦈P'" by(rule Scope)
        moreover from ‹(φ, P) mem Cs› have "(φ, ⦇νx⦈P) mem (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)"
          by(induct Cs) auto
        moreover note ‹Ψ ⊢ φ›
        moreover from ‹guarded P› have "guarded(⦇νx⦈P)" by simp
        ultimately have "Ψ ⊳ (Cases (map (λ(φ, P). (φ, ⦇νx⦈P)) Cs)) ⟼α ≺ ⦇νx⦈P'"
          by(rule Case)
        moreover have "(Ψ, ⦇νx⦈P', ⦇νx⦈P') ∈ Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

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

  assumes Trans: "Ψ ⊳ ⦇νx⦈P ⟼M⦇N⦈ ≺ P'"
  and     "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ N"
  and     "x ♯ P'"
  and     rScope:  "⋀P'. ⟦Ψ ⊳ P ⟼M⦇N⦈ ≺ P'⟧ ⟹ Prop (⦇νx⦈P')"

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

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

  assumes "x ♯ P"
  and     "x ♯ Ψ"
  and     "eqvt Rel"
  and     C1: "⋀Ψ' R. (Ψ', R, R) ∈ Rel"
  and     C2: "⋀y Ψ' R S zvec. ⟦y ♯ Ψ'; y ♯ R; zvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇νy⦈(⦇ν*zvec⦈(R ∥ S)), ⦇ν*zvec⦈(R ∥ ⦇νy⦈S)) ∈ Rel"
  and     C3: "⋀Ψ' zvec R y. ⟦y ♯ Ψ'; zvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇νy⦈(⦇ν*zvec⦈R), ⦇ν*zvec⦈(⦇νy⦈R)) ∈ Rel"

  shows "Ψ ⊳ ⦇νx⦈(P ∥ Q) ↝[Rel] P ∥ ⦇νx⦈Q"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover have "x ♯ ⦇νx⦈(P ∥ Q)" by(simp add: abs_fresh)
  moreover from ‹x ♯ P› have "x ♯ P ∥ ⦇νx⦈Q" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ x])
    case(cSim α PQ)
    from ‹x ♯ α› ‹bn α ♯* (P ∥ ⦇νx⦈Q)› have "bn α ♯* Q" by simp
    note ‹Ψ ⊳ P ∥ ⦇νx⦈Q ⟼α ≺ PQ› ‹bn α ♯* Ψ›
    moreover from ‹bn α ♯* (P ∥ ⦇νx⦈Q)› have "bn α ♯* P" and "bn α ♯* ⦇νx⦈Q" by simp+
    ultimately show ?case using ‹bn α ♯* subject α› ‹x ♯ PQ›
    proof(induct rule: parCases[where C=x])
      case(cPar1 P' AQ ΨQ)
      from ‹x ♯ P' ∥ ⦇νx⦈Q› have "x ♯ P'" by simp
      have PTrans: "Ψ ⊗ ΨQ ⊳ P ⟼α ≺ P'" by fact
      from ‹extractFrame(⦇νx⦈Q) = ⟨AQ, ΨQ⟩› have FrxQ: "⦇νx⦈(extractFrame Q) = ⟨AQ, ΨQ⟩" by simp
      then obtain y AQ' where A: "AQ = y#AQ'" by(case_tac AQ) auto
      with ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* α›
      have "AQ' ♯* Ψ" and "AQ' ♯* P" and "AQ' ♯* α"
        and "y ♯ Ψ" and "y ♯ P" and "y ♯ α"
        by simp+
      from PTrans ‹y ♯ P› ‹y ♯ α› ‹bn α ♯* subject α› ‹distinct(bn α)› have "y ♯ P'"
        by(auto intro: freeFreshDerivative)
      note PTrans
      moreover from A ‹AQ ♯* x› FrxQ have "extractFrame([(y, x)] ∙ Q) = ⟨AQ', ΨQ⟩" 
        by(simp add: frame.inject alpha' fresh_list_cons eqvts) 
      moreover from ‹bn α ♯* Q› have "([(y, x)] ∙ (bn α)) ♯* ([(y, x)] ∙ Q)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹x ♯ α› ‹AQ ♯* α› A have "bn α ♯* ([(y, x)] ∙ Q)" by simp
      ultimately have "Ψ ⊳ P ∥ ([(y, x)] ∙ Q) ⟼α ≺ (P' ∥ ([(y, x)] ∙ Q))"
        using ‹AQ' ♯* Ψ› ‹AQ' ♯* P› ‹AQ' ♯* α›
        by(rule Par1)
      hence "Ψ ⊳ ⦇νy⦈(P ∥ ([(y, x)] ∙ Q)) ⟼α ≺ ⦇νy⦈(P' ∥ ([(y, x)] ∙ Q))"
        using ‹y ♯ Ψ› ‹y ♯ α›
        by(rule Scope)
      hence "([(y, x)] ∙ Ψ) ⊳ ([(y, x)] ∙ (⦇νy⦈(P ∥ ([(y, x)] ∙ Q)))) ⟼([(y, x)] ∙ (α ≺ ⦇νy⦈(P' ∥ ([(y, x)] ∙ Q))))"
        by(rule semantics.eqvt)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹x ♯ P› ‹y ♯ P› ‹x ♯ α› ‹y ♯ α› ‹x ♯ P'› ‹y ♯ P'›
      have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼α ≺ ⦇νx⦈(P' ∥ Q)"
        by(simp add: eqvts calc_atm)
      moreover from ‹x ♯ Ψ› ‹x ♯ P'› have "(Ψ, ⦇νx⦈(⦇ν*[]⦈(P' ∥ Q)), ⦇ν*[]⦈(P' ∥ ⦇νx⦈Q)) ∈ Rel"
        by(rule_tac C2) auto
      ultimately show ?case
        by force
    next
      case(cPar2 xQ' AP ΨP)
      from ‹AP ♯* ⦇νx⦈Q› ‹AP ♯* x› have "AP ♯* Q" by simp
      note ‹Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼α ≺ xQ'›
      moreover have FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact
      with ‹x ♯ P› ‹AP ♯* x› have "x ♯ ΨP" and "x ♯ AP"
        by(force dest: extractFrameFresh)+
      with ‹x ♯ Ψ› have "x ♯ Ψ ⊗ ΨP" by force
      moreover note ‹x ♯ α›
      moreover from ‹x ♯ P ∥ xQ'› have "x ♯ xQ'" by simp
      moreover from FrP ‹bn α ♯* P› ‹AP ♯* α› have "bn α ♯* ΨP"
        by(drule_tac extractFrameFreshChain) auto
      with ‹bn α ♯* Ψ› have "bn α ♯* (Ψ ⊗ ΨP)" by force
      ultimately show ?case using ‹bn α ♯* Q› ‹bn α ♯* subject α› ‹x ♯ α› ‹bn α ♯* P› ‹AP ♯* α› ‹bn α ♯* Ψ›
      proof(induct rule: resCases')
        case(cOpen M xvec1 xvec2 y N Q')
        from ‹x ♯ M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩› have "x ♯ xvec1" and "x ≠ y" and "x ♯ xvec2" by simp+
        from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* Ψ› have "y ♯ Ψ" by simp
        note ‹Ψ ⊗ ΨP ⊳ ([(x, y)] ∙ Q) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ Q'› FrP
        moreover from ‹bn(M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩) ♯* P› have "(xvec1@xvec2) ♯* P" and "y ♯ P" by simp+
        moreover from ‹AP ♯* (M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩)› have "AP ♯* (M⦇ν*(xvec1@xvec2)⦈⟨N⟩)" and "y ♯ AP" by simp+
        moreover from ‹AP ♯* Q› ‹x ♯ AP› ‹y ♯ AP› have "AP ♯* ([(x, y)] ∙ Q)" by simp
        ultimately have "Ψ ⊳ P ∥ ([(x, y)] ∙ Q) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ (P ∥ Q')" 
          using ‹AP ♯* Ψ›
          by(rule_tac Par2) (assumption | simp)+
         hence "Ψ ⊳ ⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ (P ∥ Q')"
           using ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
           by(rule Open)
         with ‹x ♯ P› ‹y ♯ P› ‹y ♯ Q› have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ (P ∥ Q')"
           by(subst alphaRes[where y=y]) (simp add: fresh_left calc_atm eqvts)+
        moreover have "(Ψ, P ∥ Q', P ∥ Q') ∈ Rel" by(rule C1)
        ultimately show ?case by blast
      next
        case(cRes Q')
        from ‹Ψ ⊗ ΨP ⊳ Q ⟼α ≺ Q'› FrP ‹bn α ♯* P›
        have "Ψ ⊳ P ∥ Q ⟼α ≺ (P ∥ Q')" using ‹AP ♯* Ψ› ‹AP ♯* Q› ‹AP ♯* α›
          by(rule Par2)
        hence "Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼α ≺ ⦇νx⦈(P ∥ Q')" using ‹x ♯ Ψ› ‹x ♯ α›
          by(rule Scope)
        moreover from ‹x ♯ Ψ› ‹x ♯ P› have "(Ψ, ⦇νx⦈(⦇ν*[]⦈(P ∥ Q')), ⦇ν*[]⦈(P ∥ ⦇νx⦈Q')) ∈ Rel"
          by(rule_tac C2) auto
        ultimately show ?case
          by force
      qed
    next
      case(cComm1 ΨQ M N P' AP ΨP K xvec xQ' AQ)
      have QTrans: "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ xQ'" and FrQ: "extractFrame(⦇νx⦈Q) = ⟨AQ, ΨQ⟩" by fact+
      have PTrans: "Ψ ⊗ ΨQ ⊳ P ⟼M⦇N⦈ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact+
      have "x ♯ ⦇νx⦈Q" by(simp add: abs_fresh)
      with QTrans have "x ♯ N" and "x ♯ xQ'" using ‹xvec ♯* x› ‹xvec ♯* K› ‹distinct xvec› 
        by(force intro: outputFreshDerivative)+
      from PTrans ‹x ♯ P› ‹x ♯ N›  have "x ♯ P'" by(rule inputFreshDerivative)
      from ‹x ♯ ⦇νx⦈Q› FrQ ‹AQ ♯* x› have "x ♯ ΨQ"
        by(drule_tac extractFrameFresh) auto
      from ‹x ♯ P› FrP ‹AP ♯* x› have "x ♯ ΨP"
        by(drule_tac extractFrameFresh) auto
      from ‹AP ♯* ⦇νx⦈Q› ‹AP ♯* x› have "AP ♯* Q" by simp
      from ‹AQ ♯* ⦇νx⦈Q› ‹AQ ♯* x› have "AQ ♯* Q" by simp
      from PTrans FrP ‹distinct AP› ‹x ♯ P› ‹AQ ♯* P› ‹xvec ♯* P› ‹AP ♯* Ψ› ‹AP ♯* ΨQ› ‹AP ♯* x› ‹AP ♯* AQ› ‹AP ♯* P›  ‹AP ♯* M› ‹AP ♯* xvec›
      obtain M' where "(Ψ ⊗ ΨQ) ⊗ ΨP ⊢ M ↔ M'" and "x ♯ M'" and "AQ ♯* M'" and "xvec ♯* M'"
        by(rule_tac B="x#xvec@AQ" in obtainPrefix) (assumption | force simp add: fresh_star_list_cons)+
      hence MeqM': "Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ M'" by(metis statEqEnt Associativity Commutativity Composition)
      with ‹Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ K› have "Ψ ⊗ ΨP ⊗ ΨQ ⊢ K ↔ M'"
        by(blast intro: chanEqTrans chanEqSym)
      hence "(Ψ ⊗ ΨP) ⊗ ΨQ ⊢ K ↔ M'" by(metis statEqEnt Associativity Commutativity Composition)
      with QTrans FrQ ‹distinct AQ› ‹AQ ♯* Ψ› ‹AQ ♯* ΨP› ‹AQ ♯* (⦇νx⦈Q)› ‹AQ ♯* K› ‹AQ ♯* M'›
      have "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M'⦇ν*xvec⦈⟨N⟩ ≺ xQ'"
        by(force intro: outputRenameSubject)
      moreover from ‹x ♯ Ψ› ‹x ♯ ΨP› have "x ♯ Ψ ⊗ ΨP" by force
      moreover from ‹xvec ♯* x› have "x ♯ xvec" by simp
      with ‹x ♯ M'› ‹x ♯ N› have "x ♯ M'⦇ν*xvec⦈⟨N⟩" by simp
      moreover note ‹x ♯ xQ'›
      moreover from ‹xvec ♯* Ψ› ‹xvec ♯* ΨP› have "bn(M'⦇ν*xvec⦈⟨N⟩) ♯* (Ψ ⊗ ΨP)" by force
      moreover from ‹xvec ♯* ⦇νx⦈Q› ‹x ♯ xvec› have "bn(M'⦇ν*xvec⦈⟨N⟩) ♯* Q" by simp
      moreover from ‹xvec ♯* P› have "bn(M'⦇ν*xvec⦈⟨N⟩) ♯* P" by simp
      from ‹xvec ♯* Ψ› have "bn(M'⦇ν*xvec⦈⟨N⟩) ♯* Ψ" by simp
      from ‹AQ ♯* xvec› ‹AQ ♯* M'› ‹AQ ♯* N› have "AQ ♯* (M'⦇ν*xvec⦈⟨N⟩)" by simp
      have "object(M'⦇ν*xvec⦈⟨N⟩) = Some N" by simp
      have "bn(M'⦇ν*xvec⦈⟨N⟩) = xvec" by simp
      have "subject(M'⦇ν*xvec⦈⟨N⟩) = Some M'" by simp
      from ‹xvec ♯* M'› have "bn(M'⦇ν*xvec⦈⟨N⟩) ♯* subject(M'⦇ν*xvec⦈⟨N⟩)" by simp
      ultimately show ?case 
        using ‹x ♯ M'⦇ν*xvec⦈⟨N⟩› ‹bn(M'⦇ν*xvec⦈⟨N⟩) ♯* P› ‹bn(M'⦇ν*xvec⦈⟨N⟩) ♯* Ψ› ‹object(M'⦇ν*xvec⦈⟨N⟩) = Some N›
              ‹bn(M'⦇ν*xvec⦈⟨N⟩) = xvec› ‹subject(M'⦇ν*xvec⦈⟨N⟩) = Some M'› ‹AQ ♯* (M'⦇ν*xvec⦈⟨N⟩)›
      proof(induct rule: resCases)
        case(cOpen M'' xvec1 xvec2 y N' Q')
        from ‹x ♯ M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩› have "x ♯ xvec1" and "x ≠ y" and "x ♯ xvec2" and "x ♯ M''"
          by simp+
        from ‹bn(M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) ♯* P› have "(xvec1@xvec2) ♯* P" and "y ♯ P" by simp+
        from ‹AQ ♯* (M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩)› have "(xvec1@xvec2) ♯* AQ" and "y ♯ AQ" and "AQ ♯* M''" by simp+
        from ‹bn(M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) ♯* Ψ› have "(xvec1@xvec2) ♯* Ψ" and "y ♯ Ψ" by simp+
        from ‹object(M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) = Some N› have "N = N'" by simp
        from ‹bn(M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) = xvec› have "xvec = xvec1@y#xvec2" by simp
        from ‹subject(M''⦇ν*(xvec1@y#xvec2)⦈⟨N'⟩) = Some M'› have "M' = M''" by simp
        from ‹x ♯ P› ‹y ♯ P› ‹x ≠ y› ‹Ψ ⊗ ΨQ ⊳ P ⟼M⦇N⦈ ≺ P'›
        have "Ψ ⊗ ΨQ ⊳ P ⟼M⦇([(y, x)] ∙ N)⦈ ≺ ([(y, x)] ∙ P')"
          by(rule_tac xvec="[y]" in inputAlpha) (auto simp add: calc_atm)
        hence PTrans: "Ψ ⊗ ΨQ ⊳ P ⟼M⦇([(x, y)] ∙ N)⦈ ≺ ([(x, y)] ∙ P')"
          by(simp add: name_swap)
        have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼M''⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N')⟩ ≺ ([(x, y)] ∙ Q')" by fact
        with ‹AQ ♯* x› ‹y ♯ AQ› ‹distinct xvec1› ‹distinct xvec2› ‹xvec1 ♯* xvec2› ‹xvec1 ♯* M''› ‹xvec2 ♯* M''›
             ‹(xvec1@xvec2) ♯* AQ›
        have "AQ ♯* ([(x, y)] ∙ Q')" using ‹AQ ♯* Q›
          by(rule_tac outputFreshChainDerivative(2)) (assumption | simp)+

        from ‹extractFrame(⦇νx⦈Q) = ⟨AQ, ΨQ⟩› have FrxQ: "⦇νx⦈(extractFrame Q) = ⟨AQ, ΨQ⟩" by simp
        then obtain z AQ' where A: "AQ = z#AQ'" by(case_tac AQ) auto
        with ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* P'› ‹AQ ♯* ΨP› ‹AQ ♯* Q› ‹(xvec1@xvec2) ♯* AQ› ‹AQ ♯* M''› ‹AQ ♯* ([(x, y)] ∙ Q')› ‹y ♯ AQ› ‹AQ ♯* N›
        have "AQ' ♯* Ψ" and "AQ' ♯* P" and "AQ' ♯* ΨP" and "AQ' ♯* Q"
          and "z ♯ Ψ" and "z ♯ P" and "z ♯ P'" and "z ♯ ΨP" and "z ♯ Q" and "z ♯ xvec1" and "z ♯ xvec2"
          and "z ♯ M''" and "z ♯ ([(x, y)] ∙ Q')" and "AQ' ♯* M''" and "z ≠ y" and "z ♯ (xvec1@xvec2)"
          by auto
        from A ‹AP ♯* AQ› have "AP ♯* AQ'" and "z ♯ AP" by simp+
        from A ‹AQ ♯* x› have "x ≠ z" and "x ♯ AQ'" by simp+

        from ‹distinct AQ› A have "z ♯ AQ'" 
          by(induct AQ') (auto simp add: fresh_list_nil fresh_list_cons)
        from PTrans ‹x ♯ P› ‹z ♯ P› ‹x ≠ z› have "Ψ ⊗ ΨQ ⊳ P ⟼M⦇([(x, z)] ∙ [(x, y)] ∙ N)⦈ ≺ ([(x, z)] ∙ [(x, y)] ∙ P')"
          by(rule_tac xvec="[x]" in inputAlpha) (auto simp add: calc_atm)
        moreover note FrP 
        moreover from QTrans have "([(x, z)] ∙ (Ψ ⊗ ΨP)) ⊳ ([(x, z)] ∙ Q) ⟼([(x, z)] ∙ (M''⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N')⟩ ≺ ([(x, y)] ∙ Q')))" 
          by(rule semantics.eqvt)
        with ‹x ♯ Ψ› ‹z ♯ Ψ› ‹x ♯ ΨP› ‹z ♯ ΨP› ‹x ♯ M''› ‹z ♯ M''› ‹x ♯ xvec1› ‹x ♯ xvec2› ‹z ♯ xvec1› ‹z ♯ xvec2›
        have "Ψ ⊗ ΨP ⊳ ([(x, z)] ∙ Q) ⟼M''⦇ν*(xvec1@xvec2)⦈⟨([(x, z)] ∙ [(x, y)] ∙ N')⟩ ≺ ([(x, z)] ∙ [(x, y)] ∙ Q')" 
          by(simp add: eqvts)
        moreover from A ‹AQ ♯* x› FrxQ have "extractFrame([(x, z)] ∙ Q) = ⟨AQ', ΨQ⟩"
          by(clarsimp simp add: alpha' eqvts frame.inject fresh_list_cons name_swap)
        moreover from ‹AP ♯* Q› have "([(x, z)] ∙ AP) ♯* ([(x, z)] ∙ Q)"
          by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹AP ♯* x› ‹z ♯ AP› have "AP ♯* ([(x, z)] ∙ Q)" by simp
        moreover from ‹AQ' ♯* Q› have "([(x, z)] ∙ AQ') ♯* ([(x, z)] ∙ Q)"
          by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹x ♯ AQ'› ‹z ♯ AQ'› have "AQ' ♯* ([(x, z)] ∙ Q)" by simp
        ultimately have "Ψ ⊳ (P ∥ ([(x, z)] ∙ Q)) ⟼τ ≺ ⦇ν*(xvec1@xvec2)⦈(([(x, z)] ∙ [(x, y)] ∙ P') ∥ ([(x, z)] ∙ [(x, y)] ∙ Q'))"
          using MeqM' ‹M'=M''› ‹N=N'› ‹AP ♯* Ψ› ‹AP ♯* P›  ‹AP ♯* AQ'› ‹AQ' ♯* Ψ› ‹AQ' ♯* P› ‹(xvec1@xvec2) ♯* P› ‹AP ♯* M› ‹AQ' ♯* M''›
          by(rule_tac Comm1) (assumption | simp)+
        with‹z ♯ Ψ› have "Ψ ⊳ ⦇νz⦈(P ∥ ([(x, z)] ∙ Q)) ⟼τ ≺ ⦇νz⦈(⦇ν*(xvec1@xvec2)⦈(([(x, z)] ∙ [(x, y)] ∙ P') ∥ ([(x, z)] ∙ [(x, y)] ∙ Q')))"
          by(rule_tac Scope) auto
        moreover from ‹x ♯ P› ‹z ♯ P› ‹z ♯ Q› have "⦇νz⦈(P ∥ ([(x, z)] ∙ Q)) = ⦇νx⦈([(x, z)] ∙ (P ∥ ([(x, z)] ∙ Q)))"
          by(subst alphaRes[of x]) (auto simp add: calc_atm fresh_left name_swap)
        with ‹x ♯ P› ‹z ♯ P› have "⦇νz⦈(P ∥ ([(x, z)] ∙ Q)) = ⦇νx⦈(P ∥ Q)"
          by(simp add: eqvts)
        moreover from ‹z ≠ y› ‹x ≠ z› ‹z ♯ P'› ‹z ♯ [(x, y)] ∙ Q'› have "⦇νz⦈(⦇ν*(xvec1@xvec2)⦈(([(x, z)] ∙ [(x, y)] ∙ P') ∥ ([(x, z)] ∙ [(x, y)] ∙ Q'))) = ⦇νx⦈([(x, z)] ∙ (⦇ν*(xvec1@xvec2)⦈(([(x, z)] ∙ [(x, y)] ∙ P') ∥ ([(x, z)] ∙ [(x, y)] ∙ Q'))))"
          by(subst alphaRes[of x]) (auto simp add: resChainFresh fresh_left calc_atm name_swap)
        with ‹x ♯ xvec1› ‹x ♯ xvec2› ‹z ♯ xvec1› ‹z ♯ xvec2› have "⦇νz⦈(⦇ν*(xvec1@xvec2)⦈(([(x, z)] ∙ [(x, y)] ∙ P') ∥ ([(x, z)] ∙ [(x, y)] ∙ Q'))) = ⦇νx⦈(⦇ν*(xvec1@xvec2)⦈(([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q')))"
          by(simp add: eqvts)
        moreover from ‹x ♯ P'› ‹x ♯ Q'› ‹x ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec1› ‹y ♯ xvec2›
          have "⦇νx⦈(⦇ν*(xvec1@xvec2)⦈(([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q'))) =  ⦇νy⦈(⦇ν*(xvec1@xvec2)⦈(P' ∥ Q'))"
          by(subst alphaRes[of y]) (auto simp add: resChainFresh calc_atm eqvts fresh_left name_swap)
        ultimately have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼τ ≺ ⦇νy⦈(⦇ν*(xvec1@xvec2)⦈(P' ∥ Q'))"
          by simp
        moreover from ‹y ♯ Ψ› ‹(xvec1@xvec2) ♯* Ψ› ‹xvec=xvec1@y#xvec2›
        have "(Ψ, ⦇νy⦈(⦇ν*(xvec1@xvec2)⦈(P' ∥ Q')), ⦇ν*xvec⦈(P' ∥ Q')) ∈ Rel"
          by(force intro: C3 simp add: resChainAppend)
        ultimately show ?case by blast
      next
        case(cRes Q')   
        have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼M'⦇ν*xvec⦈⟨N⟩ ≺ Q'" by fact
        with ‹AQ ♯* Q› ‹AQ ♯* xvec› ‹xvec ♯* M'› ‹distinct xvec› have "AQ ♯* Q'"
          by(force dest: outputFreshChainDerivative)
        
        with ‹extractFrame(⦇νx⦈Q) = ⟨AQ, ΨQ⟩› have FrxQ: "⦇νx⦈(extractFrame Q) = ⟨AQ, ΨQ⟩" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(case_tac AQ) auto
        with ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* P'› ‹AQ ♯* ΨP› ‹AQ ♯* Q› ‹AQ ♯* xvec› ‹AQ ♯* M'› ‹AQ ♯* Q'›
        have "AQ' ♯* Ψ" and "AQ' ♯* P" and "AQ' ♯* ΨP" and "AQ' ♯* Q" and "AQ ♯* xvec" and "AQ ♯* Q'"
          and "y ♯ Ψ" and "y ♯ P" and "y ♯ P'" and "y ♯ ΨP" and "y ♯ Q" and "y ♯ xvec" and "y ♯ M'" and "y ♯ Q'"
          and "AQ' ♯* M'"
          by(simp)+
        from A ‹AP ♯* AQ› have "AP ♯* AQ'" and "y ♯ AP" by(simp add: fresh_star_list_cons)+
        from A ‹AQ ♯* x› have "x ≠ y" and "x ♯ AQ'" by(simp add: fresh_list_cons)+
        
        with A ‹distinct AQ› have "y ♯ AQ'" 
          by(induct AQ') (auto simp add: fresh_list_nil fresh_list_cons)

        from ‹x ♯ P› ‹y ♯ P› ‹x ≠ y› ‹Ψ ⊗ ΨQ ⊳ P ⟼M⦇N⦈ ≺ P'›
        have "Ψ ⊗ ΨQ ⊳ P ⟼M⦇([(y, x)] ∙ N)⦈ ≺ [(y, x)] ∙ P'"
          by(rule_tac xvec="[y]" in inputAlpha) (auto simp add: calc_atm)
        hence "Ψ ⊗ ΨQ ⊳ P ⟼M⦇([(x, y)] ∙ N)⦈ ≺ [(x, y)] ∙ P'"
          by(simp add: name_swap)
        moreover note FrP
        moreover from  ‹Ψ ⊗ ΨP ⊳ Q ⟼M'⦇ν*xvec⦈⟨N⟩ ≺ Q'› have "([(x, y)] ∙ (Ψ ⊗ ΨP)) ⊳ ([(x, y)] ∙ Q) ⟼([(x, y)] ∙ (M'⦇ν*xvec⦈⟨N⟩ ≺ Q'))" 
          by(rule semantics.eqvt)
        with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹x ♯ ΨP› ‹y ♯ ΨP› ‹x ♯ M'› ‹y ♯ M'› ‹x ♯ xvec› ‹y ♯ xvec›
        have "Ψ ⊗ ΨP ⊳ ([(x, y)] ∙ Q) ⟼M'⦇ν*xvec⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ Q')" 
          by(simp add: eqvts)
        moreover from A ‹AQ ♯* x› FrxQ have FrQ: "extractFrame([(x, y)] ∙ Q) = ⟨AQ', ΨQ⟩"
          by(clarsimp simp add: alpha' eqvts frame.inject fresh_list_cons name_swap)
        moreover from ‹AP ♯* Q› have "([(x, y)] ∙ AP) ♯* ([(x, y)] ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹AP ♯* x› ‹y ♯ AP› have "AP ♯* ([(x, y)] ∙ Q)" by simp
        moreover from ‹AQ' ♯* Q› have "([(x, y)] ∙ AQ') ♯* ([(x, y)] ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹x ♯ AQ'› ‹y ♯ AQ'› have "AQ' ♯* ([(x, y)] ∙ Q)" by simp
        ultimately have "Ψ ⊳ (P ∥ ([(x, y)] ∙ Q)) ⟼τ ≺ ⦇ν*xvec⦈([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q')"
          using MeqM' ‹AP ♯* Ψ› ‹AP ♯* P›  ‹AP ♯* AQ'› ‹AQ' ♯* Ψ› ‹AQ' ♯* P› ‹xvec ♯* P› ‹AP ♯* M› ‹AQ' ♯* M'›
          by(rule_tac Comm1) (assumption | simp)+
        with‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) ⟼τ ≺ ⦇νy⦈(⦇ν*xvec⦈(([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q')))"
          by(rule_tac Scope) auto
        moreover from ‹x ♯ P› ‹y ♯ P› ‹y ♯ Q› have "⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) = ⦇νx⦈([(x, y)] ∙ (P ∥ ([(x, y)] ∙ Q)))"
          by(subst alphaRes[of x]) (auto simp add: calc_atm fresh_left name_swap)
        with ‹x ♯ P› ‹y ♯ P› have "⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) = ⦇νx⦈(P ∥ Q)"
          by(simp add: eqvts)
        moreover from ‹y ♯ P'› ‹y ♯ Q'› ‹x ♯ xvec› ‹y ♯ xvec› have "⦇νy⦈(⦇ν*xvec⦈(([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q'))) =  ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))"
          by(subst alphaRes[of y]) (auto simp add: resChainFresh calc_atm eqvts fresh_left name_swap)
        ultimately have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼τ ≺ ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))"
          by simp
        moreover from ‹x ♯ Ψ› ‹x ♯ P'› ‹xvec ♯* Ψ› have "(Ψ, ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q')), ⦇ν*xvec⦈(P' ∥ ⦇νx⦈Q')) ∈ Rel"
          by(rule C2)
        ultimately show ?case by blast
      qed
    next
      case(cComm2 ΨQ M xvec N P' AP ΨP K xQ' AQ)
      have QTrans: "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼K⦇N⦈ ≺ xQ'" and FrQ: "extractFrame(⦇νx⦈Q) = ⟨AQ, ΨQ⟩" by fact+
      have PTrans: "Ψ ⊗ ΨQ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact+
      from PTrans ‹x ♯ P› have "x ♯ N" and "x ♯ P'" using ‹xvec ♯* x› ‹xvec ♯* M› ‹distinct xvec› 
        by(force intro: outputFreshDerivative)+
      have "x ♯ ⦇νx⦈Q" by(simp add: abs_fresh)
      with FrQ ‹AQ ♯* x› have "x ♯ ΨQ"
        by(drule_tac extractFrameFresh) auto
      from ‹x ♯ P› FrP ‹AP ♯* x› have "x ♯ ΨP"
        by(drule_tac extractFrameFresh) auto
      from ‹AP ♯* ⦇νx⦈Q› ‹AP ♯* x› have "AP ♯* Q" by simp
      from ‹AQ ♯* ⦇νx⦈Q› ‹AQ ♯* x› have "AQ ♯* Q" by simp
      from ‹xvec ♯* x› ‹xvec ♯* ⦇νx⦈Q› have "xvec ♯* Q" by simp

      from PTrans FrP ‹distinct AP› ‹x ♯ P› ‹AQ ♯* P› ‹AP ♯* Ψ› ‹AP ♯* ΨQ› ‹AP ♯* x› ‹AP ♯* AQ› ‹AP ♯* P›  ‹AP ♯* M› ‹xvec ♯* M› ‹distinct xvec›
      obtain M' where "(Ψ ⊗ ΨQ) ⊗ ΨP ⊢ M ↔ M'" and "x ♯ M'" and "AQ ♯* M'"
        by(rule_tac B="x#AQ" in obtainPrefix) (assumption | force simp add: fresh_star_list_cons)+
      hence MeqM': "Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ M'"
        by(metis statEqEnt Associativity Commutativity Composition)
      with ‹Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ K› have "Ψ ⊗ ΨP ⊗ ΨQ ⊢ K ↔ M'"
        by(blast intro: chanEqTrans chanEqSym)
      hence "(Ψ ⊗ ΨP) ⊗ ΨQ ⊢ K ↔ M'"
        by(metis statEqEnt Associativity Commutativity Composition)
      with QTrans FrQ ‹distinct AQ› ‹AQ ♯* Ψ› ‹AQ ♯* ΨP› ‹AQ ♯* (⦇νx⦈Q)› ‹AQ ♯* K› ‹AQ ♯* M'›
      have "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M'⦇N⦈ ≺ xQ'" by(force intro: inputRenameSubject)

      moreover from ‹x ♯ Ψ› ‹x ♯ ΨP› have "x ♯ Ψ ⊗ ΨP" by force
      moreover note ‹x ♯ M'› ‹x ♯ N› 
      moreover from QTrans ‹x ♯ N› have "x ♯ xQ'" by(force dest: inputFreshDerivative simp add: abs_fresh)
      ultimately show ?case
      proof(induct rule: resInputCases)
        case(cRes Q')   
        have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼M'⦇N⦈ ≺ Q'" by fact
        with ‹AQ ♯* Q› ‹AQ ♯* N› have "AQ ♯* Q'"
          by(rule_tac inputFreshChainDerivative)

        with ‹extractFrame(⦇νx⦈Q) = ⟨AQ, ΨQ⟩› have FrxQ: "⦇νx⦈(extractFrame Q) = ⟨AQ, ΨQ⟩" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(case_tac AQ) auto
        with ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* P'› ‹AQ ♯* ΨP› ‹AQ ♯* Q› ‹AQ ♯* xvec› ‹AQ ♯* M'› ‹AQ ♯* Q'› ‹AQ ♯* N›
        have "AQ' ♯* Ψ" and "AQ' ♯* P" and "AQ' ♯* ΨP" and "AQ' ♯* Q" and "AQ ♯* xvec" and "AQ ♯* Q'"
          and "y ♯ Ψ" and "y ♯ P" and "y ♯ P'" and "y ♯ ΨP" and "y ♯ Q" and "y ♯ xvec" and "y ♯ M'" and "y ♯ Q'" and "y ♯ N"
          and "AQ' ♯* M'"
          by(simp)+
        from A ‹AP ♯* AQ› have "AP ♯* AQ'" and "y ♯ AP" by(simp add: fresh_star_list_cons)+
        from A ‹AQ ♯* x› have "x ≠ y" and "x ♯ AQ'" by(simp add: fresh_list_cons)+
        
        with A ‹distinct AQ› have "y ♯ AQ'" 
          by(induct AQ') (auto simp add: fresh_list_nil fresh_list_cons)

        note PTrans FrP
        moreover from  ‹Ψ ⊗ ΨP ⊳ Q ⟼M'⦇N⦈ ≺ Q'› have "([(x, y)] ∙ (Ψ ⊗ ΨP)) ⊳ ([(x, y)] ∙ Q) ⟼([(x, y)] ∙ (M'⦇N⦈ ≺ Q'))" 
          by(rule semantics.eqvt)
        with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹x ♯ ΨP› ‹y ♯ ΨP› ‹x ♯ M'› ‹y ♯ M'› ‹x ♯ N› ‹y ♯ N›
        have "Ψ ⊗ ΨP ⊳ ([(x, y)] ∙ Q) ⟼M'⦇N⦈ ≺ ([(x, y)] ∙ Q')" 
          by(simp add: eqvts)
        moreover from A ‹AQ ♯* x› FrxQ have FrQ: "extractFrame([(x, y)] ∙ Q) = ⟨AQ', ΨQ⟩" and "y ♯ extractFrame Q"
          by(clarsimp simp add: alpha' eqvts frame.inject fresh_list_cons name_swap)+
        moreover from ‹AP ♯* Q› have "([(x, y)] ∙ AP) ♯* ([(x, y)] ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹AP ♯* x› ‹y ♯ AP› have "AP ♯* ([(x, y)] ∙ Q)" by simp
        moreover from ‹AQ' ♯* Q› have "([(x, y)] ∙ AQ') ♯* ([(x, y)] ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹x ♯ AQ'› ‹y ♯ AQ'› have "AQ' ♯* ([(x, y)] ∙ Q)" by simp
        moreover from ‹xvec ♯* Q› have "([(x, y)] ∙ xvec) ♯* ([(x, y)] ∙ Q)" by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
        with ‹xvec ♯* x› ‹y ♯ xvec› have "xvec ♯* ([(x, y)] ∙ Q)" by simp
        ultimately have "Ψ ⊳ (P ∥ ([(x, y)] ∙ Q)) ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ ([(x, y)] ∙ Q'))"
          using MeqM' ‹AP ♯* Ψ› ‹AP ♯* P›  ‹AP ♯* AQ'› ‹AQ' ♯* Ψ› ‹AQ' ♯* P› ‹AP ♯* M› ‹AQ' ♯* M'›
          by(rule_tac Comm2) (assumption | simp)+
        with‹y ♯ Ψ› have "Ψ ⊳ ⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) ⟼τ ≺ ⦇νy⦈(⦇ν*xvec⦈(P' ∥ ([(x, y)] ∙ Q')))"
          by(rule_tac Scope) auto
        moreover from ‹x ♯ P› ‹y ♯ P› ‹y ♯ Q› have "⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) = ⦇νx⦈([(x, y)] ∙ (P ∥ ([(x, y)] ∙ Q)))"
          by(subst alphaRes[of x]) (auto simp add: calc_atm fresh_left name_swap)
        with ‹x ♯ P› ‹y ♯ P› have "⦇νy⦈(P ∥ ([(x, y)] ∙ Q)) = ⦇νx⦈(P ∥ Q)"
          by(simp add: eqvts)
        moreover from ‹x ♯ P'› ‹y ♯ P'› ‹y ♯ Q'› ‹xvec ♯* x› ‹y ♯ xvec› have "⦇νy⦈(⦇ν*xvec⦈(P' ∥ ([(x, y)] ∙ Q'))) =  ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))"
          by(subst alphaRes[of y]) (auto simp add: resChainFresh calc_atm eqvts fresh_left name_swap)
        ultimately have "Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼τ ≺ ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))"
          by simp
        moreover from ‹x ♯ Ψ› ‹x ♯ P'› ‹xvec ♯* Ψ› have "(Ψ, ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q')), ⦇ν*xvec⦈(P' ∥ ⦇νx⦈Q')) ∈ Rel"
          by(rule C2)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

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

  assumes "x ♯ P"
  and     "x ♯ Ψ"
  and     "eqvt Rel"
  and     C1: "⋀Ψ' R. (Ψ, R, R) ∈ Rel"
  and     C2: "⋀y Ψ' R S zvec. ⟦y ♯ Ψ'; y ♯ R; zvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*zvec⦈(R ∥ ⦇νy⦈S), ⦇νy⦈(⦇ν*zvec⦈(R ∥ S))) ∈ Rel"

  shows "Ψ ⊳ P ∥ ⦇νx⦈Q ↝[Rel] ⦇νx⦈(P ∥ Q)"
proof -
  note ‹eqvt Rel› ‹x ♯ Ψ›
  moreover from ‹x ♯ P› have "x ♯ P ∥ ⦇νx⦈Q" by(simp add: abs_fresh)
  moreover from ‹x ♯ P› have "x ♯ ⦇νx⦈(P ∥ Q)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α xPQ)
    from ‹bn α ♯* (P ∥ ⦇νx⦈Q)› ‹x ♯ α› have "bn α  ♯* P" and "bn α  ♯* Q" by simp+
    note ‹Ψ ⊳ ⦇νx⦈(P ∥ Q) ⟼α ≺ xPQ› ‹x ♯ Ψ› ‹x ♯ α› ‹x ♯ xPQ› ‹bn α ♯* Ψ›
    moreover from ‹bn α ♯* P› ‹bn α ♯* Q› have "bn α ♯* (P ∥ Q)" by simp
    ultimately show ?case using ‹bn α ♯* subject α› ‹x ♯ α›
    proof(induct rule: resCases)
      case(cOpen M xvec1 xvec2 y N PQ)
      from ‹x ♯ M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩› have "x ♯ xvec1" and "x ≠ y" and "x ♯ xvec2" and "x ♯ M" by simp+
      from ‹xvec1 ♯* (P ∥ Q)› ‹xvec2 ♯* (P ∥ Q)› ‹y ♯ (P ∥ Q)›
      have "(xvec1@xvec2) ♯* P" and "(xvec1@xvec2) ♯* Q" and "y ♯ P" and "y ♯ Q"
        by simp+
      from ‹Ψ ⊳ P ∥ Q ⟼ M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ PQ)›
      have "([(x, y)] ∙ Ψ) ⊳ ([(x, y)] ∙ (P ∥ Q)) ⟼ ([(x, y)] ∙ (M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)] ∙ N)⟩ ≺ ([(x, y)] ∙ PQ)))"
        by(rule semantics.eqvt)
      with ‹x ♯ Ψ› ‹y ♯ Ψ› ‹x ♯ P› ‹y ♯ P› ‹x ♯ M› ‹y ♯ M› ‹x ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec1› ‹y ♯ xvec2›
      have "Ψ ⊳ P ∥ ([(x, y)] ∙ Q) ⟼ M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ PQ"
        by(simp add: eqvts)
      moreover from ‹xvec1 ♯* Ψ› ‹xvec2 ♯* Ψ› have "(xvec1@xvec2) ♯* Ψ" by simp
      moreover note ‹(xvec1@xvec2) ♯* P›
      moreover from ‹(xvec1@xvec2) ♯* Q› have "([(x, y)] ∙ (xvec1@xvec2)) ♯* ([(x, y)] ∙ Q)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with ‹x ♯ xvec1› ‹x ♯ xvec2› ‹y ♯ xvec1› ‹y ♯ xvec2› have "(xvec1@xvec2) ♯* ([(x, y)] ∙ Q)"
        by(auto simp add: eqvts)
      moreover from ‹xvec1 ♯* M› ‹xvec2 ♯* M› have "(xvec1@xvec2) ♯* M" by simp
      ultimately show ?case
      proof(induct rule: parOutputCases[where C=y])
        case(cPar1 P' AQ ΨQ)
        from ‹y ♯ xvec1› ‹y ♯ xvec2› have "y ♯ (xvec1@xvec2)" by(auto simp add: fresh_list_append)
        with ‹Ψ ⊗ ΨQ ⊳ P ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ P'› ‹(xvec1@xvec2) ♯* M› ‹y ♯ P› 
             ‹distinct xvec1› ‹distinct xvec2› ‹xvec1 ♯* xvec2› 
        have "y ♯ N" by(force intro: outputFreshDerivative)
        with ‹y ∈ supp N› have False by(simp add: fresh_def)
        thus ?case by simp
      next
        case(cPar2 Q' AP ΨP)
        have FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact
        with ‹y ♯ P› ‹AP ♯* y› have "y ♯ ΨP" 
          apply(drule_tac extractFrameFresh)
          by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from ‹Ψ ⊗ ΨP ⊳ ([(x, y)] ∙ Q) ⟼M⦇ν*(xvec1@xvec2)⦈⟨N⟩ ≺ Q'› ‹y ∈ supp N› ‹y ♯ Ψ› ‹y ♯ ΨP› ‹y ♯ M› ‹y ♯ xvec1› ‹y ♯ xvec2›
        have "Ψ ⊗ ΨP ⊳ ⦇νy⦈(([(x, y)] ∙ Q)) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ Q'" by(force intro: Open) 
        with ‹y ♯ Q› have "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ Q'"
          by(simp add: alphaRes)
        moreover from ‹AP ♯* ([(x, y)] ∙ Q)› have "AP ♯* ⦇νy⦈([(x, y)] ∙ Q)" by(auto simp add: fresh_star_def abs_fresh)
        with ‹y ♯ Q› have "AP ♯* ⦇νx⦈Q" by(simp add: alphaRes)
        ultimately have "Ψ ⊳ P ∥ (⦇νx⦈Q) ⟼M⦇ν*(xvec1@y#xvec2)⦈⟨N⟩ ≺ (P ∥ Q')" 
          using FrP ‹(xvec1@xvec2) ♯* P› ‹AP ♯* Ψ› ‹AP ♯* M› ‹y ♯ P› ‹AP ♯* (xvec1@xvec2)› ‹AP ♯* y› ‹AP ♯* N›
          by(rule_tac Par2) auto
        moreover have "(Ψ, P ∥ Q', P ∥ Q') ∈ Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    next
      case(cRes PQ)
      from ‹Ψ ⊳ P ∥ Q ⟼α ≺ PQ› ‹bn α ♯* Ψ›  ‹bn α ♯* P› ‹bn α ♯* Q› ‹bn α ♯* subject α›
      show ?case
      proof(induct rule: parCases[where C=x])
        case(cPar1 P' AQ ΨQ)
        note ‹Ψ ⊗ ΨQ ⊳ P ⟼α ≺ P'›
        moreover with ‹x ♯ P› ‹x ♯ α› ‹bn α ♯* subject α› ‹distinct(bn α)›
        have "x ♯ P'" by(force dest: freeFreshDerivative)
        with ‹extractFrame Q = ⟨AQ, ΨQ⟩› have "extractFrame(⦇νx⦈Q) = ⟨(x#AQ), ΨQ⟩"
          by simp
        moreover from ‹bn α ♯* Q› have "bn α ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
        moreover from ‹x ♯ Ψ› ‹AQ ♯* Ψ› have "(x#AQ) ♯* Ψ" by simp
        moreover from ‹x ♯ P› ‹AQ ♯* P› have "(x#AQ) ♯* P" by simp
        moreover from ‹x ♯ α› ‹AQ ♯* α› have "(x#AQ) ♯* α" by simp
        ultimately have "Ψ ⊳ P ∥ ⦇νx⦈Q ⟼α ≺ (P' ∥ ⦇νx⦈Q)"
          by(rule Par1)
        moreover from ‹x ♯ P'› ‹x ♯ Ψ› have "(Ψ, ⦇ν*[]⦈(P' ∥ (⦇νx⦈Q)), ⦇νx⦈(⦇ν*[]⦈(P' ∥ Q))) ∈ Rel"
          by(rule_tac C2) auto
        ultimately show ?case
          by force
      next
        case(cPar2 Q' AP ΨP)
        have FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact
        with ‹x ♯ P› ‹AP ♯* x› have "x ♯ ΨP"
          apply(drule_tac extractFrameFresh)
          by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from ‹Ψ ⊗ ΨP ⊳ Q ⟼α ≺ Q'› ‹x ♯ Ψ› ‹x ♯ ΨP› ‹x ♯ α›
        have "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼α ≺ ⦇νx⦈Q'"
          by(rule_tac Scope) auto
        moreover note FrP ‹bn α ♯* P› ‹AP ♯* Ψ›
        moreover from ‹AP ♯* Q› have "AP ♯* ⦇νx⦈Q" by(simp add: fresh_star_def abs_fresh)
        ultimately have "Ψ ⊳ P ∥ ⦇νx⦈Q ⟼α ≺ (P ∥ ⦇νx⦈Q')" using ‹AP ♯* α›
          by(rule Par2)
        moreover from ‹x ♯ P› ‹x ♯ Ψ› have "(Ψ, ⦇ν*[]⦈(P ∥ (⦇νx⦈Q')), ⦇νx⦈(⦇ν*[]⦈(P ∥ Q'))) ∈ Rel"
          by(rule_tac C2) auto
        ultimately show ?case
          by force
      next
        case(cComm1 ΨQ M N P' AP ΨP K xvec Q' AQ)
        have PTrans: "Ψ ⊗ ΨQ ⊳ P ⟼M⦇N⦈ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact+
        have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼K⦇ν*xvec⦈⟨N⟩ ≺ Q'" and FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact+
        from FrP ‹x ♯ P› have "x ♯ ⟨AP, ΨP⟩" by(drule_tac extractFrameFresh) simp
        with ‹AP ♯* x› have "x ♯ ΨP" by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from PTrans FrP ‹distinct AP› ‹x ♯ P› ‹AP ♯* Ψ› ‹AP ♯* ΨQ› ‹AP ♯* x› ‹AP ♯* P› ‹AP ♯* M› ‹AQ ♯* P› ‹AP ♯* AQ›
        obtain M' where MeqM': "(Ψ ⊗ ΨQ) ⊗ ΨP ⊢ M ↔ M'" and "x ♯ M'" and "AQ ♯* M'"
          by(rule_tac B="x#AQ" in obtainPrefix) (assumption | force simp add: fresh_star_list_cons)+
        
        from MeqM' have MeqM': "Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ M'"
          by(metis statEqEnt Associativity Composition Commutativity)
        with ‹Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ K› have "Ψ ⊗ ΨP ⊗ ΨQ ⊢ K ↔ M'"
          by(blast intro: chanEqTrans chanEqSym)
        hence "(Ψ ⊗ ΨP) ⊗ ΨQ ⊢ K ↔ M'"
          by(metis statEqEnt Associativity Composition Commutativity)
        with QTrans FrQ ‹distinct AQ› have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼M'⦇ν*xvec⦈⟨N⟩ ≺ Q'" using ‹AQ ♯* Ψ› ‹AQ ♯* ΨP› ‹AQ ♯* Q› ‹AQ ♯* K› ‹AQ ♯* M'›
          by(rule_tac outputRenameSubject) (assumption | force)+
        show ?case
        proof(case_tac "x ∈ supp N")
          note PTrans FrP
          moreover assume "x ∈ supp N"
          hence "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M'⦇ν*([]@(x#xvec))⦈⟨N⟩ ≺ Q'" using QTrans ‹x ♯ Ψ› ‹x ♯ ΨP› ‹x ♯ M'› ‹xvec ♯* x›
            by(rule_tac Open) (assumption | force simp add: fresh_list_nil)+
          hence QTrans: "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M'⦇ν*(x#xvec)⦈⟨N⟩ ≺ Q'" by simp
          moreover from ‹extractFrame Q = ⟨AQ, ΨQ⟩› have "extractFrame(⦇νx⦈Q) = ⟨(x#AQ), ΨQ⟩" 
            by simp
          moreover note MeqM' ‹AP ♯* Ψ› ‹AP ♯* P›
          moreover from  ‹AP ♯* Q› have "AP ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
          moreover from ‹AP ♯* AQ› ‹AP ♯* x› have "AP ♯* (x#AQ)" 
            by(simp add: fresh_star_def fresh_list_cons) (auto simp add: fresh_def name_list_supp)
          moreover from ‹x ♯ Ψ› ‹AQ ♯* Ψ› have "(x#AQ) ♯* Ψ" by simp
          moreover from ‹x ♯ P› ‹AQ ♯* P› have "(x#AQ) ♯* P" by simp
          moreover from ‹x ♯ M'› ‹AQ ♯* M'› have "(x#AQ) ♯* M'" by simp
          moreover from ‹AQ ♯* Q› have "(x#AQ) ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
          moreover from ‹x ♯ P› ‹xvec ♯* P› have "(x#xvec) ♯* P" by(simp)
          ultimately have "Ψ ⊳ P ∥ ⦇νx⦈Q ⟼τ ≺ ⦇ν*(x#xvec)⦈(P' ∥ Q')" using ‹AP ♯* M›
            by(rule_tac Comm1) (assumption | simp)+
          moreover have "(Ψ, ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q')), ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))) ∈ Rel" by(rule C1)
          ultimately show ?case by force
        next
          note PTrans FrP
          moreover assume "x ∉ supp N"
          hence "x ♯ N" by(simp add: fresh_def)
          with QTrans ‹x ♯ Ψ› ‹x ♯ ΨP› ‹x ♯ M'› ‹xvec ♯* x›
          have QTrans: "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M'⦇ν*xvec⦈⟨N⟩ ≺ ⦇νx⦈Q'"
            by(rule_tac Scope) (assumption | force)+
          moreover from PTrans ‹x ♯ P› ‹x ♯ N› have "x ♯ P'" by(rule inputFreshDerivative)
          with ‹extractFrame Q = ⟨AQ, ΨQ⟩› have "extractFrame(⦇νx⦈Q) = ⟨(x#AQ), ΨQ⟩"
            by simp
          moreover note MeqM' ‹AP ♯* Ψ› ‹AP ♯* P›
          moreover from  ‹AP ♯* Q› have "AP ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
          moreover from ‹AP ♯* AQ› ‹AP ♯* x› have "AP ♯* (x#AQ)" 
            by(simp add: fresh_star_def fresh_list_cons) (auto simp add: fresh_def name_list_supp)
          moreover from ‹x ♯ Ψ› ‹AQ ♯* Ψ› have "(x#AQ) ♯* Ψ" by simp
          moreover from ‹x ♯ P› ‹AQ ♯* P› have "(x#AQ) ♯* P" by simp
          moreover from ‹x ♯ M'› ‹AQ ♯* M'› have "(x#AQ) ♯* M'" by simp
          moreover from ‹AQ ♯* Q› have "(x#AQ) ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
          moreover from ‹x ♯ P› ‹xvec ♯* P› have "(x#xvec) ♯* P" by(simp)
          ultimately have "Ψ ⊳ P ∥ ⦇νx⦈Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ ⦇νx⦈Q')" using ‹AP ♯* M›
            by(rule_tac Comm1) (assumption | simp)+
          moreover from ‹x ♯ Ψ› ‹x ♯ P'› ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ ⦇νx⦈Q'), ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))) ∈ Rel" by(rule C2)
          ultimately show ?case by blast
        qed
      next
        case(cComm2 ΨQ M xvec N P' AP ΨP K Q' AQ)
        have PTrans: "Ψ ⊗ ΨQ ⊳ P ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'" and FrP: "extractFrame P = ⟨AP, ΨP⟩" by fact+
        have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼K⦇N⦈ ≺ Q'" and FrQ: "extractFrame Q = ⟨AQ, ΨQ⟩" by fact+
        from FrP ‹x ♯ P› have "x ♯ ⟨AP, ΨP⟩" by(drule_tac extractFrameFresh) simp
        with ‹AP ♯* x› have "x ♯ ΨP" by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from PTrans FrP ‹distinct AP› ‹x ♯ P› ‹AP ♯* Ψ› ‹AP ♯* ΨQ› ‹AP ♯* x› ‹AP ♯* P› ‹AP ♯* M› ‹AQ ♯* P› ‹AP ♯* AQ› ‹xvec ♯* M› ‹distinct xvec›
        obtain M' where MeqM': "(Ψ ⊗ ΨQ) ⊗ ΨP ⊢ M ↔ M'" and "x ♯ M'" and "AQ ♯* M'"
          by(rule_tac B="x#AQ" in obtainPrefix) (assumption | force simp add: fresh_star_list_cons)+
        
        from MeqM' have MeqM': "Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ M'"
          by(metis statEqEnt Associativity Commutativity Composition)
        with ‹Ψ ⊗ ΨP ⊗ ΨQ ⊢ M ↔ K› have "Ψ ⊗ ΨP ⊗ ΨQ ⊢ K ↔ M'"
          by(blast intro: chanEqTrans chanEqSym)
        hence "(Ψ ⊗ ΨP) ⊗ ΨQ ⊢ K ↔ M'"
          by(metis statEqEnt Associativity Commutativity Composition)
        with QTrans FrQ ‹distinct AQ› have QTrans: "Ψ ⊗ ΨP ⊳ Q ⟼M'⦇N⦈ ≺ Q'" using ‹AQ ♯* Ψ› ‹AQ ♯* ΨP› ‹AQ ♯* Q› ‹AQ ♯* K› ‹AQ ♯* M'›
          by(rule_tac inputRenameSubject) (assumption | force)+

        from PTrans ‹x ♯ P› ‹xvec ♯* x› ‹distinct xvec› ‹xvec ♯* M›
        have "x ♯ N" and "x ♯ P'" by(force intro: outputFreshDerivative)+
        from QTrans ‹x ♯ Ψ›  ‹x ♯ ΨP› ‹x ♯ M'› ‹x ♯ N› have QTrans: "Ψ ⊗ ΨP ⊳ ⦇νx⦈Q ⟼M'⦇N⦈ ≺ ⦇νx⦈Q'"
          by(rule_tac Scope) (assumption | force)+

        note PTrans FrP QTrans
        moreover with ‹extractFrame Q = ⟨AQ, ΨQ⟩› have "extractFrame(⦇νx⦈Q) = ⟨(x#AQ), ΨQ⟩"
          by simp
        moreover note MeqM' ‹AP ♯* Ψ› ‹AP ♯* P›
        moreover from  ‹AP ♯* Q› have "AP ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
        moreover from ‹AP ♯* AQ› ‹AP ♯* x› have "AP ♯* (x#AQ)" 
          by(simp add: fresh_star_def fresh_list_cons) (auto simp add: fresh_def name_list_supp)
        moreover from ‹x ♯ Ψ› ‹AQ ♯* Ψ› have "(x#AQ) ♯* Ψ" by simp
        moreover from ‹x ♯ P› ‹AQ ♯* P› have "(x#AQ) ♯* P" by simp
        moreover from ‹x ♯ M'› ‹AQ ♯* M'› have "(x#AQ) ♯* M'" by simp
        moreover from ‹AQ ♯* Q› have "(x#AQ) ♯* (⦇νx⦈Q)" by(simp add: fresh_star_def abs_fresh)
        moreover from ‹xvec ♯* Q› have "(x#xvec) ♯* (⦇νx⦈Q)" by(simp add: abs_fresh fresh_star_def)
        ultimately have "Ψ ⊳ P ∥ ⦇νx⦈Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ ⦇νx⦈Q')" using ‹AP ♯* M›
          by(rule_tac Comm2) (assumption | simp)+
        moreover from ‹x ♯ Ψ› ‹x ♯ P'› ‹xvec ♯* Ψ› have "(Ψ, ⦇ν*xvec⦈(P' ∥ ⦇νx⦈Q'), ⦇νx⦈(⦇ν*xvec⦈(P' ∥ Q'))) ∈ Rel" by(rule C2)
        ultimately show ?case by blast
      qed
    qed
  qed
qed

lemma simParComm:
  fixes Ψ   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b × ('a, 'b, 'c) psi × ('a, 'b, 'c) psi) set"
  
  assumes "eqvt Rel"
  and     C1: "⋀Ψ' R S. (Ψ', R ∥ S, S ∥ R) ∈ Rel"
  and     C2: "⋀Ψ' R S xvec. ⟦(Ψ', R, S) ∈ Rel; xvec ♯* Ψ'⟧ ⟹ (Ψ', ⦇ν*xvec⦈R, ⦇ν*xvec⦈S) ∈ Rel"

  shows "Ψ ⊳ P ∥ Q ↝[Rel] Q ∥ P"
using ‹eqvt Rel›
proof(induct rule: simI[of _ _ _ _ "()"])
  case(cSim α PQ)
  from ‹bn α ♯* (P ∥ Q)› have "bn α ♯* Q" and "bn α ♯* P" by simp+
  with ‹Ψ ⊳ Q ∥ P ⟼α ≺ PQ› ‹bn α ♯* Ψ› show ?case using ‹bn α ♯* subject α›
  proof(induct rule: parCases[where C="()"])
    case(cPar1 Q' AP ΨP)
    from ‹Ψ ⊗ ΨP ⊳ Q ⟼α≺ Q'› ‹extractFrame P = ⟨AP, ΨP⟩› ‹bn α ♯* P› ‹AP ♯* Ψ› ‹AP ♯* Q› ‹AP ♯* α› 
    have "Ψ ⊳ P ∥ Q ⟼α ≺ (P ∥ Q')" by(rule Par2)
    moreover have "(Ψ, P ∥ Q', Q' ∥ P) ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case(cPar2 P' AQ ΨQ)
    from ‹Ψ ⊗ ΨQ ⊳ P ⟼α ≺ P'› ‹extractFrame Q = ⟨AQ, ΨQ⟩› ‹bn α ♯* Q› ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* α› 
    have "Ψ ⊳ P ∥ Q ⟼α ≺ (P' ∥ Q)" by(rule Par1)
    moreover have "(Ψ, P' ∥ Q, Q ∥ P') ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case(cComm1 ΨP M N Q' AQ ΨQ K xvec P' AP)
    note ‹Ψ ⊗ ΨQ ⊳ P ⟼K⦇ν*xvec⦈⟨N⟩ ≺ P'› ‹extractFrame P = ⟨AP, ΨP⟩›
         ‹Ψ ⊗ ΨP ⊳ Q ⟼M⦇N⦈ ≺ Q'› ‹extractFrame Q = ⟨AQ, ΨQ⟩›
    moreover from ‹Ψ ⊗ ΨQ ⊗ ΨP ⊢ M ↔ K›
    have "Ψ ⊗ ΨQ ⊗ ΨP ⊢ K ↔ M"
      by(rule chanEqSym)
    hence "Ψ ⊗ ΨP ⊗ ΨQ ⊢ K ↔ M"
      by(blast intro: statEqEnt compositionSym Commutativity)
    ultimately have "Ψ ⊳ P ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')"
      using ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* Q› ‹AQ ♯* AP› ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* Q› ‹xvec ♯* Q› ‹AP ♯* K› ‹AQ ♯* M›
      by(rule_tac Comm2) (assumption | simp)+
    moreover have "(Ψ, P' ∥ Q', Q' ∥ P') ∈ Rel" by(rule C1)
    hence "(Ψ, ⦇ν*xvec⦈(P' ∥ Q'), ⦇ν*xvec⦈(Q' ∥ P')) ∈ Rel" using ‹xvec ♯* Ψ› by(rule C2)
    ultimately show ?case by blast
  next
    case(cComm2 ΨP M xvec N Q' AQ ΨQ K P' AP)
    note ‹Ψ ⊗ ΨQ ⊳ P ⟼K⦇N⦈ ≺ P'› ‹extractFrame P = ⟨AP, ΨP⟩›
         ‹Ψ ⊗ ΨP ⊳ Q ⟼M⦇ν*xvec⦈⟨N⟩ ≺ Q'› ‹extractFrame Q = ⟨AQ, ΨQ⟩›
    moreover from ‹Ψ ⊗ ΨQ ⊗ ΨP ⊢ M ↔ K›
    have "Ψ ⊗ ΨQ ⊗ ΨP ⊢ K ↔ M"
      by(rule chanEqSym)
    hence "Ψ ⊗ ΨP ⊗ ΨQ ⊢ K ↔ M"
      by(blast intro: statEqEnt compositionSym Commutativity)
    ultimately have "Ψ ⊳ P ∥ Q ⟼τ ≺ ⦇ν*xvec⦈(P' ∥ Q')"
      using ‹AP ♯* Ψ› ‹AP ♯* P› ‹AP ♯* Q› ‹AQ ♯* AP› ‹AQ ♯* Ψ› ‹AQ ♯* P› ‹AQ ♯* Q› ‹xvec ♯* P› ‹AP ♯* K› ‹AQ ♯* M›
      by(rule_tac Comm1) (assumption | simp add: freshChainSym)+
    moreover have "(Ψ, P' ∥ Q', Q' ∥ P') ∈ Rel" by(rule C1)
    hence "(Ψ, ⦇ν*xvec⦈(P' ∥ Q'), ⦇ν*xvec⦈(Q' ∥ P')) ∈ Rel" using ‹xvec ♯* Ψ› by(rule C2)
    ultimately show ?case by blast
  qed
qed

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

  assumes "guarded P"
  and     "⋀Ψ' Q. (Ψ', Q, Q) ∈ Rel"

  shows "Ψ ⊳ !P ↝[Rel] P ∥ !P"
using assms
by(auto simp add: simulation_def dest: Bang)

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

  assumes C1: "⋀Ψ' Q. (Ψ', Q, Q) ∈ Rel"

  shows "Ψ ⊳ P ∥ !P ↝[Rel] !P"
proof(auto simp add: simulation_def)
  fix α P'
  assume "Ψ ⊳ !P ⟼α ≺ P'"
  hence "Ψ ⊳ P ∥ !P ⟼α ≺ P'"
    apply -
    by(ind_cases "Ψ ⊳ !P ⟼α ≺ P'") (auto simp add: psi.inject)
  moreover have "(Ψ, P', P') ∈ Rel" by(rule C1)
  ultimately show "∃P''. Ψ ⊳ P ∥ !P ⟼α ≺ P'' ∧ (Ψ, P'', P') ∈ Rel"
    by blast
qed

end

end