[STATEMENT]
lemma kernel_of_eq_imp_bij:
  assumes "kernel_of x = kernel_of y"
  shows "\<exists>f. bij_betw f (set x) (set y) \<and>
    (\<forall>z \<in> set x. count_list x z = count_list y (f z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
obtain x' where x'_def: "inj_on x' (set x)" "rgf (map x' x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>inj_on x' (set x); rgf (map x' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using map_list_to_rgf
[PROOF STATE]
proof (prove)
using this:
\<exists>f. inj_on f (set ?x) \<and> rgf (map f ?x)

goal (1 subgoal):
 1. (\<And>x'. \<lbrakk>inj_on x' (set x); rgf (map x' x)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on x' (set x)
rgf (map x' x)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
obtain y' where y'_def: "inj_on y' (set y)" "rgf (map y' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>inj_on y' (set y); rgf (map y' y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using map_list_to_rgf
[PROOF STATE]
proof (prove)
using this:
\<exists>f. inj_on f (set ?x) \<and> rgf (map f ?x)

goal (1 subgoal):
 1. (\<And>y'. \<lbrakk>inj_on y' (set y); rgf (map y' y)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
inj_on y' (set y)
rgf (map y' y)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
have "kernel_of (map x' x) = kernel_of (map y' y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. kernel_of (map x' x) = kernel_of (map y' y)
[PROOF STEP]
using assms x'_def(1) y'_def(1)
[PROOF STATE]
proof (prove)
using this:
kernel_of x = kernel_of y
inj_on x' (set x)
inj_on y' (set y)

goal (1 subgoal):
 1. kernel_of (map x' x) = kernel_of (map y' y)
[PROOF STEP]
by (simp add: kernel_of_under_inj_map[symmetric])
[PROOF STATE]
proof (state)
this:
kernel_of (map x' x) = kernel_of (map y' y)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
hence b:"map x' x = map y' y"
[PROOF STATE]
proof (prove)
using this:
kernel_of (map x' x) = kernel_of (map y' y)

goal (1 subgoal):
 1. map x' x = map y' y
[PROOF STEP]
using inj_onD[OF kernel_of_inj_on_rgfs] x'_def(2) y'_def(2) length_map
[PROOF STATE]
proof (prove)
using this:
kernel_of (map x' x) = kernel_of (map y' y)
\<lbrakk>kernel_of ?x = kernel_of ?y; ?x \<in> {x. rgf x}; ?y \<in> {x. rgf x}\<rbrakk> \<Longrightarrow> ?x = ?y
rgf (map x' x)
rgf (map y' y)
length (map ?f ?xs) = length ?xs

goal (1 subgoal):
 1. map x' x = map y' y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
map x' x = map y' y

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
hence f: "x' ` set x = y' ` set y"
[PROOF STATE]
proof (prove)
using this:
map x' x = map y' y

goal (1 subgoal):
 1. x' ` set x = y' ` set y
[PROOF STEP]
by (metis list.set_map)
[PROOF STATE]
proof (state)
this:
x' ` set x = y' ` set y

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
define f where "f = the_inv_into (set y) y' \<circ> x'"
[PROOF STATE]
proof (state)
this:
f = the_inv_into (set y) y' \<circ> x'

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
have g:"\<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
fix z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
assume a:"z \<in> set x"
[PROOF STATE]
proof (state)
this:
z \<in> set x

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have e: "x' z \<in> y' ` set y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x' z \<in> y' ` set y
[PROOF STEP]
by (metis a b imageI image_set)
[PROOF STATE]
proof (state)
this:
x' z \<in> y' ` set y

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have c: "the_inv_into (set y) y' (x' z) \<in> set y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. the_inv_into (set y) y' (x' z) \<in> set y
[PROOF STEP]
using e the_inv_into_into[OF y'_def(1)]
[PROOF STATE]
proof (prove)
using this:
x' z \<in> y' ` set y
\<lbrakk>?x \<in> y' ` set y; set y \<subseteq> ?B\<rbrakk> \<Longrightarrow> the_inv_into (set y) y' ?x \<in> ?B

goal (1 subgoal):
 1. the_inv_into (set y) y' (x' z) \<in> set y
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
the_inv_into (set y) y' (x' z) \<in> set y

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have d: "(y' (the_inv_into (set y) y' (x' z))) = x' z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y' (the_inv_into (set y) y' (x' z)) = x' z
[PROOF STEP]
using e f_the_inv_into_f y'_def(1)
[PROOF STATE]
proof (prove)
using this:
x' z \<in> y' ` set y
\<lbrakk>inj_on ?f ?A; ?y \<in> ?f ` ?A\<rbrakk> \<Longrightarrow> ?f (the_inv_into ?A ?f ?y) = ?y
inj_on y' (set y)

goal (1 subgoal):
 1. y' (the_inv_into (set y) y' (x' z)) = x' z
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y' (the_inv_into (set y) y' (x' z)) = x' z

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have "count_list x z = count_list (map x' x) (x' z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list x z = count_list (map x' x) (x' z)
[PROOF STEP]
using a x'_def
[PROOF STATE]
proof (prove)
using this:
z \<in> set x
inj_on x' (set x)
rgf (map x' x)

goal (1 subgoal):
 1. count_list x z = count_list (map x' x) (x' z)
[PROOF STEP]
by (simp add: count_list_inj_map)
[PROOF STATE]
proof (state)
this:
count_list x z = count_list (map x' x) (x' z)

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_list x z = count_list (map x' x) (x' z)

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have "... = count_list (map y' y) (x' z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (map x' x) (x' z) = count_list (map y' y) (x' z)
[PROOF STEP]
by (simp add:b)
[PROOF STATE]
proof (state)
this:
count_list (map x' x) (x' z) = count_list (map y' y) (x' z)

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_list (map x' x) (x' z) = count_list (map y' y) (x' z)

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have "... = count_list (map y' y) (y' (the_inv_into (set y) y' (x' z)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (map y' y) (x' z) = count_list (map y' y) (y' (the_inv_into (set y) y' (x' z)))
[PROOF STEP]
by (simp add:d)
[PROOF STATE]
proof (state)
this:
count_list (map y' y) (x' z) = count_list (map y' y) (y' (the_inv_into (set y) y' (x' z)))

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_list (map y' y) (x' z) = count_list (map y' y) (y' (the_inv_into (set y) y' (x' z)))

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have "... = count_list y (the_inv_into (set y) y' (x' z))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list (map y' y) (y' (the_inv_into (set y) y' (x' z))) = count_list y (the_inv_into (set y) y' (x' z))
[PROOF STEP]
using c count_list_inj_map[OF y'_def(1)]
[PROOF STATE]
proof (prove)
using this:
the_inv_into (set y) y' (x' z) \<in> set y
?y \<in> set y \<Longrightarrow> count_list (map y' y) (y' ?y) = count_list y ?y

goal (1 subgoal):
 1. count_list (map y' y) (y' (the_inv_into (set y) y' (x' z))) = count_list y (the_inv_into (set y) y' (x' z))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list (map y' y) (y' (the_inv_into (set y) y' (x' z))) = count_list y (the_inv_into (set y) y' (x' z))

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
count_list (map y' y) (y' (the_inv_into (set y) y' (x' z))) = count_list y (the_inv_into (set y) y' (x' z))

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
have "... = count_list y (f z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. count_list y (the_inv_into (set y) y' (x' z)) = count_list y (f z)
[PROOF STEP]
by (simp add:f_def)
[PROOF STATE]
proof (state)
this:
count_list y (the_inv_into (set y) y' (x' z)) = count_list y (f z)

goal (1 subgoal):
 1. \<And>z. z \<in> set x \<Longrightarrow> count_list x z = count_list y (f z)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
count_list x z = count_list y (f z)
[PROOF STEP]
show "count_list x z = count_list y (f z)"
[PROOF STATE]
proof (prove)
using this:
count_list x z = count_list y (f z)

goal (1 subgoal):
 1. count_list x z = count_list y (f z)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
count_list x z = count_list y (f z)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?z \<in> set x \<Longrightarrow> count_list x ?z = count_list y (f ?z)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
have "bij_betw x' (set x) (x' ` set x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw x' (set x) (x' ` set x)
[PROOF STEP]
using x'_def(1) bij_betw_imageI
[PROOF STATE]
proof (prove)
using this:
inj_on x' (set x)
\<lbrakk>inj_on ?f ?A; ?f ` ?A = ?B\<rbrakk> \<Longrightarrow> bij_betw ?f ?A ?B

goal (1 subgoal):
 1. bij_betw x' (set x) (x' ` set x)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij_betw x' (set x) (x' ` set x)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
bij_betw x' (set x) (x' ` set x)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
have "bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)
[PROOF STEP]
using bij_betw_the_inv_into[OF bij_betw_imageI] y'_def(1)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>inj_on ?f ?A; ?f ` ?A = ?B\<rbrakk> \<Longrightarrow> bij_betw (the_inv_into ?A ?f) ?B ?A
inj_on y' (set y)

goal (1 subgoal):
 1. bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
hence "bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)"
[PROOF STATE]
proof (prove)
using this:
bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)

goal (1 subgoal):
 1. bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)
[PROOF STEP]
using f
[PROOF STATE]
proof (prove)
using this:
bij_betw (the_inv_into (set y) y') (y' ` set y) (set y)
x' ` set x = y' ` set y

goal (1 subgoal):
 1. bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
bij_betw x' (set x) (x' ` set x)
bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)
[PROOF STEP]
have "bij_betw f (set x) (set y)"
[PROOF STATE]
proof (prove)
using this:
bij_betw x' (set x) (x' ` set x)
bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)

goal (1 subgoal):
 1. bij_betw f (set x) (set y)
[PROOF STEP]
using bij_betw_trans f_def
[PROOF STATE]
proof (prove)
using this:
bij_betw x' (set x) (x' ` set x)
bij_betw (the_inv_into (set y) y') (x' ` set x) (set y)
\<lbrakk>bij_betw ?f ?A ?B; bij_betw ?g ?B ?C\<rbrakk> \<Longrightarrow> bij_betw (?g \<circ> ?f) ?A ?C
f = the_inv_into (set y) y' \<circ> x'

goal (1 subgoal):
 1. bij_betw f (set x) (set y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
bij_betw f (set x) (set y)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
bij_betw f (set x) (set y)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
using g
[PROOF STATE]
proof (prove)
using this:
bij_betw f (set x) (set y)
?z \<in> set x \<Longrightarrow> count_list x ?z = count_list y (f ?z)

goal (1 subgoal):
 1. \<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>f. bij_betw f (set x) (set y) \<and> (\<forall>z\<in>set x. count_list x z = count_list y (f z))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma exec_cons:
  "s \<star> (rs # r)= (s \<star> rs) \<bullet> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s \<star> Cons r rs = (s \<star> rs) \<bullet> r
[PROOF STEP]
by simp


[STATEMENT]
lemma gfun_mem_iff: "good_fun f x e \<rho> = (\<forall> v1 v2. (v1,v2) \<in> fset f \<longrightarrow>
    (\<forall> v \<in> good v1. \<exists> v'. (x,v)#\<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
proof (induction f arbitrary: x e \<rho>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x e \<rho>. good_fun {||} x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset {||} \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
 2. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x e \<rho>. good_fun {||} x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset {||} \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
 2. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
interpret ge: comp_fun_commute "(good_entry x e \<rho>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_commute (good_entry x e \<rho>)
[PROOF STEP]
unfolding comp_fun_commute_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y x. good_entry x e \<rho> y \<circ> good_entry x e \<rho> x = good_entry x e \<rho> x \<circ> good_entry x e \<rho> y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x e \<rho>. good_fun {||} x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset {||} \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
 2. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
from empty
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_fun {||} x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset {||} \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
using good_fun_def2
[PROOF STATE]
proof (prove)
using this:
good_fun ?f ?x ?e ?\<rho> = ffold (good_entry ?x ?e ?\<rho> \<circ> good_prod) True ?f

goal (1 subgoal):
 1. good_fun {||} x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset {||} \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
good_fun {||} x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset {||} \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))

goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
case (insert p f)
[PROOF STATE]
proof (state)
this:
p |\<notin>| f
good_fun f ?x ?e ?\<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (?x, v) # ?\<rho> \<turnstile> ?e \<Down> v' \<and> v' \<in> good v2))

goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
interpret ge: comp_fun_commute "(good_entry x e \<rho>) \<circ> good_prod"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. comp_fun_commute (good_entry x e \<rho> \<circ> good_prod)
[PROOF STEP]
unfolding comp_fun_commute_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>y x. (good_entry x e \<rho> \<circ> good_prod) y \<circ> (good_entry x e \<rho> \<circ> good_prod) x = (good_entry x e \<rho> \<circ> good_prod) x \<circ> (good_entry x e \<rho> \<circ> good_prod) y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
have "good_fun (finsert p f) x e \<rho>
         = ffold ((good_entry x e \<rho>) \<circ> good_prod) True (finsert p f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_fun (finsert p f) x e \<rho> = ffold (good_entry x e \<rho> \<circ> good_prod) True (finsert p f)
[PROOF STEP]
by (simp add: good_fun_def2)
[PROOF STATE]
proof (state)
this:
good_fun (finsert p f) x e \<rho> = ffold (good_entry x e \<rho> \<circ> good_prod) True (finsert p f)

goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
good_fun (finsert p f) x e \<rho> = ffold (good_entry x e \<rho> \<circ> good_prod) True (finsert p f)

goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
from insert(1)
[PROOF STATE]
proof (chain)
picking this:
p |\<notin>| f
[PROOF STEP]
have "... = ((good_entry x e \<rho>) \<circ> good_prod) p
                  (ffold ((good_entry x e \<rho>) \<circ> good_prod) True f)"
[PROOF STATE]
proof (prove)
using this:
p |\<notin>| f

goal (1 subgoal):
 1. ffold (good_entry x e \<rho> \<circ> good_prod) True (finsert p f) = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ffold (good_entry x e \<rho> \<circ> good_prod) True (finsert p f) = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)

goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
have 1: "good_fun (finsert p f) x e \<rho>
      = ((good_entry x e \<rho>) \<circ> good_prod) p (ffold ((good_entry x e \<rho>) \<circ> good_prod) True f)"
[PROOF STATE]
proof (prove)
using this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)

goal (1 subgoal):
 1. good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)

goal (1 subgoal):
 1. \<And>x f xa e \<rho>. \<lbrakk>x |\<notin>| f; \<And>x e \<rho>. good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))\<rbrakk> \<Longrightarrow> good_fun (finsert x f) xa e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert x f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (xa, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_fun (finsert p f) x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. good_fun (finsert p f) x e \<rho> \<Longrightarrow> \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)
 2. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
assume 2: "good_fun (finsert p f) x e \<rho>"
[PROOF STATE]
proof (state)
this:
good_fun (finsert p f) x e \<rho>

goal (2 subgoals):
 1. good_fun (finsert p f) x e \<rho> \<Longrightarrow> \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)
 2. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
show "\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow>
       (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)
[PROOF STEP]
proof clarify
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v1 v2 v. \<lbrakk>(v1, v2) \<in> fset (finsert p f); v \<in> good v1\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
fix v1 v2 v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v1 v2 v. \<lbrakk>(v1, v2) \<in> fset (finsert p f); v \<in> good v1\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
assume 3: "(v1, v2) \<in> fset (finsert p f)" and 4: "v \<in> good v1"
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> fset (finsert p f)
v \<in> good v1

goal (1 subgoal):
 1. \<And>v1 v2 v. \<lbrakk>(v1, v2) \<in> fset (finsert p f); v \<in> good v1\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
from 3
[PROOF STATE]
proof (chain)
picking this:
(v1, v2) \<in> fset (finsert p f)
[PROOF STEP]
have "(v1,v2) = p \<or> (v1,v2) \<in> fset f"
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> fset (finsert p f)

goal (1 subgoal):
 1. (v1, v2) = p \<or> (v1, v2) \<in> fset f
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(v1, v2) = p \<or> (v1, v2) \<in> fset f

goal (1 subgoal):
 1. \<And>v1 v2 v. \<lbrakk>(v1, v2) \<in> fset (finsert p f); v \<in> good v1\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
from this
[PROOF STATE]
proof (chain)
picking this:
(v1, v2) = p \<or> (v1, v2) \<in> fset f
[PROOF STEP]
show "\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2"
[PROOF STATE]
proof (prove)
using this:
(v1, v2) = p \<or> (v1, v2) \<in> fset f

goal (1 subgoal):
 1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (v1, v2) = p \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
 2. (v1, v2) \<in> fset f \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
assume v12_p: "(v1,v2) = p"
[PROOF STATE]
proof (state)
this:
(v1, v2) = p

goal (2 subgoals):
 1. (v1, v2) = p \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
 2. (v1, v2) \<in> fset f \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
from 1 v12_p[THEN sym] 2 4
[PROOF STATE]
proof (chain)
picking this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
p = (v1, v2)
good_fun (finsert p f) x e \<rho>
v \<in> good v1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
p = (v1, v2)
good_fun (finsert p f) x e \<rho>
v \<in> good v1

goal (1 subgoal):
 1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2

goal (1 subgoal):
 1. (v1, v2) \<in> fset f \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (v1, v2) \<in> fset f \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
assume v12_f: "(v1,v2) \<in> fset f"
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> fset f

goal (1 subgoal):
 1. (v1, v2) \<in> fset f \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
from 1 2
[PROOF STATE]
proof (chain)
picking this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
good_fun (finsert p f) x e \<rho>
[PROOF STEP]
have 5: "good_fun f x e \<rho>"
[PROOF STATE]
proof (prove)
using this:
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
good_fun (finsert p f) x e \<rho>

goal (1 subgoal):
 1. good_fun f x e \<rho>
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>good_entry x e \<rho> (good_prod p) (ffold (good_entry x e \<rho> \<circ> good_prod) True f); good_fun (finsert p f) x e \<rho>\<rbrakk> \<Longrightarrow> good_fun f x e \<rho>
[PROOF STEP]
apply (cases "(good_prod p)")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. \<lbrakk>good_entry x e \<rho> (good_prod p) (ffold (good_entry x e \<rho> \<circ> good_prod) True f); good_fun (finsert p f) x e \<rho>; good_prod p = (a, b, c)\<rbrakk> \<Longrightarrow> good_fun f x e \<rho>
[PROOF STEP]
by (auto simp: good_fun_def2)
[PROOF STATE]
proof (state)
this:
good_fun f x e \<rho>

goal (1 subgoal):
 1. (v1, v2) \<in> fset f \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
from v12_f 5 4 insert(2)[of x e \<rho>]
[PROOF STATE]
proof (chain)
picking this:
(v1, v2) \<in> fset f
good_fun f x e \<rho>
v \<in> good v1
good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> fset f
good_fun f x e \<rho>
v \<in> good v1
good_fun f x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))

goal (1 subgoal):
 1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)

goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
assume 2: "\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow>
       (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)"
[PROOF STATE]
proof (state)
this:
\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)

goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
have 3: "good_entry x e \<rho> (good_prod p) True"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_entry x e \<rho> (good_prod p) True
[PROOF STEP]
apply (cases p)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. p = (a, b) \<Longrightarrow> good_entry x e \<rho> (good_prod p) True
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b. p = (a, b) \<Longrightarrow> \<forall>v\<in>good a. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good b
[PROOF STEP]
apply clarify
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b v. \<lbrakk>p = (a, b); v \<in> good a\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good b
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b v. \<lbrakk>p = (a, b); v \<in> good a\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good b
[PROOF STEP]
fix v1 v2 v
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b v. \<lbrakk>p = (a, b); v \<in> good a\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good b
[PROOF STEP]
assume p: "p = (v1,v2)" and v_v1: "v \<in> good v1"
[PROOF STATE]
proof (state)
this:
p = (v1, v2)
v \<in> good v1

goal (1 subgoal):
 1. \<And>a b v. \<lbrakk>p = (a, b); v \<in> good a\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good b
[PROOF STEP]
from p
[PROOF STATE]
proof (chain)
picking this:
p = (v1, v2)
[PROOF STEP]
have "(v1,v2) \<in> fset (finsert p f)"
[PROOF STATE]
proof (prove)
using this:
p = (v1, v2)

goal (1 subgoal):
 1. (v1, v2) \<in> fset (finsert p f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(v1, v2) \<in> fset (finsert p f)

goal (1 subgoal):
 1. \<And>a b v. \<lbrakk>p = (a, b); v \<in> good a\<rbrakk> \<Longrightarrow> \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good b
[PROOF STEP]
from this 2 v_v1
[PROOF STATE]
proof (chain)
picking this:
(v1, v2) \<in> fset (finsert p f)
\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)
v \<in> good v1
[PROOF STEP]
show "\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2"
[PROOF STATE]
proof (prove)
using this:
(v1, v2) \<in> fset (finsert p f)
\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)
v \<in> good v1

goal (1 subgoal):
 1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
good_entry x e \<rho> (good_prod p) True

goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
from insert(2) 2
[PROOF STATE]
proof (chain)
picking this:
good_fun f ?x ?e ?\<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (?x, v) # ?\<rho> \<turnstile> ?e \<Down> v' \<and> v' \<in> good v2))
\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)
[PROOF STEP]
have 4: "good_fun f x e \<rho>"
[PROOF STATE]
proof (prove)
using this:
good_fun f ?x ?e ?\<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset f \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (?x, v) # ?\<rho> \<turnstile> ?e \<Down> v' \<and> v' \<in> good v2))
\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2)

goal (1 subgoal):
 1. good_fun f x e \<rho>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
good_fun f x e \<rho>

goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
have "(good_entry x e \<rho> \<circ> good_prod) p
     (ffold (good_entry x e \<rho> \<circ> good_prod) True f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. good_entry x e \<rho> (good_prod p) (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
apply (cases "good_prod p")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. good_prod p = (a, b, c) \<Longrightarrow> good_entry x e \<rho> (good_prod p) (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
apply (rename_tac a b c)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c. good_prod p = (a, b, c) \<Longrightarrow> good_entry x e \<rho> (good_prod p) (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
apply (case_tac a)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = (a, b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> good_entry x e \<rho> (good_prod p) (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> (\<forall>v\<in>ba. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> c) \<and> ffold (good_entry x e \<rho> \<circ> good_prod) True f
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> \<forall>v\<in>ba. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> c
 2. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> ffold (good_entry x e \<rho> \<circ> good_prod) True f
[PROOF STEP]
prefer 2
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> ffold (good_entry x e \<rho> \<circ> good_prod) True f
 2. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> \<forall>v\<in>ba. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> c
[PROOF STEP]
using 4 good_fun_def2
[PROOF STATE]
proof (prove)
using this:
good_fun f x e \<rho>
good_fun ?f ?x ?e ?\<rho> = ffold (good_entry ?x ?e ?\<rho> \<circ> good_prod) True ?f

goal (2 subgoals):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> ffold (good_entry x e \<rho> \<circ> good_prod) True f
 2. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> \<forall>v\<in>ba. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> c
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> \<forall>v\<in>ba. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> c
[PROOF STEP]
using 3
[PROOF STATE]
proof (prove)
using this:
good_entry x e \<rho> (good_prod p) True

goal (1 subgoal):
 1. \<And>a b c aa ba. \<lbrakk>good_prod p = ((aa, ba), b, c); a = (aa, ba)\<rbrakk> \<Longrightarrow> \<forall>v\<in>ba. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> c
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
(good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)

goal (1 subgoal):
 1. \<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2) \<Longrightarrow> good_fun (finsert p f) x e \<rho>
[PROOF STEP]
from this 1
[PROOF STATE]
proof (chain)
picking this:
(good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
[PROOF STEP]
show "good_fun (finsert p f) x e \<rho>"
[PROOF STATE]
proof (prove)
using this:
(good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
good_fun (finsert p f) x e \<rho> = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)

goal (1 subgoal):
 1. good_fun (finsert p f) x e \<rho>
[PROOF STEP]
unfolding good_fun_def
[PROOF STATE]
proof (prove)
using this:
(good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)
ffold (good_entry x e \<rho>) True (good_prod |`| finsert p f) = (good_entry x e \<rho> \<circ> good_prod) p (ffold (good_entry x e \<rho> \<circ> good_prod) True f)

goal (1 subgoal):
 1. ffold (good_entry x e \<rho>) True (good_prod |`| finsert p f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
good_fun (finsert p f) x e \<rho>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
good_fun (finsert p f) x e \<rho> = (\<forall>v1 v2. (v1, v2) \<in> fset (finsert p f) \<longrightarrow> (\<forall>v\<in>good v1. \<exists>v'. (x, v) # \<rho> \<turnstile> e \<Down> v' \<and> v' \<in> good v2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sSplice_pubActs[simp]:
  "pubActs (sSplice a s s') = pubActs s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pubActs (sSplice a s s') = pubActs s
[PROOF STEP]
unfolding sSplice_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pubActs (s\<lparr>ps := (ps s)(a := ps s' a)\<rparr>) = pubActs s
[PROOF STEP]
by simp


[STATEMENT]
lemma term_okD1: "term_ok \<Theta> t \<Longrightarrow> term_ok' (sig \<Theta>) t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok \<Theta> t \<Longrightarrow> term_ok' (sig \<Theta>) t
[PROOF STEP]
by (simp add: wt_term_def)


[STATEMENT]
lemma lm002:
  assumes "runiq R"
  shows "R \<supseteq> graph (Domain R) (toFunction R)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. graph (Domain R) (toFunction R) \<subseteq> R
[PROOF STEP]
unfolding graph_def toFunction_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {(x, R ,, x) |x. x \<in> Domain R} \<subseteq> R
[PROOF STEP]
using assms graph_def toFunction_def eval_runiq_rel
[PROOF STATE]
proof (prove)
using this:
runiq R
graph ?X ?f = {(x, ?f x) |x. x \<in> ?X}
toFunction ?R = (,,) ?R
\<lbrakk>?x \<in> Domain ?R; runiq ?R\<rbrakk> \<Longrightarrow> (?x, ?R ,, ?x) \<in> ?R

goal (1 subgoal):
 1. {(x, R ,, x) |x. x \<in> Domain R} \<subseteq> R
[PROOF STEP]
by fastforce


[STATEMENT]
lemma cardinalityOneSubset:
  assumes "card X=1" and "X \<subseteq> Y"
  shows "Union X \<in> Y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Union> X \<in> Y
[PROOF STEP]
using assms cardinalityOneTheElemIdentity
[PROOF STATE]
proof (prove)
using this:
card X = 1
X \<subseteq> Y
(card ?X = 1) = (?X = {the_elem ?X})

goal (1 subgoal):
 1. \<Union> X \<in> Y
[PROOF STEP]
by (metis cSup_singleton insert_subset)


[STATEMENT]
lemma rangeOutside:
  assumes "runiq f" "runiq (f^-1)"
  shows "Range(f outside X) = (Range f)-(f``X)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Range (f outside X) = Range f - f `` X
[PROOF STEP]
using assms lm089 lm092
[PROOF STATE]
proof (prove)
using this:
runiq f
runiq (f\<inverse>)
Range ?f - ?f `` ?X \<subseteq> Range (?f outside ?X)
\<lbrakk>runiq ?f; runiq (?f\<inverse>)\<rbrakk> \<Longrightarrow> Range (?f outside ?X) \<subseteq> Range ?f - ?f `` ?X

goal (1 subgoal):
 1. Range (f outside X) = Range f - f `` X
[PROOF STEP]
by (metis order_class.order.antisym)


[STATEMENT]
lemma (in is_tiny_functor) is_tiny_functor_op'[cat_op_intros]:
  assumes "\<AA>' = op_cat \<AA>" and "\<BB>' = op_cat \<BB>" and "\<alpha>' = \<alpha>"
  shows "op_cf \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cf \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cf \<FF> : op_cat \<AA> \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>t\<^sub>i\<^sub>n\<^sub>y\<^bsub>\<alpha>\<^esub> op_cat \<BB>
[PROOF STEP]
by (rule is_tiny_functor_op)


[STATEMENT]
lemma terminating_path_root_end_forward_finite:
  assumes "terminating_path_root_end r x e"
    shows "backward_finite_path_root e (x\<^sup>T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. backward_finite_path_root e (x\<^sup>T)
[PROOF STEP]
using assms terminating_path_root_end_connected inj_p_fun connected_root_iff2
      backward_finite_path_root_def
[PROOF STATE]
proof (prove)
using this:
terminating_path_root_end r x e
terminating_path_root_end ?r ?x ?e \<Longrightarrow> ?x ; 1 \<le> ?x\<^sup>+ ; ?e
is_inj ?x = is_p_fun (?x\<^sup>T)
point ?r \<Longrightarrow> connected_root ?r ?x = (?x\<^sup>T ; 1 \<le> ?x\<^sup>T\<^sup>+ ; ?r)
backward_finite_path_root ?r ?x \<equiv> connected_root ?r ?x \<and> is_inj ?x \<and> is_p_fun ?x \<and> point ?r

goal (1 subgoal):
 1. backward_finite_path_root e (x\<^sup>T)
[PROOF STEP]
by force


[STATEMENT]
lemma flush_step_preserves_read_tmps:
  assumes step: "(m,sb,\<O>) \<rightarrow>\<^sub>f (m',sb',\<O>')"
  assumes less_sb: "\<forall>i \<in> read_tmps sb. i < n"
  shows "\<forall>i \<in> read_tmps sb'. i < n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>read_tmps sb'. i < n
[PROOF STEP]
using step less_sb
[PROOF STATE]
proof (prove)
using this:
(m, sb, \<O>) \<rightarrow>\<^sub>f (m', sb', \<O>')
\<forall>i\<in>read_tmps sb. i < n

goal (1 subgoal):
 1. \<forall>i\<in>read_tmps sb'. i < n
[PROOF STEP]
by cases (auto simp add: read_tmps_append)


[STATEMENT]
lemma term_ok_app_eqD: "term_ok \<Theta> (s $ t) \<Longrightarrow> term_ok \<Theta> s \<and> term_ok \<Theta> t"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. term_ok \<Theta> (s $ t) \<Longrightarrow> term_ok \<Theta> s \<and> term_ok \<Theta> t
[PROOF STEP]
using term_ok'.simps(4) wt_term_def typ_of_def
[PROOF STATE]
proof (prove)
using this:
term_ok' ?\<Sigma> (?t $ ?u) = (term_ok' ?\<Sigma> ?t \<and> term_ok' ?\<Sigma> ?u)
wt_term ?\<Sigma> ?t \<equiv> wf_term ?\<Sigma> ?t \<and> (\<exists>T. \<turnstile>\<^sub>\<tau> ?t : T)
typ_of ?t \<equiv> typ_of1 [] ?t

goal (1 subgoal):
 1. term_ok \<Theta> (s $ t) \<Longrightarrow> term_ok \<Theta> s \<and> term_ok \<Theta> t
[PROOF STEP]
by (auto simp add: bind_eq_Some_conv)


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

  assumes xFreshQ: "x \<sharp> Q"

  shows "<\<nu>x>(P \<parallel> Q) \<approx> (<\<nu>x>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx> <\<nu>x>P \<parallel> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx> <\<nu>x>P \<parallel> Q
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> Q
[PROOF STEP]
have "<\<nu>x>(P \<parallel> Q) \<sim> (<\<nu>x>P) \<parallel> Q"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<sim> <\<nu>x>P \<parallel> Q
[PROOF STEP]
by(rule Strong_Late_Bisim_SC.scopeExtPar')
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<parallel> Q) \<sim> <\<nu>x>P \<parallel> Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx> <\<nu>x>P \<parallel> Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>(P \<parallel> Q) \<sim> <\<nu>x>P \<parallel> Q

goal (1 subgoal):
 1. <\<nu>x>(P \<parallel> Q) \<approx> <\<nu>x>P \<parallel> Q
[PROOF STEP]
by(rule strongBisimWeakBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<parallel> Q) \<approx> <\<nu>x>P \<parallel> Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma list_all_not_nthD:"list_all P xs \<Longrightarrow> \<not> P (xs ! n) \<Longrightarrow> length xs \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all P xs; \<not> P (xs ! n)\<rbrakk> \<Longrightarrow> length xs \<le> n
[PROOF STEP]
proof (induction xs arbitrary: n)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>n. \<lbrakk>list_all P []; \<not> P ([] ! n)\<rbrakk> \<Longrightarrow> length [] \<le> n
 2. \<And>a xs n. \<lbrakk>\<And>n. \<lbrakk>list_all P xs; \<not> P (xs ! n)\<rbrakk> \<Longrightarrow> length xs \<le> n; list_all P (a # xs); \<not> P ((a # xs) ! n)\<rbrakk> \<Longrightarrow> length (a # xs) \<le> n
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
list_all P []
\<not> P ([] ! n)

goal (2 subgoals):
 1. \<And>n. \<lbrakk>list_all P []; \<not> P ([] ! n)\<rbrakk> \<Longrightarrow> length [] \<le> n
 2. \<And>a xs n. \<lbrakk>\<And>n. \<lbrakk>list_all P xs; \<not> P (xs ! n)\<rbrakk> \<Longrightarrow> length xs \<le> n; list_all P (a # xs); \<not> P ((a # xs) ! n)\<rbrakk> \<Longrightarrow> length (a # xs) \<le> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
list_all P []
\<not> P ([] ! n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
list_all P []
\<not> P ([] ! n)

goal (1 subgoal):
 1. length [] \<le> n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
length [] \<le> n

goal (1 subgoal):
 1. \<And>a xs n. \<lbrakk>\<And>n. \<lbrakk>list_all P xs; \<not> P (xs ! n)\<rbrakk> \<Longrightarrow> length xs \<le> n; list_all P (a # xs); \<not> P ((a # xs) ! n)\<rbrakk> \<Longrightarrow> length (a # xs) \<le> n
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs n. \<lbrakk>\<And>n. \<lbrakk>list_all P xs; \<not> P (xs ! n)\<rbrakk> \<Longrightarrow> length xs \<le> n; list_all P (a # xs); \<not> P ((a # xs) ! n)\<rbrakk> \<Longrightarrow> length (a # xs) \<le> n
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>list_all P xs; \<not> P (xs ! ?n)\<rbrakk> \<Longrightarrow> length xs \<le> ?n
list_all P (x # xs)
\<not> P ((x # xs) ! n)

goal (1 subgoal):
 1. \<And>a xs n. \<lbrakk>\<And>n. \<lbrakk>list_all P xs; \<not> P (xs ! n)\<rbrakk> \<Longrightarrow> length xs \<le> n; list_all P (a # xs); \<not> P ((a # xs) ! n)\<rbrakk> \<Longrightarrow> length (a # xs) \<le> n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>list_all P xs; \<not> P (xs ! ?n)\<rbrakk> \<Longrightarrow> length xs \<le> ?n
list_all P (x # xs)
\<not> P ((x # xs) ! n)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>list_all P xs; \<not> P (xs ! ?n)\<rbrakk> \<Longrightarrow> length xs \<le> ?n
list_all P (x # xs)
\<not> P ((x # xs) ! n)

goal (1 subgoal):
 1. length (x # xs) \<le> n
[PROOF STEP]
by (cases n) simp_all
[PROOF STATE]
proof (state)
this:
length (x # xs) \<le> n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma subst_agreement: "(t \<cdot> r = t \<cdot> s) \<longleftrightarrow> (\<forall>v \<in> fv t. Var v \<cdot> r = Var v \<cdot> s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (t \<cdot> r = t \<cdot> s) = (\<forall>v\<in>fv t. Var v \<cdot> r = Var v \<cdot> s)
[PROOF STEP]
by (induct t) auto


[STATEMENT]
lemma subst_sends_fv_to_img: "fv (t \<cdot> s) \<subseteq> fv t \<union> range_vars s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (t \<cdot> s) \<subseteq> fv t \<union> range_vars s
[PROOF STEP]
proof (induction t)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. fv (Var x \<cdot> s) \<subseteq> fv (Var x) \<union> range_vars s
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fv (x2a \<cdot> s) \<subseteq> fv x2a \<union> range_vars s) \<Longrightarrow> fv (Fun x1a x2 \<cdot> s) \<subseteq> fv (Fun x1a x2) \<union> range_vars s
[PROOF STEP]
case (Var v)
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. \<And>x. fv (Var x \<cdot> s) \<subseteq> fv (Var x) \<union> range_vars s
 2. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fv (x2a \<cdot> s) \<subseteq> fv x2a \<union> range_vars s) \<Longrightarrow> fv (Fun x1a x2 \<cdot> s) \<subseteq> fv (Fun x1a x2) \<union> range_vars s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
proof (cases "Var v \<cdot> s = Var v")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. Var v \<cdot> s = Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
 2. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
Var v \<cdot> s = Var v

goal (2 subgoals):
 1. Var v \<cdot> s = Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
 2. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Var v \<cdot> s = Var v

goal (1 subgoal):
 1. fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s

goal (1 subgoal):
 1. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
Var v \<cdot> s \<noteq> Var v

goal (1 subgoal):
 1. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
hence "v \<in> subst_domain s"
[PROOF STATE]
proof (prove)
using this:
Var v \<cdot> s \<noteq> Var v

goal (1 subgoal):
 1. v \<in> subst_domain s
[PROOF STEP]
by (meson trm_subst_ident')
[PROOF STATE]
proof (state)
this:
v \<in> subst_domain s

goal (1 subgoal):
 1. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
hence "fv (Var v \<cdot> s) \<subseteq> range_vars s"
[PROOF STATE]
proof (prove)
using this:
v \<in> subst_domain s

goal (1 subgoal):
 1. fv (Var v \<cdot> s) \<subseteq> range_vars s
[PROOF STEP]
using subst_sends_dom_to_img
[PROOF STATE]
proof (prove)
using this:
v \<in> subst_domain s
?v \<in> subst_domain ?\<theta> \<Longrightarrow> fv (Var ?v \<cdot> ?\<theta>) \<subseteq> range_vars ?\<theta>

goal (1 subgoal):
 1. fv (Var v \<cdot> s) \<subseteq> range_vars s
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
fv (Var v \<cdot> s) \<subseteq> range_vars s

goal (1 subgoal):
 1. Var v \<cdot> s \<noteq> Var v \<Longrightarrow> fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fv (Var v \<cdot> s) \<subseteq> range_vars s

goal (1 subgoal):
 1. fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
fv (Var v \<cdot> s) \<subseteq> fv (Var v) \<union> range_vars s

goal (1 subgoal):
 1. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fv (x2a \<cdot> s) \<subseteq> fv x2a \<union> range_vars s) \<Longrightarrow> fv (Fun x1a x2 \<cdot> s) \<subseteq> fv (Fun x1a x2) \<union> range_vars s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fv (x2a \<cdot> s) \<subseteq> fv x2a \<union> range_vars s) \<Longrightarrow> fv (Fun x1a x2 \<cdot> s) \<subseteq> fv (Fun x1a x2) \<union> range_vars s
[PROOF STEP]
case Fun
[PROOF STATE]
proof (state)
this:
?x2a \<in> set x2_ \<Longrightarrow> fv (?x2a \<cdot> s) \<subseteq> fv ?x2a \<union> range_vars s

goal (1 subgoal):
 1. \<And>x1a x2. (\<And>x2a. x2a \<in> set x2 \<Longrightarrow> fv (x2a \<cdot> s) \<subseteq> fv x2a \<union> range_vars s) \<Longrightarrow> fv (Fun x1a x2 \<cdot> s) \<subseteq> fv (Fun x1a x2) \<union> range_vars s
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
?x2a \<in> set x2_ \<Longrightarrow> fv (?x2a \<cdot> s) \<subseteq> fv ?x2a \<union> range_vars s

goal (1 subgoal):
 1. fv (Fun x1a_ x2_ \<cdot> s) \<subseteq> fv (Fun x1a_ x2_) \<union> range_vars s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fv (Fun x1a_ x2_ \<cdot> s) \<subseteq> fv (Fun x1a_ x2_) \<union> range_vars s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nu_fusion_equal_2:
  "galois l u \<Longrightarrow> isotone h \<Longrightarrow> has_greatest_postfixpoint g \<Longrightarrow> has_greatest_postfixpoint h \<Longrightarrow> h (u (l (\<nu> h))) \<le> u (g (l (\<nu> h))) \<and> h (u (p\<nu> g)) = u (g (p\<nu> g)) \<Longrightarrow> p\<nu> h = u (p\<nu> g) \<and> \<nu> h = u (p\<nu> g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>galois l u; isotone h; has_greatest_postfixpoint g; has_greatest_postfixpoint h; h (u (l (\<nu> h))) \<le> u (g (l (\<nu> h))) \<and> h (u (p\<nu> g)) = u (g (p\<nu> g))\<rbrakk> \<Longrightarrow> p\<nu> h = u (p\<nu> g) \<and> \<nu> h = u (p\<nu> g)
[PROOF STEP]
by (metis greatest_fixpoint_char greatest_postfixpoint greatest_postfixpoint_fixpoint is_greatest_postfixpoint_def order.antisym galois_char nu_fusion_1 isotone_def)


[STATEMENT]
lemma restrict_rel_prod:
  "rel_prod (R \<upharpoonleft> I1 \<otimes> I2) (S \<upharpoonleft> I1' \<otimes> I2') = rel_prod R S \<upharpoonleft> pred_prod I1 I1' \<otimes> pred_prod I2 I2'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_prod (R \<upharpoonleft> I1 \<otimes> I2) (S \<upharpoonleft> I1' \<otimes> I2') = rel_prod R S \<upharpoonleft> pred_prod I1 I1' \<otimes> pred_prod I2 I2'
[PROOF STEP]
by(auto simp add: fun_eq_iff)


[STATEMENT]
lemma sprefix_same_imp_eq:
  assumes "sprefix xs ys" "sprefix xs' ys"
  and "length xs = length xs'"
  shows "xs = xs'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. xs = xs'
[PROOF STEP]
using assms(3,1,2)
[PROOF STATE]
proof (prove)
using this:
length xs = length xs'
sprefix xs ys
sprefix xs' ys

goal (1 subgoal):
 1. xs = xs'
[PROOF STEP]
by(induct arbitrary: ys rule: list_induct2) auto


[STATEMENT]
lemma cond_pmf_of_set:
  assumes fin: "finite A" and nonempty: "A \<inter> B \<noteq> {}"
  shows "cond_pmf (pmf_of_set A) B = pmf_of_set (A \<inter> B)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cond_pmf (pmf_of_set A) B = pmf_of_set (A \<inter> B)
[PROOF STEP]
proof(rule pmf_eqI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. pmf (cond_pmf (pmf_of_set A) B) i = pmf (pmf_of_set (A \<inter> B)) i
[PROOF STEP]
from nonempty
[PROOF STATE]
proof (chain)
picking this:
A \<inter> B \<noteq> {}
[PROOF STEP]
have A: "A \<noteq> {}"
[PROOF STATE]
proof (prove)
using this:
A \<inter> B \<noteq> {}

goal (1 subgoal):
 1. A \<noteq> {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A \<noteq> {}

goal (1 subgoal):
 1. \<And>i. pmf (cond_pmf (pmf_of_set A) B) i = pmf (pmf_of_set (A \<inter> B)) i
[PROOF STEP]
show "pmf ?lhs x = pmf ?rhs x" for x
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. pmf (cond_pmf (pmf_of_set A) B) x = pmf (pmf_of_set (A \<inter> B)) x
[PROOF STEP]
by(subst pmf_cond; clarsimp simp add: fin A nonempty measure_pmf_of_set split: split_indicator)
[PROOF STATE]
proof (state)
this:
pmf (cond_pmf (pmf_of_set A) B) ?x = pmf (pmf_of_set (A \<inter> B)) ?x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma return_option_spmf_transfer [transfer_parametric return_spmf_parametric, transfer_rule]:
  "((=) ===> cr_spmf_option) return_spmf Some"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((=) ===> ??.Misc_CryptHOL.option_to_spmf.cr_option) return_spmf Some
[PROOF STEP]
by(rule rel_funI)(simp add: cr_spmf_option_def)


[STATEMENT]
lemma equalOn_Un:  "equalOn (A \<union> B) f g = (equalOn A f g \<and> equalOn B f g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. equalOn (A \<union> B) f g = (equalOn A f g \<and> equalOn B f g)
[PROOF STEP]
by(auto simp add: equalOn_def)


[STATEMENT]
lemma HCollectE:
  assumes "a \<^bold>\<in> \<lbrace>x \<^bold>\<in> A. P x\<rbrace>" obtains "a \<^bold>\<in> A" "P a"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>a \<^bold>\<in> A; P a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<^bold>\<in> HCollect P A

goal (1 subgoal):
 1. (\<lbrakk>a \<^bold>\<in> A; P a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto


[STATEMENT]
lemma parts_Un [simp]: "parts(G \<union> H) = parts(G) \<union> parts(H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. parts (G \<union> H) = parts G \<union> parts H
[PROOF STEP]
by (intro equalityI parts_Un_subset1 parts_Un_subset2)


[STATEMENT]
lemma analz_insert_Hash [simp]:
     "analz (insert (Hash X) H) = insert (Hash X) (analz H)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. analz (insert (Hash X) H) = insert (Hash X) (analz H)
[PROOF STEP]
apply (rule analz_insert_eq_I)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. x \<in> analz (insert (Hash X) H) \<Longrightarrow> x \<in> insert (Hash X) (analz H)
[PROOF STEP]
apply (erule analz.induct, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma pw_Inf_inres[refine_pw_simps]: "inres (Inf C) r \<longleftrightarrow> (\<forall>M\<in>C. inres M r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inres (Inf C) r = (\<forall>M\<in>C. inres M r)
[PROOF STEP]
apply (unfold Inf_nres_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inres (if \<exists>x. RES x \<in> C then RES (\<Inter> {x. RES x \<in> C}) else FAILi) r = (\<forall>M\<in>C. inres M r)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x M. \<lbrakk>RES x \<in> C; \<forall>x. RES x \<in> C \<longrightarrow> r \<in> x; M \<in> C\<rbrakk> \<Longrightarrow> inres M r
 2. \<And>M. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C\<rbrakk> \<Longrightarrow> inres M r
[PROOF STEP]
apply (case_tac M)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x M. \<lbrakk>RES x \<in> C; \<forall>x. RES x \<in> C \<longrightarrow> r \<in> x; M \<in> C; M = FAIL\<rbrakk> \<Longrightarrow> inres M r
 2. \<And>x M X. \<lbrakk>RES x \<in> C; \<forall>x. RES x \<in> C \<longrightarrow> r \<in> x; M \<in> C; M = RES X\<rbrakk> \<Longrightarrow> inres M r
 3. \<And>M. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C\<rbrakk> \<Longrightarrow> inres M r
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x M X. \<lbrakk>RES x \<in> C; \<forall>x. RES x \<in> C \<longrightarrow> r \<in> x; M \<in> C; M = RES X\<rbrakk> \<Longrightarrow> inres M r
 2. \<And>M. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C\<rbrakk> \<Longrightarrow> inres M r
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C\<rbrakk> \<Longrightarrow> inres M r
[PROOF STEP]
apply (case_tac M)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>M. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C; M = FAIL\<rbrakk> \<Longrightarrow> inres M r
 2. \<And>M X. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C; M = RES X\<rbrakk> \<Longrightarrow> inres M r
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>M X. \<lbrakk>\<forall>x. RES x \<notin> C; M \<in> C; M = RES X\<rbrakk> \<Longrightarrow> inres M r
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma d_dist1: "d x \<cdot> (d y + d z) = d x \<cdot> d y + d x \<cdot> d z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d x \<cdot> (d y + d z) = d x \<cdot> d y + d x \<cdot> d z
[PROOF STEP]
by (simp add: local.c2_d local.p_prod_distl)


[STATEMENT]
lemma cat_comma_CId_vdomain[cat_comma_cs_simps]:
  assumes "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>" and "\<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<D>\<^sub>\<circ> (\<GG> \<^sub>C\<^sub>F\<down>\<^sub>C\<^sub>F \<HH>\<lparr>CId\<rparr>) = \<GG> \<^sub>C\<^sub>F\<down>\<^sub>C\<^sub>F \<HH>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<GG> \<^sub>C\<^sub>F\<down>\<^sub>C\<^sub>F \<HH>\<lparr>CId\<rparr>) = \<GG> \<^sub>C\<^sub>F\<down>\<^sub>C\<^sub>F \<HH>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding cat_comma_components'[OF assms(1,2)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>A\<in>\<^sub>\<circ>cat_comma_Obj \<GG> \<HH>. [A, A, [\<AA>\<lparr>CId\<rparr>\<lparr>A\<lparr>[]\<^sub>\<circ>\<rparr>\<rparr>, \<BB>\<lparr>CId\<rparr>\<lparr>A\<lparr>1\<^sub>\<nat>\<rparr>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>) = cat_comma_Obj \<GG> \<HH>
[PROOF STEP]
by simp


[STATEMENT]
lemma cf_comma_proj_right_is_functor'[cat_comma_cs_intros]:
  assumes "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<AA>' = \<GG> \<^sub>C\<^sub>F\<down>\<^sub>C\<^sub>F \<HH>"
  shows "\<GG> \<Sqinter>\<^sub>C\<^sub>F \<HH> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<Sqinter>\<^sub>C\<^sub>F \<HH> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<GG> \<Sqinter>\<^sub>C\<^sub>F \<HH> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
unfolding assms(3)
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<GG> \<Sqinter>\<^sub>C\<^sub>F \<HH> : \<GG> \<^sub>C\<^sub>F\<down>\<^sub>C\<^sub>F \<HH> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule cf_comma_proj_right_is_functor)


[STATEMENT]
lemma dlex_pm_lin: "dlex_pm s t \<or> dlex_pm t s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dlex_pm s t \<or> dlex_pm t s
[PROOF STEP]
unfolding dlex_pm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dord_pm lex_pm s t \<or> dord_pm lex_pm t s
[PROOF STEP]
using lex_pm_lin
[PROOF STATE]
proof (prove)
using this:
lex_pm ?s ?t \<or> lex_pm ?t ?s

goal (1 subgoal):
 1. dord_pm lex_pm s t \<or> dord_pm lex_pm t s
[PROOF STEP]
by (rule dord_pm_lin)


[STATEMENT]
lemma ladder_last_n_of_cut:
  assumes L_non_empty: "L \<noteq> []"
  shows "ladder_last_n (ladder_cut L n) = n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_last_n (ladder_cut L n) = n
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ladder_last_n (ladder_cut L n) = n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_last_n (ladder_cut L n) = n
[PROOF STEP]
apply (simp add: ladder_last_n_def length_ladder_cut[OF L_non_empty])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ladder_n (ladder_cut L n) (length L - Suc 0) = n
[PROOF STEP]
apply (simp add: ladder_n_def ladder_cut_def deriv_n_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst ((let i = length L - Suc 0 in L[i := (n, snd (L ! i))]) ! (length L - Suc 0)) = n
[PROOF STEP]
by (metis assms diff_Suc_less fst_conv length_greater_0_conv nth_list_update_eq)
[PROOF STATE]
proof (state)
this:
ladder_last_n (ladder_cut L n) = n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma arr_mkIde [iff]:
    shows "arr (mkIde A) \<longleftrightarrow> setp A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. arr (mkIde A) = setp A
[PROOF STEP]
using not_arr_null mkIde_def ide_mkIde
[PROOF STATE]
proof (prove)
using this:
\<not> arr null
mkIde ?A = (if setp ?A then inv_into (Collect ide) local.set ?A else null)
setp ?A \<Longrightarrow> ide (mkIde ?A)

goal (1 subgoal):
 1. arr (mkIde A) = setp A
[PROOF STEP]
by auto


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

  assumes "x \<sharp> P"

  shows "<\<nu>x>(P \<oplus> Q) \<sim>\<^sub>e P \<oplus> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<sim>\<^sub>e P \<oplus> <\<nu>x>Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<sim>\<^sub>e P \<oplus> <\<nu>x>Q
[PROOF STEP]
from \<open>x \<sharp> P\<close>
[PROOF STATE]
proof (chain)
picking this:
x \<sharp> P
[PROOF STEP]
have "<\<nu>x>(P \<oplus> Q) \<sim>\<^sub>l P \<oplus> <\<nu>x>Q"
[PROOF STATE]
proof (prove)
using this:
x \<sharp> P

goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<sim>\<^sub>l P \<oplus> <\<nu>x>Q
[PROOF STEP]
by(rule Strong_Late_Bisim_SC.scopeExtSum)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<oplus> Q) \<sim>\<^sub>l P \<oplus> <\<nu>x>Q

goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<sim>\<^sub>e P \<oplus> <\<nu>x>Q
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
<\<nu>x>(P \<oplus> Q) \<sim>\<^sub>l P \<oplus> <\<nu>x>Q

goal (1 subgoal):
 1. <\<nu>x>(P \<oplus> Q) \<sim>\<^sub>e P \<oplus> <\<nu>x>Q
[PROOF STEP]
by(rule lateEarlyBisim)
[PROOF STATE]
proof (state)
this:
<\<nu>x>(P \<oplus> Q) \<sim>\<^sub>e P \<oplus> <\<nu>x>Q

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x9:
  assumes "(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')"
      and "expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)"
      and "decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)"
      and "msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))"
    shows "gas s'c < gas st \<or> gas s'c = gas st"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))
[PROOF STEP]
have "gas s'c = gas s'a"
[PROOF STATE]
proof (prove)
using this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))

goal (1 subgoal):
 1. gas s'c = gas s'a
[PROOF STEP]
using decl_gas_address[of id0 tp "(Some (aa, b))" False cd vb cd e\<^sub>v s'a]
[PROOF STATE]
proof (prove)
using this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((?l1', ?t1'), ?st1') \<Longrightarrow> gas ?st1' = gas s'a \<and> address e\<^sub>v = address ?t1' \<and> sender e\<^sub>v = sender ?t1' \<and> svalue e\<^sub>v = svalue ?t1'

goal (1 subgoal):
 1. gas s'c = gas s'a
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gas s'c = gas s'a

goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gas s'c = gas s'a

goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))
[PROOF STEP]
have "\<dots> \<le> gas s'"
[PROOF STATE]
proof (prove)
using this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))

goal (1 subgoal):
 1. gas s'a \<le> gas s'
[PROOF STEP]
using msel_ssel_lexp_expr_load_rexp_stmt_dom_gas(4)[of a e\<^sub>p e\<^sub>v cd s']
[PROOF STATE]
proof (prove)
using this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
expr a e\<^sub>p e\<^sub>v cd s' = Normal ((aa, b), s'a)
decl id0 tp (Some (aa, b)) False cd vb cd e\<^sub>v s'a = Normal ((ab, ba), s'c)
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s'))))
msel_ssel_lexp_expr_load_rexp_stmt_dom (Inr (Inl (Inl (a, e\<^sub>p, e\<^sub>v, cd, s')))) \<Longrightarrow> \<forall>st4' v4 t4. expr a e\<^sub>p e\<^sub>v cd s' = Normal ((v4, t4), st4') \<longrightarrow> gas st4' \<le> gas s'

goal (1 subgoal):
 1. gas s'a \<le> gas s'
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gas s'a \<le> gas s'

goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
gas s'a \<le> gas s'

goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')
[PROOF STEP]
have "\<dots> \<le> gas st"
[PROOF STATE]
proof (prove)
using this:
(if gas st \<le> costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st then throw Gas st else (get \<bind> (\<lambda>sa. put (sa\<lparr>gas := gas sa - costs (BLOCK ((id0, tp), Some a) s) e\<^sub>p e\<^sub>v cd st\<rparr>))) st) = Normal ((), s')

goal (1 subgoal):
 1. gas s' \<le> gas st
[PROOF STEP]
by (auto split:if_split_asm)
[PROOF STATE]
proof (state)
this:
gas s' \<le> gas st

goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
gas s'c \<le> gas st
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gas s'c \<le> gas st

goal (1 subgoal):
 1. gas s'c < gas st \<or> gas s'c = gas st
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
gas s'c < gas st \<or> gas s'c = gas st

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lcp_roots_lcp: assumes "x \<cdot> y \<noteq> y \<cdot> x" shows "x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
obtain k where "\<rho> x\<^sup>@Suc k = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>k. \<rho> x \<^sup>@ Suc k = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms primroot_expE
[PROOF STATE]
proof (prove)
using this:
x \<cdot> y \<noteq> y \<cdot> x
\<lbrakk>?x \<noteq> \<epsilon>; \<And>k. \<rho> ?x \<^sup>@ Suc k = ?x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>k. \<rho> x \<^sup>@ Suc k = x \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<rho> x \<^sup>@ Suc k = x

goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
obtain m where "\<rho> y\<^sup>@Suc m = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. \<rho> y \<^sup>@ Suc m = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms primroot_expE
[PROOF STATE]
proof (prove)
using this:
x \<cdot> y \<noteq> y \<cdot> x
\<lbrakk>?x \<noteq> \<epsilon>; \<And>k. \<rho> ?x \<^sup>@ Suc k = ?x \<Longrightarrow> ?thesis\<rbrakk> \<Longrightarrow> ?thesis

goal (1 subgoal):
 1. (\<And>m. \<rho> y \<^sup>@ Suc m = y \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<rho> y \<^sup>@ Suc m = y

goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
have "\<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x
[PROOF STEP]
using assms comp_primroot_conv'
[PROOF STATE]
proof (prove)
using this:
x \<cdot> y \<noteq> y \<cdot> x
\<lbrakk>?u \<noteq> \<epsilon>; ?v \<noteq> \<epsilon>\<rbrakk> \<Longrightarrow> (?u \<cdot> ?v = ?v \<cdot> ?u) = (\<rho> ?u \<cdot> \<rho> ?v = \<rho> ?v \<cdot> \<rho> ?u)

goal (1 subgoal):
 1. \<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x

goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x
[PROOF STEP]
interpret binary_code "\<rho> x" "\<rho> y"
[PROOF STATE]
proof (prove)
using this:
\<rho> x \<cdot> \<rho> y \<noteq> \<rho> y \<cdot> \<rho> x

goal (1 subgoal):
 1. binary_code (\<rho> x) (\<rho> y)
[PROOF STEP]
by unfold_locales
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
from bin_lcp_pows_lcp[of k m, unfolded \<open>\<rho> y\<^sup>@Suc m = y\<close> \<open>\<rho> x\<^sup>@Suc k = x\<close>]
[PROOF STATE]
proof (chain)
picking this:
x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x

goal (1 subgoal):
 1. x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
x \<cdot> y \<and>\<^sub>p y \<cdot> x = \<rho> x \<cdot> \<rho> y \<and>\<^sub>p \<rho> y \<cdot> \<rho> x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gen_drop_exp: assumes "p \<in> \<langle>{u,v\<^sup>@(Suc k)}\<rangle>" shows "p \<in> \<langle>{u,v}\<rangle>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<in> \<langle>{u, v}\<rangle>
[PROOF STEP]
by (rule hull.induct[OF assms], simp, blast)


[STATEMENT]
lemma eqd_exchange:
  assumes "u \<cdot> v = x \<cdot> y" and "u \<cdot> v' = x \<cdot> y'" and "u' \<cdot> v = x' \<cdot> y"
  shows "u' \<cdot> v' = x' \<cdot> y'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. u' \<cdot> v' = x' \<cdot> y'
[PROOF STEP]
using eqd_exchange_aux[OF assms]  eqd_exchange_aux[OF assms[symmetric], symmetric]
[PROOF STATE]
proof (prove)
using this:
\<^bold>|u\<^bold>| \<le> \<^bold>|x\<^bold>| \<Longrightarrow> u' \<cdot> v' = x' \<cdot> y'
\<^bold>|x\<^bold>| \<le> \<^bold>|u\<^bold>| \<Longrightarrow> u' \<cdot> v' = x' \<cdot> y'

goal (1 subgoal):
 1. u' \<cdot> v' = x' \<cdot> y'
[PROOF STEP]
by force


[STATEMENT]
lemma NF_anti_mono:
  assumes "A \<subseteq> B" shows "NF B \<subseteq> NF A"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. NF B \<subseteq> NF A
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A \<subseteq> B

goal (1 subgoal):
 1. NF B \<subseteq> NF A
[PROOF STEP]
by auto


[STATEMENT]
lemma meet_imp_conversion: "r\<^sup>\<up> \<subseteq> r\<^sup>\<leftrightarrow>\<^sup>*"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r\<^sup>\<up> \<subseteq> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
proof (rule subrelI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> r\<^sup>\<up> \<Longrightarrow> (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
fix y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> r\<^sup>\<up> \<Longrightarrow> (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
assume "(y, z) \<in> r\<^sup>\<up>"
[PROOF STATE]
proof (state)
this:
(y, z) \<in> r\<^sup>\<up>

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> r\<^sup>\<up> \<Longrightarrow> (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(y, z) \<in> r\<^sup>\<up>
[PROOF STEP]
obtain x where "(x, y) \<in> r\<^sup>*" and "(x, z) \<in> r\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(y, z) \<in> r\<^sup>\<up>

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>(x, y) \<in> r\<^sup>*; (x, z) \<in> r\<^sup>*\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r\<^sup>*
(x, z) \<in> r\<^sup>*

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> r\<^sup>\<up> \<Longrightarrow> (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r\<^sup>*
(x, z) \<in> r\<^sup>*
[PROOF STEP]
have "(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*" and "(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r\<^sup>*
(x, z) \<in> r\<^sup>*

goal (1 subgoal):
 1. (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>* &&& (x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> r\<^sup>\<up> \<Longrightarrow> (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
from \<open>(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
have "(y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*

goal (1 subgoal):
 1. (y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
using conversion_sym
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
sym (?A\<^sup>\<leftrightarrow>\<^sup>*)

goal (1 subgoal):
 1. (y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
unfolding sym_def
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
\<forall>x y. (x, y) \<in> ?A\<^sup>\<leftrightarrow>\<^sup>* \<longrightarrow> (y, x) \<in> ?A\<^sup>\<leftrightarrow>\<^sup>*

goal (1 subgoal):
 1. (y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
by best
[PROOF STATE]
proof (state)
this:
(y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*

goal (1 subgoal):
 1. \<And>x y. (x, y) \<in> r\<^sup>\<up> \<Longrightarrow> (x, y) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
with \<open>(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*\<close>
[PROOF STATE]
proof (chain)
picking this:
(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
(y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
show "(y, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*"
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
(y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*

goal (1 subgoal):
 1. (y, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
using conversion_trans
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
(y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
trans (?A\<^sup>\<leftrightarrow>\<^sup>*)

goal (1 subgoal):
 1. (y, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
unfolding trans_def
[PROOF STATE]
proof (prove)
using this:
(x, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
(y, x) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
\<forall>x y z. (x, y) \<in> ?A\<^sup>\<leftrightarrow>\<^sup>* \<longrightarrow> (y, z) \<in> ?A\<^sup>\<leftrightarrow>\<^sup>* \<longrightarrow> (x, z) \<in> ?A\<^sup>\<leftrightarrow>\<^sup>*

goal (1 subgoal):
 1. (y, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*
[PROOF STEP]
by best
[PROOF STATE]
proof (state)
this:
(y, z) \<in> r\<^sup>\<leftrightarrow>\<^sup>*

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma fold_A_facet_im: "fold_A ` z = z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fold_A ` z = z
[PROOF STEP]
using facet_in_chambers(1) fixespointwise_im[OF fold_A_fixespointwise1]
[PROOF STATE]
proof (prove)
using this:
z \<subseteq> C
?B \<subseteq> C \<Longrightarrow> fold_A ` ?B = ?B

goal (1 subgoal):
 1. fold_A ` z = z
[PROOF STEP]
by simp


[STATEMENT]
lemma prefixes_set_Nil : "[] \<in> list.set (prefixes xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [] \<in> set (prefixes xs)
[PROOF STEP]
by (metis append.left_neutral list.set_intros(1) prefixes.simps(1) prefixes_set_subset subset_iff)


[STATEMENT]
lemma non_sym_dist_pairs'_elems_distinct:
  assumes "distinct xs"
  and     "(x,y) \<in> set (non_sym_dist_pairs' xs)"
shows "x \<in> set xs"
and   "y \<in> set xs"
and   "x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs &&& y \<in> set xs &&& x \<noteq> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. x \<in> set xs
 2. y \<in> set xs
 3. x \<noteq> y
[PROOF STEP]
show "x \<in> set xs" and "y \<in> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> set xs &&& y \<in> set xs
[PROOF STEP]
using non_sym_dist_pairs_subset assms(2)
[PROOF STATE]
proof (prove)
using this:
set (non_sym_dist_pairs ?xs) \<subseteq> set ?xs \<times> set ?xs
(x, y) \<in> set (non_sym_dist_pairs' xs)

goal (1 subgoal):
 1. x \<in> set xs &&& y \<in> set xs
[PROOF STEP]
by (induction xs; auto)+
[PROOF STATE]
proof (state)
this:
x \<in> set xs
y \<in> set xs

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
show "x \<noteq> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
distinct xs
(x, y) \<in> set (non_sym_dist_pairs' xs)

goal (1 subgoal):
 1. x \<noteq> y
[PROOF STEP]
by (induction xs; auto)
[PROOF STATE]
proof (state)
this:
x \<noteq> y

goal:
No subgoals!
[PROOF STEP]
qed