Theory Tau_Chain

(* 
   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 ⟹⇧^⇩τ 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 ⟹⇩τ P' ≡ (P, P') ∈ {(P, P'). Ψ ⊳ P ⟼τ ≺ P'}^+"

abbreviation tauContextChain :: "('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" ("_ ⟹⇧^⇩τ _" [80, 80] 80)
where "P ⟹⇧^⇩τ P' ≡ 𝟭 ⊳ P ⟹⇧^⇩τ P'"
abbreviation tauContextStepChain :: "('a, 'b, 'c) psi ⇒ ('a, 'b, 'c) psi ⇒ bool" ("_ ⟹⇩τ _" [80, 80] 80)
where "P ⟹⇩τ P' ≡ 𝟭 ⊳ P ⟹⇩τ 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 ⟹⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇩τ P'"

  shows "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇩τ (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 ⟹⇧^⇩τ P'"

  shows "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (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 ⟹⇩τ P')) = (p ∙ Ψ) ⊳ (p ∙ P) ⟹⇩τ (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 ⟹⇧^⇩τ P')) = (p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (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 ⟹⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇩τ P'"
  and     "(φ, P) mem Cs"
  and     "Ψ ⊢ φ"
  and     "guarded P"

  shows "Ψ ⊳ (Cases Cs) ⟹⇩τ 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 ⟹⇩τ P'"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ ⦇νx⦈P ⟹⇩τ ⦇ν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 ⟹⇧^⇩τ P'"
  and     "x ♯ Ψ"

  shows "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇ν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 ⟹⇩τ P'"
  and     "xvec ♯* Ψ"

  shows "Ψ ⊳ ⦇ν*xvec⦈P ⟹⇩τ ⦇ν*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 ⟹⇧^⇩τ P'"
  and     "xvec ♯* Ψ"

  shows "Ψ ⊳ ⦇ν*xvec⦈P ⟹⇧^⇩τ ⦇ν*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 ⟹⇩τ P'"
  and     "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
  and     "A⇩Q ♯* Ψ"
  and     "A⇩Q ♯* P"

  shows "Ψ ⊳ P ∥ Q ⟹⇩τ 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 ⟹⇧^⇩τ P'"
  and     "extractFrame Q = ⟨A⇩Q, Ψ⇩Q⟩"
  and     "A⇩Q ♯* Ψ"
  and     "A⇩Q ♯* P"

  shows "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ 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 ⟹⇩τ Q'"
  and     "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
  and     "A⇩P ♯* Ψ"
  and     "A⇩P ♯* Q"

  shows "Ψ ⊳ P ∥ Q ⟹⇩τ 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 ⟹⇧^⇩τ Q'"
  and     "extractFrame P = ⟨A⇩P, Ψ⇩P⟩"
  and     "A⇩P ♯* Ψ"
  and     "A⇩P ♯* Q"

  shows "Ψ ⊳ P ∥ Q ⟹⇧^⇩τ 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 ⟹⇩τ P'"
  and     "guarded P"

  shows "Ψ ⊳ !P ⟹⇩τ 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 ⟹⇩τ P'"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' ⊳ P ⟹⇩τ 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 ⟹⇧^⇩τ P'"
  and     "Ψ ≃ Ψ'"

  shows "Ψ' ⊳ P ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ P''" and "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
                           and "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from ‹Ψ ⊳ P ⟹⇧^⇩τ P''› have "(p ∙ Ψ) ⊳ (p ∙ P) ⟹⇧^⇩τ (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 Ψ   :: '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 ⟹α ≺ P'"
  and     S: "set p ⊆ set xvec × set(p ∙ xvec)"
  and     "xvec ♯* (p ∙ xvec)"
  and     "(p ∙ xvec) ♯* P"
  and     "(p ∙ xvec) ♯* N"

  shows "Ψ : Q ⊳ P ⟹M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ P')"
proof -
  from PTrans obtain P'' where PChain: "Ψ ⊳ P ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼M⦇ν*xvec⦈⟨N⟩ ≺ P'"
    by(rule weakTransitionE)

  note PChain QeqP''
  moreover from PChain `(p ∙ xvec) ♯* P` have "(p ∙ xvec) ♯* P''" by(rule tauChainFreshChain)
  with P''Trans `xvec ♯* (p ∙ xvec)` `(p ∙ xvec) ♯* N` have "(p ∙ xvec) ♯* P'"
    by(force intro: outputFreshChainDerivative)
  with P''Trans S `(p ∙ xvec) ♯* N` have "Ψ ⊳ P'' ⟼M⦇ν*(p ∙ xvec)⦈⟨(p ∙ N)⟩ ≺ (p ∙ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟨ε, Ψ ⊗ 𝟭⟩"

  shows "Ψ : Q ⊳ M⦇λ*xvec N⦈.P ⟹K⦇(N[xvec::=Tvec])⦈ ≺ P[xvec::=Tvec]"
proof -
  have "Ψ ⊳  M⦇λ*xvec N⦈.P ⟹⇧^⇩τ 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 ⟨ε, Ψ ⊗ 𝟭⟩"

  shows "Ψ : Q ⊳ M⟨N⟩.P ⟹K⟨N⟩ ≺ P"
proof -
  have "Ψ ⊳  M⟨N⟩.P ⟹⇧^⇩τ 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 ⟨ε, Ψ ⊗ 𝟭⟩"
proof -
  obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" and "A⇩P ♯* Ψ" by(rule freshFrame)
  from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" and "supp Ψ⇩P = ({}::name set)"
    by(blast dest: guardedStatEq)+
  
  from FrP ‹A⇩P ♯* Ψ› ‹Ψ⇩P ≃ 𝟭› have "insertAssertion(extractFrame P) Ψ ≃⇩F ⟨A⇩P, Ψ ⊗ 𝟭⟩"
    by simp (metis frameIntCompositionSym)
  moreover from ‹A⇩P ♯* Ψ› have "⟨A⇩P, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
    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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇩τ P''" by(simp add: rtrancl_eq_or_trancl)
    hence "Ψ ⊳ Cases CsP ⟹⇩τ P''" using ‹(φ, P) mem CsP› ‹Ψ ⊢ φ› ‹guarded P› 
      by(rule tauStepChainCase)
    hence "Ψ ⊳ Cases CsP ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ ⦇ν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 ⟹⇧^⇩τ P''" and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹x ♯ Ψ› have "Ψ ⊳ ⦇νx⦈P ⟹⇧^⇩τ ⦇ν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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇩τ (⦇ν*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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇩τ (⦇ν*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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ P''"
                           and QeqP'': "insertAssertion (extractFrame Q) Ψ ↪⇩F insertAssertion (extractFrame P'') Ψ"
                           and P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'"
    by(rule weakTransitionE)

  from PChain ‹Ψ ≃ Ψ'› have "Ψ' ⊳ P ⟹⇧^⇩τ 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 ≃ 𝟭" 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 ⟹⇧^⇩τ 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 ≃ 𝟭" by(blast dest: guardedStatEq)
  ultimately show ?thesis
  proof(auto simp add: rtrancl_eq_or_trancl)
    have "Ψ ⊳ !P ⟹⇧^⇩τ !P" by simp
    moreover assume RimpP: "insertAssertion(extractFrame R) Ψ ↪⇩F ⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ 𝟭⟩"
    have "insertAssertion(extractFrame R) Ψ ↪⇩F insertAssertion(extractFrame(!P)) Ψ"
    proof -
      from ‹Ψ⇩P ≃ 𝟭› have "⟨A⇩P, Ψ ⊗ Ψ⇩P ⊗ 𝟭⟩ ≃⇩F ⟨A⇩P, Ψ ⊗ 𝟭⟩"
        by(metis frameIntCompositionSym frameIntAssociativity frameIntCommutativity frameIntIdentity FrameStatEqTrans FrameStatEqSym)
      moreover from ‹A⇩P ♯* Ψ› have "⟨A⇩P, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩"
        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 ⟹⇩τ  P''"
    hence "Ψ ⊳ !P ⟹⇩τ P''" using ‹guarded P› by(rule tauStepChainBang)
    hence "Ψ ⊳ !P ⟹⇧^⇩τ 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 ⟨ε, 𝟭⟩"
proof -
  obtain A⇩P Ψ⇩P where FrP: "extractFrame P = ⟨A⇩P, Ψ⇩P⟩" by(rule freshFrame)
  from ‹guarded P› FrP have "Ψ⇩P ≃ 𝟭" by(blast dest: guardedStatEq)
  hence "⟨A⇩P, Ψ⇩P⟩ ≃⇩F ⟨A⇩P, 𝟭⟩" by(rule_tac frameResChainPres) auto
  moreover have "⟨A⇩P, 𝟭⟩ ≃⇩F ⟨ε, 𝟭⟩" 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 "Ψ : 𝟬 ⊳ 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 ≃ 𝟭" by(blast dest: guardedStatEq)
  hence "⟨A⇩Q, Ψ ⊗ Ψ⇩Q⟩ ≃⇩F ⟨A⇩Q, Ψ ⊗ 𝟭⟩" by(metis frameIntCompositionSym)
  moreover from ‹A⇩Q ♯* Ψ› have "⟨A⇩Q, Ψ ⊗ 𝟭⟩ ≃⇩F ⟨ε, Ψ ⊗ 𝟭⟩" by(rule_tac frameResFreshChain) auto
  ultimately have "insertAssertion(extractFrame Q) Ψ ≃⇩F insertAssertion (extractFrame (𝟬)) Ψ"
    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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ P'"
  and     cBase: "⋀P. Prop P P"
  and     cStep: "⋀P P' P''. ⟦Ψ ⊳ P' ⟼τ ≺ P''; Ψ ⊳ P ⟹⇧^⇩τ 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 ⟹⇩τ P'"
  and     cBase: "⋀P P'. Ψ ⊳ P ⟼τ ≺ P' ⟹ Prop P P'"
  and     cStep: "⋀P P' P''. ⟦Ψ ⊳ P' ⟼τ ≺ P''; Ψ ⊳ P ⟹⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ⟹⇧^⇩τ 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 ‹A⇩F ♯* P› ‹A⇩G ♯* P› have "A⇩F ♯* P'" and "A⇩G ♯* P'" by(blast dest: tauChainFreshChain)+

  with ‹A⇩F ♯* P› ‹A⇩G ♯* P› ‹A⇩P ♯* A⇩F› ‹A⇩P ♯* A⇩G›‹A⇩P' ♯* A⇩F› ‹A⇩P' ♯* A⇩G› FrP FrP'
  have "A⇩F ♯* Ψ⇩P" and "A⇩G ♯* Ψ⇩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⇩F) ♯* Ψ⇩P› ‹(p ∙ A⇩F) ♯* Ψ⇩F› ‹(p ∙ A⇩F) ♯* Ψ'› Sp
  have "⟨(p ∙ A⇩F), Ψ' ⊗ ((p ∙ Ψ⇩F) ⊗ Ψ⇩P)⟩ ↪⇩F insertAssertion (⟨A⇩G, Ψ⇩G ⊗ Ψ⇩P⟩) Ψ'"
    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) ⊗ Ψ⇩P⟩)"
    using ‹A⇩G ♯* Ψ⇩P› ‹(q ∙ A⇩G) ♯* Ψ⇩P› ‹(q ∙ A⇩G) ♯* Ψ⇩G› ‹(q ∙ A⇩G) ♯* Ψ'› Sq
    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)
  hence "⟨(q ∙ A⇩G), Ψ' ⊗ ((q ∙ Ψ⇩G) ⊗ Ψ⇩P)⟩ ≃⇩F ⟨(q ∙ A⇩G), (q ∙ Ψ⇩G) ⊗ Ψ⇩P'⟩" using ‹Ψ⇩P ⊗ Ψ' ≃ Ψ⇩P'›
    by(blast intro: FrameStatEqTrans frameIntCompositionSym)
  ultimately have "⟨(p ∙ A⇩F), (p ∙ Ψ⇩F) ⊗ Ψ⇩P'⟩ ↪⇩F ⟨(q ∙ A⇩G), (q ∙ Ψ⇩G) ⊗ Ψ⇩P'⟩"
    by(rule FrameStatEqImpCompose)
  with ‹A⇩F ♯* Ψ⇩P'› ‹(p ∙ A⇩F) ♯* Ψ⇩P'› ‹(p ∙ A⇩F) ♯* Ψ⇩F› Sp have "⟨A⇩F, Ψ⇩F ⊗ Ψ⇩P'⟩ ↪⇩F ⟨(q ∙ A⇩G), (q ∙ Ψ⇩G) ⊗ Ψ⇩P'⟩"
    by(subst frameChainAlpha) (auto simp add: eqvts)
  with ‹A⇩G ♯* Ψ⇩P'› ‹(q ∙ A⇩G) ♯* Ψ⇩P'› ‹(q ∙ A⇩G) ♯* Ψ⇩G› Sq have "⟨A⇩F, Ψ⇩F ⊗ Ψ⇩P'⟩ ↪⇩F ⟨A⇩G, Ψ⇩G ⊗ Ψ⇩P'⟩"
    by(subst frameChainAlpha) (auto simp add: eqvts)
  
  with ‹Ψ⇩F ⊳ P' ⟼τ ≺ P''› FrP' ‹distinct A⇩P'›
       ‹A⇩F ♯* P'› ‹A⇩G ♯* P'› ‹A⇩F ♯* Ψ⇩G› ‹A⇩G ♯* Ψ⇩F› ‹A⇩P' ♯* A⇩F› ‹A⇩P' ♯* A⇩G› ‹A⇩P' ♯* Ψ⇩F› ‹A⇩P' ♯* Ψ⇩G›
  have "Ψ⇩G ⊳ P' ⟼τ ≺ P''" by(rule_tac transferTauFrame)
  with PChain show ?case by(simp add: r_into_rtrancl rtrancl_into_rtrancl)
qed

coinductive quiet :: "('a, 'b, 'c) psi ⇒ bool"
  where "⟦∀Ψ. (insertAssertion (extractFrame P) Ψ ≃⇩F ⟨ε, Ψ⟩ ∧ 
              (∀Rs. Ψ ⊳ P ⟼ Rs ⟶ (∃P'. Rs = τ ≺ P' ∧ quiet P')))⟧ ⟹ quiet P"

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

  assumes "quiet P"

  shows "insertAssertion (extractFrame P) Ψ ≃⇩F ⟨ε, Ψ⟩"
using assms
by(erule_tac quiet.cases) force
  
lemma 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'"
using assms
by(erule_tac quiet.cases) force
  
lemma quietEqvt:
  fixes P :: "('a, 'b, 'c) psi"
  and   p :: "name prm"

  assumes "quiet P"

  shows "quiet(p ∙ P)"
proof -
  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
qed
  

lemma 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
using assms
apply(erule_tac quiet.cases)
by(force simp add: residualInject)

lemma 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
using assms
by(erule_tac quiet.cases) (force simp add: residualInject)

lemma 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'"
using assms
by(erule_tac quiet.cases) (force simp add: residualInject)

lemma 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
using assms
by(blast elim: rtranclE dest: rtrancl_into_trancl1)

end

end