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

  assumes PRelQ: "(P, Q) \<in> Rel"

  shows "\<tau>.(P) \<leadsto>[Rel] \<tau>.(Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>.P \<leadsto>[Rel] \<tau>.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau>.P \<leadsto>[Rel] \<tau>.Q
[PROOF STEP]
show "\<tau>.(P) \<leadsto>[Rel] \<tau>.(Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>.P \<leadsto>[Rel] \<tau>.Q
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>\<tau>.Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> \<tau>.P\<rbrakk> \<Longrightarrow> \<exists>P'. \<tau>.P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel
 2. \<And>\<alpha> Q'. \<tau>.Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. \<tau>.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
case(Bound a x Q')
[PROOF STATE]
proof (state)
this:
\<tau>.Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> \<tau>.P

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P'. \<tau>.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
proof(induct rule: tauCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<alpha> = \<tau>; Q = Q'\<rbrakk> \<Longrightarrow> \<exists>P'. \<tau>.P \<longmapsto> \<tau> \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
case cTau
[PROOF STATE]
proof (state)
this:
\<alpha> = \<tau>
Q = Q'

goal (1 subgoal):
 1. \<lbrakk>\<alpha> = \<tau>; Q = Q'\<rbrakk> \<Longrightarrow> \<exists>P'. \<tau>.P \<longmapsto> \<tau> \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
have "\<tau>.(P) \<longmapsto> \<tau> \<prec> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>.P \<longmapsto> \<tau> \<prec> P
[PROOF STEP]
by(rule Late_Semantics.Tau)
[PROOF STATE]
proof (state)
this:
\<tau>.P \<longmapsto> \<tau> \<prec> P

goal (1 subgoal):
 1. \<lbrakk>\<alpha> = \<tau>; Q = Q'\<rbrakk> \<Longrightarrow> \<exists>P'. \<tau>.P \<longmapsto> \<tau> \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
with PRelQ
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> Rel
\<tau>.P \<longmapsto> \<tau> \<prec> P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> Rel
\<tau>.P \<longmapsto> \<tau> \<prec> P

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<tau>.P \<leadsto>[Rel] \<tau>.Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inputPres:
  fixes P    :: pi
  and   x    :: name
  and   Q    :: pi
  and   a    :: name
  and   Rel  :: "(pi \<times> pi) set"

  assumes PRelQ: "\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel"
  and     Eqvt: "eqvt Rel"

  shows "a<x>.P \<leadsto>[Rel] a<x>.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a<x>.P \<leadsto>[Rel] a<x>.Q
[PROOF STEP]
using Eqvt
[PROOF STATE]
proof (prove)
using this:
eqvt Rel

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

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

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

goal (2 subgoals):
 1. \<And>aa xa Q'. \<lbrakk>a<x>.Q \<longmapsto> aa\<guillemotleft>xa\<guillemotright> \<prec> Q'; xa \<sharp> a<x>.P; xa \<sharp> a<x>.Q; xa \<sharp> aa; xa \<sharp> (x, a, P, Q)\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> aa\<guillemotleft>xa\<guillemotright> \<prec> P' \<and> derivative P' Q' aa xa Rel
 2. \<And>\<alpha> Q'. a<x>.Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
from \<open>a<x>.Q \<longmapsto>b\<guillemotleft>y\<guillemotright> \<prec> Q'\<close> \<open>y \<noteq> a\<close> \<open>y \<noteq> x\<close> \<open>y \<sharp> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
a<x>.Q \<longmapsto> b\<guillemotleft>y\<guillemotright> \<prec> Q'
y \<noteq> a
y \<noteq> x
y \<sharp> Q
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a<x>.Q \<longmapsto> b\<guillemotleft>y\<guillemotright> \<prec> Q'
y \<noteq> a
y \<noteq> x
y \<sharp> Q

goal (1 subgoal):
 1. \<exists>P'. a<x>.P \<longmapsto> b\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' b y Rel
[PROOF STEP]
proof(induct rule: inputCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>b = InputS a; Q' = [(x, y)] \<bullet> Q\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
case cInput
[PROOF STATE]
proof (state)
this:
b = InputS a
Q' = [(x, y)] \<bullet> Q

goal (1 subgoal):
 1. \<lbrakk>b = InputS a; Q' = [(x, y)] \<bullet> Q\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
have "a<x>.P \<longmapsto> a<x> \<prec> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a<x>.P \<longmapsto> a<x> \<prec> P
[PROOF STEP]
by(rule Input)
[PROOF STATE]
proof (state)
this:
a<x>.P \<longmapsto> a<x> \<prec> P

goal (1 subgoal):
 1. \<lbrakk>b = InputS a; Q' = [(x, y)] \<bullet> Q\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
hence "a<x>.P \<longmapsto> a<y> \<prec> ([(x, y)] \<bullet> P)"
[PROOF STATE]
proof (prove)
using this:
a<x>.P \<longmapsto> a<x> \<prec> P

goal (1 subgoal):
 1. a<x>.P \<longmapsto> a<y> \<prec> [(x, y)] \<bullet> P
[PROOF STEP]
using \<open>y \<sharp> P\<close>
[PROOF STATE]
proof (prove)
using this:
a<x>.P \<longmapsto> a<x> \<prec> P
y \<sharp> P

goal (1 subgoal):
 1. a<x>.P \<longmapsto> a<y> \<prec> [(x, y)] \<bullet> P
[PROOF STEP]
by(simp add: alphaBoundResidual)
[PROOF STATE]
proof (state)
this:
a<x>.P \<longmapsto> a<y> \<prec> [(x, y)] \<bullet> P

goal (1 subgoal):
 1. \<lbrakk>b = InputS a; Q' = [(x, y)] \<bullet> Q\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
a<x>.P \<longmapsto> a<y> \<prec> [(x, y)] \<bullet> P

goal (1 subgoal):
 1. \<lbrakk>b = InputS a; Q' = [(x, y)] \<bullet> Q\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
have "derivative ([(x, y)] \<bullet> P) ([(x, y)] \<bullet> Q) (InputS a) y Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derivative ([(x, y)] \<bullet> P) ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
proof(auto simp add: derivative_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>u. (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
show "(([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
proof(cases "y=u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. y = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
assume "y = u"
[PROOF STATE]
proof (state)
this:
y = u

goal (2 subgoals):
 1. y = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y = u

goal (2 subgoals):
 1. y = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
have "([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel
[PROOF STEP]
have "(P[x::=x], Q[x::=x]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel

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

goal (1 subgoal):
 1. ([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel
[PROOF STEP]
hence "(P, Q) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(P[x::=x], Q[x::=x]) \<in> Rel

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

goal (1 subgoal):
 1. ([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel
[PROOF STEP]
with Eqvt
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(P, Q) \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P, Q) \<in> Rel

goal (1 subgoal):
 1. ([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel

goal (2 subgoals):
 1. y = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y = u
([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y = u
([(y, x)] \<bullet> P, [(y, x)] \<bullet> Q) \<in> Rel

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

goal (1 subgoal):
 1. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
assume yinequ: "y \<noteq> u"
[PROOF STATE]
proof (state)
this:
y \<noteq> u

goal (1 subgoal):
 1. y \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
proof(cases "x = u")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
assume "x = u"
[PROOF STATE]
proof (state)
this:
x = u

goal (2 subgoals):
 1. x = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
x = u

goal (2 subgoals):
 1. x = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
have "(([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel
[PROOF STEP]
have "(P[x::=y], Q[x::=y]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel

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

goal (1 subgoal):
 1. (([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel
[PROOF STEP]
with Eqvt
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(P[x::=y], Q[x::=y]) \<in> Rel
[PROOF STEP]
have "([(y, x)] \<bullet> (P[x::=y]), [(y, x)] \<bullet> (Q[x::=y])) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P[x::=y], Q[x::=y]) \<in> Rel

goal (1 subgoal):
 1. ([(y, x)] \<bullet> P[x::=y], [(y, x)] \<bullet> Q[x::=y]) \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
([(y, x)] \<bullet> P[x::=y], [(y, x)] \<bullet> Q[x::=y]) \<in> Rel

goal (1 subgoal):
 1. (([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel
[PROOF STEP]
with \<open>y \<noteq> x\<close>
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> x
([(y, x)] \<bullet> P[x::=y], [(y, x)] \<bullet> Q[x::=y]) \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
([(y, x)] \<bullet> P[x::=y], [(y, x)] \<bullet> Q[x::=y]) \<in> Rel

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel

goal (2 subgoals):
 1. x = u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
 2. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
x = u
(([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x = u
(([(y, x)] \<bullet> P)[y::=x], ([(y, x)] \<bullet> Q)[y::=x]) \<in> Rel

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

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
assume xinequ: "x \<noteq> u"
[PROOF STATE]
proof (state)
this:
x \<noteq> u

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
hence "(([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> u

goal (1 subgoal):
 1. (([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel
[PROOF STEP]
have "(P[x::=u], Q[x::=u]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. (P[x::=y], Q[x::=y]) \<in> Rel

goal (1 subgoal):
 1. (P[x::=u], Q[x::=u]) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P[x::=u], Q[x::=u]) \<in> Rel

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
with Eqvt
[PROOF STATE]
proof (chain)
picking this:
eqvt Rel
(P[x::=u], Q[x::=u]) \<in> Rel
[PROOF STEP]
have "([(y, x)] \<bullet> (P[x::=u]), [(y, x)] \<bullet> (Q[x::=u])) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
eqvt Rel
(P[x::=u], Q[x::=u]) \<in> Rel

goal (1 subgoal):
 1. ([(y, x)] \<bullet> P[x::=u], [(y, x)] \<bullet> Q[x::=u]) \<in> Rel
[PROOF STEP]
by(rule eqvtRelI)
[PROOF STATE]
proof (state)
this:
([(y, x)] \<bullet> P[x::=u], [(y, x)] \<bullet> Q[x::=u]) \<in> Rel

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
with \<open>y \<noteq> x\<close>  xinequ yinequ
[PROOF STATE]
proof (chain)
picking this:
y \<noteq> x
x \<noteq> u
y \<noteq> u
([(y, x)] \<bullet> P[x::=u], [(y, x)] \<bullet> Q[x::=u]) \<in> Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<noteq> x
x \<noteq> u
y \<noteq> u
([(y, x)] \<bullet> P[x::=u], [(y, x)] \<bullet> Q[x::=u]) \<in> Rel

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel

goal (1 subgoal):
 1. x \<noteq> u \<Longrightarrow> (([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(([(y, x)] \<bullet> P)[y::=u], ([(y, x)] \<bullet> Q)[y::=u]) \<in> Rel

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(([(x, y)] \<bullet> P)[y::=u], ([(x, y)] \<bullet> Q)[y::=u]) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
derivative ([(x, y)] \<bullet> P) ([(x, y)] \<bullet> Q) (InputS a) y Rel

goal (1 subgoal):
 1. \<lbrakk>b = InputS a; Q' = [(x, y)] \<bullet> Q\<rbrakk> \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
a<x>.P \<longmapsto> a<y> \<prec> [(x, y)] \<bullet> P
derivative ([(x, y)] \<bullet> P) ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
a<x>.P \<longmapsto> a<y> \<prec> [(x, y)] \<bullet> P
derivative ([(x, y)] \<bullet> P) ([(x, y)] \<bullet> Q) (InputS a) y Rel

goal (1 subgoal):
 1. \<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. a<x>.P \<longmapsto> a<y> \<prec> P' \<and> derivative P' ([(x, y)] \<bullet> Q) (InputS a) y Rel

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

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

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

goal (1 subgoal):
 1. \<And>\<alpha> Q'. a<x>.Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. a<x>.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
a<x>.Q \<longmapsto> \<alpha> \<prec> Q'

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma outputPres:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: name
  and   b    :: name
  and   Rel  :: "(pi \<times> pi) set"
  and   Rel' :: "(pi \<times> pi) set"

  assumes PRelQ: "(P, Q) \<in> Rel"

  shows "a{b}.P \<leadsto>[Rel] a{b}.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a{b}.P \<leadsto>[Rel] a{b}.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a{b}.P \<leadsto>[Rel] a{b}.Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a{b}.P \<leadsto>[Rel] a{b}.Q
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa y Q'. \<lbrakk>a{b}.Q \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> a{b}.P\<rbrakk> \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' aa y Rel
 2. \<And>\<alpha> Q'. a{b}.Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
case(Bound c x Q')
[PROOF STATE]
proof (state)
this:
a{b}.Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> a{b}.P

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

goal (2 subgoals):
 1. \<And>aa y Q'. \<lbrakk>a{b}.Q \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> a{b}.P\<rbrakk> \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' aa y Rel
 2. \<And>\<alpha> Q'. a{b}.Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
hence False
[PROOF STATE]
proof (prove)
using this:
a{b}.Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'

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

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

goal (1 subgoal):
 1. \<exists>P'. a{b}.P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>P'. a{b}.P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel

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

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

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

goal (1 subgoal):
 1. \<exists>P'. a{b}.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel
[PROOF STEP]
proof(induct rule: outputCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<alpha> = a[b]; Q = Q'\<rbrakk> \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> a[b] \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
case cOutput
[PROOF STATE]
proof (state)
this:
\<alpha> = a[b]
Q = Q'

goal (1 subgoal):
 1. \<lbrakk>\<alpha> = a[b]; Q = Q'\<rbrakk> \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> a[b] \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
have "a{b}.P \<longmapsto> a[b] \<prec> P"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a{b}.P \<longmapsto> a[b] \<prec> P
[PROOF STEP]
by(rule Late_Semantics.Output)
[PROOF STATE]
proof (state)
this:
a{b}.P \<longmapsto> a[b] \<prec> P

goal (1 subgoal):
 1. \<lbrakk>\<alpha> = a[b]; Q = Q'\<rbrakk> \<Longrightarrow> \<exists>P'. a{b}.P \<longmapsto> a[b] \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
with PRelQ
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> Rel
a{b}.P \<longmapsto> a[b] \<prec> P
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> Rel
a{b}.P \<longmapsto> a[b] \<prec> P

goal (1 subgoal):
 1. \<exists>P'. a{b}.P \<longmapsto> a[b] \<prec> P' \<and> (P', Q) \<in> Rel
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P'. a{b}.P \<longmapsto> a[b] \<prec> P' \<and> (P', Q) \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P'. a{b}.P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
a{b}.P \<leadsto>[Rel] a{b}.Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchPres:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: name
  and   b    :: name
  and   Rel  :: "(pi \<times> pi) set"
  and   Rel' :: "(pi \<times> pi) set"

  assumes PSimQ: "P \<leadsto>[Rel] Q"
  and     "Rel \<subseteq> Rel'"

  shows "[a\<frown>b]P \<leadsto>[Rel'] [a\<frown>b]Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<frown>b]P \<leadsto>[Rel'] [a\<frown>b]Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<frown>b]P \<leadsto>[Rel'] [a\<frown>b]Q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<frown>b]P \<leadsto>[Rel'] [a\<frown>b]Q
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa y Q'. \<lbrakk>[a\<frown>b]Q \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> [a\<frown>b]P\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>b]P \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' aa y Rel'
 2. \<And>\<alpha> Q'. [a\<frown>b]Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. [a\<frown>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case(Bound c x Q')
[PROOF STATE]
proof (state)
this:
[a\<frown>b]Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> [a\<frown>b]P

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P'. [a\<frown>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
proof(induct rule: matchCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
case cMatch
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
a = b

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
have "Q \<longmapsto>c\<guillemotleft>x\<guillemotright> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
with PSimQ xFreshP
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
x \<sharp> P
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>c\<guillemotleft>x\<guillemotright> \<prec> P'"
                                     and Pderivative: "derivative P' Q' c x Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
x \<sharp> P
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'

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

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
[PROOF STEP]
have "[a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'

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

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
from Pderivative \<open>Rel \<subseteq> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivative P' Q' c x Rel
Rel \<subseteq> Rel'
[PROOF STEP]
have "derivative P' Q' c x Rel'"
[PROOF STATE]
proof (prove)
using this:
derivative P' Q' c x Rel
Rel \<subseteq> Rel'

goal (1 subgoal):
 1. derivative P' Q' c x Rel'
[PROOF STEP]
by(cases c) (auto simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
derivative P' Q' c x Rel'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
derivative P' Q' c x Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[a\<frown>a]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
derivative P' Q' c x Rel'

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P'. [a\<frown>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
proof(induct rule: matchCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case cMatch
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'
a = b

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
have "Q \<longmapsto> \<alpha> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with PSimQ
[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 (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
have "[a\<frown>a]P \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<alpha> \<prec> P'

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

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a = b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<frown>a]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with PRel \<open>Rel \<subseteq> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
(P', Q') \<in> Rel
Rel \<subseteq> Rel'
[a\<frown>a]P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P', Q') \<in> Rel
Rel \<subseteq> Rel'
[a\<frown>a]P \<longmapsto> \<alpha> \<prec> P'

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
[a\<frown>b]P \<leadsto>[Rel'] [a\<frown>b]Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mismatchPres:
  fixes P    :: pi
  and   Q    :: pi
  and   a    :: name
  and   b    :: name
  and   Rel  :: "(pi \<times> pi) set"
  and   Rel' :: "(pi \<times> pi) set"

  assumes PSimQ: "P \<leadsto>[Rel] Q"
  and     "Rel \<subseteq> Rel'"

  shows "[a\<noteq>b]P \<leadsto>[Rel'] [a\<noteq>b]Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>b]P \<leadsto>[Rel'] [a\<noteq>b]Q
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>aa y Q'. \<lbrakk>[a\<noteq>b]Q \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> [a\<noteq>b]P\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' aa y Rel'
 2. \<And>\<alpha> Q'. [a\<noteq>b]Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case(Bound c x Q')
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
x \<sharp> [a\<noteq>b]P

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

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

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

goal (2 subgoals):
 1. \<And>aa y Q'. \<lbrakk>[a\<noteq>b]Q \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> [a\<noteq>b]P\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> aa\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' aa y Rel'
 2. \<And>\<alpha> Q'. [a\<noteq>b]Q \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from \<open>[a\<noteq>b]Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
[a\<noteq>b]Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[a\<noteq>b]Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (1 subgoal):
 1. \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
proof(induct rule: mismatchCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
case cMismatch
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
a \<noteq> b

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
have "Q \<longmapsto>c\<guillemotleft>x\<guillemotright> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
with PSimQ xFreshP
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
x \<sharp> P
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>c\<guillemotleft>x\<guillemotright> \<prec> P'"
                                   and Pderivative: "derivative P' Q' c x Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
x \<sharp> P
Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'

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

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
from PTrans \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
a \<noteq> b
[PROOF STEP]
have "[a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
a \<noteq> b

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

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
from Pderivative \<open>Rel \<subseteq> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivative P' Q' c x Rel
Rel \<subseteq> Rel'
[PROOF STEP]
have "derivative P' Q' c x Rel'"
[PROOF STATE]
proof (prove)
using this:
derivative P' Q' c x Rel
Rel \<subseteq> Rel'

goal (1 subgoal):
 1. derivative P' Q' c x Rel'
[PROOF STEP]
by(cases c) (auto simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
derivative P' Q' c x Rel'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' Q' c x Rel'
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
[a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
derivative P' Q' c x Rel'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
[a\<noteq>b]P \<longmapsto> c\<guillemotleft>x\<guillemotright> \<prec> P'
derivative P' Q' c x Rel'

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

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

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

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

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

goal (1 subgoal):
 1. \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
proof(induct rule: mismatchCases)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case cMismatch
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'
a \<noteq> b

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
have "Q \<longmapsto> \<alpha> \<prec> Q'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> \<alpha> \<prec> Q'
[PROOF STEP]
by fact
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with PSimQ
[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 (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
from PTrans \<open>a \<noteq> b\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> \<alpha> \<prec> P'
a \<noteq> b
[PROOF STEP]
have "[a\<noteq>b]P \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<alpha> \<prec> P'
a \<noteq> b

goal (1 subgoal):
 1. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
by(rule Late_Semantics.Mismatch)
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P'

goal (1 subgoal):
 1. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; a \<noteq> b\<rbrakk> \<Longrightarrow> \<exists>P'. [a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
with PRel \<open>Rel \<subseteq> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
(P', Q') \<in> Rel
Rel \<subseteq> Rel'
[a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P', Q') \<in> Rel
Rel \<subseteq> Rel'
[a\<noteq>b]P \<longmapsto> \<alpha> \<prec> P'

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sumPres:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi

  assumes PSimQ: "P \<leadsto>[Rel] Q"
  and     "Id \<subseteq> Rel'"
  and     "Rel \<subseteq> Rel'"

  shows "P \<oplus> R \<leadsto>[Rel'] Q \<oplus> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> R \<leadsto>[Rel'] Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> R \<leadsto>[Rel'] Q \<oplus> R
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> R \<leadsto>[Rel'] Q \<oplus> R
[PROOF STEP]
proof(induct rule: simCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a y Q'. \<lbrakk>Q \<oplus> R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; y \<sharp> P \<oplus> R\<rbrakk> \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' Q' a y Rel'
 2. \<And>\<alpha> Q'. Q \<oplus> R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case(Bound a x QR)
[PROOF STATE]
proof (state)
this:
Q \<oplus> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR
x \<sharp> P \<oplus> R

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

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

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

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

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

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

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

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

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P'; derivative P' QR 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' QR a x Rel

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

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

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

goal (2 subgoals):
 1. Q \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' QR a x Rel'
 2. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' QR a x Rel'
[PROOF STEP]
from Pderivative \<open>Rel \<subseteq> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
derivative P' QR a x Rel
Rel \<subseteq> Rel'
[PROOF STEP]
have "derivative P' QR a x Rel'"
[PROOF STATE]
proof (prove)
using this:
derivative P' QR a x Rel
Rel \<subseteq> Rel'

goal (1 subgoal):
 1. derivative P' QR a x Rel'
[PROOF STEP]
by(cases a) (auto simp add: derivative_def)
[PROOF STATE]
proof (state)
this:
derivative P' QR a x Rel'

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

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

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

goal (1 subgoal):
 1. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' QR a x Rel'
[PROOF STEP]
from \<open>R \<longmapsto>a\<guillemotleft>x\<guillemotright> \<prec> QR\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR
[PROOF STEP]
have "P \<oplus> R \<longmapsto>a\<guillemotleft>x\<guillemotright> \<prec> QR"
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR

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

goal (1 subgoal):
 1. R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> P' \<and> derivative P' QR a x Rel'
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
P \<oplus> R \<longmapsto> a\<guillemotleft>x\<guillemotright> \<prec> QR

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

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

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

goal (1 subgoal):
 1. \<And>\<alpha> Q'. Q \<oplus> R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<oplus> 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 \<oplus> R \<longmapsto> \<alpha> \<prec> Q' \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', Q') \<in> Rel'
[PROOF STEP]
case(Free \<alpha> QR)
[PROOF STATE]
proof (state)
this:
Q \<oplus> R \<longmapsto> \<alpha> \<prec> QR

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

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

goal (1 subgoal):
 1. \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
proof(induct rule: sumCases)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
 2. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
case cSum1
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> QR

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

goal (2 subgoals):
 1. Q \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
 2. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
with PSimQ
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> \<alpha> \<prec> QR
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>\<alpha> \<prec> P'" and PRel: "(P', QR) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> \<alpha> \<prec> QR

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

goal (2 subgoals):
 1. Q \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
 2. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
from PTrans
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
have "P \<oplus> R \<longmapsto>\<alpha> \<prec> P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<alpha> \<prec> P'

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

goal (2 subgoals):
 1. Q \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
 2. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
with PRel \<open>Rel \<subseteq> Rel'\<close>
[PROOF STATE]
proof (chain)
picking this:
(P', QR) \<in> Rel
Rel \<subseteq> Rel'
P \<oplus> R \<longmapsto> \<alpha> \<prec> P'
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(P', QR) \<in> Rel
Rel \<subseteq> Rel'
P \<oplus> R \<longmapsto> \<alpha> \<prec> P'

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

goal (1 subgoal):
 1. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
case cSum2
[PROOF STATE]
proof (state)
this:
R \<longmapsto> \<alpha> \<prec> QR

goal (1 subgoal):
 1. R \<longmapsto> \<alpha> \<prec> QR \<Longrightarrow> \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
from \<open>R \<longmapsto>\<alpha> \<prec> QR\<close>
[PROOF STATE]
proof (chain)
picking this:
R \<longmapsto> \<alpha> \<prec> QR
[PROOF STEP]
have "P \<oplus> R \<longmapsto>\<alpha> \<prec> QR"
[PROOF STATE]
proof (prove)
using this:
R \<longmapsto> \<alpha> \<prec> QR

goal (1 subgoal):
 1. P \<oplus> R \<longmapsto> \<alpha> \<prec> QR
[PROOF STEP]
by(rule Sum2)
[PROOF STATE]
proof (state)
this:
P \<oplus> R \<longmapsto> \<alpha> \<prec> QR

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

goal (1 subgoal):
 1. \<exists>P'. P \<oplus> R \<longmapsto> \<alpha> \<prec> P' \<and> (P', QR) \<in> Rel'
[PROOF STEP]
using \<open>Id \<subseteq> Rel'\<close>
[PROOF STATE]
proof (prove)
using this:
P \<oplus> R \<longmapsto> \<alpha> \<prec> QR
Id \<subseteq> Rel'

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

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<oplus> R \<leadsto>[Rel'] Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed