[STATEMENT]
lemma weakSimClosedAux:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"
  and     PSimQ: "\<Psi> \<rhd> P \<leadsto><Rel> Q"

  shows "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<leadsto><Rel> (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<leadsto><Rel> p \<bullet> Q
[PROOF STEP]
using EqvtRel
[PROOF STATE]
proof (prove)
using this:
eqvt Rel

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<leadsto><Rel> p \<bullet> Q
[PROOF STEP]
proof(induct rule: weakSimI[of _ _ _ _ "(\<Psi>, P, p)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cAct \<Psi>' \<alpha> Q')
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* (p \<bullet> \<Psi>)
bn \<alpha> \<sharp>* (p \<bullet> P)
bn \<alpha> \<sharp>* (p \<bullet> Q)
bn \<alpha> \<sharp>* subject \<alpha>
bn \<alpha> \<sharp>* (\<Psi>, P, p)
distinct (bn \<alpha>)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto>\<alpha> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
have "(rev p \<bullet> p \<bullet> \<Psi>) \<rhd> (rev p \<bullet> p \<bullet> Q) \<longmapsto>(rev p \<bullet> (\<alpha> \<prec> Q'))"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. rev p \<bullet> p \<bullet> \<Psi> \<rhd> rev p \<bullet> p \<bullet> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> Q'
[PROOF STEP]
by(blast dest: semantics.eqvt)
[PROOF STATE]
proof (state)
this:
rev p \<bullet> p \<bullet> \<Psi> \<rhd> rev p \<bullet> p \<bullet> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> Q'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
hence "\<Psi> \<rhd> Q \<longmapsto>(rev p \<bullet> \<alpha>) \<prec> (rev p \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
rev p \<bullet> p \<bullet> \<Psi> \<rhd> rev p \<bullet> p \<bullet> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with \<open>bn \<alpha> \<sharp>* (\<Psi>, P, p)\<close>
[PROOF STATE]
proof (chain)
picking this:
bn \<alpha> \<sharp>* (\<Psi>, P, p)
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'
[PROOF STEP]
have "bn \<alpha>  \<sharp>* \<Psi>" and "bn \<alpha>  \<sharp>* P" and "bn \<alpha>  \<sharp>* p"
[PROOF STATE]
proof (prove)
using this:
bn \<alpha> \<sharp>* (\<Psi>, P, p)
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* \<Psi> &&& bn \<alpha> \<sharp>* P &&& bn \<alpha> \<sharp>* p
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* p

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* p

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<noteq> \<tau>
[PROOF STEP]
have "(rev p \<bullet> \<alpha>) \<noteq> \<tau>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. rev p \<bullet> \<alpha> \<noteq> \<tau>
[PROOF STEP]
by(cases rule: actionCases[where \<alpha>=\<alpha>]) auto
[PROOF STATE]
proof (state)
this:
rev p \<bullet> \<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* p
rev p \<bullet> \<alpha> \<noteq> \<tau>
[PROOF STEP]
obtain P'' P' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>(rev p \<bullet> \<alpha>) \<prec> P''"
                          and P''Chain: "\<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* p
rev p \<bullet> \<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>rev p \<bullet> \<alpha> \<prec> P''; \<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<alpha> \<noteq> \<tau>\<close> PSimQ
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> rev p \<bullet> \<alpha> \<prec> rev p \<bullet> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* p
rev p \<bullet> \<alpha> \<noteq> \<tau>
\<alpha> \<noteq> \<tau>
\<Psi> \<rhd> P \<leadsto><Rel> Q

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>rev p \<bullet> \<alpha> \<prec> P''; \<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(drule_tac \<Psi>'="rev p \<bullet> \<Psi>'" in weakSimE(1)) (auto simp add: freshChainPermSimp bnEqvt[symmetric])
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>rev p \<bullet> \<alpha> \<prec> P''
\<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>rev p \<bullet> \<alpha> \<prec> P''
[PROOF STEP]
have "(p \<bullet> \<Psi>) : (p \<bullet> Q) \<rhd> (p \<bullet> P) \<Longrightarrow>(p \<bullet> (rev p \<bullet> \<alpha>)) \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>rev p \<bullet> \<alpha> \<prec> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> rev p \<bullet> \<alpha> \<prec> p \<bullet> P''
[PROOF STEP]
by(rule eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> rev p \<bullet> \<alpha> \<prec> p \<bullet> P''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
hence "(p \<bullet> \<Psi>) : (p \<bullet> Q) \<rhd> (p \<bullet> P) \<Longrightarrow>\<alpha> \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> rev p \<bullet> \<alpha> \<prec> p \<bullet> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> p \<bullet> P''
[PROOF STEP]
by(simp add: eqvts freshChainPermSimp)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> p \<bullet> P''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> p \<bullet> P''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from P''Chain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
have  "(p \<bullet> (\<Psi> \<otimes> (rev p \<bullet> \<Psi>'))) \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
by(rule eqvts)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
hence "(p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<otimes> (rev p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (1 subgoal):
 1. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from P'RelQ' EqvtRel
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel
eqvt Rel
[PROOF STEP]
have "(p \<bullet> ((\<Psi> \<otimes> (rev p \<bullet> \<Psi>')), P', rev p \<bullet> Q')) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel
eqvt Rel

goal (1 subgoal):
 1. p \<bullet> (\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel
[PROOF STEP]
by(simp only: eqvt_def)
[PROOF STATE]
proof (state)
this:
p \<bullet> (\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
hence "((p \<bullet> \<Psi>) \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> (\<Psi> \<otimes> (rev p \<bullet> \<Psi>'), P', rev p \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. ((p \<bullet> \<Psi>) \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
((p \<bullet> \<Psi>) \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* (p \<bullet> \<Psi>); bn \<alpha> \<sharp>* (p \<bullet> P); bn \<alpha> \<sharp>* (p \<bullet> Q); bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (\<Psi>, P, p); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> p \<bullet> P''
(p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
((p \<bullet> \<Psi>) \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> p \<bullet> P''
(p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
((p \<bullet> \<Psi>) \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. (p \<bullet> \<Psi>) \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> ((p \<bullet> \<Psi>) \<otimes> \<Psi>', P', Q') \<in> Rel)

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
case(cTau Q')
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from \<open>p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto>\<tau> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q'
[PROOF STEP]
have "(rev p \<bullet> p \<bullet> \<Psi>) \<rhd> (rev p \<bullet> p \<bullet> Q) \<longmapsto>(rev p \<bullet> (\<tau> \<prec> Q'))"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q'

goal (1 subgoal):
 1. rev p \<bullet> p \<bullet> \<Psi> \<rhd> rev p \<bullet> p \<bullet> Q \<longmapsto> rev p \<bullet> \<tau> \<prec> Q'
[PROOF STEP]
by(blast dest: semantics.eqvt)
[PROOF STATE]
proof (state)
this:
rev p \<bullet> p \<bullet> \<Psi> \<rhd> rev p \<bullet> p \<bullet> Q \<longmapsto> rev p \<bullet> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
hence "\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> (rev p \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
rev p \<bullet> p \<bullet> \<Psi> \<rhd> rev p \<bullet> p \<bullet> Q \<longmapsto> rev p \<bullet> \<tau> \<prec> Q'

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> rev p \<bullet> Q'
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> rev p \<bullet> Q'

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
with PSimQ
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> rev p \<bullet> Q'
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', rev p \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> rev p \<bullet> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', rev p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', rev p \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from PChain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
have "(p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
by(rule tauChainEqvt)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
from P'RelQ' EqvtRel
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', rev p \<bullet> Q') \<in> Rel
eqvt Rel
[PROOF STEP]
have "(p \<bullet> (\<Psi>,  P', rev p \<bullet> Q')) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', rev p \<bullet> Q') \<in> Rel
eqvt Rel

goal (1 subgoal):
 1. p \<bullet> (\<Psi>, P', rev p \<bullet> Q') \<in> Rel
[PROOF STEP]
by(simp only: eqvt_def)
[PROOF STATE]
proof (state)
this:
p \<bullet> (\<Psi>, P', rev p \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
hence "(p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> (\<Psi>, P', rev p \<bullet> Q') \<in> Rel

goal (1 subgoal):
 1. (p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. p \<bullet> \<Psi> \<rhd> p \<bullet> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(p \<bullet> \<Psi>, p \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. p \<bullet> \<Psi> \<rhd> p \<bullet> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (p \<bullet> \<Psi>, P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakSimClosed:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   p   :: "name prm"

  assumes EqvtRel: "eqvt Rel"

  shows "\<Psi> \<rhd> P \<leadsto><Rel> Q \<Longrightarrow> (p \<bullet> \<Psi>) \<rhd> (p \<bullet> P) \<leadsto><Rel> (p \<bullet> Q)"
  and   "P \<leadsto><Rel> Q \<Longrightarrow> (p \<bullet> P) \<leadsto><Rel> (p \<bullet> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Psi> \<rhd> P \<leadsto><Rel> Q \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> P \<leadsto><Rel> p \<bullet> Q) &&& (P \<leadsto><Rel> Q \<Longrightarrow> p \<bullet> P \<leadsto><Rel> p \<bullet> Q)
[PROOF STEP]
using EqvtRel
[PROOF STATE]
proof (prove)
using this:
eqvt Rel

goal (1 subgoal):
 1. (\<Psi> \<rhd> P \<leadsto><Rel> Q \<Longrightarrow> p \<bullet> \<Psi> \<rhd> p \<bullet> P \<leadsto><Rel> p \<bullet> Q) &&& (P \<leadsto><Rel> Q \<Longrightarrow> p \<bullet> P \<leadsto><Rel> p \<bullet> Q)
[PROOF STEP]
by(force dest: weakSimClosedAux simp add: permBottom)+


[STATEMENT]
lemma weakSimReflexive:
  fixes Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"

  assumes "{(\<Psi>, P, P) | \<Psi> P. True} \<subseteq> Rel"

  shows "\<Psi> \<rhd> P \<leadsto><Rel> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> P
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
{(\<Psi>, P, P) |\<Psi> P. True} \<subseteq> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> P
[PROOF STEP]
by(auto simp add: weakSimulation_def weakTransition_def dest: rtrancl_into_rtrancl) force+


[STATEMENT]
lemma weakSimTauChain:
  fixes \<Psi>   :: 'b
  and   Q   :: "('a, 'b, 'c) psi"
  and   Q'  :: "('a, 'b, 'c) psi"
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
  and     "(\<Psi>, P, Q) \<in> Rel"
  and     Sim: "\<And>\<Psi>' R S. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> \<Psi>' \<rhd> R \<leadsto><Rel> S"

  obtains P' where "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume A: "\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'\<close> \<open>(\<Psi>, P, Q) \<in> Rel\<close> A
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. thesis
[PROOF STEP]
proof(induct arbitrary: P thesis rule: tauChainInduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', a) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case(TauBase Q P)
[PROOF STATE]
proof (state)
this:
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q) \<in> Rel\<rbrakk> \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>a P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', a) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q) \<in> Rel\<rbrakk> \<Longrightarrow> thesis

goal (2 subgoals):
 1. \<And>a P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', a) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
have "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P

goal (2 subgoals):
 1. \<And>a P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', a) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
 2. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q) \<in> Rel\<rbrakk> \<Longrightarrow> thesis
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q) \<in> Rel\<rbrakk> \<Longrightarrow> thesis
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
case(TauStep Q Q' Q'' P)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
\<lbrakk>(\<Psi>, ?P, Q) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> ?P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis
\<Psi> \<rhd> Q' \<longmapsto> \<tau> \<prec> Q''
(\<Psi>, P, Q) \<in> Rel
\<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi>, ?P', Q'') \<in> Rel\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>(\<Psi>, P, Q) \<in> Rel\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> Rel
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> Rel

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule TauStep)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from \<open>(\<Psi>, P', Q') \<in> Rel\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> P' \<leadsto><Rel> Q'"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P' \<leadsto><Rel> Q'
[PROOF STEP]
by(rule Sim)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P' \<leadsto><Rel> Q'

goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P' \<leadsto><Rel> Q'
[PROOF STEP]
obtain P'' where P'Chain: "\<Psi> \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and "(\<Psi>, P'', Q'') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P' \<leadsto><Rel> Q'

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; (\<Psi>, P'', Q'') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>\<Psi> \<rhd> Q' \<longmapsto>\<tau> \<prec> Q''\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P' \<leadsto><Rel> Q'
\<Psi> \<rhd> Q' \<longmapsto> \<tau> \<prec> Q''

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; (\<Psi>, P'', Q'') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
(\<Psi>, P'', Q'') \<in> Rel

goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
from PChain P'Chain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
have "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
\<Psi> \<rhd> P' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. \<And>a b c P thesis. \<lbrakk>\<Psi> \<rhd> a \<Longrightarrow>\<^sup>^\<^sub>\<tau> b; \<And>P thesis. \<lbrakk>(\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', b) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis; \<Psi> \<rhd> b \<longmapsto> \<tau> \<prec> c; (\<Psi>, P, a) \<in> Rel; \<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', c) \<in> Rel\<rbrakk> \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''

goal (1 subgoal):
 1. thesis
[PROOF STEP]
using \<open>(\<Psi>, P'', Q'') \<in> Rel\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
(\<Psi>, P'', Q'') \<in> Rel

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by(rule TauStep)
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakSimE2:
  fixes \<Psi>  :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"

  assumes PRelQ: "(\<Psi>, P, Q) \<in> Rel"
  and     Sim: "\<And>\<Psi>' R S. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> \<Psi>' \<rhd> R \<leadsto><Rel> S"
  and     QTrans: "\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q'"
  and     "bn \<alpha> \<sharp>* \<Psi>"
  and     "bn \<alpha> \<sharp>* P"
  and     "\<alpha> \<noteq> \<tau>"

  obtains P'' P' where "\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''" and "\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and "(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
assume A: "\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis"
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> ?P''; \<Psi> \<otimes> \<Psi>' \<rhd> ?P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi> \<otimes> \<Psi>', ?P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from QTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q'
[PROOF STEP]
obtain Q''
    where QChain: "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''"
      and ReqQ'': "insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>"
      and Q''Trans: "\<Psi> \<rhd> Q'' \<longmapsto>\<alpha> \<prec> Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q'

goal (1 subgoal):
 1. (\<And>Q''. \<lbrakk>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''; insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>; \<Psi> \<rhd> Q'' \<longmapsto> \<alpha> \<prec> Q'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
\<Psi> \<rhd> Q'' \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from QChain PRelQ Sim
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
(\<Psi>, P, Q) \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S
[PROOF STEP]
obtain P'' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and P''RelQ'': "(\<Psi>, P'', Q'') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q''
(\<Psi>, P, Q) \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S

goal (1 subgoal):
 1. (\<And>P''. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; (\<Psi>, P'', Q'') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakSimTauChain)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
(\<Psi>, P'', Q'') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from PChain \<open>bn \<alpha> \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
bn \<alpha> \<sharp>* P
[PROOF STEP]
have "bn \<alpha> \<sharp>* P''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
bn \<alpha> \<sharp>* P

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* P''
[PROOF STEP]
by(rule tauChainFreshChain)
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* P''

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from P''RelQ''
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P'', Q'') \<in> Rel
[PROOF STEP]
have "\<Psi> \<rhd> P'' \<leadsto><Rel> Q''"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P'', Q'') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P'' \<leadsto><Rel> Q''
[PROOF STEP]
by(rule Sim)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<leadsto><Rel> Q''

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with Q''Trans \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P''\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q'' \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P''
\<alpha> \<noteq> \<tau>
\<Psi> \<rhd> P'' \<leadsto><Rel> Q''
[PROOF STEP]
obtain P''' P' where P''Trans: "\<Psi> : Q'' \<rhd> P'' \<Longrightarrow>\<alpha> \<prec> P'''" and P'''Chain: "\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
                   and P'RelQ': "(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q'' \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P''
\<alpha> \<noteq> \<tau>
\<Psi> \<rhd> P'' \<leadsto><Rel> Q''

goal (1 subgoal):
 1. (\<And>P''' P'. \<lbrakk>\<Psi> : Q'' \<rhd> P'' \<Longrightarrow>\<alpha> \<prec> P'''; \<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q'' \<rhd> P'' \<Longrightarrow>\<alpha> \<prec> P'''
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from P''Trans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q'' \<rhd> P'' \<Longrightarrow>\<alpha> \<prec> P'''
[PROOF STEP]
obtain P'''' where P''Chain: "\<Psi> \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''"
                               and Q''eqP'''': "insertAssertion (extractFrame Q'') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>"
                               and P''''Trans: "\<Psi> \<rhd> P'''' \<longmapsto>\<alpha> \<prec> P'''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q'' \<rhd> P'' \<Longrightarrow>\<alpha> \<prec> P'''

goal (1 subgoal):
 1. (\<And>P''''. \<lbrakk>\<Psi> \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''; insertAssertion (extractFrame Q'') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>; \<Psi> \<rhd> P'''' \<longmapsto> \<alpha> \<prec> P'''\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakTransitionE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''
insertAssertion (extractFrame Q'') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>
\<Psi> \<rhd> P'''' \<longmapsto> \<alpha> \<prec> P'''

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from PChain P''Chain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''
[PROOF STEP]
have "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from ReqQ'' Q''eqP''''
[PROOF STATE]
proof (chain)
picking this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
insertAssertion (extractFrame Q'') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>
[PROOF STEP]
have "insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>"
[PROOF STATE]
proof (prove)
using this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame Q'') \<Psi>
insertAssertion (extractFrame Q'') \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>

goal (1 subgoal):
 1. insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>
[PROOF STEP]
by(rule FrameStatImpTrans)
[PROOF STATE]
proof (state)
this:
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>
[PROOF STEP]
have "\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>

goal (1 subgoal):
 1. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''
[PROOF STEP]
using P''''Trans
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''''
insertAssertion (extractFrame R) \<Psi> \<hookrightarrow>\<^sub>F insertAssertion (extractFrame P'''') \<Psi>
\<Psi> \<rhd> P'''' \<longmapsto> \<alpha> \<prec> P'''

goal (1 subgoal):
 1. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''
[PROOF STEP]
by(rule weakTransitionI)
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P''; \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with P'''Chain P'RelQ' A
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
\<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> ?P''; \<Psi> \<otimes> \<Psi>' \<rhd> ?P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi> \<otimes> \<Psi>', ?P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
\<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> ?P''; \<Psi> \<otimes> \<Psi>' \<rhd> ?P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> ?P'; (\<Psi> \<otimes> \<Psi>', ?P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''

goal (1 subgoal):
 1. thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
thesis

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakSimTransitive:
  fixes \<Psi>     :: 'b
  and   P     :: "('a, 'b, 'c) psi"
  and   Rel   :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q     :: "('a, 'b, 'c) psi"
  and   Rel'  :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   T     :: "('a, 'b, 'c) psi"
  and   Rel'' :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"

  assumes PRelQ: "(\<Psi>, P, Q) \<in> Rel"
  and     QSimR: "\<Psi> \<rhd> Q \<leadsto><Rel'> R"
  and     Eqvt: "eqvt Rel''"
  and     Set: "{(\<Psi>, P, R) | \<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''"
  and     Sim: "\<And>\<Psi>' R S. (\<Psi>', R, S) \<in> Rel \<Longrightarrow> \<Psi>' \<rhd> R \<leadsto><Rel> S"

  shows "\<Psi> \<rhd> P \<leadsto><Rel''> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel''> R
[PROOF STEP]
using \<open>eqvt Rel''\<close>
[PROOF STATE]
proof (prove)
using this:
eqvt Rel''

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel''> R
[PROOF STEP]
proof(induct rule: weakSimI[of _ _ _ _ Q])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
case(cAct \<Psi>' \<alpha> R')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> R'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* R
bn \<alpha> \<sharp>* subject \<alpha>
bn \<alpha> \<sharp>* Q
distinct (bn \<alpha>)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from QSimR \<open>\<Psi> \<rhd> R \<longmapsto>\<alpha> \<prec> R'\<close> \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* Q\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<leadsto><Rel'> R
\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> R'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* Q
\<alpha> \<noteq> \<tau>
[PROOF STEP]
obtain Q'' Q' where QTrans: "\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''" and Q''Chain: "\<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'"
                  and Q'RelR': "(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<leadsto><Rel'> R
\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> R'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* Q
\<alpha> \<noteq> \<tau>

goal (1 subgoal):
 1. (\<And>Q'' Q'. \<lbrakk>\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''; \<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'; (\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''
\<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
with PRelQ Sim QTrans \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P, Q) \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''
\<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'
[PROOF STEP]
obtain P''' P'' where PTrans: "\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''"
                and P'''Chain: "\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''" and P''RelQ'': "(\<Psi> \<otimes> \<Psi>', P'', Q'') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P, Q) \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>
\<Psi> : R \<rhd> Q \<Longrightarrow>\<alpha> \<prec> Q''
\<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'

goal (1 subgoal):
 1. (\<And>P''' P''. \<lbrakk>\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''; \<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''; (\<Psi> \<otimes> \<Psi>', P'', Q'') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(drule_tac weakSimE2) auto
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
(\<Psi> \<otimes> \<Psi>', P'', Q'') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
note PTrans
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from Q''Chain P''RelQ'' Sim
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', P'', Q'') \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S
[PROOF STEP]
obtain P' where P''Chain: "\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>' \<rhd> Q'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi> \<otimes> \<Psi>', P'', Q'') \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakSimTauChain)
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from P'''Chain P''Chain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
have "\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P''
\<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from P'RelQ' Q'RelR' Set
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''
[PROOF STEP]
have "(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel
(\<Psi> \<otimes> \<Psi>', Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''

goal (1 subgoal):
 1. (\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> R \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* R; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* Q; distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel'')
 2. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'''
\<Psi> \<otimes> \<Psi>' \<rhd> P''' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel''

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel'')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : R \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', R') \<in> Rel'')

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
case(cTau R')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> R'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from QSimR \<open>\<Psi> \<rhd> R \<longmapsto>\<tau> \<prec> R'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<leadsto><Rel'> R
\<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> R'
[PROOF STEP]
obtain Q' where QChain: "\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'" and Q'RelR': "(\<Psi>, Q', R') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<leadsto><Rel'> R
\<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> R'

goal (1 subgoal):
 1. (\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'; (\<Psi>, Q', R') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: weakSimE)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi>, Q', R') \<in> Rel'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from QChain PRelQ Sim
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi>, P, Q) \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S
[PROOF STEP]
obtain P' where PChain: "\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'" and P'RelQ': "(\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<Longrightarrow>\<^sup>^\<^sub>\<tau> Q'
(\<Psi>, P, Q) \<in> Rel
(?\<Psi>', ?R, ?S) \<in> Rel \<Longrightarrow> ?\<Psi>' \<rhd> ?R \<leadsto><Rel> ?S

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi>, P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule weakSimTauChain)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
note PChain
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
from P'RelQ' Q'RelR' Set
[PROOF STATE]
proof (chain)
picking this:
(\<Psi>, P', Q') \<in> Rel
(\<Psi>, Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''
[PROOF STEP]
have "(\<Psi>, P', R') \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(\<Psi>, P', Q') \<in> Rel
(\<Psi>, Q', R') \<in> Rel'
{(\<Psi>, P, R) |\<Psi> P R. \<exists>Q. (\<Psi>, P, Q) \<in> Rel \<and> (\<Psi>, Q, R) \<in> Rel'} \<subseteq> Rel''

goal (1 subgoal):
 1. (\<Psi>, P', R') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<Psi>, P', R') \<in> Rel''

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> R \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', R') \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi>, P', R') \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', R') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', R') \<in> Rel''

goal:
No subgoals!
[PROOF STEP]
qed