Theory Early_Semantics

(* 
   Title: The pi-calculus   
   Author/Maintainer: Jesper Bengtson (jebe.dk), 2012
*)
theory Early_Semantics
  imports Agent
begin

declare name_fresh[simp del]

nominal_datatype freeRes = InputR name name              (‹_<_>› [110, 110] 110)
                         | OutputR name name             (‹_[_]› [110, 110] 110)
                         | TauR                          (‹τ› 110)

nominal_datatype residual = BoundOutputR name "«name» pi" (‹_<ν_> ≺ _› [110, 110, 110] 110)
                          | FreeR freeRes pi

lemma alphaBoundOutput:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   x' :: name

  assumes A1: "x' ♯ P"

  shows "a<νx> ≺ P = a<νx'> ≺ ([(x, x')] ∙ P)"
proof(cases "x=x'")
  assume "x=x'"
  thus ?thesis by simp
next
  assume "x ≠ x'"
  with A1 show ?thesis
    by(simp add: residual.inject alpha name_fresh_left name_calc)
qed

declare name_fresh[simp]

abbreviation Transitions_Freejudge (‹_ ≺ _› [80, 80] 80) where "α ≺ P' ≡ (FreeR α P')"

inductive "TransitionsEarly" :: "pi ⇒ residual ⇒ bool" (‹_ ⟼ _› [80, 80] 80)
where
  Tau:               "τ.(P) ⟼ τ ≺ P"
| Input:             "⟦x ≠ a; x ≠ u⟧ ⟹ a<x>.P ⟼ a<u> ≺ (P[x::=u])"
| Output:            "a{b}.P ⟼ a[b] ≺  P"

| Match:             "⟦P ⟼ V⟧ ⟹ [b⌢b]P ⟼ V"
| Mismatch:          "⟦P ⟼ V; a ≠ b⟧ ⟹ [a≠b]P ⟼ V"

| Open:              "⟦P ⟼ a[b] ≺ P'; a ≠ b⟧ ⟹ <νb>P ⟼ a<νb> ≺ P'"
| Sum1:              "⟦P ⟼ V⟧ ⟹ (P ⊕ Q) ⟼ V"
| Sum2:              "⟦Q ⟼ V⟧ ⟹ (P ⊕ Q) ⟼ V"

| Par1B:             "⟦P ⟼ a<νx> ≺ P'; x ♯ P; x ♯ Q; x ≠ a⟧ ⟹ P ∥ Q ⟼ a<νx> ≺ (P' ∥ Q)"
| Par1F:             "⟦P ⟼ α ≺ P'⟧ ⟹ P ∥ Q ⟼ α ≺ (P' ∥ Q)"
| Par2B:             "⟦Q ⟼ a<νx> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a⟧ ⟹ P ∥ Q ⟼ a<νx> ≺ (P ∥ Q')"
| Par2F:             "⟦Q ⟼ α ≺ Q'⟧ ⟹ P ∥ Q ⟼ α ≺ (P ∥ Q')"

| Comm1:             "⟦P ⟼ a<b> ≺ P'; Q ⟼ a[b] ≺ Q'⟧ ⟹ P ∥ Q ⟼ τ ≺ P' ∥ Q'"
| Comm2:             "⟦P ⟼ a[b] ≺ P'; Q ⟼ a<b> ≺ Q'⟧ ⟹ P ∥ Q ⟼ τ ≺ P' ∥ Q'"
| Close1:            "⟦P ⟼ a<x> ≺ P'; Q ⟼ a<νx> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a⟧ ⟹ P ∥ Q ⟼ τ ≺ <νx>(P' ∥ Q')"
| Close2:            "⟦P ⟼ a<νx> ≺ P'; Q ⟼ a<x> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a⟧ ⟹ P ∥ Q ⟼ τ ≺ <νx>(P' ∥ Q')"

| ResB:              "⟦P ⟼ a<νx> ≺ P'; y ≠ a; y ≠ x; x ♯ P; x ≠ a⟧ ⟹ <νy>P ⟼ a<νx> ≺ (<νy>P')"
| ResF:              "⟦P ⟼ α ≺ P'; y ♯ α⟧ ⟹ <νy>P ⟼ α ≺ <νy>P'"

| Bang:              "⟦P ∥ !P ⟼ V⟧ ⟹ !P ⟼ V"

equivariance TransitionsEarly
nominal_inductive TransitionsEarly
by(auto simp add: abs_fresh fresh_fact2)

lemmas [simp] = freeRes.inject

lemma freshOutputAction:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P ⟼ a[b] ≺ P'"
  and     "c ♯ P"

  shows "c ≠ a" and "c ≠ b" and "c ♯ P'"
proof -
  from assms have "c ≠ a ∧ c ≠ b ∧ c ♯ P'"
    by(nominal_induct x2=="a[b] ≺ P'" arbitrary: P' rule: TransitionsEarly.strong_induct) (fastforce simp add: residual.inject abs_fresh freeRes.inject)+
  thus "c ≠ a" and "c ≠ b" and "c ♯ P'"
    by blast+
qed

lemma freshInputAction:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P ⟼ a<b> ≺ P'"
  and     "c ♯ P"

  shows "c ≠ a"
using assms
by(nominal_induct x2=="a<b> ≺ P'" arbitrary: P' rule: TransitionsEarly.strong_induct) (auto simp add: residual.inject abs_fresh)

lemma freshBoundOutputAction:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   c  :: name
  
  assumes "P ⟼ a<νx> ≺ P'"
  and     "c ♯ P"

  shows "c ≠ a"
using assms
by(nominal_induct x2=="a<νx> ≺ P'" avoiding: x arbitrary: P' rule: TransitionsEarly.strong_induct) (auto simp add: residual.inject abs_fresh fresh_left calc_atm dest: freshOutputAction)

lemmas freshAction = freshOutputAction freshInputAction freshBoundOutputAction

lemma freshInputTransition:
  fixes P  :: pi
  and   a  :: name
  and   u  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P ⟼ a<u> ≺ P'"
  and     "c ♯ P"
  and     "c ≠ u"

  shows "c ♯ P'"
using assms
by(nominal_induct x2=="a<u> ≺ P'" arbitrary: P' rule: TransitionsEarly.strong_induct)
  (fastforce simp add: residual.inject name_fresh_abs fresh_fact1 fresh_fact2)+
   
lemma freshBoundOutputTransition:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   c  :: name

  assumes "P ⟼ a<νx> ≺ P'"
  and     "c ♯ P"
  and     "c ≠ x"

  shows "c ♯ P'"
using assms
apply(nominal_induct x2=="a<νx> ≺ P'" avoiding: x arbitrary: P' rule: TransitionsEarly.strong_induct)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(force simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction | simp | auto simp add: abs_fresh residual.inject alpha' calc_atm)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(fastforce simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
apply(auto simp add: residual.inject name_fresh_abs alpha' fresh_left calc_atm dest: freshOutputAction)
done

lemma freshTauTransition:
  fixes P  :: pi
  and   P' :: pi
  and   c  :: name

  assumes "P ⟼ τ ≺ P'"
  and     "c ♯ P"

  shows "c ♯ P'"
using assms
apply(nominal_induct x2=="τ ≺ P'" arbitrary: P' rule: TransitionsEarly.strong_induct)
by(fastforce simp add: residual.inject abs_fresh dest: freshOutputAction freshInputTransition freshBoundOutputTransition)+

lemma freshFreeTransition:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   c  :: name

  assumes "P ⟼α ≺ P'"
  and     "c ♯ P"
  and     "c ♯ α"

  shows "c ♯ P'"
using assms
by(nominal_induct α rule: freeRes.strong_inducts)
  (auto dest: freshInputTransition freshOutputAction freshTauTransition)

lemmas freshTransition = freshInputTransition freshOutputAction freshFreeTransition
                         freshBoundOutputTransition freshTauTransition

lemma substTrans[simp]: "b ♯ P ⟹ ((P::pi)[a::=b])[b::=c] = P[a::=c]"
apply(simp add: injPermSubst[THEN sym])
apply(simp add: renaming)
by(simp add: pt_swap[OF pt_name_inst, OF at_name_inst])

lemma Input:
  fixes a :: name
  and   x :: name
  and   u :: name
  and   P :: pi

  shows "a<x>.P ⟼a<u> ≺ P[x::=u]"
proof -
  obtain y::name where "y ≠ a" and "y ≠ u" and "y ♯ P"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹y ≠ a› ‹y ≠ u› have "a<y>.([(x, y)] ∙ P) ⟼a<u> ≺ ([(x, y)] ∙ P)[y::=u]"
    by(rule Input)
  with ‹y ♯ P› show ?thesis by(simp add: alphaInput renaming name_swap) 
qed

lemma Par1B:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi

  assumes "P ⟼a<νx> ≺ P'"
  and     "x ♯ Q"

  shows "P ∥ Q ⟼ a<νx> ≺ (P' ∥ Q)"
proof -
  obtain y::name where "y ♯ P" and "y ♯ Q" and "y ≠ a" and "y ♯ P'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹P ⟼a<νx> ≺ P'› ‹y ♯ P'› have "P ⟼a<νy> ≺ ([(x, y)] ∙ P')"
    by(simp add: alphaBoundOutput)
  hence "P ∥ Q ⟼a<νy> ≺ (([(x, y)] ∙ P') ∥ Q)" using ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a›
    by(rule Par1B)
  with ‹x ♯ Q› ‹y ♯ Q› ‹y ♯ P'› show ?thesis
    by(subst alphaBoundOutput) (auto simp add: name_fresh_fresh)
qed

lemma Par2B:
  fixes Q  :: pi
  and   a  :: name
  and   x  :: name
  and   Q' :: pi
  and   P  :: pi

  assumes "Q ⟼a<νx> ≺ Q'"
  and     "x ♯ P"

  shows "P ∥ Q ⟼ a<νx> ≺ (P ∥ Q')"
proof -
  obtain y::name where "y ♯ P" and "y ♯ Q" and "y ≠ a" and "y ♯ Q'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹Q ⟼a<νx> ≺ Q'› ‹y ♯ Q'› have "Q ⟼a<νy> ≺ ([(x, y)] ∙ Q')"
    by(simp add: alphaBoundOutput)
  hence "P ∥ Q ⟼a<νy> ≺ (P ∥ ([(x, y)] ∙ Q'))" using ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a›
    by(rule Par2B)
  with ‹x ♯ P› ‹y ♯ P› ‹y ♯ Q'› show ?thesis
    by(subst alphaBoundOutput[of y]) (auto simp add: name_fresh_fresh)
qed

lemma inputInduct[consumes 1, case_names cInput cMatch cMismatch cSum1 cSum2 cPar1 cPar2 cRes cBang]:
  fixes P  :: pi
  and   a  :: name
  and   u  :: name
  and   P' :: pi
  and   F  :: "'a::fs_name ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P ⟼a<u> ≺ P'"
  and     "⋀a x P u C. ⟦x ♯ C; x ≠ u; x ≠ a⟧ ⟹ F C (a<x>.P) a u (P[x::=u])"
  and     "⋀P a u P' b C. ⟦P ⟼a<u> ≺ P'; ⋀C. F C P a u P'⟧ ⟹ F C ([b⌢b]P) a u P'"
  and     "⋀P a u P' b c C. ⟦P ⟼a<u> ≺ P'; ⋀C. F C P a u P'; b≠c⟧ ⟹ F C ([b≠c]P) a u P'"
  and     "⋀P a u P' Q C. ⟦P ⟼a<u> ≺ P'; ⋀C. F C P a u P'⟧ ⟹ F C (P ⊕ Q) a u P'"
  and     "⋀Q a u Q' P C. ⟦Q ⟼a<u> ≺ Q'; ⋀C. F C Q a u Q'⟧ ⟹ F C (P ⊕ Q) a u Q'"
  and     "⋀P a u P' Q C. ⟦P ⟼a<u> ≺ P'; ⋀C. F C P a u P'⟧ ⟹ F C (P ∥ Q) a u (P' ∥ Q)"
  and     "⋀Q a u Q' P C. ⟦Q ⟼a<u> ≺ Q'; ⋀C. F C Q a u Q'⟧ ⟹ F C (P ∥ Q) a u (P ∥ Q')"
  and     "⋀P a u P' x C. ⟦P ⟼a<u> ≺ P'; x ≠ a; x ≠ u; x ♯ C; ⋀C. F C P a u P'⟧ ⟹ F C (<νx>P) a u (<νx>P')"
  and     "⋀P a u P' C. ⟦P ∥ !P ⟼a<u> ≺ P'; ⋀C. F C (P ∥ !P) a u P'⟧ ⟹ F C (!P) a u P'"

  shows "F C P a u P'"
using assms
by(nominal_induct x2=="a<u> ≺ P'" avoiding: C arbitrary: P' rule: TransitionsEarly.strong_induct)
  (auto simp add: residual.inject)

lemma inputAlpha:
  assumes "P ⟼a<u> ≺ P'"
  and     "u ♯ P"
  and     "r ♯ P'"

  shows "P ⟼a<r> ≺ ([(u, r)] ∙ P')"
using assms
proof(nominal_induct avoiding: r rule: inputInduct)
  case(cInput a x P u r)
  from ‹x ≠ u› ‹u ♯ a<x>.P›have "u ≠ a" and "u ♯ P" by(simp add: abs_fresh)+
  have "a<x>.P ⟼a<r> ≺ P[x::=r]"
    by(rule Input)
  thus ?case using ‹r ♯ P[x::=u]› ‹u ♯ P›
    by(simp add: injPermSubst substTrans)
next
  case(cMatch P a u P' b r)
  thus ?case by(force intro: Match) 
next
  case(cMismatch P a u P' b c r)
  thus ?case by(force intro: Mismatch)
next
  case(cSum1 P a u P' Q r)
  thus ?case by(force intro: Sum1)
next
  case(cSum2 Q a u Q' P r)
  thus ?case by(force intro: Sum2)
next
  case(cPar1 P a u P' Q r)
  thus ?case by(force intro: Par1F simp add: eqvts name_fresh_fresh) 
next
  case(cPar2 Q a u Q' P r)
  thus ?case by(force intro: Par2F simp add: eqvts name_fresh_fresh) 
next
  case(cRes P a u P' x r)
  thus ?case by(force intro: ResF simp add: eqvts calc_atm abs_fresh) 
next
  case(cBang P a u P' R)
  thus ?case by(force intro: Bang)
qed

lemma Close1:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "P ⟼a<x> ≺ P'"
  and     "Q ⟼a<νx> ≺ Q'"
  and     "x ♯ P"

  shows "P ∥ Q ⟼τ ≺ <νx>(P' ∥ Q')"
proof -
  obtain y::name where "y ♯ P" and "y ♯ Q" and "y ≠ a" and "y ♯ Q'" and "y ♯ P'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹P ⟼a<x> ≺ P'› ‹x ♯ P› ‹y ♯ P'› have "P ⟼a<y> ≺ ([(x, y)] ∙ P')"
    by(rule inputAlpha)
  moreover from ‹Q ⟼a<νx> ≺ Q'› ‹y ♯ Q'› have "Q ⟼a<νy> ≺ ([(x, y)] ∙ Q')"
    by(simp add: alphaBoundOutput)
  
  ultimately have "P ∥ Q ⟼τ ≺ <νy>(([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q'))" using ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a›
    by(rule Close1)
  with ‹y ♯ P'› ‹y ♯ Q'› show ?thesis by(subst alphaRes) (auto simp add: name_fresh_fresh)
qed

lemma Close2:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   Q  :: pi
  and   Q' :: pi

  assumes "P ⟼a<νx> ≺ P'"
  and     "Q ⟼a<x> ≺ Q'"
  and     "x ♯ Q"

  shows "P ∥ Q ⟼τ ≺ <νx>(P' ∥ Q')"
proof -
  obtain y::name where "y ♯ P" and "y ♯ Q" and "y ≠ a" and "y ♯ Q'" and "y ♯ P'"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹P ⟼a<νx> ≺ P'› ‹y ♯ P'› have "P ⟼a<νy> ≺ ([(x, y)] ∙ P')"
    by(simp add: alphaBoundOutput)
  moreover from ‹Q ⟼a<x> ≺ Q'› ‹x ♯ Q› ‹y ♯ Q'› have "Q ⟼a<y> ≺ ([(x, y)] ∙ Q')"
    by(rule inputAlpha)
  
  ultimately have "P ∥ Q ⟼τ ≺ <νy>(([(x, y)] ∙ P') ∥ ([(x, y)] ∙ Q'))" using ‹y ♯ P› ‹y ♯ Q› ‹y ≠ a›
    by(rule Close2)
  with ‹y ♯ P'› ‹y ♯ Q'› show ?thesis by(subst alphaRes) (auto simp add: name_fresh_fresh)
qed

lemma ResB:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   y  :: name

  assumes "P ⟼a<νx> ≺ P'"
  and     "y ≠ a"
  and     "y ≠ x"

  shows "<νy>P ⟼a<νx> ≺ (<νy>P')"
proof -
  obtain z :: name where "z ♯ P" and "z ♯ P'" and "z ≠ a" and "z ≠ y"
    by(generate_fresh "name") (auto simp add: fresh_prod)
  from ‹P ⟼a<νx> ≺ P'› ‹z ♯ P'› have "P ⟼a<νz> ≺ ([(x, z)] ∙ P')"
    by(simp add: alphaBoundOutput)
  hence "<νy>P ⟼a<νz> ≺ (<νy>([(x, z)] ∙ P'))" using ‹y ≠ a› ‹z ≠ y› ‹z ♯ P› ‹z ≠ a›
    by(rule_tac ResB) auto
  thus ?thesis using ‹z ≠ y› ‹y ≠ x› ‹z ♯ P'›
    by(subst alphaBoundOutput[where x'=z]) (auto simp add: eqvts calc_atm abs_fresh)
qed

lemma outputInduct[consumes 1, case_names Output Match Mismatch Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi
  and   F  :: "'a::fs_name ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P ⟼a[b] ≺ P'"
  and     "⋀a b P C. F C (a{b}.P) a b P"
  and     "⋀P a b P' c C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'⟧ ⟹ F C ([c⌢c]P) a b P'"
  and     "⋀P a b P' c d C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'; c≠d⟧ ⟹ F C ([c≠d]P) a b P'"
  and     "⋀P a b P' Q C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'⟧ ⟹ F C (P ⊕ Q) a b P'"
  and     "⋀Q a b Q' P C. ⟦Q ⟼OutputR a b ≺ Q'; ⋀C. F C Q a b Q'⟧ ⟹ F C (P ⊕ Q) a b Q'"
  and     "⋀P a b P' Q C. ⟦P ⟼OutputR a b ≺ P'; ⋀C. F C P a b P'⟧ ⟹ F C (P ∥ Q) a b (P' ∥ Q)"
  and     "⋀Q a b Q' P C. ⟦Q ⟼OutputR a b ≺ Q'; ⋀C. F C Q a b Q'⟧ ⟹ F C (P ∥ Q) a b (P ∥ Q')"
  and     "⋀P a b P' x C. ⟦P ⟼OutputR a b ≺ P'; x ≠ a; x ≠ b; x ♯ C; ⋀C. F C P a b P'⟧ ⟹
                            F C (<νx>P) a b (<νx>P')"
  and     "⋀P a b P' C. ⟦P ∥ !P ⟼OutputR a b ≺ P'; ⋀C. F C (P ∥ !P) a b P'⟧ ⟹ F C (!P) a b P'"

  shows "F C P a b P'"
using assms
by(nominal_induct x2=="a[b] ≺ P'" avoiding: C arbitrary: P' rule: TransitionsEarly.strong_induct)
  (auto simp add: residual.inject)

lemma boundOutputInduct[consumes 2, case_names Match Mismatch Open Sum1 Sum2 Par1 Par2 Res Bang]:
  fixes P  :: pi
  and   a  :: name
  and   x  :: name
  and   P' :: pi
  and   F  :: "('a::fs_name) ⇒ pi ⇒ name ⇒ name ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes a: "P ⟼a<νx> ≺ P'"
  and     xFreshP:  "x ♯ P"
  and     cMatch:   "⋀P a x P' b C. ⟦P ⟼a<νx> ≺ P'; ⋀C. F C P a x P'⟧ ⟹ F C ([b⌢b]P) a x P'"
  and     cMismatch:   "⋀P a x P' b c C. ⟦P ⟼a<νx> ≺ P'; ⋀C. F C P a x P'; b ≠ c⟧ ⟹ F C ([b≠c]P) a x P'"
  and     cOpen:    "⋀P a x P' C.   ⟦P ⟼(OutputR a x) ≺ P'; a ≠ x⟧ ⟹ F C (<νx>P) a x P'"
  and     cSum1:    "⋀P Q a x P' C. ⟦P ⟼a<νx> ≺ P'; ⋀C. F C P a x P'⟧ ⟹ F C (P ⊕ Q) a x P'" 
  and     cSum2:    "⋀P Q a x Q' C. ⟦Q ⟼a<νx> ≺ Q'; ⋀C. F C Q a x Q'⟧ ⟹ F C (P ⊕ Q) a x Q'" 
  and     cPar1B:   "⋀P P' Q a x C. ⟦P ⟼a<νx> ≺ P'; x ♯ Q; ⋀C. F C P a x P'⟧ ⟹
                                  F C (P ∥ Q) a x (P' ∥ Q)" 
  and     cPar2B:   "⋀P Q Q' a x C. ⟦Q ⟼a<νx> ≺ Q'; x ♯ P; ⋀C. F C Q a x Q'⟧ ⟹
                                  F C (P ∥ Q) a x (P ∥ Q')"
  and     cResB:    "⋀P P' a x y C. ⟦P ⟼a<νx> ≺ P'; y ≠ a; y ≠ x; y ♯ C;
                                      ⋀C. F C P a x P'⟧ ⟹ F C (<νy>P) a x (<νy>P')"
  and     cBang:    "⋀P a x P' C. ⟦P ∥ !P ⟼a<νx> ≺ P'; ⋀C. F C (P ∥ !P) a x P'⟧ ⟹
                                    F C (!P) a x P'"
  shows "F C P a x P'"
using assms
proof -
  have Goal: "⋀P Rs a x P' C. ⟦P ⟼ Rs; Rs = a<νx> ≺ P'; x ♯ P⟧ ⟹ F C P a x P'"
  proof -
    fix P Rs a x P' C
    assume "P ⟼ Rs" and "Rs = a<νx> ≺ P'" and "x ♯ P"
    thus "F C P a x P'"
    proof(nominal_induct avoiding: C a x P' rule: TransitionsEarly.strong_induct)
      case(Tau P)
      thus ?case by(simp add: residual.inject)
    next
      case(Input P a x)
      thus ?case by(simp add: residual.inject)
    next
      case(Output P a b)
      thus ?case by(simp add: residual.inject)
    next
      case(Match P Rs b C a x P')
      thus ?case 
        by(force intro: cMatch simp add: residual.inject) 
    next
      case(Mismatch P Rs b c C a x P')
      thus ?case 
        by(force intro: cMismatch simp add: residual.inject) 
    next
      case(Sum1 P Q Rs C)
      thus ?case by(force intro: cSum1)
    next
      case(Sum2 P Q Rs C)
      thus ?case by(force intro: cSum2)
    next
      case(Open P a b P' C a' x P'')
      have "b ♯ x" by fact hence bineqx: "b ≠ x" by simp
      moreover have "a<νb> ≺ P' = a'<νx> ≺ P''" by fact
      ultimately have aeqa': "a=a'" and P'eqP'': "P'' = [(b, x)] ∙ P'"
        by(simp add: residual.inject name_abs_eq)+
      have "x ♯ <νb>P" by fact 
      with bineqx have xFreshP: "x ♯ P" by(simp add: name_fresh_abs)
      have aineqb: "a ≠ b" by fact

      have PTrans: "P ⟼a[b] ≺ P'" by fact
      with xFreshP have xineqa: "x ≠ a" by(force dest: freshAction)
      from PTrans have "([(b, x)] ∙ P) ⟼[(b, x)] ∙ (a[b] ≺ P')" by(rule TransitionsEarly.eqvt)
      with P'eqP'' xineqa aineqb have Trans: "([(b, x)] ∙ P) ⟼a[x] ≺ P''"
        by(auto simp add: name_calc)
      hence "F C (<νx>([(b, x)] ∙ P)) a x P''" using xineqa by(blast intro: cOpen)
      with xFreshP aeqa' show ?case by(simp add: alphaRes)
    next
      case(Par1B P  a x P' Q C a' x' P'')
      have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
      moreover have Eq: "a<νx> ≺ (P' ∥ Q) = a'<νx'> ≺ P''" by fact
      hence aeqa': "a = a'" by(simp add: residual.inject)
      have xFreshQ: "x ♯ Q" by fact
      have "x' ♯ P ∥ Q" by fact
      hence x'FreshP: "x' ♯ P" and x'FreshQ: "x' ♯ Q" by simp+
      have P''eq: "P'' = ([(x, x')] ∙ P') ∥ Q"
      proof -
        from Eq xineqx' have "(P' ∥ Q) = [(x, x')] ∙ P''"
          by(simp add: residual.inject name_abs_eq)
        hence "([(x, x')] ∙ (P' ∥ Q)) = P''" by simp
        with x'FreshQ xFreshQ show ?thesis by(simp add: name_fresh_fresh)
      qed

      have "x ♯ P''" by fact
      with P''eq have x'FreshP': "x' ♯ P'" by(simp add: name_fresh_left name_calc)

      have "P ⟼a<νx> ≺ P'" by fact
      with x'FreshP' aeqa' have "P ⟼a'<νx'> ≺ ([(x, x')] ∙ P')"
        by(simp add: alphaBoundOutput)
      moreover have "⋀C. F C P a x' ([(x, x')] ∙ P')"
      proof -
        fix C
        have "⋀C a' x' P''. ⟦a<νx> ≺ P' = a'<νx'> ≺ P''; x' ♯ P⟧ ⟹ F C P a' x' P''" by fact
        moreover with aeqa' xineqx' x'FreshP' have "a<νx> ≺ P' = a'<νx'> ≺ ([(x, x')] ∙ P')"
          by(simp add: residual.inject name_abs_eq name_fresh_left name_calc)
        ultimately show "F C P a x' ([(x, x')] ∙ P')" using x'FreshP aeqa' by blast 
      qed
      ultimately have "F C (P ∥ Q) a' x' (([(x, x')] ∙ P') ∥ Q)" using x'FreshQ aeqa'
        by(blast intro: cPar1B)
      with P''eq show ?case by simp
    next
      case(Par1F P P' Q α)
      thus ?case by(simp add: residual.inject)
    next
      case(Par2B Q a x Q' P C a' x' Q'')
      have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
      moreover have Eq: "a<νx> ≺ (P ∥ Q') = a'<νx'> ≺ Q''" by fact
      hence aeqa': "a = a'" by(simp add: residual.inject)
      have xFreshP: "x ♯ P" by fact
      have "x' ♯ P ∥ Q" by fact
      hence x'FreshP: "x' ♯ P" and x'FreshQ: "x' ♯ Q" by simp+
      have Q''eq: "Q'' = P ∥ ([(x, x')] ∙ Q')"
      proof -
        from Eq xineqx' have "(P ∥ Q') = [(x, x')] ∙ Q''"
          by(simp add: residual.inject name_abs_eq)
        hence "([(x, x')] ∙ (P ∥ Q')) = Q''" by simp
        with x'FreshP xFreshP show ?thesis by(simp add: name_fresh_fresh)
      qed

      have "x ♯ Q''" by fact
      with Q''eq have x'FreshQ': "x' ♯ Q'" by(simp add: name_fresh_left name_calc)

      have "Q ⟼a<νx> ≺ Q'" by fact
      with x'FreshQ' aeqa' have "Q ⟼a'<νx'> ≺ ([(x, x')] ∙ Q')"
        by(simp add: alphaBoundOutput)
      moreover have "⋀C. F C Q a x' ([(x, x')] ∙ Q')"
      proof -
        fix C
        have "⋀C a' x' Q''. ⟦a<νx> ≺ Q' = a'<νx'> ≺ Q''; x' ♯ Q⟧ ⟹ F C Q a' x' Q''" by fact
        moreover with aeqa' xineqx' x'FreshQ' have "a<νx> ≺ Q' = a'<νx'> ≺ ([(x, x')] ∙ Q')"
          by(simp add: residual.inject name_abs_eq name_fresh_left name_calc)
        ultimately show "F C Q a x' ([(x, x')] ∙ Q')" using x'FreshQ aeqa' by blast 
      qed
      ultimately have "F C (P ∥ Q) a' x' (P ∥ ([(x, x')] ∙ Q'))" using x'FreshP aeqa'
        by(blast intro: cPar2B)
      with Q''eq show ?case by simp
    next
      case(Par2F P P' Q α)
      thus ?case by(simp add: residual.inject)
    next
      case(Comm1 P P' Q Q' a b x)
      thus ?case by(simp add: residual.inject)
    next
      case(Comm2 P P' Q Q' a b x)
      thus ?case by(simp add: residual.inject)
    next
      case(Close1 P P' Q Q' a x y)
      thus ?case by(simp add: residual.inject)
    next
      case(Close2 P P' Q Q' a x y)
      thus ?case by(simp add: residual.inject)
    next
      case(ResB P a x P' y C a' x' P'')
      have "x ♯ x'" by fact hence xineqx': "x ≠ x'" by simp
      moreover have Eq: "a<νx> ≺ (<νy>P') = a'<νx'> ≺ P''" by fact
      hence aeqa': "a = a'" by(simp add: residual.inject)
      have "y ♯ x'" by fact hence yineqx': "y ≠ x'" by simp
      moreover have "x' ♯ <νy>P" by fact
      ultimately have x'FreshP: "x' ♯ P" by(simp add: name_fresh_abs)
      have yineqx: "y ≠ x" and yineqa: "y ≠ a" and yFreshC: "y ♯ C" by fact+

      have P''eq: "P'' = <νy>([(x, x')] ∙ P')"
      proof -
        from Eq xineqx' have "<νy>P' = [(x, x')] ∙ P''"
          by(simp add: residual.inject name_abs_eq)
        hence "([(x, x')] ∙ (<νy>P')) = P''" by simp
        with yineqx' yineqx show ?thesis by(simp add: name_fresh_fresh)
      qed

      have "x ♯ P''" by fact
      with P''eq yineqx  have x'FreshP': "x' ♯ P'" by(simp add: name_fresh_left name_calc name_fresh_abs)

      have "P ⟼a<νx> ≺ P'" by fact
      with x'FreshP' aeqa' have "P ⟼a'<νx'> ≺ ([(x, x')] ∙ P')"
        by(simp add: alphaBoundOutput)
      moreover have "⋀C. F C P a x' ([(x, x')] ∙ P')"
      proof -
        fix C
        have "⋀C a' x' P''. ⟦a<νx> ≺ P' = a'<νx'> ≺ P''; x' ♯ P⟧ ⟹ F C P a' x' P''" by fact
        moreover with aeqa' xineqx' x'FreshP' have "a<νx> ≺ P' = a'<νx'> ≺ ([(x, x')] ∙ P')"
          by(simp add: residual.inject name_abs_eq name_fresh_left name_calc)
        ultimately show "F C P a x' ([(x, x')] ∙ P')" using x'FreshP aeqa' by blast 
      qed
      ultimately have "F C (<νy>P) a' x' (<νy>([(x, x')] ∙ P'))" using yineqx' yineqa yFreshC aeqa'
        by(force intro: cResB)
      with P''eq show ?case by simp
    next
      case(ResF P P' α y)
      thus ?case by(simp add: residual.inject)
    next
      case(Bang P Rs)
      thus ?case by(force intro: cBang)
    qed
  qed
    
  with a xFreshP show ?thesis by simp
qed

lemma tauInduct[consumes 1, case_names Tau Match Mismatch Sum1 Sum2 Par1 Par2 Comm1 Comm2 Close1 Close2 Res Bang]:
  fixes P  :: pi
  and   P' :: pi
  and   F  :: "'a::fs_name ⇒ pi ⇒ pi ⇒ bool"
  and   C  :: "'a::fs_name"

  assumes Trans:  "P ⟼τ ≺ P'"
  and     "⋀P C. F C (τ.(P)) P"
  and     "⋀P P' a C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'⟧ ⟹ F C ([a⌢a]P) P'"
  and     "⋀P P' a b C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'; a ≠ b⟧ ⟹ F C ([a≠b]P) P'"
  and     "⋀P P' Q C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'⟧ ⟹ F C (P ⊕ Q) P'"
  and     "⋀Q Q' P C. ⟦Q ⟼τ ≺ Q'; ⋀C. F C Q Q'⟧ ⟹ F C (P ⊕ Q) Q'"
  and     "⋀P P' Q C. ⟦P ⟼τ ≺ P'; ⋀C. F C P P'⟧ ⟹ F C (P ∥ Q) (P' ∥ Q)"
  and     "⋀Q Q' P C. ⟦Q ⟼τ ≺ Q'; ⋀C. F C Q Q'⟧ ⟹ F C (P ∥ Q) (P ∥ Q')"
  and     "⋀P a b P' Q Q' C. ⟦P ⟼a<b> ≺ P'; Q ⟼OutputR a b ≺ Q'⟧ ⟹ F C (P ∥ Q) (P' ∥ Q')"
  and     "⋀P a b P' Q Q' C. ⟦P ⟼OutputR a b ≺ P'; Q ⟼a<b> ≺ Q'⟧ ⟹ F C (P ∥ Q) (P' ∥ Q')"
  and     "⋀P a x P' Q Q' C. ⟦P ⟼a<x> ≺ P'; Q ⟼a<νx> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ♯ C⟧ ⟹ F C (P ∥ Q) (<νx>(P' ∥ Q'))"
  and     "⋀P a x P' Q Q' C. ⟦P ⟼a<νx> ≺ P'; Q ⟼a<x> ≺ Q'; x ♯ P; x ♯ Q; x ≠ a; x ♯ C⟧ ⟹ F C (P ∥ Q) (<νx>(P' ∥ Q'))"
  and     "⋀P P' x C. ⟦P ⟼τ ≺ P'; x ♯ C; ⋀C. F C P P'⟧ ⟹
                        F C (<νx>P) (<νx>P')"
  and     "⋀P P' C. ⟦P ∥ !P ⟼τ ≺ P'; ⋀C. F C (P ∥ !P) P'⟧ ⟹ F C (!P) P'"

  shows "F C P P'"
using ‹P ⟼τ ≺ P'›
by(nominal_induct x2=="τ ≺ P'" avoiding: C arbitrary: P' rule: TransitionsEarly.strong_induct)
  (auto simp add: residual.inject intro: assms)+

inductive bangPred :: "pi ⇒ pi ⇒ bool"
where
  aux1: "bangPred P (!P)"
| aux2: "bangPred P (P ∥ !P)"

inductive_cases tauCases'[simplified pi.distinct residual.distinct]: "τ.(P) ⟼ Rs"
inductive_cases inputCases'[simplified pi.inject residual.inject]: "a<b>.P ⟼ Rs"
inductive_cases outputCases'[simplified pi.inject residual.inject]: "a{b}.P ⟼ Rs"
inductive_cases matchCases'[simplified pi.inject residual.inject]: "[a⌢b]P ⟼ Rs"
inductive_cases mismatchCases'[simplified pi.inject residual.inject]: "[a≠b]P ⟼ Rs"
inductive_cases sumCases'[simplified pi.inject residual.inject]: "P ⊕ Q ⟼ Rs"
inductive_cases parCasesB'[simplified pi.distinct residual.distinct]: "A ∥ B ⟼ b<νy> ≺ A'"
inductive_cases parCasesF'[simplified pi.distinct residual.distinct]: "P ∥ Q ⟼ α ≺ P'"
inductive_cases resCasesB'[simplified pi.distinct residual.distinct]: "<νx'>A ⟼ a<νy'> ≺ A'"
inductive_cases resCasesF'[simplified pi.distinct residual.distinct]: "<νx>A ⟼ α ≺ A'"

lemma tauCases:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "τ.(P) ⟼α ≺ P'"
  and     "Prop (τ) P"

  shows "Prop α P'"
using assms
by(cases rule: tauCases') (auto simp add: pi.inject residual.inject)

lemma inputCases[consumes 1, case_names cInput]:
  fixes a  :: name
  and   x  :: name
  and   P  :: pi
  and   P' :: pi

  assumes Input: "a<x>.P ⟼α ≺ P'"
  and     A: "⋀u. Prop (a<u>) (P[x::=u])"

  shows "Prop α P'"
proof -
  {
    fix x P
    assume "a<x>.P ⟼α ≺ P'"
    moreover assume "(x::name) ♯ α" and "x ♯ P'" and "x ≠ a"
    moreover assume "⋀u. Prop (a<u>) (P[x::=u])"
    moreover obtain z::name where "z ≠ x" and "z ♯ P" and "z ♯ α" and "z ♯ P'"  and "z ≠ a"
      by(generate_fresh "name", auto simp add: fresh_prod)
    moreover obtain z'::name where "z' ≠ x" and "z' ≠ z" and "z' ♯ P" and "z' ♯ α" and "z' ♯ P'" and "z' ≠ a"
      by(generate_fresh "name", auto simp add: fresh_prod)
    ultimately have "Prop α P'"
      by(cases rule: TransitionsEarly.strong_cases[where x=x and b=z and xa=z and xb=z and xc=z and xd=z and xe=z
                                                   and y=z' and ya=z'])
        (auto simp add: pi.inject residual.inject abs_fresh alpha)
   }
   note Goal = this
   obtain y::name where "y ♯ P" and "y ♯ α" and "y ♯ P'" and "y ≠ a"
     by(generate_fresh "name") (auto simp add: fresh_prod)
   from Input ‹y ♯ P› have "a<y>.([(x, y)] ∙ P) ⟼α ≺ P'" by(simp add: alphaInput)
   moreover note ‹y ♯ α› ‹y ♯ P'› ‹y ≠ a›
   moreover from A ‹y ♯ P› have "⋀u. Prop (a<u>) (([(x, y)] ∙ P)[y::=u])"
     by(simp add: renaming name_swap)
   ultimately show ?thesis by(rule Goal)
qed

lemma outputCases:
  fixes P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes "a{b}.P ⟼α ≺ P'"
  and     "Prop (OutputR a b) P"

  shows "Prop α P'"
using assms
by(cases rule: outputCases') (auto simp add: pi.inject residual.inject)

lemma zeroTrans[dest]:
  fixes Rs :: residual

  assumes "𝟬 ⟼ e Rs"

  shows "False"
using assms
by - (ind_cases "𝟬 ⟼ e Rs")

lemma mismatchTrans[dest]:
  fixes a   :: name
  and   P   :: pi
  and   Rs  :: residual

  assumes "[a≠a]P ⟼ Rs"

  shows "False"
using assms
by(erule_tac mismatchCases') auto

lemma matchCases[consumes 1, case_names Match]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   Rs :: residual
  and   F  :: "name ⇒ name ⇒ bool"

  assumes Trans:  "[a⌢b]P ⟼ Rs"
  and     cMatch: "P ⟼ Rs ⟹ F a a"

  shows "F a b"
using assms
by(erule_tac matchCases', auto)

lemma mismatchCases[consumes 1, case_names Mismatch]:
  fixes a  :: name
  and   b  :: name
  and   P  :: pi
  and   Rs :: residual
  and   F  :: "name ⇒ name ⇒ bool"

  assumes Trans:  "[a≠b]P ⟼ Rs"
  and     cMatch: "⟦P ⟼ Rs; a ≠ b⟧ ⟹ F a b"

  shows "F a b"
using assms  
by(erule_tac mismatchCases') auto

lemma sumCases[consumes 1, case_names Sum1 Sum2]:
  fixes P  :: pi
  and   Q  :: pi
  and   Rs :: residual

  assumes Trans: "P ⊕ Q ⟼ Rs"
  and     cSum1: "P ⟼ Rs ⟹ F"
  and     cSum2: "Q ⟼ Rs ⟹ F"

  shows F
using assms
by(erule_tac sumCases') auto

lemma parCasesB[consumes 1, case_names cPar1 cPar2]:
  fixes P   :: pi
  and   Q   :: pi
  and   a   :: name
  and   x   :: name
  and   PQ' :: pi
  
  assumes Trans: "P ∥ Q ⟼ a<νx> ≺ PQ'"
  and     icPar1B: "⋀P'. ⟦P ⟼ a<νx> ≺ P'; x ♯ Q⟧ ⟹ F (P' ∥ Q)"
  and     icPar2B: "⋀Q'. ⟦Q ⟼ a<νx> ≺ Q'; x ♯ P⟧ ⟹ F (P ∥ Q')"

  shows "F PQ'"
proof -
  from Trans show ?thesis
  proof(induct rule: parCasesB', auto simp add: pi.inject residual.inject)
    fix P' y
    assume PTrans: "P ⟼ a<νy> ≺ P'"
    assume yFreshQ: "y ♯ (Q::pi)"
    assume absEq: "[x].PQ' = [y].(P' ∥ Q)"

    have "∃c::name. c ♯ (P', x, y, Q)" by(blast intro: name_exists_fresh)
    then obtain c where cFreshP': "c ♯ P'" and cineqx: "x ≠ c" and cineqy: "c ≠ y" and cFreshQ: "c ♯ Q"
      by(force simp add: fresh_prod name_fresh)

    from cFreshP' PTrans have Trans: "P ⟼ a<νc> ≺ ([(y, c)] ∙ P')" by(simp add: alphaBoundOutput)

    from cFreshP' cFreshQ have "c ♯ P' ∥ Q" by simp
    hence "[y].(P' ∥ Q) = [c].([(y, c)] ∙ (P' ∥ Q))"
      by(auto simp add: alpha fresh_left calc_atm)
    with yFreshQ cFreshQ have "[y].(P' ∥ Q) = [c].(([(y, c)] ∙ P') ∥ Q)"
      by(simp add: name_fresh_fresh)

    with cineqx absEq have L1: "PQ' = [(x, c)] ∙ (([(y, c)] ∙ P') ∥ Q)" and L2: "x ♯ ([(y, c)] ∙ P') ∥ Q"
      by(simp add: name_abs_eq)+
    
    from L2 have xFreshQ: "x ♯ Q" and xFreshP': "x ♯ [(y, c)] ∙ P'" by simp+
    with cFreshQ L1 have L3: "PQ' = ([(x, c)] ∙ [(y, c)] ∙ P') ∥ Q" by(simp add: name_fresh_fresh)

    from Trans xFreshP' have "P ⟼ a<νx> ≺ ([(x, c)] ∙ [(y, c)] ∙ P')" by(simp add: alphaBoundOutput name_swap)

    thus ?thesis using xFreshQ L3
      by(blast intro: icPar1B)
  next
    fix Q' y
    assume QTrans: "Q ⟼ a<νy> ≺ Q'"
    assume yFreshP: "y ♯ (P::pi)"
    assume absEq: "[x].PQ' = [y].(P ∥ Q')"

    have "∃c::name. c ♯ (Q', x, y, P)" by(blast intro: name_exists_fresh)
    then obtain c where cFreshQ': "c ♯ Q'" and cineqx: "x ≠ c" and cineqy: "c ≠ y" and cFreshP: "c ♯ P"
      by(force simp add: fresh_prod name_fresh)

    from cFreshQ' QTrans have Trans: "Q ⟼ a<νc> ≺ ([(y, c)] ∙ Q')" by(simp add: alphaBoundOutput)

    from cFreshQ' cFreshP have "c ♯ P ∥ Q'" by simp
    hence "[y].(P ∥ Q') = [c].([(y, c)] ∙ (P ∥ Q'))"
      by(auto simp add: alpha fresh_left calc_atm)
    with yFreshP cFreshP have "[y].(P ∥ Q') = [c].(P ∥ ([(y, c)] ∙ Q'))"
      by(simp add: name_fresh_fresh)

    with cineqx absEq have L1: "PQ' = [(x, c)] ∙ (P ∥ ([(y, c)] ∙ Q'))" and L2: "x ♯ P ∥ ([(y, c)] ∙ Q')"
      by(simp add: name_abs_eq)+
    
    from L2 have xFreshP: "x ♯ P" and xFreshQ': "x ♯ [(y, c)] ∙ Q'" by simp+
    with cFreshP L1 have L3: "PQ' = P ∥ ([(x, c)] ∙ [(y, c)] ∙ Q')" by(simp add: name_fresh_fresh)

    from Trans xFreshQ' have "Q ⟼ a<νx> ≺ ([(x, c)] ∙ [(y, c)] ∙ Q')" by(simp add: alphaBoundOutput name_swap)

    thus ?thesis using xFreshP L3
      by(blast intro: icPar2B)
  qed
qed

lemma parCasesOutput[consumes 1, case_names Par1 Par2]:
  fixes P  :: pi
  and   Q  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes "P ∥ Q ⟼a[b] ≺ PQ'"
  and     "⋀P'. ⟦P ⟼a[b] ≺ P'⟧ ⟹ F (P' ∥ Q)"
  and     "⋀Q'. ⟦Q ⟼a[b] ≺ Q'⟧ ⟹ F (P ∥ Q')"

  shows "F PQ'"
using assms
by(erule_tac parCasesF', auto simp add: pi.inject residual.inject)

lemma parCasesInput[consumes 1, case_names Par1 Par2]:
  fixes P  :: pi
  and   Q  :: pi
  and   a  :: name
  and   b  :: name
  and   P' :: pi

  assumes Trans: "P ∥ Q ⟼a<b> ≺ PQ'"
  and     icPar1F: "⋀P'. ⟦P ⟼a<b> ≺ P'⟧ ⟹ F (P' ∥ Q)"
  and     icPar2F: "⋀Q'. ⟦Q ⟼a<b> ≺ Q'⟧ ⟹ F (P ∥ Q')"

  shows "F PQ'"
using assms
by(erule_tac parCasesF') (auto simp add: pi.inject residual.inject)

lemma parCasesF[consumes 1, case_names cPar1 cPar2 cComm1 cComm2 cClose1 cClose2]:
  fixes P  :: pi
  and   Q  :: pi
  and   α  :: freeRes
  and   P' :: pi
  and   C  :: "'a::fs_name"

  assumes Trans: "P ∥ Q ⟼ α ≺ PQ'"
  and     icPar1F: "⋀P'. ⟦P ⟼ α ≺ P'⟧ ⟹ F α (P' ∥ Q)"
  and     icPar2F: "⋀Q'. ⟦Q ⟼ α ≺ Q'⟧ ⟹ F α (P ∥ Q')"
  and     icComm1: "⋀P' Q' a b. ⟦P ⟼ a<b> ≺ P'; Q ⟼ a[b] ≺ Q'⟧ ⟹ F (τ) (P' ∥ Q')"
  and     icComm2: "⋀P' Q' a b. ⟦P ⟼ a[b] ≺ P'; Q ⟼ a<b> ≺ Q'⟧ ⟹ F (τ) (P' ∥ Q')"
  and     icClose1: "⋀P' Q' a x. ⟦P ⟼ a<x> ≺ P'; Q ⟼ a<νx> ≺ Q'; x ♯ P; x ♯ C⟧ ⟹ F (τ) (<νx>(P' ∥ Q'))"
  and     icClose2: "⋀P' Q' a x. ⟦P ⟼ a<νx> ≺ P'; Q ⟼ a<x> ≺ Q'; x ♯ Q; x ♯ C⟧ ⟹ F (τ) (<νx>(P' ∥ Q'))"

  shows "F α PQ'"
proof -
  from Trans show ?thesis
  proof(rule parCasesF', auto)
    fix Pa Pa' Qa α'
    assume Trans': "Pa ⟼ α' ≺ Pa'"
    assume Eq: "P ∥ Q = Pa ∥ Qa"
    assume Eq': "α ≺ PQ' = α' ≺ Pa' ∥ Qa"

    from Eq have "P = Pa" and "Q = Qa"
      by(simp add: pi.inject)+
    
    moreover with Eq' have "α = α'" and "PQ' = Pa' ∥ Q"
      by(simp add: residual.inject)+

    ultimately show ?thesis using icPar1F Trans'
      by simp
  next
    fix Pa Qa Qa' α'
    assume Trans': "Qa ⟼ α' ≺ Qa'"
    assume Eq: "P ∥ Q = Pa ∥ Qa"
    assume Eq': "α ≺ PQ' = α' ≺ Pa ∥ Qa'"

    from Eq have "P = Pa" and "Q = Qa"
      by(simp add: pi.inject)+
    
    moreover with Eq' have "α = α'" and "PQ' = P ∥ Qa'"
      by(simp add: residual.inject)+

    ultimately show ?thesis using icPar2F Trans'
      by simp
  next
    fix Pa Pa' Qa Qa' a b
    assume TransP: "Pa ⟼ a<b> ≺ Pa'"
    assume TransQ: "Qa ⟼ a[b] ≺ Qa'"
    assume Eq: "P ∥ Q = Pa ∥ Qa"
    assume Eq': "α ≺ PQ' = τ ≺ Pa' ∥ Qa'"

    from TransP TransQ Eq Eq' icComm1 show ?thesis
      by(simp add: pi.inject residual.inject)
  next
    fix Pa Pa' Qa Qa' a b x
    assume TransP: "Pa ⟼ (a::name)[b] ≺ Pa'"
    assume TransQ: "Qa ⟼ a<b> ≺ Qa'"
    assume Eq: "P ∥ Q = Pa ∥ Qa"
    assume Eq': "α ≺ PQ' = τ ≺ Pa' ∥ Qa'"

    from TransP TransQ Eq Eq' icComm2 show ?thesis
      by(simp add: pi.inject residual.inject)
  next
    fix Pa Pa' Qa Qa' a x
    assume TransP: "Pa ⟼ a<x> ≺ Pa'"
    assume TransQ: "Qa ⟼ a<νx> ≺ Qa'"
    assume xFreshPa: "x ♯ Pa"
    assume Eq: "P ∥ Q = Pa ∥ Qa"
    assume Eq': "α ≺ PQ' = τ ≺ <νx>(Pa' ∥ Qa')"

    have "∃(c::name). c ♯ (Pa, Pa', x, Qa', a, C)"
      by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshPa: "c ♯ Pa" and cFreshPa': "c ♯ Pa'" and cineqy: "c ≠ x" and cFreshQa': "c ♯ Qa'" and cFreshC: "c ♯ C" and cineqa: "c ≠ a"
      by(force simp add: fresh_prod name_fresh)

    from cFreshQa' have L1: "a<νx> ≺ Qa' = a<νc> ≺ ([(x, c)] ∙ Qa')"
      by(simp add: alphaBoundOutput)
    with cFreshQa' cFreshPa' have "c ♯ (Pa' ∥ Qa')"
      by simp
    then have L4: "<νx>(Pa' ∥ Qa') = <νc>(([(x, c)] ∙ Pa') ∥ ([(x, c)] ∙ Qa'))"
      by(simp add: alphaRes)

    have TransP: "Pa ⟼ a<c> ≺ [(x, c)] ∙ Pa'"
    proof -
      from xFreshPa TransP have xineqa: "x≠a" by(force dest: freshAction)
      from TransP have "([(x, c)] ∙ Pa) ⟼ [(x, c)] ∙ (a<x> ≺ Pa')"
        by(rule TransitionsEarly.eqvt)
      with xineqa xFreshPa cFreshPa cineqa show ?thesis
        by(simp add: name_fresh_fresh name_calc)
    qed

    with TransQ L1 L4 icClose1 Eq Eq' cFreshPa cFreshC show ?thesis
      by(simp add: residual.inject, simp add: pi.inject)
  next
    fix Pa Pa' Qa Qa' a x
    assume TransP: "Pa ⟼ a<νx> ≺ Pa'"
    assume TransQ: "Qa ⟼ a<x> ≺ Qa'"
    assume xFreshQa: "x ♯ Qa"
    assume Eq: "P ∥ Q = Pa ∥ Qa"
    assume Eq': "α ≺ PQ' = τ ≺ <νx>(Pa' ∥ Qa')"

    have "∃(c::name). c ♯ (Qa, Pa', x, Qa', a, C)"
      by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshQa: "c ♯ Qa" and cFreshPa': "c ♯ Pa'" and cineqy: "c ≠ x" and cFreshQa': "c ♯ Qa'" and cFreshC: "c ♯ C" and cineqa: "c ≠ a"
      by(force simp add: fresh_prod name_fresh)

    from cFreshPa' have L1: "a<νx> ≺ Pa' = a<νc> ≺ ([(x, c)] ∙ Pa')"
      by(simp add: alphaBoundOutput)
    with cFreshQa' cFreshPa' have "c ♯ (Pa' ∥ Qa')"
      by simp
    then have L4: "<νx>(Pa' ∥ Qa') = <νc>(([(x, c)] ∙ Pa') ∥ ([(x, c)] ∙ Qa'))"
      by(simp add: alphaRes)

    have TransQ: "Qa ⟼ a<c> ≺ [(x, c)] ∙ Qa'"
    proof -
      from xFreshQa TransQ have xineqa: "x≠a" by(force dest: freshAction)
      from TransQ have "([(x, c)] ∙ Qa) ⟼ [(x, c)] ∙ (a<x> ≺ Qa')"
        by(rule TransitionsEarly.eqvt)
      with xineqa xFreshQa cFreshQa cineqa show ?thesis
        by(simp add: name_fresh_fresh name_calc)
    qed

    with TransP L1 L4 icClose2 Eq Eq' cFreshQa cFreshC show ?thesis
      by(simp add: residual.inject, simp add: pi.inject)
  qed
qed

lemma resCasesF[consumes 2, case_names Res]:
  fixes x :: name
  and   P  :: pi
  and   α  :: freeRes
  and   P' :: pi

  assumes Trans: "<νx>P ⟼ α ≺ RP'"
  and     xFreshAlpha: "x ♯ α"
  and     rcResF: " ⋀P'. P ⟼ α ≺ P' ⟹ F (<νx>P')"

  shows "F RP'"
proof -
  from Trans show ?thesis
  proof(induct rule: resCasesF', auto)
    fix Pa Pa' β y
    assume PTrans: "Pa ⟼ β ≺ Pa'"
    assume yFreshBeta: "(y::name) ♯ β"
    assume TermEq: "<νx>P = <νy>Pa"
    assume ResEq: "α ≺ RP' = β ≺ <νy>Pa'"

    hence alphaeqbeta: "α = β" and L2: "RP' = <νy>Pa'" by(simp add: residual.inject)+

    have "∃(c::name). c ♯ (Pa, α, Pa', x, y)" by(blast intro: name_exists_fresh)
    then obtain c::name where cFreshPa: "c ♯ Pa" and cFreshAlpha: "c ♯ α" and cFreshPa': "c ♯ Pa'" and cineqx: "x ≠ c" and cineqy: "c ≠ y"
      by(force simp add: fresh_prod name_fresh)

    from cFreshPa have "<νy>Pa = <νc>([(y, c)] ∙ Pa)" by(rule alphaRes)
    with TermEq cineqx have Peq: "P = [(x, c)] ∙ [(y, c)] ∙ Pa" and xeq: "x ♯ [(y, c)] ∙ Pa"
      by(simp add: pi.inject name_abs_eq)+

    from PTrans have "([(y, c)] ∙ Pa) ⟼ [(y, c)] ∙ (β ≺ Pa')" by(rule TransitionsEarly.eqvt)
    with yFreshBeta cFreshAlpha alphaeqbeta have PTrans': "([(y, c)] ∙ Pa) ⟼ α ≺ ([(y, c)] ∙ Pa')" 
      by(simp add: name_fresh_fresh)

    from PTrans' have "([(x, c)] ∙ [(y, c)] ∙ Pa) ⟼ [(x, c)] ∙ (α ≺ [(y, c)] ∙ Pa')"
      by(rule TransitionsEarly.eqvt)
    with xFreshAlpha cFreshAlpha Peq have PTrans'': "P ⟼ α ≺ [(x, c)] ∙ [(y, c)] ∙ Pa'"
      by(simp add: name_fresh_fresh)

    from PTrans' xeq xFreshAlpha have xeq': "x ♯ [(y, c)] ∙ Pa'"
      by(nominal_induct α rule: freeRes.strong_induct)
        (auto simp add: fresh_left calc_atm eqvts dest: freshTransition)

    from cFreshPa' have "<νy>Pa' = <νc>([(y, c)] ∙ Pa')" by(rule alphaRes)
    moreover from xeq' have "<νc>([(y, c)] ∙ Pa') = <νx>([(c, x)] ∙ [(y, c)] ∙ Pa')"
      by(rule alphaRes)
    ultimately have "RP' = <νx>([(x, c)] ∙ [(y, c)] ∙ Pa')" using ResEq
      by(simp add: residual.inject name_swap)

    with PTrans'' xFreshAlpha show ?thesis
      by(blast intro: rcResF)
  qed
qed

lemma resCasesB[consumes 2, case_names Open Res]:
  fixes x :: name
  and   P  :: pi
  and   a  :: name
  and   y :: name
  and   RP' :: pi

  assumes Trans:  "<νy>P ⟼ a<νx> ≺ RP'"
  and     xineqy: "x ≠ y"
  and     rcOpen: "⋀P'. ⟦P ⟼(OutputR a y) ≺ P'; a ≠ y⟧ ⟹ F ([(x, y)] ∙ P')"
  and     rcResB: "⋀P'. ⟦P ⟼a<νx> ≺ P'; y ≠ a⟧ ⟹ F (<νy>P')"

  shows "F RP'"
proof -
  from Trans show ?thesis
  proof(induct rule: resCasesB', auto)
    fix Pa Pa' aa b
    assume PTrans: "Pa ⟼ (aa::name)[b] ≺ Pa'"
    assume aaineqb: "aa≠b"
    assume TermEq: "<νy>P = <νb>Pa"
    assume ResEq: "a<νx> ≺ RP' = aa<νb> ≺ Pa'"

    have "∃(c::name). c ♯ (x, a, aa, y, Pa, Pa', b)" by(blast intro: name_exists_fresh)
    then obtain c where cineqx: "c≠x" and cFresha: "c ♯ a" and cineqy: "c ≠ y" and cineqaa: "c ≠ aa" and cFreshPa: "c ♯ Pa" and cFreshPa': "c ♯ Pa'" and cineqb: "c ≠ b"
      by(force simp add: fresh_prod name_fresh)

    from cFreshPa have "<νb>Pa = <νc>([(b, c)] ∙ Pa)" by(rule alphaRes)
    with cineqy TermEq have PEq: "P = [(y, c)] ∙ [(b, c)] ∙ Pa" and yFreshPa: "y ♯ [(b, c)] ∙ Pa"
      by(simp add: pi.inject name_abs_eq)+

    from PTrans have "([(b, c)] ∙ Pa) ⟼ ([(b, c)] ∙ (aa[b] ≺ Pa'))" by(rule TransitionsEarly.eqvt)
    with aaineqb cineqaa have L1: "([(b, c)] ∙ Pa) ⟼ aa[c] ≺ [(b, c)] ∙ Pa'" by(simp add: name_calc)
    with yFreshPa have yineqaa: "y ≠ aa" by(force dest: freshAction)
    from L1 yFreshPa cineqy have yFreshPa': "y ♯ [(b, c)] ∙ Pa'" by(force intro: freshTransition)

    from L1 have "([(y, c)] ∙ [(b, c)] ∙ Pa) ⟼ [(y, c)] ∙ (aa[c] ≺ [(b, c)] ∙ Pa')"
      by(rule TransitionsEarly.eqvt)
    with cineqaa yineqaa cineqy PEq have PTrans: "P ⟼ aa[y] ≺ [(y, c)] ∙ [(b, c)] ∙ Pa'"
      by(simp add: name_calc)
    moreover from cFreshPa' have "aa<νb> ≺ Pa' = aa<νc> ≺ ([(b, c)] ∙ Pa')" by(rule alphaBoundOutput)
    with ResEq cineqx have ResEq': "RP' = [(x, c)] ∙ [(b, c)] ∙ Pa'" and "x ♯ [(b, c)] ∙ Pa'"
      by(simp add: residual.inject name_abs_eq)+
    with xineqy cineqy cineqx yFreshPa' have "RP' = [(x, y)] ∙ [(y, c)] ∙ [(b, c)] ∙ Pa'"
      by(subst pt_perm_compose[OF pt_name_inst, OF at_name_inst], simp add: name_calc name_fresh_fresh)
    moreover from ResEq have "a=aa" by(simp add: residual.inject)
    ultimately show ?thesis using yineqaa rcOpen
      by blast
  next
    fix Pa Pa' aa xa ya
    assume PTrans: "Pa ⟼ aa<νxa> ≺ Pa'"
    assume yaFreshaa: "(ya::name) ≠ aa"
    assume yaineqxa: "ya ≠ xa"
    assume EqTrans: "<νy>P = <νya>Pa"
    assume EqRes: "a<νx> ≺ RP' = aa<νxa> ≺ (<νya>Pa')"
    
    hence aeqaa: "a = aa" by(simp add: residual.inject)
    with yaFreshaa have yaFresha: "ya ♯ a" by simp

    have "∃(c::name). c ♯ (Pa', y, xa, ya, x, Pa, aa)" by(blast intro: name_exists_fresh)
    then obtain c where cFreshPa': "c ♯ Pa'" and cineqy: "c ≠ y" and cineqxa: "c ≠ xa" and cineqya: "c ≠ ya" and cineqx: "c ≠ x" and cFreshP: "c ♯ Pa" and cFreshaa: "c ♯ aa"
      by(force simp add: fresh_prod name_fresh)

    have "∃(d::name). d ♯ (Pa, a, x, Pa', c, xa, ya, y)" by(blast intro: name_exists_fresh)
    then obtain d where dFreshPa: "d ♯ Pa" and dFresha: "d ♯ a" and dineqx: "d ≠ x" and dFreshPa': "d ♯ Pa'" and dineqc: "d≠c" and dineqxa: "d ≠ xa" and dineqya: "d ≠ ya" and dineqy: "d ≠ y"
      by(force simp add: fresh_prod name_fresh)

    from dFreshPa have "<νya>Pa = <νd>([(ya, d)] ∙ Pa)" by(rule alphaRes)
    with EqTrans dineqy have PEq: "P = [(y, d)] ∙ [(ya, d)] ∙ Pa"
                         and yFreshPa: "y ♯ [(ya, d)] ∙ Pa"
      by(simp add: pi.inject name_abs_eq)+

    from dFreshPa' have L1: "<νya>Pa' = <νd>([(ya, d)] ∙ Pa')" by(rule alphaRes)
    from cFreshPa' dineqc cineqya have "c ♯ <νd>([(ya, d)] ∙ Pa')"
      by(simp add: name_fresh_abs name_calc name_fresh_left)
    hence "aa<νxa> ≺ (<νd>([(ya, d)] ∙ Pa')) = aa<νc> ≺ ([(xa, c)] ∙ <νd>([(ya, d)] ∙ Pa'))" (is "?LHS = _")
      by(rule alphaBoundOutput)
    with dineqxa dineqc have "?LHS = aa<νc> ≺ (<νd>([(xa, c)] ∙ [(ya, d)] ∙ Pa'))"
      by(simp add: name_calc)
    with L1 EqRes cineqx dineqc dineqx have
          RP'Eq: "RP' = <νd>([(x, c)] ∙ [(xa, c)] ∙ [(ya, d)] ∙ Pa')"
      and xFreshPa': "x ♯ [(xa, c)] ∙ [(ya, d)] ∙ Pa'"
      by(simp add: residual.inject name_abs_eq name_fresh_abs name_calc)+

    from PTrans aeqaa have "([(ya, d)] ∙ Pa) ⟼ [(ya, d)] ∙ (a<νxa> ≺ Pa')"
      by(blast intro: TransitionsEarly.eqvt)
    with yaineqxa yaFresha dineqxa dFresha have L1:
      "([(ya, d)] ∙ Pa) ⟼ a<νxa> ≺ ([(ya, d)] ∙ Pa')" by(simp add: name_calc name_fresh_fresh)
    with yFreshPa have yineqa: "y ≠ a" by(force dest: freshAction)    
    from dineqc cineqya cFreshPa' have "c ♯ [(ya, d)] ∙ Pa'"
      by(simp add: name_fresh_left name_calc)
    hence "a<νxa> ≺ ([(ya, d)] ∙ Pa') = a<νc> ≺ ([(xa, c)] ∙ [(ya, d)] ∙ Pa')" (is "?LHS = _")
      by(rule alphaBoundOutput)
    with xFreshPa' have L2: "?LHS = a<νx> ≺ ([(c, x)] ∙ [(xa, c)] ∙ [(ya, d)] ∙ Pa')"
      by(simp add: alphaBoundOutput)
    with L1 PEq have "P ⟼ [(y, d)] ∙ (a<νx> ≺ ([(c, x)] ∙ [(xa, c)] ∙ [(ya, d)] ∙ Pa'))"
      by(force intro: TransitionsEarly.eqvt simp del: residual.perm)
    with yineqa dFresha xineqy dineqx have Trans: "P ⟼ a<νx> ≺ ([(y, d)] ∙ [(c, x)] ∙ [(xa, c)] ∙ [(ya, d)] ∙ Pa')"
      by(simp add: name_calc name_fresh_fresh)

    from L1 L2 yFreshPa xineqy have "y ♯ [(c, x)] ∙ [(xa, c)] ∙ [(ya, d)] ∙ Pa'"
      by(force intro: freshTransition)
    with RP'Eq have "RP' = <νy>([(y, d)] ∙ [(c, x)] ∙ [(xa, c)] ∙ [(ya, d)] ∙ Pa')"
      by(simp add: alphaRes name_swap)

    with Trans yineqa show ?thesis
      by(blast intro: rcResB)
  qed
qed

lemma bangInduct[consumes 1, case_names Par1B Par1F Par2B Par2F Comm1 Comm2 Close1 Close2 Bang]:
  fixes F  :: "'a::fs_name ⇒ pi ⇒ residual ⇒ bool"
  and   P  :: pi
  and   Rs :: residual
  and   C  :: "'a::fs_name"

  assumes Trans:  "!P ⟼ Rs"
  and     cPar1B: "⋀a x P' C. ⟦P ⟼ a<νx> ≺ P'; x ♯ P; x ♯ C⟧ ⟹ F  C (P ∥ !P) (a<νx> ≺ (P' ∥ !P))"
  and     cPar1F: "⋀(α::freeRes) (P'::pi) C. ⟦P ⟼ α ≺ P'⟧ ⟹ F  C (P ∥ !P) (α ≺ P' ∥ !P)"
  and     cPar2B: "⋀a x P' C. ⟦!P ⟼ a<νx> ≺ P'; x ♯ P; x ♯ C; ⋀C. F C (!P) (a<νx> ≺ P')⟧ ⟹ F  C (P ∥ !P) (a<νx> ≺ (P ∥ P'))"
  and     cPar2F: "⋀α P' C. ⟦!P ⟼ α ≺ P'; ⋀C. F C (!P) (α ≺ P')⟧ ⟹ F C (P ∥ !P) (α ≺ P ∥ P')"
  and     cComm1: "⋀a P' b P'' C. ⟦P ⟼ a<b> ≺ P'; !P ⟼ (OutputR a b) ≺ P''; ⋀C. F C (!P) ((OutputR a b) ≺ P'')⟧ ⟹
                                     F C (P ∥ !P) (τ ≺ P' ∥ P'')"
  and     cComm2: "⋀a b P' P'' C. ⟦P ⟼ (OutputR a b) ≺ P'; !P ⟼ a<b> ≺ P''; ⋀C. F C (!P) (a<b> ≺ P'')⟧ ⟹
                                     F C (P ∥ !P) (τ ≺ P' ∥ P'')"
  and     cClose1: "⋀a x P' P'' C. ⟦P ⟼ a<x> ≺ P'; !P ⟼ a<νx> ≺ P''; x ♯ P; x ♯ C; ⋀C. F C (!P) (a<νx> ≺ P'')⟧ ⟹
                                     F C (P ∥ !P) (τ ≺ <νx>(P' ∥ P''))"
  and     cClose2: "⋀a x P' P'' C. ⟦P ⟼ a<νx> ≺ P'; !P ⟼ a<x> ≺ P''; x ♯ P; x ♯ C; ⋀C. F C (!P) (a<x> ≺ P'')⟧ ⟹
                                     F C (P ∥ !P) (τ ≺ <νx>(P' ∥ P''))"
  and     cBang: "⋀Rs C. ⟦P ∥ !P ⟼ Rs; ⋀C. F C (P ∥ !P) Rs⟧ ⟹ F C (!P) Rs"

  shows "F C (!P) Rs"
proof -
  have "⋀X Y C. ⟦X ⟼ Y; bangPred P X⟧ ⟹ F C X Y"
  proof -
    fix X Y C
    assume "X ⟼ Y" and "bangPred P X"
    thus "F C X Y"
    proof(nominal_induct avoiding: C rule: TransitionsEarly.strong_induct)
      case(Tau Pa)
      thus ?case
        apply -
        by(ind_cases "bangPred P (τ.(Pa))")
    next
      case(Input x a u Pa C)
      thus ?case
        by - (ind_cases "bangPred P (a<x>.Pa)")
    next
      case(Output a b Pa C)
      thus ?case
        by - (ind_cases "bangPred P (a{b}.Pa)")
    next
      case(Match Pa Rs b C)
      thus ?case
        by - (ind_cases "bangPred P ([b⌢b]Pa)")
    next
      case(Mismatch Pa Rs a b C)
      thus ?case
        by - (ind_cases "bangPred P ([a ≠ b]Pa)")
    next
      case(Open Pa a b Pa')
      thus ?case
        by - (ind_cases "bangPred P (<νb>Pa)")
    next
      case(Sum1 Pa Rs Q)
      thus ?case
        by - (ind_cases "bangPred P (Pa ⊕ Q)")
    next
      case(Sum2 Q Rs Pa)
      thus ?case
        by - (ind_cases "bangPred P (Pa ⊕ Q)")
    next
      case(Par1B Pa a x P' Q C)
      thus ?case 
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject cPar1B)
    next
      case(Par1F Pa α P' Q C)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject cPar1F)
    next
      case(Par2B Q a x Q' Pa)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject aux1 cPar2B)
    next
      case(Par2F Q α Q' Pa)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject intro: cPar2F aux1)
    next
      case(Comm1 Pa a b Pa' Q Q' C)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject intro: cComm1 aux1)
    next
      case(Comm2 Pa a b Pa' Q P'' C)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject intro: cComm2 aux1)
    next
      case(Close1 Pa a x Pa' Q Q'' C)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject aux1 cClose1)
    next
      case(Close2 Pa a x Pa' Q Q' C)
      thus ?case
        by - (ind_cases "bangPred P (Pa ∥ Q)", auto simp add: pi.inject aux1 cClose2)
    next
      case(ResB Pa a x Pa' y)
      thus ?case
        by - (ind_cases "bangPred P (<νy>Pa)")
    next
      case(ResF Pa α Pa' y)
      thus ?case
        by - (ind_cases "bangPred P (<νy>Pa)")
    next
      case(Bang Pa Rs)
      thus ?case
        by - (ind_cases "bangPred P (!Pa)", auto simp add: pi.inject intro: aux2 cBang)
    qed
  qed
  with Trans show ?thesis by(force intro: bangPred.aux1)
qed

end