[STATEMENT]
lemma max_length_elem :
  fixes xs :: "'a list set"
  assumes "finite xs"
  and     "xs \<noteq> {}"
shows "\<exists> x \<in> xs . \<not>(\<exists> y \<in> xs . length y > length x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>xs. \<not> (\<exists>y\<in>xs. length x < length y)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
finite xs
xs \<noteq> {}

goal (1 subgoal):
 1. \<exists>x\<in>xs. \<not> (\<exists>y\<in>xs. length x < length y)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. {} \<noteq> {} \<Longrightarrow> \<exists>x\<in>{}. \<not> (\<exists>y\<in>{}. length x < length y)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
case empty
[PROOF STATE]
proof (state)
this:
{} \<noteq> {}

goal (2 subgoals):
 1. {} \<noteq> {} \<Longrightarrow> \<exists>x\<in>{}. \<not> (\<exists>y\<in>{}. length x < length y)
 2. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{} \<noteq> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
{} \<noteq> {}

goal (1 subgoal):
 1. \<exists>x\<in>{}. \<not> (\<exists>y\<in>{}. length x < length y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<in>{}. \<not> (\<exists>y\<in>{}. length x < length y)

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
case (insert x F)
[PROOF STATE]
proof (state)
this:
finite F
x \<notin> F
F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y)
insert x F \<noteq> {}

goal (1 subgoal):
 1. \<And>x F. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
finite F
x \<notin> F
F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y)
insert x F \<noteq> {}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
finite F
x \<notin> F
F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y)
insert x F \<noteq> {}

goal (1 subgoal):
 1. \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
proof (cases "F = {}")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F = {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
 2. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
F = {}

goal (2 subgoals):
 1. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F = {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
 2. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
F = {}

goal (1 subgoal):
 1. \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)

goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
F \<noteq> {}

goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
F \<noteq> {}
[PROOF STEP]
obtain y where "y \<in> F" and "\<not>(\<exists> y' \<in> F . length y' > length y)"
[PROOF STATE]
proof (prove)
using this:
F \<noteq> {}

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> F; \<not> (\<exists>y'\<in>F. length y < length y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using insert.IH
[PROOF STATE]
proof (prove)
using this:
F \<noteq> {}
F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y)

goal (1 subgoal):
 1. (\<And>y. \<lbrakk>y \<in> F; \<not> (\<exists>y'\<in>F. length y < length y')\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y \<in> F
\<not> (\<exists>y'\<in>F. length y < length y')

goal (1 subgoal):
 1. \<lbrakk>finite F; x \<notin> F; F \<noteq> {} \<Longrightarrow> \<exists>x\<in>F. \<not> (\<exists>y\<in>F. length x < length y); insert x F \<noteq> {}; F \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
y \<in> F
\<not> (\<exists>y'\<in>F. length y < length y')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
y \<in> F
\<not> (\<exists>y'\<in>F. length y < length y')

goal (1 subgoal):
 1. \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
using dual_order.strict_trans
[PROOF STATE]
proof (prove)
using this:
y \<in> F
\<not> (\<exists>y'\<in>F. length y < length y')
\<lbrakk>?b < ?a; ?c < ?b\<rbrakk> \<Longrightarrow> ?c < ?a

goal (1 subgoal):
 1. \<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)
[PROOF STEP]
by (cases "length x > length y"; auto)
[PROOF STATE]
proof (state)
this:
\<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>xa\<in>insert x F. \<not> (\<exists>y\<in>insert x F. length xa < length y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma corder_intro: "class.linorder le lt \<Longrightarrow> a = Some (le, lt)\<Longrightarrow> a = Some (le',lt') \<Longrightarrow>
  class.linorder le' lt'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>class.linorder le lt; a = Some (le, lt); a = Some (le', lt')\<rbrakk> \<Longrightarrow> class.linorder le' lt'
[PROOF STEP]
by auto


[STATEMENT]
lemma natural_isomorphism_\<alpha>:
    shows "natural_isomorphism VVV.comp V HoHV HoVH
             (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
interpret \<alpha>: transformation_by_components VVV.comp V HoHV HoVH
                     \<open>\<lambda>f. \<a>[fst f, fst (snd f), snd (snd f)]\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transformation_by_components VVV.comp (\<cdot>) HoHV HoVH (\<lambda>f. \<a>[fst f, fst (snd f), snd (snd f)])
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>a. VVV.ide a \<Longrightarrow> \<guillemotleft>\<a>[fst a, fst (snd a), snd (snd a)] : HoHV a \<Rightarrow> HoVH a\<guillemotright>
 2. \<And>f. VVV.arr f \<Longrightarrow> \<a>[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] \<cdot> HoHV f = HoVH f \<cdot> \<a>[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]
[PROOF STEP]
show 1: "\<And>x. VVV.ide x \<Longrightarrow> \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x. VVV.ide x \<Longrightarrow> \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. VVV.ide x \<Longrightarrow> \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. VVV.ide x \<Longrightarrow> \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
assume x: "VVV.ide x"
[PROOF STATE]
proof (state)
this:
VVV.ide x

goal (1 subgoal):
 1. \<And>x. VVV.ide x \<Longrightarrow> \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
show "\<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
have "ide (fst x) \<and> ide (fst (snd x)) \<and> ide (snd (snd x)) \<and>
                  fst x \<star> fst (snd x) \<noteq> null \<and> fst (snd x) \<star> snd (snd x) \<noteq> null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ide (fst x) \<and> ide (fst (snd x)) \<and> ide (snd (snd x)) \<and> fst x \<star> fst (snd x) \<noteq> null \<and> fst (snd x) \<star> snd (snd x) \<noteq> null
[PROOF STEP]
using x VVV.ide_char\<^sub>S\<^sub>b\<^sub>C VVV.arr_char\<^sub>S\<^sub>b\<^sub>C VV.arr_char\<^sub>S\<^sub>b\<^sub>C composable_char\<^sub>P\<^sub>B\<^sub>H
[PROOF STATE]
proof (prove)
using this:
VVV.ide x
VVV.ide ?a = (VVV.arr ?a \<and> VxVxV.ide ?a)
VVV.arr ?f = (arr (fst ?f) \<and> VV.arr (snd ?f) \<and> src (fst ?f) = trg (fst (snd ?f)))
VV.arr ?f = (arr (fst ?f) \<and> arr (snd ?f) \<and> src (fst ?f) = trg (snd ?f))
(?\<nu> \<star> ?\<mu> \<noteq> null) = (arr ?\<mu> \<and> arr ?\<nu> \<and> src ?\<nu> = trg ?\<mu>)

goal (1 subgoal):
 1. ide (fst x) \<and> ide (fst (snd x)) \<and> ide (snd (snd x)) \<and> fst x \<star> fst (snd x) \<noteq> null \<and> fst (snd x) \<star> snd (snd x) \<noteq> null
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
ide (fst x) \<and> ide (fst (snd x)) \<and> ide (snd (snd x)) \<and> fst x \<star> fst (snd x) \<noteq> null \<and> fst (snd x) \<star> snd (snd x) \<noteq> null

goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
hence "\<a>[fst x, fst (snd x), snd (snd x)]
                     \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x))
                             (fst x \<star> fst (snd x) \<star> snd (snd x))"
[PROOF STATE]
proof (prove)
using this:
ide (fst x) \<and> ide (fst (snd x)) \<and> ide (snd (snd x)) \<and> fst x \<star> fst (snd x) \<noteq> null \<and> fst (snd x) \<star> snd (snd x) \<noteq> null

goal (1 subgoal):
 1. \<a>[fst x, fst (snd x), snd (snd x)] \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x)) (fst x \<star> fst (snd x) \<star> snd (snd x))
[PROOF STEP]
using x assoc_in_hom\<^sub>A\<^sub>W\<^sub>C
[PROOF STATE]
proof (prove)
using this:
ide (fst x) \<and> ide (fst (snd x)) \<and> ide (snd (snd x)) \<and> fst x \<star> fst (snd x) \<noteq> null \<and> fst (snd x) \<star> snd (snd x) \<noteq> null
VVV.ide x
\<lbrakk>ide ?f; ide ?g; ide ?h; ?f \<star> ?g \<noteq> null; ?g \<star> ?h \<noteq> null\<rbrakk> \<Longrightarrow> sources \<a>[?f, ?g, ?h] = sources ?h
\<lbrakk>ide ?f; ide ?g; ide ?h; ?f \<star> ?g \<noteq> null; ?g \<star> ?h \<noteq> null\<rbrakk> \<Longrightarrow> targets \<a>[?f, ?g, ?h] = targets ?f
\<lbrakk>ide ?f; ide ?g; ide ?h; ?f \<star> ?g \<noteq> null; ?g \<star> ?h \<noteq> null\<rbrakk> \<Longrightarrow> \<guillemotleft>\<a>[?f, ?g, ?h] : (?f \<star> ?g) \<star> ?h \<Rightarrow> ?f \<star> ?g \<star> ?h\<guillemotright>

goal (1 subgoal):
 1. \<a>[fst x, fst (snd x), snd (snd x)] \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x)) (fst x \<star> fst (snd x) \<star> snd (snd x))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<a>[fst x, fst (snd x), snd (snd x)] \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x)) (fst x \<star> fst (snd x) \<star> snd (snd x))

goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
\<a>[fst x, fst (snd x), snd (snd x)] \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x)) (fst x \<star> fst (snd x) \<star> snd (snd x))

goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>
[PROOF STEP]
unfolding HoHV_def HoVH_def
[PROOF STATE]
proof (prove)
using this:
\<a>[fst x, fst (snd x), snd (snd x)] \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x)) (fst x \<star> fst (snd x) \<star> snd (snd x))

goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : if VVV.arr x then (fst x \<star> fst (snd x)) \<star> snd (snd x) else null \<Rightarrow> if VVV.arr x then fst x \<star> fst (snd x) \<star> snd (snd x) else null\<guillemotright>
[PROOF STEP]
using x VVV.ideD(1)
[PROOF STATE]
proof (prove)
using this:
\<a>[fst x, fst (snd x), snd (snd x)] \<in> hom ((fst x \<star> fst (snd x)) \<star> snd (snd x)) (fst x \<star> fst (snd x) \<star> snd (snd x))
VVV.ide x
VVV.ide ?a \<Longrightarrow> VVV.arr ?a

goal (1 subgoal):
 1. \<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : if VVV.arr x then (fst x \<star> fst (snd x)) \<star> snd (snd x) else null \<Rightarrow> if VVV.arr x then fst x \<star> fst (snd x) \<star> snd (snd x) else null\<guillemotright>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<guillemotleft>\<a>[fst x, fst (snd x), snd (snd x)] : HoHV x \<Rightarrow> HoVH x\<guillemotright>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
VVV.ide ?x \<Longrightarrow> \<guillemotleft>\<a>[fst ?x, fst (snd ?x), snd (snd ?x)] : HoHV ?x \<Rightarrow> HoVH ?x\<guillemotright>

goal (1 subgoal):
 1. \<And>f. VVV.arr f \<Longrightarrow> \<a>[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] \<cdot> HoHV f = HoVH f \<cdot> \<a>[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]
[PROOF STEP]
show "\<And>f. VVV.arr f \<Longrightarrow>
                   \<a>[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] \<cdot> HoHV f =
                   HoVH f \<cdot> \<a>[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. VVV.arr f \<Longrightarrow> \<a>[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] \<cdot> HoHV f = HoVH f \<cdot> \<a>[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]
[PROOF STEP]
unfolding HoHV_def HoVH_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>f. VVV.arr f \<Longrightarrow> \<a>[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] \<cdot> (if VVV.arr f then (fst f \<star> fst (snd f)) \<star> snd (snd f) else null) = (if VVV.arr f then fst f \<star> fst (snd f) \<star> snd (snd f) else null) \<cdot> \<a>[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]
[PROOF STEP]
using assoc_naturality\<^sub>A\<^sub>W\<^sub>C VVV.arr_char\<^sub>S\<^sub>b\<^sub>C VV.arr_char\<^sub>S\<^sub>b\<^sub>C VVV.dom_char\<^sub>S\<^sub>b\<^sub>C VVV.cod_char\<^sub>S\<^sub>b\<^sub>C
                composable_char\<^sub>P\<^sub>B\<^sub>H
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<tau> \<star> ?\<mu> \<noteq> null; ?\<mu> \<star> ?\<nu> \<noteq> null\<rbrakk> \<Longrightarrow> \<a>[cod ?\<tau>, cod ?\<mu>, cod ?\<nu>] \<cdot> ((?\<tau> \<star> ?\<mu>) \<star> ?\<nu>) = (?\<tau> \<star> ?\<mu> \<star> ?\<nu>) \<cdot> \<a>[local.dom ?\<tau>, local.dom ?\<mu>, local.dom ?\<nu>]
VVV.arr ?f = (arr (fst ?f) \<and> VV.arr (snd ?f) \<and> src (fst ?f) = trg (fst (snd ?f)))
VV.arr ?f = (arr (fst ?f) \<and> arr (snd ?f) \<and> src (fst ?f) = trg (snd ?f))
VVV.dom ?f = (if VVV.arr ?f then VxVxV.dom ?f else VxVxV.null)
VVV.cod ?f = (if VVV.arr ?f then VxVxV.cod ?f else VxVxV.null)
(?\<nu> \<star> ?\<mu> \<noteq> null) = (arr ?\<mu> \<and> arr ?\<nu> \<and> src ?\<nu> = trg ?\<mu>)

goal (1 subgoal):
 1. \<And>f. VVV.arr f \<Longrightarrow> \<a>[fst (VVV.cod f), fst (snd (VVV.cod f)), snd (snd (VVV.cod f))] \<cdot> (if VVV.arr f then (fst f \<star> fst (snd f)) \<star> snd (snd f) else null) = (if VVV.arr f then fst f \<star> fst (snd f) \<star> snd (snd f) else null) \<cdot> \<a>[fst (VVV.dom f), fst (snd (VVV.dom f)), snd (snd (VVV.dom f))]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
VVV.arr ?f \<Longrightarrow> \<a>[fst (VVV.cod ?f), fst (snd (VVV.cod ?f)), snd (snd (VVV.cod ?f))] \<cdot> HoHV ?f = HoVH ?f \<cdot> \<a>[fst (VVV.dom ?f), fst (snd (VVV.dom ?f)), snd (snd (VVV.dom ?f))]

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
interpret \<alpha>: natural_isomorphism VVV.comp V HoHV HoVH \<alpha>.map
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH \<alpha>.map
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. VVV.ide a \<Longrightarrow> local.iso (\<alpha>.map a)
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a. VVV.ide a \<Longrightarrow> local.iso (\<alpha>.map a)
[PROOF STEP]
assume f: "VVV.ide f"
[PROOF STATE]
proof (state)
this:
VVV.ide f

goal (1 subgoal):
 1. \<And>a. VVV.ide a \<Longrightarrow> local.iso (\<alpha>.map a)
[PROOF STEP]
show "iso (\<alpha>.map f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. local.iso (\<alpha>.map f)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. local.iso (\<alpha>.map f)
[PROOF STEP]
have "fst f \<star> fst (snd f) \<noteq> null \<and> fst (snd f) \<star> snd (snd f) \<noteq> null"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. fst f \<star> fst (snd f) \<noteq> null \<and> fst (snd f) \<star> snd (snd f) \<noteq> null
[PROOF STEP]
using f VVV.ideD(1) VVV.arr_char\<^sub>S\<^sub>b\<^sub>C [of f] VV.arr_char\<^sub>S\<^sub>b\<^sub>C composable_char\<^sub>P\<^sub>B\<^sub>H
[PROOF STATE]
proof (prove)
using this:
VVV.ide f
VVV.ide ?a \<Longrightarrow> VVV.arr ?a
VVV.arr f = (arr (fst f) \<and> VV.arr (snd f) \<and> src (fst f) = trg (fst (snd f)))
VV.arr ?f = (arr (fst ?f) \<and> arr (snd ?f) \<and> src (fst ?f) = trg (snd ?f))
(?\<nu> \<star> ?\<mu> \<noteq> null) = (arr ?\<mu> \<and> arr ?\<nu> \<and> src ?\<nu> = trg ?\<mu>)

goal (1 subgoal):
 1. fst f \<star> fst (snd f) \<noteq> null \<and> fst (snd f) \<star> snd (snd f) \<noteq> null
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
fst f \<star> fst (snd f) \<noteq> null \<and> fst (snd f) \<star> snd (snd f) \<noteq> null

goal (1 subgoal):
 1. local.iso (\<alpha>.map f)
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
fst f \<star> fst (snd f) \<noteq> null \<and> fst (snd f) \<star> snd (snd f) \<noteq> null

goal (1 subgoal):
 1. local.iso (\<alpha>.map f)
[PROOF STEP]
using f \<alpha>.map_simp_ide iso_assoc\<^sub>A\<^sub>W\<^sub>C VVV.ide_char\<^sub>S\<^sub>b\<^sub>C VVV.arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
fst f \<star> fst (snd f) \<noteq> null \<and> fst (snd f) \<star> snd (snd f) \<noteq> null
VVV.ide f
VVV.ide ?a \<Longrightarrow> \<alpha>.map ?a = \<a>[fst ?a, fst (snd ?a), snd (snd ?a)]
\<lbrakk>ide ?f; ide ?g; ide ?h; ?f \<star> ?g \<noteq> null; ?g \<star> ?h \<noteq> null\<rbrakk> \<Longrightarrow> local.iso \<a>[?f, ?g, ?h]
VVV.ide ?a = (VVV.arr ?a \<and> VxVxV.ide ?a)
VVV.arr ?f = (arr (fst ?f) \<and> VV.arr (snd ?f) \<and> src (fst ?f) = trg (fst (snd ?f)))

goal (1 subgoal):
 1. local.iso (\<alpha>.map f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
local.iso (\<alpha>.map f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
local.iso (\<alpha>.map f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
have "(\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>))) = \<alpha>.map"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>))) = \<alpha>.map
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
fix \<mu>\<nu>\<tau>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
have "\<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
using \<alpha>_def \<alpha>.map_def
[PROOF STATE]
proof (prove)
using this:
\<alpha> ?\<mu> ?\<nu> ?\<tau> \<equiv> if VVV.arr (?\<mu>, ?\<nu>, ?\<tau>) then (?\<mu> \<star> ?\<nu> \<star> ?\<tau>) \<cdot> \<a>[local.dom ?\<mu>, local.dom ?\<nu>, local.dom ?\<tau>] else null
\<alpha>.map ?f = (if VVV.arr ?f then \<a>[fst (VVV.cod ?f), fst (snd (VVV.cod ?f)), snd (snd (VVV.cod ?f))] \<cdot> HoHV ?f else null)

goal (1 subgoal):
 1. \<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. \<And>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. \<And>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
have "VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow>
                         \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
assume \<mu>\<nu>\<tau>: "VVV.arr \<mu>\<nu>\<tau>"
[PROOF STATE]
proof (state)
this:
VVV.arr \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
have "\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) =
                (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot>
                  \<a>[dom (fst \<mu>\<nu>\<tau>), dom (fst (snd \<mu>\<nu>\<tau>)), dom (snd (snd \<mu>\<nu>\<tau>))]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))]
[PROOF STEP]
using \<mu>\<nu>\<tau> \<alpha>_def
[PROOF STATE]
proof (prove)
using this:
VVV.arr \<mu>\<nu>\<tau>
\<alpha> ?\<mu> ?\<nu> ?\<tau> \<equiv> if VVV.arr (?\<mu>, ?\<nu>, ?\<tau>) then (?\<mu> \<star> ?\<nu> \<star> ?\<tau>) \<cdot> \<a>[local.dom ?\<mu>, local.dom ?\<nu>, local.dom ?\<tau>] else null

goal (1 subgoal):
 1. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))]
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))]

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))]

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
have "... = \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot>
                             ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))] = \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))
[PROOF STEP]
using \<mu>\<nu>\<tau> HoHV_def HoVH_def VVV.arr_char\<^sub>S\<^sub>b\<^sub>C VV.arr_char\<^sub>S\<^sub>b\<^sub>C assoc_naturality\<^sub>A\<^sub>W\<^sub>C
                  composable_char\<^sub>P\<^sub>B\<^sub>H
[PROOF STATE]
proof (prove)
using this:
VVV.arr \<mu>\<nu>\<tau>
HoHV ?\<mu> \<equiv> if VVV.arr ?\<mu> then (fst ?\<mu> \<star> fst (snd ?\<mu>)) \<star> snd (snd ?\<mu>) else null
HoVH ?\<mu> \<equiv> if VVV.arr ?\<mu> then fst ?\<mu> \<star> fst (snd ?\<mu>) \<star> snd (snd ?\<mu>) else null
VVV.arr ?f = (arr (fst ?f) \<and> VV.arr (snd ?f) \<and> src (fst ?f) = trg (fst (snd ?f)))
VV.arr ?f = (arr (fst ?f) \<and> arr (snd ?f) \<and> src (fst ?f) = trg (snd ?f))
\<lbrakk>?\<tau> \<star> ?\<mu> \<noteq> null; ?\<mu> \<star> ?\<nu> \<noteq> null\<rbrakk> \<Longrightarrow> \<a>[cod ?\<tau>, cod ?\<mu>, cod ?\<nu>] \<cdot> ((?\<tau> \<star> ?\<mu>) \<star> ?\<nu>) = (?\<tau> \<star> ?\<mu> \<star> ?\<nu>) \<cdot> \<a>[local.dom ?\<tau>, local.dom ?\<mu>, local.dom ?\<nu>]
(?\<nu> \<star> ?\<mu> \<noteq> null) = (arr ?\<mu> \<and> arr ?\<nu> \<and> src ?\<nu> = trg ?\<mu>)

goal (1 subgoal):
 1. (fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))] = \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))] = \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>) \<star> snd (snd \<mu>\<nu>\<tau>)) \<cdot> \<a>[local.dom (fst \<mu>\<nu>\<tau>), local.dom (fst (snd \<mu>\<nu>\<tau>)), local.dom (snd (snd \<mu>\<nu>\<tau>))] = \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
have "... =
                     \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot>
                       ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))
[PROOF STEP]
using \<mu>\<nu>\<tau> VVV.arr_char\<^sub>S\<^sub>b\<^sub>C VVV.cod_char\<^sub>S\<^sub>b\<^sub>C VV.arr_char\<^sub>S\<^sub>b\<^sub>C
[PROOF STATE]
proof (prove)
using this:
VVV.arr \<mu>\<nu>\<tau>
VVV.arr ?f = (arr (fst ?f) \<and> VV.arr (snd ?f) \<and> src (fst ?f) = trg (fst (snd ?f)))
VVV.cod ?f = (if VVV.arr ?f then VxVxV.cod ?f else VxVxV.null)
VV.arr ?f = (arr (fst ?f) \<and> arr (snd ?f) \<and> src (fst ?f) = trg (snd ?f))

goal (1 subgoal):
 1. \<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<a>[cod (fst \<mu>\<nu>\<tau>), cod (fst (snd \<mu>\<nu>\<tau>)), cod (snd (snd \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>))

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
have "... = \<alpha>.map \<mu>\<nu>\<tau>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
using \<mu>\<nu>\<tau> \<alpha>.map_def HoHV_def composable_char\<^sub>P\<^sub>B\<^sub>H
[PROOF STATE]
proof (prove)
using this:
VVV.arr \<mu>\<nu>\<tau>
\<alpha>.map ?f = (if VVV.arr ?f then \<a>[fst (VVV.cod ?f), fst (snd (VVV.cod ?f)), snd (snd (VVV.cod ?f))] \<cdot> HoHV ?f else null)
HoHV ?\<mu> \<equiv> if VVV.arr ?\<mu> then (fst ?\<mu> \<star> fst (snd ?\<mu>)) \<star> snd (snd ?\<mu>) else null
(?\<nu> \<star> ?\<mu> \<noteq> null) = (arr ?\<mu> \<and> arr ?\<nu> \<and> src ?\<nu> = trg ?\<mu>)

goal (1 subgoal):
 1. \<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<a>[fst (VVV.cod \<mu>\<nu>\<tau>), fst (snd (VVV.cod \<mu>\<nu>\<tau>)), snd (snd (VVV.cod \<mu>\<nu>\<tau>))] \<cdot> ((fst \<mu>\<nu>\<tau> \<star> fst (snd \<mu>\<nu>\<tau>)) \<star> snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. \<And>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
show "\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>"
[PROOF STATE]
proof (prove)
using this:
\<not> VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
VVV.arr \<mu>\<nu>\<tau> \<Longrightarrow> \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal (1 subgoal):
 1. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)) = \<alpha>.map \<mu>\<nu>\<tau>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>))) = \<alpha>.map

goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>))) = \<alpha>.map

goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
using \<alpha>.natural_isomorphism_axioms
[PROOF STATE]
proof (prove)
using this:
(\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>))) = \<alpha>.map
natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH \<alpha>.map

goal (1 subgoal):
 1. natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
natural_isomorphism VVV.comp (\<cdot>) HoHV HoVH (\<lambda>\<mu>\<nu>\<tau>. \<alpha> (fst \<mu>\<nu>\<tau>) (fst (snd \<mu>\<nu>\<tau>)) (snd (snd \<mu>\<nu>\<tau>)))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma TQ: "preT C e s = e (postQ C s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preT C e s = e (postQ C s)
[PROOF STEP]
apply(induct C arbitrary: e s)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>e s. preT SKIP e s = e (postQ SKIP s)
 2. \<And>x1 x2 e s. preT (x1 ::= x2) e s = e (postQ (x1 ::= x2) s)
 3. \<And>C1 C2 e s. \<lbrakk>\<And>e s. preT C1 e s = e (postQ C1 s); \<And>e s. preT C2 e s = e (postQ C2 s)\<rbrakk> \<Longrightarrow> preT (C1;; C2) e s = e (postQ (C1;; C2) s)
 4. \<And>x1 C1 C2 e s. \<lbrakk>\<And>e s. preT C1 e s = e (postQ C1 s); \<And>e s. preT C2 e s = e (postQ C2 s)\<rbrakk> \<Longrightarrow> preT (IF x1 THEN C1 ELSE C2) e s = e (postQ (IF x1 THEN C1 ELSE C2) s)
 5. \<And>x1 x2 x3 C e s. (\<And>e s. preT C e s = e (postQ C s)) \<Longrightarrow> preT ({x1/x2/x3} CONSEQ C) e s = e (postQ ({x1/x2/x3} CONSEQ C) s)
 6. \<And>x1 x2 C e s. (\<And>e s. preT C e s = e (postQ C s)) \<Longrightarrow> preT ({x1} WHILE x2 DO C) e s = e (postQ ({x1} WHILE x2 DO C) s)
[PROOF STEP]
by (auto)


[STATEMENT]
lemma Max_to_image:
  "Max {f t | t. t \<in> S} = Max (f ` S)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Max {f t |t. t \<in> S} = Max (f ` S)
[PROOF STEP]
by (rule arg_cong[where f = Max]) auto


[STATEMENT]
lemma step_outerFriendIDs_idem:
assumes "step s a = (ou, s')"
and "\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and>
                      a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and>
                      a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and>
                      a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')"
shows "sentOuterFriendIDs s' = sentOuterFriendIDs s" (is ?sent)
  and "recvOuterFriendIDs s' = recvOuterFriendIDs s" (is ?recv)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s &&& recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s
 2. recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
have "?sent \<and> ?recv"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Sact x1\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Cact x2\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
case (Sact sa)
[PROOF STATE]
proof (state)
this:
a = Sact sa

goal (7 subgoals):
 1. \<And>x1. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Sact x1\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Cact x2\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 6. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 7. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Sact sa
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Sact sa

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
by (cases sa) (auto simp add: s_defs)
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Cact x2\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Cact x2\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
case (Cact ca)
[PROOF STATE]
proof (state)
this:
a = Cact ca

goal (6 subgoals):
 1. \<And>x2. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Cact x2\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 6. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Cact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Cact ca

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
by (cases ca) (auto simp add: c_defs)
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (5 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
case (Dact da)
[PROOF STATE]
proof (state)
this:
a = Dact da

goal (5 subgoals):
 1. \<And>x3. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Dact x3\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 5. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Dact da
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Dact da

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
by (cases da) (auto simp add: d_defs)
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (4 subgoals):
 1. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
case (Uact ua)
[PROOF STATE]
proof (state)
this:
a = Uact ua

goal (4 subgoals):
 1. \<And>x4. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Uact x4\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 4. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Uact ua
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = Uact ua

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
by (cases ua) (auto simp add: u_defs)
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (3 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
case (COMact ca)
[PROOF STATE]
proof (state)
this:
a = COMact ca

goal (3 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 3. \<And>x7. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = COMact x7\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = COMact ca
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
step s a = (ou, s')
\<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID')
a = COMact ca

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
by (cases ca) (auto simp add: com_defs)
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (2 subgoals):
 1. \<And>x5. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Ract x5\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
 2. \<And>x6. \<lbrakk>step s a = (ou, s'); \<forall>uID p aID uID'. a \<noteq> COMact (comSendCreateOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveCreateOFriend aID p uID uID') \<and> a \<noteq> COMact (comSendDeleteOFriend uID p aID uID') \<and> a \<noteq> COMact (comReceiveDeleteOFriend aID p uID uID'); a = Lact x6\<rbrakk> \<Longrightarrow> sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (2 subgoals):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s
 2. recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
show "?sent" and "?recv"
[PROOF STATE]
proof (prove)
using this:
sentOuterFriendIDs s' = sentOuterFriendIDs s \<and> recvOuterFriendIDs s' = recvOuterFriendIDs s

goal (1 subgoal):
 1. sentOuterFriendIDs s' = sentOuterFriendIDs s &&& recvOuterFriendIDs s' = recvOuterFriendIDs s
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sentOuterFriendIDs s' = sentOuterFriendIDs s
recvOuterFriendIDs s' = recvOuterFriendIDs s

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Tree\<^sub>\<alpha>_abs_rep [simp]: "abs_Tree\<^sub>\<alpha> (rep_Tree\<^sub>\<alpha> t\<^sub>\<alpha>) = t\<^sub>\<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abs_Tree\<^sub>\<alpha> (rep_Tree\<^sub>\<alpha> t\<^sub>\<alpha>) = t\<^sub>\<alpha>
[PROOF STEP]
by (metis Quotient_Tree\<^sub>\<alpha> Quotient_abs_rep)


[STATEMENT]
lemma similar_matrix_trans: "A \<sim> B \<Longrightarrow> B \<sim> C \<Longrightarrow> A \<sim> C" for A B C :: "('a::semiring_1)^'n^'n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A \<sim> B; B \<sim> C\<rbrakk> \<Longrightarrow> A \<sim> C
[PROOF STEP]
proof(unfold similar_matrix_def, clarsimp)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
fix P Q
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
assume "A = P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P" and "B = Q\<^sup>-\<^sup>1 ** C ** Q"
[PROOF STATE]
proof (state)
this:
A = P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P
B = Q\<^sup>-\<^sup>1 ** C ** Q

goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
let ?R = "Q ** P"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
assume inverts: "invertible Q" "invertible P"
[PROOF STATE]
proof (state)
this:
invertible Q
invertible P

goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
hence "?R\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1"
[PROOF STATE]
proof (prove)
using this:
invertible Q
invertible P

goal (1 subgoal):
 1. (Q ** P)\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1
[PROOF STEP]
by (rule matrix_inv_matrix_mul)
[PROOF STATE]
proof (state)
this:
(Q ** P)\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1

goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(Q ** P)\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1

goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
have "invertible ?R"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. invertible (Q ** P)
[PROOF STEP]
using inverts invertible_mult
[PROOF STATE]
proof (prove)
using this:
invertible Q
invertible P
\<lbrakk>invertible ?A; invertible ?B\<rbrakk> \<Longrightarrow> invertible (?A ** ?B)

goal (1 subgoal):
 1. invertible (Q ** P)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
invertible (Q ** P)

goal (1 subgoal):
 1. \<And>P Pa. \<lbrakk>invertible P; A = P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P; invertible Pa; B = Pa\<^sup>-\<^sup>1 ** C ** Pa\<rbrakk> \<Longrightarrow> \<exists>Pb. invertible Pb \<and> P\<^sup>-\<^sup>1 ** (Pa\<^sup>-\<^sup>1 ** C ** Pa) ** P = Pb\<^sup>-\<^sup>1 ** C ** Pb
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(Q ** P)\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1
invertible (Q ** P)
[PROOF STEP]
show "\<exists>R. invertible R \<and> P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P = R\<^sup>-\<^sup>1 ** C ** R"
[PROOF STATE]
proof (prove)
using this:
(Q ** P)\<^sup>-\<^sup>1 = P\<^sup>-\<^sup>1 ** Q\<^sup>-\<^sup>1
invertible (Q ** P)

goal (1 subgoal):
 1. \<exists>R. invertible R \<and> P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P = R\<^sup>-\<^sup>1 ** C ** R
[PROOF STEP]
by (metis matrix_mul_assoc)
[PROOF STATE]
proof (state)
this:
\<exists>R. invertible R \<and> P\<^sup>-\<^sup>1 ** (Q\<^sup>-\<^sup>1 ** C ** Q) ** P = R\<^sup>-\<^sup>1 ** C ** R

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ltlr_rel_sv[relator_props]:
  assumes SV: "single_valued R"
  shows "single_valued (\<langle>R\<rangle>ltlr_rel)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. single_valued (\<langle>R\<rangle>ltlr_rel)
[PROOF STEP]
proof (intro single_valuedI allI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> \<langle>R\<rangle>ltlr_rel; (x, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
fix x y z
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> \<langle>R\<rangle>ltlr_rel; (x, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
assume "(x, y) \<in> \<langle>R\<rangle>ltlr_rel" "(x, z) \<in> \<langle>R\<rangle>ltlr_rel"
[PROOF STATE]
proof (state)
this:
(x, y) \<in> \<langle>R\<rangle>ltlr_rel
(x, z) \<in> \<langle>R\<rangle>ltlr_rel

goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>(x, y) \<in> \<langle>R\<rangle>ltlr_rel; (x, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> y = z
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> \<langle>R\<rangle>ltlr_rel
(x, z) \<in> \<langle>R\<rangle>ltlr_rel
[PROOF STEP]
show "y=z"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> \<langle>R\<rangle>ltlr_rel
(x, z) \<in> \<langle>R\<rangle>ltlr_rel

goal (1 subgoal):
 1. y = z
[PROOF STEP]
apply (induction arbitrary: z)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<And>z. (true\<^sub>r, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> true\<^sub>r = z
 2. \<And>z. (false\<^sub>r, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> false\<^sub>r = z
 3. \<And>a a' z. \<lbrakk>(a, a') \<in> R; (prop\<^sub>r(a), z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> prop\<^sub>r(a') = z
 4. \<And>a a' z. \<lbrakk>(a, a') \<in> R; (nprop\<^sub>r(a), z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> nprop\<^sub>r(a') = z
 5. \<And>a a' b b' z. \<lbrakk>(a, a') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (a, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> a' = z; (b, b') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (b, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> b' = z; (a and\<^sub>r b, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> a' and\<^sub>r b' = z
 6. \<And>a a' b b' z. \<lbrakk>(a, a') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (a, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> a' = z; (b, b') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (b, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> b' = z; (a or\<^sub>r b, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> a' or\<^sub>r b' = z
 7. \<And>a a' z. \<lbrakk>(a, a') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (a, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> a' = z; (X\<^sub>r a, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> X\<^sub>r a' = z
 8. \<And>a a' b b' z. \<lbrakk>(a, a') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (a, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> a' = z; (b, b') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (b, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> b' = z; (a U\<^sub>r b, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> a' U\<^sub>r b' = z
 9. \<And>a a' b b' z. \<lbrakk>(a, a') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (a, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> a' = z; (b, b') \<in> \<langle>R\<rangle>ltlr_rel; \<And>z. (b, z) \<in> \<langle>R\<rangle>ltlr_rel \<Longrightarrow> b' = z; (a R\<^sub>r b, z) \<in> \<langle>R\<rangle>ltlr_rel\<rbrakk> \<Longrightarrow> a' R\<^sub>r b' = z
[PROOF STEP]
apply (simp (no_asm_use) only: ltlr_rel_left_simps
      | blast intro: single_valuedD[OF SV])+
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
y = z

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma bisimWeakCoinduct[consumes 1, case_names cSim cSym]:
  fixes P :: "ccs"
  and   Q :: "ccs"
  and   X :: "(ccs \<times> ccs) set"

  assumes "(P, Q) \<in> X"
  and     "\<And>P Q. (P, Q) \<in> X \<Longrightarrow> P \<leadsto>[X] Q"
  and     "\<And>P Q. (P, Q) \<in> X \<Longrightarrow> (Q, P) \<in> X"

  shows "P \<sim> Q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. P \<sim> Q
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. P \<sim> Q
[PROOF STEP]
have "X \<union> bisim = {(P, Q). (P, Q) \<in> X \<or> (P, Q) \<in> bisim}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. X \<union> bisim = {(P, Q). (P, Q) \<in> X \<or> P \<sim> Q}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
X \<union> bisim = {(P, Q). (P, Q) \<in> X \<or> P \<sim> Q}

goal (1 subgoal):
 1. P \<sim> Q
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
(P, Q) \<in> X
(?P, ?Q) \<in> X \<Longrightarrow> ?P \<leadsto>[X] ?Q
(?P, ?Q) \<in> X \<Longrightarrow> (?Q, ?P) \<in> X
X \<union> bisim = {(P, Q). (P, Q) \<in> X \<or> P \<sim> Q}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(P, Q) \<in> X
(?P, ?Q) \<in> X \<Longrightarrow> ?P \<leadsto>[X] ?Q
(?P, ?Q) \<in> X \<Longrightarrow> (?Q, ?P) \<in> X
X \<union> bisim = {(P, Q). (P, Q) \<in> X \<or> P \<sim> Q}

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma extended_distance_middle_formula:
  assumes "x \<in> wo.underS (middle a b)"
  shows "extended_distance x (middle a b) = (extended_distance a b)/2
    + (SUP w\<in>wo.underS (middle a b) \<inter> extended_distance_set.
          extended_distance x w - max (extended_distance a w) (extended_distance b w))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extended_distance x (middle a b) = extended_distance a b / 2 + (SUP w\<in>underS Bonk_Schramm_extension_unfolded_wo (middle a b) \<inter> extended_distance_set. extended_distance x w - max (extended_distance a w) (extended_distance b w))
[PROOF STEP]
unfolding extended_distance_set_def extended_distance_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x (middle a b)) x (middle a b) = extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a b) a b / 2 + (SUP w\<in>underS Bonk_Schramm_extension_unfolded_wo (middle a b) \<inter> {z. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo z z) z z = 0}. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x w) x w - max (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a w) a w) (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo b w) b w))
[PROOF STEP]
apply (subst extend_distance_fp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. extend_distance extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x (middle a b)) x (middle a b) = extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a b) a b / 2 + (SUP w\<in>underS Bonk_Schramm_extension_unfolded_wo (middle a b) \<inter> {z. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo z z) z z = 0}. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x w) x w - max (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a w) a w) (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo b w) b w))
[PROOF STEP]
apply (simp add: assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (SUP w\<in>{z \<in> underS Bonk_Schramm_extension_unfolded_wo (middle a b). extend_distance_fp z z z = 0}. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x w) x w - max (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a w) a w) (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo b w) b w)) = (SUP xa\<in>underS Bonk_Schramm_extension_unfolded_wo (middle a b) \<inter> {z. extend_distance_fp z z z = 0}. extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x xa) x xa - max (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a xa) a xa) (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo b xa) b xa))
[PROOF STEP]
apply (rule SUP_cong)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. {z \<in> underS Bonk_Schramm_extension_unfolded_wo (middle a b). extend_distance_fp z z z = 0} = underS Bonk_Schramm_extension_unfolded_wo (middle a b) \<inter> {z. extend_distance_fp z z z = 0}
 2. \<And>xa. xa \<in> underS Bonk_Schramm_extension_unfolded_wo (middle a b) \<inter> {z. extend_distance_fp z z z = 0} \<Longrightarrow> extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x xa) x xa - max (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a xa) a xa) (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo b xa) b xa) = extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo x xa) x xa - max (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo a xa) a xa) (extend_distance_fp (max2 Bonk_Schramm_extension_unfolded_wo b xa) b xa)
[PROOF STEP]
apply (auto simp add: wo.max2_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma normal_exp: "oSuc 0 < x \<Longrightarrow> normal ((**) x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. oSuc 0 < x \<Longrightarrow> normal ((**) x)
[PROOF STEP]
apply (frule_tac order_less_trans[OF less_oSuc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>oSuc 0 < x; 0 < x\<rbrakk> \<Longrightarrow> normal ((**) x)
[PROOF STEP]
apply (rule normalI, simp, rename_tac y)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>oSuc 0 < x; 0 < x\<rbrakk> \<Longrightarrow> x ** y < x ** oSuc y
[PROOF STEP]
apply (subgoal_tac "x ** y * 1 < x ** y * x", simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>oSuc 0 < x; 0 < x\<rbrakk> \<Longrightarrow> x ** y * 1 < x ** y * x
[PROOF STEP]
apply (subst ordinal_times_left_cancel_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrakk>oSuc 0 < x; 0 < x\<rbrakk> \<Longrightarrow> 0 < x ** y
 2. \<And>y. \<lbrakk>oSuc 0 < x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>oSuc 0 < x; 0 < x\<rbrakk> \<Longrightarrow> 1 < x
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma denyAllDom[simp]: "x \<in> dom (deny_all)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<in> dom D\<^sub>U
[PROOF STEP]
by (simp add: UPFDefs(24) domI)