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

nominal_datatype 'a prefix =
  pInput "'a::fs_name" "name list" 'a
| pOutput 'a 'a                           
| pTau                                    

context tau
begin

nominal_primrec bindPrefix :: "'a prefix → ('a, 'b, 'c) psi → ('a, 'b, 'c) psi"  (‹_⋅_› [100, 100] 100)
where
  "bindPrefix (pInput M xvec N) P = M(λ*xvec N).P"
| "bindPrefix (pOutput M N) P = M⟨N⟩.P"
| "bindPrefix (pTau) P = τ.(P)"
by(rule TrueI)+

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

  shows "(p ∙ (α⋅P)) = (p ∙ α)⋅(p ∙ P)"
by(nominal_induct α rule: prefix.strong_inducts) (auto simp add: eqvts)

lemma prefixCases[consumes 1, case_names cInput cOutput cTau]:
  fixes Ψ :: 'b
  and   α  :: "'a prefix"
  and   P  :: "('a, 'b, 'c) psi"
  and   β  :: "'a action"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ α⋅P ⟼β ≺ P'"
  and     rInput: "∧M xvec N K Tvec. [Ψ ⊨ M ↔ K; set xvec ⊆ supp N; length xvec = length Tvec; distinct xvec] ==>
                                       Prop (pInput M xvec N) (K(N[xvec::=Tvec])) (P[xvec::=Tvec])"
  and     rOutput: "∧M N K. Ψ ⊨ M ↔ K ==> Prop (pOutput M N) (K⟨N⟩) P"
  and     rTau: "Ψ ⊳ P ∼ P' ==> Prop (pTau) (τ) P'"

  shows "Prop α β P'"
using ‹Ψ ⊳ α⋅P ⟼β ≺ P'›
proof(nominal_induct rule: prefix.strong_induct)
  case(pInput M xvec N)
  from ‹Ψ ⊳ (pInput M xvec N)⋅P ⟼β ≺ P'› have "Ψ ⊳ M(λ*xvec N).P ⟼β ≺ P'" by simp
  thus ?case by(auto elim: inputCases intro: rInput)
next
  case(pOutput M N)
  from ‹Ψ ⊳ (pOutput M N)⋅P ⟼β ≺ P'› have "Ψ ⊳ M⟨N⟩.P ⟼β ≺ P'" by simp
  thus ?case by(auto elim: outputCases intro: rOutput)
next
  case pTau
  from ‹Ψ ⊳ (pTau)⋅P ⟼β ≺ P'› have "Ψ ⊳ τ.(P) ⟼β ≺ P'" by simp
  thus ?case
    by(nominal_induct rule: action.strong_induct) (auto dest: tauActionE intro: rTau)
qed  
  
lemma prefixTauCases[consumes 1, case_names cTau]:
  fixes α  :: "'a prefix"
  and   P  :: "('a, 'b, 'c) psi"
  and   P' :: "('a, 'b, 'c) psi"

  assumes "Ψ ⊳ α⋅P ⟼τ ≺ P'"
  and     rTau: "Ψ ⊳ P ∼ P' ==> Prop (pTau) P'"

  shows "Prop α P'"
proof -
  from ‹Ψ ⊳ α⋅P ⟼τ ≺ P'› obtain β where "Ψ ⊳ α⋅P ⟼β ≺ P'" and "β = τ" 
    by auto
  thus ?thesis
    by(induct rule: prefixCases) (auto intro: rTau)
qed

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

  assumes "Ψ ⊳ P ↝<Rel> Q"
  and     C1: "∧Ψ P Q R. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel] ==> (Ψ, P, R) ∈ Rel"

  shows "Ψ ⊳ τ.(P) ↝«Rel¬ Q"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ ⊳ P ↝🚫 Q› ‹Ψ ⊳ Q ⟼τ ≺ Q'›
  obtain P' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
    by(blast dest: weakSimE)

  from PChain obtain P'' where "Ψ ⊳ τ.(P) ==>_\<tau> P''" and "Ψ ⊳ P' ∼ P''"
    by(rule tauChainStepCons)
  thus ?case using P'RelQ' by(metis bisimE C1)
qed

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

  assumes PTrans: "Ψ ⊳ P ⟼τ ≺ P'"
  and     P'RelQ: "(Ψ, P', Q) ∈ Rel"
  and     C1: "∧Ψ P Q R. [(Ψ, P, Q) ∈ Rel; Ψ ⊳ Q ∼ R] ==> (Ψ, P, R) ∈ Rel"

  shows "Ψ ⊳ P ↝«Rel¬ τ.(Q)"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ ⊳ τ.(Q) ⟼τ ≺ Q'› have "Ψ ⊳ Q ∼ Q'" by(blast dest: tauActionE)
  with PTrans P'RelQ show ?case by(metis C1 tauActTauStepChain)
qed

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

  assumes "Ψ ⊳ P ↝<Rel> Q"
  and     C1: "∧Q'. Ψ ⊳ Q ⟼τ ≺ Q' ==> (Ψ, P, Q') ∉ Rel"

  shows "Ψ ⊳ P ↝«Rel¬ Q"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ ⊳ P ↝🚫 Q› ‹Ψ ⊳ Q ⟼τ ≺ Q'›
  obtain P' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
    by(blast dest: weakSimE)
  with C1 ‹Ψ ⊳ Q ⟼τ ≺ Q'› show ?case 
    by(force simp add: rtrancl_eq_or_trancl)
qed

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

  assumes "Ψ ⊳ P ↝<Rel> Q"
  and     "eqvt Rel"
  and     C1: "∧Ψ P Q R. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel] ==> (Ψ, P, R) ∈ Rel"

  shows "Ψ ⊳ τ.(P) ↝<Rel> Q"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α Q')
  from ‹bn α ♯* (τ.(P))› have "bn α ♯* P" by simp
  with ‹Ψ ⊳ P ↝🚫 Q› ‹Ψ ⊳ Q ⟼α ≺ Q'› ‹bn α ♯* Ψ› ‹α ≠ τ›
  obtain P'' P' where PTrans: "Ψ : Q ⊳ P ==>α ≺ P''" and P''Chain: "Ψ ⊗ Ψ' ⊳ P'' ==>^{^}_\<tau> P'"
                  and P'RelQ': "(Ψ ⊗ Ψ', P', Q') ∈ Rel"
    by(blast dest: weakSimE)

  from PTrans ‹bn α ♯* Ψ› ‹bn α ♯* P› obtain P''' where "Ψ : Q ⊳ τ.(P) ==>α ≺ P'''" and "Ψ ⊳ P'' ∼ P'''"
    by(rule weakTransitionTau)
  moreover from ‹Ψ ⊳ P'' ∼ P'''› have "Ψ ⊗ Ψ' ⊳ P'' ∼ P'''" by(rule bisimE)
  with P''Chain obtain P'''' where "Ψ ⊗ Ψ' ⊳ P''' ==>^{^}_\<tau> P''''" and "Ψ ⊗ Ψ' ⊳ P' ∼ P''''"
    by(rule tauChainBisim)
  ultimately show ?case using ‹(Ψ ⊗ Ψ', P', Q') ∈ Rel› by(metis bisimE C1)
next
  case(cTau Q')
  from ‹Ψ ⊳ P ↝🚫 Q› ‹Ψ ⊳ Q ⟼τ ≺ Q'›
  obtain P' where PChain: "Ψ ⊳ P ==>^{^}_\<tau> P'" and P'RelQ': "(Ψ, P', Q') ∈ Rel"
    by(blast dest: weakSimE)

  from PChain obtain P'' where "Ψ ⊳ τ.(P) ==>^{^}_\<tau> P''" and "Ψ ⊳ P' ∼ P''"
    by(rule tauChainCons)
  thus ?case using P'RelQ' by(metis bisimE C1)  
qed

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

  assumes "eqvt Rel"
  and     "(Ψ, P, Q) ∈ Rel"
  and     C1: "∧Ψ P Q R. [(Ψ, P, Q) ∈ Rel; Ψ ⊳ Q ∼ R] ==> (Ψ, P, R) ∈ Rel"

  shows "Ψ ⊳ P ↝<Rel> τ.(Q)"
using ‹eqvt Rel›
proof(induct rule: weakSimI[where C=Q])
  case(cAct Ψ' α Q')
  hence False by(cases rule: actionCases[where α=α]) auto
  thus ?case by simp
next
  case(cTau Q')
  have "Ψ ⊳ Q ==>^{^}_\<tau> Q" by simp
  moreover from ‹Ψ ⊳ τ.(Q) ⟼τ ≺ Q'› have "Ψ ⊳ Q ∼ Q'" by(rule tauActionE)
  with ‹(Ψ, P, Q) ∈ Rel› have "(Ψ, P, Q') ∈ Rel" by(rule C1)
  ultimately show ?case by blast
qed

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

  assumes "eqvt Rel"
  and     "(Ψ, P, Q) ∈ Rel"
  and     Subst: "∧xvec Tvec. length xvec = length Tvec ==> (Ψ, P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel"
  and     C1: "∧Ψ P Q R S. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel; Ψ ⊳ R ∼ S] ==> (Ψ, P, S) ∈ Rel"
  and     rExt: "∧Ψ P Q Ψ'. (Ψ, P, Q) ∈ Rel ==> (Ψ ⊗ Ψ', P, Q) ∈ Rel"

  shows "Ψ ⊳ α⋅(τ.(P)) ↝<Rel> α⋅Q"
using ‹eqvt Rel›
proof(induct rule: weakSimI[where C=Q])
  case(cAct Ψ' β Q')
  from ‹Ψ ⊳ α⋅Q ⟼β ≺ Q'› ‹β ≠ τ› show ?case
  proof(induct rule: prefixCases)
    case(cInput M xvec N K Tvec)
    note ‹Ψ ⊨ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
    moreover have "insertAssertion (extractFrame(M(λ*xvec N).Q)) Ψ ↪_F ⟨ε, Ψ ⊗ 1⟩" by auto
    ultimately have "Ψ : (M(λ*xvec N).Q) ⊳ (M(λ*xvec N).(τ.(P))) ==>K((N[xvec::=Tvec])) ≺ (τ.(P))[xvec::=Tvec]" 
      by(rule weakInput)
    hence "Ψ : (M(λ*xvec N).Q) ⊳ (M(λ*xvec N).(τ.(P))) ==>K((N[xvec::=Tvec])) ≺ τ.(P[xvec::=Tvec])"
      using ‹length xvec = length Tvec› ‹distinct xvec›
      by simp
      
    moreover obtain P' where PTrans: "Ψ ⊗ Ψ' ⊳ τ.(P[xvec::=Tvec]) ⟼τ ≺ P'" and "Ψ ⊗ Ψ' ⊳ (P[xvec::=Tvec]) ∼ P'" using tauActionI
      by auto
    from PTrans have "Ψ ⊗ Ψ' ⊳ τ.(P[xvec::=Tvec]) ==>^{^}_\<tau> P'" by(rule tauActTauChain)
    moreover from ‹length xvec = length Tvec› have "(Ψ, P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel" by(rule Subst)
    hence "(Ψ ⊗ Ψ', P[xvec::=Tvec], Q[xvec::=Tvec]) ∈ Rel" by(rule rExt)
    with ‹Ψ ⊗ Ψ' ⊳ P[xvec::=Tvec] ∼ P'› have "(Ψ ⊗ Ψ', P', Q[xvec::=Tvec]) ∈ Rel" by(blast intro: bisimE C1 bisimReflexive)
    ultimately show ?case by fastforce
  next
    case(cOutput M N K)
    note ‹Ψ ⊨ M ↔ K›
    moreover have "insertAssertion (extractFrame (M⟨N⟩.Q)) Ψ ↪_F ⟨ε, Ψ ⊗ 1⟩" by auto
    ultimately have "Ψ : M⟨N⟩.Q ⊳ M⟨N⟩.(τ.(P)) ==>K⟨N⟩ ≺ τ.(P)" by(rule weakOutput)
    moreover obtain P' where PTrans: "Ψ ⊗ Ψ' ⊳ τ.(P) ⟼τ ≺ P'" and "Ψ ⊗ Ψ' ⊳ P ∼ P'" using tauActionI
      by auto
    from PTrans have "Ψ ⊗ Ψ' ⊳ τ.(P) ==>^{^}_\<tau> P'" by(rule tauActTauChain)
    moreover from ‹(Ψ, P, Q) ∈ Rel› have "(Ψ ⊗ Ψ', P, Q) ∈ Rel" by(rule rExt)
    with ‹Ψ ⊗ Ψ' ⊳ P ∼ P'› have "(Ψ ⊗ Ψ', P', Q) ∈ Rel" by(blast intro: bisimE C1 bisimReflexive)
    ultimately show ?case by fastforce
  next
    case cTau
    with ‹τ ≠ τ› show ?case
      by simp
  qed
next
  case(cTau Q')
  from ‹Ψ ⊳ α⋅Q ⟼τ ≺ Q'› show ?case
  proof(induct rule: prefixTauCases)
    case cTau
    obtain P' where tPTrans: "Ψ ⊳ τ.(τ.(P)) ⟼τ ≺ P'" and "Ψ ⊳ τ.(P) ∼ P'" using tauActionI
      by auto
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    from PTrans ‹Ψ ⊳ τ.(P) ∼ P'› obtain P''' where P'Trans: "Ψ ⊳ P' ⟼τ ≺ P'''" and "Ψ ⊳ P'' ∼ P'''"
      apply(drule_tac bisimE(4))
      apply(drule_tac bisimE(2))
      apply(drule_tac simE, auto)
      by(metis bisimE)
    from tPTrans P'Trans have "Ψ ⊳ τ.(τ.(P)) ==>^{^}_\<tau> P'''" by(fastforce dest: tauActTauChain)
    moreover from ‹(Ψ, P, Q) ∈ Rel› ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P'' ∼ P'''› ‹Ψ ⊳ Q ∼ Q'› have "(Ψ, P''', Q') ∈ Rel"
      by(metis bisimTransitive C1 bisimSymmetric)
    ultimately show ?case by fastforce
  qed
qed

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

  assumes "eqvt Rel"
  and     Subst: "∧Ψ xvec Tvec. length xvec = length Tvec ==> (Ψ, P[xvec::=Tvec], τ.(Q[xvec::=Tvec])) ∈ Rel"
  and     C1: "∧Ψ P Q R S. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel; Ψ ⊳ R ∼ S] ==> (Ψ, P, S) ∈ Rel"
  and     "∧Ψ. (Ψ, P, τ.(Q)) ∈ Rel"

  shows "Ψ ⊳ α⋅P ↝<Rel> α⋅(τ.(Q))"
using ‹eqvt Rel›
proof(induct rule: weakSimI[where C=Q])
  case(cAct Ψ' β Q')
  from ‹Ψ ⊳ α⋅(τ.(Q)) ⟼β ≺ Q'› ‹β ≠ τ›
  show ?case
  proof(induct rule: prefixCases)
    case(cInput M xvec N K Tvec)
    note ‹Ψ ⊨ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec=length Tvec›
    moreover have "insertAssertion (extractFrame (M(λ*xvec N).(τ.(Q)))) Ψ ↪_F ⟨ε, Ψ ⊗ 1⟩" by auto
    ultimately have "Ψ : (M(λ*xvec N).(τ.(Q))) ⊳ M(λ*xvec N).P ==>K((N[xvec::=Tvec])) ≺ P[xvec::=Tvec]"
      by(rule weakInput)
    moreover have "Ψ ⊗ Ψ' ⊳ P[xvec::=Tvec] ==>^{^}_\<tau> P[xvec::=Tvec]" by auto
    ultimately show ?case using Subst ‹length xvec=length Tvec› ‹distinct xvec›
      by fastforce
  next
    case(cOutput M N K)
    note ‹Ψ ⊨ M ↔ K›
    moreover have "insertAssertion (extractFrame (M⟨N⟩.(τ.(Q)))) Ψ ↪_F ⟨ε, Ψ ⊗ 1⟩" by auto
    ultimately have "Ψ : M⟨N⟩.(τ.(Q)) ⊳ M⟨N⟩.P ==>K⟨N⟩ ≺ P" by(rule weakOutput)
    moreover have "Ψ ⊗ Ψ' ⊳ P ==>^{^}_\<tau> P" by auto
    ultimately show ?case using ‹(Ψ ⊗ Ψ', P, τ.(Q)) ∈ Rel› by fastforce
  next
    case cTau
    with ‹τ ≠ τ› show ?case by simp
  qed
next
  case(cTau Q')
  from ‹Ψ ⊳ α⋅(τ.(Q)) ⟼τ ≺ Q'› show ?case
  proof(induct rule: prefixTauCases)
    case cTau
    obtain P' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P'" and "Ψ ⊳ P ∼ P'" using tauActionI
      by auto
    from PTrans have "Ψ ⊳ τ.(P) ==>^{^}_\<tau> P'" by(rule tauActTauChain)
    moreover from ‹Ψ ⊳ P ∼ P'› ‹Ψ ⊳ τ.(Q) ∼ Q'›  ‹(Ψ, P, τ.(Q)) ∈ Rel›
    have "(Ψ, P', Q') ∈ Rel" by(metis bisimTransitive bisimSymmetric C1)
    ultimately show ?case by fastforce
  qed
qed

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

  assumes "(Ψ, P, Q) ∈ Rel"
  and     C1: "∧Ψ P Q R S. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel; Ψ ⊳ R ∼ S] ==> (Ψ, P, S) ∈ Rel"
  and     rExt: "∧Ψ P Q Ψ'. (Ψ, P, Q) ∈ Rel ==> (Ψ ⊗ Ψ', P, Q) ∈ Rel"

  shows "Ψ ⊳ α⋅(τ.(P)) ↝«Rel¬ α⋅Q"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ ⊳ α⋅Q ⟼τ ≺ Q'› show ?case
  proof(induct rule: prefixTauCases)
    case cTau
    obtain P' where tPTrans: "Ψ ⊳ τ.(τ.(P)) ⟼τ ≺ P'" and "Ψ ⊳ τ.(P) ∼ P'" using tauActionI
      by auto
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    from PTrans ‹Ψ ⊳ τ.(P) ∼ P'› obtain P''' where P'Trans: "Ψ ⊳ P' ⟼τ ≺ P'''" and "Ψ ⊳ P'' ∼ P'''"
      apply(drule_tac bisimE(4))
      apply(drule_tac bisimE(2))
      apply(drule_tac simE, auto)
      by(metis bisimE)
    from tPTrans P'Trans have "Ψ ⊳ τ.(τ.(P)) ==>_\<tau> P'''" by(fastforce dest: tauActTauStepChain)
    moreover from ‹(Ψ, P, Q) ∈ Rel› ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P'' ∼ P'''› ‹Ψ ⊳ Q ∼ Q'› have "(Ψ, P''', Q') ∈ Rel"
      by(metis bisimTransitive C1 bisimSymmetric)
    ultimately show ?case by fastforce
  qed
qed

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

  assumes "(Ψ, P, Q) ∈ Rel"
  and     C1: "∧Ψ P Q R S. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel; Ψ ⊳ R ∼ S] ==> (Ψ, P, S) ∈ Rel"
  and     "∧Ψ. (Ψ, P, τ.(Q)) ∈ Rel"

  shows "Ψ ⊳ α⋅P ↝«Rel¬ α⋅(τ.(Q))"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ ⊳ α⋅(τ.(Q)) ⟼τ ≺ Q'› show ?case
  proof(induct rule: prefixTauCases)
    case cTau
    obtain P' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P'" and "Ψ ⊳ P ∼ P'" using tauActionI
      by auto
    from PTrans have "Ψ ⊳ τ.(P) ==>_\<tau> P'" by(rule tauActTauStepChain)
    moreover from ‹Ψ ⊳ P ∼ P'› ‹Ψ ⊳ τ.(Q) ∼ Q'›  ‹(Ψ, P, τ.(Q)) ∈ Rel›
    have "(Ψ, P', Q') ∈ Rel" by(metis bisimTransitive bisimSymmetric C1)
    ultimately show ?case by fastforce
  qed
qed

end

locale tauSum = tau + sum
begin

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

  assumes Id: "∧Ψ P. (Ψ, P, P) ∈ Rel"
  and     C1: "∧Ψ P Q R S. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel; Ψ ⊳ R ∼ S] ==> (Ψ, P, S) ∈ Rel"

  shows "Ψ ⊳ P ⊕ τ.(P) ↝<Rel> τ.(P)"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α P')
  thus ?case by(nominal_induct α rule: action.strong_inducts) auto
next
  case(cTau P')
  from ‹Ψ ⊳ τ.(P) ⟼τ ≺ P'› have "Ψ ⊳ P ∼ P'" by(rule tauActionE)
  obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
    by auto
  have "guarded(τ.(P))" by(rule guardedTau)
  with PTrans have "Ψ ⊳ P ⊕ τ.(P) ⟼τ ≺ P''" by(rule Sum2)
  hence "Ψ ⊳ P ⊕ τ.(P) ==>^{^}_\<tau> P''" by(rule tauActTauChain)
  moreover from ‹Ψ ⊳ P ∼ P''› ‹(Ψ, P, P) ∈ Rel› ‹Ψ ⊳ P ∼ P'› have "(Ψ, P'', P') ∈ Rel"
    by(metis C1 bisimE)
  ultimately show ?case by blast
qed  

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

  assumes Id: "∧Ψ P. (Ψ, P, P) ∈ Rel"
  and     C1: "∧Ψ P Q R S. [Ψ ⊳ P ∼ Q; (Ψ, Q, R) ∈ Rel; Ψ ⊳ R ∼ S] ==> (Ψ, P, S) ∈ Rel"

  shows "Ψ ⊳ P ⊕ τ.(P) ↝«Rel¬ τ.(P)"
proof(induct rule: weakCongSimI)
  case(cTau P')
  from ‹Ψ ⊳ τ.(P) ⟼τ ≺ P'› have "Ψ ⊳ P ∼ P'" by(rule tauActionE)
  obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
    by auto
  have "guarded(τ.(P))" by(rule guardedTau)
  with PTrans have "Ψ ⊳ P ⊕ τ.(P) ⟼τ ≺ P''" by(rule Sum2)
  hence "Ψ ⊳ P ⊕ τ.(P) ==>_\<tau> P''" by(rule tauActTauStepChain)
  moreover from ‹Ψ ⊳ P ∼ P''› ‹(Ψ, P, P) ∈ Rel› ‹Ψ ⊳ P ∼ P'› have "(Ψ, P'', P') ∈ Rel"
    by(metis C1 bisimE)
  ultimately show ?case by blast
qed  

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

  assumes C1: "∧Ψ P Q. Ψ ⊳ P ∼ Q ==> (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ τ.(P) ↝<Rel> P ⊕ τ.(P)"
proof(induct rule: weakSimI2)
  case(cAct Ψ' α P')
  from ‹Ψ ⊳ P ⊕ τ.(P) ⟼α ≺ P'›
  show ?case
  proof(induct rule: sumCases)
    case cSum1 
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    from PTrans have "Ψ ⊳ τ.(P) ==>^{^}_\<tau> P''" by(rule tauActTauChain)
    moreover from ‹guarded P› have "insertAssertion (extractFrame P) Ψ ≃_F ⟨ε, Ψ ⊗ 1⟩"
      by(rule insertGuardedAssertion)
    with ‹Ψ ⊳ P ∼ P''› have "insertAssertion (extractFrame P'') Ψ ≃_F ⟨ε, Ψ ⊗ 1⟩"
      by(metis bisimE FrameStatEqTrans FrameStatEqSym)
    hence "insertAssertion (extractFrame(P ⊕ τ.(P))) Ψ ↪_F insertAssertion (extractFrame P'') Ψ"
      by(simp add: FrameStatEq_def)
    moreover from PTrans ‹bn α ♯* (τ.(P))› have "bn α ♯* P''" by(rule tauFreshChainDerivative)
    with ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P ⟼α ≺ P'› ‹bn α ♯* Ψ›
    obtain P''' where P''Trans: "Ψ ⊳ P'' ⟼α ≺ P'''" and "Ψ ⊳ P''' ∼ P'"
      by(metis bisimE simE)
    ultimately have "Ψ : (P ⊕ τ.(P)) ⊳ τ.(P) ==>α ≺ P'''"
      by(rule_tac weakTransitionI)
    moreover have "Ψ ⊗ Ψ' ⊳ P''' ==>^{^}_\<tau> P'''" by auto
    moreover from ‹Ψ ⊳ P''' ∼ P'› have "Ψ ⊗ Ψ' ⊳ P''' ∼ P'" by(rule bisimE)
    hence "(Ψ ⊗ Ψ', P''', P') ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case cSum2
    thus ?case using ‹α ≠ τ›
      by(nominal_induct α rule: action.strong_inducts) auto
  qed
next
  case(cTau P')
  from ‹Ψ ⊳ P ⊕ τ.(P) ⟼τ ≺ P'›
  show ?case
  proof(induct rule: sumCases)
    case cSum1 
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    moreover from ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P ⟼τ ≺ P'›
    obtain P''' where P''Trans: "Ψ ⊳ P'' ⟼τ ≺ P'''" and "Ψ ⊳ P''' ∼ P'"
      apply(drule_tac bisimE(4))
      apply(drule_tac bisimE(2))
      by(drule_tac simE, auto)
    ultimately have "Ψ ⊳ τ.(P) ==>^{^}_\<tau> P'''" by(auto dest: tauActTauChain rtrancl_into_rtrancl)
    moreover from ‹Ψ ⊳ P''' ∼ P'› have "(Ψ, P''', P') ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case cSum2
    from ‹Ψ ⊳ τ.(P) ⟼τ ≺ P'› have "Ψ ⊳ P ∼ P'" by(rule tauActionE)
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    hence "Ψ ⊳ τ.(P) ==>^{^}_\<tau> P''" by(rule_tac tauActTauChain)
    moreover from ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P ∼ P'› have "(Ψ, P'', P') ∈ Rel"
      by(metis C1 bisimTransitive bisimE)
    ultimately show ?case by blast
  qed
qed

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

  assumes C1: "∧Ψ P Q. Ψ ⊳ P ∼ Q ==> (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ τ.(P) ↝«Rel¬ P ⊕ τ.(P)"
proof(induct rule: weakCongSimI)
  case(cTau P')
  from ‹Ψ ⊳ P ⊕ τ.(P) ⟼τ ≺ P'›
  show ?case
  proof(induct rule: sumCases)
    case cSum1 
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    moreover from ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P ⟼τ ≺ P'›
    obtain P''' where P''Trans: "Ψ ⊳ P'' ⟼τ ≺ P'''" and "Ψ ⊳ P''' ∼ P'"
      apply(drule_tac bisimE(4))
      apply(drule_tac bisimE(2))
      by(drule_tac simE) auto
    ultimately have "Ψ ⊳ τ.(P) ==>_\<tau> P'''" by(auto dest: tauActTauStepChain trancl_into_trancl)
    moreover from ‹Ψ ⊳ P''' ∼ P'› have "(Ψ, P''', P') ∈ Rel" by(rule C1)
    ultimately show ?case by blast
  next
    case cSum2
    from ‹Ψ ⊳ τ.(P) ⟼τ ≺ P'› have "Ψ ⊳ P ∼ P'" by(rule tauActionE)
    obtain P'' where PTrans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
      by auto
    hence "Ψ ⊳ τ.(P) ==>_\<tau> P''" by(rule_tac tauActTauStepChain)
    moreover from ‹Ψ ⊳ P ∼ P''› ‹Ψ ⊳ P ∼ P'› have "(Ψ, P'', P') ∈ Rel"
      by(metis C1 bisimTransitive bisimE)
    ultimately show ?case by blast
  qed
qed

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

  assumes "∧Ψ P. (Ψ, P, P) ∈ Rel"
  and     C1: "∧Ψ P Q. Ψ ⊳ P ∼ Q ==> (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ↝<Rel> α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakSimI2)
  case(cAct Ψ' β PQ)
  from ‹Ψ ⊳ α⋅(τ.(P) ⊕ Q) ⟼β ≺ PQ› ‹β ≠ τ›
  show ?case
  proof(induct rule: prefixCases)
    case(cInput M xvec N K Tvec)
    have "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ==>^{^}_\<tau> α⋅P ⊕ α⋅(τ.(P) ⊕ Q)" by auto
    moreover have "insertAssertion (extractFrame(α⋅(τ.(P) ⊕ Q))) Ψ ↪_F insertAssertion (extractFrame(α⋅P ⊕ α⋅(τ.(P) ⊕ Q))) Ψ"
      using insertTauAssertion Identity
      by(nominal_induct α rule: prefix.strong_inducts, auto) 
        (rule FrameStatImpTrans[where G="⟨ε, Ψ⟩"], auto simp add: FrameStatEq_def AssertionStatEq_def)
    moreover from ‹Ψ ⊨ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec=length Tvec›
    have "Ψ ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ⟼K((N[xvec::=Tvec])) ≺ (τ.(P) ⊕ Q)[xvec::=Tvec]"
      by(rule Input)
    hence "Ψ ⊳ (M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q) ⟼K((N[xvec::=Tvec])) ≺ (τ.(P) ⊕ Q)[xvec::=Tvec]" 
      by(rule_tac Sum2) auto
    ultimately have "Ψ : (M(λ*xvec N).(τ.(P) ⊕ Q)) ⊳ (M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q) ==>K((N[xvec::=Tvec])) ≺ (τ.(P) ⊕ Q)[xvec::=Tvec]"
      by(rule_tac weakTransitionI) auto
    moreover have "Ψ ⊗ Ψ' ⊳ (τ.(P) ⊕ Q)[xvec::=Tvec] ==>^{^}_\<tau> (τ.(P) ⊕ Q)[xvec::=Tvec]" by auto
    ultimately show ?case using ‹(Ψ ⊗ Ψ', (τ.(P) ⊕ Q)[xvec::=Tvec], (τ.(P) ⊕ Q)[xvec::=Tvec]) ∈ Rel› by fastforce
  next
    case(cOutput M N K)
    have "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ==>^{^}_\<tau> α⋅P ⊕ α⋅(τ.(P) ⊕ Q)" by auto
    moreover have "insertAssertion (extractFrame(α⋅(τ.(P) ⊕ Q))) Ψ ↪_F insertAssertion (extractFrame(α⋅P ⊕ α⋅(τ.(P) ⊕ Q))) Ψ"
      using insertTauAssertion Identity
      by(nominal_induct α rule: prefix.strong_inducts, auto) 
        (rule FrameStatImpTrans[where G="⟨ε, Ψ⟩"], auto simp add: FrameStatEq_def AssertionStatEq_def)

    moreover from ‹Ψ ⊨ M ↔ K› have "Ψ ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ⟼K⟨N⟩ ≺ (τ.(P) ⊕ Q)"
      by(rule Output)
    hence "Ψ ⊳ M⟨N⟩.P ⊕ M⟨N⟩.(τ.(P) ⊕ Q) ⟼K⟨N⟩ ≺ (τ.(P) ⊕ Q)" by(rule_tac Sum2) auto
    ultimately have "Ψ : (M⟨N⟩.(τ.(P) ⊕ Q)) ⊳ M⟨N⟩.P ⊕ M⟨N⟩.(τ.(P) ⊕ Q) ==>K⟨N⟩ ≺ (τ.(P) ⊕ Q)"
      by(rule_tac weakTransitionI) auto
    moreover have "Ψ ⊗ Ψ' ⊳ τ.(P) ⊕ Q ==>^{^}_\<tau> τ.(P) ⊕ Q" by auto
    ultimately show ?case using ‹(Ψ ⊗ Ψ', τ.(P) ⊕ Q, τ.(P) ⊕ Q) ∈ Rel› by fastforce
  next
    case cTau
    from ‹τ ≠ τ› show ?case
      by simp
  qed
next
  case(cTau Q')
  from ‹Ψ ⊳ α⋅(τ.(P)) ⊕_\⊤ Q ⟼ τ ≺ Q'› show ?case
  proof(induct rule: prefixTauCases)
    case cTau
    obtain P' where PTrans: "Ψ ⊳ τ.(τ.(P) ⊕ Q) ⟼τ ≺ P'" and "Ψ ⊳ τ.(P) ⊕ Q ∼ P'" using tauActionI
      by auto
    from PTrans have "Ψ ⊳ (τ.(P)) ⊕ τ.(τ.(P) ⊕ Q) ⟼τ ≺ P'" by(rule_tac Sum2) (auto intro: guardedTau)
    hence "Ψ ⊳ (τ.(P)) ⊕ τ.(τ.(P) ⊕ Q) ==>^{^}_\<tau> P'" by(rule tauActTauChain)
    moreover from ‹Ψ ⊳ τ.(P) ⊕ Q ∼ P'› ‹Ψ ⊳ (τ.(P)) ⊕ Q ∼ Q'› have "Ψ ⊳ P' ∼ Q'" by(metis bisimSymmetric bisimTransitive)
    hence "(Ψ, P', Q') ∈ Rel" by(rule C1)
    ultimately show ?case by fastforce
  qed
qed

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

  assumes "∧Ψ P. (Ψ, P, P) ∈ Rel"
  and     C1: "∧Ψ P Q. Ψ ⊳ P ∼ Q ==> (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ↝«Rel¬ α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakCongSimI)
  case(cTau Q')
  from ‹Ψ ⊳ α⋅(τ.(P)) ⊕_\⊤ Q ⟼ τ ≺ Q'› show ?case
  proof(induct rule: prefixTauCases)
    case cTau
    obtain P' where PTrans: "Ψ ⊳ τ.(τ.(P) ⊕ Q) ⟼τ ≺ P'" and "Ψ ⊳ τ.(P) ⊕ Q ∼ P'" using tauActionI
      by auto
    from PTrans have "Ψ ⊳ (τ.(P)) ⊕ τ.(τ.(P) ⊕ Q) ⟼τ ≺ P'" by(rule_tac Sum2) (auto intro: guardedTau)
    hence "Ψ ⊳ (τ.(P)) ⊕ τ.(τ.(P) ⊕ Q) ==>_\<tau> P'" by(rule tauActTauStepChain)
    moreover from ‹Ψ ⊳ τ.(P) ⊕ Q ∼ P'› ‹Ψ ⊳ (τ.(P)) ⊕ Q ∼ Q'› have "Ψ ⊳ P' ∼ Q'" by(metis bisimSymmetric bisimTransitive)
    hence "(Ψ, P', Q') ∈ Rel" by(rule C1)
    ultimately show ?case by fastforce
  qed
qed

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

  assumes C1: "∧Ψ P Q. Ψ ⊳ P ∼ Q ==> (Ψ, P, Q) ∈ Rel"
  and         "∧Ψ P. (Ψ, P, P) ∈ Rel"

  shows "Ψ ⊳ α⋅(τ.(P) ⊕ Q) ↝<Rel> α⋅P ⊕ α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakSimI2)
  case(cAct Ψ' β PQ)
  from ‹Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⟼β ≺ PQ› show ?case
  proof(induct rule: sumCases)
    case cSum1
    from ‹Ψ ⊳ α⋅P ⟼β ≺ PQ› ‹β ≠ τ› show ?case
    proof(induct rule: prefixCases)
      case(cInput M xvec N K Tvec)
      have "Ψ ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ==>^{^}_\<tau> M(λ*xvec N).(τ.(P) ⊕ Q)" by auto
      moreover have "insertAssertion (extractFrame((M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q))) Ψ ↪_F insertAssertion (extractFrame(M(λ*xvec N).(τ.(P) ⊕ Q))) Ψ"
        by auto
      moreover from ‹Ψ ⊨ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
      have "Ψ ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ⟼K((N[xvec::=Tvec])) ≺ (τ.(P) ⊕ Q)[xvec::=Tvec]" by(rule Input)
      ultimately have "Ψ : ((M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q)) ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ==>K((N[xvec::=Tvec]))≺ (τ.(P) ⊕ Q)[xvec::=Tvec]"
        by(rule_tac weakTransitionI) auto
      with ‹length xvec = length Tvec› ‹distinct xvec›
      have "Ψ : ((M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q)) ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ==>K((N[xvec::=Tvec])) ≺ (τ.(P[xvec::=Tvec]) ⊕ Q[xvec::=Tvec])"
        by auto
      moreover obtain P' where PTrans: "Ψ ⊗ Ψ' ⊳ τ.(P[xvec::=Tvec]) ⟼τ ≺ P'" and "Ψ ⊗ Ψ' ⊳ P[xvec::=Tvec] ∼ P'" using tauActionI
        by auto
      have "guarded(τ.(P[xvec::=Tvec]))" by(rule guardedTau)
      with PTrans have "Ψ ⊗ Ψ' ⊳ (τ.(P[xvec::=Tvec])) ⊕ (Q[xvec::=Tvec]) ⟼τ ≺ P'" by(rule Sum1)
      hence "Ψ ⊗ Ψ' ⊳ (τ.(P[xvec::=Tvec])) ⊕ (Q[xvec::=Tvec]) ==>^{^}_\<tau> P'" by(rule tauActTauChain)
      moreover from ‹Ψ ⊗ Ψ' ⊳ P[xvec::=Tvec] ∼ P'› have "(Ψ ⊗ Ψ', P', P[xvec::=Tvec]) ∈ Rel" by(metis bisimE C1)
      ultimately show ?case by fastforce
    next
      case(cOutput M N K)
      have "Ψ ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ==>^{^}_\<tau> M⟨N⟩.(τ.(P) ⊕ Q)" by auto
      moreover have "insertAssertion (extractFrame(M⟨N⟩.P ⊕ M⟨N⟩.(τ.(P) ⊕ Q))) Ψ ↪_F insertAssertion (extractFrame(M⟨N⟩.(τ.(P) ⊕ Q))) Ψ"
        by auto
      moreover from ‹Ψ ⊨ M ↔ K› have "Ψ ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ⟼K⟨N⟩ ≺ (τ.(P) ⊕ Q)" by(rule Output)
      ultimately have "Ψ : (M⟨N⟩.P ⊕ M⟨N⟩.(τ.(P) ⊕ Q)) ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ==>K⟨N⟩ ≺ (τ.(P) ⊕ Q)"
        by(rule_tac weakTransitionI) auto
      moreover obtain P' where PTrans: "Ψ ⊗ Ψ' ⊳ τ.(P) ⟼τ ≺ P'" and "Ψ ⊗ Ψ' ⊳ P ∼ P'" using tauActionI
        by auto
      have "guarded(τ.(P))" by(rule guardedTau)
      with PTrans have "Ψ ⊗ Ψ' ⊳ (τ.(P)) ⊕ Q ⟼τ ≺ P'" by(rule Sum1)
      hence "Ψ ⊗ Ψ' ⊳ (τ.(P)) ⊕ Q ==>^{^}_\<tau> P'" by(rule tauActTauChain)
      moreover from ‹Ψ ⊗ Ψ' ⊳ P ∼ P'› have "(Ψ ⊗ Ψ', P', P) ∈ Rel" by(metis bisimE C1)
      ultimately show ?case by fastforce 
    next
      case cTau
      from ‹τ ≠ τ› show ?case by simp
    qed
  next
    case cSum2
    from ‹Ψ ⊳ α⋅(τ.(P) ⊕ Q) ⟼β ≺ PQ› ‹β ≠ τ› show ?case
    proof(induct rule: prefixCases)
      case(cInput M xvec N K Tvec)
      have "Ψ ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ==>^{^}_\<tau> M(λ*xvec N).(τ.(P) ⊕ Q)" by auto
      moreover have "insertAssertion (extractFrame((M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q))) Ψ ↪_F insertAssertion (extractFrame(M(λ*xvec N).(τ.(P) ⊕ Q))) Ψ"
        by auto
      moreover from ‹Ψ ⊨ M ↔ K› ‹distinct xvec› ‹set xvec ⊆ supp N› ‹length xvec = length Tvec›
      have "Ψ ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ⟼K((N[xvec::=Tvec])) ≺ (τ.(P) ⊕ Q)[xvec::=Tvec]"
        by(rule Input)
      with ‹length xvec = length Tvec› ‹distinct xvec›
      have "Ψ ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ⟼K((N[xvec::=Tvec])) ≺ (τ.(P[xvec::=Tvec]) ⊕ Q[xvec::=Tvec])"
        by simp
      ultimately have "Ψ : ((M(λ*xvec N).P) ⊕ M(λ*xvec N).(τ.(P) ⊕ Q)) ⊳ M(λ*xvec N).(τ.(P) ⊕ Q) ==>K((N[xvec::=Tvec])) ≺ (τ.(P[xvec::=Tvec]) ⊕ Q[xvec::=Tvec])"
        by(rule_tac weakTransitionI) auto
      moreover have "Ψ ⊗ Ψ' ⊳ τ.(P[xvec::=Tvec]) ⊕ (Q[xvec::=Tvec]) ==>^{^}_\<tau> τ.(P[xvec::=Tvec]) ⊕ (Q[xvec::=Tvec])" by auto
      ultimately show ?case using ‹(Ψ ⊗ Ψ', τ.(P[xvec::=Tvec]) ⊕ (Q[xvec::=Tvec]), τ.(P[xvec::=Tvec]) ⊕ (Q[xvec::=Tvec])) ∈ Rel› ‹length xvec = length Tvec› ‹distinct xvec›
        by fastforce
    next
      case(cOutput M N K)
      have "Ψ ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ==>^{^}_\<tau> M⟨N⟩.(τ.(P) ⊕ Q)" by auto
      moreover have "insertAssertion (extractFrame(M⟨N⟩.P ⊕ M⟨N⟩.(τ.(P) ⊕ Q))) Ψ ↪_F insertAssertion (extractFrame(M⟨N⟩.(τ.(P) ⊕ Q))) Ψ"
        by auto
      moreover from ‹Ψ ⊨ M ↔ K› have "Ψ ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ⟼K⟨N⟩ ≺ (τ.(P) ⊕ Q)"
        by(rule Output)
      ultimately have "Ψ : (M⟨N⟩.P ⊕ M⟨N⟩.(τ.(P) ⊕ Q)) ⊳ M⟨N⟩.(τ.(P) ⊕ Q) ==>K⟨N⟩ ≺ (τ.(P) ⊕ Q)"
        by(rule_tac weakTransitionI) auto
      moreover have "Ψ ⊗ Ψ' ⊳ τ.(P) ⊕ Q ==>^{^}_\<tau> τ.(P) ⊕ Q" by auto
      ultimately show ?case using ‹(Ψ ⊗ Ψ', τ.(P) ⊕ Q, τ.(P) ⊕ Q) ∈ Rel› by fastforce
    next
      case cTau
      from ‹τ ≠ τ› show ?case by simp
    qed
  qed
next
  case(cTau PQ)
  from ‹Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⟼τ ≺ PQ› show ?case
  proof(induct rule: sumCases)
    case cSum1
    from ‹Ψ ⊳ α⋅P ⟼ τ ≺ PQ› show ?case
    proof(induct rule: prefixTauCases)
      case cTau
      obtain P' where PTrans: "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ⟼τ ≺ P'" and "Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'" using tauActionI
        by auto
      obtain P'' where P'Trans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
        by auto
      from P'Trans have "Ψ ⊳ τ.(P) ⊕ Q⟼τ ≺ P''" by(rule_tac Sum1) (auto intro: guardedTau)
      with ‹Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'› obtain P''' where P''Trans: "Ψ ⊳ P' ⟼τ ≺ P'''" and "Ψ ⊳ P'' ∼ P'''"
        apply(drule_tac bisimE(4))
        apply(drule_tac bisimE(2))
        apply(drule_tac simE)
        by(auto dest: bisimE)
      from PTrans P''Trans have "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ==>^{^}_\<tau> P'''" by(fastforce dest: tauActTauChain)
      moreover from ‹Ψ ⊳ P ∼ PQ› ‹Ψ ⊳ P'' ∼ P'''› ‹Ψ ⊳ P ∼ P''› have "Ψ ⊳ P''' ∼ PQ"
        by(metis bisimSymmetric bisimTransitive)
      hence "(Ψ, P''', PQ) ∈ Rel" by(rule C1)
      ultimately show ?case by fastforce
    qed
  next
    case cSum2
    from ‹Ψ ⊳ α⋅((τ.(P)) ⊕ Q) ⟼τ ≺ PQ› show ?case
    proof(induct rule: prefixTauCases)
      case cTau
      obtain P' where PTrans: "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ⟼τ ≺ P'" and "Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'" using tauActionI
        by auto
      from PTrans have "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ==>^{^}_\<tau> P'" by(rule tauActTauChain)
      moreover from ‹Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'› ‹Ψ ⊳ τ.(P) ⊕ Q ∼ PQ› have "Ψ ⊳ P' ∼ PQ"
        by(metis bisimSymmetric bisimTransitive)
      hence "(Ψ, P', PQ) ∈ Rel" by(rule C1)
      ultimately show ?case by fastforce
    qed
  qed
qed

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

  assumes C1: "∧Ψ P Q. Ψ ⊳ P ∼ Q ==> (Ψ, P, Q) ∈ Rel"

  shows "Ψ ⊳ α⋅(τ.(P) ⊕ Q) ↝«Rel¬ α⋅P ⊕ α⋅(τ.(P) ⊕ Q)"
proof(induct rule: weakCongSimI)
  case(cTau PQ)
  from ‹Ψ ⊳ α⋅P ⊕ α⋅(τ.(P) ⊕ Q) ⟼τ ≺ PQ› show ?case
  proof(induct rule: sumCases)
    case cSum1
    from ‹Ψ ⊳ α⋅P ⟼ τ ≺ PQ› show ?case
    proof(induct rule: prefixTauCases)
      case cTau
      obtain P' where PTrans: "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ⟼τ ≺ P'" and "Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'" using tauActionI
        by auto
      obtain P'' where P'Trans: "Ψ ⊳ τ.(P) ⟼τ ≺ P''" and "Ψ ⊳ P ∼ P''" using tauActionI
        by auto
      from P'Trans have "Ψ ⊳ τ.(P) ⊕ Q⟼τ ≺ P''" by(rule_tac Sum1) (auto intro: guardedTau)
      with ‹Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'› obtain P''' where P''Trans: "Ψ ⊳ P' ⟼τ ≺ P'''" and "Ψ ⊳ P'' ∼ P'''"
        apply(drule_tac bisimE(4))
        apply(drule_tac bisimE(2))
        apply(drule_tac simE)
        by(auto dest: bisimE)
      from PTrans P''Trans have "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ==>_\<tau> P'''" by(fastforce dest: tauActTauStepChain)
      moreover from ‹Ψ ⊳ P ∼ PQ› ‹Ψ ⊳ P'' ∼ P'''› ‹Ψ ⊳ P ∼ P''› have "Ψ ⊳ P''' ∼ PQ"
        by(metis bisimSymmetric bisimTransitive)
      hence "(Ψ, P''', PQ) ∈ Rel" by(rule C1)
      ultimately show ?case by fastforce
    qed
  next
    case cSum2
    from ‹Ψ ⊳ α⋅((τ.(P)) ⊕ Q) ⟼τ ≺ PQ› show ?case
    proof(induct rule: prefixTauCases)
      case cTau
      obtain P' where PTrans: "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ⟼τ ≺ P'" and "Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'" using tauActionI
        by auto
      from PTrans have "Ψ ⊳ τ.((τ.(P)) ⊕ Q) ==>_\<tau> P'" by(rule tauActTauStepChain)
      moreover from ‹Ψ ⊳ (τ.(P)) ⊕ Q ∼ P'› ‹Ψ ⊳ τ.(P) ⊕ Q ∼ PQ› have "Ψ ⊳ P' ∼ PQ"
        by(metis bisimSymmetric bisimTransitive)
      hence "(Ψ, P', PQ) ∈ Rel" by(rule C1)
      ultimately show ?case by fastforce
    qed
  qed
qed

end

end