Theory Sim_Struct_Cong

theory Sim_Struct_Cong
  imports Simulation "HOL-Library.Multiset"
begin

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

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

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

lemma partitionListRight:

assumes "xs@ys=xs'@y#ys'"
  and   "y  set 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 resOutputCases''''[consumes 8, case_names cOpen cRes]:
  fixes Ψ    :: 'b
    and x    :: name
    and zvec :: "name list"
    and P    :: "('a, 'b, 'c) psi"
    and α    :: "'a action"
    and P'   :: "('a, 'b, 'c) psi"
    and C    :: "'f::fs_name"

assumes Trans: "Ψ  ⦇νxP α  P'"
  and   1: "x  Ψ"
  and   2: "x  α"
  and   3: "x  P'"
  and   4: "bn α ♯* Ψ"
  and   5: "bn α ♯* P"
  and   6: "bn α ♯* subject α"
  and   "α = M⦇ν*zvec⦈⟨N"
  and   rOpen: "M xvec yvec y N P'. Ψ  ([(x, y)]  P) M⦇ν*(xvec@yvec)⦈⟨N  P'; y  supp N;
                                         x  N; x  P'; x  y; y  xvec; y  yvec; y  M; distinct xvec; distinct yvec;
                                         xvec ♯* Ψ; y  Ψ; yvec ♯* Ψ; xvec ♯* P; y  P; yvec ♯* P; xvec ♯* M; y  M;
                                         yvec ♯* M; xvec ♯* yvec 
                                         Prop (M⦇ν*(xvec@y#yvec)⦈⟨N) P'"
  and   rScope:  "P'. Ψ  P α  P'  Prop α (⦇νxP')"

shows "Prop α P'"
proof -
  from Trans have "distinct (bn α)" by(auto dest: boundOutputDistinct)
  show ?thesis using Trans 1 2 3 4 5 6 α=M⦇ν*zvec⦈⟨N rOpen rScope
  proof(induct rule: resCases'[where C="(zvec, C)"])
    case cBrOpen
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case cRes
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case cBrClose
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case(cOpen M' xvec yvec y N' P')
    show ?case
      using Ψ  [(x, y)]  P  M'⦇ν*(xvec @ yvec)⦈⟨N'  P' y  supp N' x  N' x  P'
        x  y y  xvec y  yvec y  M' distinct xvec distinct yvec xvec ♯* Ψ
        y  Ψ yvec ♯* Ψ xvec ♯* P y  P yvec ♯* P xvec ♯* M' y  M'
        yvec ♯* M' xvec ♯* yvec
      by(rule cOpen(22))
  qed
qed

lemma resOutputCases'''''[consumes 7, case_names cOpen cRes]:
  fixes Ψ    :: 'b
    and x    :: name
    and zvec :: "name list"
    and P    :: "('a, 'b, 'c) psi"
    and P'   :: "('a, 'b, 'c) psi"
    and C    :: "'f::fs_name"

assumes Trans: "Ψ  ⦇νxP M⦇ν*zvec⦈⟨N  P'"
  and   1: "x  Ψ"
  and   "x  M⦇ν*zvec⦈⟨N"
  and   3: "x  P'"
  and   "zvec ♯* Ψ"
  and   "zvec ♯* P"
  and   "zvec ♯* M"
  and   rOpen: "M' xvec yvec y N' P'. Ψ  ([(x, y)]  P) M'⦇ν*(xvec@yvec)⦈⟨N'  P'; y  supp N';
                                         x  N'; x  P'; x  y; y  xvec; y  yvec; y  M'; distinct xvec; distinct yvec;
                                         xvec ♯* Ψ; y  Ψ; yvec ♯* Ψ; xvec ♯* P; y  P; yvec ♯* P; xvec ♯* M'; y  M';
                                         yvec ♯* M'; xvec ♯* yvec; M'⦇ν*(xvec@y#yvec)⦈⟨N' = M⦇ν*zvec⦈⟨N 
                                         Prop P'"
  and   rScope:  "P'. Ψ  P M⦇ν*zvec⦈⟨N  P'  Prop (⦇νxP')"

shows "Prop P'"
proof -
  from Trans have "distinct zvec" by(auto dest: boundOutputDistinct)
  obtain al where "al=M⦇ν*zvec⦈⟨N" by simp
  from al = M⦇ν*zvec⦈⟨N Trans zvec ♯* Ψ zvec ♯* P zvec ♯* M
  have αTrans: "Ψ  ⦇νxP al  P'" and 4: "bn al ♯* Ψ" and 5: "bn al ♯* P" and 6: "bn al ♯* subject al"
    by simp+
  from x  M⦇ν*zvec⦈⟨N al=M⦇ν*zvec⦈⟨N have 2: "x  al" by simp
  show ?thesis using αTrans 1 2 3 4 5 6 al=M⦇ν*zvec⦈⟨N rOpen rScope
  proof(induct rule: resCases'[where C="(zvec, C)"])
    case cBrOpen
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case cBrClose
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case(cOpen M' xvec yvec y N' P')
    show ?case
      using Ψ  [(x, y)]  P  M'⦇ν*(xvec @ yvec)⦈⟨N'  P' y  supp N' x  N' x  P'
        x  y y  xvec y  yvec y  M' distinct xvec distinct yvec xvec ♯* Ψ
        y  Ψ yvec ♯* Ψ xvec ♯* P y  P yvec ♯* P xvec ♯* M' y  M'
        yvec ♯* M' xvec ♯* yvec M'⦇ν*(xvec @ y # yvec)⦈⟨N' = M⦇ν*zvec⦈⟨N
      by(rule cOpen(22))
  next
    case (cRes P')
    from Ψ  P  al  P' al = M⦇ν*zvec⦈⟨N
    show ?case
      by (simp add: cRes(4))
  qed
qed

lemma resBrOutputCases'[consumes 7, case_names cBrOpen cRes]:
  fixes Ψ    :: 'b
    and x    :: name
    and zvec :: "name list"
    and P    :: "('a, 'b, 'c) psi"
    and P'   :: "('a, 'b, 'c) psi"
    and C    :: "'f::fs_name"

assumes Trans: "Ψ  ⦇νxP ¡M⦇ν*zvec⦈⟨N  P'"
  and   1: "x  Ψ"
  and   "x  ¡M⦇ν*zvec⦈⟨N"
  and   3: "x  P'"
  and   "zvec ♯* Ψ"
  and   "zvec ♯* P"
  and   "zvec ♯* M"
  and   rBrOpen: "M' xvec yvec y N' P'. Ψ  ([(x, y)]  P) ¡M'⦇ν*(xvec@yvec)⦈⟨N'  P'; y  supp N';
                                         x  N'; x  P'; x  y; y  xvec; y  yvec; y  M'; distinct xvec; distinct yvec;
                                         xvec ♯* Ψ; y  Ψ; yvec ♯* Ψ; xvec ♯* P; y  P; yvec ♯* P; xvec ♯* M'; y  M';
                                         yvec ♯* M'; xvec ♯* yvec; ¡M'⦇ν*(xvec@y#yvec)⦈⟨N' = ¡M⦇ν*zvec⦈⟨N 
                                         Prop P'"
  and   rScope:  "P'. Ψ  P ¡M⦇ν*zvec⦈⟨N  P'  Prop (⦇νxP')"

shows "Prop P'"
proof -
  from Trans have "distinct zvec" by(auto dest: boundOutputDistinct)
  obtain al where "al=¡M⦇ν*zvec⦈⟨N" by simp
  from al = ¡M⦇ν*zvec⦈⟨N Trans zvec ♯* Ψ zvec ♯* P zvec ♯* M
  have αTrans: "Ψ  ⦇νxP al  P'" and 4: "bn al ♯* Ψ" and 5: "bn al ♯* P" and 6: "bn al ♯* subject al"
    by simp+
  from x  ¡M⦇ν*zvec⦈⟨N al=¡M⦇ν*zvec⦈⟨N have 2: "x  al" by simp
  show ?thesis using αTrans 1 2 3 4 5 6 al=¡M⦇ν*zvec⦈⟨N rBrOpen rScope
  proof(induct rule: resCases'[where C="(zvec, C)"])
    case cBrOpen
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case cBrClose
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case(cOpen M' xvec yvec y N' P')
    then show ?case
      by(auto simp add: residualInject boundOutputApp)
  next
    case (cRes P')
    from Ψ  P  al  P' al = ¡M⦇ν*zvec⦈⟨N
    show ?case
      by (simp add: cRes(4))
  qed
qed

lemma brOutputFreshSubject:
  fixes x::name
  assumes "Ψ  P  ¡M⦇ν*xvec⦈⟨N  P'"
    and   "xvec ♯* M"
    and   "x  P"
  shows "x  M"
  using assms
proof(nominal_induct avoiding: x rule: brOutputInduct')
  case(cAlpha Ψ P M xvec N P' p)
  then show ?case by simp
next
  case(cBrOutput Ψ M K N P)
  then show ?case
    by(auto simp add: fresh_def psi.supp dest: chanOutConSupp)
next
  case(cCase Ψ P M xvec N P' φ Cs) then show ?case
    by(induct Cs) auto
next
  case(cPar1 Ψ ΨQ P M xvec N P' AQ Q) then show ?case
    by simp
next
  case cPar2 then show ?case by simp
next
  case cBrComm1 then show ?case by simp
next
  case cBrComm2 then show ?case by simp
next
  case cBrOpen then show ?case by(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
next
  case cScope then show ?case by(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
next
  case cBang then show ?case by simp
qed

lemma brInputFreshSubject:
  fixes x::name
  assumes "Ψ  P  ¿MN  P'"
    and   "x  P"
  shows "x  M"
  using assms
proof(nominal_induct avoiding: x rule: brInputInduct)
  case(cBrInput Ψ K M xvec N Tvec P y)
  then show ?case
    by(auto simp add: fresh_def psi.supp dest: chanInConSupp)
next
  case(cCase Ψ P M N P' φ Cs y) then show ?case
    by(induct Cs) auto
next
  case(cPar1 Ψ ΨQ P M N P' AQ Q y) then show ?case
    by simp
next
  case cPar2 then show ?case by simp
next
  case cBrMerge then show ?case by simp
next
  case cScope then show ?case by(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
next
  case cBang then show ?case by simp
qed

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(⦇νbQ), ⦇νb(⦇νaQ))  Rel"
  and   R3: "Ψ' xvec yvec Q. xvec ♯* Ψ'; mset xvec = mset yvec  (Ψ', ⦇ν*xvecQ, ⦇ν*yvecQ)  Rel"

shows "Ψ  ⦇νx(⦇νyP) ↝[Rel] ⦇νy(⦇νxP)"
proof(cases "x=y")
  assume "x = y"
  then show ?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(⦇νyP)" by(simp add: abs_fresh)
  moreover have "[x, y] ♯* ⦇νy(⦇νxP)" 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(⦇νyP)) 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 α ♯* ⦇νxP" by(simp add: abs_fresh)
    with Ψ  ⦇νy(⦇νxP) α  P' y  Ψ y  α y  P' bn α ♯* Ψ
    show ?case using bn α ♯* subject α x  α x  P' bn α ♯* Ψ bn α ♯* P bn α ♯* subject α y  α
    proof(induct rule: resCases'[where C=x])
      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')]  ⦇νxP) 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 "(yvec1@yvec2) ♯* Ψ" by simp
      moreover from yvec1 ♯* ⦇νxP yvec2 ♯* ⦇νxP y  yvec1 y'  yvec1 y  yvec2 y'  yvec2 x  yvec1 x  yvec2
      have "(yvec1@yvec2) ♯* ([(y, y')]  P)" by simp
      moreover from yvec1 ♯* M yvec2 ♯* M have "(yvec1 @ yvec2) ♯* M"
        by simp
      ultimately show ?case
      proof(induct rule: resOutputCases''''')
        case(cOpen M' xvec1 xvec2 x' N' P')
        from M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N' = M⦇ν*(yvec1 @ yvec2)⦈⟨N have "yvec1@yvec2 = xvec1@x'#xvec2" and "M = M'" and "N = N'" by (simp add: action.inject)+
        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(cases "x'  set yvec1")
          assume "x'  set yvec1"

          with yvec1@yvec2 = xvec1@x'#xvec2 distinct (yvec1@yvec2)
          obtain xvec2' where Eq1: "yvec1=xvec1@x'#xvec2'"
            and Eq: "xvec2=xvec2'@yvec2"
            by(metis 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(intro 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(intro 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'  ⦇νxP x  y' R1 show ?case
            by(auto simp add: alphaRes abs_fresh)
        next
          assume "¬x'  set yvec1"
          then have "x'  yvec1" by(simp add: fresh_def)
          from ¬x'  set yvec1 yvec1@yvec2 = xvec1@x'#xvec2
          have "x'  set yvec2"
            by(auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
          with yvec1@yvec2 = xvec1@x'#xvec2 distinct (yvec1@yvec2)
          obtain xvec2' where Eq: "xvec1=yvec1@xvec2'"
            and Eq1: "yvec2=xvec2'@x'#xvec2"
            by(metis 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(intro 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(intro 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'  ⦇νxP x  y' R1 show ?case
            by(auto 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'  ⦇νxP x  y'have "Ψ  ⦇νyP M⦇ν*(yvec1@y'#yvec2)⦈⟨N  P'" by(simp add: alphaRes abs_fresh)
        then have "Ψ  ⦇νx(⦇νyP) M⦇ν*(yvec1@y'#yvec2)⦈⟨N  ⦇νxP'" using x  Ψ x  M x  yvec1 x  y' x  yvec2 x  N
          by(intro Scope) auto
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule R1)
        ultimately show ?case by blast
      qed
    next
      case(cBrOpen 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')]  ⦇νxP) ¡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 "(yvec1@yvec2) ♯* Ψ" by simp
      moreover from yvec1 ♯* ⦇νxP yvec2 ♯* ⦇νxP y  yvec1 y'  yvec1 y  yvec2 y'  yvec2 x  yvec1 x  yvec2
      have "(yvec1@yvec2) ♯* ([(y, y')]  P)" by simp
      moreover from yvec1 ♯* M yvec2 ♯* M have "(yvec1 @ yvec2) ♯* M"
        by simp
      ultimately show ?case
      proof(induct rule: resBrOutputCases')
        case(cBrOpen M' xvec1 xvec2 x' N' P')
        from ¡M'⦇ν*(xvec1 @ x' # xvec2)⦈⟨N' = ¡M⦇ν*(yvec1 @ yvec2)⦈⟨N have "yvec1@yvec2 = xvec1@x'#xvec2" and "M = M'" and "N = N'" by (simp add: action.inject)+
        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(cases "x'  set yvec1")
          assume "x'  set yvec1"

          with yvec1@yvec2 = xvec1@x'#xvec2 distinct (yvec1@yvec2)
          obtain xvec2' where Eq1: "yvec1=xvec1@x'#xvec2'"
            and Eq: "xvec2=xvec2'@yvec2"
            by(metis 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(intro BrOpen) 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(intro BrOpen) 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'  ⦇νxP x  y' R1 show ?case
            by(auto simp add: alphaRes abs_fresh)
        next
          assume "¬x'  set yvec1"
          then have "x'  yvec1" by(simp add: fresh_def)
          from ¬x'  set yvec1 yvec1@yvec2 = xvec1@x'#xvec2
          have "x'  set yvec2"
            by(auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
          with yvec1@yvec2 = xvec1@x'#xvec2 distinct (yvec1@yvec2)
          obtain xvec2' where Eq: "xvec1=yvec1@xvec2'"
            and Eq1: "yvec2=xvec2'@x'#xvec2"
            by(metis 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(intro BrOpen) (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(intro BrOpen) 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'  ⦇νxP x  y' R1 show ?case
            by(auto 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 BrOpen)
        with y'  ⦇νxP x  y'have "Ψ  ⦇νyP ¡M⦇ν*(yvec1@y'#yvec2)⦈⟨N  P'" by(simp add: alphaRes abs_fresh)
        then have "Ψ  ⦇νx(⦇νyP) ¡M⦇ν*(yvec1@y'#yvec2)⦈⟨N  ⦇νxP'" using x  Ψ x  M x  yvec1 x  y' x  yvec2 x  N
          by(intro Scope) auto
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule R1)
        ultimately show ?case by blast
      qed
    next
      case(cRes P')
      from x  ⦇νyP' x  y have "x  P'" by(simp add: abs_fresh)
      with Ψ  ⦇νxP α  P' x  Ψ x  α
      show ?case using bn α ♯* Ψ bn α ♯* P bn α ♯* subject α y  α
      proof(induct rule: resCases'[where C="(x, y)"])
        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  ⦇νyP'"
          by(rule Scope)
        then have "Ψ  ⦇νx'(⦇νy([(x, x')]  P)) M⦇ν*(xvec1@x'#xvec2)⦈⟨N  ⦇νyP'"
          using x'  supp N x'  Ψ x'  M x'  xvec1 x'  xvec2
          by(rule Open)
        with y  x' x  y x'  P have "Ψ  ⦇νx(⦇νyP) M⦇ν*(xvec1@x'#xvec2)⦈⟨N  ⦇νyP'"
          by(subst alphaRes[where y=x']) (simp add: abs_fresh eqvts calc_atm)+
        moreover have "(Ψ, ⦇νyP', ⦇νyP')  Rel" by(rule R1)
        ultimately show ?case by blast
      next
        case(cBrOpen 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  ⦇νyP'"
          by(rule Scope)
        then have "Ψ  ⦇νx'(⦇νy([(x, x')]  P)) ¡M⦇ν*(xvec1@x'#xvec2)⦈⟨N  ⦇νyP'"
          using x'  supp N x'  Ψ x'  M x'  xvec1 x'  xvec2
          by(rule BrOpen)
        with y  x' x  y x'  P have "Ψ  ⦇νx(⦇νyP) ¡M⦇ν*(xvec1@x'#xvec2)⦈⟨N  ⦇νyP'"
          by(subst alphaRes[where y=x']) (simp add: abs_fresh eqvts calc_atm)+
        moreover have "(Ψ, ⦇νyP', ⦇νyP')  Rel" by(rule R1)
        ultimately show ?case by blast
      next
        case(cRes P')
        from Ψ  P α  P' y  Ψ y  α
        have "Ψ  ⦇νyP α  ⦇νyP'" by(rule Scope)
        then have "Ψ  ⦇νx(⦇νyP) α  ⦇νx(⦇νyP')" using x  Ψ x  α
          by(rule Scope)
        moreover from x  Ψ y  Ψ have "(Ψ, ⦇νx(⦇νyP'), ⦇νy(⦇νxP'))  Rel"
          by(rule R2)
        ultimately show ?case by blast
      next
        case(cBrClose M xvec N P')
        then show ?case
        proof(cases "y  ¡M⦇ν*xvec⦈⟨N")
          case True
          with Ψ  P ¡M⦇ν*xvec⦈⟨N  P'
          have "Ψ  ⦇νyP ¡M⦇ν*xvec⦈⟨N  ⦇νyP'" using y  Ψ
            by(intro Scope)
          then have "Ψ  ⦇νx(⦇νyP)  τ  (⦇νx(⦇ν*xvec⦇νyP'))" using x  supp M x  Ψ
            by(rule BrClose)
          moreover have "(Ψ, (⦇νx(⦇ν*xvec⦇νyP')), ⦇νy(⦇νx(⦇ν*xvecP')))  Rel"
          proof -
            have "mset (x#xvec@[y]) = mset (y#x#xvec)"
              by simp
            moreover have "(x#xvec@[y]) ♯* Ψ" using x  Ψ y  Ψ xvec ♯* Ψ
              by simp
            ultimately have "(Ψ, ⦇ν*(x#xvec@[y])P', ⦇ν*(y#x#xvec)P')  Rel"
              by(metis R3)
            then show ?thesis
              by(auto simp add: resChainAppend)
          qed
          ultimately show ?thesis
            by blast
        next
          case False
          then have "y  supp(¡M⦇ν*xvec⦈⟨N)" unfolding fresh_def by simp
          show ?thesis
          proof(cases "y  supp(M)")
            case True
            with Ψ  P ¡M⦇ν*xvec⦈⟨N  P'
            have "Ψ  ⦇νyP τ  ⦇νy(⦇ν*xvecP')" using y  Ψ
              by(rule BrClose)
            then have "Ψ  ⦇νx(⦇νyP) τ  ⦇νx(⦇νy(⦇ν*xvecP'))" using x  Ψ
              by(rule Scope) simp
            moreover have "(Ψ, ⦇νx(⦇νy(⦇ν*xvecP')), ⦇νy(⦇νx(⦇ν*xvecP')))  Rel" using x  Ψ y  Ψ
              by(metis R2)
            ultimately show ?thesis
              by blast
          next
            case False
            then have "y  M" by(simp add: fresh_def)
            from xvec ♯* (x, y) have "y  xvec" by simp
            with False y  supp(¡M⦇ν*xvec⦈⟨N)
            have "y  supp N"
              by(simp add: fresh_def action.supp)
            from Ψ  P ¡M⦇ν*xvec⦈⟨N  P' have "Ψ  P ¡M⦇ν*([]@xvec)⦈⟨N  P'"
              by simp
            then have "Ψ  ⦇νyP ¡M⦇ν*([]@y#xvec)⦈⟨N  P'" using y  supp N y  Ψ y  M y  xvec
              by(intro BrOpen) (assumption|simp)+
            then have "Ψ  ⦇νyP ¡M⦇ν*(y#xvec)⦈⟨N  P'"
              by simp
            then have "Ψ  ⦇νx(⦇νyP) τ  ⦇νx(⦇νy(⦇ν*xvecP'))" using x  supp M x  Ψ
              by(auto dest: BrClose)
            moreover have "(Ψ, ⦇νx(⦇νy(⦇ν*xvecP')), ⦇νy(⦇νx(⦇ν*xvecP')))  Rel" using x  Ψ y  Ψ
              by(rule R2)
            ultimately show ?thesis by blast
          qed
        qed
      qed
    next
      case(cBrClose M xvec N P')
      from xvec ♯* x have "x  xvec" by simp
      have "x  ⦇νxP" by(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
      have "x  P'"
        by(rule broutputFreshDerivativeP) fact+
      have "x  N"
        by(rule broutputFreshDerivativeN) fact+
      moreover from Ψ  ⦇νxP  ¡M⦇ν*xvec⦈⟨N  P' xvec ♯* M x  ⦇νxP have "x  M"
        by(rule brOutputFreshSubject)
      moreover note x  xvec
      ultimately have "x  ¡M⦇ν*xvec⦈⟨N"
        by simp
      have "bn (¡M⦇ν*xvec⦈⟨N) ♯* Ψ" using xvec ♯* Ψ by simp
      have "bn (¡M⦇ν*xvec⦈⟨N) ♯* P" using xvec ♯* ⦇νxP x  xvec by(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
      have "bn (¡M⦇ν*xvec⦈⟨N) ♯* subject (¡M⦇ν*xvec⦈⟨N)" using xvec ♯* M by simp
      have "y  supp(subject (¡M⦇ν*xvec⦈⟨N))" using y  supp M
        by(simp add: supp_some)
      obtain M' xvec' N' where "¡M⦇ν*xvec⦈⟨N = ¡M'⦇ν*xvec'⦈⟨N'"
        by auto
      from Ψ  ⦇νxP  ¡M⦇ν*xvec⦈⟨N  P' x  Ψ x  ¡M⦇ν*xvec⦈⟨N x  P' bn (¡M⦇ν*xvec⦈⟨N) ♯* Ψ bn (¡M⦇ν*xvec⦈⟨N) ♯* P bn (¡M⦇ν*xvec⦈⟨N) ♯* subject (¡M⦇ν*xvec⦈⟨N) ¡M⦇ν*xvec⦈⟨N = ¡M'⦇ν*xvec'⦈⟨N' y  supp(subject (¡M⦇ν*xvec⦈⟨N))
      have "Q'. Ψ  ⦇νx(⦇νyP)  τ  Q'  (Ψ, Q', ⦇νy(⦇ν*(bn (¡M⦇ν*xvec⦈⟨N))P'))  Rel"
      proof(induct rule: resCases'[where C=y])
        case cOpen then show ?case by(simp add: residualInject)
      next
        case(cBrOpen M xvec yvec z N P')
        from y  supp (subject (¡M⦇ν*(xvec @ z # yvec)⦈⟨N)) have "y  supp M"
          by(simp add: supp_some)
        then have "y  z" using z  M by(auto simp add: fresh_def)
        from Ψ  [(x, z)]  P  ¡M⦇ν*(xvec @ yvec)⦈⟨N  P' y  supp M y  Ψ
        have "Ψ  ⦇νy([(x, z)]  P)  τ  ⦇νy(⦇ν*(xvec@yvec)P')"
          by(rule BrClose)
        then have "Ψ  ⦇νz(⦇νy([(x, z)]  P))  τ  ⦇νz(⦇νy(⦇ν*(xvec@yvec)P'))" using z  Ψ
          by(rule Scope) simp
        then have "Ψ  ⦇νx(⦇νyP)  τ  ⦇νz(⦇νy(⦇ν*(xvec@yvec)P'))" using z  P x  y y  z
          apply(subst alphaRes[where x=x and y=z])
           apply(simp add: fresh_abs_fun_iff[OF pt_name_inst, OF at_name_inst, OF fin_supp])
          apply(simp add: eqvts swap_simps)
          done
        moreover have "(Ψ, ⦇νz(⦇νy(⦇ν*(xvec @ yvec)P')), ⦇νy(⦇ν*bn (¡M⦇ν*(xvec @ z # yvec)⦈⟨N)P'))  Rel"
        proof -
          have "mset(z#y#xvec@yvec) = mset(y#xvec@z#yvec)"
            by simp
          moreover have "(z#y#xvec@yvec) ♯* Ψ" using z  Ψ y  Ψ xvec ♯* Ψ yvec ♯* Ψ
            by simp
          ultimately have "(Ψ, ⦇ν*(z#y#xvec@yvec)P', ⦇ν*(y#xvec@z#yvec)P')  Rel"
            by(metis R3)
          then show ?thesis
            by(simp add: resChainAppend)
        qed
        ultimately show ?case
          by blast
      next
        case(cRes P')
        from Ψ  P  ¡M⦇ν*xvec⦈⟨N  P' y  supp M y  Ψ
        have "Ψ  ⦇νyP  τ  ⦇νy(⦇ν*xvecP')"
          by(rule BrClose)
        then have "Ψ  ⦇νx(⦇νyP)  τ  ⦇νx(⦇νy(⦇ν*xvecP'))" using x  Ψ
          by(rule Scope) simp
        moreover have "(Ψ, ⦇νx(⦇νy(⦇ν*xvecP')), ⦇νy(⦇ν*bn (¡M⦇ν*xvec⦈⟨N)⦇νxP'))  Rel"
        proof -
          have "mset(x#y#xvec) = mset(y#xvec@[x])"
            by simp
          moreover have "(x#y#xvec) ♯* Ψ" using x  Ψ y  Ψ xvec ♯* Ψ
            by simp
          ultimately have "(Ψ, ⦇ν*(x#y#xvec)P', ⦇ν*(y#xvec@[x])P')  Rel"
            by(metis R3)
          then show ?thesis by(simp add: resChainAppend)
        qed
        ultimately show ?case
          by blast
      next
        case cBrClose then show ?case by simp
      qed
      then show ?case by simp
    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 ♯* Ψ'  (Ψ', ⦇ν*xvecS, ⦇ν*xvecT)  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+
  then have "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(auto intro: mergeFrameE 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)
    then have "Ψ  ΨR  P  Q α  (P'  Q)" using FrQ bn α ♯* Q AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* α
      by(intro Par1) auto
    then have "Ψ  (P  Q)  R α  ((P'  Q)  R)" using FrR bn α ♯* R AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* α
      by(auto intro: Par1)
    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(auto dest: extractFrameFreshChain)
      from (Ψ  ΨP)  ΨR  Q α  Q' have "(Ψ  ΨR)  ΨP  Q α  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      then have "Ψ  ΨR  P  Q α  (P  Q')"
        using FrP bn α ♯* P AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* α
        by(intro Par2) (assumption | force)+
      then have "Ψ  (P  Q)  R α  ((P  Q')  R)"
        using extractFrame R = AR, ΨR bn α ♯* R AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* α
        by(intro 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(auto dest: extractFrameFreshChain)
      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(auto dest: extractFrameFreshChain)
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)
      from (Ψ  ΨP)  ΨQ  R K⦇ν*xvec⦈⟨N  R' AP ♯* R xvec ♯* AP xvec ♯* K distinct xvec have "AP ♯* N"
        by(auto intro: outputFreshChainDerivative)

      from (Ψ  ΨP)  ΨR  Q MN  Q' have "(Ψ  ΨR)  ΨP  Q MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      then have "Ψ  ΨR  P  Q MN  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N
        by(intro 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(intro 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(auto dest: extractFrameFreshChain)
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)

      from (Ψ  ΨP)  ΨR  Q M⦇ν*xvec⦈⟨N  Q' AP ♯* Q xvec ♯* AP xvec ♯* M distinct xvec have "AP ♯* N"
        by(auto intro: outputFreshChainDerivative)

      from (Ψ  ΨP)  ΨR  Q M⦇ν*xvec⦈⟨N  Q' have "(Ψ  ΨR)  ΨP  Q M⦇ν*xvec⦈⟨N  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      then have "Ψ  ΨR  P  Q M⦇ν*xvec⦈⟨N  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N xvec ♯* P xvec ♯* AP
        by(intro 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 KN  R' have "Ψ  ΨP  ΨQ  R KN  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(intro 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
    next
      case(cBrMerge ΨR M N Q' AQ ΨQ R' AR)
      from AP ♯* α α = ¿MN have "AP ♯* M" and "AP ♯* N" by simp+
      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+

      have FrQ: "extractFrame Q = AQ, ΨQ" by fact
      with AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
        by(auto dest: extractFrameFreshChain)
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)

      from (Ψ  ΨP)  ΨR  Q ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      then have "Ψ  ΨR  P  Q ¿MN  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N
        by(intro 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 ¿MN  R' have "Ψ  ΨP  ΨQ  R ¿MN  R'"
        by(metis statEqTransition Associativity)
      moreover note extractFrame R = AR, ΨR
      ultimately have "Ψ  (P  Q)  R ¿MN  (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 ♯* M AR ♯* AP AQ ♯* AR
        by(auto intro: BrMerge)
      moreover have "(Ψ, (P  Q')  R', P  (Q'  R'))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrComm1 ΨR M N Q' AQ ΨQ xvec R' AR)
      from ¡M⦇ν*xvec⦈⟨N = α have "xvec = bn α"
        by(auto simp add: action.inject)
      from ¡M⦇ν*xvec⦈⟨N = α AP ♯* α
      have "AP ♯* xvec" and "AP ♯* M" and "AP ♯* N" by auto
      from xvec = bn α bn α ♯* P bn α ♯* Ψ bn α ♯* ΨP have "xvec ♯* P" and "xvec ♯* Ψ" and "xvec ♯* ΨP"
        by simp+
      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+

      have FrQ: "extractFrame Q = AQ, ΨQ" by fact
      with AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
        by(auto dest: extractFrameFreshChain)
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)

      from (Ψ  ΨP)  ΨR  Q ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      then have "Ψ  ΨR  P  Q ¿MN  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N
        by(intro 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 ¡M⦇ν*xvec⦈⟨N  R' have "Ψ  ΨP  ΨQ  R ¡M⦇ν*xvec⦈⟨N  R'"
        by(metis statEqTransition Associativity)
      moreover note extractFrame R = AR, ΨR
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  ((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 ♯* M AR ♯* AP AQ ♯* AR xvec ♯* P xvec ♯* Q
        by(intro BrComm1) (assumption | simp)+
      moreover have "(Ψ, ((P  Q')  R'), (P  (Q'  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrComm2 ΨR M xvec N Q' AQ ΨQ R' AR)
      from ¡M⦇ν*xvec⦈⟨N = α have "xvec = bn α"
        by(auto simp add: action.inject)
      from ¡M⦇ν*xvec⦈⟨N = α AP ♯* α
      have "AP ♯* xvec" and "AP ♯* M" and "AP ♯* N" by auto
      from xvec = bn α bn α ♯* P bn α ♯* Ψ bn α ♯* ΨP have "xvec ♯* P" and "xvec ♯* Ψ" and "xvec ♯* ΨP"
        by simp+
      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+

      have FrQ: "extractFrame Q = AQ, ΨQ" by fact
      with AP ♯* Q AQ ♯* AP have "AP ♯* ΨQ"
        by(auto dest: extractFrameFreshChain)
      have FrR: "extractFrame R = AR, ΨR" by fact
      with AP ♯* R AR ♯* AP have "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)

      from (Ψ  ΨP)  ΨR  Q ¡M⦇ν*xvec⦈⟨N  Q' have "(Ψ  ΨR)  ΨP  Q ¡M⦇ν*xvec⦈⟨N  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      then have "Ψ  ΨR  P  Q ¡M⦇ν*xvec⦈⟨N  (P  Q')" using FrP AP ♯* Ψ AP ♯* ΨR AP ♯* Q AP ♯* M AP ♯* N xvec ♯* P AP ♯* xvec
        by(intro 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 ¿MN  R' have "Ψ  ΨP  ΨQ  R ¿MN  R'"
        by(metis statEqTransition Associativity)
      moreover note extractFrame R = AR, ΨR
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  ((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 ♯* M AR ♯* AP AQ ♯* AR xvec ♯* R
        by(auto intro: BrComm2)
      moreover have "(Ψ, ((P  Q')  R'), (P  (Q'  R')))  Rel"
        by(rule C1)
      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 MN  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 ♯* Qxvec ♯* 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 MN  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(intro 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(intro 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 have "(Ψ  ΨP)  ΨQ  R  ROut K (⦇ν*xvecN ≺' R')" by(simp add: residualInject)
      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 FrR
        using outputObtainPrefix[where B="AP@AQ"]
        by (smt (verit, ccfv_threshold) freshChainAppend freshChainSym freshCompChain(1))
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P MN  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(auto intro: inputRenameSubject)
      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(intro 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(intro 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 KN  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 KN  Q' have "(Ψ  ΨR)  ΨP  Q KN  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(intro 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(intro 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 KN  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
        using inputObtainPrefix[where B="AP@AQ"]
        by (smt (verit, ccfv_threshold) freshChainAppend freshChainSym freshCompChain(1))
      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(auto intro: outputRenameSubject)
      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(intro 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 KN  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(intro 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
  next
    case(cBrMerge ΨQR M N P' AP ΨP QR' AQR)
    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 ¿MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
    note Ψ  ΨP  Q  R ¿MN  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 ♯* M AQR ♯* N AQR ♯* P AQR ♯* M AQR ♯* Ψ
    proof(induct rule: parCasesBrInputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¿MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      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 ¿MN  (P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* M
        by(intro BrMerge) (assumption | force)+
      moreover from AQR ♯* Ψ AQR ♯* P Aeq have "AR ♯* Ψ" and "AR ♯* P" by simp+
      ultimately have "Ψ  (P  Q)  R ¿MN  (P'  Q')  R" using extractFrame R = AR, ΨR AR ♯* Q AR ♯* M AR ♯* N
        by(intro 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 AR ΨR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      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 ¿MN  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¿MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from AP ♯* R AP ♯* Q AP ♯* AQR FrR extractFrame Q = AQ, ΨQ Aeq have "AP ♯* ΨQ" and "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)
      moreover from AQR ♯* P AQR ♯* N Aeq have "AQ ♯* P" and "AQ ♯* N" by simp+
      ultimately have "Ψ  ΨR  P  Q ¿MN  (P'  Q)" using extractFrame Q = AQ, ΨQ AQ ♯* ΨR AQ ♯* M AQ ♯* Ψ
        by(intro 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 ¿MN  R'" by(metis Associativity statEqTransition)
      moreover note FrR
      ultimately have "Ψ  (P  Q)  R ¿MN  ((P'  Q)  R')"
        using AP ♯* Ψ AQ ♯* Ψ AP ♯* P AQ ♯* P AP ♯* Q AQ ♯* Q AP ♯* R AQ ♯* R AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR
          AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* M
        by(auto intro: BrMerge)
      moreover have "(Ψ, ((P'  Q)  R'), (P'  (Q  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrMerge ΨR Q' AQ ΨQ R' AR)
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from AQR ♯* N AQR ♯* M AQR ♯* P AQR ♯* Ψ AQR ♯* ΨP AP ♯* AQR Aeq Ψeq
      have "AQ ♯* N" and "AR ♯* N" and "AQ ♯* M" and "AR ♯* M"
        and "AQ ♯* Ψ" and "AR ♯* Ψ" and "AP ♯* AQ" and "AP ♯* AR"
        and "AQ ♯* ΨP" and "AR ♯* ΨP"
        and "AQ ♯* P" and "AR ♯* P"
        by simp+

      from extractFrame Q = AQ, ΨQ AP ♯* Q AP ♯* AQ
      have "AP ♯* ΨQ"
        by (metis extractFrameFreshChain freshFrameDest)
      from Aeq Ψeq PTrans have "Ψ  (ΨQ  ΨR)  P  ¿MN  P'" by simp
      then have "Ψ  (ΨR  ΨQ)  P  ¿MN  P'"
        by (metis Commutativity Ψeq compositionSym statEqTransition)
      then have "(Ψ  ΨR)  ΨQ  P  ¿MN  P'"
        by (metis AssertionStatEqSym Associativity statEqTransition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by (metis associativitySym statEqTransition)
      moreover note extractFrame Q = AQ, ΨQ
      moreover note AP ♯* Ψ AQ ♯* Ψ AQ ♯* ΨR
      moreover from extractFrame R = AR, ΨR AP ♯* AR AP ♯* R have "AP ♯* ΨR"
        by (metis extractFrameFreshChain freshFrameDest)
      moreover note AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* P AQ ♯* Q AQ ♯* M
      ultimately have "(Ψ  ΨR)  (P  Q) ¿MN  (P'  Q')"
        by(intro BrMerge) (assumption | force)+

      from (Ψ  ΨP)  ΨQ  R ¿MN  R' have "Ψ  (ΨP  ΨQ)  R ¿MN  R'"
        by (metis Associativity statEqTransition)

      note (Ψ  ΨR)  (P  Q) ¿MN  (P'  Q')
      moreover from FrP extractFrame Q = AQ, ΨQ AP ♯* AQ AP ♯* ΨQ AQ ♯* ΨP
      have "extractFrame(P  Q) = (AP@AQ), (ΨP  ΨQ)" by simp
      moreover note Ψ  (ΨP  ΨQ)  R ¿MN  R' extractFrame R = AR, ΨR
      moreover note AP ♯* Ψ AQ ♯* Ψ AR ♯* Ψ AP ♯* P AQ ♯* P AP ♯* Q AQ ♯* Q
        AP ♯* R AQ ♯* R AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR AR ♯* P AR ♯* Q AR ♯* R AR ♯* M
      ultimately have "Ψ  (P  Q)  R ¿MN  (P'  Q')  R'"
        by(auto intro: BrMerge)
      moreover have "(Ψ, (P'  Q')  R', (P'  (Q'  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    qed
  next
    case(cBrComm1 ΨQR M N P' AP ΨP xvec QR' AQR)
    from ¡M⦇ν*xvec⦈⟨N = α bn α ♯* Q bn α ♯* R have "xvec ♯* Q" and "xvec ♯* R" by auto
    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 ¿MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
    note Ψ  ΨP  Q  R ¡M⦇ν*xvec⦈⟨N  QR'
    moreover from xvec ♯* Ψ xvec ♯* ΨP have "xvec ♯* (Ψ  ΨP)" by force
    moreover note xvec ♯* Q xvec ♯* R xvec ♯* M
      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 ♯* M
    proof(induct rule: parCasesBrOutputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      from AQR ♯* xvec AQR = (AQ@AR) have "AQ ♯* xvec" and "AR ♯* xvec"
        by simp+
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¿MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q ¡M⦇ν*xvec⦈⟨N  Q' have "(Ψ  ΨR)  ΨP  Q ¡M⦇ν*xvec⦈⟨N  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      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 ¡M⦇ν*xvec⦈⟨N  (P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* M xvec ♯* P
        by(intro BrComm1) (assumption | force)+
      moreover from AQR ♯* Ψ AQR ♯* P Aeq have "AR ♯* Ψ" and "AR ♯* P" by simp+
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  (P'  Q')  R" using extractFrame R = AR, ΨR AR ♯* Q AR ♯* M AR ♯* N xvec ♯* R AR ♯* xvec
        by(intro 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 AR ΨR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      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 ¡M⦇ν*xvec⦈⟨N  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¿MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from AP ♯* R AP ♯* Q AP ♯* AQR FrR extractFrame Q = AQ, ΨQ Aeq have "AP ♯* ΨQ" and "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)
      moreover from AQR ♯* P AQR ♯* N Aeq have "AQ ♯* P" and "AQ ♯* N" by simp+
      ultimately have "Ψ  ΨR  P  Q ¿MN  (P'  Q)" using extractFrame Q = AQ, ΨQ AQ ♯* ΨR AQ ♯* M AQ ♯* Ψ
        by(intro 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 ¡M⦇ν*xvec⦈⟨N  R'" by(metis Associativity statEqTransition)
      moreover note FrR
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  ((P'  Q)  R')"
        using AP ♯* Ψ AQ ♯* Ψ AP ♯* P AQ ♯* P AP ♯* Q AQ ♯* Q AP ♯* R AQ ♯* R AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR
          AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* M xvec ♯* P xvec ♯* Q
        by(intro BrComm1) (assumption | simp)+
      moreover have "(Ψ, ((P'  Q)  R'), (P'  (Q  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrComm1 ΨR Q' AQ ΨQ R' AR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      from AQR ♯* xvec AQR = (AQ@AR) have "AQ ♯* xvec" and "AR ♯* xvec"
        by simp+
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from Aeq AQR ♯* P have "AQ ♯* P" and "AR ♯* P" by simp+
      from Aeq AQR ♯* Ψ have "AQ ♯* Ψ" and "AR ♯* Ψ" by simp+
      from Aeq AP ♯* AQR have "AP ♯* AQ" and "AP ♯* AR" by simp+
      with AP ♯* Q extractFrame Q = AQ, ΨQ have "AP ♯* ΨQ"
        by (metis extractFrameFreshChain freshChainSym freshFrameDest)
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¿MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      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 PQTrans: "Ψ  ΨR  P  Q ¿MN  (P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* M
        by(intro BrMerge) (assumption | force)+
      have RTrans: "(Ψ  ΨP)  ΨQ  R ¡M⦇ν*xvec⦈⟨N  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      note PQTrans
      moreover from FrP extractFrame Q = AQ, ΨQ AP ♯* AQ AP ♯* ΨQ AQR ♯* ΨP Aeq
      have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ" by simp+
      moreover from RTrans have "Ψ  (ΨP  ΨQ)  R ¡M⦇ν*xvec⦈⟨N  R'"
        by (metis Associativity statEqTransition)
      moreover note FrR
      moreover note AP ♯* Ψ AQ ♯* Ψ AP ♯* P AP ♯* Q AQ ♯* P AQ ♯* Q AP ♯* R AQ ♯* R
        AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* M xvec ♯* P xvec ♯* Q
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  (P'  Q')  R'"
        by(intro BrComm1) (assumption | force)+
      moreover have "(Ψ, (P'  Q')  R', (P'  (Q'  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrComm2 ΨR Q' AQ ΨQ R' AR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      from AQR ♯* xvec AQR = (AQ@AR) have "AQ ♯* xvec" and "AR ♯* xvec"
        by simp+
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from Aeq AQR ♯* P have "AQ ♯* P" and "AR ♯* P" by simp+
      from Aeq AQR ♯* Ψ have "AQ ♯* Ψ" and "AR ♯* Ψ" by simp+
      from Aeq AP ♯* AQR have "AP ♯* AQ" and "AP ♯* AR" by simp+
      with AP ♯* Q extractFrame Q = AQ, ΨQ have "AP ♯* ΨQ"
        by (metis extractFrameFreshChain freshChainSym freshFrameDest)
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¿MN  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note FrP
      moreover from (Ψ  ΨP)  ΨR  Q ¡M⦇ν*xvec⦈⟨N  Q' have "(Ψ  ΨR)  ΨP  Q ¡M⦇ν*xvec⦈⟨N  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      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 PQTrans: "Ψ  ΨR  P  Q ¡M⦇ν*xvec⦈⟨N  (P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* M xvec ♯* P
        by(intro BrComm1) (assumption | force)+
      have RTrans: "(Ψ  ΨP)  ΨQ  R ¿MN  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      note PQTrans
      moreover from FrP extractFrame Q = AQ, ΨQ AP ♯* AQ AP ♯* ΨQ AQR ♯* ΨP Aeq
      have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ" by simp+
      moreover from RTrans have "Ψ  (ΨP  ΨQ)  R ¿MN  R'"
        by (metis Associativity statEqTransition)
      moreover note FrR
      moreover note AP ♯* Ψ AQ ♯* Ψ AP ♯* P AP ♯* Q AQ ♯* P AQ ♯* Q AP ♯* R AQ ♯* R
        AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* M
        xvec ♯* P xvec ♯* Q xvec ♯* R
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  (P'  Q')  R'"
        by(auto intro: BrComm2)
      moreover have "(Ψ, (P'  Q')  R', (P'  (Q'  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    qed
  next
    case(cBrComm2 ΨQR M xvec N P' AP ΨP QR' AQR)
    from ¡M⦇ν*xvec⦈⟨N = α bn α ♯* Q bn α ♯* R have "xvec ♯* Q" and "xvec ♯* R" by auto
    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⦇ν*xvec⦈⟨N  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
    note Ψ  ΨP  Q  R ¿MN  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 ♯* M
    proof(induct rule: parCasesBrInputFrame)
      case(cPar1 Q' AQ ΨQ AR ΨR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      from AQR ♯* xvec AQR = (AQ@AR) have "AQ ♯* xvec" and "AR ♯* xvec"
        by simp+
      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 ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      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 ¡M⦇ν*xvec⦈⟨N  (P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q AQ ♯* M xvec ♯* Q
        by(intro BrComm2) (assumption | force)+
      moreover from AQR ♯* Ψ AQR ♯* P Aeq have "AR ♯* Ψ" and "AR ♯* P" by simp+
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  (P'  Q')  R" using extractFrame R = AR, ΨR AR ♯* Q AR ♯* M AR ♯* N xvec ♯* R AR ♯* xvec
        by(intro 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 AR ΨR)
      from AQR ♯* N AQR ♯* xvec AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N" and "AQ ♯* xvec" and "AR ♯* xvec"
        by simp+
      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 ¿MN  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      from PTrans Ψeq have "(Ψ  ΨR)  ΨQ  P ¡M⦇ν*xvec⦈⟨N  P'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover from AP ♯* R AP ♯* Q AP ♯* AQR FrR extractFrame Q = AQ, ΨQ Aeq have "AP ♯* ΨQ" and "AP ♯* ΨR"
        by(auto dest: extractFrameFreshChain)
      moreover from AQR ♯* P AQR ♯* N Aeq have "AQ ♯* P" and "AQ ♯* N" by simp+
      ultimately have "Ψ  ΨR  P  Q ¡M⦇ν*xvec⦈⟨N  (P'  Q)" using extractFrame Q = AQ, ΨQ AQ ♯* ΨR
          AQ ♯* M AQ ♯* Ψ xvec ♯* Q AQ ♯* xvec
        by(intro 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 ¿MN  R'" by(metis Associativity statEqTransition)
      moreover note FrR
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  ((P'  Q)  R')"
        using AP ♯* Ψ AQ ♯* Ψ AP ♯* P AQ ♯* P AP ♯* Q AQ ♯* Q AP ♯* R AQ ♯* R AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR
          AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* M xvec ♯* P xvec ♯* R
        by(auto intro: BrComm2)
      moreover have "(Ψ, ((P'  Q)  R'), (P'  (Q  R')))  Rel"
        by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrMerge ΨR Q' AQ ΨQ R' AR)
      from AQR ♯* N AQR = AQ @ AR have "AQ ♯* N" and "AR ♯* N"
        by simp+
      from AQR ♯* xvec AQR = (AQ@AR) have "AQ ♯* xvec" and "AR ♯* xvec"
        by simp+
      have Aeq: "AQR = AQ@AR" and Ψeq: "ΨQR = ΨQ  ΨR" by fact+
      from Aeq AQR ♯* P have "AQ ♯* P" and "AR ♯* P" by simp+
      from Aeq AQR ♯* M have "AQ ♯* M" and "AR ♯* M" by simp+
      from Aeq AQR ♯* Ψ have "AQ ♯* Ψ" and "AR ♯* Ψ" by simp+
      from Aeq AP ♯* AQR have "AP ♯* AQ" and "AP ♯* AR" by simp+
      with AP ♯* Q extractFrame Q = AQ, ΨQ have "AP ♯* ΨQ"
        by (metis extractFrameFreshChain freshChainSym freshFrameDest)
      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 ¿MN  Q' have "(Ψ  ΨR)  ΨP  Q ¿MN  Q'"
        by(metis statEqTransition Associativity Commutativity Composition)
      moreover note extractFrame Q = AQ, ΨQ
      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 PQTrans: "Ψ  ΨR  P  Q ¡M⦇ν*xvec⦈⟨N  (P'  Q')"
        using AP ♯* Ψ AP ♯* P AP ♯* Q AP ♯* M AP ♯* AQ AQ ♯* Ψ AQ ♯* ΨR AQ ♯* P AQ ♯* Q xvec ♯* Q AQ ♯* M
        by(intro BrComm2) (assumption | force)+
      have RTrans: "(Ψ  ΨP)  ΨQ  R ¿MN  R'" and FrR: "extractFrame R = AR, ΨR" by fact+
      note PQTrans
      moreover from FrP extractFrame Q = AQ, ΨQ AP ♯* AQ AP ♯* ΨQ AQR ♯* ΨP Aeq
      have "extractFrame(P  Q) = (AP@AQ), ΨP  ΨQ" by simp+
      moreover from RTrans have "Ψ  (ΨP  ΨQ)  R ¿MN  R'"
        by (metis Associativity statEqTransition)
      moreover note FrR
      moreover note AP ♯* Ψ AQ ♯* Ψ AP ♯* P AP ♯* Q AQ ♯* P AQ ♯* Q AP ♯* R AQ ♯* R
        AP ♯* M AQ ♯* M AP ♯* AR AQ ♯* AR AR ♯* Ψ AR ♯* P AR ♯* Q AR ♯* R AR ♯* M xvec ♯* P xvec ♯* R
      ultimately have "Ψ  (P  Q)  R ¡M⦇ν*xvec⦈⟨N  (P'  Q')  R'"
        by(auto intro: BrComm2)
      moreover have "(Ψ, (P'  Q')  R', (P'  (Q'  R')))  Rel"
        by(rule C1)
      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)
  then have "Ψ  (P  𝟬) α  (P'  𝟬)"
    by(rule 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
    then show ?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
    then show ?case by simp
  next
    case(cComm2 ΨQ M xvec N P' AP ΨP K Q' AQ)
    from Ψ  ΨP  𝟬 KN  Q' have False
      by auto
    then show ?case by simp
  next
    case(cBrMerge ΨQ M N P' AP ΨP Q' AQ)
    from Ψ  ΨP  𝟬  ¿MN  Q' have False
      by auto
    then show ?case by simp
  next
    case(cBrComm1 ΨQ M N P' AP ΨP xvec Q' AQ)
    from Ψ  ΨP  𝟬  ¡M⦇ν*xvec⦈⟨N  Q' have False
      by auto
    then show ?case by simp
  next
    case(cBrComm2 ΨQ M xvec N P' AP ΨP Q' AQ)
    from Ψ  ΨP  𝟬  ¿MN  Q' have False
      by auto
    then show ?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(clarsimp 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⦈.⦇νxP"
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⦈.⦇νxP"
    by(auto simp add: inputChainFresh abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    from Ψ  M⦇λ*xvec N⦈.⦇νxP α  P' x  α show ?case
    proof(induct rule: inputCases)
      case(cInput K Tvec)
      from x  KN[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)
      then have "Ψ  ⦇νx(M⦇λ*xvec N⦈.P) K(N[xvec::=Tvec])  ⦇νx(P[xvec::=Tvec])" using x  Ψ x  K x  N[xvec::=Tvec]
        by(intro 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]), (⦇νxP)[xvec::=Tvec])  Rel"
        by(force intro: C1)
      ultimately show ?case by blast
    next
      case(cBrInput K Tvec)
      from x  ¿KN[xvec::=Tvec] have "x  K" and "x  N[xvec::=Tvec]" by simp+
      from Ψ  K  M distinct xvec set xvec  supp N length xvec = length Tvec
      have "Ψ  M⦇λ*xvec N⦈.P ¿K(N[xvec::=Tvec])  P[xvec::=Tvec]"
        by(rule BrInput)
      then have "Ψ  ⦇νx(M⦇λ*xvec N⦈.P) ¿K(N[xvec::=Tvec])  ⦇νx(P[xvec::=Tvec])" using x  Ψ x  K x  N[xvec::=Tvec]
        by(intro 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]), (⦇νxP)[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⦈.⦇νxP ↝[Rel] ⦇νx(M⦇λ*xvec N⦈.P)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  M x  N have "x  M⦇λ*xvec N⦈.⦇νxP"
    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[where C="()"])
      case(cRes P')
      from Ψ  M⦇λ*xvec N⦈.P α  P' x  α show ?case
      proof(induct rule: inputCases)
        case(cInput K Tvec)
        from x  KN[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⦈.(⦇νxP) K(N[xvec::=Tvec])  (⦇νxP)[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 "(Ψ, (⦇νxP)[xvec::=Tvec], ⦇νx(P[xvec::=Tvec]))  Rel"
          by(force intro: C1)
        ultimately show ?case by blast
      next
        case(cBrInput K Tvec)
        from x  ¿KN[xvec::=Tvec] have "x  K" and "x  N[xvec::=Tvec]" by simp+
        from Ψ  K  M distinct xvec set xvec  supp N length xvec = length Tvec
        have "Ψ  M⦇λ*xvec N⦈.(⦇νxP) ¿K(N[xvec::=Tvec])  (⦇νxP)[xvec::=Tvec]"
          by(rule BrInput)
        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 "(Ψ, (⦇νxP)[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
      then show ?case by simp
    next
      case cBrOpen
      then have False by auto
      then show ?case by simp
    next
      case (cBrClose M xvec N P')
      then have False by auto
      then show ?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(MN⟩.P) ↝[Rel] MN⟩.⦇νxP"
proof -
  note eqvt Rel x  Ψ
  moreover have "x  ⦇νx(MN⟩.P)" by(simp add: abs_fresh)
  moreover from x  M x  N have "x  MN⟩.⦇νxP"
    by(auto simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "()"])
    case(cSim α P')
    from Ψ  MN⟩.⦇νxP α  P' x  α
    show ?case
    proof(induct rule: outputCases)
      case(cOutput K)
      from Ψ  M  K have "Ψ  MN⟩.P KN  P"
        by(rule Output)
      then have "Ψ  ⦇νx(MN⟩.P) KN  ⦇νxP" using x  Ψ x  KN
        by(rule Scope)
      moreover have "(Ψ, ⦇νxP, ⦇νxP)  Rel" by(rule C1)
      ultimately show ?case by blast
    next
      case(cBrOutput K)
      from Ψ  M  K have "Ψ  MN⟩.P ¡KN  P"
        by(rule BrOutput)
      then have "Ψ  ⦇νx(MN⟩.P) ¡KN  ⦇νxP" using x  Ψ x  ¡KN
        by(rule Scope)
      moreover have "(Ψ, ⦇νxP, ⦇νxP)  Rel" by(rule C1)
      ultimately show ?case by blast
    qed
  qed
qed

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

assumes "Ψ  MN⟩.P (¡K⦇ν*xvec⦈⟨N')  P'"
shows "xvec = []"
proof -
  from assms have "bn(¡K⦇ν*xvec⦈⟨N') = []"
    by(induct rule: outputCases) auto
  then show ?thesis by simp
qed

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

assumes "Ψ  MN⟩.P (¡K⦇ν*xvec⦈⟨N')  P'"
shows "N = N'"
proof -
  from assms have "object(¡K⦇ν*xvec⦈⟨N') = Some N"
    by(induct rule: outputCases) auto
  then show ?thesis
    by simp
qed

lemma brOutputOutputCases[consumes 1, case_names cBrOutput]:
  fixes Ψ :: 'b
    and M  :: 'a
    and N  :: 'a
    and P  :: "('a, 'b, 'c) psi"
    and α  :: "'a action"
    and P' :: "('a, 'b, 'c) psi"

assumes Trans: "Ψ  MN⟩.P (¡K⦇ν*xvec⦈⟨N')  P'"
  and   rBrOutput: "K. Ψ  M  K  Prop (¡KN) P"

shows "Prop (¡K⦇ν*xvec⦈⟨N') P'"
proof -
  have "xvec = []" using Trans by(rule broutputNoBind)
  then obtain K' N'' where eq: "(¡K⦇ν*xvec⦈⟨N')= ¡K'N''"
    by blast
  have "N = N'" using Trans by(rule broutputObjectEq)
  from Trans (¡K⦇ν*xvec⦈⟨N')= ¡K'N''
  show ?thesis unfolding N = N'[symmetric]
  proof(induct rule: outputCases)
    case (cOutput K) then show ?case by simp
  next
    case (cBrOutput K) then show ?case
      by(intro rBrOutput)
  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 "Ψ  MN⟩.⦇νxP ↝[Rel] ⦇νx(MN⟩.P)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  M x  N have "x  MN⟩.⦇νxP"
    by(auto simp add: abs_fresh)
  moreover have "x  ⦇νx(MN⟩.P)" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ "(M, N)"])
    case(cSim α P')
    note Ψ  ⦇νx(MN⟩.P) α  P' x  Ψ x  α x  P' bn α ♯* Ψ
    moreover from bn α ♯* (⦇νx(MN⟩.P)) x  α have "bn α ♯* (MN⟩.P)" by simp
    ultimately show ?case using bn α ♯* subject α bn α ♯* (M, N) x  α x  M x  N
    proof(induct rule: resCases[where C="()"])
      case(cOpen K xvec1 xvec2 y N' P')
      from bn(K⦇ν*(xvec1@y#xvec2)⦈⟨N') ♯* (M, N) have "y  N" by simp+
      from Ψ  MN⟩.P K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N')  ([(x, y)]  P')
      have "N = ([(x, y)]  N')"
        apply -
        by(ind_cases "Ψ  MN⟩.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)
      then show ?case by simp
    next
      case(cBrOpen K xvec1 xvec2 y N' P')
      from bn(¡K⦇ν*(xvec1@y#xvec2)⦈⟨N') ♯* (M, N) have "y  N" by simp+
      from Ψ  MN⟩.P ¡K⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N')  ([(x, y)]  P')
      have "N = ([(x, y)]  N')"
        apply -
        by(ind_cases "Ψ  MN⟩.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)
      then show ?case by simp
    next
      case(cRes P')
      from Ψ  MN⟩.P α  P' show ?case
      proof(induct rule: outputCases)
        case(cOutput K)
        from Ψ  M  K have "Ψ  MN⟩.(⦇νxP) KN  ⦇νxP"
          by(rule Output)
        moreover have "(Ψ, ⦇νxP, ⦇νxP)  Rel" by(rule C1)
        ultimately show ?case by force
      next
        case(cBrOutput K)
        from Ψ  M  K have "Ψ  MN⟩.(⦇νxP) ¡KN  ⦇νxP"
          by(rule BrOutput)
        moreover have "(Ψ, ⦇νxP, ⦇νxP)  Rel" by(rule C1)
        ultimately show ?case by force
      qed
    next
      case(cBrClose K xvec N' P')
      from Ψ  MN⟩.P  ¡K⦇ν*xvec⦈⟨N'  P'
      have "Ψ  M  the(subject(¡K⦇ν*xvec⦈⟨N'))"
        by(rule brOutputOutputCases) simp
      then have "Ψ  M  K" by simp
      then have "supp K  (supp M:: name set)" by(rule chanOutConSupp)
      then have False using x  supp K x  M unfolding fresh_def
        by blast
      then show ?case by(rule FalseE)
    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). (φ, ⦇νxP)) 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). (φ, ⦇νxP)) 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). (φ, ⦇νxP)) Cs) α  P''
    show ?case
    proof(induct rule: caseCases)
      case(cCase φ P')
      from (φ, P')  set (map (λ(φ, P). (φ, ⦇νxP)) Cs)
      obtain P where "(φ, P)  set Cs" and "P' = ⦇νxP"
        by(induct Cs) auto
      from guarded P' P' = ⦇νxP have "guarded P" by simp
      from Ψ  P' α  P'' P' = ⦇νxP have "Ψ  ⦇νxP α  P''"
        by simp
      moreover note x  Ψ x  α x  P'' bn α ♯* Ψ
      moreover from bn α ♯* Cs (φ, P)  set Cs
      have "bn α ♯* P" by(auto dest: memFreshChain)
      ultimately show ?case using bn α ♯* subject α x  α bn α ♯* Cs
      proof(induct rule: resCases[where C="()"])
        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)  set Cs Ψ  φ guarded P
        have "Ψ  Cases Cs M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')" by(rule Case)
        then have "([(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)
        then have "Ψ  ⦇ν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)
        then have "Ψ  ⦇ν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(cBrOpen 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)  set Cs Ψ  φ guarded P
        have "Ψ  Cases Cs ¡M⦇ν*(xvec1@xvec2)⦈⟨([(x, y)]  N)  ([(x, y)]  P')" by(rule Case)
        then have "([(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)
        then have "Ψ  ⦇νy([(x, y)]  (Cases Cs))  ¡M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  supp N y  Ψ y  M y  xvec1 y  xvec2
          by(rule BrOpen)
        then have "Ψ  ⦇ν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)  set Cs Ψ  φ guarded P
        have "Ψ  Cases Cs α  P'" by(rule Case)
        then have "Ψ  ⦇νx(Cases Cs) α  ⦇νxP'" using x  Ψ x  α
          by(rule Scope)
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule C1)
        ultimately show ?case by blast
      next
        case(cBrClose M xvec N P')
        from Ψ  P  ¡M⦇ν*xvec⦈⟨N  P' x  supp M x  Ψ
        have "Ψ  ⦇νxP  τ  ⦇νx(⦇ν*xvecP')"
          by(rule BrClose)
        from Ψ  P  ¡M⦇ν*xvec⦈⟨N  P' (φ, P)  set Cs Ψ  φ guarded P
        have "Ψ  Cases Cs  ¡M⦇ν*xvec⦈⟨N  P'"
          by(rule Case)
        then have "Ψ  ⦇νx(Cases Cs)  τ  ⦇νx(⦇ν*xvecP')" using x  supp M x  Ψ
          by(rule BrClose)
        moreover have "(Ψ,⦇νx(⦇ν*xvecP'),⦇νx(⦇ν*xvecP'))  Rel" by fact
        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). (φ, ⦇νxP)) Cs) ↝[Rel] ⦇νx(Cases Cs)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  map fst Cs have "x  Cases (map (λ(φ, P). (φ, ⦇νxP)) 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[where C="()"])
      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)
        then have "Ψ  ⦇νy([(x, y)]  P)  M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  supp N y  Ψ y  M y  xvec1 y  xvec2
          by(rule Open)
        then have "Ψ  ⦇νxP  M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  Cs (φ, P)  set Cs
          by(subst alphaRes, auto dest: memFresh)
        moreover from (φ, P)  set Cs have "(φ, ⦇νxP)  set (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
          by(induct Cs) auto
        moreover note Ψ  φ
        moreover from guarded P have "guarded(⦇νxP)" by simp
        ultimately have "Ψ  (Cases (map (λ(φ, P). (φ, ⦇νxP)) 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(cBrOpen 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)
        then have "Ψ  ⦇νy([(x, y)]  P)  ¡M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  supp N y  Ψ y  M y  xvec1 y  xvec2
          by(rule BrOpen)
        then have "Ψ  ⦇νxP ¡M⦇ν*(xvec1@y#xvec2)⦈⟨N  P'" using y  Cs (φ, P)  set Cs
          by(subst alphaRes, auto dest: memFresh)
        moreover from (φ, P)  set Cs have "(φ, ⦇νxP)  set (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
          by(induct Cs) auto
        moreover note Ψ  φ
        moreover from guarded P have "guarded(⦇νxP)" by simp
        ultimately have "Ψ  (Cases (map (λ(φ, P). (φ, ⦇νxP)) 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 "Ψ  ⦇νxP α  ⦇νxP'" by(rule Scope)
        moreover from (φ, P)  set Cs have "(φ, ⦇νxP)  set (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
          by(induct Cs) auto
        moreover note Ψ  φ
        moreover from guarded P have "guarded(⦇νxP)" by simp
        ultimately have "Ψ  (Cases (map (λ(φ, P). (φ, ⦇νxP)) Cs)) α  ⦇νxP'"
          by(rule Case)
        moreover have "(Ψ, ⦇νxP', ⦇νxP')  Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    next
      case(cBrClose M xvec N P')
      then show ?case
      proof(induct rule: caseCases)
        case(cCase φ P)
        from Ψ  P ¡M⦇ν*xvec⦈⟨N  P' x  Ψ x  supp M
        have "Ψ  ⦇νxP  τ  ⦇νx(⦇ν*xvecP')"
          by(intro BrClose)
        moreover from (φ, P)  set Cs have "(φ, ⦇νxP)  set (map (λ(φ, P). (φ, ⦇νxP)) Cs)"
          by(induct Cs) auto
        moreover from guarded P have "guarded(⦇νxP)" by simp
        moreover note Ψ  φ
        ultimately have "Ψ  Cases map (λ(φ, P). (φ, ⦇νxP)) Cs  τ  ⦇νx(⦇ν*xvecP')"
          by(intro Case)
        moreover have "(Ψ,⦇νx(⦇ν*xvecP'),⦇νx(⦇ν*xvecP'))  Rel"
          by fact
        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: "Ψ  ⦇νxP MN  P'"
  and   "x  Ψ"
  and   "x  M"
  and   "x  N"
  and   "x  P'"
  and   rScope:  "P'. Ψ  P MN  P'  Prop (⦇νxP')"

shows "Prop P'"
proof -
  note Trans x  Ψ
  moreover from x  M x  N have "x  MN" by simp
  moreover note x  P'
  ultimately show ?thesis using assms
    by(induct rule: resInputCases') simp
qed

lemma resBrInputCases[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: "Ψ  ⦇νxP ¿MN  P'"
  and   "x  Ψ"
  and   "x  M"
  and   "x  N"
  and   "x  P'"
  and   rScope:  "P'. Ψ  P ¿MN  P'  Prop (⦇νxP')"

shows "Prop P'"
proof -
  note Trans x  Ψ
  moreover from x  M x  N have "x  ¿MN" by simp
  moreover note x  P'
  ultimately show ?thesis using assms
    by(induct rule: resBrInputCases') simp
qed

lemma swap_supp:
  fixes x   :: name
    and y   :: name
    and N   :: 'a

assumes "y  supp N"

shows "x  supp ([(x, y)]  N)"
  using assms
  by (metis fresh_bij fresh_def swap_simps(2))

lemma swap_supp':
  fixes x   :: name
    and y   :: name
    and N   :: 'a

assumes "x  supp N"

shows "y  supp ([(x, y)]  N)"
  using assms
  by (metis fresh_bij fresh_def swap_simps(1))

lemma brOutputFreshSubjectChain:
  fixes Ψ   :: 'b
    and Q   :: "('a, 'b, 'c) psi"
    and M   :: 'a
    and xvec :: "name list"
    and N   :: 'a
    and Q'  :: "('a, 'b, 'c) psi"
    and yvec :: "name list"

assumes "Ψ  Q  ¡M⦇ν*xvec⦈⟨N  Q'"
  and "xvec ♯* M"
  and "yvec ♯* Q"

shows "yvec ♯* M"
  using assms
proof(induct yvec)
  case Nil
  then show ?case by simp
next
  case(Cons a yvec)
  then have "yvec ♯* M" by simp
  from (a # yvec) ♯* Q have "a  Q" by simp
  from xvec ♯* M a  Q Ψ  Q  ¡M⦇ν*xvec⦈⟨N  Q'
  have "a  M"
    by(simp add: brOutputFreshSubject)
  with yvec ♯* M show ?case
    by simp
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  ⦇νyS))  Rel"
  and   C3: "Ψ' zvec R y. y  Ψ'; zvec ♯* Ψ'  (Ψ', ⦇νy(⦇ν*zvecR), ⦇ν*zvec(⦇νyR))  Rel"
  ― ‹Addition for Broadcast›
  and   C4: "Ψ' R S zvec. zvec ♯* R; zvec ♯* Ψ'  (Ψ', (⦇ν*zvec(R  S)), (R  (⦇ν*zvecS)))  Rel"

shows "Ψ  ⦇νx(P  Q) ↝[Rel] P  ⦇νxQ"
proof -
  note eqvt Rel x  Ψ
  moreover have "x  ⦇νx(P  Q)" by(simp add: abs_fresh)
  moreover from x  P have "x  P  ⦇νxQ" by(simp add: abs_fresh)
  ultimately show ?thesis
  proof(induct rule: simIFresh[of _ _ _ _ _ x])
    case(cSim α PQ)
    from x  α bn α ♯* (P  ⦇νxQ) have "bn α ♯* Q" by simp
    note Ψ  P  ⦇νxQ α  PQ bn α ♯* Ψ
    moreover from bn α ♯* (P  ⦇νxQ) have "bn α ♯* P" and "bn α ♯* ⦇νxQ" 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'  ⦇νxQ have "x  P'" by simp
      have PTrans: "Ψ  ΨQ  P α  P'" by fact
      from extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
      then obtain y AQ' where A: "AQ = y#AQ'" by(cases 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)
      then have "Ψ  ⦇νy(P  ([(y, x)]  Q)) α  ⦇νy(P'  ([(y, x)]  Q))"
        using y  Ψ y  α
        by(rule Scope)
      then have "([(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'  ⦇νxQ))  Rel"
        by(rule C2) auto
      ultimately show ?case
        by force
    next
      case(cPar2 xQ' AP ΨP)
      from AP ♯* ⦇νxQ AP ♯* x have "AP ♯* Q" by simp
      note Ψ  ΨP  ⦇νxQ α  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(auto dest: extractFrameFreshChain)
      with bn α ♯* Ψ have "bn α ♯* (Ψ  ΨP)" by force
      ultimately show ?case using bn α ♯* Q bn α ♯* subject α x  α bn α ♯* P AP ♯* α bn α ♯* Ψ x  P
      proof(induct rule: resCases'[where C="(P, AP, Ψ)"])
        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(intro Par2) (assumption | simp)+
        then have "Ψ  ⦇ν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(cBrOpen 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(intro Par2) (assumption | simp)+
        then have "Ψ  ⦇ν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 BrOpen)
        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)
        then have "Ψ  ⦇νx(P  Q) α  ⦇νx(P  Q')" using x  Ψ x  α
          by(rule Scope)
        moreover from x  Ψ x  P have "(Ψ, ⦇νx(⦇ν*[](P  Q')), ⦇ν*[](P  ⦇νxQ'))  Rel"
          by(rule C2) auto
        ultimately show ?case
          by force
      next
        case(cBrClose M xvec N Q')
        from xvec ♯* (P, AP, Ψ)
        have "xvec ♯* P" and "AP ♯* xvec" and "xvec ♯* Ψ"
          by simp+
        from Ψ  ΨP  Q  ¡M⦇ν*xvec⦈⟨N  Q' AP ♯* Q
          xvec ♯* M
        have "AP ♯* M"
          by(simp add: brOutputFreshSubjectChain)

        from Ψ  ΨP  Q  ¡M⦇ν*xvec⦈⟨N  Q' xvec ♯* M distinct xvec AP ♯* Q AP ♯* xvec
        have "AP ♯* N" and "AP ♯* Q'" by(simp add: broutputFreshChainDerivative)+
        from AP ♯* M AP ♯* xvec AP ♯* N have "AP ♯* (¡M⦇ν*xvec⦈⟨N)"
          by simp

        from Ψ  ΨP  Q  ¡M⦇ν*xvec⦈⟨N  Q' extractFrame P = AP, ΨP xvec ♯* P AP ♯* Ψ AP ♯* Q AP ♯* (¡M⦇ν*xvec⦈⟨N)
        have "Ψ  P  Q  ¡M⦇ν*xvec⦈⟨N  P  Q'"
          by(simp add: Par2)

        from x  Ψ x  P xvec ♯* P xvec ♯* Ψ
        have "(x#xvec) ♯* P" and "(x#xvec) ♯* Ψ" by simp+
        then have "(Ψ, (⦇ν*(x#xvec)(P  Q')), P  (⦇ν*(x#xvec)Q'))  Rel"
          by(rule C4)
        then have "(Ψ, ⦇νx(⦇ν*xvec(P  Q')), P  ⦇νx(⦇ν*xvecQ'))  Rel"
          by simp

        moreover from Ψ  P  Q  ¡M⦇ν*xvec⦈⟨N  P  Q' x  supp M x  Ψ
        have "Ψ  ⦇νx(P  Q)  τ  ⦇νx(⦇ν*xvec(P  Q'))"
          by(rule BrClose)

        ultimately show ?case
          by force
      qed
    next
      case(cComm1 ΨQ M N P' AP ΨP K xvec xQ' AQ)
      have QTrans: "Ψ  ΨP  ⦇νxQ K⦇ν*xvec⦈⟨N  xQ'" and FrQ: "extractFrame(⦇νxQ) = AQ, ΨQ" by fact+
      have PTrans: "Ψ  ΨQ  P MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
      have "x  ⦇νxQ" 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  ⦇νxQ 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 ♯* ⦇νxQ AP ♯* x have "AP ♯* Q" by simp
      from AQ ♯* ⦇νxQ 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(elim inputObtainPrefix[where B="x#xvec@AQ"]) (assumption | force simp add: fresh_star_list_cons)+
      then 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)
      then have "(Ψ  ΨP)  ΨQ  K  M'" by(metis statEqEnt Associativity Commutativity Composition)
      with QTrans FrQ distinct AQ AQ ♯* Ψ AQ ♯* ΨP AQ ♯* (⦇νxQ) AQ ♯* K AQ ♯* M'
      have "Ψ  ΨP  ⦇νxQ 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 "xvec ♯* (Ψ  ΨP)" by force
      moreover from xvec ♯* ⦇νxQ x  xvec have "xvec ♯* Q" by simp
      moreover note xvec ♯* M'

      moreover from xvec ♯* Ψ xvec ♯* ΨP have "bn(M'⦇ν*xvec⦈⟨N) ♯* (Ψ  ΨP)" by force
      moreover from xvec ♯* ⦇νxQ 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: resOutputCases''''')
      	case(cOpen M'' xvec1 xvec2 y N' Q')
        then have Eq: "M'⦇ν*xvec⦈⟨N = M''⦇ν*(xvec1 @ y # xvec2)⦈⟨N'" by simp
        from x  M'⦇ν*xvec⦈⟨N Eq have "x  xvec1" and "x  y" and "x  xvec2" and "x  M''"
          by simp+
        from bn(M'⦇ν*xvec⦈⟨N) ♯* P Eq have "(xvec1@xvec2) ♯* P" and "y  P" by simp+
        from AQ ♯* (M'⦇ν*xvec⦈⟨N) Eq have "(xvec1@xvec2) ♯* AQ" and "y  AQ" and "AQ ♯* M''" by simp+
        from bn(M'⦇ν*xvec⦈⟨N) ♯* Ψ Eq have "(xvec1@xvec2) ♯* Ψ" and "y  Ψ" by simp+
        from Eq have "N = N'" and "xvec = xvec1@y#xvec2" and "M' = M''" by(simp add: action.inject)+
        from x  P y  P x  y Ψ  ΨQ  P MN  P'
        have "Ψ  ΨQ  P M([(y, x)]  N)  ([(y, x)]  P')"
          by(elim inputAlpha[where xvec="[y]"]) (auto simp add: calc_atm)
        then have PTrans: "Ψ  ΨQ  P M([(x, y)]  N)  ([(x, y)]  P')"
          by(simp add: name_swap)

        from Ψ  ΨP  [(x, y)]  Q  M''⦇ν*(xvec1 @ xvec2)⦈⟨N'  Q'
        have "[(x, y)]  (Ψ  ΨP  [(x, y)]  Q  M''⦇ν*(xvec1 @ xvec2)⦈⟨N'  Q')"
          by simp
        then have "[(x, y)]  (Ψ  ΨP)  ([(x, y)]  ([(x, y)]  Q))  ([(x, y)]  M'')⦇ν*([(x, y)]  (xvec1 @ xvec2))⦈⟨([(x, y)]  N')  [(x, y)]  Q'"
          by(simp add: eqvts)
        with x  (Ψ  ΨP) y  (Ψ  ΨP) x  xvec1 y  xvec1 x  xvec2 y  xvec2 x  M'' y  M''
        have QTrans: "Ψ  ΨP  Q  M''⦇ν*(xvec1 @ xvec2)⦈⟨([(x, y)]  N')  [(x, y)]  Q'"
          by simp
        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(elim outputFreshChainDerivative(2)) (assumption | simp)+

        from extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain z AQ' where A: "AQ = z#AQ'" by(cases 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(elim inputAlpha[where xvec="[x]"]) (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(intro Comm1) (assumption | simp)+
        withz  Ψ have "Ψ  ⦇νz(P  ([(x, z)]  Q)) τ  ⦇νz(⦇ν*(xvec1@xvec2)(([(x, z)]  [(x, y)]  P')  ([(x, z)]  [(x, y)]  Q')))"
          by(intro 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(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(cases 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 MN  P'
        have "Ψ  ΨQ  P M([(y, x)]  N)  [(y, x)]  P'"
          by(intro inputAlpha[where xvec="[y]"]) (auto simp add: calc_atm)
        then have "Ψ  Ψ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(intro Comm1) (assumption | simp)+
        withy  Ψ have "Ψ  ⦇νy(P  ([(x, y)]  Q)) τ  ⦇νy(⦇ν*xvec(([(x, y)]  P')  ([(x, y)]  Q')))"
          by(intro 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'  ⦇νxQ'))  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  ⦇νxQ KN  xQ'" and FrQ: "extractFrame(⦇νxQ) = 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  ⦇νxQ" 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 ♯* ⦇νxQ AP ♯* x have "AP ♯* Q" by simp
      from AQ ♯* ⦇νxQ AQ ♯* x have "AQ ♯* Q" by simp
      from xvec ♯* x xvec ♯* ⦇νxQ have "xvec ♯* Q" by simp

      from Ψ  ΨQ  P  M⦇ν*xvec⦈⟨N  P' have PResTrans: "Ψ  ΨQ  P  ROut M (⦇ν*xvecN ≺' P')"
        by(simp add: residualInject)

      from PResTrans 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(elim outputObtainPrefix[where B="x#AQ"]) (assumption | force simp add: fresh_star_list_cons)+
      then 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)
      then have "(Ψ  ΨP)  ΨQ  K  M'"
        by(metis statEqEnt Associativity Commutativity Composition)
      with QTrans FrQ distinct AQ AQ ♯* Ψ AQ ♯* ΨP AQ ♯* (⦇νxQ) AQ ♯* K AQ ♯* M'
      have "Ψ  ΨP  ⦇νxQ 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(elim inputFreshChainDerivative)

        with extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(cases 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(intro Comm2) (assumption | simp)+
        withy  Ψ have "Ψ  ⦇νy(P  ([(x, y)]  Q)) τ  ⦇νy(⦇ν*xvec(P'  ([(x, y)]  Q')))"
          by(intro 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'  ⦇νxQ'))  Rel"
          by(rule C2)
        ultimately show ?case by blast
      qed
    next
      case(cBrMerge ΨQ M N P' AP ΨP xQ' AQ)
      have QTrans: "Ψ  ΨP  ⦇νxQ ¿MN  xQ'" and FrQ: "extractFrame(⦇νxQ) = AQ, ΨQ" by fact+
      have PTrans: "Ψ  ΨQ  P ¿MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
      from x  α α = ¿MN have "x  M" and "x  N" by simp+
      from x  P'  xQ' have "x  xQ'" by simp
      from FrP AP ♯* x x  P have "x  ΨP"
        by(drule_tac extractFrameFresh) auto
      from PTrans x  P x  N have "x  P'"
        by(rule brinputFreshDerivative)
      have "x  ⦇νxQ" by(simp add: abs_fresh)
      with FrQ AQ ♯* x have "x  ΨQ"
        by(drule_tac extractFrameFresh) auto
      from AP ♯* ⦇νxQ AP ♯* x have "AP ♯* Q" by simp
      from AQ ♯* ⦇νxQ AQ ♯* x have "AQ ♯* Q" by simp
      from x  Ψ x  ΨP
      have "x  (Ψ  ΨP)" by force
      from Ψ  ΨP  ⦇νxQ  ¿MN  xQ' x  (Ψ  ΨP) x  M x  N x  xQ'
      show ?case
      proof(induct rule: resBrInputCases)
        case(cRes Q')
        have QTrans: "Ψ  ΨP  Q ¿MN  Q'" by fact
        with AQ ♯* Q AQ ♯* N have "AQ ♯* Q'"
          by(elim brinputFreshChainDerivative)

        with extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(cases AQ) auto
        with AQ ♯* Ψ AQ ♯* P AQ ♯* P' AQ ♯* ΨP AQ ♯* Q AQ ♯* M AQ ♯* Q' AQ ♯* N
        have "AQ' ♯* Ψ" and "AQ' ♯* P" and "AQ' ♯* ΨP" and "AQ' ♯* Q" and "AQ ♯* Q'"
          and "y  Ψ" and "y  P" and "y  P'" and "y  ΨP" and "y  Q" 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 ¿MN  Q' have "([(x, y)]  (Ψ  ΨP))  ([(x, y)]  Q) ([(x, y)]  (¿MN  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) ¿MN  ([(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
        ultimately have "Ψ  (P  ([(x, y)]  Q)) ¿MN  (P'  ([(x, y)]  Q'))"
          using AP ♯* Ψ AP ♯* P  AP ♯* AQ' AQ' ♯* Ψ AQ' ♯* P AP ♯* M AQ' ♯* M
          by(intro BrMerge)
        withy  Ψ y  M y  N have "Ψ  ⦇νy(P  ([(x, y)]  Q)) ¿MN  ⦇νy(P'  ([(x, y)]  Q'))"
          by(intro 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)
        moreover 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' have "⦇νy(P'  ([(x, y)]  Q')) =  ⦇νx(P'  Q')"
          by(subst alphaRes[of y]) (auto simp add: resChainFresh calc_atm eqvts fresh_left name_swap)
        ultimately have finTrans: "Ψ  ⦇νx(P  Q) ¿MN  ⦇νx(P'  Q')"
          by simp
        from x  Ψ x  P' have "[x] ♯* P'" and "[x] ♯* Ψ" by simp+
        then have "(Ψ, ⦇ν*[x](P'  Q'), (P'  (⦇ν*[x]Q')))  Rel"
          by(rule C4)
        then have "(Ψ, ⦇νx(P'  Q'), (P'  ⦇νxQ'))  Rel"
          by simp
        with finTrans show ?case by blast
      qed
    next
      case(cBrComm1 ΨQ M N P' AP ΨP xvec xQ' AQ)
      have QTrans: "Ψ  ΨP  ⦇νxQ ¡M⦇ν*xvec⦈⟨N  xQ'" and FrQ: "extractFrame(⦇νxQ) = AQ, ΨQ" by fact+
      have PTrans: "Ψ  ΨQ  P ¿MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
      from bn α ♯* x ¡M⦇ν*xvec⦈⟨N = α have "x  xvec" by force
      have "x  ⦇νxQ" by(simp add: abs_fresh)
      with QTrans have "x  N" and "x  xQ'" using x  xvec xvec ♯* M distinct xvec
        by(force intro: broutputFreshDerivative)+
      from PTrans x  P x  N  have "x  P'" by(rule brinputFreshDerivative)
      from x  ⦇νxQ 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 ♯* ⦇νxQ AP ♯* x have "AP ♯* Q" by simp
      from AQ ♯* ⦇νxQ AQ ♯* x have "AQ ♯* Q" by simp
      note QTrans
      moreover from x  Ψ x  ΨP have "x  Ψ  ΨP" by force
      moreover from x  xvec have "xvec ♯* x" by simp
      from x  α ¡M⦇ν*xvec⦈⟨N = α have "x  ¡M⦇ν*xvec⦈⟨N" by simp
      moreover note x  xQ'

      moreover from xvec ♯* Ψ xvec ♯* ΨP have "xvec ♯* (Ψ  ΨP)" by force
      moreover from xvec ♯* ⦇νxQ x  xvec have "xvec ♯* Q" by simp
      moreover note xvec ♯* M

      moreover from xvec ♯* Ψ xvec ♯* ΨP have "bn(¡M⦇ν*xvec⦈⟨N) ♯* (Ψ  ΨP)" by force
      moreover from xvec ♯* ⦇νxQ 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: resBrOutputCases')
      	case(cBrOpen M'' xvec1 xvec2 y N' Q')
        then have Eq: "¡M⦇ν*xvec⦈⟨N = ¡M''⦇ν*(xvec1 @ y # xvec2)⦈⟨N'" by simp
        from x  ¡M⦇ν*xvec⦈⟨N Eq have "x  xvec1" and "x  y" and "x  xvec2" and "x  M''"
          by simp+
        from bn(¡M⦇ν*xvec⦈⟨N) ♯* P Eq have "(xvec1@xvec2) ♯* P" and "y  P" by simp+
        from AQ ♯* (¡M⦇ν*xvec⦈⟨N) Eq have "(xvec1@xvec2) ♯* AQ" and "y  AQ" and "AQ ♯* M''" by simp+
        from bn(¡M⦇ν*xvec⦈⟨N) ♯* Ψ Eq have "(xvec1@xvec2) ♯* Ψ" and "y  Ψ" by simp+
        from Eq have "N = N'" and "xvec = xvec1@y#xvec2" and "M = M''" by(simp add: action.inject)+
        from x  P y  P x  y Ψ  ΨQ  P ¿MN  P'
        have "Ψ  ΨQ  P ¿M([(y, x)]  N)  ([(y, x)]  P')"
          by(intro brinputAlpha[where xvec="[y]"]) (auto simp add: calc_atm)
        then have PTrans: "Ψ  ΨQ  P ¿M([(x, y)]  N)  ([(x, y)]  P')"
          by(simp add: name_swap)

        from Ψ  ΨP  [(x, y)]  Q  ¡M''⦇ν*(xvec1 @ xvec2)⦈⟨N'  Q'
        have "[(x, y)]  (Ψ  ΨP  [(x, y)]  Q  ¡M''⦇ν*(xvec1 @ xvec2)⦈⟨N'  Q')"
          by simp
        then have "[(x, y)]  (Ψ  ΨP)  ([(x, y)]  ([(x, y)]  Q))  ¡([(x, y)]  M'')⦇ν*([(x, y)]  (xvec1 @ xvec2))⦈⟨([(x, y)]  N')  [(x, y)]  Q'"
          by(simp add: eqvts)
        with x  (Ψ  ΨP) y  (Ψ  ΨP) x  xvec1 y  xvec1 x  xvec2 y  xvec2 x  M'' y  M''
        have QTrans: "Ψ  ΨP  Q  ¡M''⦇ν*(xvec1 @ xvec2)⦈⟨([(x, y)]  N')  [(x, y)]  Q'"
          by simp
        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(elim broutputFreshChainDerivative(2)) (assumption | simp)+

        from extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain z AQ' where A: "AQ = z#AQ'" by(cases 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 AQ ♯* (¡M⦇ν*xvec⦈⟨N) A have "z  M" and "z  xvec" and "z  N" by simp+

        from y  supp N' N = N' have "y  supp N" by simp
        then have "x  supp ([(x, y)]  N)"
          by (rule swap_supp)
        then have zsupp: "z  supp ([(x, z)]  [(x, y)]  N)"
          by (rule swap_supp')

        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(elim brinputAlpha[where xvec="[x]"]) (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)) ¡M⦇ν*(xvec1@xvec2)⦈⟨([(x, z)]  [(x, y)]  N)  (([(x, z)]  [(x, y)]  P')  ([(x, z)]  [(x, y)]  Q'))"
          using M=M'' N=N' AP ♯* Ψ AP ♯* P  AP ♯* AQ' AQ' ♯* Ψ AQ' ♯* P (xvec1@xvec2) ♯* P AP ♯* M AQ' ♯* M''
          by(intro BrComm1) (assumption | simp)+
        then have permTrans: "Ψ  ⦇νz(P  ([(x, z)]  Q)) ¡M⦇ν*(xvec1@z#xvec2)⦈⟨([(x, z)]  [(x, y)]  N)  (([(x, z)]  [(x, y)]  P')  ([(x, z)]  [(x, y)]  Q'))"
          using zsupp z  Ψ z  M z  xvec1 z  xvec2
          by(rule BrOpen)

        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)
        with permTrans have permTrans2: "Ψ  ⦇νx(P  Q) ¡M⦇ν*(xvec1@z#xvec2)⦈⟨([(x, z)]  [(x, y)]  N)  (([(x, z)]  [(x, y)]  P')  ([(x, z)]  [(x, y)]  Q'))"
          by simp
        then have "Ψ  ⦇νx(P  Q)  RBrOut M (⦇ν*(xvec1@z#xvec2)([(x, z)]  [(x, y)]  N) ≺' (([(x, z)]  [(x, y)]  P')  ([(x, z)]  [(x, y)]  Q')))"
          by(simp add: residualInject)
        then have permTrans3: "Ψ  ⦇νx(P  Q)  RBrOut M (⦇ν*(xvec1@z#xvec2) (([(x, z)]  [(x, y)]  N) ≺' ([(x, z)]  [(x, y)]  (P'  Q'))))"
          by simp
        from z  N x  z z  y
        have "z  ([(x, y)]  N)"
          by (metis calc_atm(2) calc_atm(3) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def)
        from z  P' x  z z  y
        have "z  ([(x, y)]  P')"
          by (metis calc_atm(2) calc_atm(3) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def)
        from z  ([(x, y)]  N) have "x  ([(x, z)]  [(x, y)]  N)"
          by (metis calc_atm(2) calc_atm(3) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def)
        from z  ([(x, y)]  P') have "x  ([(x, z)]  [(x, y)]  P')"
          by (metis calc_atm(2) calc_atm(3) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def)
        moreover from z  [(x, y)]  Q'
        have "x  ([(x, z)]  [(x, y)]  Q')"
          by (metis calc_atm(2) calc_atm(3) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def)
        ultimately have "x  ([(x, z)]  [(x, y)]  (P'  Q'))"
          by simp
        have "z  set ((xvec1@z#xvec2))"
          by simp
        from x  ([(x, z)]  [(x, y)]  N) x  ([(x, z)]  [(x, y)]  (P'  Q')) z  set ((xvec1@z#xvec2))
        have eq1: "(⦇ν*(xvec1@z#xvec2) (([(x, z)]  [(x, y)]  N) ≺' ([(x, z)]  [(x, y)]  (P'  Q')))) = (⦇ν*([(z, x)]  (xvec1@z#xvec2)) (([(z, x)]  [(x, z)]  [(x, y)]  N) ≺' ([(z, x)]  [(x, z)]  [(x, y)]  (P'  Q'))))"
          by(rule boundOutputChainSwap)
        have eq2: "(⦇ν*([(z, x)]  (xvec1@z#xvec2)) (([(z, x)]  [(x, z)]  [(x, y)]  N) ≺' ([(z, x)]  [(x, z)]  [(x, y)]  (P'  Q')))) = (⦇ν*([(z, x)]  (xvec1@z#xvec2)) (([(x, y)]  N) ≺' ([(x, y)]  (P'  Q'))))"
          by auto (metis perm_swap(2))+
        from x  xvec1 x  xvec2 z  xvec1 z  xvec2
        have "([(z, x)]  (xvec1@z#xvec2)) = (xvec1@x#xvec2)"
          by(simp add: eqvts swap_simps)
        then have eq3: "(⦇ν*([(z, x)]  (xvec1@z#xvec2)) (([(x, y)]  N) ≺' ([(x, y)]  (P'  Q')))) = (⦇ν*(xvec1@x#xvec2) (([(x, y)]  N) ≺' ([(x, y)]  (P'  Q'))))"
          by simp

        from permTrans3 eq1 eq2 eq3 have noXZTrans: "Ψ  ⦇νx(P  Q)  RBrOut M (⦇ν*(xvec1@x#xvec2) (([(x, y)]  N) ≺' ([(x, y)]  (P'  Q'))))"
          by simp

        from x  N
        have "y  ([(x, y)]  N)"
          by (metis calc_atm(2) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def swap_simps(2))
        moreover from x  P' x  Q'
        have "y  ([(x, y)]  (P'  Q'))"
          by (metis fresh_left psi.fresh(5) singleton_rev_conv swap_simps(2))
        moreover have "x  set (xvec1@x#xvec2)"
          by simp
        ultimately have eq1: "⦇ν*(xvec1@x#xvec2)([(x, y)]  N) ≺' ([(x, y)]  (P'  Q')) = ⦇ν*([(x, y)]  (xvec1@x#xvec2))([(x, y)]  [(x, y)]  N) ≺' ([(x, y)]  [(x, y)]  (P'  Q'))"
          by(rule boundOutputChainSwap)
        have eq2: "⦇ν*([(x, y)]  (xvec1@x#xvec2))([(x, y)]  [(x, y)]  N) ≺' ([(x, y)]  [(x, y)]  (P'  Q')) = ⦇ν*([(x, y)]  (xvec1@x#xvec2))N ≺' (P'  Q')"
          by simp
        from x  xvec1 x  xvec2 y  xvec1 y  xvec2
        have eq3: "([(x, y)]  (xvec1@x#xvec2)) = (xvec1@y#xvec2)"
          by(simp add: eqvts swap_simps)

        from eq1 eq2 eq3 noXZTrans have "Ψ  ⦇νx(P  Q)  RBrOut M (⦇ν*(xvec1@y#xvec2)N ≺' (P'  Q'))"
          by simp
        then have "Ψ  ⦇νx(P  Q) ¡M⦇ν*(xvec1@y#xvec2)⦈⟨N  (P'  Q')"
          by(simp add: residualInject)

        with xvec = xvec1@y#xvec2
        have "Ψ  ⦇νx(P  Q) ¡M⦇ν*xvec⦈⟨N  (P'  Q')"
          by simp
        moreover have "(Ψ, P'  Q', P'  Q')  Rel"
          by(rule C1)

        ultimately show ?case
          by force
      next
        case(cRes Q')
        from x  ¡M⦇ν*xvec⦈⟨N
        have "x  M" and "x  xvec" and "x  N"
          by simp+
        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: broutputFreshChainDerivative)

        with extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(cases 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 "AQ' ♯* M" and "y  N"
          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  N have "y  [(x, y)]  N"
          by (metis calc_atm(2) fresh_right name_prm_name.simps(2) name_prm_name_def singleton_rev_conv swap_name_def swap_simps(2))

        from x  P y  P x  y Ψ  ΨQ  P ¿MN  P'
        have "Ψ  ΨQ  P ¿M([(y, x)]  N)  [(y, x)]  P'"
          by(elim brinputAlpha[where xvec="[y]"]) (auto simp add: calc_atm)
        then have "Ψ  Ψ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)) ¡M⦇ν*xvec⦈⟨([(x, y)]  N)  ([(x, y)]  P')  ([(x, y)]  Q')"
          using AP ♯* Ψ AP ♯* P  AP ♯* AQ' AQ' ♯* Ψ AQ' ♯* P xvec ♯* P AP ♯* M AQ' ♯* M
          by(intro BrComm1) (assumption | simp)+
        withy  Ψ y  M y  xvec y  [(x, y)]  N have "Ψ  ⦇νy(P  ([(x, y)]  Q)) ¡M⦇ν*xvec⦈⟨([(x, y)]  N)  ⦇νy(([(x, y)]  P')  ([(x, y)]  Q'))"
          by(intro 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(([(x, y)]  P')  ([(x, y)]  Q')) =  ⦇νx(P'  Q')"
          by(subst alphaRes[of y]) (auto simp add: resChainFresh calc_atm eqvts fresh_left name_swap)
        ultimately have "Ψ  ⦇νx(P  Q) ¡M⦇ν*xvec⦈⟨([(x, y)]  N)  ⦇νx(P'  Q')"
          by simp
        with x  N y  N
        have Trans: "Ψ  ⦇νx(P  Q) ¡M⦇ν*xvec⦈⟨N  ⦇νx(P'  Q')"
          by simp
        from x  P' x  Ψ
        have "(Ψ, ⦇ν*[x](P'  Q'), (P'  (⦇ν*[x]Q')))  Rel"
          by(intro C4) simp+
        then have Relation: "(Ψ, ⦇νx(P'  Q'), (P'  (⦇νxQ')))  Rel"
          by simp
        from Trans Relation show ?case
          by blast
      qed
    next
      case(cBrComm2 ΨQ M xvec N P' AP ΨP xQ' AQ)
      from x  α ¡M⦇ν*xvec⦈⟨N = α
      have "x  M" "x  xvec" "x  N"
        by force+
      have QTrans: "Ψ  ΨP  ⦇νxQ ¿MN  xQ'" and FrQ: "extractFrame(⦇νxQ) = 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 x  xvec xvec ♯* M distinct xvec
        by(force intro: broutputFreshDerivative)+
      have "x  ⦇νxQ" 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 ♯* ⦇νxQ AP ♯* x have "AP ♯* Q" by simp
      from AQ ♯* ⦇νxQ AQ ♯* x have "AQ ♯* Q" by simp
      from x  xvec xvec ♯* ⦇νxQ have "xvec ♯* Q" by simp

      from Ψ  ΨQ  P  ¡M⦇ν*xvec⦈⟨N  P' have PResTrans: "Ψ  ΨQ  P  RBrOut M (⦇ν*xvecN ≺' P')"
        by(simp add: residualInject)

      note QTrans
      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: brinputFreshDerivative simp add: abs_fresh)
      ultimately show ?case
      proof(induct rule: resBrInputCases)
        case(cRes Q')
        have QTrans: "Ψ  ΨP  Q ¿MN  Q'" by fact
        with AQ ♯* Q AQ ♯* N have "AQ ♯* Q'"
          by(elim brinputFreshChainDerivative)

        with extractFrame(⦇νxQ) = AQ, ΨQ have FrxQ: "⦇νx(extractFrame Q) = AQ, ΨQ" by simp
        then obtain y AQ' where A: "AQ = y#AQ'" by(cases 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 ¿MN  Q' have "([(x, y)]  (Ψ  ΨP))  ([(x, y)]  Q) ([(x, y)]  (¿MN  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) ¿MN  ([(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 x  xvec y  xvec have "xvec ♯* ([(x, y)]  Q)" by simp
        ultimately have "Ψ  (P  ([(x, y)]  Q)) ¡M⦇ν*xvec⦈⟨N  (P'  ([(x, y)]  Q'))"
          using AP ♯* Ψ AP ♯* P  AP ♯* AQ' AQ' ♯* Ψ AQ' ♯* P AP ♯* M AQ' ♯* M
          by(intro BrComm2) (assumption | simp)+
        with y  Ψ y  M y  xvec y  N have "Ψ  ⦇νy(P  ([(x, y)]  Q)) ¡M⦇ν*xvec⦈⟨N  ⦇νy(P'  ([(x, y)]  Q'))"
          by(intro 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' x  xvec y  xvec have "⦇νy(P'  ([(x, y)]  Q')) =  ⦇νx(P'  Q')"
          by(subst alphaRes[of y]) (auto simp add: resChainFresh calc_atm eqvts fresh_left name_swap)
        ultimately have "Ψ  ⦇νx(P  Q) ¡M⦇ν*xvec⦈⟨N  ⦇νx(P'  Q')"
          by simp
        moreover from x  Ψ x  P' have "(Ψ, ⦇ν*[x](P'  Q'), (P'  (⦇ν*[x]Q')))  Rel"
          by(intro C4) simp+
        moreover then have "(Ψ, ⦇νx(P'  Q'), (P'  (⦇νxQ')))  Rel"
          by simp
        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  ⦇νyS), ⦇νy(⦇ν*zvec(R  S)))  Rel"
  ― ‹Addition for Broadcast›
  and   C3: "Ψ' R S zvec. zvec ♯* R; zvec ♯* Ψ'  (Ψ', (R  (⦇ν*zvecS)), (⦇ν*zvec(R  S)))  Rel"

shows "Ψ  P  ⦇νxQ ↝[Rel] ⦇νx(P  Q)"
proof -
  note eqvt Rel x  Ψ
  moreover from x  P have "x  P  ⦇νxQ" 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  ⦇νxQ) 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[where C="()"])
      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)
        then show ?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  ⦇νxQ 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 ♯* ⦇νxQ" by(simp add: alphaRes)
        ultimately have "Ψ  P  (⦇νxQ) 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(intro Par2) auto
        moreover have "(Ψ, P  Q', P  Q')  Rel" by(rule C1)
        ultimately show ?case by blast
      qed
    next
      case(cBrOpen 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: parBrOutputCases[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: broutputFreshDerivative)
        with y  supp N have False by(simp add: fresh_def)
        then show ?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: BrOpen)
        with y  Q have "Ψ  ΨP  ⦇νxQ ¡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 ♯* ⦇νxQ" by(simp add: alphaRes)
        ultimately have "Ψ  P  (⦇νxQ) ¡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(intro Par2) auto
        moreover have "(Ψ, P  Q', P  Q')  Rel" by(rule C1)
        ultimately show ?case by blast
      next
        case(cBrComm1 ΨQ P' AP ΨP Q' AQ)
        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 extractFrame ([(x, y)]  Q) = AQ, ΨQ
        have "extractFrame (⦇νy([(x, y)]  Q)) = (y#AQ), ΨQ"
          by simp
        with y  Q
        have FrQ: "extractFrame (⦇νxQ) = (y#AQ), ΨQ"
          by(simp add: alphaRes)
        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: BrOpen)
        with y  Q have QTrans: "Ψ  ΨP  ⦇νxQ ¡M⦇ν*(xvec1@y#xvec2)⦈⟨N  Q'"
          by(simp add: alphaRes)
        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 ♯* ⦇νxQ" by(simp add: alphaRes)
        from AQ ♯* ([(x, y)]  Q) have "AQ ♯* ⦇νy([(x, y)]  Q)" by(auto simp add: fresh_star_def abs_fresh)
        with y  Q have "AQ ♯* ⦇νxQ" by(simp add: alphaRes)
        moreover from y  Q have "y  ⦇νxQ"
          by (metis resChain.base resChain.step resChainFresh)
        ultimately have "(y # AQ) ♯* (⦇νxQ)" by simp
        from Ψ  ΨQ  P  ¿MN  P' FrP QTrans FrQ
          AP ♯* Ψ AP ♯* P AP ♯* ⦇νxQ AP ♯* M AP ♯* y AP ♯* AQ
          y  Ψ AQ ♯* Ψ y  P AQ ♯* P (y#AQ) ♯* ⦇νxQ
          y  M AQ ♯* M y  P (xvec1@xvec2) ♯* P
        have "Ψ  P  (⦇νxQ) ¡M⦇ν*(xvec1@y#xvec2)⦈⟨N  (P'  Q')"
          by(intro BrComm1) (assumption | simp)+
        moreover have "(Ψ, P'  Q', P'  Q')  Rel" by(rule C1)
        ultimately show ?case by blast
      next
        case(cBrComm2 ΨQ P' AP ΨP Q' AQ)
        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: broutputFreshDerivative)
        with y  supp N have False by(simp add: fresh_def)
        then show ?case by simp
      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(⦇νxQ) = (x#AQ), ΨQ"
          by simp
        moreover from bn α ♯* Q have "bn α ♯* (⦇νxQ)" 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  ⦇νxQ α  (P'  ⦇νxQ)"
          by(rule Par1)
        moreover from x  P' x  Ψ have "(Ψ, ⦇ν*[](P'  (⦇νxQ)), ⦇νx(⦇ν*[](P'  Q)))  Rel"
          by(intro 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  ⦇νxQ α  ⦇νxQ'"
          by(intro Scope) auto
        moreover note FrP bn α ♯* P AP ♯* Ψ
        moreover from AP ♯* Q have "AP ♯* ⦇νxQ" by(simp add: fresh_star_def abs_fresh)
        ultimately have "Ψ  P  ⦇νxQ α  (P  ⦇νxQ')" using AP ♯* α
          by(rule Par2)
        moreover from x  P x  Ψ have "(Ψ, ⦇ν*[](P  (⦇νxQ')), ⦇νx(⦇ν*[](P  Q')))  Rel"
          by(intro C2) auto
        ultimately show ?case
          by force
      next
        case(cComm1 ΨQ M N P' AP ΨP K xvec Q' AQ)
        have PTrans: "Ψ  ΨQ  P MN  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(auto dest: extractFrameFresh)
        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(elim inputObtainPrefix[where B="x#AQ"]) (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)
        then have "(Ψ  Ψ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(elim outputRenameSubject) (assumption | force)+
        show ?case
        proof(cases "x  supp N")
          note PTrans FrP
          moreover assume "x  supp N"
          then have "Ψ  ΨP  ⦇νxQ M'⦇ν*([]@(x#xvec))⦈⟨N  Q'" using QTrans x  Ψ x  ΨP x  M' xvec ♯* x
            by(intro Open) (assumption | force simp add: fresh_list_nil)+
          then have QTrans: "Ψ  ΨP  ⦇νxQ M'⦇ν*(x#xvec)⦈⟨N  Q'" by simp
          moreover from extractFrame Q = AQ, ΨQ have "extractFrame(⦇νxQ) = (x#AQ), ΨQ"
            by simp
          moreover note MeqM' AP ♯* Ψ AP ♯* P
          moreover from  AP ♯* Q have "AP ♯* (⦇νxQ)" 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) ♯* (⦇νxQ)" by(simp add: fresh_star_def abs_fresh)
          moreover from x  P xvec ♯* P have "(x#xvec) ♯* P" by(simp)
          ultimately have "Ψ  P  ⦇νxQ τ  ⦇ν*(x#xvec)(P'  Q')" using AP ♯* M
            by(intro 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"
          then have "x  N" by(simp add: fresh_def)
          with QTrans x  Ψ x  ΨP x  M' xvec ♯* x
          have QTrans: "Ψ  ΨP  ⦇νxQ M'⦇ν*xvec⦈⟨N  ⦇νxQ'"
            by(intro Scope) (assumption | force)+
          moreover from PTrans x  P x  N have "x  P'" by(rule inputFreshDerivative)
          with extractFrame Q = AQ, ΨQ have "extractFrame(⦇νxQ) = (x#AQ), ΨQ"
            by simp
          moreover note MeqM' AP ♯* Ψ AP ♯* P
          moreover from  AP ♯* Q have "AP ♯* (⦇νxQ)" 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) ♯* (⦇νxQ)" by(simp add: fresh_star_def abs_fresh)
          moreover from x  P xvec ♯* P have "(x#xvec) ♯* P" by(simp)
          ultimately have "Ψ  P  ⦇νxQ τ  ⦇ν*xvec(P'  ⦇νxQ')" using AP ♯* M
            by(intro Comm1) (assumption | simp)+
          moreover from x  Ψ x  P' xvec ♯* Ψ have "(Ψ, ⦇ν*xvec(P'  ⦇νxQ'), ⦇ν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 KN  Q'" and FrQ: "extractFrame Q = AQ, ΨQ" by fact+
        from FrP x  P have "x  AP, ΨP"
          by(auto dest: extractFrameFresh)
        with AP ♯* x have "x  ΨP" by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from PTrans
        have "Ψ  ΨQ  P  ROut M (⦇ν*xvecN ≺' P')"
          by(simp add: residualInject)
        with 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(elim outputObtainPrefix[where B="x#AQ"]) (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)
        then have "(Ψ  Ψ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(auto intro: inputRenameSubject)

        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  ⦇νxQ M'N  ⦇νxQ'"
          by(intro Scope) (assumption | force)+

        note PTrans FrP QTrans
        moreover with extractFrame Q = AQ, ΨQ have "extractFrame(⦇νxQ) = (x#AQ), ΨQ"
          by simp
        moreover note MeqM' AP ♯* Ψ AP ♯* P
        moreover from  AP ♯* Q have "AP ♯* (⦇νxQ)" 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) ♯* (⦇νxQ)" by(simp add: fresh_star_def abs_fresh)
        moreover from xvec ♯* Q have "(x#xvec) ♯* (⦇νxQ)" by(simp add: abs_fresh fresh_star_def)
        ultimately have "Ψ  P  ⦇νxQ τ  ⦇ν*xvec(P'  ⦇νxQ')" using AP ♯* M
          by(intro Comm2) (assumption | simp)+
        moreover from x  Ψ x  P' xvec ♯* Ψ have "(Ψ, ⦇ν*xvec(P'  ⦇νxQ'), ⦇νx(⦇ν*xvec(P'  Q')))  Rel" by(rule C2)
        ultimately show ?case by blast
      next
        case(cBrMerge ΨQ M N P' AP ΨP Q' AQ)
        have PTrans: "Ψ  ΨQ  P ¿MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
        have QTrans: "Ψ  ΨP  Q ¿MN  Q'" and FrQ: "extractFrame Q = AQ, ΨQ" by fact+
        from FrP x  P have "x  AP, ΨP"
          by(auto dest: extractFrameFresh)
        with AP ♯* x have "x  ΨP"
          by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from x  α α = ¿MN have "x  M" and "x  N" by simp+
        from PTrans x  P x  N
        have "x  P'"
          by(rule brinputFreshDerivative)
        from QTrans x  Ψ  x  ΨP x  M x  N have QTrans: "Ψ  ΨP  ⦇νxQ ¿MN  ⦇νxQ'"
          by(intro Scope) (assumption | force)+

        note PTrans FrP QTrans
        moreover with extractFrame Q = AQ, ΨQ have "extractFrame(⦇νxQ) = (x#AQ), ΨQ"
          by simp
        moreover note AP ♯* Ψ AP ♯* P
        moreover from  AP ♯* Q have "AP ♯* (⦇νxQ)" 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) ♯* (⦇νxQ)" by(simp add: fresh_star_def abs_fresh)
        ultimately have Trans: "Ψ  P  ⦇νxQ ¿MN  (P'  ⦇νxQ')" using AP ♯* M
          by(intro BrMerge) (assumption | simp)+
        from x  Ψ x  P' have "(Ψ, (P'  (⦇ν*[x]Q')), ⦇ν*[x](P'  Q'))  Rel"
          by(intro C3) simp+
        then have Relation: "(Ψ, (P'  (⦇νxQ')), ⦇νx(P'  Q'))  Rel" by simp
        with Trans Relation show ?case by blast
      next
        case(cBrComm1 ΨQ M N P' AP ΨP xvec Q' AQ)
        from x  α ¡M⦇ν*xvec⦈⟨N = α have "x  M" and "x  xvec" and "x  N" by force+
        have PTrans: "Ψ  ΨQ  P ¿MN  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
        have QTrans: "Ψ  ΨP  Q ¡M⦇ν*xvec⦈⟨N  Q'" and FrQ: "extractFrame Q = AQ, ΨQ" by fact+
        from FrP x  P have "x  AP, ΨP"
          by(auto dest: extractFrameFresh)
        with AP ♯* x have "x  ΨP"
          by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        show ?case
        proof(cases "x  supp N")
          note PTrans FrP
          moreover assume "x  supp N"
          with x  N have False
            by(simp add: fresh_def)
          then show ?case
            by simp
        next
          note PTrans FrP
          moreover assume "x  supp N"
          from QTrans x  Ψ x  ΨP x  M x  N x  xvec
          have QTrans: "Ψ  ΨP  ⦇νxQ ¡M⦇ν*xvec⦈⟨N  ⦇νxQ'"
            by(intro Scope) (assumption | force)+
          moreover from PTrans x  P x  N have "x  P'" by(rule brinputFreshDerivative)
          with extractFrame Q = AQ, ΨQ have "extractFrame(⦇νxQ) = (x#AQ), ΨQ"
            by simp
          moreover note AP ♯* Ψ AP ♯* P
          moreover from  AP ♯* Q have "AP ♯* (⦇νxQ)" 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) ♯* (⦇νxQ)" by(simp add: fresh_star_def abs_fresh)
          moreover from x  P xvec ♯* P have "(x#xvec) ♯* P" by(simp)
          ultimately have Trans: "Ψ  P  ⦇νxQ ¡M⦇ν*xvec⦈⟨N  (P'  ⦇νxQ')" using AP ♯* M
            by(intro BrComm1) (assumption | simp)+
          from x  Ψ x  P' have "(Ψ, (P'  (⦇ν*[x]Q')), ⦇ν*[x](P'  Q'))  Rel"
            by(intro C3) simp+
          then have Relation: "(Ψ, (P'  (⦇νxQ')), ⦇νx(P'  Q'))  Rel" by simp
          from Trans Relation show ?case by blast
        qed
      next
        case(cBrComm2 ΨQ M xvec N P' AP ΨP Q' AQ)
        from x  α ¡M⦇ν*xvec⦈⟨N = α have "x  M" and "x  xvec" and "x  N" by force+
        have PTrans: "Ψ  ΨQ  P ¡M⦇ν*xvec⦈⟨N  P'" and FrP: "extractFrame P = AP, ΨP" by fact+
        have QTrans: "Ψ  ΨP  Q ¿MN  Q'" and FrQ: "extractFrame Q = AQ, ΨQ" by fact+
        from FrP x  P have "x  AP, ΨP"
          by(auto dest: extractFrameFresh)
        with AP ♯* x have "x  ΨP"
          by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from PTrans x  P x  xvec distinct xvec xvec ♯* M
        have "x  N" and "x  P'" by(force intro: broutputFreshDerivative)+
        from QTrans x  Ψ  x  ΨP x  M x  N have QTrans: "Ψ  ΨP  ⦇νxQ ¿MN  ⦇νxQ'"
          by(intro Scope) (assumption | force)+

        note PTrans FrP QTrans
        moreover with extractFrame Q = AQ, ΨQ have "extractFrame(⦇νxQ) = (x#AQ), ΨQ"
          by simp
        moreover note AP ♯* Ψ AP ♯* P
        moreover from  AP ♯* Q have "AP ♯* (⦇νxQ)" 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) ♯* (⦇νxQ)" by(simp add: fresh_star_def abs_fresh)
        moreover from xvec ♯* Q have "(x#xvec) ♯* (⦇νxQ)" by(simp add: abs_fresh fresh_star_def)
        ultimately have Trans: "Ψ  P  ⦇νxQ ¡M⦇ν*xvec⦈⟨N  (P'  ⦇νxQ')" using AP ♯* M
          by(intro BrComm2) (assumption | simp)+
        from x  Ψ x  P' have "(Ψ, (P'  (⦇ν*[x]Q')), ⦇ν*[x](P'  Q'))  Rel"
          by(intro C3) simp+
        then have Relation: "(Ψ, (P'  ⦇νxQ'), ⦇νx(P'  Q'))  Rel" by simp
        from Trans Relation show ?case by blast
      qed
    next
      case(cBrClose M xvec N PQ)
      from xvec ♯* (P  Q) have "xvec ♯* P" and "xvec ♯* Q" by simp+
      note Ψ  P  Q  ¡M⦇ν*xvec⦈⟨N  PQ xvec ♯* Ψ xvec ♯* P xvec ♯* Q xvec ♯* M
      then show ?case
      proof(induct rule: parBrOutputCases[where C=x])
        case(cPar1 P' AQ ΨQ)
        from Ψ  ΨQ  P  ¡M⦇ν*xvec⦈⟨N  P' xvec ♯* M x  P
        have "x  M"
          by(rule brOutputFreshSubject)
        with x  supp M have False
          by(simp add: fresh_def)
        then show ?case
          by simp
      next
        case(cPar2 Q' AP ΨP)
        from AP ♯* x have "x  AP" by simp
        with x  P extractFrame P = AP, ΨP
        have "x  ΨP"
          apply(drule_tac extractFrameFresh)
          by(simp add: frameResChainFresh) (simp add: fresh_def name_list_supp)
        from x  Ψ x  ΨP have "x  (Ψ  ΨP)" by force
        from Ψ  ΨP  Q  ¡M⦇ν*xvec⦈⟨N  Q' x  supp M x  (Ψ  ΨP)
        have QTrans: "Ψ  ΨP  ⦇νxQ  τ  ⦇νx(⦇ν*xvecQ')"
          by(rule BrClose)
        with extractFrame P = AP, ΨP AP ♯* Ψ x  AP AP ♯* Q
        have Trans: "Ψ  (P  ⦇νxQ)  τ  (P  ⦇νx(⦇ν*xvecQ'))"
          by(intro Par2) (assumption | simp)+
        from x  P xvec ♯* P have "(x#xvec) ♯* P" by simp
        moreover from x  Ψ xvec ♯* Ψ have "(x#xvec) ♯* Ψ" by simp
        ultimately have "(Ψ, (P  (⦇ν*(x#xvec)Q')), (⦇ν*(x#xvec)P  Q'))  Rel"
          by(rule C3)
        then have Relation: "(Ψ, (P  ⦇νx(⦇ν*xvecQ')), ⦇νx(⦇ν*xvecP  Q'))  Rel"
          by simp
        from Trans Relation
        show ?case
          by blast
      next
        case(cBrComm1 ΨQ P' AP ΨP Q' AQ)
        from Ψ  ΨQ  P  ¿MN  P' x  P
        have "x  M"
          by(rule brInputFreshSubject)
        with x  supp M have False
          by(simp add: fresh_def)
        then show ?case
          by simp
      next
        case(cBrComm2 ΨQ P' AP ΨP Q' AQ)
        from Ψ  ΨQ  P  ¡M⦇ν*xvec⦈⟨N  P' xvec ♯* M x  P
        have "x  M"
          by(rule brOutputFreshSubject)
        with x  supp M have False
          by(simp add: fresh_def)
        then show ?case
          by simp
      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 ♯* Ψ'  (Ψ', ⦇ν*xvecR, ⦇ν*xvecS)  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 MN  Q' extractFrame Q = AQ, ΨQ
    moreover from Ψ  ΨQ  ΨP  M  K
    have "Ψ  ΨQ  ΨP  K  M"
      by(rule chanEqSym)
    then have "Ψ  Ψ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(intro Comm2) (assumption | simp)+
    moreover have "(Ψ, P'  Q', Q'  P')  Rel" by(rule C1)
    then have "(Ψ, ⦇ν*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 KN  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)
    then have "Ψ  Ψ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(intro Comm1) (assumption | simp add: freshChainSym)+
    moreover have "(Ψ, P'  Q', Q'  P')  Rel" by(rule C1)
    then have "(Ψ, ⦇ν*xvec(P'  Q'), ⦇ν*xvec(Q'  P'))  Rel" using xvec ♯* Ψ by(rule C2)
    ultimately show ?case by blast
  next
    case(cBrMerge ΨP M N Q' AQ ΨQ P' AP)
    then have "Ψ  P  Q  ¿MN  P'  Q'"
      by(intro BrMerge) (assumption|simp)+
    then show ?case by(blast intro: C1)
  next
    case(cBrComm1 ΨP M N Q' AQ ΨQ xvec P' AP)
    then have "Ψ  P  Q  ¡M⦇ν*xvec⦈⟨N  P'  Q'"
      by(intro BrComm2) (assumption|simp)+
    then show ?case by(blast intro: C1)
  next
    case(cBrComm2 ΨP M xvec N Q' AQ ΨQ P' AP)
    then have "Ψ  P  Q  ¡M⦇ν*xvec⦈⟨N  P'  Q'"
      by(intro BrComm1) (assumption|simp)+
    then show ?case by(blast intro: C1)
  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 -
  {
    fix α P'
    assume "Ψ  !P α  P'"
    then have "Ψ  P  !P α  P'"
      apply -
      by(ind_cases "Ψ  !P α  P'") (auto simp add: psi.inject)
    moreover have "(Ψ, P', P')  Rel" by(rule C1)
    ultimately have "P''. Ψ  P  !P α  P''  (Ψ, P'', P')  Rel"
      by blast
  }
  then show ?thesis
    by(auto simp add: simulation_def)
qed

end

end