[STATEMENT]
lemma parCompose:
  fixes P     :: pi
  and   Q     :: pi
  and   R     :: pi
  and   T     :: pi
  and   Rel   :: "(pi \<times> pi) set"
  and   Rel'  :: "(pi \<times> pi) set"
  and   Rel'' :: "(pi \<times> pi) set"

  assumes PSimQ:    "P \<leadsto>[Rel] Q"
  and     RSimT:    "R \<leadsto>[Rel'] T"
  and     PRelQ:    "(P, Q) \<in> Rel"
  and     RRel'T:   "(R, T) \<in> Rel'"
  and     Par:      "\<And>P Q R T. \<lbrakk>(P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> (P \<parallel> R, Q \<parallel> T) \<in> Rel''"
  and     Res:      "\<And>P Q a. (P, Q) \<in> Rel'' \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> Rel''"
  and     EqvtRel:  "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"
  and     EqvtRel'': "eqvt Rel''"

  shows "P \<parallel> R \<leadsto>[Rel''] Q \<parallel> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel''] Q \<parallel> T
[PROOF STEP]
using EqvtRel''
[PROOF STATE]
proof (prove)
using this:
eqvt Rel''

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel''] Q \<parallel> T
[PROOF STEP]
proof(induct rule: simCasesCont[where C="()"])
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a x Q'. \<lbrakk>Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'; x \<sharp> P \<parallel> R; x \<sharp> Q \<parallel> T; x \<sharp> a; x \<sharp> ()\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
 2. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
case(Bound a x Q')
[PROOF STATE]
proof (state)
this:
Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> P \<parallel> R
x \<sharp> Q \<parallel> T
x \<sharp> a
x \<sharp> ()

goal (2 subgoals):
 1. \<And>a x Q'. \<lbrakk>Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'; x \<sharp> P \<parallel> R; x \<sharp> Q \<parallel> T; x \<sharp> a; x \<sharp> ()\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
 2. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
have "x \<sharp> P \<parallel> R" and "x \<sharp> Q \<parallel> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<sharp> P \<parallel> R &&& x \<sharp> Q \<parallel> T
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
x \<sharp> P \<parallel> R
x \<sharp> Q \<parallel> T

goal (2 subgoals):
 1. \<And>a x Q'. \<lbrakk>Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'; x \<sharp> P \<parallel> R; x \<sharp> Q \<parallel> T; x \<sharp> a; x \<sharp> ()\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
 2. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
hence xFreshP: "x \<sharp> P" and xFreshR: "x \<sharp> R" and "x \<sharp> Q" and "x \<sharp> T"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P \<parallel> R
x \<sharp> Q \<parallel> T

goal (1 subgoal):
 1. (x \<sharp> P &&& x \<sharp> R) &&& x \<sharp> Q &&& x \<sharp> T
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<sharp> P
x \<sharp> R
x \<sharp> Q
x \<sharp> T

goal (2 subgoals):
 1. \<And>a x Q'. \<lbrakk>Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'; x \<sharp> P \<parallel> R; x \<sharp> Q \<parallel> T; x \<sharp> a; x \<sharp> ()\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
 2. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
have QTTrans: "Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (2 subgoals):
 1. \<And>a x Q'. \<lbrakk>Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'; x \<sharp> P \<parallel> R; x \<sharp> Q \<parallel> T; x \<sharp> a; x \<sharp> ()\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
 2. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
[PROOF STEP]
using \<open>x \<sharp> Q\<close> \<open>x \<sharp> T\<close>
[PROOF STATE]
proof (prove)
using this:
Q \<parallel> T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> Q
x \<sharp> T

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''
[PROOF STEP]
proof(induct rule: parCasesB)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
case(cPar1 Q')
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
have QTrans: "Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'" and xFreshT: "x \<sharp> T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' &&& x \<sharp> T
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> T

goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
from xFreshP PSimQ QTrans
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P
P \<leadsto>[Rel] Q
Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
obtain P' where PTrans:"P \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'"
                                          and Pderivative: "derivative P' Q' a x Rel"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P
P \<leadsto>[Rel] Q
Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'; derivative P' Q' a x Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'
derivative P' Q' a x Rel

goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
from PTrans xFreshR
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'
x \<sharp> R
[PROOF STEP]
have "P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<parallel> R"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'
x \<sharp> R

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<parallel> R
[PROOF STEP]
by(rule Late_Semantics.Par1B)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<parallel> R

goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<parallel> R

goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
from Pderivative xFreshR xFreshT RRel'T
[PROOF STATE]
proof (chain)
picking this:
derivative P' Q' a x Rel
x \<sharp> R
x \<sharp> T
(R, T) \<in> Rel'
[PROOF STEP]
have "derivative (P' \<parallel> R) (Q' \<parallel> T) a x Rel''"
[PROOF STATE]
proof (prove)
using this:
derivative P' Q' a x Rel
x \<sharp> R
x \<sharp> T
(R, T) \<in> Rel'

goal (1 subgoal):
 1. derivative (P' \<parallel> R) (Q' \<parallel> T) a x Rel''
[PROOF STEP]
by(cases a, auto intro: Par simp add: derivative_def forget)
[PROOF STATE]
proof (state)
this:
derivative (P' \<parallel> R) (Q' \<parallel> T) a x Rel''

goal (2 subgoals):
 1. \<And>P'. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'a \<and> derivative P'a (P' \<parallel> T) a x Rel''
 2. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<parallel> R
derivative (P' \<parallel> R) (Q' \<parallel> T) a x Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<parallel> R
derivative (P' \<parallel> R) (Q' \<parallel> T) a x Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q' \<parallel> T) a x Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q' \<parallel> T) a x Rel''

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
case(cPar2 T')
[PROOF STATE]
proof (state)
this:
T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> T'

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
have TTrans: "T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> T'" and xFreshQ: "x \<sharp> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> T' &&& x \<sharp> Q
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> T'
x \<sharp> Q

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
from xFreshR RSimT TTrans
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> R
R \<leadsto>[Rel'] T
T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> T'
[PROOF STEP]
obtain R' where RTrans:"R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'"
                                          and Rderivative: "derivative R' T' a x Rel'"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> R
R \<leadsto>[Rel'] T
T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> T'

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'; derivative R' T' a x Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
derivative R' T' a x Rel'

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
from RTrans xFreshP
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
x \<sharp> P
[PROOF STEP]
have ParTrans: "P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P \<parallel> R'"
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> R'
x \<sharp> P

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P \<parallel> R'
[PROOF STEP]
by(rule Late_Semantics.Par2B)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P \<parallel> R'

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P \<parallel> R'

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
from Rderivative xFreshP xFreshQ PRelQ
[PROOF STATE]
proof (chain)
picking this:
derivative R' T' a x Rel'
x \<sharp> P
x \<sharp> Q
(P, Q) \<in> Rel
[PROOF STEP]
have "derivative (P \<parallel> R') (Q \<parallel>  T') a x Rel''"
[PROOF STATE]
proof (prove)
using this:
derivative R' T' a x Rel'
x \<sharp> P
x \<sharp> Q
(P, Q) \<in> Rel

goal (1 subgoal):
 1. derivative (P \<parallel> R') (Q \<parallel> T') a x Rel''
[PROOF STEP]
by(cases a, auto intro: Par simp add: derivative_def forget)
[PROOF STATE]
proof (state)
this:
derivative (P \<parallel> R') (Q \<parallel> T') a x Rel''

goal (1 subgoal):
 1. \<And>Q'. T \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> Q') a x Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P \<parallel> R'
derivative (P \<parallel> R') (Q \<parallel> T') a x Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P \<parallel> R'
derivative (P \<parallel> R') (Q \<parallel> T') a x Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> T') a x Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' (Q \<parallel> T') a x Rel''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' a x Rel''

goal (1 subgoal):
 1. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
case(Free \<alpha> QT')
[PROOF STATE]
proof (state)
this:
Q \<parallel> T \<longmapsto> \<alpha> \<prec> QT'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
have QTTrans: "Q \<parallel> T \<longmapsto> \<alpha> \<prec> QT'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<parallel> T \<longmapsto> \<alpha> \<prec> QT'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<parallel> T \<longmapsto> \<alpha> \<prec> QT'

goal (1 subgoal):
 1. \<And>\<alpha> Q'. Q \<parallel> T \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel''
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
Q \<parallel> T \<longmapsto> \<alpha> \<prec> QT'

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QT') \<in> Rel''
[PROOF STEP]
using PSimQ RSimT PRelQ RRel'T
[PROOF STATE]
proof (prove)
using this:
Q \<parallel> T \<longmapsto> \<alpha> \<prec> QT'
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QT') \<in> Rel''
[PROOF STEP]
proof(induct rule: parCasesF[where C="(P, R)"])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
case(cPar1 Q')
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
have RRel'T: "(R, T) \<in> Rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R, T) \<in> Rel'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(R, T) \<in> Rel'

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
have "P \<leadsto>[Rel] Q" and "Q \<longmapsto> \<alpha> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[Rel] Q &&& Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P \<leadsto>[Rel] Q
Q \<longmapsto> \<alpha> \<prec> Q'

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> \<alpha> \<prec> P'" and PRel: "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> \<alpha> \<prec> P'; (P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> \<alpha> \<prec> P'
(P', Q') \<in> Rel

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
have Trans: "P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<parallel> R"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<parallel> R
[PROOF STEP]
by(rule Late_Semantics.Par1F)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<parallel> R

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<parallel> R

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PRel RRel'T
[PROOF STATE]
proof (chain)
picking this:
(P', Q') \<in> Rel
(R, T) \<in> Rel'
[PROOF STEP]
have "(P' \<parallel> R, Q' \<parallel> T) \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(P', Q') \<in> Rel
(R, T) \<in> Rel'

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

goal (6 subgoals):
 1. \<And>P'. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> P'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<alpha> \<prec> P'a \<and> (P'a, P' \<parallel> T) \<in> Rel''
 2. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 4. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 6. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<parallel> R
(P' \<parallel> R, Q' \<parallel> T) \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<parallel> R
(P' \<parallel> R, Q' \<parallel> T) \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q' \<parallel> T) \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q' \<parallel> T) \<in> Rel''

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
case(cPar2 T')
[PROOF STATE]
proof (state)
this:
T \<longmapsto> \<alpha> \<prec> T'
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
have PRelQ: "(P, Q) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (P, Q) \<in> Rel
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
have "R \<leadsto>[Rel'] T" and "T \<longmapsto> \<alpha> \<prec> T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<leadsto>[Rel'] T &&& T \<longmapsto> \<alpha> \<prec> T'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
R \<leadsto>[Rel'] T
T \<longmapsto> \<alpha> \<prec> T'

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R \<leadsto>[Rel'] T
T \<longmapsto> \<alpha> \<prec> T'
[PROOF STEP]
obtain R' where RTrans: "R \<longmapsto> \<alpha> \<prec> R'" and RRel: "(R', T') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[Rel'] T
T \<longmapsto> \<alpha> \<prec> T'

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R \<longmapsto> \<alpha> \<prec> R'; (R', T') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> \<alpha> \<prec> R'
(R', T') \<in> Rel'

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from RTrans
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto> \<alpha> \<prec> R'
[PROOF STEP]
have Trans: "P \<parallel> R \<longmapsto> \<alpha> \<prec> P \<parallel> R'"
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto> \<alpha> \<prec> R'

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> \<alpha> \<prec> P \<parallel> R'
[PROOF STEP]
by(rule Late_Semantics.Par2F)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P \<parallel> R'

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P \<parallel> R'

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PRelQ RRel
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> Rel
(R', T') \<in> Rel'
[PROOF STEP]
have "(P \<parallel> R', Q \<parallel> T') \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> Rel
(R', T') \<in> Rel'

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

goal (5 subgoals):
 1. \<And>Q'. \<lbrakk>T \<longmapsto> \<alpha> \<prec> Q'; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 3. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 5. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P \<parallel> R'
(P \<parallel> R', Q \<parallel> T') \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> \<alpha> \<prec> P \<parallel> R'
(P \<parallel> R', Q \<parallel> T') \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> T') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q \<parallel> T') \<in> Rel''

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
case(cComm1 Q' T' a b x)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a<x> \<prec> Q'
T \<longmapsto> a[b] \<prec> T'
x \<sharp> Q
x \<sharp> T
x \<noteq> a
x \<noteq> b
x \<sharp> T'
x \<sharp> (P, R)
\<alpha> = \<tau>
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>x \<sharp> (P, R)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> (P, R)
[PROOF STEP]
have "x \<sharp> P"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> (P, R)

goal (1 subgoal):
 1. x \<sharp> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> P

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
with \<open>P \<leadsto>[Rel] Q\<close> \<open>Q \<longmapsto> a<x> \<prec> Q'\<close> \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<x> \<prec> Q'
x \<sharp> P
x \<sharp> P
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>a<x> \<prec> P'"
                and Pderivative: "derivative P' Q' (InputS a) x Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<x> \<prec> Q'
x \<sharp> P
x \<sharp> P

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a<x> \<prec> P'; derivative P' Q' (InputS a) x Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<x> \<prec> P'
derivative P' Q' (InputS a) x Rel

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from Pderivative
[PROOF STATE]
proof (chain)
picking this:
derivative P' Q' (InputS a) x Rel
[PROOF STEP]
have PRel: "(P'[x::=b], Q'[x::=b]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
derivative P' Q' (InputS a) x Rel

goal (1 subgoal):
 1. (P'[x::=b], Q'[x::=b]) \<in> Rel
[PROOF STEP]
by(simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
(P'[x::=b], Q'[x::=b]) \<in> Rel

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
have "R \<leadsto>[Rel'] T" and "T \<longmapsto> a[b] \<prec> T'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<leadsto>[Rel'] T &&& T \<longmapsto> a[b] \<prec> T'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
R \<leadsto>[Rel'] T
T \<longmapsto> a[b] \<prec> T'

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
R \<leadsto>[Rel'] T
T \<longmapsto> a[b] \<prec> T'
[PROOF STEP]
obtain R' where RTrans: "R \<longmapsto>a[b] \<prec> R'" and RRel: "(R', T') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[Rel'] T
T \<longmapsto> a[b] \<prec> T'

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R \<longmapsto> a[b] \<prec> R'; (R', T') \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a[b] \<prec> R'
(R', T') \<in> Rel'

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PTrans RTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a<x> \<prec> P'
R \<longmapsto> a[b] \<prec> R'
[PROOF STEP]
have "P \<parallel> R \<longmapsto> \<tau> \<prec> P'[x::=b] \<parallel> R'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a<x> \<prec> P'
R \<longmapsto> a[b] \<prec> R'

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> \<tau> \<prec> P'[x::=b] \<parallel> R'
[PROOF STEP]
by(rule Late_Semantics.Comm1)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P'[x::=b] \<parallel> R'

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P'[x::=b] \<parallel> R'

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PRel RRel
[PROOF STATE]
proof (chain)
picking this:
(P'[x::=b], Q'[x::=b]) \<in> Rel
(R', T') \<in> Rel'
[PROOF STEP]
have "(P'[x::=b] \<parallel> R', Q'[x::=b] \<parallel> T') \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(P'[x::=b], Q'[x::=b]) \<in> Rel
(R', T') \<in> Rel'

goal (1 subgoal):
 1. (P'[x::=b] \<parallel> R', Q'[x::=b] \<parallel> T') \<in> Rel''
[PROOF STEP]
by(blast intro: Par)
[PROOF STATE]
proof (state)
this:
(P'[x::=b] \<parallel> R', Q'[x::=b] \<parallel> T') \<in> Rel''

goal (4 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a[b] \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> Q'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P'[x::=b] \<parallel> Q') \<in> Rel''
 2. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 4. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P'[x::=b] \<parallel> R'
(P'[x::=b] \<parallel> R', Q'[x::=b] \<parallel> T') \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P'[x::=b] \<parallel> R'
(P'[x::=b] \<parallel> R', Q'[x::=b] \<parallel> T') \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', Q'[x::=b] \<parallel> T') \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', Q'[x::=b] \<parallel> T') \<in> Rel''

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
case(cComm2 Q' T' a b x)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a[b] \<prec> Q'
T \<longmapsto> a<x> \<prec> T'
x \<sharp> Q
x \<sharp> T
x \<noteq> a
x \<noteq> b
x \<sharp> Q'
x \<sharp> (P, R)
\<alpha> = \<tau>
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
have "P \<leadsto>[Rel] Q" and "Q \<longmapsto>a[b] \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<leadsto>[Rel] Q &&& Q \<longmapsto> a[b] \<prec> Q'
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a[b] \<prec> Q'

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a[b] \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>a[b] \<prec> P'" and PRel: "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a[b] \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a[b] \<prec> P'; (P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a[b] \<prec> P'
(P', Q') \<in> Rel

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>x \<sharp> (P, R)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> (P, R)
[PROOF STEP]
have "x \<sharp> R"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> (P, R)

goal (1 subgoal):
 1. x \<sharp> R
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> R

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
with \<open>R \<leadsto>[Rel'] T\<close> \<open>T \<longmapsto>a<x> \<prec> T'\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<leadsto>[Rel'] T
T \<longmapsto> a<x> \<prec> T'
x \<sharp> R
[PROOF STEP]
obtain R' where RTrans: "R \<longmapsto>a<x> \<prec> R'"
                and Rderivative: "derivative R' T' (InputS a) x Rel'"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[Rel'] T
T \<longmapsto> a<x> \<prec> T'
x \<sharp> R

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R \<longmapsto> a<x> \<prec> R'; derivative R' T' (InputS a) x Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a<x> \<prec> R'
derivative R' T' (InputS a) x Rel'

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from Rderivative
[PROOF STATE]
proof (chain)
picking this:
derivative R' T' (InputS a) x Rel'
[PROOF STEP]
have RRel: "(R'[x::=b], T'[x::=b]) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
derivative R' T' (InputS a) x Rel'

goal (1 subgoal):
 1. (R'[x::=b], T'[x::=b]) \<in> Rel'
[PROOF STEP]
by(simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
(R'[x::=b], T'[x::=b]) \<in> Rel'

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PTrans RTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a[b] \<prec> P'
R \<longmapsto> a<x> \<prec> R'
[PROOF STEP]
have "P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<parallel> R'[x::=b]"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a[b] \<prec> P'
R \<longmapsto> a<x> \<prec> R'

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<parallel> R'[x::=b]
[PROOF STEP]
by(rule Late_Semantics.Comm2)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<parallel> R'[x::=b]

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<parallel> R'[x::=b]

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PRel RRel
[PROOF STATE]
proof (chain)
picking this:
(P', Q') \<in> Rel
(R'[x::=b], T'[x::=b]) \<in> Rel'
[PROOF STEP]
have "(P' \<parallel> R'[x::=b], Q' \<parallel> T'[x::=b]) \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(P', Q') \<in> Rel
(R'[x::=b], T'[x::=b]) \<in> Rel'

goal (1 subgoal):
 1. (P' \<parallel> R'[x::=b], Q' \<parallel> T'[x::=b]) \<in> Rel''
[PROOF STEP]
by(blast intro: Par)
[PROOF STATE]
proof (state)
this:
(P' \<parallel> R'[x::=b], Q' \<parallel> T'[x::=b]) \<in> Rel''

goal (3 subgoals):
 1. \<And>P' Q' a b x. \<lbrakk>Q \<longmapsto> a[b] \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> b; x \<sharp> P'; x \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, P' \<parallel> Q'[x::=b]) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 3. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<parallel> R'[x::=b]
(P' \<parallel> R'[x::=b], Q' \<parallel> T'[x::=b]) \<in> Rel''
[PROOF STEP]
show "\<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', Q' \<parallel> T'[x::=b]) \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<parallel> R'[x::=b]
(P' \<parallel> R'[x::=b], Q' \<parallel> T'[x::=b]) \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', Q' \<parallel> T'[x::=b]) \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', Q' \<parallel> T'[x::=b]) \<in> Rel''

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
case(cClose1 Q' T' a x y)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a<x> \<prec> Q'
T \<longmapsto> a<\<nu>y> \<prec> T'
x \<sharp> Q
x \<sharp> T
x \<noteq> a
x \<noteq> y
x \<sharp> T'
y \<sharp> Q
y \<sharp> T
y \<noteq> a
y \<sharp> Q'
x \<sharp> (P, R)
y \<sharp> (P, R)
\<alpha> = \<tau>
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>x \<sharp> (P, R)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> (P, R)
[PROOF STEP]
have "x \<sharp> P"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> (P, R)

goal (1 subgoal):
 1. x \<sharp> P
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<sharp> P

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
with \<open>P \<leadsto>[Rel] Q\<close> \<open>Q \<longmapsto>a<x> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<x> \<prec> Q'
x \<sharp> P
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>a<x> \<prec> P'"
                and Pderivative: "derivative P' Q' (InputS a) x Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<x> \<prec> Q'
x \<sharp> P

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a<x> \<prec> P'; derivative P' Q' (InputS a) x Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<x> \<prec> P'
derivative P' Q' (InputS a) x Rel

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from Pderivative
[PROOF STATE]
proof (chain)
picking this:
derivative P' Q' (InputS a) x Rel
[PROOF STEP]
have PRel: "(P'[x::=y], Q'[x::=y]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
derivative P' Q' (InputS a) x Rel

goal (1 subgoal):
 1. (P'[x::=y], Q'[x::=y]) \<in> Rel
[PROOF STEP]
by(simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
(P'[x::=y], Q'[x::=y]) \<in> Rel

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>y \<sharp> (P, R)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> (P, R)
[PROOF STEP]
have "y \<sharp> R" and "y \<sharp> P"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> (P, R)

goal (1 subgoal):
 1. y \<sharp> R &&& y \<sharp> P
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
y \<sharp> R
y \<sharp> P

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>R \<leadsto>[Rel'] T\<close> \<open>T \<longmapsto>a<\<nu>y> \<prec> T'\<close> \<open>y \<sharp> R\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<leadsto>[Rel'] T
T \<longmapsto> a<\<nu>y> \<prec> T'
y \<sharp> R
[PROOF STEP]
obtain R' where RTrans: "R \<longmapsto>a<\<nu>y> \<prec> R'"
                and Rderivative: "derivative R' T' (BoundOutputS a) y Rel'"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[Rel'] T
T \<longmapsto> a<\<nu>y> \<prec> T'
y \<sharp> R

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R \<longmapsto> a<\<nu>y> \<prec> R'; derivative R' T' (BoundOutputS a) y Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(blast dest: simE)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a<\<nu>y> \<prec> R'
derivative R' T' (BoundOutputS a) y Rel'

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from Rderivative
[PROOF STATE]
proof (chain)
picking this:
derivative R' T' (BoundOutputS a) y Rel'
[PROOF STEP]
have RRel: "(R', T') \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
derivative R' T' (BoundOutputS a) y Rel'

goal (1 subgoal):
 1. (R', T') \<in> Rel'
[PROOF STEP]
by(simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
(R', T') \<in> Rel'

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PTrans RTrans \<open>y \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a<x> \<prec> P'
R \<longmapsto> a<\<nu>y> \<prec> R'
y \<sharp> P
[PROOF STEP]
have Trans: "P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P'[x::=y] \<parallel> R')"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a<x> \<prec> P'
R \<longmapsto> a<\<nu>y> \<prec> R'
y \<sharp> P

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P'[x::=y] \<parallel> R')
[PROOF STEP]
by(rule Late_Semantics.Close1)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P'[x::=y] \<parallel> R')

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P'[x::=y] \<parallel> R')

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PRel RRel
[PROOF STATE]
proof (chain)
picking this:
(P'[x::=y], Q'[x::=y]) \<in> Rel
(R', T') \<in> Rel'
[PROOF STEP]
have "(<\<nu>y>(P'[x::=y] \<parallel> R'), <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(P'[x::=y], Q'[x::=y]) \<in> Rel
(R', T') \<in> Rel'

goal (1 subgoal):
 1. (<\<nu>y>(P'[x::=y] \<parallel> R'), <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''
[PROOF STEP]
by(blast intro: Par Res)
[PROOF STATE]
proof (state)
this:
(<\<nu>y>(P'[x::=y] \<parallel> R'), <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''

goal (2 subgoals):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<x> \<prec> P'; T \<longmapsto> a<\<nu>y> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> Q'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> P'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P'[x::=y] \<parallel> Q')) \<in> Rel''
 2. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P'[x::=y] \<parallel> R')
(<\<nu>y>(P'[x::=y] \<parallel> R'), <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P'[x::=y] \<parallel> R')
(<\<nu>y>(P'[x::=y] \<parallel> R'), <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', <\<nu>y>(Q'[x::=y] \<parallel> T')) \<in> Rel''

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
case(cClose2 Q' T' a x y)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a<\<nu>y> \<prec> Q'
T \<longmapsto> a<x> \<prec> T'
x \<sharp> Q
x \<sharp> T
x \<noteq> a
x \<noteq> y
x \<sharp> Q'
y \<sharp> Q
y \<sharp> T
y \<noteq> a
y \<sharp> T'
x \<sharp> (P, R)
y \<sharp> (P, R)
\<alpha> = \<tau>
P \<leadsto>[Rel] Q
R \<leadsto>[Rel'] T
(P, Q) \<in> Rel
(R, T) \<in> Rel'

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>y \<sharp> (P, R)\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<sharp> (P, R)
[PROOF STEP]
have "y \<sharp> P" and "y \<sharp> R"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> (P, R)

goal (1 subgoal):
 1. y \<sharp> P &&& y \<sharp> R
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
y \<sharp> P
y \<sharp> R

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>P \<leadsto>[Rel] Q\<close> \<open>Q \<longmapsto>a<\<nu>y> \<prec> Q'\<close> \<open>y \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<\<nu>y> \<prec> Q'
y \<sharp> P
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>a<\<nu>y> \<prec> P'" and P'RelQ': "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a<\<nu>y> \<prec> Q'
y \<sharp> P

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a<\<nu>y> \<prec> P'; (P', Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force dest: simE simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
P \<longmapsto> a<\<nu>y> \<prec> P'
(P', Q') \<in> Rel

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from \<open>x \<sharp> (P, R)\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> (P, R)
[PROOF STEP]
have "x \<sharp> R"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> (P, R)

goal (1 subgoal):
 1. x \<sharp> R
[PROOF STEP]
by simp+
[PROOF STATE]
proof (state)
this:
x \<sharp> R

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
with \<open>R \<leadsto>[Rel'] T\<close> \<open>T \<longmapsto>a<x> \<prec> T'\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<leadsto>[Rel'] T
T \<longmapsto> a<x> \<prec> T'
x \<sharp> R
[PROOF STEP]
obtain R' where RTrans: "R \<longmapsto>a<x> \<prec> R'"
                and R'Rel'T': "(R'[x::=y], T'[x::=y]) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
R \<leadsto>[Rel'] T
T \<longmapsto> a<x> \<prec> T'
x \<sharp> R

goal (1 subgoal):
 1. (\<And>R'. \<lbrakk>R \<longmapsto> a<x> \<prec> R'; (R'[x::=y], T'[x::=y]) \<in> Rel'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force dest: simE simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
R \<longmapsto> a<x> \<prec> R'
(R'[x::=y], T'[x::=y]) \<in> Rel'

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from PTrans RTrans \<open>y \<sharp> R\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> a<\<nu>y> \<prec> P'
R \<longmapsto> a<x> \<prec> R'
y \<sharp> R
[PROOF STEP]
have Trans: "P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P' \<parallel> R'[x::=y])"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> a<\<nu>y> \<prec> P'
R \<longmapsto> a<x> \<prec> R'
y \<sharp> R

goal (1 subgoal):
 1. P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P' \<parallel> R'[x::=y])
[PROOF STEP]
by(rule Close2)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P' \<parallel> R'[x::=y])

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P' \<parallel> R'[x::=y])

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
from P'RelQ' R'Rel'T'
[PROOF STATE]
proof (chain)
picking this:
(P', Q') \<in> Rel
(R'[x::=y], T'[x::=y]) \<in> Rel'
[PROOF STEP]
have "(<\<nu>y>(P' \<parallel> R'[x::=y]), <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''"
[PROOF STATE]
proof (prove)
using this:
(P', Q') \<in> Rel
(R'[x::=y], T'[x::=y]) \<in> Rel'

goal (1 subgoal):
 1. (<\<nu>y>(P' \<parallel> R'[x::=y]), <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''
[PROOF STEP]
by(blast intro: Par Res)
[PROOF STATE]
proof (state)
this:
(<\<nu>y>(P' \<parallel> R'[x::=y]), <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''

goal (1 subgoal):
 1. \<And>P' Q' a x y. \<lbrakk>Q \<longmapsto> a<\<nu>y> \<prec> P'; T \<longmapsto> a<x> \<prec> Q'; x \<sharp> Q; x \<sharp> T; x \<noteq> a; x \<noteq> y; x \<sharp> P'; y \<sharp> Q; y \<sharp> T; y \<noteq> a; y \<sharp> Q'; x \<sharp> (P, R); y \<sharp> (P, R); \<alpha> = \<tau>; P \<leadsto>[Rel] Q; R \<leadsto>[Rel'] T; (P, Q) \<in> Rel; (R, T) \<in> Rel'\<rbrakk> \<Longrightarrow> \<exists>P'a. P \<parallel> R \<longmapsto> \<tau> \<prec> P'a \<and> (P'a, <\<nu>y>(P' \<parallel> Q'[x::=y])) \<in> Rel''
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P' \<parallel> R'[x::=y])
(<\<nu>y>(P' \<parallel> R'[x::=y]), <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
P \<parallel> R \<longmapsto> \<tau> \<prec> <\<nu>y>(P' \<parallel> R'[x::=y])
(<\<nu>y>(P' \<parallel> R'[x::=y]), <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''

goal (1 subgoal):
 1. \<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<tau> \<prec> P' \<and> (P', <\<nu>y>(Q' \<parallel> T'[x::=y])) \<in> Rel''

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. P \<parallel> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QT') \<in> Rel''

goal:
No subgoals!
[PROOF STEP]
qed