Theory Semantics

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

nominal_datatype ('a, 'b, 'c) boundOutput = 
  BOut "'a::fs_name" "('a, 'b::fs_name, 'c::fs_name) psi" (‹_ ≺'' _› [110, 110] 110)
| BStep "«name» ('a, 'b, 'c) boundOutput"                (⦇ν__› [110, 110] 110)

primrec BOresChain :: "name list  ('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput  
                      ('a, 'b, 'c) boundOutput" where
  Base: "BOresChain [] B = B"
| Step: "BOresChain (x#xs) B = ⦇νx(BOresChain xs B)"

abbreviation
  BOresChainJudge (⦇ν*__› [80, 80] 80) where "⦇ν*xvecB  BOresChain xvec B"

lemma BOresChainEqvt[eqvt]:
  fixes perm :: "name prm"
  and   lst  :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  
  shows "perm  (⦇ν*xvecB) = ⦇ν*(perm  xvec)(perm  B)"
by(induct_tac xvec, auto)

lemma BOresChainSimps[simp]:
  fixes xvec :: "name list"
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   N'   :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   B    :: "('a, 'b, 'c) boundOutput"
  and   B'    :: "('a, 'b, 'c) boundOutput"

  shows "(⦇ν*xvecN ≺' P = N' ≺' P') = (xvec = []  N = N'  P = P')"
  and   "(N' ≺' P' = ⦇ν*xvecN ≺' P) = (xvec = []  N = N'  P = P')"
  and   "(N' ≺' P' = N ≺' P) = (N = N'  P = P')"
  and   "(⦇ν*xvecB = ⦇ν*xvecB') = (B = B')"
by(induct xvec) (auto simp add: boundOutput.inject alpha)

lemma outputFresh[simp]:
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"

  shows "(Xs ♯* (N ≺' P)) = ((Xs ♯* N)  (Xs ♯* P))"
  and   "(xvec ♯* (N ≺' P)) = ((xvec ♯* N)  (xvec ♯* P))"
by(auto simp add: fresh_star_def)

lemma boundOutputFresh: 
  fixes x    :: name
  and   xvec :: "name list"
  and   B   :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"

  shows "(x  (⦇ν*xvecB)) = (x  set xvec  x  B)"
by (induct xvec) (simp_all add: abs_fresh)

lemma boundOutputFreshSet: 
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   yvec :: "name list"
  and   x    :: name

  shows "Xs ♯* (⦇ν*xvecB) = (xXs. x  set xvec  x  B)"
  and   "yvec ♯* (⦇ν*xvecB) = (x(set yvec). x  set xvec  x  B)"
  and   "Xs ♯* (⦇νxB) = Xs ♯* [x].B"
  and   "xvec ♯* (⦇νxB) = xvec ♯* [x].B"
by(simp add: fresh_star_def boundOutputFresh)+

lemma BOresChainSupp:
  fixes xvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"

  shows "(supp(⦇ν*xvecB)::name set) = (supp B) - (supp xvec)" 
by(induct xvec)
  (auto simp add: boundOutput.supp supp_list_nil supp_list_cons abs_supp supp_atm)

lemma boundOutputFreshSimps[simp]:
  fixes Xs   :: "name set"
  and   xvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   yvec :: "name list"
  and   x    :: name

  shows "Xs ♯* xvec  (Xs ♯* (⦇ν*xvecB)) = (Xs ♯* B)"
  and   "yvec ♯* xvec  yvec ♯* (⦇ν*xvecB) = yvec ♯* B"
  and   "xvec ♯* (⦇ν*xvecB)"
  and   "x  xvec  x  ⦇ν*xvecB = x  B"
apply(simp add: boundOutputFreshSet) apply(force simp add: fresh_star_def name_list_supp fresh_def)
apply(simp add: boundOutputFreshSet) apply(force simp add: fresh_star_def name_list_supp fresh_def)
apply(simp add: boundOutputFreshSet)  
by(simp add: BOresChainSupp fresh_def)

lemma boundOutputChainAlpha:
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   yvec :: "name list"

  assumes xvecFreshB: "(p  xvec) ♯* B"
  and     S: "set p  set xvec × set (p  xvec)"
  and     "(set xvec)  (set yvec)"

  shows "(⦇ν*yvecB) = (⦇ν*(p  yvec)(p  B))"
proof -
  note pt_name_inst at_name_inst S
  moreover from (set xvec)  (set yvec) have "set xvec ♯* (⦇ν*yvecB)"
    by(force simp add: boundOutputFreshSet)
  moreover from xvecFreshB (set xvec)  (set yvec) have "set (p  xvec) ♯* (⦇ν*yvecB)"
    by (simp add: boundOutputFreshSet) (simp add: fresh_star_def)
  ultimately have "(⦇ν*yvecB) = p  (⦇ν*yvecB)"
    by (rule_tac pt_freshs_freshs [symmetric])
  then show ?thesis by(simp add: eqvts)
qed

lemma boundOutputChainAlpha':
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   yvec :: "name list"
  and   zvec :: "name list"

  assumes xvecFreshB: "xvec ♯* B"
  and     S: "set p  set xvec × set yvec"
  and     "yvec ♯* (⦇ν*zvecB)"

  shows "(⦇ν*zvecB) = (⦇ν*(p  zvec)(p  B))"
proof -
  note pt_name_inst at_name_inst S yvec ♯* (⦇ν*zvecB)
  moreover from xvecFreshB have "set (xvec) ♯* (⦇ν*zvecB)"
    by (simp add: boundOutputFreshSet) (simp add: fresh_star_def)
  ultimately have "(⦇ν*zvecB) = p  (⦇ν*zvecB)"
    by (rule_tac pt_freshs_freshs [symmetric]) auto
  then show ?thesis by(simp add: eqvts)
qed

lemma boundOutputChainAlpha'':
  fixes p    :: "name prm"
  and   xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"

  assumes "(p  xvec) ♯* M"
  and     "(p  xvec) ♯* P"
  and      "set p  set xvec × set (p  xvec)"
  and     "(set xvec)  (set yvec)"

  shows "(⦇ν*yvecM ≺' P) = (⦇ν*(p  yvec)(p  M) ≺' (p  P))"
using assms
by(subst boundOutputChainAlpha) auto

lemma boundOutputChainSwap:
  fixes x    :: name
  and   y    :: name
  and   N    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   xvec :: "name list"

  assumes "y  N"
  and     "y  P"
  and     "x  (set xvec)"

  shows "⦇ν*xvecN ≺' P = ⦇ν*([(x, y)]  xvec)([(x ,y)]  N) ≺' ([(x, y)]  P)"
proof(case_tac "x=y")
  assume "x=y"
  thus ?thesis by simp
next
  assume "x  y"
  with assms show ?thesis
    by(rule_tac xvec="[x]" in boundOutputChainAlpha'') (auto simp add: calc_atm)
qed

lemma alphaBoundOutput:
  fixes x  :: name
  and   y  :: name
  and   B  :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"

  assumes "y  B"

  shows "⦇νxB = ⦇νy([(x, y)]  B)"
using assms
by(auto simp add: boundOutput.inject alpha fresh_left calc_atm)

lemma boundOutputEqFresh:
  fixes B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   C :: "('a, 'b, 'c) boundOutput"
  and   x :: name
  and   y :: name

  assumes "⦇νxB = ⦇νyC"
  and     "x  B"
  
  shows "y  C"
using assms
by(auto simp add: boundOutput.inject alpha fresh_left calc_atm)  

lemma boundOutputEqSupp:
  fixes B :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   C :: "('a, 'b, 'c) boundOutput"
  and   x :: name
  and   y :: name

  assumes "⦇νxB = ⦇νyC"
  and     "x  supp B"
  
  shows "y  supp C"
using assms
apply(auto simp add: boundOutput.inject alpha fresh_left calc_atm)
apply(drule_tac pi="[(x, y)]" in pt_set_bij2[OF pt_name_inst, OF at_name_inst])
by(simp add: eqvts calc_atm)

lemma boundOutputChainEq:
  fixes xvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   yvec :: "name list"
  and   B'   :: "('a, 'b, 'c) boundOutput"

  assumes "⦇ν*xvecB = ⦇ν*yvecB'"
  and     "xvec ♯* yvec"
  and     "length xvec = length yvec"

  shows "p. (set p)  (set xvec) × set (yvec)  distinctPerm p   B = p  B'  (set (map fst p))  (supp B)  xvec ♯* B'  yvec ♯* B"
proof -
  obtain n where "n = length xvec" by auto
  with assms show ?thesis
  proof(induct n arbitrary: xvec yvec B B')
    case(0 xvec yvec B B')
    have Eq: "⦇ν*xvecB = ⦇ν*yvecB'" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with length xvec = length yvec have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: boundOutput.inject)
  next
    case(Suc n xvec yvec B B')
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecB = ⦇ν*yvecB' xvec = x # xvec' length xvec = length yvec
    obtain y yvec' where "⦇ν*(x#xvec')B = ⦇ν*(y#yvec')B'"
      and "yvec = y#yvec'" and "length xvec' = length yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx(⦇ν*xvec'B) = ⦇νy(⦇ν*yvec'B')"
      by simp
    from xvec = x#xvec' yvec=y#yvec' xvec ♯* yvec
    have "x  y" and "xvec' ♯* yvec'" and "x  yvec'" and "y  xvec'"
      by auto
    have IH: "xvec yvec B B'. ⦇ν*xvec(B::('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput) = ⦇ν*yvecB'; xvec ♯* yvec; length xvec = length yvec; n = length xvec  p. (set p)  (set xvec) × (set yvec)  distinctPerm p   B = p  B'  set(map fst p)  supp B  xvec ♯* B'  yvec ♯* B"
      by fact
    from EQ x  y have EQ': "⦇ν*xvec'B = ([(x, y)]  (⦇ν*yvec'B'))" 
                     and xFreshB': "x  (⦇ν*yvec'B')"
                     and yFreshB: "y  (⦇ν*xvec'B)"
      by(metis boundOutput.inject alpha)+
    from xFreshB' x  yvec' have "x  B'"
      by(auto simp add: boundOutputFresh) (simp add: fresh_def name_list_supp)+
    from yFreshB y  xvec' have "y  B"
      by(auto simp add: boundOutputFresh) (simp add: fresh_def name_list_supp)+
    show ?case
    proof(case_tac "x  ⦇ν*xvec'B")
      assume xFreshB: "x  ⦇ν*xvec'B"
      with EQ have yFreshB': "y  ⦇ν*yvec'B'"
        by(rule boundOutputEqFresh)
      with xFreshB' EQ' have "⦇ν*xvec'B = ⦇ν*yvec'B'" 
        by(simp)
      with xvec' ♯* yvec' length xvec' = length yvec' length xvec' = n IH
      obtain p where S: "(set p)  (set xvec') × (set yvec')" and "distinctPerm p" and "B = p  B'"
                 and "set(map fst p)  supp B" and "xvec' ♯* B'"  and "yvec' ♯* B"
        by blast
      from S have "(set p)  set(x#xvec') × set(y#yvec')" by auto
      moreover note xvec = x#xvec' yvec=y#yvec' distinctPerm p B = p  B'
                    xvec' ♯* B' x  B' x  B' yvec' ♯* B y  B set(map fst p)  supp B

      ultimately show ?case by auto
    next
      assume "¬(x  ⦇ν*xvec'B)"
      hence xSuppB: "x  supp(⦇ν*xvec'B)"
        by(simp add: fresh_def)
      with EQ have ySuppB': "y  supp (⦇ν*yvec'B')"
        by(rule boundOutputEqSupp)
      hence "y  yvec'"
        by(induct yvec') (auto simp add: boundOutput.supp abs_supp)      
      with x  yvec' EQ' have "⦇ν*xvec'B = ⦇ν*yvec'([(x, y)]  B')"
        by(simp add: eqvts)
      with  xvec' ♯* yvec' length xvec' = length yvec' length xvec' = n IH
      obtain p where S: "(set p)  (set xvec') × (set yvec')" and "distinctPerm p" and "B = p  [(x, y)]  B'"
                 and "set(map fst p)  supp B" and "xvec' ♯* ([(x, y)]  B')" and "yvec' ♯* B" 
        by blast

      from xSuppB have "x  xvec'"
        by(induct xvec') (auto simp add: boundOutput.supp abs_supp)      
      with x  yvec' y  xvec' y  yvec' S have "x  p" and "y  p"
        apply(induct p)
        by(auto simp add: name_list_supp) (auto simp add: fresh_def) 
      from S have "(set ((x, y)#p))  (set(x#xvec')) × (set(y#yvec'))"
        by force
      moreover from x  y x  p y  p S distinctPerm p
      have "distinctPerm((x,y)#p)" by simp
      moreover from B = p  [(x, y)]  B' x  p y  p have "B = [(x, y)]  p  B'"
        by(subst perm_compose) simp
      hence "B = ((x, y)#p)  B'" by simp
      moreover from xvec' ♯* ([(x, y)]  B') have "([(x, y)]  xvec') ♯* ([(x, y)]  [(x, y)]  B')"
        by(simp only: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with x  xvec' y  xvec' x  B' have "(x#xvec') ♯* B'" by simp
      moreover from y  B yvec' ♯* B have "(y#yvec') ♯* B" by simp
      moreover from set(map fst p)  supp B xSuppB x  xvec'
      have "set(map fst ((x, y)#p))  supp B"
        by(simp add: BOresChainSupp)
      ultimately show ?case using xvec=x#xvec' yvec=y#yvec'
        by metis
    qed
  qed
qed

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

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q"

  shows "length xvec = length yvec"
proof -
  obtain n where "n = length xvec" by auto
  with assms show ?thesis
  proof(induct n arbitrary: xvec yvec M P N Q)
    case(0 xvec yvec M P N Q)
    from 0 = length xvec have "xvec = []" by auto
    moreover with ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case by simp
  next
    case(Suc n xvec yvec M P N Q)
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q xvec = x # xvec'
    obtain y yvec' where "⦇ν*(x#xvec')M ≺' P = ⦇ν*(y#yvec')N ≺' Q"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx(⦇ν*xvec'M ≺' P) = ⦇νy(⦇ν*yvec'N ≺' Q)"
      by simp
    have IH: "xvec yvec M P N Q. ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q::('a, 'b, 'c) psi); n = length xvec  length xvec = length yvec"
      by fact
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "⦇ν*xvec'M ≺' P  = ⦇ν*yvec'N ≺' Q"
        by(simp add: alpha boundOutput.inject)
      with IH length xvec' = n have "length xvec' = length yvec'"
        by blast
      with xvec = x#xvec' yvec=y#yvec'
      show ?case by simp
    next
      assume "x  y"
      with EQ have "⦇ν*xvec'M ≺' P = [(x, y)]  ⦇ν*yvec'N ≺' Q"
        by(simp add: alpha boundOutput.inject)
      hence "⦇ν*xvec'M ≺' P = ⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' ([(x, y)]  Q)"
        by(simp add: eqvts)
      with IH length xvec' = n have "length xvec' = length ([(x, y)]  yvec')"
        by blast
      hence "length xvec' = length yvec'"
        by simp
      with xvec = x#xvec' yvec=y#yvec'
      show ?case by simp
    qed
  qed
qed

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

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q"
  and     "xvec ♯* yvec"

  shows "p. (set p)  (set xvec) × set (yvec)  distinctPerm p   M = p  N   P = p  Q  xvec ♯* N  xvec ♯* Q  yvec ♯* M  yvec ♯* P"
using assms
apply(frule_tac boundOutputChainEqLength)
apply(drule_tac boundOutputChainEq)
by(auto simp add: boundOutput.inject)

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

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q"
  and     "xvec ♯* yvec"
  and     "distinct xvec"
  and     "distinct yvec"

  obtains p where "(set p)  (set xvec) × set (p  xvec)" and "distinctPerm p" and "yvec = p  xvec" and "N = p  M" and "Q = p  P" and "xvec ♯* N" and "xvec ♯* Q" and "(p  xvec) ♯* M" and "(p  xvec) ♯* P"
proof -

  assume "p. set p  set xvec × set (p  xvec); distinctPerm p; yvec = p  xvec; N = p  M; Q = p  P; xvec ♯* N; xvec ♯* Q; (p  xvec) ♯* M; (p  xvec) ♯* P  thesis"

  moreover obtain n where "n = length xvec" by auto
  with assms have "p. (set p)  (set xvec) × set (yvec)  distinctPerm p   yvec = p  xvec  N = p  M  Q = p  P  xvec ♯* N  xvec ♯* Q  (p  xvec) ♯* M  (p  xvec) ♯* P"
  proof(induct n arbitrary: xvec yvec M P N Q)
    case(0 xvec yvec M P N Q)
    have Eq: "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: boundOutput.inject)
  next
    case(Suc n xvec yvec M P N Q)
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' Q xvec = x # xvec'
    obtain y yvec' where "⦇ν*(x#xvec')M ≺' P = ⦇ν*(y#yvec')N ≺' Q"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx(⦇ν*xvec'M ≺' P) = ⦇νy(⦇ν*yvec'N ≺' Q)"
      by simp
    from xvec = x#xvec' yvec=y#yvec' xvec ♯* yvec
    have "x  y" and "xvec' ♯* yvec'" and "x  yvec'" and "y  xvec'"
      by auto
    from distinct xvec distinct yvec xvec=x#xvec' yvec=y#yvec' have "x  xvec'" and "y  yvec'" and "distinct xvec'" and "distinct yvec'"
      by simp+
    have IH: "xvec yvec M P N Q. ⦇ν*xvec(M::'a) ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvecN ≺' Q; xvec ♯* yvec; distinct xvec; distinct yvec; n = length xvec  p. (set p)  (set xvec) × (set yvec)  distinctPerm p   yvec = p  xvec  N = p  M  Q = p  P  xvec ♯* N  xvec ♯* Q  (p  xvec) ♯* M  (p  xvec) ♯* P"
      by fact 
    from EQ x  y  x  yvec' y  yvec' y  xvec' x  xvec' have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  Q)" and "x  N" and "x  Q" and "y  M" and "y  P"
      apply -
      apply(simp add: boundOutput.inject alpha eqvts)
      apply(simp add: boundOutput.inject alpha eqvts)
      apply(simp add: boundOutput.inject alpha eqvts)
      by(simp add: boundOutput.inject alpha' eqvts)+
    with xvec' ♯* yvec' distinct xvec' distinct yvec' length xvec' = n IH
    obtain p where S: "(set p)  (set xvec') × (set yvec')" and "distinctPerm p" and "yvec' = p  xvec'" and "([(x, y)]  N) = p  M" and "([(x, y)]  Q) = p  P" and "xvec' ♯* ([(x, y)]  N)" and "xvec' ♯* ([(x, y)]  Q)" and "yvec' ♯* M" and "yvec' ♯* P"
      by metis
    from S have "set((x, y)#p)  set(x#xvec') × set(y#yvec')" by auto
    moreover from x  xvec' x  yvec' y  xvec' y  yvec' S have "x  p" and "y  p"
      apply(induct p)
      by(auto simp add: fresh_prod name_list_supp) (auto simp add: fresh_def) 

    with S distinctPerm p x  y have "distinctPerm((x, y)#p)" by auto
    moreover from yvec' = p  xvec' x  p y  p x  xvec' y  xvec' have "(y#yvec') = ((x, y)#p)  (x#xvec')"
      by(simp add: eqvts calc_atm perm_compose freshChainSimps)
    moreover from ([(x, y)]  N) = p  M
    have "([(x, y)]  [(x, y)]  N) = [(x, y)]  p  M"
      by(simp add: pt_bij)
    hence "N = ((x, y)#p)  M" by simp
    moreover from ([(x, y)]  Q) = p  P
    have "([(x, y)]  [(x, y)]  Q) = [(x, y)]  p  P"
      by(simp add: pt_bij)
    hence "Q = ((x, y)#p)  P" by simp
    moreover from xvec' ♯* ([(x, y)]  N) have "([(x, y)]  xvec') ♯* ([(x, y)]  [(x, y)]  N)"
      by(subst fresh_star_bij)
    with x  xvec' y  xvec' have "xvec' ♯* N" by simp
    with x  N have "(x#xvec') ♯* N" by simp
    moreover from xvec' ♯* ([(x, y)]  Q) have "([(x, y)]  xvec') ♯* ([(x, y)]  [(x, y)]  Q)"
      by(subst fresh_star_bij)
    with x  xvec' y  xvec' have "xvec' ♯* Q" by simp
    with x  Q have "(x#xvec') ♯* Q" by simp
    moreover from y  M yvec' ♯* M have "(y#yvec') ♯* M" by simp
    moreover from y  P yvec' ♯* P have "(y#yvec') ♯* P" by simp
    ultimately show ?case using xvec=x#xvec' yvec=y#yvec'
      by metis
  qed
  ultimately show ?thesis by blast
qed

lemma boundOutputEqSupp':
  fixes x    :: name
  and   xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   y    :: name
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"

  assumes Eq: "⦇νx(⦇ν*xvecM ≺' P) = ⦇νy(⦇ν*yvecN ≺' Q)"
  and     "x  y"
  and     "x  yvec"
  and     "x  xvec"
  and     "y  xvec"
  and     "y  yvec"
  and     "xvec ♯* yvec"
  and     "x  supp M"
  
  shows "y  supp N"
proof -
  from Eq x  y x  yvec y  yvec have "⦇ν*xvecM ≺' P = ⦇ν*yvec([(x, y)]  N) ≺' ([(x, y)]  Q)"
    by(simp add: boundOutput.inject alpha eqvts)
  then obtain p where S: "set p  set xvec × set yvec" and "M = p  [(x, y)]  N" and "distinctPerm p" using xvec ♯* yvec
    by(blast dest: boundOutputChainEq')
  with x  supp M have "x  supp(p  [(x, y)]  N)" by simp
  hence "(p  x)  p  supp(p  [(x, y)]  N)"
    by(simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst])
  with x  xvec x  yvec S distinctPerm p have "x  supp([(x, y)]  N)"
    by(simp add: eqvts)
  hence "([(x, y)]  x)  ([(x, y)]  (supp([(x, y)]  N)))"
    by(simp add: pt_set_bij[OF pt_name_inst, OF at_name_inst])
  with x  y show ?thesis by(simp add: calc_atm eqvts)
qed

lemma boundOutputChainOpenIH:
  fixes xvec :: "name list"
  and   x    :: name
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"
  and   yvec :: "name list"
  and   y    :: name
  and   B'   :: "('a, 'b, 'c) boundOutput"

  assumes Eq: "⦇ν*xvec(⦇νxB) = ⦇ν*yvec(⦇νyB')"
  and     L: "length xvec = length yvec"
  and     xFreshB': "x  B'"
  and     xFreshxvec: "x  xvec"
  and     xFreshyvec: "x  yvec"

  shows "⦇ν*xvecB = ⦇ν*yvec([(x, y)]  B')"
using assms
proof(induct n=="length xvec" arbitrary: xvec yvec y B' rule: nat.induct)
  case(zero xvec yvec y B')
  have "0 = length xvec" and "length xvec = length yvec" by fact+
  moreover have "⦇ν*xvec⦇νxB = ⦇ν*yvec⦇νyB'" by fact
  ultimately show ?case by(auto simp add: boundOutput.inject alpha)
next
  case(Suc n xvec yvec y B')
  have L: "length xvec = length yvec" and "Suc n = length xvec" by fact+
  then obtain x' xvec' y' yvec' where xEq: "xvec = x'#xvec'" and yEq: "yvec = y'#yvec'"
                                  and L': "length xvec' = length yvec'"
    by(cases xvec, auto, cases yvec, auto)
  have xFreshB': "x  B'" by fact
  have "x  xvec" and "x  yvec" by fact+
  with xEq yEq have xineqx': "x  x'" and xFreshxvec': "x  xvec'"
                and xineqy': "x  y'" and xFreshyvec': "x  yvec'"
    by simp+
  have "⦇ν*xvec⦇νxB = ⦇ν*yvec⦇νyB'" by fact
  with xEq yEq have Eq: "⦇νx'(⦇ν*xvec'⦇νxB) = ⦇νy'(⦇ν*yvec'⦇νyB')" by simp
  have "Suc n = length xvec" by fact
  with xEq have L'': "n = length xvec'" by simp
  have "⦇νx'(⦇ν*xvec'B) = ⦇νy'(⦇ν*yvec'([(x, y)]  B'))"
  proof(case_tac "x'=y'")
    assume x'eqy': "x' = y'"
    with Eq have "⦇ν*xvec'⦇νxB = ⦇ν*yvec'⦇νyB'" by(simp add: boundOutput.inject alpha)
    hence "⦇ν*xvec'B = ⦇ν*yvec'([(x, y)]  B')" using L' xFreshB' xFreshxvec' xFreshyvec' L'' 
      by(rule_tac Suc)
    with x'eqy' show ?thesis by(simp add: boundOutput.inject alpha)
  next
    assume x'ineqy': "x'  y'"
    with Eq have Eq': "⦇ν*xvec'⦇νxB = ⦇ν*([(x', y')]  yvec')⦇ν([(x', y')]  y)([(x', y')]  B')"
             and x'FreshB': "x'  ⦇ν*yvec'⦇νyB'"
      by(simp add: boundOutput.inject alpha eqvts)+
    from L' have "length xvec' = length ([(x', y')]  yvec')" by simp
    moreover from xineqx' xineqy' xFreshB' have "x  [(x', y')]  B'" by(simp add: fresh_left calc_atm)
    moreover from xineqx' xineqy' xFreshyvec' have "x  [(x', y')]  yvec'" by(simp add: fresh_left calc_atm)
    ultimately have "⦇ν*xvec'B = ⦇ν*([(x', y')]  yvec')([(x, ([(x', y')]  y))]  [(x', y')]  B')" using Eq' xFreshxvec' L''
      by(rule_tac Suc)
    moreover from x'FreshB' have "x'  ⦇ν*yvec'([(x, y)]  B')"
    proof(case_tac "x'  yvec'")
      assume "x'  yvec'"
      with x'FreshB' have x'FreshB': "x'  ⦇νyB'"
        by(simp add: fresh_def BOresChainSupp)
      show ?thesis
      proof(case_tac "x'=y")
        assume x'eqy: "x' = y"
        show ?thesis
        proof(case_tac "x=y")
          assume "x=y"
          with xFreshB' x'eqy show ?thesis by(simp add: BOresChainSupp fresh_def)
        next
          assume "x  y"
          with x  B' have "y  [(x, y)]  B'" by(simp add: fresh_left calc_atm)
          with x'eqy show ?thesis by(simp add: BOresChainSupp fresh_def)
        qed
      next
        assume x'ineqy: "x'  y"
        with x'FreshB' have "x'  B'" by(simp add: abs_fresh)
        with xineqx' x'ineqy have "x'  ([(x, y)]  B')" by(simp add: fresh_left calc_atm)
        thus ?thesis by(simp add: BOresChainSupp fresh_def)
      qed
    next
      assume "¬x'  yvec'"
      thus ?thesis by(simp add: BOresChainSupp fresh_def)
    qed
    ultimately show ?thesis using x'ineqy' xineqx' xineqy'
      apply(simp add: boundOutput.inject alpha eqvts)
      apply(subst perm_compose[of "[(x', y')]"])
      by(simp add: calc_atm)
  qed
  with xEq yEq show ?case by simp
qed

lemma boundOutputPar1Dest:
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)"
  and     "xvec ♯* R"
  and     "yvec ♯* R"

  obtains T where "P = T  R" and "⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q"
proof -
  assume "T. P = T  R; ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "T. P = T  R  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: boundOutput.inject)
  next
    case(Suc n xvec yvec M N P Q R)
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R) xvec = x # xvec'
    obtain y yvec' where "⦇ν*(x#xvec')M ≺' P = ⦇ν*(y#yvec')N ≺' (Q  R)"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx(⦇ν*xvec'M ≺' P) = ⦇νy(⦇ν*yvec'N ≺' (Q  R))"
      by simp
    from xvec ♯* R yvec ♯* R xvec = x#xvec' yvec = y#yvec'
    have "x  R" and "xvec' ♯* R" and "y  R" and "yvec' ♯* R" by auto
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'N ≺' (Q  R)"
        by(simp add: boundOutput.inject alpha)
      with xvec' ♯* R yvec' ♯* R length xvec' = n
      obtain T where "P = T  R" and "⦇ν*xvec'M ≺' T = ⦇ν*yvec'N ≺' Q"
        by(drule_tac Suc) auto
      with xvec=x#xvec' yvec=y#yvec' x=y show ?case
        by(force simp add: boundOutput.inject alpha)
    next
      assume "x  y"
      with EQ x  R y  R
      have "⦇ν*xvec'M ≺' P = ⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' (([(x, y)]  Q)  R)"
       and xFreshQR: "x  ⦇ν*yvec'N ≺' (Q  R)"
        by(simp add: boundOutput.inject alpha eqvts)+
      moreover from yvec' ♯* R have "([(x, y)]  yvec') ♯* ([(x, y)]  R)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with x  R y  R have "([(x, y)]  yvec') ♯* R" by simp
      moreover note xvec' ♯* R length xvec' = n
      ultimately obtain T where "P = T  R" and A: "⦇ν*xvec'M ≺' T = ⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' ([(x, y)]  Q)"
        by(drule_tac Suc) auto

      from A have "⦇νx(⦇ν*xvec'M ≺' T) = ⦇νx(⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' ([(x, y)]  Q))"
        by(simp add: boundOutput.inject alpha)
      moreover from xFreshQR have "x  ⦇ν*yvec'N ≺' Q"
        by(force simp add: boundOutputFresh)
      ultimately show ?thesis using P = T  R xvec=x#xvec' yvec=y#yvec' xFreshQR
        by(force simp add: alphaBoundOutput name_swap eqvts)
    qed
  qed
  ultimately show ?thesis
    by blast
qed

lemma boundOutputPar1Dest':
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)"
  and     "xvec ♯* yvec"

  obtains T p where "set p  set xvec × set yvec" and "P = T  (p  R)" and "⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q"
proof -
  assume "p T. set p  set xvec × set yvec; P = T  (p  R); ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "p T. set p  set xvec × set yvec  P = T  (p  R)  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: boundOutput.inject)
  next
    case(Suc n xvec yvec M N P Q R)
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R) xvec = x # xvec'
    obtain y yvec' where "⦇ν*(x#xvec')M ≺' P = ⦇ν*(y#yvec')N ≺' (Q  R)"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence Eq: "⦇νx(⦇ν*xvec'M ≺' P) = ⦇νy(⦇ν*yvec'N ≺' (Q  R))"
      by simp
    from xvec = x#xvec' yvec=y#yvec' xvec ♯* yvec have "x  y" and "x  yvec'" and "y  xvec'" and "xvec' ♯* yvec'"
      by auto
    from Eq x  y have Eq': "⦇ν*xvec'M ≺' P = [(x, y)]  ⦇ν*yvec'N ≺' (Q  R)"
                     and xFreshQR: "x  ⦇ν*yvec'N ≺' (Q  R)"
      by(simp add: boundOutput.inject alpha)+
    have IH: "xvec yvec M N P Q R. ⦇ν*xvecM ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvecN ≺' (Q  R);  xvec ♯* yvec; n = length xvec  p T. set p  set xvec × set yvec  P = T  (p  R)  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' Q"
      by fact
    show ?case
    proof(case_tac "x  ⦇ν*xvec'M ≺' P")
      assume "x  ⦇ν*xvec'M ≺' P"
      with Eq have yFreshQR: "y  ⦇ν*yvec'N ≺' (Q  R)"
        by(rule boundOutputEqFresh)
      with Eq' xFreshQR have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'N ≺' (Q  R)"
        by simp
      with xvec' ♯* yvec' length xvec' = n
      obtain p T where S: "set p  set xvec' × set yvec'" and "P = T  (p  R)" and A: "⦇ν*xvec'M ≺' T = ⦇ν*yvec'N ≺' Q"
        by(drule_tac IH) auto
      from yFreshQR xFreshQR have yFreshQ: "y  ⦇ν*yvec'N ≺' Q" and xFreshQ: "x  ⦇ν*yvec'N ≺' Q" 
        by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
      hence "⦇νx(⦇ν*yvec'N ≺' Q) = ⦇νy(⦇ν*yvec'N ≺' Q)" by (subst alphaBoundOutput) simp+
      with A have "⦇νx(⦇ν*xvec'M ≺' T) = ⦇νy(⦇ν*yvec'N ≺' Q)" by simp
      with xvec=x#xvec' yvec=y#yvec' S P = T  (p  R) show ?case
        by auto
    next
      assume "¬(x  ⦇ν*xvec'M ≺' P)"
      hence "x  supp(⦇ν*xvec'M ≺' P)" by(simp add: fresh_def)
      with Eq have "y  supp(⦇ν*yvec'N ≺' (Q  R))"
        by(rule boundOutputEqSupp)
      hence "y  yvec'" by(simp add: BOresChainSupp fresh_def)
      with Eq' x  yvec' have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'([(x, y)]  N) ≺' (([(x, y)]  Q)  ([(x, y)]  R))"
        by(simp add: eqvts)
      moreover note xvec' ♯* yvec' length xvec' = n
      ultimately obtain p T where S: "set p  set xvec' × set yvec'" and "P = T  (p  [(x, y)]  R)" and A: "⦇ν*xvec'M ≺' T = ⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  Q)"
        by(drule_tac IH) auto

      from S have "set(p@[(x, y)])  set(x#xvec') × set(y#yvec')" by auto
      moreover from P = T  (p  [(x, y)]  R)  have "P = T  ((p @ [(x, y)])  R)"
        by(simp add: pt2[OF pt_name_inst])
      moreover from xFreshQR have xFreshQ: "x  ⦇ν*yvec'N ≺' Q" 
        by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
      with x  yvec' y  yvec' x  y have "y  ⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  Q)"
        by(simp add: fresh_left calc_atm)
      with x  yvec' y  yvec' have "⦇νx(⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  Q)) = ⦇νy(⦇ν*yvec'N ≺' Q)"
        by(subst alphaBoundOutput) (assumption | simp add: eqvts)+
      with  A have "⦇νx(⦇ν*xvec'M ≺' T) = ⦇νy(⦇ν*yvec'N ≺' Q)" by simp
      ultimately show ?thesis using xvec=x#xvec' yvec=y#yvec'
        by(rule_tac x="p@[(x, y)]" in exI) force
    qed
  qed
  ultimately show ?thesis
    by blast
qed

lemma boundOutputPar2Dest:
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)"
  and     "xvec ♯* Q"
  and     "yvec ♯* Q"

  obtains T where "P = Q  T" and "⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R"
proof -
  assume "T. P = Q  T; ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "T. P = Q  T  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: boundOutput.inject)
  next
    case(Suc n xvec yvec M N P Q R)
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R) xvec = x # xvec'
    obtain y yvec' where "⦇ν*(x#xvec')M ≺' P = ⦇ν*(y#yvec')N ≺' (Q  R)"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence EQ: "⦇νx(⦇ν*xvec'M ≺' P) = ⦇νy(⦇ν*yvec'N ≺' (Q  R))"
      by simp
    from xvec ♯* Q yvec ♯* Q xvec = x#xvec' yvec = y#yvec'
    have "x  Q" and "xvec' ♯* Q" and "y  Q" and "yvec' ♯* Q" by auto
    have IH: "xvec yvec M N P Q R. ⦇ν*xvecM ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvecN ≺' (Q  R); xvec ♯* Q; yvec ♯* Q; n = length xvec  T. P = Q  T  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R"
      by fact
    show ?case
    proof(case_tac "x = y")
      assume "x = y"
      with EQ have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'N ≺' (Q  R)"
        by(simp add: boundOutput.inject alpha)
      with xvec' ♯* Q yvec' ♯* Q length xvec' = n
      obtain T where "P = Q  T" and "⦇ν*xvec'M ≺' T = ⦇ν*yvec'N ≺' R"
        by(drule_tac IH) auto
      with xvec=x#xvec' yvec=y#yvec' x=y show ?case
        by(force simp add: boundOutput.inject alpha)
    next
      assume "x  y"
      with EQ x  Q y  Q
      have "⦇ν*xvec'M ≺' P = ⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' (Q  ([(x, y)]  R))"
       and xFreshQR: "x  ⦇ν*yvec'N ≺' (Q  R)"
        by(simp add: boundOutput.inject alpha eqvts)+
      moreover from yvec' ♯* Q have "([(x, y)]  yvec') ♯* ([(x, y)]  Q)"
        by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
      with x  Q y  Q have "([(x, y)]  yvec') ♯* Q" by simp
      moreover note xvec' ♯* Q length xvec' = n
      ultimately obtain T where "P = Q  T" and A: "⦇ν*xvec'M ≺' T = ⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' ([(x, y)]  R)"
        by(drule_tac IH) auto

      from A have "⦇νx(⦇ν*xvec'M ≺' T) = ⦇νx(⦇ν*([(x, y)]  yvec')([(x, y)]  N) ≺' ([(x, y)]  R))"
        by(simp add: boundOutput.inject alpha)
      moreover from xFreshQR have "x  ⦇ν*yvec'N ≺' R"
        by(force simp add: boundOutputFresh)
      ultimately show ?thesis using P = Q  T xvec=x#xvec' yvec=y#yvec' xFreshQR
        by(force simp add: alphaBoundOutput name_swap eqvts)
    qed
  qed
  ultimately show ?thesis
    by blast
qed

lemma boundOutputPar2Dest':
  fixes xvec :: "name list"
  and   M    :: "'a::fs_name"
  and   P    :: "('a, 'b::fs_name, 'c::fs_name) psi"
  and   yvec :: "name list"
  and   N    :: 'a
  and   Q    :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)"
  and     "xvec ♯* yvec"

  obtains T p where "set p  set xvec × set yvec" and "P = (p  Q)  T" and "⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R"
proof -
  assume "p T. set p  set xvec × set yvec; P = (p  Q)  T; ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R  thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "p T. set p  set xvec × set yvec  P = (p  Q)  T  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R)" by fact
    from 0 = length xvec have "xvec = []" by auto
    moreover with Eq have "yvec = []"
      by(case_tac yvec) auto
    ultimately show ?case using Eq
      by(simp add: boundOutput.inject)
  next
    case(Suc n xvec yvec M N P Q R)
    from Suc n = length xvec
    obtain x xvec' where "xvec = x#xvec'" and "length xvec' = n"
      by(case_tac xvec) auto
    from ⦇ν*xvecM ≺' P = ⦇ν*yvecN ≺' (Q  R) xvec = x # xvec'
    obtain y yvec' where "⦇ν*(x#xvec')M ≺' P = ⦇ν*(y#yvec')N ≺' (Q  R)"
      and "yvec = y#yvec'"
      by(case_tac yvec) auto
    hence Eq: "⦇νx(⦇ν*xvec'M ≺' P) = ⦇νy(⦇ν*yvec'N ≺' (Q  R))"
      by simp
    from xvec = x#xvec' yvec=y#yvec' xvec ♯* yvec have "x  y" and "x  yvec'" and "y  xvec'" and "xvec' ♯* yvec'"
      by auto
    from Eq x  y have Eq': "⦇ν*xvec'M ≺' P = [(x, y)]  ⦇ν*yvec'N ≺' (Q  R)"
                     and xFreshQR: "x  ⦇ν*yvec'N ≺' (Q  R)"
      by(simp add: boundOutput.inject alpha)+
    have IH: "xvec yvec M N P Q R. ⦇ν*xvecM ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvecN ≺' (Q  R);  xvec ♯* yvec; n = length xvec  p T. set p  set xvec × set yvec  P = (p  Q)  T  ⦇ν*xvecM ≺' T = ⦇ν*yvecN ≺' R"
      by fact
    show ?case
    proof(case_tac "x  ⦇ν*xvec'M ≺' P")
      assume "x  ⦇ν*xvec'M ≺' P"
      with Eq have yFreshQR: "y  ⦇ν*yvec'N ≺' (Q  R)"
        by(rule boundOutputEqFresh)
      with Eq' xFreshQR have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'N ≺' (Q  R)"
        by simp
      with xvec' ♯* yvec' length xvec' = n
      obtain p T where S: "set p  set xvec' × set yvec'" and "P = (p  Q)  T" and A: "⦇ν*xvec'M ≺' T = ⦇ν*yvec'N ≺' R"
        by(drule_tac IH) auto
      from yFreshQR xFreshQR have yFreshR: "y  ⦇ν*yvec'N ≺' R" and xFreshQ: "x  ⦇ν*yvec'N ≺' R" 
        by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
      hence "⦇νx(⦇ν*yvec'N ≺' R) = ⦇νy(⦇ν*yvec'N ≺' R)" by (subst alphaBoundOutput) simp+
      with A have "⦇νx(⦇ν*xvec'M ≺' T) = ⦇νy(⦇ν*yvec'N ≺' R)" by simp
      with xvec=x#xvec' yvec=y#yvec' S P = (p  Q)  T show ?case
        by auto
    next
      assume "¬(x  ⦇ν*xvec'M ≺' P)"
      hence "x  supp(⦇ν*xvec'M ≺' P)" by(simp add: fresh_def)
      with Eq have "y  supp(⦇ν*yvec'N ≺' (Q  R))"
        by(rule boundOutputEqSupp)
      hence "y  yvec'" by(simp add: BOresChainSupp fresh_def)
      with Eq' x  yvec' have "⦇ν*xvec'M ≺' P = ⦇ν*yvec'([(x, y)]  N) ≺' (([(x, y)]  Q)  ([(x, y)]  R))"
        by(simp add: eqvts)
      moreover note xvec' ♯* yvec' length xvec' = n
      ultimately obtain p T where S: "set p  set xvec' × set yvec'" and "P = (p  [(x, y)]  Q)  T" and A: "⦇ν*xvec'M ≺' T = ⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  R)"
        by(drule_tac IH) auto

      from S have "set(p@[(x, y)])  set(x#xvec') × set(y#yvec')" by auto
      moreover from P = (p  [(x, y)]  Q)  T  have "P = ((p @ [(x, y)])  Q)  T"
        by(simp add: pt2[OF pt_name_inst])
      moreover from xFreshQR have xFreshR: "x  ⦇ν*yvec'N ≺' R" 
        by(force simp add: BOresChainSupp fresh_def boundOutput.supp psi.supp)+
      with x  yvec' y  yvec' x  y have "y  ⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  R)"
        by(simp add: fresh_left calc_atm)
      with x  yvec' y  yvec' have "⦇νx(⦇ν*yvec'([(x, y)]  N) ≺' ([(x, y)]  R)) = ⦇νy(⦇ν*yvec'N ≺' R)"
        by(subst alphaBoundOutput) (assumption | simp add: eqvts)+
      with  A have "⦇νx(⦇ν*xvec'M ≺' T) = ⦇νy(⦇ν*yvec'N ≺' R)" by simp
      ultimately show ?thesis using xvec=x#xvec' yvec=y#yvec'
        by(rule_tac x="p@[(x, y)]" in exI) force
    qed
  qed
  ultimately show ?thesis
    by blast
qed

lemma boundOutputApp:
  fixes xvec :: "name list"
  and   yvec :: "name list"
  and   B    :: "('a::fs_name, 'b::fs_name, 'c::fs_name) boundOutput"

  shows "⦇ν*(xvec@yvec)B = ⦇ν*xvec(⦇ν*yvecB)"
by(induct xvec) auto
  
lemma openInjectAuxAuxAux:
  fixes x    :: name
  and   xvec :: "name list"

  shows "y yvec. x # xvec = yvec @ [y]  length xvec = length yvec"
apply(induct xvec arbitrary: x)
apply auto
apply(subgoal_tac "y yvec. a # xvec = yvec @ [y]  length xvec = length yvec")
apply(clarify)
apply(rule_tac x=y in exI)
by auto

lemma openInjectAuxAux:
  fixes xvec1 :: "name list"
  and   xvec2 :: "name list"
  and   yvec  :: "name list"

  assumes "length(xvec1@xvec2) = length yvec"

  shows "yvec1 yvec2. yvec = yvec1@yvec2  length xvec1 = length yvec1  length xvec2 = length yvec2"
using assms
apply(induct yvec