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

context env begin

abbreviation tauChain :: "'b → ('a, 'b, 'c) psi → ('a, 'b, 'c) psi → bool" (‹_ ⊳ _ ==>^{^}_\τ _› [80, 80, 80] 80)
where "Ψ ⊳ P ==>^{^}_\<tau> P' ≡ (P, P') ∈ {(P, P'). Ψ ⊳ P ⟼τ ≺ P'}^*"

abbreviation tauStepChain :: "'b → ('a, 'b, 'c) psi → ('a, 'b, 'c) psi → bool" (‹_ ⊳ _ ==>_\τ _› [80, 80, 80] 80)
where "Ψ ⊳ P ==>_\<tau> P' ≡ (P, P') ∈ {(P, P'). Ψ ⊳ P ⟼τ ≺ P'}^+"

abbreviation tauContextChain :: "('a, 'b, 'c) psi → ('a, 'b, 'c) psi → bool" (‹_ ==>^{^}_\τ _› [80, 80] 80)
where "P ==>^{^}_\<tau> P' ≡ 1 ⊳ P ==>^{^}_\<tau> P'"
abbreviation tauContextStepChain :: "('a, 'b, 'c) psi → ('a, 'b, 'c) psi → bool" (‹_ ==>_\τ _› [80, 80] 80)
where "P ==>_\<tau> P' ≡ 1 ⊳ P ==>_\<tau> P'"

lemmas tauChainInduct[consumes 1, case_names TauBase TauStep] = rtrancl.induct[of _ _ "{(P, P'). Ψ ⊳ P ⟼τ ≺ P'}", simplified] for Ψ
lemmas tauStepChainInduct[consumes 1, case_names TauBase TauStep] = trancl.induct[of _ _ "{(P, P'). Ψ ⊳ P ⟼τ ≺ P'}", simplified] for Ψ


lemma tauActTauStepChain:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ⟼τ ≺ P'"

  shows "Ψ ⊳ P ==>_\<tau> P'"
using assms by auto

lemma tauActTauChain:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ⟼τ ≺ P'"

  shows "Ψ ⊳ P ==>^{^}_\<tau> P'"
using assms by(auto simp add: rtrancl_eq_or_trancl)

lemma tauStepChainEqvt[eqvt]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  assumes "Ψ ⊳ P ==>_\<tau> P'"

  shows "(p ∙ Ψ) ⊳ (p ∙ P) ==>_\<tau> (p ∙ P')"
using assms
proof(induct rule: tauStepChainInduct)  
  case(TauBase P P')
  hence "Ψ ⊳ P ⟼τ ≺ P'" by simp
  thus ?case by(force dest: semantics.eqvt simp add: eqvts)
next
  case(TauStep P P' P'')
  hence "Ψ ⊳ P' ⟼τ ≺ P''" by simp  
  hence "(p ∙ Ψ) ⊳ (p ∙ P') ⟼τ ≺ (p ∙ P'')" by(force dest: semantics.eqvt simp add: eqvts)
  with ‹(p ∙ Ψ) ⊳ (p ∙ P) ==>_\τ (p ∙ P')› show ?case
    by(subst trancl.trancl_into_trancl) auto
qed

lemma tauChainEqvt[eqvt]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P'"

  shows "(p ∙ Ψ) ⊳ (p ∙ P) ==>^{^}_\<tau> (p ∙ P')"
using assms
by(auto simp add: rtrancl_eq_or_trancl eqvts)

lemma tauStepChainEqvt'[eqvt]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  shows "(p ∙ (Ψ ⊳ P ==>_\<tau> P')) = (p ∙ Ψ) ⊳ (p ∙ P) ==>_\<tau> (p ∙ P')"
apply(auto simp add: eqvts perm_set_def pt_bij[OF pt_name_inst, OF at_name_inst])
by(drule_tac p="rev p" in tauStepChainEqvt) auto

lemma tauChainEqvt'[eqvt]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   p  :: "name prm"

  shows "(p ∙ (Ψ ⊳ P ==>^{^}_\<tau> P')) = (p ∙ Ψ) ⊳ (p ∙ P) ==>^{^}_\<tau> (p ∙ P')"
apply(auto simp add: eqvts perm_set_def pt_bij[OF pt_name_inst, OF at_name_inst] rtrancl_eq_or_trancl)
by(drule_tac p="rev p" in tauStepChainEqvt) auto

lemma tauStepChainFresh:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name

  assumes "Ψ ⊳ P ==>_\<tau> P'"
  and     "x ♯ P"

  shows "x ♯ P'"
using assms
by(induct rule: trancl.induct) (auto dest: tauFreshDerivative)

lemma tauChainFresh:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     "x ♯ P"

  shows "x ♯ P'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainFresh)

lemma tauStepChainFreshChain:
  fixes Ψ    :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   P'    :: "('a, 'b, 'c) psi"
  and   xvec  :: "name list"

  assumes "Ψ ⊳ P ==>_\<tau> P'"
  and     "xvec ♯* P"

  shows "xvec ♯* P'"
using assms
by(induct xvec) (auto intro: tauStepChainFresh)

lemma tauChainFreshChain:
  fixes Ψ    :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   P'    :: "('a, 'b, 'c) psi"
  and   xvec  :: "name list"

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     "xvec ♯* P"

  shows "xvec ♯* P'"
using assms
by(induct xvec) (auto intro: tauChainFresh)

lemma tauStepChainCase:
  fixes Ψ  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   φ  :: 'c
  and   Cs :: "('c × ('a, 'b, 'c) psi) list"

  assumes "Ψ ⊳ P ==>_\<tau> P'"
  and     "(φ, P) mem Cs"
  and     "Ψ ⊨ φ"
  and     "guarded P"

  shows "Ψ ⊳ (Cases Cs) ==>_\<tau> P'"
using assms
by(induct rule: trancl.induct) (auto intro: Case trancl_into_trancl)

lemma tauStepChainResPres:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name  

  assumes "Ψ ⊳ P ==>_\<tau> P'"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ (νx)P ==>_\<tau> (νx)P'"
using assms
by(induct rule: trancl.induct) (auto dest: Scope trancl_into_trancl)

lemma tauChainResPres:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   x  :: name  

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ (νx)P ==>^{^}_\<tau> (νx)P'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainResPres)

lemma tauStepChainResChainPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes "Ψ ⊳ P ==>_\<tau> P'"
  and     "xvec ♯* Ψ"

  shows "Ψ ⊳ (ν*xvec)P ==>_\<tau> (ν*xvec)P'"
using assms
by(induct xvec) (auto intro: tauStepChainResPres)

lemma tauChainResChainPres:
  fixes Ψ    :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   P'   :: "('a, 'b, 'c) psi"
  and   xvec :: "name list"

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     "xvec ♯* Ψ"

  shows "Ψ ⊳ (ν*xvec)P ==>^{^}_\<tau> (ν*xvec)P'"
using assms
by(induct xvec) (auto intro: tauChainResPres)

lemma tauStepChainPar1:
  fixes Ψ  :: 'b
  and   Ψ_Q :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   A_Q :: "name list"

  assumes "Ψ ⊗ Ψ_Q ⊳ P ==>_\<tau> P'"
  and     "extractFrame Q = ⟨A_Q, Ψ_Q⟩"
  and     "A_Q ♯* Ψ"
  and     "A_Q ♯* P"

  shows "Ψ ⊳ P ∥ Q ==>_\<tau> P' ∥ Q"
using assms
by(induct rule: trancl.induct)  (auto dest: Par1 tauStepChainFreshChain trancl_into_trancl)

lemma tauChainPar1:
  fixes Ψ  :: 'b
  and   Ψ_Q :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   Q   :: "('a, 'b, 'c) psi"
  and   A_Q :: "name list"

  assumes "Ψ ⊗ Ψ_Q ⊳ P ==>^{^}_\<tau> P'"
  and     "extractFrame Q = ⟨A_Q, Ψ_Q⟩"
  and     "A_Q ♯* Ψ"
  and     "A_Q ♯* P"

  shows "Ψ ⊳ P ∥ Q ==>^{^}_\<tau> P' ∥ Q"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainPar1)

lemma tauStepChainPar2:
  fixes Ψ  :: 'b
  and   Ψ_P :: 'b
  and   Q   :: "('a, 'b, 'c) psi"
  and   Q'  :: "('a, 'b, 'c) psi"
  and   P   :: "('a, 'b, 'c) psi"
  and   A_P :: "name list"

  assumes "Ψ ⊗ Ψ_P ⊳ Q ==>_\<tau> Q'"
  and     "extractFrame P = ⟨A_P, Ψ_P⟩"
  and     "A_P ♯* Ψ"
  and     "A_P ♯* Q"

  shows "Ψ ⊳ P ∥ Q ==>_\<tau> P ∥ Q'"
using assms
by(induct rule: trancl.induct) (auto dest: Par2 trancl_into_trancl tauStepChainFreshChain)

lemma tauChainPar2:
  fixes Ψ  :: 'b
  and   Ψ_P :: 'b
  and   Q   :: "('a, 'b, 'c) psi"
  and   Q'  :: "('a, 'b, 'c) psi"
  and   P   :: "('a, 'b, 'c) psi"
  and   A_P :: "name list"

  assumes "Ψ ⊗ Ψ_P ⊳ Q ==>^{^}_\<tau> Q'"
  and     "extractFrame P = ⟨A_P, Ψ_P⟩"
  and     "A_P ♯* Ψ"
  and     "A_P ♯* Q"

  shows "Ψ ⊳ P ∥ Q ==>^{^}_\<tau> P ∥ Q'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainPar2)

lemma tauStepChainBang:
  fixes Ψ  :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ∥ !P ==>_\<tau> P'"
  and     "guarded P"

  shows "Ψ ⊳ !P ==>_\<tau> P'"
using assms
by(induct x1=="P ∥ !P" P' rule: trancl.induct) (auto intro: Bang dest: Bang trancl_into_trancl)

lemma tauStepChainStatEq:
  fixes Ψ  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b

  assumes "Ψ ⊳ P ==>_\<tau> P'"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' ⊳ P ==>_\<tau> P'"
using assms
by(induct rule: trancl.induct) (auto dest: statEqTransition trancl_into_trancl)

lemma tauChainStatEq:
  fixes Ψ  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   P'  :: "('a, 'b, 'c) psi"
  and   Ψ' :: 'b

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' ⊳ P ==>^{^}_\<tau> P'"
using assms
by(auto simp add: rtrancl_eq_or_trancl intro: tauStepChainStatEq)

definition weakTransition :: "'b → ('a, 'b, 'c) psi → ('a, 'b, 'c) psi → 'a action → ('a, 'b, 'c) psi → bool" (‹_ : _ ⊳ _ ==>_ ≺ _› [80, 80, 80, 80, 80] 80)
where
  "Ψ : Q ⊳ P ==>α ≺ P' ≡ ∃P''. Ψ ⊳ P ==>^{^}_\<tau> P'' ∧ (insertAssertion (extractFrame Q) Ψ) ↪_F (insertAssertion (extractFrame P'') Ψ) ∧
                                          Ψ ⊳ P'' ⟼α ≺ P'"

lemma weakTransitionI:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   P''  :: "('a, 'b, 'c) psi"
  and   α   :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ P ==>^{^}_\<tau> P''"
  and     "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
  and     "Ψ ⊳ P'' ⟼α ≺ P'"

  shows "Ψ : Q ⊳ P ==>α ≺ P'"
using assms
by(auto simp add: weakTransition_def)

lemma weakTransitionE:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes "Ψ : Q ⊳ P ==>α ≺ P'"

  obtains P'' where "Ψ ⊳ P ==>^{^}_\<tau> P''" and "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                 and "Ψ ⊳ P'' ⟼α ≺ P'"
using assms
by(auto simp add: weakTransition_def)

lemma weakTransitionClosed[eqvt]:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"

  assumes "Ψ : Q ⊳ P ==>α ≺ P'"

  shows "(p ∙ Ψ) : (p ∙ Q) ⊳ (p ∙ P) ==>(p ∙ α)≺ (p ∙ P')"
proof -
  from assms obtain P'' where "Ψ ⊳ P ==>^{^}_\<tau> P''" and "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                           and "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from ‹Ψ ⊳ P ==>^{^}_\τ P''› have "(p ∙ Ψ) ⊳ (p ∙ P) ==>^{^}_\<tau> (p ∙ P'')"
    by(rule tauChainEqvt)
  moreover from ‹insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ›
  have "(p ∙ (insertAssertion (extractFrame Q) Ψ)) ↪_F (p ∙ (insertAssertion (extractFrame P'') Ψ))"
    by(rule FrameStatImpClosed)
  hence "insertAssertion (extractFrame(p ∙ Q)) (p ∙ Ψ) ↪_F insertAssertion (extractFrame(p ∙ P'')) (p ∙ Ψ)" by(simp add: eqvts)
  moreover from ‹Ψ ⊳ P'' ⟼α ≺ P'› have "(p ∙ Ψ) ⊳ (p ∙ P'') ⟼(p ∙ (α ≺ P'))"
    by(rule semantics.eqvt)
  hence "(p ∙ Ψ) ⊳ (p ∙ P'') ⟼(p ∙ α) ≺ (p ∙ P')" by(simp add: eqvts)
  ultimately show ?thesis by(rule weakTransitionI)
qed
(*
lemma weakTransitionAlpha:
  fixes \<Psi>   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"

  assumes PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'"
  and     S: "set p \<subseteq> set xvec \<times> set(p \<bullet> xvec)"
  and     "xvec \<sharp>* (p \<bullet> xvec)"
  and     "(p \<bullet> xvec) \<sharp>* P"
  and     "(p \<bullet> xvec) \<sharp>* N"

  shows "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> P')"
proof -
  from PTrans obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'') \<Psi>"
                           and P''Trans: "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'"
    by(rule weakTransitionE)

  note PChain QeqP''
  moreover from PChain `(p \<bullet> xvec) \<sharp>* P` have "(p \<bullet> xvec) \<sharp>* P''" by(rule tauChainFreshChain)
  with P''Trans `xvec \<sharp>* (p \<bullet> xvec)` `(p \<bullet> xvec) \<sharp>* N` have "(p \<bullet> xvec) \<sharp>* P'"
    by(force intro: outputFreshChainDerivative)
  with P''Trans S `(p \<bullet> xvec) \<sharp>* N` have "\<Psi> \<rhd> P'' \<longmapsto>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> P')"
    by(simp add: boundOutputChainAlpha'')
  ultimately show ?thesis by(rule weakTransitionI)
qed
*)
lemma weakOutputAlpha:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"

  assumes PTrans: "Ψ : Q ⊳ P ==>M(ν*(p ∙ xvec))⟨(p ∙ N)⟩ ≺ P'"
  and     S: "set p ⊆ set xvec × set(p ∙ xvec)"
  and     "distinctPerm p"
  and     "xvec ♯* P"
  and     "xvec ♯* (p ∙ xvec)"
  and     "(p ∙ xvec) ♯* M"
  and     "distinct xvec"

  shows "Ψ : Q ⊳ P ==>M(ν*xvec)⟨N⟩ ≺ (p ∙ P')"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼M(ν*(p ∙ xvec))⟨(p ∙ N)⟩ ≺ P'"
    by(rule weakTransitionE)


  note PChain QeqP''
  moreover from PChain ‹xvec ♯* P› have "xvec ♯* P''" by(rule tauChainFreshChain)
  with P''Trans ‹xvec ♯* (p ∙ xvec)› ‹distinct xvec› ‹(p ∙ xvec) ♯* M› have "xvec ♯* (p ∙ N)" and "xvec ♯* P'"
    by(force intro: outputFreshChainDerivative)+
  hence "(p ∙ xvec) ♯* (p ∙ p ∙ N)" and "(p ∙ xvec) ♯* (p ∙ P')"
    by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])+
  with ‹distinctPerm p› have "(p ∙ xvec) ♯* N" and "(p ∙ xvec) ♯* (p ∙ P')" by simp+
  with P''Trans S ‹distinctPerm p› have "Ψ ⊳ P'' ⟼M(ν*xvec)⟨N⟩ ≺ (p ∙ P')"
    apply(simp add: residualInject)
    by(subst boundOutputChainAlpha) auto
    
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakFreshDerivative:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   x    :: name

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and     "x ♯ P"
  and     "x ♯ α"
  and     "bn α ♯* subject α"
  and     "distinct(bn α)"

  shows "x ♯ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹x ♯ P› have "x ♯ P''" by(rule tauChainFresh)
  with P''Trans show "x ♯ P'" using ‹x ♯ α› ‹bn α ♯* subject α› ‹distinct(bn α)›
    by(force intro: freeFreshDerivative)
qed

lemma weakFreshChainDerivative:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   yvec :: "name list"

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and     "yvec ♯* P"
  and     "yvec ♯* α"
  and     "bn α ♯* subject α"
  and     "distinct(bn α)"

  shows "yvec ♯* P'"
using assms
by(induct yvec) (auto intro: weakFreshDerivative)

lemma weakInputFreshDerivative:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   x    :: name

  assumes PTrans: "Ψ : Q ⊳ P ==>M(N) ≺ P'"
  and     "x ♯ P"
  and     "x ♯ N"

  shows "x ♯ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and P''Trans: "Ψ ⊳ P'' ⟼M(N) ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹x ♯ P› have "x ♯ P''" by(rule tauChainFresh)
  with P''Trans show "x ♯ P'" using ‹x ♯ N›
    by(force intro: inputFreshDerivative)
qed

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

  assumes PTrans: "Ψ : Q ⊳ P ==>M(N) ≺ P'"
  and     "xvec ♯* P"
  and     "xvec ♯* N"

  shows "xvec ♯* P'"
using assms
by(induct xvec) (auto intro: weakInputFreshDerivative)

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

  assumes PTrans: "Ψ : Q ⊳ P ==>M(ν*xvec)⟨N⟩ ≺ P'"
  and     "x ♯ P"
  and     "x ♯ xvec"
  and     "xvec ♯* M"
  and     "distinct xvec"

  shows "x ♯ N"
  and   "x ♯ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and P''Trans: "Ψ ⊳ P'' ⟼M(ν*xvec)⟨N⟩ ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹x ♯ P› have "x ♯ P''" by(rule tauChainFresh)
  with P''Trans show "x ♯ N" and "x ♯ P'" using ‹x ♯ xvec› ‹xvec ♯* M› ‹distinct xvec›
    by(force intro: outputFreshDerivative)+
qed

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

  assumes PTrans: "Ψ : Q ⊳ P ==>M(ν*xvec)⟨N⟩ ≺ P'"
  and     "yvec ♯* P"
  and     "xvec ♯* yvec"
  and     "xvec ♯* M"
  and     "distinct xvec"

  shows "yvec ♯* N"
  and   "yvec ♯* P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and P''Trans: "Ψ ⊳ P'' ⟼M(ν*xvec)⟨N⟩ ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹yvec ♯* P› have "yvec ♯* P''" by(rule tauChainFreshChain)
  with P''Trans show "yvec ♯* N" and "yvec ♯* P'" using ‹xvec ♯* yvec› ‹xvec ♯* M› ‹distinct xvec›
    by(force intro: outputFreshChainDerivative)+
qed

lemma weakOutputPermSubject:
  fixes Ψ   :: 'b
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"
  and   zvec :: "name list"

  assumes PTrans: "Ψ : Q ⊳ P ==>M(ν*xvec)⟨N⟩ ≺ P'"
  and     S: "set p ⊆ set yvec × set zvec"
  and     "yvec ♯* Ψ"
  and     "zvec ♯* Ψ"
  and     "yvec ♯* P"
  and     "zvec ♯* P"

  shows "Ψ : Q ⊳ P ==>(p ∙ M)(ν*xvec)⟨N⟩ ≺ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ" 
                            and P''Trans: "Ψ ⊳ P'' ⟼M(ν*xvec)⟨N⟩ ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹yvec ♯* P› ‹zvec ♯* P› have "yvec ♯* P''" and "zvec ♯* P''"
    by(force intro: tauChainFreshChain)+

  note PChain QeqP''
  moreover from P''Trans S ‹yvec ♯* Ψ› ‹zvec ♯* Ψ› ‹yvec ♯* P''› ‹zvec ♯* P''› have "Ψ ⊳ P'' ⟼(p ∙ M)(ν*xvec)⟨N⟩ ≺ P'"
    by(rule_tac outputPermSubject) (assumption | auto)
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakInputPermSubject:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   N    :: 'a
  and   P'   :: "('a, 'b, 'c) psi"
  and   p    :: "name prm"
  and   yvec :: "name list"
  and   zvec :: "name list"

  assumes PTrans: "Ψ : Q ⊳ P ==>M(N) ≺ P'"
  and     S: "set p ⊆ set yvec × set zvec"
  and     "yvec ♯* Ψ"
  and     "zvec ♯* Ψ"
  and     "yvec ♯* P"
  and     "zvec ♯* P"

  shows "Ψ : Q ⊳ P ==>(p ∙ M)(N) ≺ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ" 
                            and P''Trans: "Ψ ⊳ P'' ⟼M(N) ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹yvec ♯* P› ‹zvec ♯* P› have "yvec ♯* P''" and "zvec ♯* P''"
    by(force intro: tauChainFreshChain)+

  note PChain QeqP''
  moreover from P''Trans S ‹yvec ♯* Ψ› ‹zvec ♯* Ψ› ‹yvec ♯* P''› ‹zvec ♯* P''› have "Ψ ⊳ P'' ⟼(p ∙ M)(N) ≺ P'"
    by(rule_tac inputPermSubject) auto
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakInput:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   K    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   Tvec :: "'a list"
  and   P    :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊨ M ↔ K"
  and     "distinct xvec" 
  and     "set xvec ⊆ supp N"
  and     "length xvec = length Tvec"
  and     QeqΨ: "insertAssertion (extractFrame Q) Ψ ↪_F ⟨ε, Ψ ⊗ 1⟩"

  shows "Ψ : Q ⊳ M(λ*xvec N).P ==>K((N[xvec::=Tvec])) ≺ P[xvec::=Tvec]"
proof -
  have "Ψ ⊳ M(λ*xvec N).P ==>^{^}_\<tau> M(λ*xvec N).P" by simp
  moreover from QeqΨ have "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame(M(λ*xvec N).P)) Ψ"
    by auto
  moreover from assms have "Ψ ⊳ M(λ*xvec N).P ⟼K((N[xvec::=Tvec])) ≺ P[xvec::=Tvec]"
    by(rule_tac Input)
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakOutput:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   K    :: 'a
  and   N    :: 'a
  and   P    :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊨ M ↔ K"
  and     QeqΨ: "insertAssertion (extractFrame Q) Ψ ↪_F ⟨ε, Ψ ⊗ 1⟩"

  shows "Ψ : Q ⊳ M⟨N⟩.P ==>K⟨N⟩ ≺ P"
proof -
  have "Ψ ⊳ M⟨N⟩.P ==>^{^}_\<tau> M⟨N⟩.P" by simp
  moreover from QeqΨ have "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame(M⟨N⟩.P)) Ψ"
    by auto
  moreover have "insertAssertion (extractFrame(M⟨N⟩.P)) Ψ ↪_F insertAssertion (extractFrame(M⟨N⟩.P)) Ψ" by simp
  moreover from ‹Ψ ⊨ M ↔ K› have "Ψ ⊳ M⟨N⟩.P ⟼K⟨N⟩ ≺ P"
    by(rule Output)
  ultimately show ?thesis by(rule_tac weakTransitionI) auto
qed

lemma insertGuardedAssertion:
  fixes P :: "('a, 'b, 'c) psi"

  assumes "guarded P"

  shows "insertAssertion(extractFrame P) Ψ ≃_F ⟨ε, Ψ ⊗ 1⟩"
proof -
  obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* Ψ" by(rule freshFrame)
  from ‹guarded P› FrP have "Ψ_P ≃ 1" and "supp Ψ_P = ({}::name set)"
    by(blast dest: guardedStatEq)+
  
  from FrP ‹A_P ♯* Ψ› ‹Ψ_P ≃ 1› have "insertAssertion(extractFrame P) Ψ ≃_F ⟨A_P, Ψ ⊗ 1⟩"
    by simp (metis frameIntCompositionSym)
  moreover from ‹A_P ♯* Ψ› have "⟨A_P, Ψ ⊗ 1⟩ ≃_F ⟨ε, Ψ ⊗ 1⟩"
    by(rule_tac frameResFreshChain) auto
  ultimately show ?thesis by(rule FrameStatEqTrans)
qed
  
lemma weakCase:
  fixes Ψ   :: 'b 
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and     "(φ, P) mem CsP"
  and     "Ψ ⊨ φ"
  and     "guarded P"
  and     RImpQ: "insertAssertion (extractFrame R) Ψ ↪_F insertAssertion (extractFrame Q) Ψ"
  and     ImpR: "insertAssertion (extractFrame R) Ψ ↪_F ⟨ε, Ψ⟩"

  shows "Ψ : R ⊳ Cases CsP ==>α ≺ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''"
                           and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)
  show ?thesis
  proof(case_tac "P = P''")
    assume "P = P''"
    have "Ψ ⊳ Cases CsP ==>^{^}_\<tau> Cases CsP" by simp
    moreover from ImpR AssertionStatEq_def have "insertAssertion(extractFrame R) Ψ ↪_F insertAssertion(extractFrame(Cases CsP)) Ψ"
      by(rule_tac FrameStatImpTrans) (auto intro: Identity)+

    moreover from P''Trans ‹(φ, P) mem CsP› ‹Ψ ⊨ φ› ‹guarded P› ‹P = P''› have "Ψ ⊳ Cases CsP ⟼α ≺ P'"
      by(blast intro: Case)
    ultimately show ?thesis
      by(rule weakTransitionI)
  next
    assume "P ≠ P''"
    with PChain have "Ψ ⊳ P ==>_\<tau> P''" by(simp add: rtrancl_eq_or_trancl)
    hence "Ψ ⊳ Cases CsP ==>_\<tau> P''" using ‹(φ, P) mem CsP› ‹Ψ ⊨ φ› ‹guarded P›
      by(rule tauStepChainCase)
    hence "Ψ ⊳ Cases CsP ==>^{^}_\<tau> P''" by simp
    moreover from RImpQ QeqP'' have "insertAssertion(extractFrame R) Ψ ↪_F insertAssertion(extractFrame P'') Ψ"
      by(rule FrameStatImpTrans)
    ultimately show ?thesis using P''Trans by(rule weakTransitionI)
  qed
qed

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

  assumes PTrans: "Ψ : Q ⊳ P ==>M(ν*(xvec@yvec))⟨N⟩ ≺ P'"
  and     "x ∈ supp N"
  and     "x ♯ Ψ"
  and     "x ♯ M"
  and     "x ♯ xvec"
  and     "x ♯ yvec"

  shows "Ψ : (νx)Q ⊳ (νx)P ==>M(ν*(xvec@x#yvec))⟨N⟩ ≺ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼M(ν*(xvec@yvec))⟨N⟩ ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹x ♯ Ψ› have "Ψ ⊳ (νx)P ==>^{^}_\<tau> (νx)P''" by(rule tauChainResPres)
  moreover from QeqP'' ‹x ♯ Ψ› have "insertAssertion (extractFrame((νx)Q)) Ψ ↪_F insertAssertion (extractFrame((νx)P'')) Ψ" by(force intro: frameImpResPres)
  moreover from P''Trans ‹x ∈ supp N› ‹x ♯ Ψ› ‹x ♯ M› ‹x ♯ xvec› ‹x ♯ yvec› have "Ψ ⊳ (νx)P'' ⟼M(ν*(xvec@x#yvec))⟨N⟩ ≺ P'"
    by(rule Open)
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakScope:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and     "x ♯ Ψ"
  and     "x ♯ α"

  shows "Ψ : (νx)Q ⊳ (νx)P ==>α ≺ (νx)P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹x ♯ Ψ› have "Ψ ⊳ (νx)P ==>^{^}_\<tau> (νx)P''" by(rule tauChainResPres)
  moreover from QeqP'' ‹x ♯ Ψ› have "insertAssertion (extractFrame((νx)Q)) Ψ ↪_F insertAssertion (extractFrame((νx)P'')) Ψ" by(force intro: frameImpResPres)
  moreover from P''Trans ‹x ♯ Ψ› ‹x ♯ α› have "Ψ ⊳ (νx)P'' ⟼α ≺ (νx)P'"
    by(rule Scope)
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakPar1:
  fixes Ψ   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   A_Q   :: "name list"
  and   Ψ_Q   :: 'b

  assumes PTrans: "Ψ ⊗ Ψ_Q : R ⊳ P ==>α ≺ P'"
  and     FrQ: "extractFrame Q = ⟨A_Q, Ψ_Q⟩"
  and     "bn α ♯* Q"
  and     "A_Q ♯* Ψ"
  and     "A_Q ♯* P"
  and     "A_Q ♯* α"
  and     "A_Q ♯* R"

  shows "Ψ : R ∥ Q ⊳ P ∥ Q ==>α ≺ P' ∥ Q"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ_Q ⊳ P ==>^{^}_\<tau> P''"
                           and ReqP'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ_Q) ↪_F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ_Q)"
                           and P''Trans: "Ψ ⊗ Ψ_Q ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹A_Q ♯* P› have "A_Q ♯* P''" by(rule tauChainFreshChain)
  from PChain FrQ ‹A_Q ♯* Ψ› ‹A_Q ♯* P› have "Ψ ⊳ P ∥ Q ==>^{^}_\<tau> P'' ∥ Q" by(rule tauChainPar1)
  moreover have "insertAssertion (extractFrame(R ∥ Q)) Ψ ↪_F insertAssertion (extractFrame(P'' ∥ Q)) Ψ"
  proof -
    obtain A_R Ψ_R where FrR: "extractFrame R = ⟨A_R, Ψ_R⟩" and "A_R ♯* A_Q" and "A_R ♯* Ψ_Q" and "A_R ♯* Ψ"
      by(rule_tac C="(A_Q, Ψ_Q, Ψ)" in freshFrame) auto
    obtain A_P'' Ψ_P'' where FrP'': "extractFrame P'' = ⟨A_P'', Ψ_P''⟩" and "A_P'' ♯* A_Q" and "A_P'' ♯* Ψ_Q" and "A_P'' ♯* Ψ"
      by(rule_tac C="(A_Q, Ψ_Q, Ψ)" in freshFrame) auto

    from FrR FrP'' ‹A_Q ♯* R› ‹A_Q ♯* P''› ‹A_R ♯* A_Q› ‹A_P'' ♯* A_Q› have "A_Q ♯* Ψ_R" and "A_Q ♯* Ψ_P''"
      by(force dest: extractFrameFreshChain)+
    have "⟨A_R, Ψ ⊗ Ψ_R ⊗ Ψ_Q⟩ ≃_F ⟨A_R, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
    moreover from ReqP'' FrR FrP'' ‹A_R ♯* Ψ› ‹A_R ♯* Ψ_Q› ‹A_P'' ♯* Ψ› ‹A_P'' ♯* Ψ_Q›
    have "⟨A_R, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ↪_F ⟨A_P'', (Ψ ⊗ Ψ_Q) ⊗ Ψ_P''⟩" using freshCompChain by auto
    moreover have "⟨A_P'', (Ψ ⊗ Ψ_Q) ⊗ Ψ_P''⟩ ≃_F ⟨A_P'', Ψ ⊗ Ψ_P'' ⊗ Ψ_Q⟩"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
    ultimately have "⟨A_R, Ψ ⊗ Ψ_R ⊗ Ψ_Q⟩ ↪_F ⟨A_P'', Ψ ⊗ Ψ_P'' ⊗ Ψ_Q⟩"
      by(force dest: FrameStatImpTrans simp add: FrameStatEq_def)

    hence "⟨(A_R@A_Q), Ψ ⊗ Ψ_R ⊗ Ψ_Q⟩ ↪_F ⟨(A_P''@A_Q), Ψ ⊗ Ψ_P'' ⊗ Ψ_Q⟩"
      apply(simp add: frameChainAppend)
      apply(drule_tac xvec=A_Q in frameImpResChainPres)
      by(metis frameImpChainComm FrameStatImpTrans)
    with FrR FrQ FrP'' ‹A_R ♯* A_Q› ‹A_R ♯* Ψ_Q› ‹A_Q ♯* Ψ_R› ‹A_P'' ♯* A_Q› ‹A_P'' ♯* Ψ_Q› ‹A_Q ♯* Ψ_P''› ‹A_R ♯* Ψ› ‹A_P'' ♯* Ψ› ‹A_Q ♯* Ψ› ReqP''
    show ?thesis by simp
  qed
  moreover from P''Trans FrQ ‹bn α ♯* Q› ‹A_Q ♯* Ψ› ‹A_Q ♯* P''› ‹A_Q ♯* α› have "Ψ ⊳ P'' ∥ Q ⟼α ≺ (P' ∥ Q)"
    by(rule Par1)  
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakPar2:
  fixes Ψ   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   M    :: 'a
  and   xvec :: "name list"
  and   N    :: 'a
  and   Q'   :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   A_P   :: "name list"
  and   Ψ_P  :: 'b

  assumes QTrans: "Ψ ⊗ Ψ_P : R ⊳ Q ==>α ≺ Q'"
  and     FrP: "extractFrame P = ⟨A_P, Ψ_P⟩"
  and     "bn α ♯* P"
  and     "A_P ♯* Ψ"
  and     "A_P ♯* Q"
  and     "A_P ♯* α"
  and     "A_P ♯* R"

  shows "Ψ : P ∥ R ⊳ P ∥ Q ==>α ≺ P ∥ Q'"
proof -
  from QTrans obtain Q'' where QChain: "Ψ ⊗ Ψ_P ⊳ Q ==>^{^}_\<tau> Q''"
                           and ReqQ'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ_P) ↪_F insertAssertion (extractFrame Q'') (Ψ ⊗ Ψ_P)"
                           and Q''Trans: "Ψ ⊗ Ψ_P ⊳ Q'' ⟼α ≺ Q'"
    by(rule weakTransitionE)

  from QChain ‹A_P ♯* Q› have "A_P ♯* Q''" by(rule tauChainFreshChain)

  from QChain FrP ‹A_P ♯* Ψ› ‹A_P ♯* Q› have "Ψ ⊳ P ∥ Q ==>^{^}_\<tau> P ∥ Q''" by(rule tauChainPar2)
  moreover have "insertAssertion (extractFrame(P ∥ R)) Ψ ↪_F insertAssertion (extractFrame(P ∥ Q'')) Ψ"
  proof -
    obtain A_R Ψ_R where FrR: "extractFrame R = ⟨A_R, Ψ_R⟩" and "A_R ♯* A_P" and "A_R ♯* Ψ_P" and "A_R ♯* Ψ"
      by(rule_tac C="(A_P, Ψ_P, Ψ)" in freshFrame) auto
    obtain A_Q'' Ψ_Q'' where FrQ'': "extractFrame Q'' = ⟨A_Q'', Ψ_Q''⟩" and "A_Q'' ♯* A_P" and "A_Q'' ♯* Ψ_P" and "A_Q'' ♯* Ψ"
      by(rule_tac C="(A_P, Ψ_P, Ψ)" in freshFrame) auto

    from FrR FrQ'' ‹A_P ♯* R› ‹A_P ♯* Q''› ‹A_R ♯* A_P› ‹A_Q'' ♯* A_P› have "A_P ♯* Ψ_R" and "A_P ♯* Ψ_Q''"
      by(force dest: extractFrameFreshChain)+
    have "⟨A_R, Ψ ⊗ Ψ_P ⊗ Ψ_R⟩ ≃_F ⟨A_R, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)

    moreover from ReqQ'' FrR FrQ'' ‹A_R ♯* Ψ› ‹A_R ♯* Ψ_P› ‹A_Q'' ♯* Ψ› ‹A_Q'' ♯* Ψ_P›
    have "⟨A_R, (Ψ ⊗ Ψ_P) ⊗ Ψ_R⟩ ↪_F ⟨A_Q'', (Ψ ⊗ Ψ_P) ⊗ Ψ_Q''⟩" using freshCompChain by simp
    moreover have "⟨A_Q'', (Ψ ⊗ Ψ_P) ⊗ Ψ_Q''⟩ ≃_F ⟨A_Q'', Ψ ⊗ Ψ_P ⊗ Ψ_Q''⟩"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
    ultimately have "⟨A_R, Ψ ⊗ Ψ_P ⊗ Ψ_R⟩ ↪_F ⟨A_Q'', Ψ ⊗ Ψ_P ⊗ Ψ_Q''⟩"
      by(force dest: FrameStatImpTrans simp add: FrameStatEq_def)
    hence "⟨(A_P@A_R), Ψ ⊗ Ψ_P ⊗ Ψ_R⟩ ↪_F ⟨(A_P@A_Q''), Ψ ⊗ Ψ_P ⊗ Ψ_Q''⟩"
      apply(simp add: frameChainAppend)
      apply(drule_tac xvec=A_P in frameImpResChainPres)
      by(metis frameImpChainComm FrameStatImpTrans)
    with FrR FrP FrQ'' ‹A_R ♯* A_P› ‹A_R ♯* Ψ_P› ‹A_P ♯* Ψ_R› ‹A_Q'' ♯* A_P› ‹A_Q'' ♯* Ψ_P› ‹A_P ♯* Ψ_Q''› ‹A_R ♯* Ψ› ‹A_Q'' ♯* Ψ› ‹A_P ♯* Ψ› ReqQ''
    show ?thesis by simp
  qed
  moreover from Q''Trans FrP ‹bn α ♯* P› ‹A_P ♯* Ψ› ‹A_P ♯* Q''› ‹A_P ♯* α› have "Ψ ⊳ P ∥ Q'' ⟼α ≺ (P ∥ Q')"
    by(rule_tac Par2) auto
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma weakComm1:
  fixes Ψ   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   A_Q   :: "name list"
  and   Ψ_Q   :: 'b

  assumes PTrans: "Ψ ⊗ Ψ_Q : R ⊳ P ==>M(N) ≺ P'"
  and     FrR: "extractFrame R = ⟨A_R, Ψ_R⟩"
  and     QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼K(ν*xvec)⟨N⟩ ≺ Q'"
  and     FrQ: "extractFrame Q = ⟨A_Q, Ψ_Q⟩"
  and     MeqK: "Ψ ⊗ Ψ_R ⊗ Ψ_Q ⊨ M ↔ K"
  and     "A_R ♯* Ψ"
  and     "A_R ♯* P"
  and     "A_R ♯* Q"
  and     "A_R ♯* R"
  and     "A_R ♯* M"
  and     "A_R ♯* A_Q"
  and     "A_Q ♯* Ψ"
  and     "A_Q ♯* P"
  and     "A_Q ♯* Q"
  and     "A_Q ♯* R"
  and     "A_Q ♯* K"
  and     "xvec ♯* P"

  shows "Ψ ⊳ P ∥ Q ==>_\<tau> ((ν*xvec)(P' ∥ Q'))"
proof -
  from ‹extractFrame Q = ⟨A_Q, Ψ_Q⟩› ‹A_Q ♯* Ψ› ‹A_Q ♯* P› ‹A_Q ♯* Q› ‹A_Q ♯* R› ‹A_Q ♯* K› ‹A_R ♯* A_Q›
  obtain A_Q' where FrQ': "extractFrame Q = ⟨A_Q', Ψ_Q⟩" and "distinct A_Q'" and "A_Q' ♯* Ψ" and "A_Q' ♯* P" 
               and "A_Q' ♯* Q" and "A_Q' ♯* R" and "A_Q' ♯* K" and "A_R ♯* A_Q'"
    by(rule_tac C="(Ψ, P, Q, R, K, A_R)" in distinctFrame) auto

  from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ_Q ⊳ P ==>^{^}_\<tau> P''"
                           and RimpP'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ_Q) ↪_F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ_Q)"
                           and P''Trans: "Ψ ⊗ Ψ_Q ⊳ P'' ⟼M(N) ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹A_Q' ♯* P› have "A_Q' ♯* P''" by(rule tauChainFreshChain)
  obtain A_P'' Ψ_P'' where FrP'': "extractFrame P'' = ⟨A_P'', Ψ_P''⟩" and "A_P'' ♯* (Ψ, A_Q', Ψ_Q, A_R, Ψ_R, M, N, K, R, Q, P'', xvec)" and "distinct A_P''"
    by(rule freshFrame)
  hence "A_P'' ♯* Ψ" and "A_P'' ♯* A_Q'" and "A_P'' ♯* Ψ_Q" and "A_P'' ♯* M" and "A_P'' ♯* R" and "A_P'' ♯* Q"
    and "A_P'' ♯* N" and "A_P'' ♯* K" and "A_P'' ♯* A_R" and "A_P'' ♯* P''" and "A_P'' ♯* xvec" and "A_P'' ♯* Ψ_R"
    by simp+
  from FrR ‹A_R ♯* A_Q'› ‹A_Q' ♯* R› have "A_Q' ♯* Ψ_R" by(drule_tac extractFrameFreshChain) auto
  from FrQ' ‹A_R ♯* A_Q'› ‹A_R ♯* Q› have "A_R ♯* Ψ_Q" by(drule_tac extractFrameFreshChain) auto
  from PChain ‹xvec ♯* P› have "xvec ♯* P''" by(force intro: tauChainFreshChain)+

  have "⟨A_R, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩ ≃_F ⟨A_R, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩" 
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  moreover with RimpP'' FrP'' FrR ‹A_P'' ♯* Ψ› ‹A_R ♯* Ψ› ‹A_P'' ♯* Ψ_Q› ‹A_R ♯* Ψ_Q›
  have "⟨A_R, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ↪_F ⟨A_P'', (Ψ ⊗ Ψ_Q) ⊗ Ψ_P''⟩" using freshCompChain
    by(simp add: freshChainSimps)
  moreover have "⟨A_P'', (Ψ ⊗ Ψ_Q) ⊗ Ψ_P''⟩ ≃_F ⟨A_P'', (Ψ ⊗ Ψ_P'') ⊗ Ψ_Q⟩"
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  ultimately have RImpP'': "⟨A_R, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩ ↪_F ⟨A_P'', (Ψ ⊗ Ψ_P'') ⊗ Ψ_Q⟩"
    by(rule FrameStatEqImpCompose)
      
  from PChain FrQ' ‹A_Q' ♯* Ψ› ‹A_Q' ♯* P› have "Ψ ⊳ P ∥ Q ==>^{^}_\<tau> P'' ∥ Q" by(rule tauChainPar1)
  moreover from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' ‹distinct A_P''› ‹distinct A_Q'› ‹A_P'' ♯* A_Q'› ‹A_R ♯* A_Q'›
        ‹A_Q' ♯* Ψ› ‹A_Q' ♯* P''› ‹A_Q' ♯* Q› ‹A_Q' ♯* R› ‹A_Q' ♯* K› ‹A_P'' ♯* Ψ› ‹A_P'' ♯* R› ‹A_P'' ♯* Q›
        ‹A_P'' ♯* P''› ‹A_P'' ♯* M› ‹A_Q ♯* R› ‹A_R ♯* Q› ‹A_R ♯* M›
  obtain K' where "Ψ ⊗ Ψ_P'' ⊳ Q ⟼K'(ν*xvec)⟨N⟩ ≺ Q'" and "Ψ ⊗ Ψ_P'' ⊗ Ψ_Q ⊨ M ↔ K'" and "A_Q' ♯* K'"
    by(rule_tac comm1Aux) (assumption | simp)+
  with P''Trans FrP'' have "Ψ ⊳ P'' ∥ Q ⟼τ ≺ (ν*xvec)(P' ∥ Q')" using FrQ' ‹A_Q' ♯* Ψ› ‹A_Q' ♯* P''› ‹A_Q' ♯* Q›
    ‹xvec ♯* P''› ‹A_P'' ♯* Ψ› ‹A_P'' ♯* P''› ‹A_P'' ♯* Q› ‹A_P'' ♯* M›  ‹A_P'' ♯* A_Q'›
    by(rule_tac Comm1)
  ultimately show ?thesis
    by(drule_tac tauActTauStepChain) auto
qed

lemma weakComm2:
  fixes Ψ   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"
  and   A_Q   :: "name list"
  and   Ψ_Q   :: 'b

  assumes PTrans: "Ψ ⊗ Ψ_Q : R ⊳ P ==>M(ν*xvec)⟨N⟩ ≺ P'"
  and     FrR: "extractFrame R = ⟨A_R, Ψ_R⟩"
  and     QTrans: "Ψ ⊗ Ψ_R ⊳ Q ⟼K(N) ≺ Q'"
  and     FrQ: "extractFrame Q = ⟨A_Q, Ψ_Q⟩"
  and     MeqK: "Ψ ⊗ Ψ_R ⊗ Ψ_Q ⊨ M ↔ K"
  and     "A_R ♯* Ψ"
  and     "A_R ♯* P"
  and     "A_R ♯* Q"
  and     "A_R ♯* R"
  and     "A_R ♯* M"
  and     "A_R ♯* A_Q"
  and     "A_Q ♯* Ψ"
  and     "A_Q ♯* P"
  and     "A_Q ♯* Q"
  and     "A_Q ♯* R"
  and     "A_Q ♯* K"
  and     "xvec ♯* Q"
  and     "xvec ♯* M"
  and     "xvec ♯* A_Q"
  and     "xvec ♯* A_R"

  shows "Ψ ⊳ P ∥ Q ==>_\<tau> ((ν*xvec)(P' ∥ Q'))"
proof -
  from ‹extractFrame Q = ⟨A_Q, Ψ_Q⟩› ‹A_Q ♯* Ψ› ‹A_Q ♯* P› ‹A_Q ♯* Q› ‹A_Q ♯* R› ‹A_Q ♯* K› ‹A_R ♯* A_Q› ‹xvec ♯* A_Q›
  obtain A_Q' where FrQ': "extractFrame Q = ⟨A_Q', Ψ_Q⟩" and "distinct A_Q'" and "A_Q' ♯* Ψ" and "A_Q' ♯* P" 
               and "A_Q' ♯* Q" and "A_Q' ♯* R" and "A_Q' ♯* K" and "A_R ♯* A_Q'" and "A_Q' ♯* xvec"
    by(rule_tac C="(Ψ, P, Q, R, K, A_R, xvec)" in distinctFrame) auto

  from PTrans obtain P'' where PChain: "Ψ ⊗ Ψ_Q ⊳ P ==>^{^}_\<tau> P''"
                           and RimpP'': "insertAssertion (extractFrame R) (Ψ ⊗ Ψ_Q) ↪_F insertAssertion (extractFrame P'') (Ψ ⊗ Ψ_Q)"
                           and P''Trans: "Ψ ⊗ Ψ_Q ⊳ P'' ⟼M(ν*xvec)⟨N⟩ ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹A_Q' ♯* P› have "A_Q' ♯* P''" by(rule tauChainFreshChain)
  obtain A_P'' Ψ_P'' where FrP'': "extractFrame P'' = ⟨A_P'', Ψ_P''⟩" and "A_P'' ♯* (Ψ, A_Q', Ψ_Q, A_R, Ψ_R, M, N, K, R, Q, P'', xvec)" and "distinct A_P''"
    by(rule freshFrame)
  hence "A_P'' ♯* Ψ" and "A_P'' ♯* A_Q'" and "A_P'' ♯* Ψ_Q" and "A_P'' ♯* M" and "A_P'' ♯* R" and "A_P'' ♯* Q"
    and "A_P'' ♯* N" and "A_P'' ♯* K" and "A_P'' ♯* A_R" and "A_P'' ♯* P''" and "A_P'' ♯* xvec" and "A_P'' ♯* Ψ_R"
    by simp+
  from FrR ‹A_R ♯* A_Q'› ‹A_Q' ♯* R› have "A_Q' ♯* Ψ_R" by(drule_tac extractFrameFreshChain) auto
  from FrQ' ‹A_R ♯* A_Q'› ‹A_R ♯* Q› have "A_R ♯* Ψ_Q" by(drule_tac extractFrameFreshChain) auto

  have "⟨A_R, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩ ≃_F ⟨A_R, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩" 
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  moreover with RimpP'' FrP'' FrR ‹A_P'' ♯* Ψ› ‹A_R ♯* Ψ› ‹A_P'' ♯* Ψ_Q› ‹A_R ♯* Ψ_Q›
  have "⟨A_R, (Ψ ⊗ Ψ_Q) ⊗ Ψ_R⟩ ↪_F ⟨A_P'', (Ψ ⊗ Ψ_Q) ⊗ Ψ_P''⟩" using freshCompChain
    by(simp add: freshChainSimps)
  moreover have "⟨A_P'', (Ψ ⊗ Ψ_Q) ⊗ Ψ_P''⟩ ≃_F ⟨A_P'', (Ψ ⊗ Ψ_P'') ⊗ Ψ_Q⟩"
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  ultimately have RImpP'': "⟨A_R, (Ψ ⊗ Ψ_R) ⊗ Ψ_Q⟩ ↪_F ⟨A_P'', (Ψ ⊗ Ψ_P'') ⊗ Ψ_Q⟩"
    by(rule FrameStatEqImpCompose)
      
  from PChain FrQ' ‹A_Q' ♯* Ψ› ‹A_Q' ♯* P› have "Ψ ⊳ P ∥ Q ==>^{^}_\<tau> P'' ∥ Q" by(rule tauChainPar1)
  moreover from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' ‹distinct A_P''› ‹distinct A_Q'› ‹A_P'' ♯* A_Q'› ‹A_R ♯* A_Q'›
        ‹A_Q' ♯* Ψ› ‹A_Q' ♯* P''› ‹A_Q' ♯* Q› ‹A_Q' ♯* R› ‹A_Q' ♯* K› ‹A_P'' ♯* Ψ› ‹A_P'' ♯* R› ‹A_P'' ♯* Q›
        ‹A_P'' ♯* P''› ‹A_P'' ♯* M› ‹A_Q ♯* R› ‹A_R ♯* Q› ‹A_R ♯* M› ‹xvec ♯* A_R› ‹xvec ♯* M› ‹A_Q' ♯* xvec›
  obtain K' where "Ψ ⊗ Ψ_P'' ⊳ Q ⟼K'(N) ≺ Q'" and "Ψ ⊗ Ψ_P'' ⊗ Ψ_Q ⊨ M ↔ K'" and "A_Q' ♯* K'"
    by(rule_tac comm2Aux) (assumption | simp)+
  with P''Trans FrP'' have "Ψ ⊳ P'' ∥ Q ⟼τ ≺ (ν*xvec)(P' ∥ Q')" using FrQ' ‹A_Q' ♯* Ψ› ‹A_Q' ♯* P''› ‹A_Q' ♯* Q›
    ‹xvec ♯* Q› ‹A_P'' ♯* Ψ› ‹A_P'' ♯* P''› ‹A_P'' ♯* Q› ‹A_P'' ♯* M›  ‹A_P'' ♯* A_Q'›
    by(rule_tac Comm2)
  ultimately show ?thesis
    by(drule_tac tauActTauStepChain) auto
qed

lemma frameImpIntComposition:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   A_F :: "name list"
  and   Ψ_F :: 'b

  assumes "Ψ ≃ Ψ'"

  shows "⟨A_F, Ψ ⊗ Ψ_F⟩ ↪_F ⟨A_F, Ψ' ⊗ Ψ_F⟩"
proof -
  from assms have "⟨A_F, Ψ ⊗ Ψ_F⟩ ≃_F ⟨A_F, Ψ' ⊗ Ψ_F⟩" by(rule frameIntComposition)
  thus ?thesis by(simp add: FrameStatEq_def)
qed

lemma insertAssertionStatImp:
  fixes F  :: "'b frame"
  and   Ψ  :: 'b
  and   G  :: "'b frame"
  and   Ψ' :: 'b

  assumes FeqG: "insertAssertion F Ψ ↪_F insertAssertion G Ψ"
  and     "Ψ ≃ Ψ'"

  shows "insertAssertion F Ψ' ↪_F insertAssertion G Ψ'"
proof -
  obtain A_F Ψ_F where FrF: "F = ⟨A_F, Ψ_F⟩" and "A_F ♯* Ψ" and "A_F ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
  obtain A_G Ψ_G where FrG: "G = ⟨A_G, Ψ_G⟩" and "A_G ♯* Ψ" and "A_G ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto

  from ‹Ψ ≃ Ψ'› have "⟨A_F, Ψ' ⊗ Ψ_F⟩ ≃_F ⟨A_F, Ψ ⊗ Ψ_F⟩" by (metis frameIntComposition FrameStatEqSym)
  moreover from ‹Ψ ≃ Ψ'› have "⟨A_G, Ψ ⊗ Ψ_G⟩ ≃_F ⟨A_G, Ψ' ⊗ Ψ_G⟩" by(rule frameIntComposition)
  ultimately have "⟨A_F, Ψ' ⊗ Ψ_F⟩ ↪_F ⟨A_G, Ψ' ⊗ Ψ_G⟩" using FeqG FrF FrG ‹A_F ♯* Ψ› ‹A_G ♯* Ψ› ‹Ψ ≃ Ψ'›
    by(force simp add: FrameStatEq_def dest: FrameStatImpTrans)
  with FrF FrG ‹A_F ♯* Ψ'› ‹A_G ♯* Ψ'› show ?thesis by simp
qed

lemma insertAssertionStatEq:
  fixes F  :: "'b frame"
  and   Ψ  :: 'b
  and   G  :: "'b frame"
  and   Ψ' :: 'b

  assumes FeqG: "insertAssertion F Ψ ≃_F insertAssertion G Ψ"
  and     "Ψ ≃ Ψ'"

  shows "insertAssertion F Ψ' ≃_F insertAssertion G Ψ'"
proof -
  obtain A_F Ψ_F where FrF: "F = ⟨A_F, Ψ_F⟩" and "A_F ♯* Ψ" and "A_F ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
  obtain A_G Ψ_G where FrG: "G = ⟨A_G, Ψ_G⟩" and "A_G ♯* Ψ" and "A_G ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto

  from FeqG FrF FrG ‹A_F ♯* Ψ› ‹A_G ♯* Ψ› ‹Ψ ≃ Ψ'›
  have "⟨A_F, Ψ' ⊗ Ψ_F⟩ ≃_F ⟨A_G, Ψ' ⊗ Ψ_G⟩"
    by simp (metis frameIntComposition FrameStatEqTrans FrameStatEqSym)
  with FrF FrG ‹A_F ♯* Ψ'› ‹A_G ♯* Ψ'› show ?thesis by simp
qed

lemma weakTransitionStatEq:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Ψ'  :: 'b

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' : Q ⊳ P ==>α ≺ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P''"
                           and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P ==>^{^}_\<tau> P''" by(rule tauChainStatEq)
  moreover from QeqP'' ‹Ψ ≃ Ψ'› have "insertAssertion (extractFrame Q) Ψ' ↪_F insertAssertion (extractFrame P'') Ψ'"
    by(rule insertAssertionStatImp)
  moreover from P''Trans ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P'' ⟼α ≺ P'"
    by(rule statEqTransition)
  ultimately show ?thesis by(rule weakTransitionI)
qed

lemma transitionWeakTransition:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  
  assumes "Ψ ⊳ P ⟼α ≺ P'"
  and     "insertAssertion(extractFrame Q) Ψ ↪_F insertAssertion(extractFrame P) Ψ"

  shows "Ψ : Q ⊳ P ==>α ≺ P'"
using assms
by(fastforce intro: weakTransitionI)

lemma weakPar1Guarded:
  fixes Ψ  :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"

  assumes PTrans: "Ψ : R ⊳ P ==>α ≺ P'"
  and     "bn α ♯* Q"
  and     "guarded Q"

  shows "Ψ : (R ∥ Q) ⊳ P ∥ Q ==>α ≺ P' ∥ Q"
proof -
  obtain A_Q Ψ_Q where FrQ: "extractFrame Q = ⟨A_Q, Ψ_Q⟩" and "A_Q ♯* Ψ" and "A_Q ♯* P" and "A_Q ♯* α" and "A_Q ♯* R"
    by(rule_tac C="(Ψ, P, α, R)" in freshFrame) auto
  from ‹guarded Q› FrQ have "Ψ_Q ≃ 1" by(blast dest: guardedStatEq)
  with PTrans have "Ψ ⊗ Ψ_Q : R ⊳ P ==>α ≺ P'" by(metis weakTransitionStatEq Identity AssertionStatEqSym compositionSym)
  thus ?thesis using FrQ ‹bn α ♯* Q› ‹A_Q ♯* Ψ› ‹A_Q ♯* P› ‹A_Q ♯* α› ‹A_Q ♯* R›
    by(rule weakPar1)
qed

lemma weakBang:
  fixes Ψ   :: 'b
  and   R    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   Q    :: "('a, 'b, 'c) psi"

  assumes PTrans: "Ψ : R ⊳ P ∥ !P ==>α ≺ P'"
  and     "guarded P"

  shows "Ψ : R ⊳ !P ==>α ≺ P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ∥ !P ==>^{^}_\<tau> P''"
                           and RImpP'': "insertAssertion(extractFrame R) Ψ ↪_F insertAssertion(extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)
  moreover obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" and "A_P ♯* Ψ" by(rule freshFrame)
  moreover from ‹guarded P› FrP have "Ψ_P ≃ 1" by(blast dest: guardedStatEq)
  ultimately show ?thesis
  proof(auto simp add: rtrancl_eq_or_trancl)
    have "Ψ ⊳ !P ==>^{^}_\<tau> !P" by simp
    moreover assume RimpP: "insertAssertion(extractFrame R) Ψ ↪_F ⟨A_P, Ψ ⊗ Ψ_P ⊗ 1⟩"
    have "insertAssertion(extractFrame R) Ψ ↪_F insertAssertion(extractFrame(!P)) Ψ"
    proof -
      from ‹Ψ_P ≃ 1› have "⟨A_P, Ψ ⊗ Ψ_P ⊗ 1⟩ ≃_F ⟨A_P, Ψ ⊗ 1⟩"
        by(metis frameIntCompositionSym frameIntAssociativity frameIntCommutativity frameIntIdentity FrameStatEqTrans FrameStatEqSym)
      moreover from ‹A_P ♯* Ψ› have "⟨A_P, Ψ ⊗ 1⟩ ≃_F ⟨ε, Ψ ⊗ 1⟩"
        by(force intro: frameResFreshChain)
      ultimately show ?thesis using RimpP by(auto simp add: FrameStatEq_def dest: FrameStatImpTrans)
    qed
    moreover assume "Ψ ⊳ P ∥ !P ⟼α ≺ P'"
    hence "Ψ ⊳ !P ⟼α ≺ P'" using ‹guarded P› by(rule Bang)
   ultimately show ?thesis by(rule weakTransitionI)
  next
    fix P'''
    assume "Ψ ⊳ P ∥ !P ==>_\<tau> P''"
    hence "Ψ ⊳ !P ==>_\<tau> P''" using ‹guarded P› by(rule tauStepChainBang)
    hence "Ψ ⊳ !P ==>^{^}_\<tau> P''" by simp
    moreover assume "insertAssertion(extractFrame R) Ψ ↪_F insertAssertion(extractFrame P'') Ψ"
                and "Ψ ⊳ P'' ⟼α ≺ P'"
    ultimately show ?thesis by(rule weakTransitionI)
  qed
qed

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

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and             "insertAssertion(extractFrame R) Ψ ↪_F insertAssertion(extractFrame Q) Ψ"

  shows "Ψ : R ⊳ P ==>α ≺ P'"
using assms
by(auto simp add: weakTransition_def intro: FrameStatImpTrans)

lemma guardedFrameStatEq:
  fixes P :: "('a, 'b, 'c) psi"

  assumes "guarded P"

  shows "extractFrame P ≃_F ⟨ε, 1⟩"
proof -
  obtain A_P Ψ_P where FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" by(rule freshFrame)
  from ‹guarded P› FrP have "Ψ_P ≃ 1" by(blast dest: guardedStatEq)
  hence "⟨A_P, Ψ_P⟩ ≃_F ⟨A_P, 1⟩" by(rule_tac frameResChainPres) auto
  moreover have "⟨A_P, 1⟩ ≃_F ⟨ε, 1⟩" by(rule_tac frameResFreshChain) auto
  ultimately show ?thesis using FrP by(force intro: FrameStatEqTrans)
qed

lemma weakGuardedTransition:
  fixes Ψ   :: 'b
  and   Q    :: "('a, 'b, 'c) psi"
  and   P    :: "('a, 'b, 'c) psi"
  and   α    :: "'a action"
  and   P'   :: "('a, 'b, 'c) psi"
  and   R    :: "('a, 'b, 'c) psi"

  assumes PTrans: "Ψ : Q ⊳ P ==>α ≺ P'"
  and    "guarded Q"

  shows "Ψ : 0 ⊳ P ==>α ≺ P'"
proof -
  obtain A_Q Ψ_Q where FrQ: "extractFrame Q = ⟨A_Q, Ψ_Q⟩" and "A_Q ♯* Ψ" by(rule freshFrame)
  moreover from ‹guarded Q› FrQ have "Ψ_Q ≃ 1" by(blast dest: guardedStatEq)
  hence "⟨A_Q, Ψ ⊗ Ψ_Q⟩ ≃_F ⟨A_Q, Ψ ⊗ 1⟩" by(metis frameIntCompositionSym)
  moreover from ‹A_Q ♯* Ψ› have "⟨A_Q, Ψ ⊗ 1⟩ ≃_F ⟨ε, Ψ ⊗ 1⟩" by(rule_tac frameResFreshChain) auto
  ultimately have "insertAssertion(extractFrame Q) Ψ ≃_F insertAssertion (extractFrame (0)) Ψ"
    using FrQ ‹A_Q ♯* Ψ› by simp (blast intro: FrameStatEqTrans)
  with PTrans show ?thesis by(rule_tac weakTransitionFrameImp) (auto simp add: FrameStatEq_def) 
qed

lemma expandTauChainFrame:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   A_P :: "name list"
  and   Ψ_P :: 'b
  and   C   :: "'d::fs_name"

  assumes PChain: "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     FrP: "extractFrame P = ⟨A_P, Ψ_P⟩"
  and     "distinct A_P"
  and     "A_P ♯* P"
  and     "A_P ♯* C"

  obtains Ψ' A_P' Ψ_P' where "extractFrame P' = ⟨A_P', Ψ_P'⟩" and "Ψ_P ⊗ Ψ' ≃ Ψ_P'" and "A_P' ♯* P'" and "A_P' ♯* C" and "distinct A_P'"
using PChain FrP ‹A_P ♯* P›
proof(induct arbitrary: thesis rule: tauChainInduct)
  case(TauBase P)
  have "Ψ_P ⊗ SBottom' ≃ Ψ_P" by(rule Identity)
  with ‹extractFrame P = ⟨A_P, Ψ_P⟩› show ?case using ‹A_P ♯* P› ‹A_P ♯* C› ‹distinct A_P› by(rule TauBase)
next
  case(TauStep P P' P'')
  from ‹extractFrame P = ⟨A_P, Ψ_P⟩› ‹A_P ♯* P›
  obtain Ψ' A_P' Ψ_P' where FrP': "extractFrame P' = ⟨A_P', Ψ_P'⟩" and "Ψ_P ⊗ Ψ' ≃ Ψ_P'"
                       and "A_P' ♯* P'" and "A_P' ♯* C" and "distinct A_P'"
    by(rule_tac TauStep)
  from ‹Ψ ⊳ P' ⟼τ ≺ P''› FrP' ‹distinct A_P'› ‹A_P' ♯* P'› ‹A_P' ♯* C›
  obtain Ψ'' A_P'' Ψ_P'' where FrP'': "extractFrame P'' = ⟨A_P'', Ψ_P''⟩" and "Ψ_P' ⊗ Ψ'' ≃ Ψ_P''"
                          and "A_P'' ♯* P''" and "A_P'' ♯* C" and "distinct A_P''"
    by(rule expandTauFrame)
  from ‹Ψ_P ⊗ Ψ' ≃ Ψ_P'› have "(Ψ_P ⊗ Ψ') ⊗ Ψ'' ≃ Ψ_P' ⊗ Ψ''" by(rule Composition)
  with ‹Ψ_P' ⊗ Ψ'' ≃ Ψ_P''› have "Ψ_P ⊗ Ψ' ⊗ Ψ'' ≃ Ψ_P''"
    by(metis AssertionStatEqTrans Associativity Commutativity)
  with FrP'' show ?case using ‹A_P'' ♯* P''› ‹A_P'' ♯* C› ‹distinct A_P''›
    by(rule TauStep)
qed

lemma frameIntImpComposition:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   A_F :: "name list"
  and   Ψ_F :: 'b

  assumes "Ψ ≃ Ψ'"

  shows "⟨A_F, Ψ ⊗ Ψ_F⟩ ↪_F ⟨A_F, Ψ' ⊗ Ψ_F⟩"
using assms frameIntComposition
by(simp add: FrameStatEq_def)

lemma tauChainInduct2[consumes 1, case_names TauBase TauStep]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes PChain: "Ψ ⊳ P ==>^{^}_\<tau> P'"
  and     cBase: "∧P. Prop P P"
  and     cStep: "∧P P' P''. [Ψ ⊳ P' ⟼τ ≺ P''; Ψ ⊳ P ==>^{^}_\<tau> P'; Prop P P'] ==> Prop P P''"

  shows "Prop P P'"
using assms
by(rule tauChainInduct)

lemma tauStepChainInduct2[consumes 1, case_names TauBase TauStep]:
  fixes Ψ :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes PChain: "Ψ ⊳ P ==>_\<tau> P'"
  and     cBase: "∧P P'. Ψ ⊳ P ⟼τ ≺ P' ==> Prop P P'"
  and     cStep: "∧P P' P''. [Ψ ⊳ P' ⟼τ ≺ P''; Ψ ⊳ P ==>_\<tau> P'; Prop P P'] ==> Prop P P''"

  shows "Prop P P'"
using assms
by(rule tauStepChainInduct)

lemma weakTransferTauChainFrame:
  fixes Ψ_F :: 'b
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"
  and   A_P :: "name list"
  and   Ψ_P :: 'b
  and   A_F :: "name list"
  and   A_G :: "name list"
  and   Ψ_G :: 'b

  assumes PChain: "Ψ_F ⊳ P ==>^{^}_\<tau> P'"
  and     FrP: "extractFrame P = ⟨A_P, Ψ_P⟩"
  and     "distinct A_P"
  and     FeqG: "∧Ψ. insertAssertion (⟨A_F, Ψ_F ⊗ Ψ_P⟩) Ψ ↪_F insertAssertion (⟨A_G, Ψ_G ⊗ Ψ_P⟩) Ψ"
  and     "A_F ♯* Ψ_G"
  and     "A_G ♯* Ψ"
  and     "A_G ♯* Ψ_F"
  and     "A_F ♯* A_G"
  and     "A_F ♯* P"
  and     "A_G ♯* P"
  and     "A_P ♯* A_F"
  and     "A_P ♯* A_G"
  and     "A_P ♯* Ψ_F"
  and     "A_P ♯* Ψ_G"
  and     "A_P ♯* P"

  shows "Ψ_G ⊳ P ==>^{^}_\<tau> P'"
using PChain FrP ‹A_F ♯* P› ‹A_G ♯* P› ‹A_P ♯* P›
proof(induct rule: tauChainInduct2)
  case TauBase
  thus ?case by simp
next
  case(TauStep P P' P'')
  have FrP: "extractFrame P = ⟨A_P, Ψ_P⟩" by fact
  then have PChain: "Ψ_G ⊳ P ==>^{^}_\<tau> P'" using ‹A_F ♯* P› ‹A_G ♯* P› ‹A_P ♯* P› by(rule TauStep)
  then obtain A_P' Ψ_P' Ψ' where FrP': "extractFrame P' = ⟨A_P', Ψ_P'⟩" and "Ψ_P ⊗ Ψ' ≃ Ψ_P'"
                            and "A_P' ♯* A_F" and "A_P' ♯* A_G" and "A_P' ♯* Ψ_F" and "A_P' ♯* Ψ_G"
                            and "distinct A_P'"
                
    using FrP ‹distinct A_P› ‹A_P ♯* P› ‹A_P ♯* A_F› ‹A_P ♯* A_G› ‹A_P ♯* Ψ_F› ‹A_P ♯* Ψ_G›
    by(rule_tac C="(A_F, A_G, Ψ_F, Ψ_G)" in expandTauChainFrame) auto

  from PChain \   Maintainer:Georg <.struth  

  with java.lang.StringIndexOutOfBoundsException: Range [0, 176) out of bounds for length 78
 have "A_* Ψ_G ♯s>P" and "A_F ♯* Ψ_P'" and "A_G ♯* Ψ_P'"
 by(auto dest: extractFrameFreshChain)

 from FeqG have FeqG: "insertAssertion (⟨A_F, Ψ_F ⊗ Ψ_P⟩) Ψ' ↪_F insertAssertion (⟨A_G, Ψ_G ⊗ Ψ_P⟩) Ψ'"
 by blast
 obtain p::"name prm" where "(p ∙ A_F) ♯* Ψ_F" and "(p ∙ A_F) ♯* Ψ_P" and "(p ∙ A_F) ♯* Ψ_P'" and "(p ∙ A_F) ♯* Ψ'"
 and Sp: "(set p) ⊆ set A_F × set(p ∙ A_F)" and "distinctPerm p"
 by(rule_tac xvec=A_F and c="(Ψ_F, Ψ_P, Ψ', Ψ_P')" in name_list_avoiding) auto
 obtain q::"name prm" where "(q ∙ A_G) ♯* Ψ_G" and "(q ∙ A_G) ♯* Ψ_P" and "(q ∙ A_G) ♯* Ψ_P'" and "(q ∙ A_G) ♯* Ψ'"
 and Sq: "(set q) ⊆ set A_G × set(q ∙ A_G)" and "distinctPerm q"
 by(rule_tac xvec=A_G and c="(Ψ_G, Ψ_P, Ψ', Ψ_P')" in name_list_avoiding) auto
 from ‹Ψ_P ⊗ Ψ' ≃ Ψ_P'› have "⟨(p ∙ A_F), ((p ∙ Ψ_F) ⊗ Ψ_P')⟩ ≃_F ⟨(p ∙ A_F), (p ∙ Ψ_F) ⊗ (Ψ_P ⊗ Ψ')⟩"
 by(rule frameIntCompositionSym[OF AssertionStatEqSym])
 hence "⟨(p ∙ A_F), (p ∙ Ψ_F) ⊗ Ψ_P'⟩ ≃_F ⟨(p ∙ A_F), Ψ' ⊗ ((p ∙ Ψ_F) ⊗ Ψ_P)⟩"
 by(metis frameIntAssociativity FrameStatEqTrans frameIntCommutativity FrameStatEqSym)
 moreover from FeqG ‹A_F ♯* Ψ_P› ‹(p ∙ A ♯P› ‹ A_* Ψsu>F› ‹ A_* Ψ Sp
 ), 🚫
 apply(erule_tac rev_mp) by(subst frameChainAlpha) (auto simp add: eqvts)
 hence "⟨(p ∙ A_F), Ψ' ⊗ ((p ∙ Ψ_F) ⊗ Ψ_P)⟩ ↪_F (⟨(q ∙ A_G), Ψ' ⊗ (q ∙ Ψ_G) ⊗iterat star_den star_si star_sli star_ tc_e)
 using ‹A_G ♯* Ψ_P› ‹(q ∙ A_G) ♯* Ψ_P› ‹(q ∙ A_G) ♯* Ψ_G› ‹(q ∙ A_G) ♯
 apply(erule_tac rev_mp) by(subst frameChainAlpha) (auto simp add: eqvts)
 moreover have "⟨(q ∙ A_G), Ψ' ⊗ ((q ∙ Ψ_G) ⊗ Ψ_P)⟩ ≃_F ⟨(q ∙ A_G), (q ∙ Ψ_G) ⊗ (Ψ_P ⊗ Ψ')⟩"
 by(metis frameIntAssociativity FrameStatEqTrans frameIntCommutativity FrameStatEqSym)
 ultimately show ?thesis
 by(blast intro: FrameStatEqTrans frameIntCompositionSym)
 🚫
 by(rule FrameStatEqImpCompose)
 with ‹A_F ♯* Ψ_P'› ‹(p ∙ A_F) ♯* Ψ -
 by(subst frameChainAlpha) (auto simp add: eqvts)
 with ‹A_G ♯* Ψ_P'› ‹(q ∙ A_G) ♯* Ψ_P'› ‹(q ∙ A_\cdo> z \l>y star> \cdo> z 🚫
 by(subst frameChainAlpha) (auto simp add: eqvts)
 
 with ‹Ψ_F ⊳ P' ⟼τ \<by (metis add.commute add_idem' add.left_commute distrib_right)
java.lang.NullPointerException
 have "ΨG ⊳ P' ⟼ \< P
 with PChain show ?case by(simp add: r_into_rtrancl rtrancl_into_rtrancl)
 

 eie :"(a, ', c) psi\ghtarrow
 where "[∀ "... ≤ a ⋅ e'" using ‹ (a' ⋅⋆∞∞ z›
 (∀Rs. Ψ ⊳.assoc mult_iso mult.assoult_is order_trans)

  quietFrame:
 fixes Ψ :: 'b
 and P :: "('a, 'b, 'c) psi"

 assumes "quiet P"

 shows "insertAssertion (extractFrame P) Ψ ≃_F ⟨ε, Ψ⟩"
  assms
 (erule_tac quiet.cases) force
 
  quietTransition:
 fixes Ψ :: 'b
 and P :: "('a, 'b, 'c) psi"
 and Rs :: "('a, 'b, 'c) residual"

 assumes "quiet P"
 and "Ψ ⊳ P ⟼ Rs"

 obtains P' where "Rs = τ ≺ P'" and "quiet P'"
  assms
 (erule_tac quiet.cases) force
 
  quietEqvt:
 fixes P :: "('a, 'b, 'c) psi"
 and p :: "name prm"

 assumes "quiet P"

 shows "quiet(p ∙ P)"
  -
 let ?X = "λP. ∃p::name prm. quiet(p ∙ P)"
 from assms have "?X (p ∙ P)" by(rule_tac x="rev p" in exI) auto
 thus ?thesis
 apply coinduct
 apply(clarify)
 apply(rule_tac x=x in exI)
 apply auto
 apply(drule_tac Ψ="p ∙ Ψ" in quietFrame)
 apply(drule_tac p="rev p" in FrameStatEqClosed)
 apply(simp add: eqvts)
 apply(drule_tac pi=p in semantics.eqvt)
 apply(erule_tac quietTransition)
 apply assumption
 apply(rule_tac x="rev p ∙ P'" in exI)
 apply auto
 apply(drule_tac pi="rev p" in pt_bij3)
 apply(simp add: eqvts)
 apply(rule_tac x=p in exI)
 by simp
 
 

  quietOutput:
 fixes Ψ :: 'b
 and P :: "('a, 'b, 'c) psi"
 and M :: 'a
 and xvec :: "name list"
 and N :: 'a
 and P' :: "('a, 'b, 'c) psi"
 
 assumes "Ψ ⊳ P ⟼M(ν*xvec)⟨N⟩ ≺ P'"
 and "quiet P"

 shows False
  assms
 (erule_tac quiet.cases)
 (force simp add: residualInject)

  quietInput:
 fixes Ψ :: 'b
 and P :: "('a, 'b, 'c) psi"
 and M :: 'a
 and N :: 'a
 and P' :: "('a, 'b, 'c) psi"
 
 assumes "Ψ ⊳ P ⟼M(N) ≺ P'"
 and "quiet P"

 shows False
  assms
 (erule_tac quiet.cases) (force simp add: residualInject)

  quietTau:
 fixes Ψ :: 'b
 and P :: "('a, 'b, 'c) psi"
 and P' :: "('a, 'b, 'c) psi"
 
 assumes "Ψ ⊳ P ⟼τ ≺ P'"
 and "insertAssertion (extractFrame P) Ψ ≃_F ⟨ε, Ψ⟩"
 and "quiet P"

 shows "quiet P'"
  assms
 (erule_tac quiet.cases) (force simp add: residualInject)

  tauChainCases[consumes 1, case_names TauBase TauStep]:
 fixes Ψ :: 'b
 and P :: "('a, 'b, 'c) psi"
 and P' :: "('a, 'b, 'c) psi"

 assumes "Ψ ⊳ P ==>^{^}_\τ P'"
 and "P = P' ==> Prop"
 and "Ψ ⊳ P ==>_\τ P' ==> Prop"

 shows Prop
  assms
 (blast elim: rtranclE dest: rtrancl_into_trancl1)