[STATEMENT]
lemma vcons_in_vcpowerE2:
  assumes "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> n" and "n \<in>\<^sub>\<circ> \<omega>" and "0 \<in>\<^sub>\<circ> n"
  obtains x xs' where "xs = xs' #\<^sub>\<circ> x"
    and "xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'"
    and "x \<in>\<^sub>\<circ> A"
    and "n = vcard (xs' #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
n \<in>\<^sub>\<circ> \<omega>

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
n \<in>\<^sub>\<circ> \<omega>
[]\<^sub>\<circ> \<in>\<^sub>\<circ> n
[PROOF STEP]
obtain x xs' where xs_def: "xs = xs' #\<^sub>\<circ> x"
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> n
n \<in>\<^sub>\<circ> \<omega>
[]\<^sub>\<circ> \<in>\<^sub>\<circ> n

goal (1 subgoal):
 1. (\<And>xs' x. xs = xs' #\<^sub>\<circ> x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by
      (
        metis
          eq0_iff vcard_0 vcpower_vdomain vfsequence_vcons_ex vfsequence_vdomain
      )
[PROOF STATE]
proof (state)
this:
xs = xs' #\<^sub>\<circ> x

goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vcons_in_vcpowerE1[OF assms(1)[unfolded xs_def] assms(2)]
[PROOF STATE]
proof (chain)
picking this:
(\<lbrakk>xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
have
    "xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'" and "x \<in>\<^sub>\<circ> A" and "n = vcard (xs' #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
using this:
(\<lbrakk>xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs' &&& x \<in>\<^sub>\<circ> A &&& n = vcard (xs' #\<^sub>\<circ> x)
[PROOF STEP]
by blast+
[PROOF STATE]
proof (state)
this:
xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'
x \<in>\<^sub>\<circ> A
n = vcard (xs' #\<^sub>\<circ> x)

goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; n = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from xs_def this
[PROOF STATE]
proof (chain)
picking this:
xs = xs' #\<^sub>\<circ> x
xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'
x \<in>\<^sub>\<circ> A
n = vcard (xs' #\<^sub>\<circ> x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
xs = xs' #\<^sub>\<circ> x
xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'
x \<in>\<^sub>\<circ> A
n = vcard (xs' #\<^sub>\<circ> x)

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vcons_vcpower1E: (*TODO: generalize*)
  assumes "xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> 1\<^sub>\<nat>"
  obtains x where "xs = [x]\<^sub>\<circ>" and "x \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
have 01: "0 \<in>\<^sub>\<circ> 1\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. []\<^sub>\<circ> \<in>\<^sub>\<circ> 1\<^sub>\<nat>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
[]\<^sub>\<circ> \<in>\<^sub>\<circ> 1\<^sub>\<nat>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from vcons_in_vcpowerE2[OF assms ord_of_nat_\<omega> 01]
[PROOF STATE]
proof (chain)
picking this:
(\<And>x xs'. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; 1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis
[PROOF STEP]
obtain x xs'
    where xs_def: "xs = xs' #\<^sub>\<circ> x"
      and xs': "xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'"
      and x: "x \<in>\<^sub>\<circ> A"
      and one: "1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x xs'. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; 1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> ?thesis) \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>xs' x. \<lbrakk>xs = xs' #\<^sub>\<circ> x; xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'; x \<in>\<^sub>\<circ> A; 1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
xs = xs' #\<^sub>\<circ> x
xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'
x \<in>\<^sub>\<circ> A
1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret xs: vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> A ^\<^sub>\<times> 1\<^sub>\<nat>

goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (auto intro: vfsequence_vcpower)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
interpret xs': vfsequence xs'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
using xs' xs_def xs.vfsequence_vremove_vcons_vfsequence
[PROOF STATE]
proof (prove)
using this:
xs' \<in>\<^sub>\<circ> A ^\<^sub>\<times> vcard xs'
xs = xs' #\<^sub>\<circ> x
xs = ?xs' #\<^sub>\<circ> ?x \<Longrightarrow> vfsequence ?xs'

goal (1 subgoal):
 1. vfsequence xs'
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
from one
[PROOF STATE]
proof (chain)
picking this:
1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)
[PROOF STEP]
have "vcard xs' = 0"
[PROOF STATE]
proof (prove)
using this:
1\<^sub>\<nat> = vcard (xs' #\<^sub>\<circ> x)

goal (1 subgoal):
 1. vcard xs' = []\<^sub>\<circ>
[PROOF STEP]
by (metis ord_of_nat_succ_vempty succ_inject_iff xs'.vfsequence_vcard_vcons)
[PROOF STATE]
proof (state)
this:
vcard xs' = []\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
vcard xs' = []\<^sub>\<circ>
[PROOF STEP]
have "xs = [x]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
vcard xs' = []\<^sub>\<circ>

goal (1 subgoal):
 1. xs = [x]\<^sub>\<circ>
[PROOF STEP]
unfolding xs_def
[PROOF STATE]
proof (prove)
using this:
vcard xs' = []\<^sub>\<circ>

goal (1 subgoal):
 1. xs' #\<^sub>\<circ> x = [x]\<^sub>\<circ>
[PROOF STEP]
by (simp add: vcard_vempty)
[PROOF STATE]
proof (state)
this:
xs = [x]\<^sub>\<circ>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>xs = [x]\<^sub>\<circ>; x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
with x that
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> A
\<lbrakk>xs = [?x]\<^sub>\<circ>; ?x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis
xs = [x]\<^sub>\<circ>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> A
\<lbrakk>xs = [?x]\<^sub>\<circ>; ?x \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> thesis
xs = [x]\<^sub>\<circ>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma vfsequences_on_subset_\<omega>_set:
  "{x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)} \<subseteq> elts (VPow (\<omega> \<times>\<^sub>\<circ> X))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)} \<subseteq> elts (VPow (\<omega> \<times>\<^sub>\<circ> X))
[PROOF STEP]
proof
  (
    intro subsetI,
    unfold mem_Collect_eq VPow_iff,
    elim conjE,
    intro vsubsetI
  )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
fix xs nx
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
assume prems[rule_format]:
    "vfsequence xs"
    "\<forall>i\<in>\<^sub>\<circ>\<D>\<^sub>\<circ> xs. xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X"
    "nx \<in>\<^sub>\<circ> xs"
[PROOF STATE]
proof (state)
this:
vfsequence xs
?i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> X
nx \<in>\<^sub>\<circ> xs

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
interpret vfsequence xs
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs
[PROOF STEP]
by (rule prems(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
from prems(3) vbrelation
[PROOF STATE]
proof (chain)
picking this:
nx \<in>\<^sub>\<circ> xs
vpairs xs = xs
[PROOF STEP]
obtain n x where nx_def: "nx = \<langle>n, x\<rangle>"
[PROOF STATE]
proof (prove)
using this:
nx \<in>\<^sub>\<circ> xs
vpairs xs = xs

goal (1 subgoal):
 1. (\<And>n x. nx = \<langle>n, x\<rangle> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
nx = \<langle>n, x\<rangle>

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
from vsv_appI[OF prems(3)[unfolded this]]
[PROOF STATE]
proof (chain)
picking this:
xs\<lparr>n\<rparr> = x
[PROOF STEP]
have xsn: "xs\<lparr>n\<rparr> = x"
[PROOF STATE]
proof (prove)
using this:
xs\<lparr>n\<rparr> = x

goal (1 subgoal):
 1. xs\<lparr>n\<rparr> = x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
xs\<lparr>n\<rparr> = x

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
from prems(3) nx_def
[PROOF STATE]
proof (chain)
picking this:
nx \<in>\<^sub>\<circ> xs
nx = \<langle>n, x\<rangle>
[PROOF STEP]
have "n \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs"
[PROOF STATE]
proof (prove)
using this:
nx \<in>\<^sub>\<circ> xs
nx = \<langle>n, x\<rangle>

goal (1 subgoal):
 1. n \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. \<And>x xa. \<lbrakk>vfsequence x; \<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X; xa \<in>\<^sub>\<circ> x\<rbrakk> \<Longrightarrow> xa \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
with prems(2)
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> X
n \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
[PROOF STEP]
show "nx \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> X
n \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs

goal (1 subgoal):
 1. nx \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X
[PROOF STEP]
by (auto simp: nx_def xsn[symmetric] Ord_trans vfsequence_vdomain_in_omega)
[PROOF STATE]
proof (state)
this:
nx \<in>\<^sub>\<circ> \<omega> \<times>\<^sub>\<circ> X

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_vfsequences_on[simp]:
  "small {x. vfsequence x \<and> (\<forall>i\<in>\<^sub>\<circ>\<D>\<^sub>\<circ> x. x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)}
[PROOF STEP]
by (rule down, rule vfsequences_on_subset_\<omega>_set)


[STATEMENT]
lemma vfsequences_onI:
  assumes "vfsequence xs" and "\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X"
  shows "xs \<in>\<^sub>\<circ> vfsequences_on X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> vfsequences_on X
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
?i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> vfsequences_on X
[PROOF STEP]
unfolding vfsequences_on_def
[PROOF STATE]
proof (prove)
using this:
vfsequence xs
?i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> X

goal (1 subgoal):
 1. xs \<in>\<^sub>\<circ> set {x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)}
[PROOF STEP]
by simp


[STATEMENT]
lemma vfsequences_onD[dest]:
  assumes "xs \<in>\<^sub>\<circ> vfsequences_on X"
  shows "vfsequence xs" and "\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence xs &&& (\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> vfsequences_on X

goal (1 subgoal):
 1. vfsequence xs &&& (\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)
[PROOF STEP]
unfolding vfsequences_on_def
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> set {x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)}

goal (1 subgoal):
 1. vfsequence xs &&& (\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)
[PROOF STEP]
by auto


[STATEMENT]
lemma vfsequences_onE[elim]:
  assumes "xs \<in>\<^sub>\<circ> vfsequences_on X"
  obtains "vfsequence xs" and "\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>vfsequence xs; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> vfsequences_on X

goal (1 subgoal):
 1. (\<lbrakk>vfsequence xs; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding vfsequences_on_def
[PROOF STATE]
proof (prove)
using this:
xs \<in>\<^sub>\<circ> set {x. vfsequence x \<and> (\<forall>i\<in>elts (\<D>\<^sub>\<circ> x). x\<lparr>i\<rparr> \<in>\<^sub>\<circ> X)}

goal (1 subgoal):
 1. (\<lbrakk>vfsequence xs; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> X\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma vfsequences_on_vsubset_mono:
  assumes "A \<subseteq>\<^sub>\<circ> B "
  shows "vfsequences_on A \<subseteq>\<^sub>\<circ> vfsequences_on B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequences_on A \<subseteq>\<^sub>\<circ> vfsequences_on B
[PROOF STEP]
proof(intro vsubsetI vfsequences_onI; elim vfsequences_onE)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> vfsequence x
 2. \<And>x i. \<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x; vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> B
[PROOF STEP]
fix i xs
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> vfsequence x
 2. \<And>x i. \<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x; vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> B
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs" "\<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs
?i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> xs \<Longrightarrow> xs\<lparr>?i\<rparr> \<in>\<^sub>\<circ> A

goal (2 subgoals):
 1. \<And>x. \<lbrakk>vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> vfsequence x
 2. \<And>x i. \<lbrakk>i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x; vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> B
[PROOF STEP]
from assms prems(2)[OF prems(1)]
[PROOF STATE]
proof (chain)
picking this:
A \<subseteq>\<^sub>\<circ> B
xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A
[PROOF STEP]
show "xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> B"
[PROOF STATE]
proof (prove)
using this:
A \<subseteq>\<^sub>\<circ> B
xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> A

goal (1 subgoal):
 1. xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> B
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xs\<lparr>i\<rparr> \<in>\<^sub>\<circ> B

goal (1 subgoal):
 1. \<And>x. \<lbrakk>vfsequence x; \<And>i. i \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> x \<Longrightarrow> x\<lparr>i\<rparr> \<in>\<^sub>\<circ> A\<rbrakk> \<Longrightarrow> vfsequence x
[PROOF STEP]
qed


[STATEMENT]
lemma
  weak_control_dependence_def:"n weakly controls n' =
    (\<exists>a a' as. (n' \<notin> set(sourcenodes (a#as))) \<and> (n -a#as\<rightarrow>* n') \<and>
                   (n' strongly-postdominates (targetnode a)) \<and>
                   (valid_edge a') \<and> (sourcenode a' = n) \<and>
                   (\<not> n' strongly-postdominates (targetnode a')))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n weakly controls n' = (\<exists>a a' as. n' \<notin> set (sourcenodes (a # as)) \<and> n -a # as\<rightarrow>* n' \<and> n' strongly-postdominates targetnode a \<and> valid_edge a' \<and> sourcenode a' = n \<and> \<not> n' strongly-postdominates targetnode a')
[PROOF STEP]
by(auto simp:weak_control_dependences_eq dyn_weak_control_dependence_def)


[STATEMENT]
lemma Exit_not_weak_control_dependent:
  "n weakly controls (_Exit_) \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n weakly controls (_Exit_) \<Longrightarrow> False
[PROOF STEP]
by(auto simp:weak_control_dependences_eq
        intro:Exit_not_dyn_weak_control_dependent)


[STATEMENT]
lemma tauPres:
  fixes P :: pi
  and   Q :: pi

  assumes "P \<sim> Q"

  shows "\<tau>.(P) \<sim> \<tau>.(Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
let ?X = "{(\<tau>.(P), \<tau>.(Q)) | P Q. P \<sim> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
from \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(\<tau>.(P), \<tau>.(Q)) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q) |P Q. P \<sim> Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q) |P Q. P \<sim> Q}

goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<tau>.P, \<tau>.Q) \<in> {(\<tau>.P, \<tau>.Q) |P Q. P \<sim> Q}

goal (1 subgoal):
 1. \<tau>.P \<sim> \<tau>.Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto intro: tauPres dest: bisimE)
[PROOF STATE]
proof (state)
this:
\<tau>.P \<sim> \<tau>.Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma inputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   x :: name

  assumes PSimQ: "\<forall>y. P[x::=y] \<sim> Q[x::=y]"

  shows "a<x>.P \<sim> a<x>.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
let ?X = "{(a<x>.P, a<x>.Q) | a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
fix axP axQ p
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
assume "(axP, axQ) \<in> ?X"
[PROOF STATE]
proof (state)
this:
(axP, axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(axP, axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
obtain a x P Q where A: "\<forall>y. P[x::=y] \<sim> Q[x::=y]" and B: "axP = a<x>.P" and C: "axQ = a<x>.Q"
[PROOF STATE]
proof (prove)
using this:
(axP, axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. (\<And>P x Q a. \<lbrakk>\<forall>y. P[x::=y] \<sim> Q[x::=y]; axP = a<x>.P; axQ = a<x>.Q\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]
axP = a<x>.P
axQ = a<x>.Q

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
have "\<And>y. ((p::name prm) \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
fix y
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]
[PROOF STEP]
have "P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]

goal (1 subgoal):
 1. P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
hence "(p \<bullet> (P[x::=(rev p \<bullet> y)])) \<sim> p \<bullet> (Q[x::=(rev p \<bullet> y)])"
[PROOF STATE]
proof (prove)
using this:
P[x::=(rev p \<bullet> y)] \<sim> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. p \<bullet> P[x::=(rev p \<bullet> y)] \<sim> p \<bullet> Q[x::=(rev p \<bullet> y)]
[PROOF STEP]
by(rule bisimClosed)
[PROOF STATE]
proof (state)
this:
p \<bullet> P[x::=(rev p \<bullet> y)] \<sim> p \<bullet> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. \<And>y. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
thus "(p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]"
[PROOF STATE]
proof (prove)
using this:
p \<bullet> P[x::=(rev p \<bullet> y)] \<sim> p \<bullet> Q[x::=(rev p \<bullet> y)]

goal (1 subgoal):
 1. (p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]
[PROOF STEP]
by(simp add: eqvts pt_pi_rev[OF pt_name_inst, OF at_name_inst])
[PROOF STATE]
proof (state)
this:
(p \<bullet> P)[(p \<bullet> x)::=y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=y]

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

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
hence "((p::name prm) \<bullet> axP, p \<bullet> axQ) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> P)[(p \<bullet> x)::=?y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=?y]

goal (1 subgoal):
 1. (p \<bullet> axP, p \<bullet> axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
using B C
[PROOF STATE]
proof (prove)
using this:
(p \<bullet> P)[(p \<bullet> x)::=?y] \<sim> (p \<bullet> Q)[(p \<bullet> x)::=?y]
axP = a<x>.P
axQ = a<x>.Q

goal (1 subgoal):
 1. (p \<bullet> axP, p \<bullet> axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(p \<bullet> axP, p \<bullet> axQ) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
(?axP2, ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (?p2 \<bullet> ?axP2, ?p2 \<bullet> ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
hence "eqvt ?X"
[PROOF STATE]
proof (prove)
using this:
(?axP2, ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (?p2 \<bullet> ?axP2, ?p2 \<bullet> ?axQ2) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. eqvt {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by(simp add: eqvt_def)
[PROOF STATE]
proof (state)
this:
eqvt {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
from PSimQ
[PROOF STATE]
proof (chain)
picking this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]
[PROOF STEP]
have "(a<x>.P, a<x>.Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
\<forall>y. P[x::=y] \<sim> Q[x::=y]

goal (1 subgoal):
 1. (a<x>.P, a<x>.Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a<x>.P, a<x>.Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(a<x>.P, a<x>.Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. a<x>.P \<sim> a<x>.Q
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> R \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
case(cSim P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> R \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. P \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] Q
[PROOF STEP]
using \<open>eqvt ?X\<close>
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
eqvt {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. P \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] Q
[PROOF STEP]
by(force intro: inputPres)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[({(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<union> bisim)] Q

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]} \<Longrightarrow> (S, R) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

goal (1 subgoal):
 1. (Q, P) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}
[PROOF STEP]
by(blast dest: bisimE)
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> {(a<x>.P, a<x>.Q) |a x P Q. \<forall>y. P[x::=y] \<sim> Q[x::=y]}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma outputPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<sim> Q"

  shows "a{b}.P \<sim> a{b}.Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
let ?X = "{(a{b}.P, a{b}.Q) | a b P Q. P \<sim> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
from \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(a{b}.P, a{b}.Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q) |a b P Q. P \<sim> Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q) |a b P Q. P \<sim> Q}

goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(a{b}.P, a{b}.Q) \<in> {(a{b}.P, a{b}.Q) |a b P Q. P \<sim> Q}

goal (1 subgoal):
 1. a{b}.P \<sim> a{b}.Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (blast intro: outputPres dest: bisimE)+
[PROOF STATE]
proof (state)
this:
a{b}.P \<sim> a{b}.Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma matchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<sim> Q"

  shows "[a\<frown>b]P \<sim> [a\<frown>b]Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
let ?X = "{x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<frown>b]P, [a\<frown>b]Q)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "([a\<frown>b]P, [a\<frown>b]Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. ([a\<frown>b]P, [a\<frown>b]Q) \<in> {x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<frown>b]P, [a\<frown>b]Q)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
([a\<frown>b]P, [a\<frown>b]Q) \<in> {x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<frown>b]P, [a\<frown>b]Q)}

goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
([a\<frown>b]P, [a\<frown>b]Q) \<in> {x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<frown>b]P, [a\<frown>b]Q)}

goal (1 subgoal):
 1. [a\<frown>b]P \<sim> [a\<frown>b]Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (blast intro: matchPres dest: bisimE)+
[PROOF STATE]
proof (state)
this:
[a\<frown>b]P \<sim> [a\<frown>b]Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mismatchPres:
  fixes P :: pi
  and   Q :: pi
  and   a :: name
  and   b :: name

  assumes "P \<sim> Q"

  shows "[a\<noteq>b]P \<sim> [a\<noteq>b]Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
let ?X = "{x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<noteq>b]P, [a\<noteq>b]Q)}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "([a\<noteq>b]P, [a\<noteq>b]Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. ([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<noteq>b]P, [a\<noteq>b]Q)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<noteq>b]P, [a\<noteq>b]Q)}

goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
([a\<noteq>b]P, [a\<noteq>b]Q) \<in> {x. \<exists>P Q a b. P \<sim> Q \<and> x = ([a\<noteq>b]P, [a\<noteq>b]Q)}

goal (1 subgoal):
 1. [a\<noteq>b]P \<sim> [a\<noteq>b]Q
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (blast intro: mismatchPres dest: bisimE)+
[PROOF STATE]
proof (state)
this:
[a\<noteq>b]P \<sim> [a\<noteq>b]Q

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes "P \<sim> Q"

  shows "P \<oplus> R \<sim> Q \<oplus> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
let ?X = "{(P \<oplus> R, Q \<oplus> R) | P Q R. P \<sim> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(P \<oplus> R, Q \<oplus> R) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R) |P Q R. P \<sim> Q}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R) |P Q R. P \<sim> Q}

goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<oplus> R, Q \<oplus> R) \<in> {(P \<oplus> R, Q \<oplus> R) |P Q R. P \<sim> Q}

goal (1 subgoal):
 1. P \<oplus> R \<sim> Q \<oplus> R
[PROOF STEP]
by(coinduct rule: bisimCoinduct) (auto dest: bisimE intro: reflexive sumPres)
[PROOF STATE]
proof (state)
this:
P \<oplus> R \<sim> Q \<oplus> R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma resPres:
  fixes P :: pi
  and   Q :: pi
  and   x :: name

  assumes "P \<sim> Q"

  shows "<\<nu>x>P \<sim> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
let ?X = "{x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(<\<nu>x>P, <\<nu>x>Q) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (<\<nu>x>P, <\<nu>x>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(<\<nu>x>P, <\<nu>x>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. <\<nu>x>P \<sim> <\<nu>x>Q
[PROOF STEP]
proof(coinduct rule: bisimCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
case(cSim xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
assume "P \<sim> Q"
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
hence "P \<leadsto>[bisim] Q"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. P \<leadsto>[bisim] Q
[PROOF STEP]
by(rule bisimE)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "\<And>P Q a. P \<sim> Q \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> ?X \<union> bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q a. P \<sim> Q \<Longrightarrow> (<\<nu>a>P, <\<nu>a>Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "bisim \<subseteq> ?X \<union> bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "eqvt bisim"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt bisim
[PROOF STEP]
by(rule eqvt)
[PROOF STATE]
proof (state)
this:
eqvt bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt bisim

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
have "eqvt (?X \<union> bisim)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)
[PROOF STEP]
using eqvts
[PROOF STATE]
proof (prove)
using this:
?p1 \<bullet> (?P1 \<sim> ?Q1) = ?p1 \<bullet> ?P1 \<sim> ?p1 \<bullet> ?Q1
?P \<sim> ?Q \<Longrightarrow> ?p \<bullet> ?P \<sim> ?p \<bullet> ?Q
?pi1 \<bullet> ?x1.1 \<longmapsto> ?x2.1 = ?pi1 \<bullet> ?x1.1 \<longmapsto> ?pi1 \<bullet> ?x2.1
?x1.0 \<longmapsto> ?x2.0 \<Longrightarrow> ?pi \<bullet> ?x1.0 \<longmapsto> ?pi \<bullet> ?x2.0
?pi \<bullet> ?x2.0 \<prec> ?x1.0 = ?pi \<bullet> ?x2.0 \<prec> ?pi \<bullet> ?x1.0
?pi \<bullet> ?x3.0<\<nu>?x1.0> \<prec> ?x2.0 = (?pi \<bullet> ?x3.0)<\<nu>(?pi \<bullet> ?x1.0)> \<prec> (?pi \<bullet> ?x2.0)
?pi \<bullet> \<tau> = \<tau>
?pi \<bullet> ?x2.0[?x1.0] = (?pi \<bullet> ?x2.0)[(?pi \<bullet> ?x1.0)]
?pi \<bullet> ?x2.0<?x1.0> = (?pi \<bullet> ?x2.0)<(?pi \<bullet> ?x1.0)>
?p \<bullet> ?P[<?\<sigma>>] = (?p \<bullet> ?P)[<(?p \<bullet> ?\<sigma>)>]
?p \<bullet> ?P[?a::=?b] = (?p \<bullet> ?P)[(?p \<bullet> ?a)::=(?p \<bullet> ?b)]
?p \<bullet> ?a[?b::=?c] = (?p \<bullet> ?a)[(?p \<bullet> ?b)::=(?p \<bullet> ?c)]
?pi \<bullet> !?x1.0 = !(?pi \<bullet> ?x1.0)
?pi \<bullet> <\<nu>?x1.0>?x2.0 = <\<nu>(?pi \<bullet> ?x1.0)>(?pi \<bullet> ?x2.0)
?pi \<bullet> ?x2.0 \<parallel> ?x1.0 = (?pi \<bullet> ?x2.0) \<parallel> (?pi \<bullet> ?x1.0)
?pi \<bullet> ?x2.0 \<oplus> ?x1.0 = (?pi \<bullet> ?x2.0) \<oplus> (?pi \<bullet> ?x1.0)
?pi \<bullet> [?x3.0\<noteq>?x2.0]?x1.0 = [(?pi \<bullet> ?x3.0)\<noteq>(?pi \<bullet> ?x2.0)](?pi \<bullet> ?x1.0)
?pi \<bullet> [?x3.0\<frown>?x2.0]?x1.0 = [(?pi \<bullet> ?x3.0)\<frown>(?pi \<bullet> ?x2.0)](?pi \<bullet> ?x1.0)
?pi \<bullet> ?x3.0<?x1.0>.?x2.0 = (?pi \<bullet> ?x3.0)<(?pi \<bullet> ?x1.0)>.(?pi \<bullet> ?x2.0)
?pi \<bullet> \<tau>.?x1.0 = \<tau>.(?pi \<bullet> ?x1.0)
?pi \<bullet> ?x3.0{?x2.0}.?x1.0 = (?pi \<bullet> ?x3.0){(?pi \<bullet> ?x2.0)}.(?pi \<bullet> ?x1.0)
?pi \<bullet> \<zero> = \<zero>
?pi \<bullet> supp ?x = supp (?pi \<bullet> ?x)
?pi \<bullet> (?X \<subseteq> ?Y) = (?pi \<bullet> ?X \<subseteq> ?pi \<bullet> ?Y)
?pi \<bullet> (?X - ?Y) = ?pi \<bullet> ?X - ?pi \<bullet> ?Y
?pi \<bullet> (?x = ?y) = (?pi \<bullet> ?x = ?pi \<bullet> ?y)
?pi \<bullet> (?x \<in> ?X) = (?pi \<bullet> ?x \<in> ?pi \<bullet> ?X)
?pi \<bullet> ?b \<sharp>* ?x = (?pi \<bullet> ?b) \<sharp>* (?pi \<bullet> ?x)
?pi \<bullet> ?a \<sharp>* ?x = (?pi \<bullet> ?a) \<sharp>* (?pi \<bullet> ?x)
?pi \<bullet> ?a \<sharp> ?x = ?pi \<bullet> ?a \<sharp> ?pi \<bullet> ?x
?pi \<bullet> [?a].?x = [(?pi \<bullet> ?a)].(?pi \<bullet> ?x)
\<exists>!x. ?P x \<Longrightarrow> ?pi \<bullet> (THE x. ?P x) = (THE x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> (\<exists>!x. ?P x) = (\<exists>!x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> (\<exists>x. ?P x) = (\<exists>x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> HOL.induct_forall ?P = HOL.induct_forall (\<lambda>x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> (\<forall>x. ?P x) = (\<forall>x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> - numeral ?n = - numeral ?n
?pi \<bullet> numeral ?n = numeral ?n
?pi \<bullet> numeral ?n = numeral ?n
?pi \<bullet> set ?xs = set (?pi \<bullet> ?xs)
?pi \<bullet> insert ?x ?X = insert (?pi \<bullet> ?x) (?pi \<bullet> ?X)
?pi \<bullet> {} = {}
?pi \<bullet> (?X \<union> ?Y) = ?pi \<bullet> ?X \<union> ?pi \<bullet> ?Y
?pi \<bullet> (?x div ?y) = ?pi \<bullet> ?x div ?pi \<bullet> ?y
?pi \<bullet> (?x * ?y) = ?pi \<bullet> ?x * ?pi \<bullet> ?y
?pi \<bullet> (?x - ?y) = ?pi \<bullet> ?x - ?pi \<bullet> ?y
?pi \<bullet> (?x + ?y) = ?pi \<bullet> ?x + ?pi \<bullet> ?y
?pi \<bullet> max ?x ?y = max (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> min ?x ?y = min (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> 1 = 1
?pi \<bullet> 0 = 0
?pi \<bullet> (?x div ?y) = ?pi \<bullet> ?x div ?pi \<bullet> ?y
?pi \<bullet> (?x * ?y) = ?pi \<bullet> ?x * ?pi \<bullet> ?y
?pi \<bullet> (?x - ?y) = ?pi \<bullet> ?x - ?pi \<bullet> ?y
?pi \<bullet> (?x + ?y) = ?pi \<bullet> ?x + ?pi \<bullet> ?y
?pi \<bullet> max ?x ?y = max (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> min ?x ?y = min (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> 1 = 1
?pi \<bullet> 0 = 0
?pi \<bullet> Suc ?x = Suc (?pi \<bullet> ?x)
?pi \<bullet> None = None
?pi \<bullet> Some ?x = Some (?pi \<bullet> ?x)
?pi \<bullet> snd ?x = snd (?pi \<bullet> ?x)
?pi \<bullet> fst ?x = fst (?pi \<bullet> ?x)
?pi \<bullet> (?x, ?y) = (?pi \<bullet> ?x, ?pi \<bullet> ?y)
?pi \<bullet> (?l1.0 @ ?l2.0) = ?pi \<bullet> ?l1.0 @ ?pi \<bullet> ?l2.0
?pi \<bullet> (?x # ?xs) = ?pi \<bullet> ?x # ?pi \<bullet> ?xs
?pi \<bullet> [] = []
?pi \<bullet> () = ()
?pi \<bullet> HOL.induct_implies ?A ?B = HOL.induct_implies (?pi \<bullet> ?A) (?pi \<bullet> ?B)
?pi \<bullet> False = False
?pi \<bullet> True = True
?pi \<bullet> (\<not> ?A) = (\<not> ?pi \<bullet> ?A)
?pi \<bullet> (?A \<and> ?B) = (?pi \<bullet> ?A \<and> ?pi \<bullet> ?B)
?pi \<bullet> (?A \<or> ?B) = (?pi \<bullet> ?A \<or> ?pi \<bullet> ?B)
?pi \<bullet> (?A \<longrightarrow> ?B) = (?pi \<bullet> ?A \<longrightarrow> ?pi \<bullet> ?B)
?pi \<bullet> (if ?b then ?c1.0 else ?c2.0) = (if ?pi \<bullet> ?b then ?pi \<bullet> ?c1.0 else ?pi \<bullet> ?c2.0)

goal (1 subgoal):
 1. eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)
[PROOF STEP]
by(auto simp add: eqvt_def) blast
[PROOF STATE]
proof (state)
this:
eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[bisim] Q
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
eqvt bisim
eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)
[PROOF STEP]
have "<\<nu>a>P \<leadsto>[(?X \<union> bisim)] <\<nu>a>Q"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q
?P \<sim> ?Q \<Longrightarrow> (<\<nu>?a>?P, <\<nu>?a>?Q) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
bisim \<subseteq> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim
eqvt bisim
eqvt ({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)

goal (1 subgoal):
 1. <\<nu>a>P \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>a>Q
[PROOF STEP]
by(rule Strong_Early_Sim_Pres.resPres)
[PROOF STATE]
proof (state)
this:
<\<nu>a>P \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>a>Q

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Pa2 \<sim> ?Qa2 \<Longrightarrow> <\<nu>?a2>?Pa2 \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>?a2>?Qa2

goal (2 subgoals):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> R \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] S
 2. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
?Pa2 \<sim> ?Qa2 \<Longrightarrow> <\<nu>?a2>?Pa2 \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>?a2>?Qa2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
?Pa2 \<sim> ?Qa2 \<Longrightarrow> <\<nu>?a2>?Pa2 \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] <\<nu>?a2>?Qa2

goal (1 subgoal):
 1. xP \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] xQ
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
xP \<leadsto>[({x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<union> bisim)] xQ

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
case(cSym xP xQ)
[PROOF STATE]
proof (state)
this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. \<And>R S. (R, S) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))} \<Longrightarrow> (S, R) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(xP, xQ) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

goal (1 subgoal):
 1. (xQ, xP) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}
[PROOF STEP]
by(auto dest: bisimE)
[PROOF STATE]
proof (state)
this:
(xQ, xP) \<in> {x. \<exists>P Q. P \<sim> Q \<and> (\<exists>a. x = (<\<nu>a>P, <\<nu>a>Q))}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma parPres:
  fixes P :: pi
  and   Q :: pi
  and   R :: pi
  and   T :: pi

  assumes "P \<sim> Q"

  shows "P \<parallel> R \<sim> Q \<parallel> R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
let ?X = "{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) | lst P Q R. P \<sim> Q}"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
have BC: "\<And>P Q. P \<parallel> Q = resChain [] (P \<parallel> Q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q. P \<parallel> Q = resChain [] (P \<parallel> Q)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
?P \<parallel> ?Q = resChain [] (?P \<parallel> ?Q)

goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "(P \<parallel> R, Q \<parallel> R) \<in> ?X"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. (P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
by(blast intro: BC)
[PROOF STATE]
proof (state)
this:
(P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<sim> Q \<parallel> R
[PROOF STEP]
proof(coinduct rule: bisimWeakCoinduct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
case(cSim PR QR)
[PROOF STATE]
proof (state)
this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
fix lst P Q R
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
assume "P \<sim> Q"
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
have "eqvt ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
using eqvts
[PROOF STATE]
proof (prove)
using this:
?p1 \<bullet> (?P1 \<sim> ?Q1) = ?p1 \<bullet> ?P1 \<sim> ?p1 \<bullet> ?Q1
?P \<sim> ?Q \<Longrightarrow> ?p \<bullet> ?P \<sim> ?p \<bullet> ?Q
?pi1 \<bullet> ?x1.1 \<longmapsto> ?x2.1 = ?pi1 \<bullet> ?x1.1 \<longmapsto> ?pi1 \<bullet> ?x2.1
?x1.0 \<longmapsto> ?x2.0 \<Longrightarrow> ?pi \<bullet> ?x1.0 \<longmapsto> ?pi \<bullet> ?x2.0
?pi \<bullet> ?x2.0 \<prec> ?x1.0 = ?pi \<bullet> ?x2.0 \<prec> ?pi \<bullet> ?x1.0
?pi \<bullet> ?x3.0<\<nu>?x1.0> \<prec> ?x2.0 = (?pi \<bullet> ?x3.0)<\<nu>(?pi \<bullet> ?x1.0)> \<prec> (?pi \<bullet> ?x2.0)
?pi \<bullet> \<tau> = \<tau>
?pi \<bullet> ?x2.0[?x1.0] = (?pi \<bullet> ?x2.0)[(?pi \<bullet> ?x1.0)]
?pi \<bullet> ?x2.0<?x1.0> = (?pi \<bullet> ?x2.0)<(?pi \<bullet> ?x1.0)>
?p \<bullet> ?P[<?\<sigma>>] = (?p \<bullet> ?P)[<(?p \<bullet> ?\<sigma>)>]
?p \<bullet> ?P[?a::=?b] = (?p \<bullet> ?P)[(?p \<bullet> ?a)::=(?p \<bullet> ?b)]
?p \<bullet> ?a[?b::=?c] = (?p \<bullet> ?a)[(?p \<bullet> ?b)::=(?p \<bullet> ?c)]
?pi \<bullet> !?x1.0 = !(?pi \<bullet> ?x1.0)
?pi \<bullet> <\<nu>?x1.0>?x2.0 = <\<nu>(?pi \<bullet> ?x1.0)>(?pi \<bullet> ?x2.0)
?pi \<bullet> ?x2.0 \<parallel> ?x1.0 = (?pi \<bullet> ?x2.0) \<parallel> (?pi \<bullet> ?x1.0)
?pi \<bullet> ?x2.0 \<oplus> ?x1.0 = (?pi \<bullet> ?x2.0) \<oplus> (?pi \<bullet> ?x1.0)
?pi \<bullet> [?x3.0\<noteq>?x2.0]?x1.0 = [(?pi \<bullet> ?x3.0)\<noteq>(?pi \<bullet> ?x2.0)](?pi \<bullet> ?x1.0)
?pi \<bullet> [?x3.0\<frown>?x2.0]?x1.0 = [(?pi \<bullet> ?x3.0)\<frown>(?pi \<bullet> ?x2.0)](?pi \<bullet> ?x1.0)
?pi \<bullet> ?x3.0<?x1.0>.?x2.0 = (?pi \<bullet> ?x3.0)<(?pi \<bullet> ?x1.0)>.(?pi \<bullet> ?x2.0)
?pi \<bullet> \<tau>.?x1.0 = \<tau>.(?pi \<bullet> ?x1.0)
?pi \<bullet> ?x3.0{?x2.0}.?x1.0 = (?pi \<bullet> ?x3.0){(?pi \<bullet> ?x2.0)}.(?pi \<bullet> ?x1.0)
?pi \<bullet> \<zero> = \<zero>
?pi \<bullet> supp ?x = supp (?pi \<bullet> ?x)
?pi \<bullet> (?X \<subseteq> ?Y) = (?pi \<bullet> ?X \<subseteq> ?pi \<bullet> ?Y)
?pi \<bullet> (?X - ?Y) = ?pi \<bullet> ?X - ?pi \<bullet> ?Y
?pi \<bullet> (?x = ?y) = (?pi \<bullet> ?x = ?pi \<bullet> ?y)
?pi \<bullet> (?x \<in> ?X) = (?pi \<bullet> ?x \<in> ?pi \<bullet> ?X)
?pi \<bullet> ?b \<sharp>* ?x = (?pi \<bullet> ?b) \<sharp>* (?pi \<bullet> ?x)
?pi \<bullet> ?a \<sharp>* ?x = (?pi \<bullet> ?a) \<sharp>* (?pi \<bullet> ?x)
?pi \<bullet> ?a \<sharp> ?x = ?pi \<bullet> ?a \<sharp> ?pi \<bullet> ?x
?pi \<bullet> [?a].?x = [(?pi \<bullet> ?a)].(?pi \<bullet> ?x)
\<exists>!x. ?P x \<Longrightarrow> ?pi \<bullet> (THE x. ?P x) = (THE x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> (\<exists>!x. ?P x) = (\<exists>!x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> (\<exists>x. ?P x) = (\<exists>x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> HOL.induct_forall ?P = HOL.induct_forall (\<lambda>x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> (\<forall>x. ?P x) = (\<forall>x. ?pi \<bullet> ?P (rev ?pi \<bullet> x))
?pi \<bullet> - numeral ?n = - numeral ?n
?pi \<bullet> numeral ?n = numeral ?n
?pi \<bullet> numeral ?n = numeral ?n
?pi \<bullet> set ?xs = set (?pi \<bullet> ?xs)
?pi \<bullet> insert ?x ?X = insert (?pi \<bullet> ?x) (?pi \<bullet> ?X)
?pi \<bullet> {} = {}
?pi \<bullet> (?X \<union> ?Y) = ?pi \<bullet> ?X \<union> ?pi \<bullet> ?Y
?pi \<bullet> (?x div ?y) = ?pi \<bullet> ?x div ?pi \<bullet> ?y
?pi \<bullet> (?x * ?y) = ?pi \<bullet> ?x * ?pi \<bullet> ?y
?pi \<bullet> (?x - ?y) = ?pi \<bullet> ?x - ?pi \<bullet> ?y
?pi \<bullet> (?x + ?y) = ?pi \<bullet> ?x + ?pi \<bullet> ?y
?pi \<bullet> max ?x ?y = max (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> min ?x ?y = min (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> 1 = 1
?pi \<bullet> 0 = 0
?pi \<bullet> (?x div ?y) = ?pi \<bullet> ?x div ?pi \<bullet> ?y
?pi \<bullet> (?x * ?y) = ?pi \<bullet> ?x * ?pi \<bullet> ?y
?pi \<bullet> (?x - ?y) = ?pi \<bullet> ?x - ?pi \<bullet> ?y
?pi \<bullet> (?x + ?y) = ?pi \<bullet> ?x + ?pi \<bullet> ?y
?pi \<bullet> max ?x ?y = max (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> min ?x ?y = min (?pi \<bullet> ?x) (?pi \<bullet> ?y)
?pi \<bullet> 1 = 1
?pi \<bullet> 0 = 0
?pi \<bullet> Suc ?x = Suc (?pi \<bullet> ?x)
?pi \<bullet> None = None
?pi \<bullet> Some ?x = Some (?pi \<bullet> ?x)
?pi \<bullet> snd ?x = snd (?pi \<bullet> ?x)
?pi \<bullet> fst ?x = fst (?pi \<bullet> ?x)
?pi \<bullet> (?x, ?y) = (?pi \<bullet> ?x, ?pi \<bullet> ?y)
?pi \<bullet> (?l1.0 @ ?l2.0) = ?pi \<bullet> ?l1.0 @ ?pi \<bullet> ?l2.0
?pi \<bullet> (?x # ?xs) = ?pi \<bullet> ?x # ?pi \<bullet> ?xs
?pi \<bullet> [] = []
?pi \<bullet> () = ()
?pi \<bullet> HOL.induct_implies ?A ?B = HOL.induct_implies (?pi \<bullet> ?A) (?pi \<bullet> ?B)
?pi \<bullet> False = False
?pi \<bullet> True = True
?pi \<bullet> (\<not> ?A) = (\<not> ?pi \<bullet> ?A)
?pi \<bullet> (?A \<and> ?B) = (?pi \<bullet> ?A \<and> ?pi \<bullet> ?B)
?pi \<bullet> (?A \<or> ?B) = (?pi \<bullet> ?A \<or> ?pi \<bullet> ?B)
?pi \<bullet> (?A \<longrightarrow> ?B) = (?pi \<bullet> ?A \<longrightarrow> ?pi \<bullet> ?B)
?pi \<bullet> (if ?b then ?c1.0 else ?c2.0) = (if ?pi \<bullet> ?b then ?pi \<bullet> ?c1.0 else ?pi \<bullet> ?c2.0)

goal (1 subgoal):
 1. eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
by(auto simp add: eqvt_def) blast
[PROOF STATE]
proof (state)
this:
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
have Res: "\<And>P Q x. (P, Q) \<in> ?X \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q x. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>x>P, <\<nu>x>Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
by(auto, rule_tac x="x#lst" in exI) auto
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
(?P, ?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
from \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (chain)
picking this:
P \<sim> Q
[PROOF STEP]
have "P \<leadsto>[bisim] Q"
[PROOF STATE]
proof (prove)
using this:
P \<sim> Q

goal (1 subgoal):
 1. P \<leadsto>[bisim] Q
[PROOF STEP]
by(rule bisimE)
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<leadsto>[bisim] Q

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
note \<open>P \<sim> Q\<close>
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
P \<sim> Q

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
have "\<And>P Q R. P \<sim> Q \<Longrightarrow> (P \<parallel> R, Q \<parallel> R) \<in> ?X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>P Q R. P \<sim> Q \<Longrightarrow> (P \<parallel> R, Q \<parallel> R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
by(blast intro: BC)
[PROOF STATE]
proof (state)
this:
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
P \<leadsto>[bisim] Q
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
have "P \<parallel> R \<leadsto>[?X] Q \<parallel> R"
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q \<parallel> R
[PROOF STEP]
using Res
[PROOF STATE]
proof (prove)
using this:
P \<leadsto>[bisim] Q
P \<sim> Q
?P \<sim> ?Q \<Longrightarrow> (?P \<parallel> ?R, ?Q \<parallel> ?R) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
(?P, ?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (1 subgoal):
 1. P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q \<parallel> R
[PROOF STEP]
by(rule parPres)
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q \<parallel> R

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q \<parallel> R

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
(?P, ?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q \<parallel> R
[PROOF STEP]
have "resChain lst (P \<parallel> R) \<leadsto>[?X] resChain lst (Q \<parallel> R)"
[PROOF STATE]
proof (prove)
using this:
eqvt {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
(?P, ?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (<\<nu>?x>?P, <\<nu>?x>?Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
P \<parallel> R \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q \<parallel> R

goal (1 subgoal):
 1. resChain lst (P \<parallel> R) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] resChain lst (Q \<parallel> R)
[PROOF STEP]
by(rule resChainI)
[PROOF STATE]
proof (state)
this:
resChain lst (P \<parallel> R) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] resChain lst (Q \<parallel> R)

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?Pa2 \<sim> ?Qa2 \<Longrightarrow> resChain ?lst2 (?Pa2 \<parallel> ?Ra2) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] resChain ?lst2 (?Qa2 \<parallel> ?Ra2)

goal (2 subgoals):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> P \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] Q
 2. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
?Pa2 \<sim> ?Qa2 \<Longrightarrow> resChain ?lst2 (?Pa2 \<parallel> ?Ra2) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] resChain ?lst2 (?Qa2 \<parallel> ?Ra2)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
(PR, QR) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
?Pa2 \<sim> ?Qa2 \<Longrightarrow> resChain ?lst2 (?Pa2 \<parallel> ?Ra2) \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] resChain ?lst2 (?Qa2 \<parallel> ?Ra2)

goal (1 subgoal):
 1. PR \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] QR
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
PR \<leadsto>[{(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}] QR

goal (1 subgoal):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
case(cSym P Q)
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (1 subgoal):
 1. \<And>P Q. (P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q} \<Longrightarrow> (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal (1 subgoal):
 1. (Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}
[PROOF STEP]
by(auto dest: bisimE)
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> {(resChain lst (P \<parallel> R), resChain lst (Q \<parallel> R)) |lst P Q R. P \<sim> Q}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
P \<parallel> R \<sim> Q \<parallel> R

goal:
No subgoals!
[PROOF STEP]
qed


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

  assumes A:   "(P, Q) \<in> bangRel Rel"
  and     Sym: "\<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (Q, P) \<in> Rel"

  shows "(Q, P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Q, P) \<in> bangRel Rel
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (Q, P) \<in> bangRel Rel
[PROOF STEP]
from A
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> bangRel Rel
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> bangRel Rel

goal (1 subgoal):
 1. (Q, P) \<in> bangRel Rel
[PROOF STEP]
proof(induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume "(P, Q) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(P, Q) \<in> Rel

goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
hence "(Q, P) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> Rel

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

goal (3 subgoals):
 1. \<And>P Q. (P, Q) \<in> Rel \<Longrightarrow> (!Q, !P) \<in> bangRel Rel
 2. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 3. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
thus "(!Q, !P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(Q, P) \<in> Rel

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

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
fix P Q R T
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume RRelT: "(R, T) \<in> Rel"
[PROOF STATE]
proof (state)
this:
(R, T) \<in> Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume IH: "(Q, P) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> bangRel Rel

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
from RRelT
[PROOF STATE]
proof (chain)
picking this:
(R, T) \<in> Rel
[PROOF STEP]
have "(T, R) \<in> Rel"
[PROOF STATE]
proof (prove)
using this:
(R, T) \<in> Rel

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

goal (2 subgoals):
 1. \<And>R T P Q. \<lbrakk>(R, T) \<in> Rel; (P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
 2. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
thus "(T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(T, R) \<in> Rel

goal (1 subgoal):
 1. (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
[PROOF STEP]
using IH
[PROOF STATE]
proof (prove)
using this:
(T, R) \<in> Rel
(Q, P) \<in> bangRel Rel

goal (1 subgoal):
 1. (T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel
[PROOF STEP]
by(rule BRPar)
[PROOF STATE]
proof (state)
this:
(T \<parallel> Q, R \<parallel> P) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
fix P Q a
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
assume "(Q, P) \<in> bangRel Rel"
[PROOF STATE]
proof (state)
this:
(Q, P) \<in> bangRel Rel

goal (1 subgoal):
 1. \<And>P Q a. \<lbrakk>(P, Q) \<in> bangRel Rel; (Q, P) \<in> bangRel Rel\<rbrakk> \<Longrightarrow> (<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel
[PROOF STEP]
thus "(<\<nu>a>Q, <\<nu>a>P) \<in> bangRel Rel"
[PROOF STATE]
proof (prove)
using this:
(Q, P) \<in> bangRel Rel

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

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

goal:
No subgoals!
[PROOF STEP]
qed