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'. ⟦