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 "Ψ  ⦇νxP τ ⦇νxP'"
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 "Ψ  ⦇νxP ^τ ⦇νxP'"
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 "Ψ  ⦇ν*xvecP τ ⦇ν*xvecP'"
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 "Ψ  ⦇ν*xvecP ^τ ⦇ν*xvecP'"
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   AQ :: "name list"

  assumes "Ψ  ΨQ  P τ P'"
  and     "extractFrame Q = AQ, ΨQ"
  and     "AQ ♯* Ψ"
  and     "AQ ♯* 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   AQ :: "name list"

  assumes "Ψ  ΨQ  P ^τ P'"
  and     "extractFrame Q = AQ, ΨQ"
  and     "AQ ♯* Ψ"
  and     "AQ ♯* 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   AP :: "name list"

  assumes "Ψ  ΨP  Q τ Q'"
  and     "extractFrame P = AP, ΨP"
  and     "AP ♯* Ψ"
  and     "AP ♯* 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   AP :: "name list"

  assumes "Ψ  ΨP  Q ^τ Q'"
  and     "extractFrame P = AP, ΨP"
  and     "AP ♯* Ψ"
  and     "AP ♯* 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 MN  P'"
  and     "x  P"
  and     "x  N"

  shows "x  P'"
proof -
  from PTrans obtain P'' where PChain: "Ψ  P ^τ P''" and P''Trans: "Ψ  P'' MN  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 MN  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 MN  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'' MN  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  MN⟩.P KN  P"
proof -
  have "Ψ   MN⟩.P ^τ MN⟩.P" by simp
  moreover from QeqΨ have "insertAssertion (extractFrame Q) Ψ F insertAssertion (extractFrame(MN⟩.P)) Ψ"
    by auto
  moreover have "insertAssertion (extractFrame(MN⟩.P)) Ψ F insertAssertion (extractFrame(MN⟩.P)) Ψ" by simp
  moreover from Ψ  M  K have "Ψ  MN⟩.P KN  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 AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" by(rule freshFrame)
  from guarded P FrP have "ΨP  𝟭" and "supp ΨP = ({}::name set)"
    by(blast dest: guardedStatEq)+
  
  from FrP AP ♯* Ψ ΨP  𝟭 have "insertAssertion(extractFrame P) Ψ F AP, Ψ  𝟭"
    by simp (metis frameIntCompositionSym)
  moreover from AP ♯* Ψ have "AP, Ψ  𝟭 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 "Ψ : ⦇νxQ  ⦇νxP 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 "Ψ  ⦇νxP ^τ ⦇νxP''" by(rule tauChainResPres)
  moreover from QeqP'' x  Ψ have "insertAssertion (extractFrame(⦇νxQ)) Ψ F insertAssertion (extractFrame(⦇νxP'')) Ψ" by(force intro: frameImpResPres)
  moreover from P''Trans x  supp N x  Ψ x  M x  xvec x  yvec have "Ψ  ⦇νxP'' 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 "Ψ : ⦇νxQ  ⦇νxP α  ⦇νxP'"
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 "Ψ  ⦇νxP ^τ ⦇νxP''" by(rule tauChainResPres)
  moreover from QeqP'' x  Ψ have "insertAssertion (extractFrame(⦇νxQ)) Ψ F insertAssertion (extractFrame(⦇νxP'')) Ψ" by(force intro: frameImpResPres)
  moreover from P''Trans x  Ψ x  α have "Ψ  ⦇νxP'' α  ⦇νxP'"
    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   AQ   :: "name list"
  and   ΨQ   :: 'b

  assumes PTrans: "Ψ  ΨQ : R  P α  P'"
  and     FrQ: "extractFrame Q = AQ, ΨQ"
  and     "bn α ♯* Q"
  and     "AQ ♯* Ψ"
  and     "AQ ♯* P"
  and     "AQ ♯* α"
  and     "AQ ♯* 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 AQ ♯* P have "AQ ♯* P''" by(rule tauChainFreshChain)
  from PChain FrQ AQ ♯* Ψ AQ ♯* P have "Ψ  P  Q ^τ P''  Q" by(rule tauChainPar1)
  moreover have "insertAssertion (extractFrame(R  Q)) Ψ F insertAssertion (extractFrame(P''  Q)) Ψ"
  proof -
    obtain AR ΨR where FrR: "extractFrame R = AR, ΨR" and "AR ♯* AQ" and "AR ♯* ΨQ" and "AR ♯* Ψ"
      by(rule_tac C="(AQ, ΨQ, Ψ)" in freshFrame) auto
    obtain AP'' ΨP'' where FrP'': "extractFrame P'' = AP'', ΨP''" and "AP'' ♯* AQ" and "AP'' ♯* ΨQ" and "AP'' ♯* Ψ"
      by(rule_tac C="(AQ, ΨQ, Ψ)" in freshFrame) auto

    from FrR FrP'' AQ ♯* R AQ ♯* P'' AR ♯* AQ AP'' ♯* AQ have "AQ ♯* ΨR" and "AQ ♯* ΨP''"
      by(force dest: extractFrameFreshChain)+
    have "AR, Ψ  ΨR  ΨQ F AR, (Ψ  ΨQ)  ΨR"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
    moreover from ReqP'' FrR FrP'' AR ♯* Ψ AR ♯* ΨQ AP'' ♯* Ψ AP'' ♯* ΨQ
    have "AR, (Ψ  ΨQ)  ΨR F AP'', (Ψ  ΨQ)  ΨP''" using freshCompChain by auto
    moreover have "AP'', (Ψ  ΨQ)  ΨP'' F AP'', Ψ  ΨP''  ΨQ"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
    ultimately have "AR, Ψ  ΨR  ΨQ F AP'', Ψ  ΨP''  ΨQ"
      by(force dest: FrameStatImpTrans simp add: FrameStatEq_def)

    hence "(AR@AQ), Ψ  ΨR  ΨQ F (AP''@AQ), Ψ  ΨP''  ΨQ"
      apply(simp add: frameChainAppend)
      apply(drule_tac xvec=AQ in frameImpResChainPres)
      by(metis frameImpChainComm FrameStatImpTrans)
    with FrR FrQ FrP'' AR ♯* AQ AR ♯* ΨQ AQ ♯* ΨR AP'' ♯* AQ AP'' ♯* ΨQ AQ ♯* ΨP'' AR ♯* Ψ AP'' ♯* Ψ AQ ♯* Ψ ReqP''
    show ?thesis by simp
  qed
  moreover from P''Trans FrQ bn α ♯* Q AQ ♯* Ψ AQ ♯* P'' AQ ♯* α 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   AP   :: "name list"
  and   ΨP  :: 'b

  assumes QTrans: "Ψ  ΨP : R  Q α  Q'"
  and     FrP: "extractFrame P = AP, ΨP"
  and     "bn α ♯* P"
  and     "AP ♯* Ψ"
  and     "AP ♯* Q"
  and     "AP ♯* α"
  and     "AP ♯* 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 AP ♯* Q have "AP ♯* Q''" by(rule tauChainFreshChain)

  from QChain FrP AP ♯* Ψ AP ♯* Q have "Ψ  P  Q ^τ P  Q''" by(rule tauChainPar2)
  moreover have "insertAssertion (extractFrame(P  R)) Ψ F insertAssertion (extractFrame(P  Q'')) Ψ"
  proof -
    obtain AR ΨR where FrR: "extractFrame R = AR, ΨR" and "AR ♯* AP" and "AR ♯* ΨP" and "AR ♯* Ψ"
      by(rule_tac C="(AP, ΨP, Ψ)" in freshFrame) auto
    obtain AQ'' ΨQ'' where FrQ'': "extractFrame Q'' = AQ'', ΨQ''" and "AQ'' ♯* AP" and "AQ'' ♯* ΨP" and "AQ'' ♯* Ψ"
      by(rule_tac C="(AP, ΨP, Ψ)" in freshFrame) auto

    from FrR FrQ'' AP ♯* R AP ♯* Q'' AR ♯* AP AQ'' ♯* AP have "AP ♯* ΨR" and "AP ♯* ΨQ''"
      by(force dest: extractFrameFreshChain)+
    have "AR, Ψ  ΨP  ΨR F AR, (Ψ  ΨP)  ΨR"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)

    moreover from ReqQ'' FrR FrQ'' AR ♯* Ψ AR ♯* ΨP AQ'' ♯* Ψ AQ'' ♯* ΨP
    have "AR, (Ψ  ΨP)  ΨR F AQ'', (Ψ  ΨP)  ΨQ''" using freshCompChain by simp
    moreover have "AQ'', (Ψ  ΨP)  ΨQ'' F AQ'', Ψ  ΨP  ΨQ''"
      by(metis frameNilStatEq frameResChainPres Associativity Commutativity Composition AssertionStatEqTrans)
    ultimately have "AR, Ψ  ΨP  ΨR F AQ'', Ψ  ΨP  ΨQ''"
      by(force dest: FrameStatImpTrans simp add: FrameStatEq_def)
    hence "(AP@AR), Ψ  ΨP  ΨR F (AP@AQ''), Ψ  ΨP  ΨQ''"
      apply(simp add: frameChainAppend)
      apply(drule_tac xvec=AP in frameImpResChainPres)
      by(metis frameImpChainComm FrameStatImpTrans)
    with FrR FrP FrQ'' AR ♯* AP AR ♯* ΨP AP ♯* ΨR AQ'' ♯* AP AQ'' ♯* ΨP AP ♯* ΨQ'' AR ♯* Ψ AQ'' ♯* Ψ AP ♯* Ψ ReqQ''
    show ?thesis by simp
  qed
  moreover from Q''Trans FrP bn α ♯* P AP ♯* Ψ AP ♯* Q'' AP ♯* α 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   AQ   :: "name list"
  and   ΨQ   :: 'b

  assumes PTrans: "Ψ  ΨQ : R  P MN  P'"
  and     FrR: "extractFrame R = AR, ΨR"
  and     QTrans: "Ψ  ΨR  Q K⦇ν*xvec⦈⟨N  Q'"
  and     FrQ: "extractFrame Q = AQ, ΨQ"
  and     MeqK: "Ψ  ΨR  ΨQ  M  K"
  and     "AR ♯* Ψ"
  and     "AR ♯* P"
  and     "AR ♯* Q"
  and     "AR ♯* R"
  and     "AR ♯* M"
  and     "AR ♯* AQ"
  and     "AQ ♯* Ψ"
  and     "AQ ♯* P"
  and     "AQ ♯* Q"
  and     "AQ ♯* R"
  and     "AQ ♯* K"
  and     "xvec ♯* P"

  shows "Ψ  P  Q τ (⦇ν*xvec(P'  Q'))"
proof -
  from extractFrame Q = AQ, ΨQ AQ ♯* Ψ AQ ♯* P AQ ♯* Q AQ ♯* R AQ ♯* K AR ♯* AQ
  obtain AQ' where FrQ': "extractFrame Q = AQ', ΨQ" and "distinct AQ'" and "AQ' ♯* Ψ" and "AQ' ♯* P" 
               and "AQ' ♯* Q" and "AQ' ♯* R" and "AQ' ♯* K" and "AR ♯* AQ'"
    by(rule_tac C="(Ψ, P, Q, R, K, AR)" 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'' MN  P'"
    by(rule weakTransitionE)

  from PChain AQ' ♯* P have "AQ' ♯* P''" by(rule tauChainFreshChain)
  obtain AP'' ΨP'' where FrP'': "extractFrame P'' = AP'', ΨP''" and "AP'' ♯* (Ψ, AQ', ΨQ, AR, ΨR, M, N, K, R, Q, P'', xvec)" and "distinct AP''"
    by(rule freshFrame)
  hence "AP'' ♯* Ψ" and "AP'' ♯* AQ'" and "AP'' ♯* ΨQ" and "AP'' ♯* M" and "AP'' ♯* R" and "AP'' ♯* Q"
    and "AP'' ♯* N" and "AP'' ♯* K" and "AP'' ♯* AR" and "AP'' ♯* P''" and "AP'' ♯* xvec" and "AP'' ♯* ΨR"
    by simp+
  from FrR AR ♯* AQ' AQ' ♯* R have "AQ' ♯* ΨR" by(drule_tac extractFrameFreshChain) auto
  from FrQ' AR ♯* AQ' AR ♯* Q have "AR ♯* ΨQ" by(drule_tac extractFrameFreshChain) auto
  from PChain xvec ♯* P have "xvec ♯* P''" by(force intro: tauChainFreshChain)+

  have "AR, (Ψ  ΨR)  ΨQ F AR, (Ψ  ΨQ)  ΨR" 
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  moreover with RimpP'' FrP'' FrR AP'' ♯* Ψ AR ♯* Ψ AP'' ♯* ΨQ AR ♯* ΨQ
  have "AR, (Ψ  ΨQ)  ΨR F AP'', (Ψ  ΨQ)  ΨP''" using freshCompChain
    by(simp add: freshChainSimps)
  moreover have "AP'', (Ψ  ΨQ)  ΨP'' F AP'', (Ψ  ΨP'')  ΨQ"
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  ultimately have RImpP'': "AR, (Ψ  ΨR)  ΨQ F AP'', (Ψ  ΨP'')  ΨQ"
    by(rule FrameStatEqImpCompose)
      
  from PChain FrQ' AQ' ♯* Ψ AQ' ♯* P have "Ψ  P  Q ^τ P''  Q" by(rule tauChainPar1)
  moreover from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' distinct AP'' distinct AQ' AP'' ♯* AQ' AR ♯* AQ'
        AQ' ♯* Ψ AQ' ♯* P'' AQ' ♯* Q AQ' ♯* R AQ' ♯* K AP'' ♯* Ψ AP'' ♯* R AP'' ♯* Q
        AP'' ♯* P'' AP'' ♯* M AQ ♯* R AR ♯* Q AR ♯* M
  obtain K' where "Ψ  ΨP''  Q K'⦇ν*xvec⦈⟨N  Q'" and "Ψ  ΨP''  ΨQ  M  K'" and "AQ' ♯* K'"
    by(rule_tac comm1Aux) (assumption | simp)+
  with P''Trans FrP'' have "Ψ  P''  Q τ  ⦇ν*xvec(P'  Q')" using FrQ' AQ' ♯* Ψ AQ' ♯* P'' AQ' ♯* Q
    xvec ♯* P'' AP'' ♯* Ψ AP'' ♯* P'' AP'' ♯* Q AP'' ♯* M  AP'' ♯* AQ'
    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   AQ   :: "name list"
  and   ΨQ   :: 'b

  assumes PTrans: "Ψ  ΨQ : R  P M⦇ν*xvec⦈⟨N  P'"
  and     FrR: "extractFrame R = AR, ΨR"
  and     QTrans: "Ψ  ΨR  Q KN  Q'"
  and     FrQ: "extractFrame Q = AQ, ΨQ"
  and     MeqK: "Ψ  ΨR  ΨQ  M  K"
  and     "AR ♯* Ψ"
  and     "AR ♯* P"
  and     "AR ♯* Q"
  and     "AR ♯* R"
  and     "AR ♯* M"
  and     "AR ♯* AQ"
  and     "AQ ♯* Ψ"
  and     "AQ ♯* P"
  and     "AQ ♯* Q"
  and     "AQ ♯* R"
  and     "AQ ♯* K"
  and     "xvec ♯* Q"
  and     "xvec ♯* M"
  and     "xvec ♯* AQ"
  and     "xvec ♯* AR"

  shows "Ψ  P  Q τ (⦇ν*xvec(P'  Q'))"
proof -
  from extractFrame Q = AQ, ΨQ AQ ♯* Ψ AQ ♯* P AQ ♯* Q AQ ♯* R AQ ♯* K AR ♯* AQ xvec ♯* AQ
  obtain AQ' where FrQ': "extractFrame Q = AQ', ΨQ" and "distinct AQ'" and "AQ' ♯* Ψ" and "AQ' ♯* P" 
               and "AQ' ♯* Q" and "AQ' ♯* R" and "AQ' ♯* K" and "AR ♯* AQ'" and "AQ' ♯* xvec"
    by(rule_tac C="(Ψ, P, Q, R, K, AR, 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 AQ' ♯* P have "AQ' ♯* P''" by(rule tauChainFreshChain)
  obtain AP'' ΨP'' where FrP'': "extractFrame P'' = AP'', ΨP''" and "AP'' ♯* (Ψ, AQ', ΨQ, AR, ΨR, M, N, K, R, Q, P'', xvec)" and "distinct AP''"
    by(rule freshFrame)
  hence "AP'' ♯* Ψ" and "AP'' ♯* AQ'" and "AP'' ♯* ΨQ" and "AP'' ♯* M" and "AP'' ♯* R" and "AP'' ♯* Q"
    and "AP'' ♯* N" and "AP'' ♯* K" and "AP'' ♯* AR" and "AP'' ♯* P''" and "AP'' ♯* xvec" and "AP'' ♯* ΨR"
    by simp+
  from FrR AR ♯* AQ' AQ' ♯* R have "AQ' ♯* ΨR" by(drule_tac extractFrameFreshChain) auto
  from FrQ' AR ♯* AQ' AR ♯* Q have "AR ♯* ΨQ" by(drule_tac extractFrameFreshChain) auto

  have "AR, (Ψ  ΨR)  ΨQ F AR, (Ψ  ΨQ)  ΨR" 
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  moreover with RimpP'' FrP'' FrR AP'' ♯* Ψ AR ♯* Ψ AP'' ♯* ΨQ AR ♯* ΨQ
  have "AR, (Ψ  ΨQ)  ΨR F AP'', (Ψ  ΨQ)  ΨP''" using freshCompChain
    by(simp add: freshChainSimps)
  moreover have "AP'', (Ψ  ΨQ)  ΨP'' F AP'', (Ψ  ΨP'')  ΨQ"
    by(metis frameResChainPres frameNilStatEq Commutativity AssertionStatEqTrans Composition Associativity)
  ultimately have RImpP'': "AR, (Ψ  ΨR)  ΨQ F AP'', (Ψ  ΨP'')  ΨQ"
    by(rule FrameStatEqImpCompose)
      
  from PChain FrQ' AQ' ♯* Ψ AQ' ♯* P have "Ψ  P  Q ^τ P''  Q" by(rule tauChainPar1)
  moreover from QTrans FrR P''Trans MeqK RImpP'' FrP'' FrQ' distinct AP'' distinct AQ' AP'' ♯* AQ' AR ♯* AQ'
        AQ' ♯* Ψ AQ' ♯* P'' AQ' ♯* Q AQ' ♯* R AQ' ♯* K AP'' ♯* Ψ AP'' ♯* R AP'' ♯* Q
        AP'' ♯* P'' AP'' ♯* M AQ ♯* R AR ♯* Q AR ♯* M xvec ♯* AR xvec ♯* M AQ' ♯* xvec
  obtain K' where "Ψ  ΨP''  Q K'N  Q'" and "Ψ  ΨP''  ΨQ  M  K'" and "AQ' ♯* K'"
    by(rule_tac comm2Aux) (assumption | simp)+
  with P''Trans FrP'' have "Ψ  P''  Q τ  ⦇ν*xvec(P'  Q')" using FrQ' AQ' ♯* Ψ AQ' ♯* P'' AQ' ♯* Q
    xvec ♯* Q AP'' ♯* Ψ AP'' ♯* P'' AP'' ♯* Q AP'' ♯* M  AP'' ♯* AQ'
    by(rule_tac Comm2)
  ultimately show ?thesis
    by(drule_tac tauActTauStepChain) auto
qed

lemma frameImpIntComposition:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   AF :: "name list"
  and   ΨF :: 'b

  assumes "Ψ  Ψ'"

  shows "AF, Ψ  ΨF F AF, Ψ'  ΨF"
proof -
  from assms have "AF, Ψ  ΨF F AF, Ψ'  Ψ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 AF ΨF where FrF: "F = AF, ΨF" and "AF ♯* Ψ" and "AF ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
  obtain AG ΨG where FrG: "G = AG, ΨG" and "AG ♯* Ψ" and "AG ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto

  from Ψ  Ψ' have "AF, Ψ'  ΨF F AF, Ψ  ΨF" by (metis frameIntComposition FrameStatEqSym)
  moreover from Ψ  Ψ' have "AG, Ψ  ΨG F AG, Ψ'  ΨG" by(rule frameIntComposition)
  ultimately have "AF, Ψ'  ΨF F AG, Ψ'  ΨG" using FeqG FrF FrG AF ♯* Ψ AG ♯* Ψ Ψ  Ψ'
    by(force simp add: FrameStatEq_def dest: FrameStatImpTrans)
  with FrF FrG AF ♯* Ψ' AG ♯* Ψ' 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 AF ΨF where FrF: "F = AF, ΨF" and "AF ♯* Ψ" and "AF ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto
  obtain AG ΨG where FrG: "G = AG, ΨG" and "AG ♯* Ψ" and "AG ♯* Ψ'"
    by(rule_tac C="(Ψ, Ψ')" in freshFrame) auto

  from FeqG FrF FrG AF ♯* Ψ AG ♯* Ψ Ψ  Ψ'
  have "AF, Ψ'  ΨF F AG, Ψ'  ΨG"
    by simp (metis frameIntComposition FrameStatEqTrans FrameStatEqSym)
  with FrF FrG AF ♯* Ψ' AG ♯* Ψ' 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 AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" and "AQ ♯* P" and "AQ ♯* α" and "AQ ♯* 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 AQ ♯* Ψ AQ ♯* P AQ ♯* α AQ ♯* 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 AP ΨP where FrP: "extractFrame P = AP, ΨP" and "AP ♯* Ψ" 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 AP, Ψ  ΨP  𝟭"
    have "insertAssertion(extractFrame R) Ψ F insertAssertion(extractFrame(!P)) Ψ"
    proof -
      from ΨP  𝟭 have "AP, Ψ  ΨP  𝟭 F AP, Ψ  𝟭"
        by(metis frameIntCompositionSym frameIntAssociativity frameIntCommutativity frameIntIdentity FrameStatEqTrans FrameStatEqSym)
      moreover from AP ♯* Ψ have "AP, Ψ  𝟭 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 AP ΨP where FrP: "extractFrame P = AP, ΨP" by(rule freshFrame)
  from guarded P FrP have "ΨP  𝟭" by(blast dest: guardedStatEq)
  hence "AP, ΨP F AP, 𝟭" by(rule_tac frameResChainPres) auto
  moreover have "AP, 𝟭 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 AQ ΨQ where FrQ: "extractFrame Q = AQ, ΨQ" and "AQ ♯* Ψ" by(rule freshFrame)
  moreover from guarded Q FrQ have "ΨQ  𝟭" by(blast dest: guardedStatEq)
  hence "AQ, Ψ  ΨQ F AQ, Ψ  𝟭" by(metis frameIntCompositionSym)
  moreover from AQ ♯* Ψ have "AQ, Ψ  𝟭 F ⟨ε, Ψ  𝟭" by(rule_tac frameResFreshChain) auto
  ultimately have "insertAssertion(extractFrame Q) Ψ F insertAssertion (extractFrame (𝟬)) Ψ"
    using FrQ AQ ♯* Ψ 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   AP :: "name list"
  and   ΨP :: 'b
  and   C   :: "'d::fs_name"

  assumes PChain: "Ψ  P ^τ P'"
  and     FrP: "extractFrame P = AP, ΨP"
  and     "distinct AP"
  and     "AP ♯* P"
  and     "AP ♯* C"

  obtains Ψ' AP' ΨP' where "extractFrame P' = AP', ΨP'" and "ΨP  Ψ'  ΨP'" and "AP' ♯* P'" and "AP' ♯* C" and "distinct AP'"
using PChain FrP AP ♯* P
proof(induct arbitrary: thesis rule: tauChainInduct)
  case(TauBase P)
  have "ΨP  SBottom'  ΨP" by(rule Identity)
  with extractFrame P = AP, ΨP show ?case using AP ♯* P AP ♯* C distinct AP by(rule TauBase)
next
  case(TauStep P P' P'')
  from extractFrame P = AP, ΨP AP ♯* P
  obtain Ψ' AP' ΨP' where FrP': "extractFrame P' = AP', ΨP'" and "ΨP  Ψ'  ΨP'"
                       and "AP' ♯* P'" and "AP' ♯* C" and "distinct AP'"
    by(rule_tac TauStep)
  from Ψ  P' τ  P'' FrP' distinct AP' AP' ♯* P' AP' ♯* C
  obtain Ψ'' AP'' ΨP'' where FrP'': "extractFrame P'' = AP'', ΨP''" and "ΨP'  Ψ''  ΨP''"
                          and "AP'' ♯* P''" and "AP'' ♯* C" and "distinct AP''"
    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 AP'' ♯* P'' AP'' ♯* C distinct AP''
    by(rule TauStep)
qed

lemma frameIntImpComposition:
  fixes Ψ  :: 'b
  and   Ψ' :: 'b
  and   AF :: "name list"
  and   ΨF :: 'b

  assumes "Ψ  Ψ'"

  shows "AF, Ψ  ΨF F AF, Ψ'  Ψ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   AP :: "name list"
  and   ΨP :: 'b
  and   AF :: "name list"
  and   AG :: "name list"
  and   ΨG :: 'b

  assumes PChain: "ΨF  P ^τ P'"
  and     FrP: "extractFrame P = AP, ΨP"
  and     "distinct AP"
  and     FeqG: "Ψ. insertAssertion (AF, ΨF  ΨP) Ψ F insertAssertion (AG, ΨG  ΨP) Ψ"
  and     "AF ♯* ΨG"
  and     "AG ♯* Ψ"
  and     "AG ♯* ΨF"
  and     "AF ♯* AG"
  and     "AF ♯* P"
  and     "AG ♯* P"
  and     "AP ♯* AF"
  and     "AP ♯* AG"
  and     "AP ♯* ΨF"
  and     "AP ♯* ΨG"
  and     "AP ♯* P"

  shows "ΨG  P ^τ P'"
using PChain FrP AF ♯* P AG ♯* P AP ♯* P 
proof(induct rule: tauChainInduct2)
  case TauBase
  thus ?case by simp
next
  case(TauStep P P' P'')
  have FrP: "extractFrame P = AP, ΨP" by fact
  then have PChain: "ΨG  P ^τ P'" using AF ♯* P AG ♯* P AP ♯* P by(rule TauStep)
  then obtain AP' ΨP' Ψ' where FrP': "extractFrame P' = AP', ΨP'" and "ΨP  Ψ'  ΨP'"
                            and "AP' ♯* AF" and "AP' ♯* AG" and "AP' ♯* ΨF" and "AP' ♯* ΨG"
                            and "distinct AP'"
                
    using FrP distinct AP AP ♯* P AP ♯* AF AP ♯* AG AP ♯* ΨF AP ♯* ΨG
    by(rule_tac C="(AF, AG, ΨF, ΨG)" in expandTauChainFrame) auto

  from PChain AF ♯* P AG ♯* P have "AF ♯* P'" and "AG ♯* P'" by(blast dest: tauChainFreshChain)+

  with AF ♯* P AG ♯* P AP ♯* AF AP ♯* AGAP' ♯* AF AP' ♯* AG FrP FrP'
  have "AF ♯* ΨP" and "AG ♯* ΨP" and "AF ♯* ΨP'" and "AG ♯* ΨP'"
    by(auto dest: extractFrameFreshChain)

  from FeqG have FeqG: "insertAssertion (AF, ΨF  ΨP) Ψ' F insertAssertion (AG, ΨG  ΨP) Ψ'"
    by blast
  obtain p::"name prm" where "(p  AF) ♯* ΨF" and  "(p  AF) ♯* ΨP" and "(p  AF) ♯* ΨP'" and "(p  AF) ♯* Ψ'"
                         and Sp: "(set p)  set AF × set(p  AF)" and "distinctPerm p"
      by(rule_tac xvec=AF and c="(ΨF, ΨP, Ψ', ΨP')" in name_list_avoiding) auto
  obtain q::"name prm" where "(q  AG) ♯* ΨG" and  "(q  AG) ♯* ΨP" and "(q  AG) ♯* ΨP'" and "(q  AG) ♯* Ψ'"
                         and Sq: "(set q)  set AG × set(q  AG)" and "distinctPerm q"
    by(rule_tac xvec=AG and c="(ΨG, ΨP, Ψ', ΨP')" in name_list_avoiding) auto
  from ΨP  Ψ'  ΨP' have "(p  AF), ((p  ΨF)  ΨP') F (p  AF), (p  ΨF)  (ΨP  Ψ')"
    by(rule frameIntCompositionSym[OF AssertionStatEqSym])
  hence "(p  AF), (p  ΨF)  ΨP' F (p  AF), Ψ'  ((p  ΨF)  ΨP)"
    by(metis frameIntAssociativity FrameStatEqTrans frameIntCommutativity FrameStatEqSym)
  moreover from FeqG AF ♯* ΨP (p  AF) ♯* ΨP (p  AF) ♯* ΨF (p  AF) ♯* Ψ' Sp
  have "(p  AF), Ψ'  ((p  ΨF)  ΨP) F insertAssertion (AG, ΨG  ΨP) Ψ'"
    apply(erule_tac rev_mp) by(subst frameChainAlpha) (auto simp add: eqvts)
  hence "(p  AF), Ψ'  ((p  ΨF)  ΨP) F  ((q  AG), Ψ'  (q  ΨG)  ΨP)"
    using AG ♯* ΨP (q  AG) ♯* ΨP (q  AG) ♯* ΨG (q  AG) ♯* Ψ' Sq
    apply(