[STATEMENT]
lemma weakSimIChainFresh[consumes 4, case_names cOutput cInput]:
  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   yvec :: "name list"
  and   C    :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     "yvec \<sharp>* \<Psi>"
  and     "yvec \<sharp>* P"
  and     "yvec \<sharp>* Q"
  and     rAct: "\<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; \<alpha> \<noteq> \<tau>;
                             bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* C; yvec \<sharp>* \<alpha>; yvec \<sharp>* Q'; yvec \<sharp>* \<Psi>'\<rbrakk> \<Longrightarrow>
                             \<exists>P''. \<Psi> : Q \<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)"
  and     rTau: "\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'; yvec \<sharp>* Q'\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel"

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

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
proof(induct rule: weakSimI[of _ _ _ _ "(yvec, C)"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (yvec, C); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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> Q \<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> Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* Q
bn \<alpha> \<sharp>* subject \<alpha>
bn \<alpha> \<sharp>* (yvec, C)
distinct (bn \<alpha>)
\<alpha> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (yvec, C); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
obtain p::"name prm" where "(p \<bullet> yvec) \<sharp>* \<Psi>" and "(p \<bullet> yvec) \<sharp>* P" and  "(p \<bullet> yvec) \<sharp>* Q"
                         and  "(p \<bullet> yvec) \<sharp>* \<alpha>" and "(p \<bullet> yvec) \<sharp>* \<Psi>'"
                         and "(p \<bullet> yvec) \<sharp>* Q'" and S: "(set p) \<subseteq> set yvec \<times> set(p \<bullet> yvec)"
                         and "distinctPerm p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>(p \<bullet> yvec) \<sharp>* \<Psi>; (p \<bullet> yvec) \<sharp>* P; (p \<bullet> yvec) \<sharp>* Q; (p \<bullet> yvec) \<sharp>* \<alpha>; (p \<bullet> yvec) \<sharp>* \<Psi>'; (p \<bullet> yvec) \<sharp>* Q'; set p \<subseteq> set yvec \<times> set (p \<bullet> yvec); distinctPerm p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac c="(\<Psi>, P, Q, \<alpha>, Q', \<Psi>')" and xvec=yvec in name_list_avoiding) auto
[PROOF STATE]
proof (state)
this:
(p \<bullet> yvec) \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* P
(p \<bullet> yvec) \<sharp>* Q
(p \<bullet> yvec) \<sharp>* \<alpha>
(p \<bullet> yvec) \<sharp>* \<Psi>'
(p \<bullet> yvec) \<sharp>* Q'
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p

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

goal (1 subgoal):
 1. bn \<alpha> \<sharp>* yvec &&& bn \<alpha> \<sharp>* C
[PROOF STEP]
by(simp add: freshChainSym)+
[PROOF STATE]
proof (state)
this:
bn \<alpha> \<sharp>* yvec
bn \<alpha> \<sharp>* C

goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* (yvec, C); distinct (bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
proof(cases rule: actionCases[where \<alpha> = \<alpha>])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
case(cInput M N)
[PROOF STATE]
proof (state)
this:
\<alpha> = M\<lparr>N\<rparr>

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* \<alpha>\<close> \<open>\<alpha> = M\<lparr>N\<rparr>\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* \<alpha>
\<alpha> = M\<lparr>N\<rparr>
[PROOF STEP]
have "(p \<bullet> yvec) \<sharp>* M" and  "(p \<bullet> yvec) \<sharp>* N"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* \<alpha>
\<alpha> = M\<lparr>N\<rparr>

goal (1 subgoal):
 1. (p \<bullet> yvec) \<sharp>* M &&& (p \<bullet> yvec) \<sharp>* N
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
(p \<bullet> yvec) \<sharp>* M
(p \<bullet> yvec) \<sharp>* N

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>\<alpha> = M\<lparr>N\<rparr>\<close> \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* Q\<close> \<open>(p \<bullet> yvec) \<sharp>* Q\<close> S
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
\<alpha> = M\<lparr>N\<rparr>
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
[PROOF STEP]
have "\<Psi> \<rhd> Q \<longmapsto>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> (p \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
\<alpha> = M\<lparr>N\<rparr>
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> Q'
[PROOF STEP]
by(drule_tac pi=p in semantics.eqvt) (simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> Q'

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> Q'

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* M\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* M
[PROOF STEP]
have "(p \<bullet> (p \<bullet> yvec)) \<sharp>* (p \<bullet> M)"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* M

goal (1 subgoal):
 1. (p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)
[PROOF STEP]
have "yvec \<sharp>* (p \<bullet> M)"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)

goal (1 subgoal):
 1. yvec \<sharp>* (p \<bullet> M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> M)

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> M)

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* N\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* N
[PROOF STEP]
have "(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> N)"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* N

goal (1 subgoal):
 1. (p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> N)
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> N)

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> N)
[PROOF STEP]
have "yvec \<sharp>* (p \<bullet> N)"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> N)

goal (1 subgoal):
 1. yvec \<sharp>* (p \<bullet> N)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> N)

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> N)

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* Q'
[PROOF STEP]
have "(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* Q'

goal (1 subgoal):
 1. (p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> Q')
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> Q')

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> Q')
[PROOF STEP]
have "yvec \<sharp>* (p \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> Q')

goal (1 subgoal):
 1. yvec \<sharp>* (p \<bullet> Q')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> Q')

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> Q')

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* \<Psi>'
[PROOF STEP]
have "(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* \<Psi>'

goal (1 subgoal):
 1. (p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
have "yvec \<sharp>* (p \<bullet> \<Psi>')"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')

goal (1 subgoal):
 1. yvec \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> \<Psi>')

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> Q'
yvec \<sharp>* (p \<bullet> M)
yvec \<sharp>* (p \<bullet> N)
yvec \<sharp>* (p \<bullet> Q')
yvec \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
obtain P' P'' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P''" and P''Chain: "\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
                               and P'RelQ': "(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', (p \<bullet> Q')) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> Q'
yvec \<sharp>* (p \<bullet> M)
yvec \<sharp>* (p \<bullet> N)
yvec \<sharp>* (p \<bullet> Q')
yvec \<sharp>* (p \<bullet> \<Psi>')

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P''; \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto dest: rAct)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P''
\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P''
[PROOF STEP]
have "(p \<bullet> \<Psi>) : (p \<bullet> Q) \<rhd> (p \<bullet> P) \<Longrightarrow>p \<bullet> ((p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr>) \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> P''
[PROOF STEP]
by(rule weakTransitionClosed)
[PROOF STATE]
proof (state)
this:
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> P''

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with S \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* Q\<close> \<open>(p \<bullet> yvec) \<sharp>* Q\<close> \<open>yvec \<sharp>* P\<close> \<open>(p \<bullet> yvec) \<sharp>* P\<close> \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
yvec \<sharp>* P
(p \<bullet> yvec) \<sharp>* P
distinctPerm p
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> P''
[PROOF STEP]
have "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
yvec \<sharp>* P
(p \<bullet> yvec) \<sharp>* P
distinctPerm p
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>(p \<bullet> N)\<rparr> \<prec> p \<bullet> P''

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

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> p \<bullet> P''

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from P''Chain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
have  "(p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'))) \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<otimes> (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> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p
p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
have "\<Psi> \<otimes> \<Psi>' \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p
p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (1 subgoal):
 1. \<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:
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from P'RelQ' Eqvt
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel
eqvt Rel
[PROOF STEP]
have "(p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>')), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel
eqvt Rel

goal (1 subgoal):
 1. (p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
[PROOF STEP]
apply(simp add: eqvt_def eqvts)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel; \<forall>x\<in>Rel. \<forall>p. p \<bullet> x \<in> Rel\<rbrakk> \<Longrightarrow> ((p \<bullet> \<Psi>) \<otimes> (p \<bullet> p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
[PROOF STEP]
apply(erule_tac x="(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q')" in ballE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel; \<forall>pa. pa \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> ((p \<bullet> \<Psi>) \<otimes> (p \<bullet> p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
 2. \<lbrakk>(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel; (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<notin> Rel\<rbrakk> \<Longrightarrow> ((p \<bullet> \<Psi>) \<otimes> (p \<bullet> p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
[PROOF STEP]
apply(erule_tac x="p" in allE)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel; p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> ((p \<bullet> \<Psi>) \<otimes> (p \<bullet> p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
 2. \<lbrakk>(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel; (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<notin> Rel\<rbrakk> \<Longrightarrow> ((p \<bullet> \<Psi>) \<otimes> (p \<bullet> p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
[PROOF STEP]
by(auto simp add: eqvts)
[PROOF STATE]
proof (state)
this:
(p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p
(p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
[PROOF STEP]
have "(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p
(p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel

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

goal (3 subgoals):
 1. \<And>M N. \<alpha> = M\<lparr>N\<rparr> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
 3. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
using \<open>\<alpha>=M\<lparr>N\<rparr>\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
\<alpha> = M\<lparr>N\<rparr>

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<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)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
case(cOutput M xvec N)
[PROOF STATE]
proof (state)
this:
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>bn \<alpha> \<sharp>* \<Psi>\<close> \<open>bn \<alpha> \<sharp>* P\<close> \<open>bn \<alpha> \<sharp>* Q\<close>  \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>\<alpha>=M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>\<close> \<open>bn \<alpha> \<sharp>* yvec\<close>
         \<open>(p \<bullet> yvec) \<sharp>* \<alpha>\<close> \<open>bn \<alpha> \<sharp>* C\<close> \<open>bn \<alpha> \<sharp>* subject \<alpha>\<close> \<open>distinct(bn \<alpha>)\<close>
[PROOF STATE]
proof (chain)
picking this:
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* Q
bn \<alpha> \<sharp>* subject \<alpha>
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>
bn \<alpha> \<sharp>* yvec
(p \<bullet> yvec) \<sharp>* \<alpha>
bn \<alpha> \<sharp>* C
bn \<alpha> \<sharp>* subject \<alpha>
distinct (bn \<alpha>)
[PROOF STEP]
have "xvec \<sharp>* \<Psi>" and "xvec \<sharp>* P" and "xvec \<sharp>* Q" and "xvec \<sharp>* M" and "yvec \<sharp>* xvec"
     and "(p \<bullet> yvec) \<sharp>* M" and "(p \<bullet> yvec) \<sharp>* xvec" and "xvec \<sharp>* C" and "xvec \<sharp>* M" and "(p \<bullet> yvec) \<sharp>* N"
     and "distinct xvec"
[PROOF STATE]
proof (prove)
using this:
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
bn \<alpha> \<sharp>* Q
bn \<alpha> \<sharp>* subject \<alpha>
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>
bn \<alpha> \<sharp>* yvec
(p \<bullet> yvec) \<sharp>* \<alpha>
bn \<alpha> \<sharp>* C
bn \<alpha> \<sharp>* subject \<alpha>
distinct (bn \<alpha>)

goal (1 subgoal):
 1. ((xvec \<sharp>* \<Psi> &&& xvec \<sharp>* P) &&& xvec \<sharp>* Q &&& xvec \<sharp>* M &&& yvec \<sharp>* xvec) &&& ((p \<bullet> yvec) \<sharp>* M &&& (p \<bullet> yvec) \<sharp>* xvec &&& xvec \<sharp>* C) &&& xvec \<sharp>* M &&& (p \<bullet> yvec) \<sharp>* N &&& distinct xvec
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* P
xvec \<sharp>* Q
xvec \<sharp>* M
yvec \<sharp>* xvec
(p \<bullet> yvec) \<sharp>* M
(p \<bullet> yvec) \<sharp>* xvec
xvec \<sharp>* C
xvec \<sharp>* M
(p \<bullet> yvec) \<sharp>* N
distinct xvec

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* Q\<close> \<open>(p \<bullet> yvec) \<sharp>* Q\<close> S \<open>\<alpha>=M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>
[PROOF STEP]
have "\<Psi> \<rhd> Q \<longmapsto>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>

goal (1 subgoal):
 1. \<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
[PROOF STEP]
by(rule_tac outputPermSubject) (assumption | simp add: fresh_star_def)+
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
note \<open>xvec \<sharp>* \<Psi>\<close> \<open>xvec \<sharp>* P\<close>
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* P

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* \<Psi>
xvec \<sharp>* P

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
note \<open>xvec \<sharp>* Q\<close>
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* Q

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* Q

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>xvec \<sharp>* M\<close>
[PROOF STATE]
proof (chain)
picking this:
xvec \<sharp>* M
[PROOF STEP]
have "(p \<bullet> xvec) \<sharp>* (p \<bullet> M)"
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* M

goal (1 subgoal):
 1. (p \<bullet> xvec) \<sharp>* (p \<bullet> M)
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> xvec) \<sharp>* (p \<bullet> M)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>yvec \<sharp>* xvec\<close> \<open>(p \<bullet> yvec) \<sharp>* xvec\<close> S
[PROOF STATE]
proof (chain)
picking this:
yvec \<sharp>* xvec
(p \<bullet> yvec) \<sharp>* xvec
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
(p \<bullet> xvec) \<sharp>* (p \<bullet> M)
[PROOF STEP]
have "xvec \<sharp>* (p \<bullet> M)"
[PROOF STATE]
proof (prove)
using this:
yvec \<sharp>* xvec
(p \<bullet> yvec) \<sharp>* xvec
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
(p \<bullet> xvec) \<sharp>* (p \<bullet> M)

goal (1 subgoal):
 1. xvec \<sharp>* (p \<bullet> M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* (p \<bullet> M)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* (p \<bullet> M)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
note \<open>xvec \<sharp>* C\<close>
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* C

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
xvec \<sharp>* C

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* M\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* M
[PROOF STEP]
have "(p \<bullet> (p \<bullet> yvec)) \<sharp>* (p \<bullet> M)"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* M

goal (1 subgoal):
 1. (p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)
[PROOF STEP]
have "yvec \<sharp>* (p \<bullet> M)"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> M)

goal (1 subgoal):
 1. yvec \<sharp>* (p \<bullet> M)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> M)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> M)

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
note \<open>yvec \<sharp>* xvec\<close>
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* xvec

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* xvec

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'\<close> \<open>yvec \<sharp>* Q\<close> \<open>yvec \<sharp>* xvec\<close> \<open>\<alpha>=M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>\<close> \<open>xvec \<sharp>* M\<close> \<open>distinct xvec\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
yvec \<sharp>* Q
yvec \<sharp>* xvec
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>
xvec \<sharp>* M
distinct xvec
[PROOF STEP]
have "yvec \<sharp>* N" and "yvec \<sharp>* Q'"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
yvec \<sharp>* Q
yvec \<sharp>* xvec
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>
xvec \<sharp>* M
distinct xvec

goal (1 subgoal):
 1. yvec \<sharp>* N &&& yvec \<sharp>* Q'
[PROOF STEP]
by(force dest: outputFreshChainDerivative)+
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* N
yvec \<sharp>* Q'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* N
yvec \<sharp>* Q'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>(p \<bullet> yvec) \<sharp>* \<Psi>'\<close>
[PROOF STATE]
proof (chain)
picking this:
(p \<bullet> yvec) \<sharp>* \<Psi>'
[PROOF STEP]
have "(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> yvec) \<sharp>* \<Psi>'

goal (1 subgoal):
 1. (p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
by(simp add: pt_fresh_star_bij[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
have "yvec \<sharp>* (p \<bullet> \<Psi>')"
[PROOF STATE]
proof (prove)
using this:
distinctPerm p
(p \<bullet> p \<bullet> yvec) \<sharp>* (p \<bullet> \<Psi>')

goal (1 subgoal):
 1. yvec \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* (p \<bullet> \<Psi>')

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
xvec \<sharp>* \<Psi>
xvec \<sharp>* P
xvec \<sharp>* Q
xvec \<sharp>* (p \<bullet> M)
xvec \<sharp>* C
yvec \<sharp>* (p \<bullet> M)
yvec \<sharp>* xvec
yvec \<sharp>* N
yvec \<sharp>* Q'
yvec \<sharp>* (p \<bullet> \<Psi>')
[PROOF STEP]
obtain P'' P' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P''"
                               and PChain: "\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
                               and P'RelQ': "(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
xvec \<sharp>* \<Psi>
xvec \<sharp>* P
xvec \<sharp>* Q
xvec \<sharp>* (p \<bullet> M)
xvec \<sharp>* C
yvec \<sharp>* (p \<bullet> M)
yvec \<sharp>* xvec
yvec \<sharp>* N
yvec \<sharp>* Q'
yvec \<sharp>* (p \<bullet> \<Psi>')

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P''; \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(drule_tac rAct) auto
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P''
\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P''
[PROOF STEP]
have "(p \<bullet> \<Psi>) : (p \<bullet> Q) \<rhd> (p \<bullet> P) \<Longrightarrow>(p \<bullet> ((p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>)) \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>(p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P''

goal (1 subgoal):
 1. p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<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> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with S \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> \<open>yvec \<sharp>* P\<close> \<open>(p \<bullet> yvec) \<sharp>* P\<close> \<open>yvec \<sharp>* Q\<close> \<open>(p \<bullet> yvec) \<sharp>* Q\<close> \<open>yvec \<sharp>* xvec\<close> \<open>(p \<bullet> yvec) \<sharp>* xvec\<close>
      \<open>yvec \<sharp>* N\<close> \<open>(p \<bullet> yvec) \<sharp>* N\<close> \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* P
(p \<bullet> yvec) \<sharp>* P
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
yvec \<sharp>* xvec
(p \<bullet> yvec) \<sharp>* xvec
yvec \<sharp>* N
(p \<bullet> yvec) \<sharp>* N
distinctPerm p
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
[PROOF STEP]
have "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* P
(p \<bullet> yvec) \<sharp>* P
yvec \<sharp>* Q
(p \<bullet> yvec) \<sharp>* Q
yvec \<sharp>* xvec
(p \<bullet> yvec) \<sharp>* xvec
yvec \<sharp>* N
(p \<bullet> yvec) \<sharp>* N
distinctPerm p
p \<bullet> \<Psi> : p \<bullet> Q \<rhd> p \<bullet> P \<Longrightarrow>p \<bullet> (p \<bullet> M)\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''

goal (1 subgoal):
 1. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
[PROOF STEP]
by(simp add: eqvts)
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from PChain
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'
[PROOF STEP]
have "(p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'))) \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'

goal (1 subgoal):
 1. p \<bullet> \<Psi> \<otimes> (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> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with S \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close> \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
distinctPerm p
p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
have "\<Psi> \<otimes> \<Psi>' \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
distinctPerm p
p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (1 subgoal):
 1. \<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:
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from P'RelQ' \<open>eqvt Rel\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel
eqvt Rel
[PROOF STEP]
have "p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel
eqvt Rel

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

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
with \<open>yvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> yvec) \<sharp>* \<Psi>\<close>\<open>yvec \<sharp>* Q'\<close> \<open>(p \<bullet> yvec) \<sharp>* Q'\<close> S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q'
(p \<bullet> yvec) \<sharp>* Q'
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p
p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel
[PROOF STEP]
have "(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
yvec \<sharp>* \<Psi>
(p \<bullet> yvec) \<sharp>* \<Psi>
yvec \<sharp>* Q'
(p \<bullet> yvec) \<sharp>* Q'
set p \<subseteq> set yvec \<times> set (p \<bullet> yvec)
distinctPerm p
p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', Q') \<in> Rel

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

goal (2 subgoals):
 1. \<And>M xvec N. \<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
using \<open>\<alpha>=M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
\<alpha> = M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<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)

goal (1 subgoal):
 1. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
case cTau
[PROOF STATE]
proof (state)
this:
\<alpha> = \<tau>

goal (1 subgoal):
 1. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
from \<open>\<alpha> = \<tau>\<close> \<open>\<alpha> \<noteq> \<tau>\<close>
[PROOF STATE]
proof (chain)
picking this:
\<alpha> = \<tau>
\<alpha> \<noteq> \<tau>
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
\<alpha> = \<tau>
\<alpha> \<noteq> \<tau>

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

goal (1 subgoal):
 1. \<alpha> = \<tau> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<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)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<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)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<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)

goal (1 subgoal):
 1. \<And>Q'. \<Psi> \<rhd> Q \<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> Q \<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 Q')
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'

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

goal (1 subgoal):
 1. yvec \<sharp>* Q'
[PROOF STEP]
by(force dest: tauFreshChainDerivative)
[PROOF STATE]
proof (state)
this:
yvec \<sharp>* Q'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakSimIFresh[consumes 4, case_names cAct cTau]:
  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   x   :: name
  and   C   :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     "x \<sharp> \<Psi>"
  and     "x \<sharp> P"
  and     "x \<sharp> Q"
  and     "\<And>\<alpha> Q' \<Psi>'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q; \<alpha> \<noteq> \<tau>;
                       bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* C; x \<sharp> \<alpha>; x \<sharp> Q'; x \<sharp> \<Psi>'\<rbrakk> \<Longrightarrow>
                       \<exists>P''. \<Psi> : Q \<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)"
  and     "\<And>Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q'; x \<sharp> Q'\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto><Rel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
x \<sharp> \<Psi>
x \<sharp> P
x \<sharp> Q
\<lbrakk>\<Psi> \<rhd> Q \<longmapsto> ?\<alpha> \<prec> ?Q'; bn ?\<alpha> \<sharp>* \<Psi>; bn ?\<alpha> \<sharp>* P; bn ?\<alpha> \<sharp>* Q; ?\<alpha> \<noteq> \<tau>; bn ?\<alpha> \<sharp>* subject ?\<alpha>; bn ?\<alpha> \<sharp>* C; x \<sharp> ?\<alpha>; x \<sharp> ?Q'; x \<sharp> ?\<Psi>'\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)
\<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> ?Q'; x \<sharp> ?Q'\<rbrakk> \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', ?Q') \<in> Rel

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
by(rule_tac yvec="[x]" and C=C in weakSimIChainFresh) auto


[STATEMENT]
lemma weakSimE:
  fixes F   :: '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 "\<Psi> \<rhd> P \<leadsto><Rel> Q"

  shows "\<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow>
                            \<exists>P''. \<Psi> : Q \<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)"
  and   "\<And>Q'. \<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)) &&& (\<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> P \<leadsto><Rel> Q

goal (1 subgoal):
 1. (\<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<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)) &&& (\<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel)
[PROOF STEP]
by(auto simp add: weakSimulation_def)