[STATEMENT]
lemma simps: "fun x = (if Q x then g x else h' (fun (h x)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
proof (cases "dom x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
 2. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
local.dom x

goal (2 subgoals):
 1. local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
 2. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
hence dom: "recfun_aux_dom x"
[PROOF STATE]
proof (prove)
using this:
local.dom x

goal (1 subgoal):
 1. recfun_aux_dom x
[PROOF STEP]
by (rule recfun_aux_domI)
[PROOF STATE]
proof (state)
this:
recfun_aux_dom x

goal (2 subgoals):
 1. local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
 2. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
proof (cases "Q x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
 2. \<not> Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Q x

goal (2 subgoals):
 1. Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
 2. \<not> Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
with dom
[PROOF STATE]
proof (chain)
picking this:
recfun_aux_dom x
Q x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
recfun_aux_dom x
Q x

goal (1 subgoal):
 1. fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
by (simp add: fun_def recfun_aux.psimps)
[PROOF STATE]
proof (state)
this:
fun x = (if Q x then g x else h' (fun (h x)))

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> Q x

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
have "recfun_aux_dom (h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. recfun_aux_dom (h x)
[PROOF STEP]
by (rule recfun_aux_domI, rule domD, fact True, fact False)
[PROOF STATE]
proof (state)
this:
recfun_aux_dom (h x)

goal (1 subgoal):
 1. \<not> Q x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
recfun_aux_dom (h x)

goal (1 subgoal):
 1. fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
by (simp add: fun_def dom False recfun_aux.psimps)
[PROOF STATE]
proof (state)
this:
fun x = (if Q x then g x else h' (fun (h x)))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fun x = (if Q x then g x else h' (fun (h x)))

goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> local.dom x

goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> local.dom x

goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
have "\<not> Q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> Q x
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Q x \<Longrightarrow> False
[PROOF STEP]
assume "Q x"
[PROOF STATE]
proof (state)
this:
Q x

goal (1 subgoal):
 1. Q x \<Longrightarrow> False
[PROOF STEP]
hence "dom x"
[PROOF STATE]
proof (prove)
using this:
Q x

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
using domI
[PROOF STATE]
proof (prove)
using this:
Q x
(\<not> Q ?x \<Longrightarrow> local.dom (h ?x)) \<Longrightarrow> local.dom ?x

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

goal (1 subgoal):
 1. Q x \<Longrightarrow> False
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> local.dom x
local.dom x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> local.dom x
local.dom x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> Q x

goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> Q x

goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
have "\<not> dom (h x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> local.dom (h x)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.dom (h x) \<Longrightarrow> False
[PROOF STEP]
assume "dom (h x)"
[PROOF STATE]
proof (state)
this:
local.dom (h x)

goal (1 subgoal):
 1. local.dom (h x) \<Longrightarrow> False
[PROOF STEP]
hence "dom x"
[PROOF STATE]
proof (prove)
using this:
local.dom (h x)

goal (1 subgoal):
 1. local.dom x
[PROOF STEP]
using domI
[PROOF STATE]
proof (prove)
using this:
local.dom (h x)
(\<not> Q ?x \<Longrightarrow> local.dom (h ?x)) \<Longrightarrow> local.dom ?x

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

goal (1 subgoal):
 1. local.dom (h x) \<Longrightarrow> False
[PROOF STEP]
with False
[PROOF STATE]
proof (chain)
picking this:
\<not> local.dom x
local.dom x
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
\<not> local.dom x
local.dom x

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<not> local.dom (h x)

goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> local.dom x
\<not> Q x
\<not> local.dom (h x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> local.dom x
\<not> Q x
\<not> local.dom (h x)

goal (1 subgoal):
 1. fun x = (if Q x then g x else h' (fun (h x)))
[PROOF STEP]
by (simp add: recfun_aux_dom_alt fun_def b_fixpoint split del: if_split)
[PROOF STATE]
proof (state)
this:
fun x = (if Q x then g x else h' (fun (h x)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma eq_fixpointI: "\<not> dom x \<Longrightarrow> fun x = b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> local.dom x \<Longrightarrow> fun x = b
[PROOF STEP]
by (simp add: fun_def recfun_aux_dom_alt)


[STATEMENT]
lemma pinduct: "dom x \<Longrightarrow> (\<And>x. dom x \<Longrightarrow> (\<not> Q x \<Longrightarrow> P (h x)) \<Longrightarrow> P x) \<Longrightarrow> P x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>local.dom x; \<And>x. \<lbrakk>local.dom x; \<not> Q x \<Longrightarrow> P (h x)\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
unfolding recfun_aux_dom_alt[symmetric]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>recfun_aux_dom x; \<And>x. \<lbrakk>recfun_aux_dom x; \<not> Q x \<Longrightarrow> P (h x)\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> P x
[PROOF STEP]
by (fact recfun_aux.pinduct)


[STATEMENT]
lemma almost_full_on_Int:
  assumes "almost_full_on P1 A1" and "almost_full_on P2 A2"
  shows "almost_full_on (\<lambda>x y. P1 x y \<and> P2 x y) (A1 \<inter> A2)" (is "almost_full_on ?P ?A")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. almost_full_on (\<lambda>x y. P1 x y \<and> P2 x y) (A1 \<inter> A2)
[PROOF STEP]
proof (rule almost_full_onI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
fix f :: "nat \<Rightarrow> 'a"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
assume a: "\<forall>i. f i \<in> ?A"
[PROOF STATE]
proof (state)
this:
\<forall>i. f i \<in> A1 \<inter> A2

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
define g where "g = (\<lambda>i. (f i, f i))"
[PROOF STATE]
proof (state)
this:
g = (\<lambda>i. (f i, f i))

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
almost_full_on P1 A1
almost_full_on P2 A2
[PROOF STEP]
have "almost_full_on (prod_le P1 P2) (A1 \<times> A2)"
[PROOF STATE]
proof (prove)
using this:
almost_full_on P1 A1
almost_full_on P2 A2

goal (1 subgoal):
 1. almost_full_on (prod_le P1 P2) (A1 \<times> A2)
[PROOF STEP]
by (rule almost_full_on_Sigma)
[PROOF STATE]
proof (state)
this:
almost_full_on (prod_le P1 P2) (A1 \<times> A2)

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
almost_full_on (prod_le P1 P2) (A1 \<times> A2)

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
from a
[PROOF STATE]
proof (chain)
picking this:
\<forall>i. f i \<in> A1 \<inter> A2
[PROOF STEP]
have "\<And>i. g i \<in> A1 \<times> A2"
[PROOF STATE]
proof (prove)
using this:
\<forall>i. f i \<in> A1 \<inter> A2

goal (1 subgoal):
 1. \<And>i. g i \<in> A1 \<times> A2
[PROOF STEP]
by (simp add: g_def)
[PROOF STATE]
proof (state)
this:
g ?i \<in> A1 \<times> A2

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
almost_full_on (prod_le P1 P2) (A1 \<times> A2)
g ?i \<in> A1 \<times> A2
[PROOF STEP]
obtain i j where "i < j" and "prod_le P1 P2 (g i) (g j)"
[PROOF STATE]
proof (prove)
using this:
almost_full_on (prod_le P1 P2) (A1 \<times> A2)
g ?i \<in> A1 \<times> A2

goal (1 subgoal):
 1. (\<And>i j. \<lbrakk>i < j; prod_le P1 P2 (g i) (g j)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule almost_full_onD)
[PROOF STATE]
proof (state)
this:
i < j
prod_le P1 P2 (g i) (g j)

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
from this(2)
[PROOF STATE]
proof (chain)
picking this:
prod_le P1 P2 (g i) (g j)
[PROOF STEP]
have "?P (f i) (f j)"
[PROOF STATE]
proof (prove)
using this:
prod_le P1 P2 (g i) (g j)

goal (1 subgoal):
 1. P1 (f i) (f j) \<and> P2 (f i) (f j)
[PROOF STEP]
by (simp add: g_def prod_le_def)
[PROOF STATE]
proof (state)
this:
P1 (f i) (f j) \<and> P2 (f i) (f j)

goal (1 subgoal):
 1. \<And>f. \<forall>i. f i \<in> A1 \<inter> A2 \<Longrightarrow> good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
with \<open>i < j\<close>
[PROOF STATE]
proof (chain)
picking this:
i < j
P1 (f i) (f j) \<and> P2 (f i) (f j)
[PROOF STEP]
show "good ?P f"
[PROOF STATE]
proof (prove)
using this:
i < j
P1 (f i) (f j) \<and> P2 (f i) (f j)

goal (1 subgoal):
 1. good (\<lambda>x y. P1 x y \<and> P2 x y) f
[PROOF STEP]
by (rule goodI)
[PROOF STATE]
proof (state)
this:
good (\<lambda>x y. P1 x y \<and> P2 x y) f

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma is_le_relI [simp]: "is_le_rel (=)" "is_le_rel (\<le>)" "is_le_rel (<)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_le_rel (=) &&& is_le_rel (\<le>) &&& is_le_rel (<)
[PROOF STEP]
by (simp_all add: is_le_rel_def)


[STATEMENT]
lemma is_le_relE:
  assumes "is_le_rel rel"
  obtains "rel = (=)" | "rel = (\<le>)" | "rel = (<)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel = (=) \<Longrightarrow> thesis; rel = (\<le>) \<Longrightarrow> thesis; rel = (<) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>rel = (=) \<Longrightarrow> thesis; rel = (\<le>) \<Longrightarrow> thesis; rel = (<) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
unfolding is_le_rel_def
[PROOF STATE]
proof (prove)
using this:
rel = (=) \<or> rel = (\<le>) \<or> rel = (<)

goal (1 subgoal):
 1. \<lbrakk>rel = (=) \<Longrightarrow> thesis; rel = (\<le>) \<Longrightarrow> thesis; rel = (<) \<Longrightarrow> thesis\<rbrakk> \<Longrightarrow> thesis
[PROOF STEP]
by blast


[STATEMENT]
lemma is_le_rel_le:
  assumes "is_le_rel rel"
  shows "rel x y \<Longrightarrow> x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel x y \<Longrightarrow> x \<le> y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. rel x y \<Longrightarrow> x \<le> y
[PROOF STEP]
by (rule is_le_relE, auto dest: less_imp_le)


[STATEMENT]
lemma is_le_rel_trans:
  assumes "is_le_rel rel"
  shows "rel x y \<Longrightarrow> rel y z \<Longrightarrow> rel x z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel x y; rel y z\<rbrakk> \<Longrightarrow> rel x z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>rel x y; rel y z\<rbrakk> \<Longrightarrow> rel x z
[PROOF STEP]
by (rule is_le_relE, auto dest: order_trans less_trans)


[STATEMENT]
lemma is_le_rel_trans_le_left:
  assumes "is_le_rel rel"
  shows "x \<le> y \<Longrightarrow> rel y z \<Longrightarrow> x \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<le> y; rel y z\<rbrakk> \<Longrightarrow> x \<le> z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>x \<le> y; rel y z\<rbrakk> \<Longrightarrow> x \<le> z
[PROOF STEP]
by (rule is_le_relE, auto dest: order_trans le_less_trans less_imp_le)


[STATEMENT]
lemma is_le_rel_trans_le_right:
  assumes "is_le_rel rel"
  shows "rel x y \<Longrightarrow> y \<le> z \<Longrightarrow> x \<le> z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel x y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>rel x y; y \<le> z\<rbrakk> \<Longrightarrow> x \<le> z
[PROOF STEP]
by (rule is_le_relE, auto dest: order_trans less_le_trans less_imp_le)


[STATEMENT]
lemma is_le_rel_trans_less_left:
  assumes "is_le_rel rel"
  shows "x < y \<Longrightarrow> rel y z \<Longrightarrow> x < z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < y; rel y z\<rbrakk> \<Longrightarrow> x < z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>x < y; rel y z\<rbrakk> \<Longrightarrow> x < z
[PROOF STEP]
by (rule is_le_relE, auto dest: less_le_trans less_imp_le)


[STATEMENT]
lemma is_le_rel_trans_less_right:
  assumes "is_le_rel rel"
  shows "rel x y \<Longrightarrow> y < z \<Longrightarrow> x < z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel x y; y < z\<rbrakk> \<Longrightarrow> x < z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>rel x y; y < z\<rbrakk> \<Longrightarrow> x < z
[PROOF STEP]
by (rule is_le_relE, auto dest: le_less_trans less_imp_le)


[STATEMENT]
lemma is_le_rel_distinct:
  assumes "is_le_rel rel"
  shows "rel x y \<Longrightarrow> x \<noteq> y \<Longrightarrow> x < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel x y; x \<noteq> y\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>rel x y; x \<noteq> y\<rbrakk> \<Longrightarrow> x < y
[PROOF STEP]
by (rule is_le_relE, auto)


[STATEMENT]
lemma is_le_rel_antisym:
  assumes "is_le_rel rel"
  shows "rel x y \<Longrightarrow> rel y x \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rel x y; rel y x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_le_rel rel

goal (1 subgoal):
 1. \<lbrakk>rel x y; rel y x\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (rule is_le_relE, auto)


[STATEMENT]
lemma weakSimI[consumes 1, case_names cAct cTau]:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   C   :: "'d::fs_name"

  assumes Eqvt: "eqvt Rel"
  and     rAct: "\<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q';  bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; bn \<alpha> \<sharp>* Q;
                              bn \<alpha> \<sharp>* subject \<alpha>; bn \<alpha> \<sharp>* C; distinct(bn \<alpha>); \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow>

                              \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)"
  and     rTau:  "\<And>Q'. \<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel"

  shows "\<Psi> \<rhd> P \<leadsto><Rel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
proof(auto simp add: weakSimulation_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
fix \<Psi>' \<alpha> Q'
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'; bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>Q'. \<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel
[PROOF STEP]
assume "\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q'" and "bn \<alpha> \<sharp>* \<Psi>" and "bn \<alpha> \<sharp>* P" and "\<alpha> \<noteq> \<tau>"
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<alpha> \<prec> Q'
bn \<alpha> \<sharp>* \<Psi>
bn \<alpha> \<sharp>* P
\<alpha> \<noteq> \<tau>

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

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
proof(nominal_induct \<alpha> rule: action.strong_induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a1 a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>a2\<rparr> \<prec> Q'; bn (a1\<lparr>a2\<rparr>) \<sharp>* \<Psi>; bn (a1\<lparr>a2\<rparr>) \<sharp>* P; a1\<lparr>a2\<rparr> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>a2\<rparr> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 3. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
case(In M N)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>N\<rparr> \<prec> Q'
bn (M\<lparr>N\<rparr>) \<sharp>* \<Psi>
bn (M\<lparr>N\<rparr>) \<sharp>* P
M\<lparr>N\<rparr> \<noteq> \<tau>

goal (3 subgoals):
 1. \<And>a1 a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>a2\<rparr> \<prec> Q'; bn (a1\<lparr>a2\<rparr>) \<sharp>* \<Psi>; bn (a1\<lparr>a2\<rparr>) \<sharp>* P; a1\<lparr>a2\<rparr> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>a2\<rparr> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 3. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>N\<rparr> \<prec> Q'
bn (M\<lparr>N\<rparr>) \<sharp>* \<Psi>
bn (M\<lparr>N\<rparr>) \<sharp>* P
M\<lparr>N\<rparr> \<noteq> \<tau>

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
by(rule_tac rAct) auto
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>N\<rparr> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
case(Out M xvec N)
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
bn (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* \<Psi>
bn (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* P
M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<noteq> \<tau>

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>bn(M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* \<Psi>\<close> \<open>bn(M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* P\<close>
[PROOF STATE]
proof (chain)
picking this:
bn (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* \<Psi>
bn (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* P
[PROOF STEP]
have "xvec \<sharp>* \<Psi>" and "xvec \<sharp>* P"
[PROOF STATE]
proof (prove)
using this:
bn (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* \<Psi>
bn (M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle>) \<sharp>* P

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
[PROOF STEP]
have "distinct xvec"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'

goal (1 subgoal):
 1. distinct xvec
[PROOF STEP]
by(force dest: boundOutputDistinct)
[PROOF STATE]
proof (state)
this:
distinct xvec

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
obtain p where "(p \<bullet> xvec) \<sharp>* \<Psi>" and "(p \<bullet> xvec) \<sharp>* M" and "(p \<bullet> xvec) \<sharp>* xvec"
               and"(p \<bullet> xvec) \<sharp>* P" and "(p \<bullet> xvec) \<sharp>* Q" and "(p \<bullet> xvec) \<sharp>* Q'" and "(p \<bullet> xvec) \<sharp>* \<Psi>'"
               and "(p \<bullet> xvec) \<sharp>* C" and "(p \<bullet> xvec) \<sharp>* xvec" and "(p \<bullet> xvec) \<sharp>* N"
               and S: "(set p) \<subseteq> (set xvec) \<times> (set(p \<bullet> xvec))" and "distinctPerm p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>p. \<lbrakk>(p \<bullet> xvec) \<sharp>* \<Psi>; (p \<bullet> xvec) \<sharp>* M; (p \<bullet> xvec) \<sharp>* xvec; (p \<bullet> xvec) \<sharp>* P; (p \<bullet> xvec) \<sharp>* Q; (p \<bullet> xvec) \<sharp>* Q'; (p \<bullet> xvec) \<sharp>* \<Psi>'; (p \<bullet> xvec) \<sharp>* C; (p \<bullet> xvec) \<sharp>* xvec; (p \<bullet> xvec) \<sharp>* N; set p \<subseteq> set xvec \<times> set (p \<bullet> xvec); distinctPerm p\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(rule_tac xvec=xvec and c="(\<Psi>, M, Q, N, P, Q', xvec, C, \<Psi>')" in name_list_avoiding)
        (auto simp add: eqvts fresh_star_prod)
[PROOF STATE]
proof (state)
this:
(p \<bullet> xvec) \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* M
(p \<bullet> xvec) \<sharp>* xvec
(p \<bullet> xvec) \<sharp>* P
(p \<bullet> xvec) \<sharp>* Q
(p \<bullet> xvec) \<sharp>* Q'
(p \<bullet> xvec) \<sharp>* \<Psi>'
(p \<bullet> xvec) \<sharp>* C
(p \<bullet> xvec) \<sharp>* xvec
(p \<bullet> xvec) \<sharp>* N
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p

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

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from \<open>\<Psi> \<rhd> Q \<longmapsto>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'\<close> \<open>(p \<bullet> xvec) \<sharp>* N\<close> \<open>(p \<bullet> xvec) \<sharp>* Q'\<close> S
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* Q'
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
[PROOF STEP]
have "\<Psi> \<rhd> Q \<longmapsto>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> (p \<bullet> Q')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> Q'
(p \<bullet> xvec) \<sharp>* N
(p \<bullet> xvec) \<sharp>* Q'
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> p \<bullet> Q'
[PROOF STEP]
obtain P'' P' where PTrans: "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P''"
                         and P''Chain: "\<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'"
                         and P'RelQ': "(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> p \<bullet> Q'

goal (1 subgoal):
 1. (\<And>P'' P'. \<lbrakk>\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P''; \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P'; (\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* Q\<close> \<open>(p \<bullet> xvec) \<sharp>* M\<close> \<open>(p \<bullet> xvec) \<sharp>* C\<close> \<open>distinct(p \<bullet> xvec)\<close>
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> p \<bullet> Q'
(p \<bullet> xvec) \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* P
(p \<bullet> xvec) \<sharp>* Q
(p \<bullet> xvec) \<sharp>* M
(p \<bullet> xvec) \<sharp>* C
distinct (p \<bullet> xvec)

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from PTrans S \<open>distinctPerm p\<close> \<open>xvec \<sharp>* P\<close> \<open>(p \<bullet> xvec) \<sharp>* xvec\<close> \<open>(p \<bullet> xvec) \<sharp>* M\<close> \<open>distinct xvec\<close>
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P''
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
xvec \<sharp>* P
(p \<bullet> xvec) \<sharp>* xvec
(p \<bullet> xvec) \<sharp>* M
distinct xvec
[PROOF STEP]
have "\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> (p \<bullet> P'')"
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*(p \<bullet> xvec)\<rparr>\<langle>(p \<bullet> N)\<rangle> \<prec> P''
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
xvec \<sharp>* P
(p \<bullet> xvec) \<sharp>* xvec
(p \<bullet> xvec) \<sharp>* M
distinct xvec

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''

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

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>'\<close> S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
xvec \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* \<Psi>'
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
[PROOF STEP]
have "\<Psi> \<otimes> \<Psi>' \<rhd> (p \<bullet> P'') \<Longrightarrow>\<^sup>^\<^sub>\<tau> (p \<bullet> P')"
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* \<Psi>'
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>') \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'

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

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
from P'RelQ' Eqvt S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel
eqvt Rel
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
[PROOF STEP]
have "(p \<bullet> (\<Psi> \<otimes> (p \<bullet> \<Psi>')), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(\<Psi> \<otimes> (p \<bullet> \<Psi>'), P', p \<bullet> Q') \<in> Rel
eqvt Rel
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
with \<open>xvec \<sharp>* \<Psi>\<close> \<open>(p \<bullet> xvec) \<sharp>* \<Psi>\<close> S \<open>distinctPerm p\<close>
[PROOF STATE]
proof (chain)
picking this:
xvec \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* \<Psi>
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
(p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel
[PROOF STEP]
have "(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
xvec \<sharp>* \<Psi>
(p \<bullet> xvec) \<sharp>* \<Psi>
set p \<subseteq> set xvec \<times> set (p \<bullet> xvec)
distinctPerm p
(p \<bullet> \<Psi> \<otimes> (p \<bullet> \<Psi>'), p \<bullet> P', p \<bullet> p \<bullet> Q') \<in> Rel

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

goal (2 subgoals):
 1. \<And>a1 list a2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> Q'; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* \<Psi>; bn (a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle>) \<sharp>* P; a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>a1\<lparr>\<nu>*list\<rparr>\<langle>a2\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
 2. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> p \<bullet> P''
\<Psi> \<otimes> \<Psi>' \<rhd> p \<bullet> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> p \<bullet> P'
(\<Psi> \<otimes> \<Psi>', p \<bullet> P', Q') \<in> Rel

goal (1 subgoal):
 1. \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>M\<lparr>\<nu>*xvec\<rparr>\<langle>N\<rangle> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)

goal (1 subgoal):
 1. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
case Tau
[PROOF STATE]
proof (state)
this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
bn (\<tau>) \<sharp>* \<Psi>
bn (\<tau>) \<sharp>* P
\<tau> \<noteq> \<tau>

goal (1 subgoal):
 1. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'; bn (\<tau>) \<sharp>* \<Psi>; bn (\<tau>) \<sharp>* P; \<tau> \<noteq> \<tau>\<rbrakk> \<Longrightarrow> \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<tau> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<Psi> \<rhd> Q \<longmapsto> \<tau> \<prec> Q'
bn (\<tau>) \<sharp>* \<Psi>
bn (\<tau>) \<sharp>* P
\<tau> \<noteq> \<tau>

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)

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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma weakSimI2[case_names cAct cTau]:
  fixes \<Psi>   :: 'b
  and   P   :: "('a, 'b, 'c) psi"
  and   Rel :: "('b \<times> ('a, 'b, 'c) psi \<times> ('a, 'b, 'c) psi) set"
  and   Q   :: "('a, 'b, 'c) psi"
  and   C   :: "'d::fs_name"

  assumes rOutput: "\<And>\<Psi>' \<alpha> Q'. \<lbrakk>\<Psi> \<rhd> Q \<longmapsto>\<alpha> \<prec> Q';  bn \<alpha> \<sharp>* \<Psi>; bn \<alpha> \<sharp>* P; \<alpha> \<noteq> \<tau>\<rbrakk> \<Longrightarrow>
                                \<exists>P''. \<Psi> : Q \<rhd> P \<Longrightarrow>\<alpha> \<prec> P'' \<and> (\<exists>P'. \<Psi> \<otimes> \<Psi>' \<rhd> P'' \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi> \<otimes> \<Psi>', P', Q') \<in> Rel)"
  and     rTau:  "\<And>Q'. \<Psi> \<rhd> Q \<longmapsto>\<tau> \<prec> Q' \<Longrightarrow> \<exists>P'. \<Psi> \<rhd> P \<Longrightarrow>\<^sup>^\<^sub>\<tau> P' \<and> (\<Psi>, P', Q') \<in> Rel"

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

goal (1 subgoal):
 1. \<Psi> \<rhd> P \<leadsto><Rel> Q
[PROOF STEP]
by(simp add: weakSimulation_def)