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 "⦇ν*xvec⦈B ≡ 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 ∙ (⦇ν*xvec⦈B) = ⦇ν*(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 "(⦇ν*xvec⦈N ≺' P = N' ≺' P') = (xvec = [] ∧ N = N' ∧ P = P')"
  and   "(N' ≺' P' = ⦇ν*xvec⦈N ≺' P) = (xvec = [] ∧ N = N' ∧ P = P')"
  and   "(N' ≺' P' = N ≺' P) = (N = N' ∧ P = P')"
  and   "(⦇ν*xvec⦈B = ⦇ν*xvec⦈B') = (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 ♯ (⦇ν*xvec⦈B)) = (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 ♯* (⦇ν*xvec⦈B) = (∀x∈Xs. x ∈ set xvec ∨ x ♯ B)"
  and   "yvec ♯* (⦇ν*xvec⦈B) = (∀x∈(set yvec). x ∈ set xvec ∨ x ♯ B)"
  and   "Xs ♯* (⦇νx⦈B) = Xs ♯* [x].B"
  and   "xvec ♯* (⦇νx⦈B) = 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(⦇ν*xvec⦈B)::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 ♯* (⦇ν*xvec⦈B)) = (Xs ♯* B)"
  and   "yvec ♯* xvec ⟹ yvec ♯* (⦇ν*xvec⦈B) = yvec ♯* B"
  and   "xvec ♯* (⦇ν*xvec⦈B)"
  and   "x ♯ xvec ⟹ x ♯ ⦇ν*xvec⦈B = 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 "(⦇ν*yvec⦈B) = (⦇ν*(p ∙ yvec)⦈(p ∙ B))"
proof -
  note pt_name_inst at_name_inst S
  moreover from ‹(set xvec) ⊆ (set yvec)› have "set xvec ♯* (⦇ν*yvec⦈B)"
    by(force simp add: boundOutputFreshSet)
  moreover from xvecFreshB ‹(set xvec) ⊆ (set yvec)› have "set (p ∙ xvec) ♯* (⦇ν*yvec⦈B)"
    by (simp add: boundOutputFreshSet) (simp add: fresh_star_def)
  ultimately have "(⦇ν*yvec⦈B) = p ∙ (⦇ν*yvec⦈B)"
    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 ♯* (⦇ν*zvec⦈B)"

  shows "(⦇ν*zvec⦈B) = (⦇ν*(p ∙ zvec)⦈(p ∙ B))"
proof -
  note pt_name_inst at_name_inst S ‹yvec ♯* (⦇ν*zvec⦈B)›
  moreover from xvecFreshB have "set (xvec) ♯* (⦇ν*zvec⦈B)"
    by (simp add: boundOutputFreshSet) (simp add: fresh_star_def)
  ultimately have "(⦇ν*zvec⦈B) = p ∙ (⦇ν*zvec⦈B)"
    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 "(⦇ν*yvec⦈M ≺' 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 "⦇ν*xvec⦈N ≺' 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 "⦇νx⦈B = ⦇ν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 "⦇νx⦈B = ⦇νy⦈C"
  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 "⦇νx⦈B = ⦇νy⦈C"
  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 "⦇ν*xvec⦈B = ⦇ν*yvec⦈B'"
  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: "⦇ν*xvec⦈B = ⦇ν*yvec⦈B'" 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 ‹⦇ν*xvec⦈B = ⦇ν*yvec⦈B'› ‹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) = ⦇ν*yvec⦈B'; 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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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. ⟦⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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: "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' 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) = ⦇ν*yvec⦈N ≺' 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⦈(⦇ν*xvec⦈M ≺' P) = ⦇νy⦈(⦇ν*yvec⦈N ≺' 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 "⦇ν*xvec⦈M ≺' 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⦈(⦇νx⦈B) = ⦇ν*yvec⦈(⦇νy⦈B')"
  and     L: "length xvec = length yvec"
  and     xFreshB': "x ♯ B'"
  and     xFreshxvec: "x ♯ xvec"
  and     xFreshyvec: "x ♯ yvec"

  shows "⦇ν*xvec⦈B = ⦇ν*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⦈⦇νx⦈B = ⦇ν*yvec⦈⦇νy⦈B'" 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⦈⦇νx⦈B = ⦇ν*yvec⦈⦇νy⦈B'" by fact
  with xEq yEq have Eq: "⦇νx'⦈(⦇ν*xvec'⦈⦇νx⦈B) = ⦇νy'⦈(⦇ν*yvec'⦈⦇νy⦈B')" 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'⦈⦇νx⦈B = ⦇ν*yvec'⦈⦇νy⦈B'" 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'⦈⦇νx⦈B = ⦇ν*([(x', y')] ∙ yvec')⦈⦇ν([(x', y')] ∙ y)⦈([(x', y')] ∙ B')"
             and x'FreshB': "x' ♯ ⦇ν*yvec'⦈⦇νy⦈B'"
      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' ♯ ⦇νy⦈B'"
        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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (Q ∥ R)"
  and     "xvec ♯* R"
  and     "yvec ♯* R"

  obtains T where "P = T ∥ R" and "⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' Q"
proof -
  assume "⋀T. ⟦P = T ∥ R; ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' Q⟧ ⟹ thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "∃T. P = T ∥ R ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' Q"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (Q ∥ R)"
  and     "xvec ♯* yvec"

  obtains T p where "set p ⊆ set xvec × set yvec" and "P = T ∥ (p ∙ R)" and "⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' Q"
proof -
  assume "⋀p T. ⟦set p ⊆ set xvec × set yvec; P = T ∥ (p ∙ R); ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' 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) ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' Q"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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. ⟦⦇ν*xvec⦈M ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvec⦈N ≺' (Q ∥ R);  xvec ♯* yvec; n = length xvec⟧ ⟹ ∃p T. set p ⊆ set xvec × set yvec ∧ P = T ∥ (p ∙ R) ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' 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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (Q ∥ R)"
  and     "xvec ♯* Q"
  and     "yvec ♯* Q"

  obtains T where "P = Q ∥ T" and "⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' R"
proof -
  assume "⋀T. ⟦P = Q ∥ T; ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' R⟧ ⟹ thesis"
  moreover obtain n where "n = length xvec" by auto
  with assms have "∃T. P = Q ∥ T ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' R"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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. ⟦⦇ν*xvec⦈M ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvec⦈N ≺' (Q ∥ R); xvec ♯* Q; yvec ♯* Q; n = length xvec⟧ ⟹ ∃T. P = Q ∥ T ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' 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 "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (Q ∥ R)"
  and     "xvec ♯* yvec"

  obtains T p where "set p ⊆ set xvec × set yvec" and "P = (p ∙ Q) ∥ T" and "⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' R"
proof -
  assume "⋀p T. ⟦set p ⊆ set xvec × set yvec; P = (p ∙ Q) ∥ T; ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' 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 ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' R"
  proof(induct n arbitrary: xvec yvec M N P Q R)
    case(0 xvec yvec M N P Q R)
    have Eq: "⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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 ‹⦇ν*xvec⦈M ≺' P = ⦇ν*yvec⦈N ≺' (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. ⟦⦇ν*xvec⦈M ≺' (P::('a, 'b, 'c) psi) = ⦇ν*yvec⦈N ≺' (Q ∥ R);  xvec ♯* yvec; n = length xvec⟧ ⟹ ∃p T. set p ⊆ set xvec × set yvec ∧ P = (p ∙ Q) ∥ T ∧ ⦇ν*xvec⦈M ≺' T = ⦇ν*yvec⦈N ≺' 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⦈(⦇ν*yvec⦈B)"
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