[STATEMENT]
lemma parPres:
  fixes P   :: pi
  and   Q   :: pi
  and   R   :: 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     PRelQ:    "(P, Q) \<in> Rel"
  and     Par:      "\<And>P Q R. (P, Q) \<in> Rel \<Longrightarrow> (P \<parallel> R, Q \<parallel> R) \<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'"

  shows "P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
note PSimQ
[PROOF STATE]
proof (state)
this:
P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[Rel] Q

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
have RSimR: "R \<leadsto>[Id] R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. R \<leadsto>[Id] R
[PROOF STEP]
by(auto intro: reflexive)
[PROOF STATE]
proof (state)
this:
R \<leadsto>[Id] R

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
R \<leadsto>[Id] R

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
note PRelQ
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
have "(R, R) \<in> Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (R, R) \<in> Id
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(R, R) \<in> Id

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(R, R) \<in> Id

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
from Par
[PROOF STATE]
proof (chain)
picking this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> Rel'
[PROOF STEP]
have "\<And>P Q R T. \<lbrakk>(P, Q) \<in> Rel; (R, T) \<in> Id\<rbrakk> \<Longrightarrow> (P \<parallel> R, Q \<parallel> T) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> Rel'

goal (1 subgoal):
 1. \<And>P Q R T. \<lbrakk>(P, Q) \<in> Rel; (R, T) \<in> Id\<rbrakk> \<Longrightarrow> (P \<parallel> R, Q \<parallel> T) \<in> Rel'
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?P, ?Q) \<in> Rel; (?R, ?T) \<in> Id\<rbrakk> \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?T) \<in> Rel'

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<lbrakk>(?P, ?Q) \<in> Rel; (?R, ?T) \<in> Id\<rbrakk> \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?T) \<in> Rel'

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
note Res \<open>eqvt Rel\<close>
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel' \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel'
eqvt Rel

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel' \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel'
eqvt Rel

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
have "eqvt Id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt Id
[PROOF STEP]
by(auto simp add: eqvt_def)
[PROOF STATE]
proof (state)
this:
eqvt Id

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
R \<leadsto>[Id] R
(P, Q) \<in> Rel
(R, R) \<in> Id
\<lbrakk>(?P, ?Q) \<in> Rel; (?R, ?T) \<in> Id\<rbrakk> \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?T) \<in> Rel'
(?P, ?Q) \<in> Rel' \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel'
eqvt Rel
eqvt Id
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
R \<leadsto>[Id] R
(P, Q) \<in> Rel
(R, R) \<in> Id
\<lbrakk>(?P, ?Q) \<in> Rel; (?R, ?T) \<in> Id\<rbrakk> \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?T) \<in> Rel'
(?P, ?Q) \<in> Rel' \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel'
eqvt Rel
eqvt Id

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[Rel'] Q \<parallel> R
[PROOF STEP]
using EqvtRel'
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
R \<leadsto>[Id] R
(P, Q) \<in> Rel
(R, R) \<in> Id
\<lbrakk>(?P, ?Q) \<in> Rel; (?R, ?T) \<in> Id\<rbrakk> \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?T) \<in> Rel'
(?P, ?Q) \<in> Rel' \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> Rel'
eqvt Rel
eqvt Id
eqvt Rel'

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

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes Der: "derivative P Q a x Rel"
  and     Rel: "\<And>(P::pi) (Q::pi) (x::name). (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> Rel'"
  and     Eqv: "eqvt Rel"

  shows "derivative (<\<nu>y>P) (<\<nu>y>Q) a x Rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. derivative (<\<nu>y>P) (<\<nu>y>Q) a x Rel'
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. derivative (<\<nu>y>P) (<\<nu>y>Q) a x Rel'
[PROOF STEP]
from Der Rel
[PROOF STATE]
proof (chain)
picking this:
derivative P Q a x Rel
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
derivative P Q a x Rel
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel'

goal (1 subgoal):
 1. derivative (<\<nu>y>P) (<\<nu>y>Q) a x Rel'
[PROOF STEP]
proof(cases a, auto simp add: derivative_def)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 u. \<lbrakk>\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel; a = InputS x1; \<And>P Q x. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> Rel'\<rbrakk> \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
fix u
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1 u. \<lbrakk>\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel; a = InputS x1; \<And>P Q x. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> Rel'\<rbrakk> \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
assume A1: "\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel"
[PROOF STATE]
proof (state)
this:
\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel

goal (1 subgoal):
 1. \<And>x1 u. \<lbrakk>\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel; a = InputS x1; \<And>P Q x. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> Rel'\<rbrakk> \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
show "((<\<nu>y>P)[x::=u], (<\<nu>y>Q)[x::=u]) \<in> Rel'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
proof(cases "x=y")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. x = y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. x \<noteq> y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
assume xeqy: "x=y"
[PROOF STATE]
proof (state)
this:
x = y

goal (2 subgoals):
 1. x = y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. x \<noteq> y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel
[PROOF STEP]
have "(P[x::=x], Q[x::=x]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>u. (P[x::=u], Q[x::=u]) \<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 (2 subgoals):
 1. x = y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. x \<noteq> y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
hence L1: "(<\<nu>y>P, <\<nu>y>Q) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(P[x::=x], Q[x::=x]) \<in> Rel

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

goal (2 subgoals):
 1. x = y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. x \<noteq> y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
have "y \<sharp> <\<nu>y>P" and "y \<sharp> <\<nu>y>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<sharp> <\<nu>y>P &&& y \<sharp> <\<nu>y>Q
[PROOF STEP]
by(simp only: freshRes)+
[PROOF STATE]
proof (state)
this:
y \<sharp> <\<nu>y>P
y \<sharp> <\<nu>y>Q

goal (2 subgoals):
 1. x = y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. x \<noteq> y \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
hence "(<\<nu>y>P)[y::=u] = <\<nu>y>P" and "(<\<nu>y>Q)[y::=u] = <\<nu>y>Q"
[PROOF STATE]
proof (prove)
using this:
y \<sharp> <\<nu>y>P
y \<sharp> <\<nu>y>Q

goal (1 subgoal):
 1. <\<nu>y>P[y::=u] = <\<nu>y>P &&& <\<nu>y>Q[y::=u] = <\<nu>y>Q
[PROOF STEP]
by(simp add: forget)+
[PROOF STATE]
proof (state)
this:
<\<nu>y>P[y::=u] = <\<nu>y>P
<\<nu>y>Q[y::=u] = <\<nu>y>Q

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

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

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

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

goal (2 subgoals):
 1. y = u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
have "\<exists>(c::name). c \<sharp> (P, Q, x, y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>c. c \<sharp> (P, Q, x, y)
[PROOF STEP]
by(blast intro: name_exists_fresh)
[PROOF STATE]
proof (state)
this:
\<exists>c. c \<sharp> (P, Q, x, y)

goal (2 subgoals):
 1. y = u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>c. c \<sharp> (P, Q, x, y)
[PROOF STEP]
obtain c where cFreshP: "c \<sharp> P" and cFreshQ: "c \<sharp> Q" and cineqx: "c \<noteq> x" and cineqy: "y \<noteq> c"
[PROOF STATE]
proof (prove)
using this:
\<exists>c. c \<sharp> (P, Q, x, y)

goal (1 subgoal):
 1. (\<And>c. \<lbrakk>c \<sharp> P; c \<sharp> Q; c \<noteq> x; y \<noteq> c\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(force simp add: fresh_prod name_fresh)
[PROOF STATE]
proof (state)
this:
c \<sharp> P
c \<sharp> Q
c \<noteq> x
y \<noteq> c

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

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

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

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

goal (2 subgoals):
 1. y = u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
with xineqy cineqx cineqy
[PROOF STATE]
proof (chain)
picking this:
x \<noteq> y
c \<noteq> x
y \<noteq> c
([(y, c)] \<bullet> P[x::=c], [(y, c)] \<bullet> Q[x::=c]) \<in> Rel
[PROOF STEP]
have "(([(y, c)] \<bullet> P)[x::=y], ([(y, c)] \<bullet> Q)[x::=y]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
x \<noteq> y
c \<noteq> x
y \<noteq> c
([(y, c)] \<bullet> P[x::=c], [(y, c)] \<bullet> Q[x::=c]) \<in> Rel

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

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

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

goal (2 subgoals):
 1. y = u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
with cineqx cineqy
[PROOF STATE]
proof (chain)
picking this:
c \<noteq> x
y \<noteq> c
(<\<nu>c>([(y, c)] \<bullet> P)[x::=y], <\<nu>c>([(y, c)] \<bullet> Q)[x::=y]) \<in> Rel'
[PROOF STEP]
have "((<\<nu>c>(([(y, c)] \<bullet> P)))[x::=y], (<\<nu>c>(([(y, c)] \<bullet> Q)))[x::=y])\<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
c \<noteq> x
y \<noteq> c
(<\<nu>c>([(y, c)] \<bullet> P)[x::=y], <\<nu>c>([(y, c)] \<bullet> Q)[x::=y]) \<in> Rel'

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

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

goal (2 subgoals):
 1. y = u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
 2. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
from cFreshP cFreshQ
[PROOF STATE]
proof (chain)
picking this:
c \<sharp> P
c \<sharp> Q
[PROOF STEP]
have "<\<nu>c>([(y, c)] \<bullet> P) = <\<nu>y>P" and "<\<nu>c>([(y, c)] \<bullet> Q) = <\<nu>y>Q"
[PROOF STATE]
proof (prove)
using this:
c \<sharp> P
c \<sharp> Q

goal (1 subgoal):
 1. <\<nu>c>([(y, c)] \<bullet> P) = <\<nu>y>P &&& <\<nu>c>([(y, c)] \<bullet> Q) = <\<nu>y>Q
[PROOF STEP]
by(simp add: alphaRes)+
[PROOF STATE]
proof (state)
this:
<\<nu>c>([(y, c)] \<bullet> P) = <\<nu>y>P
<\<nu>c>([(y, c)] \<bullet> Q) = <\<nu>y>Q

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

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

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

goal (1 subgoal):
 1. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=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> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
from A1
[PROOF STATE]
proof (chain)
picking this:
\<forall>u. (P[x::=u], Q[x::=u]) \<in> Rel
[PROOF STEP]
have "(P[x::=u], Q[x::=u]) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<forall>u. (P[x::=u], Q[x::=u]) \<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. y \<noteq> u \<Longrightarrow> (<\<nu>y>P[x::=u], <\<nu>y>Q[x::=u]) \<in> Rel'
[PROOF STEP]
hence "(<\<nu>y>(P[x::=u]), <\<nu>y>(Q[x::=u])) \<in> Rel'"
[PROOF STATE]
proof (prove)
using this:
(P[x::=u], Q[x::=u]) \<in> Rel

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes PSimQ: "P \<leadsto>[Rel] Q"
  and     ResRel: "\<And>(P::pi) (Q::pi) (x::name). (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> Rel'"
  and     RelRel': "Rel \<subseteq> Rel'"
  and     EqvtRel: "eqvt Rel"
  and     EqvtRel': "eqvt Rel'"

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

goal (1 subgoal):
 1. <\<nu>x>P \<leadsto>[Rel'] <\<nu>x>Q
[PROOF STEP]
proof(induct rule: resSimCases[of _ _ _ _ "(P, x)"])
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>Q' a. \<lbrakk>Q \<longmapsto> a[x] \<prec> Q'; a \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a<\<nu>x> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>Q' a y. \<lbrakk>Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; x \<sharp> a; x \<noteq> y; y \<sharp> (P, x)\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' (<\<nu>x>Q') a y Rel'
 3. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
case(BoundOutput Q' a)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a[x] \<prec> Q'
a \<noteq> x

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

goal (3 subgoals):
 1. \<And>Q' a. \<lbrakk>Q \<longmapsto> a[x] \<prec> Q'; a \<noteq> x\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a<\<nu>x> \<prec> P' \<and> (P', Q') \<in> Rel'
 2. \<And>Q' a y. \<lbrakk>Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; x \<sharp> a; x \<noteq> y; y \<sharp> (P, x)\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' (<\<nu>x>Q') a y Rel'
 3. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
from PSimQ QTrans
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a[x] \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> a[x] \<prec> P'"
                                and P'RelQ': "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
Q \<longmapsto> a[x] \<prec> Q'

goal (1 subgoal):
 1. (\<And>P'. \<lbrakk>P \<longmapsto> a[x] \<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[x] \<prec> P'
(P', Q') \<in> Rel

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

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

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

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

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

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

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

goal (2 subgoals):
 1. \<And>Q' a y. \<lbrakk>Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; x \<sharp> a; x \<noteq> y; y \<sharp> (P, x)\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' (<\<nu>x>Q') a y Rel'
 2. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>Q' a y. \<lbrakk>Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; x \<sharp> a; x \<noteq> y; y \<sharp> (P, x)\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' (<\<nu>x>Q') a y Rel'
 2. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
case(BoundR Q' a y)
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'
x \<sharp> a
x \<noteq> y
y \<sharp> (P, x)

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

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

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

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

goal (2 subgoals):
 1. \<And>Q' a y. \<lbrakk>Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'; x \<sharp> a; x \<noteq> y; y \<sharp> (P, x)\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> P' \<and> derivative P' (<\<nu>x>Q') a y Rel'
 2. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
from PSimQ yFreshP QTrans
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
y \<sharp> P
Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto>a\<guillemotleft>y\<guillemotright> \<prec> P'"
                                         and Pderivative: "derivative P' Q' a y Rel"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q
y \<sharp> P
Q \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> Q'

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

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

goal (1 subgoal):
 1. <\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> <\<nu>x>P'
[PROOF STEP]
by(blast intro: Late_Semantics.ResB)
[PROOF STATE]
proof (state)
this:
<\<nu>x>P \<longmapsto> a\<guillemotleft>y\<guillemotright> \<prec> <\<nu>x>P'

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

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

goal (1 subgoal):
 1. derivative (<\<nu>x>P') (<\<nu>x>Q') a y Rel'
[PROOF STEP]
by(rule resDerivative)
[PROOF STATE]
proof (state)
this:
derivative (<\<nu>x>P') (<\<nu>x>Q') a y Rel'

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

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

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

goal (1 subgoal):
 1. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
have QTrans: "Q \<longmapsto> \<alpha> \<prec> Q'" and xFreshAlpha: "(x::name) \<sharp> \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Q \<longmapsto> \<alpha> \<prec> Q' &&& x \<sharp> \<alpha>
[PROOF STEP]
by fact+
[PROOF STATE]
proof (state)
this:
Q \<longmapsto> \<alpha> \<prec> Q'
x \<sharp> \<alpha>

goal (1 subgoal):
 1. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
from QTrans PSimQ
[PROOF STATE]
proof (chain)
picking this:
Q \<longmapsto> \<alpha> \<prec> Q'
P \<leadsto>[Rel] Q
[PROOF STEP]
obtain P' where PTrans: "P \<longmapsto> \<alpha> \<prec> P'"
                                and P'RelQ': "(P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
Q \<longmapsto> \<alpha> \<prec> Q'
P \<leadsto>[Rel] 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. \<And>Q' \<alpha>. \<lbrakk>Q \<longmapsto> \<alpha> \<prec> Q'; x \<sharp> \<alpha>\<rbrakk> \<Longrightarrow> \<exists>P'. <\<nu>x>P \<longmapsto> \<alpha> \<prec> P' \<and> (P', <\<nu>x>Q') \<in> Rel'
[PROOF STEP]
from PTrans xFreshAlpha
[PROOF STATE]
proof (chain)
picking this:
P \<longmapsto> \<alpha> \<prec> P'
x \<sharp> \<alpha>
[PROOF STEP]
have "<\<nu>x>P \<longmapsto>\<alpha> \<prec> <\<nu>x>P'"
[PROOF STATE]
proof (prove)
using this:
P \<longmapsto> \<alpha> \<prec> P'
x \<sharp> \<alpha>

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

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

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

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resChainI:
  fixes P   :: pi
  and   Q   :: pi
  and   Rel :: "(pi \<times> pi) set"
  and   xs  :: "name list"

  assumes PRelQ:   "P \<leadsto>[Rel] Q"
  and     eqvtRel: "eqvt Rel"
  and     Res:     "\<And>P Q x. (P, Q) \<in> Rel \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> Rel"

  shows "(resChain xs) P \<leadsto>[Rel] (resChain xs) Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. resChain xs P \<leadsto>[Rel] resChain xs Q
[PROOF STEP]
proof(induct xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto>[Rel] resChain [] Q
 2. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
(* Base case *)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. resChain [] P \<leadsto>[Rel] resChain [] Q
 2. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
from PRelQ
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[Rel] Q
[PROOF STEP]
show "resChain [] P \<leadsto>[Rel] resChain [] Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[Rel] Q

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

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
(* Inductive step *)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
fix x xs
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
assume IH: "(resChain xs P) \<leadsto>[Rel] (resChain xs Q)"
[PROOF STATE]
proof (state)
this:
resChain xs P \<leadsto>[Rel] resChain xs Q

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
resChain xs P \<leadsto>[Rel] resChain xs Q

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
note Res
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
have "Rel \<subseteq> Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rel \<subseteq> Rel
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Rel \<subseteq> Rel

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
resChain xs P \<leadsto>[Rel] resChain xs Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel
Rel \<subseteq> Rel
[PROOF STEP]
have "<\<nu>x>(resChain xs P) \<leadsto>[Rel] <\<nu>x>(resChain xs Q)"
[PROOF STATE]
proof (prove)
using this:
resChain xs P \<leadsto>[Rel] resChain xs Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel
Rel \<subseteq> Rel

goal (1 subgoal):
 1. <\<nu>x>resChain xs P \<leadsto>[Rel] <\<nu>x>resChain xs Q
[PROOF STEP]
using eqvtRel
[PROOF STATE]
proof (prove)
using this:
resChain xs P \<leadsto>[Rel] resChain xs Q
(?P, ?Q) \<in> Rel \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> Rel
Rel \<subseteq> Rel
eqvt Rel

goal (1 subgoal):
 1. <\<nu>x>resChain xs P \<leadsto>[Rel] <\<nu>x>resChain xs Q
[PROOF STEP]
by(rule_tac resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>x>resChain xs P \<leadsto>[Rel] <\<nu>x>resChain xs Q

goal (1 subgoal):
 1. \<And>a xs. resChain xs P \<leadsto>[Rel] resChain xs Q \<Longrightarrow> resChain (a # xs) P \<leadsto>[Rel] resChain (a # xs) Q
[PROOF STEP]
thus "resChain (x # xs) P \<leadsto>[Rel] resChain (x # xs) Q"
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>resChain xs P \<leadsto>[Rel] <\<nu>x>resChain xs Q

goal (1 subgoal):
 1. resChain (x # xs) P \<leadsto>[Rel] resChain (x # xs) Q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
resChain (x # xs) P \<leadsto>[Rel] resChain (x # xs) Q

goal:
No subgoals!
[PROOF STEP]
qed