[STATEMENT]
lemma reflexive_one_closed:
  "reflexive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma reflexive_sup_closed:
  "reflexive x \<Longrightarrow> reflexive (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive x \<Longrightarrow> reflexive (x \<squnion> y)
[PROOF STEP]
by (simp add: le_supI1)


[STATEMENT]
lemma reflexive_mult_closed:
  "reflexive x \<Longrightarrow> reflexive y \<Longrightarrow> reflexive (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x * y)
[PROOF STEP]
using mult_isotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z

goal (1 subgoal):
 1. \<lbrakk>reflexive x; reflexive y\<rbrakk> \<Longrightarrow> reflexive (x * y)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma coreflexive_bot_closed:
  "coreflexive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive bot
[PROOF STEP]
by simp


[STATEMENT]
lemma coreflexive_one_closed:
  "coreflexive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma coreflexive_sup_closed:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> coreflexive (x \<squnion> y)
[PROOF STEP]
by simp


[STATEMENT]
lemma coreflexive_mult_closed:
  "coreflexive x \<Longrightarrow> coreflexive y \<Longrightarrow> coreflexive (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> coreflexive (x * y)
[PROOF STEP]
using mult_isotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z

goal (1 subgoal):
 1. \<lbrakk>coreflexive x; coreflexive y\<rbrakk> \<Longrightarrow> coreflexive (x * y)
[PROOF STEP]
by fastforce


[STATEMENT]
lemma transitive_bot_closed:
  "transitive bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive bot
[PROOF STEP]
by simp


[STATEMENT]
lemma transitive_one_closed:
  "transitive 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma dense_bot_closed:
  "dense_rel bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel bot
[PROOF STEP]
by simp


[STATEMENT]
lemma dense_one_closed:
  "dense_rel 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma dense_sup_closed:
  "dense_rel x \<Longrightarrow> dense_rel y \<Longrightarrow> dense_rel (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dense_rel x; dense_rel y\<rbrakk> \<Longrightarrow> dense_rel (x \<squnion> y)
[PROOF STEP]
by (metis mult_right_dist_sup order_lesseq_imp sup.mono mult_left_sub_dist_sup_left mult_left_sub_dist_sup_right)


[STATEMENT]
lemma idempotent_bot_closed:
  "idempotent bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent bot
[PROOF STEP]
by simp


[STATEMENT]
lemma idempotent_one_closed:
  "idempotent 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. idempotent (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma preorder_one_closed:
  "preorder 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive (1::'a) \<and> transitive (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma coreflexive_transitive:
  "coreflexive x \<Longrightarrow> transitive x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> transitive x
[PROOF STEP]
using mult_left_isotone
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?x * ?z \<le> ?y * ?z

goal (1 subgoal):
 1. coreflexive x \<Longrightarrow> transitive x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma preorder_idempotent:
  "preorder x \<Longrightarrow> idempotent x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preorder x \<Longrightarrow> idempotent x
[PROOF STEP]
using order.antisym mult_isotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z

goal (1 subgoal):
 1. preorder x \<Longrightarrow> idempotent x
[PROOF STEP]
by fastforce


[STATEMENT]
lemma lstar_rec_isotone:
  "isotone (Lf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isotone (\<lambda>x. Rf x y)
[PROOF STEP]
using isotone_def sup_right_divisibility sup_right_isotone mult_right_sub_dist_sup_right
[PROOF STATE]
proof (prove)
using this:
isotone ?f \<equiv> \<forall>x y. x \<le> y \<longrightarrow> ?f x \<le> ?f y
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y
?y * ?z \<le> (?x \<squnion> ?y) * ?z

goal (1 subgoal):
 1. isotone (\<lambda>x. Rf x y)
[PROOF STEP]
by auto


[STATEMENT]
lemma rstar_rec_isotone:
  "isotone (Rf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isotone (Rf y)
[PROOF STEP]
using isotone_def sup_right_divisibility sup_right_isotone mult_left_sub_dist_sup_right
[PROOF STATE]
proof (prove)
using this:
isotone ?f \<equiv> \<forall>x y. x \<le> y \<longrightarrow> ?f x \<le> ?f y
(?x \<le> ?y) = (\<exists>z. z \<squnion> ?x = ?y)
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y
?x * ?z \<le> ?x * (?y \<squnion> ?z)

goal (1 subgoal):
 1. isotone (Rf y)
[PROOF STEP]
by auto


[STATEMENT]
lemma sstar_rec_isotone:
  "isotone (Sf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isotone (Sf y)
[PROOF STEP]
using isotone_def sup_right_isotone mult_isotone
[PROOF STATE]
proof (prove)
using this:
isotone ?f \<equiv> \<forall>x y. x \<le> y \<longrightarrow> ?f x \<le> ?f y
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y
\<lbrakk>?w \<le> ?y; ?x \<le> ?z\<rbrakk> \<Longrightarrow> ?w * ?x \<le> ?y * ?z

goal (1 subgoal):
 1. isotone (Sf y)
[PROOF STEP]
by auto


[STATEMENT]
lemma lstar_fixpoint:
  "has_least_prefixpoint (Lf y) \<Longrightarrow> lstar y = \<mu> (Lf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_least_prefixpoint (\<lambda>x. Rf x y) \<Longrightarrow> p\<mu> (\<lambda>x. Rf x y) = \<mu> (\<lambda>x. Rf x y)
[PROOF STEP]
by (simp add: pmu_mu lstar_rec_isotone)


[STATEMENT]
lemma rstar_fixpoint:
  "has_least_prefixpoint (Rf y) \<Longrightarrow> rstar y = \<mu> (Rf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_least_prefixpoint (Rf y) \<Longrightarrow> rstar y = \<mu> Rf y
[PROOF STEP]
by (simp add: pmu_mu rstar_rec_isotone)


[STATEMENT]
lemma sstar_fixpoint:
  "has_least_prefixpoint (Sf y) \<Longrightarrow> sstar y = \<mu> (Sf y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_least_prefixpoint (Sf y) \<Longrightarrow> sstar y = \<mu> Sf y
[PROOF STEP]
by (simp add: pmu_mu sstar_rec_isotone)


[STATEMENT]
lemma sstar_increasing:
  "has_least_prefixpoint (Sf y) \<Longrightarrow> y \<le> sstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. has_least_prefixpoint (Sf y) \<Longrightarrow> y \<le> sstar y
[PROOF STEP]
using order_trans pmu_unfold sup_ge1 sup_ge2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f
?x \<le> ?x \<squnion> ?y
?y \<le> ?x \<squnion> ?y

goal (1 subgoal):
 1. has_least_prefixpoint (Sf y) \<Longrightarrow> y \<le> sstar y
[PROOF STEP]
by blast


[STATEMENT]
lemma rstar_below_sstar:
  assumes "has_least_prefixpoint (Rf y)"
      and "has_least_prefixpoint (Sf y)"
    shows "rstar y \<le> sstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
have "y \<le> sstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> sstar y
[PROOF STEP]
using assms(2) pmu_unfold
[PROOF STATE]
proof (prove)
using this:
has_least_prefixpoint (Sf y)
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. y \<le> sstar y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
y \<le> sstar y

goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
hence "Rf y (sstar y) \<le> Sf y (sstar y)"
[PROOF STATE]
proof (prove)
using this:
y \<le> sstar y

goal (1 subgoal):
 1. Rf y (sstar y) \<le> Sf y (sstar y)
[PROOF STEP]
by (meson sup.cobounded1 sup.mono mult_left_isotone)
[PROOF STATE]
proof (state)
this:
Rf y (sstar y) \<le> Sf y (sstar y)

goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rf y (sstar y) \<le> Sf y (sstar y)

goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
have "... \<le> sstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Sf y (sstar y) \<le> sstar y
[PROOF STEP]
using assms(2) pmu_unfold
[PROOF STATE]
proof (prove)
using this:
has_least_prefixpoint (Sf y)
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. Sf y (sstar y) \<le> sstar y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Sf y (sstar y) \<le> sstar y

goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Rf y (sstar y) \<le> sstar y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Rf y (sstar y) \<le> sstar y

goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
using assms(1) is_least_prefixpoint_def least_prefixpoint
[PROOF STATE]
proof (prove)
using this:
Rf y (sstar y) \<le> sstar y
has_least_prefixpoint (Rf y)
is_least_prefixpoint ?f ?x \<equiv> ?f ?x \<le> ?x \<and> (\<forall>y. ?f y \<le> y \<longrightarrow> ?x \<le> y)
has_least_prefixpoint ?f \<Longrightarrow> is_least_prefixpoint ?f (p\<mu> ?f)

goal (1 subgoal):
 1. rstar y \<le> sstar y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rstar y \<le> sstar y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_one_associative [simp]:
  "x * 1 * y = x * y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (1::'a) * y = x * y
[PROOF STEP]
by (metis dual_order.antisym mult_left_isotone mult_left_one mult_semi_associative mult_sub_right_one)


[STATEMENT]
lemma mult_sup_associative_one:
  "(x * (y * 1)) * z \<le> x * (y * z)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y * (1::'a)) * z \<le> x * (y * z)
[PROOF STEP]
by (metis mult_semi_associative mult_one_associative)


[STATEMENT]
lemma rstar_increasing:
  assumes "has_least_prefixpoint (Rf y)"
    shows "y \<le> rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> rstar y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. y \<le> rstar y
[PROOF STEP]
have "Rf y (rstar y) \<le> rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rf y (rstar y) \<le> rstar y
[PROOF STEP]
using assms pmu_unfold
[PROOF STATE]
proof (prove)
using this:
has_least_prefixpoint (Rf y)
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. Rf y (rstar y) \<le> rstar y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Rf y (rstar y) \<le> rstar y

goal (1 subgoal):
 1. y \<le> rstar y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Rf y (rstar y) \<le> rstar y

goal (1 subgoal):
 1. y \<le> rstar y
[PROOF STEP]
by (metis le_supE mult_right_isotone mult_sub_right_one sup.absorb_iff2)
[PROOF STATE]
proof (state)
this:
y \<le> rstar y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma lres_left_isotone:
  "x \<le> y \<Longrightarrow> x / z \<le> y / z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x / z \<le> y / z
[PROOF STEP]
using dual_order.trans lres_galois
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> x / z \<le> y / z
[PROOF STEP]
by blast


[STATEMENT]
lemma lres_right_antitone:
  "x \<le> y \<Longrightarrow> z / y \<le> z / x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> z / y \<le> z / x
[PROOF STEP]
using dual_order.trans lres_galois mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?b \<le> ?a; ?c \<le> ?b\<rbrakk> \<Longrightarrow> ?c \<le> ?a
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. x \<le> y \<Longrightarrow> z / y \<le> z / x
[PROOF STEP]
by blast


[STATEMENT]
lemma lres_inverse:
  "(x / y) * y \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x / y * y \<le> x
[PROOF STEP]
by (simp add: lres_galois)


[STATEMENT]
lemma lres_one:
  "x / 1 \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x / (1::'a) \<le> x
[PROOF STEP]
using mult_sub_right_one order_trans lres_inverse
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?x * (1::'a)
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?x / ?y * ?y \<le> ?x

goal (1 subgoal):
 1. x / (1::'a) \<le> x
[PROOF STEP]
by blast


[STATEMENT]
lemma lres_mult_sub_lres_lres:
  "x / (z * y) \<le> (x / y) / z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x / (z * y) \<le> x / y / z
[PROOF STEP]
using lres_galois mult_semi_associative order.trans
[PROOF STATE]
proof (prove)
using this:
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)
?x * ?y * ?z \<le> ?x * (?y * ?z)
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c

goal (1 subgoal):
 1. x / (z * y) \<le> x / y / z
[PROOF STEP]
by blast


[STATEMENT]
lemma mult_lres_sub_assoc:
  "x * (y / z) \<le> (x * y) / z"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (y / z) \<le> x * y / z
[PROOF STEP]
by (meson dual_order.trans lres_galois mult_right_isotone lres_inverse lres_mult_sub_lres_lres)


[STATEMENT]
lemma lstar_below_rstar:
  assumes "has_least_prefixpoint (Lf y)"
      and "has_least_prefixpoint (Rf y)"
    shows "lstar y \<le> rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
have "y * (rstar y / y) * y \<le> y * rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * (rstar y / y) * y \<le> y * rstar y
[PROOF STEP]
using lres_galois mult_lres_sub_assoc
[PROOF STATE]
proof (prove)
using this:
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)
?x * (?y / ?z) \<le> ?x * ?y / ?z

goal (1 subgoal):
 1. y * (rstar y / y) * y \<le> y * rstar y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
y * (rstar y / y) * y \<le> y * rstar y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
y * (rstar y / y) * y \<le> y * rstar y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
have "... \<le> rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y * rstar y \<le> rstar y
[PROOF STEP]
using assms(2) le_supE pmu_unfold
[PROOF STATE]
proof (prove)
using this:
has_least_prefixpoint (Rf y)
\<lbrakk>?a \<squnion> ?b \<le> ?x; \<lbrakk>?a \<le> ?x; ?b \<le> ?x\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. y * rstar y \<le> rstar y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
y * rstar y \<le> rstar y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
y * (rstar y / y) * y \<le> rstar y
[PROOF STEP]
have "y * (rstar y / y) \<le> rstar y / y"
[PROOF STATE]
proof (prove)
using this:
y * (rstar y / y) * y \<le> rstar y

goal (1 subgoal):
 1. y * (rstar y / y) \<le> rstar y / y
[PROOF STEP]
by (simp add: lres_galois)
[PROOF STATE]
proof (state)
this:
y * (rstar y / y) \<le> rstar y / y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
hence "Rf y (rstar y / y) \<le> rstar y / y"
[PROOF STATE]
proof (prove)
using this:
y * (rstar y / y) \<le> rstar y / y

goal (1 subgoal):
 1. Rf y (rstar y / y) \<le> rstar y / y
[PROOF STEP]
using assms(2) lres_galois rstar_increasing
[PROOF STATE]
proof (prove)
using this:
y * (rstar y / y) \<le> rstar y / y
has_least_prefixpoint (Rf y)
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)
has_least_prefixpoint (Rf ?y) \<Longrightarrow> ?y \<le> rstar ?y

goal (1 subgoal):
 1. Rf y (rstar y / y) \<le> rstar y / y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Rf y (rstar y / y) \<le> rstar y / y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
hence "rstar y \<le> rstar y / y"
[PROOF STATE]
proof (prove)
using this:
Rf y (rstar y / y) \<le> rstar y / y

goal (1 subgoal):
 1. rstar y \<le> rstar y / y
[PROOF STEP]
using assms(2) is_least_prefixpoint_def least_prefixpoint
[PROOF STATE]
proof (prove)
using this:
Rf y (rstar y / y) \<le> rstar y / y
has_least_prefixpoint (Rf y)
is_least_prefixpoint ?f ?x \<equiv> ?f ?x \<le> ?x \<and> (\<forall>y. ?f y \<le> y \<longrightarrow> ?x \<le> y)
has_least_prefixpoint ?f \<Longrightarrow> is_least_prefixpoint ?f (p\<mu> ?f)

goal (1 subgoal):
 1. rstar y \<le> rstar y / y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
rstar y \<le> rstar y / y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
hence "Lf y (rstar y) \<le> rstar y"
[PROOF STATE]
proof (prove)
using this:
rstar y \<le> rstar y / y

goal (1 subgoal):
 1. Rf (rstar y) y \<le> rstar y
[PROOF STEP]
using assms(2) lres_galois pmu_unfold
[PROOF STATE]
proof (prove)
using this:
rstar y \<le> rstar y / y
has_least_prefixpoint (Rf y)
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. Rf (rstar y) y \<le> rstar y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Rf (rstar y) y \<le> rstar y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
Rf (rstar y) y \<le> rstar y

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
using assms(1) is_least_prefixpoint_def least_prefixpoint
[PROOF STATE]
proof (prove)
using this:
Rf (rstar y) y \<le> rstar y
has_least_prefixpoint (\<lambda>x. Rf x y)
is_least_prefixpoint ?f ?x \<equiv> ?f ?x \<le> ?x \<and> (\<forall>y. ?f y \<le> y \<longrightarrow> ?x \<le> y)
has_least_prefixpoint ?f \<Longrightarrow> is_least_prefixpoint ?f (p\<mu> ?f)

goal (1 subgoal):
 1. p\<mu> (\<lambda>x. Rf x y) \<le> rstar y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p\<mu> (\<lambda>x. Rf x y) \<le> rstar y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rstar_sstar:
  assumes "has_least_prefixpoint (Rf y)"
      and "has_least_prefixpoint (Sf y)"
    shows "rstar y = sstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
have "Rf y (rstar y / rstar y) * rstar y \<le> rstar y \<squnion> y * ((rstar y / rstar y) * rstar y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Rf y (rstar y / rstar y) * rstar y \<le> rstar y \<squnion> y * (rstar y / rstar y * rstar y)
[PROOF STEP]
using mult_right_dist_sup mult_semi_associative sup_right_isotone
[PROOF STATE]
proof (prove)
using this:
(?x \<squnion> ?y) * ?z = ?x * ?z \<squnion> ?y * ?z
?x * ?y * ?z \<le> ?x * (?y * ?z)
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y

goal (1 subgoal):
 1. Rf y (rstar y / rstar y) * rstar y \<le> rstar y \<squnion> y * (rstar y / rstar y * rstar y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Rf y (rstar y / rstar y) * rstar y \<le> rstar y \<squnion> y * (rstar y / rstar y * rstar y)

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Rf y (rstar y / rstar y) * rstar y \<le> rstar y \<squnion> y * (rstar y / rstar y * rstar y)

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
have "... \<le> rstar y \<squnion> y * rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rstar y \<squnion> y * (rstar y / rstar y * rstar y) \<le> rstar y \<squnion> y * rstar y
[PROOF STEP]
using mult_right_isotone sup_right_isotone lres_inverse
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?x \<le> ?y \<Longrightarrow> ?z \<squnion> ?x \<le> ?z \<squnion> ?y
?x / ?y * ?y \<le> ?x

goal (1 subgoal):
 1. rstar y \<squnion> y * (rstar y / rstar y * rstar y) \<le> rstar y \<squnion> y * rstar y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
rstar y \<squnion> y * (rstar y / rstar y * rstar y) \<le> rstar y \<squnion> y * rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
rstar y \<squnion> y * (rstar y / rstar y * rstar y) \<le> rstar y \<squnion> y * rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
have "... \<le> rstar y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rstar y \<squnion> y * rstar y \<le> rstar y
[PROOF STEP]
using assms(1) pmu_unfold
[PROOF STATE]
proof (prove)
using this:
has_least_prefixpoint (Rf y)
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. rstar y \<squnion> y * rstar y \<le> rstar y
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
rstar y \<squnion> y * rstar y \<le> rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Rf y (rstar y / rstar y) * rstar y \<le> rstar y
[PROOF STEP]
have "Rf y (rstar y / rstar y) \<le> rstar y / rstar y"
[PROOF STATE]
proof (prove)
using this:
Rf y (rstar y / rstar y) * rstar y \<le> rstar y

goal (1 subgoal):
 1. Rf y (rstar y / rstar y) \<le> rstar y / rstar y
[PROOF STEP]
by (simp add: lres_galois)
[PROOF STATE]
proof (state)
this:
Rf y (rstar y / rstar y) \<le> rstar y / rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
hence "rstar y * rstar y \<le> rstar y"
[PROOF STATE]
proof (prove)
using this:
Rf y (rstar y / rstar y) \<le> rstar y / rstar y

goal (1 subgoal):
 1. transitive (rstar y)
[PROOF STEP]
using assms(1) is_least_prefixpoint_def least_prefixpoint lres_galois
[PROOF STATE]
proof (prove)
using this:
Rf y (rstar y / rstar y) \<le> rstar y / rstar y
has_least_prefixpoint (Rf y)
is_least_prefixpoint ?f ?x \<equiv> ?f ?x \<le> ?x \<and> (\<forall>y. ?f y \<le> y \<longrightarrow> ?x \<le> y)
has_least_prefixpoint ?f \<Longrightarrow> is_least_prefixpoint ?f (p\<mu> ?f)
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)

goal (1 subgoal):
 1. transitive (rstar y)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
transitive (rstar y)

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
hence "y \<squnion> rstar y * rstar y \<le> rstar y"
[PROOF STATE]
proof (prove)
using this:
transitive (rstar y)

goal (1 subgoal):
 1. y \<squnion> rstar y * rstar y \<le> rstar y
[PROOF STEP]
by (simp add: assms(1) rstar_increasing)
[PROOF STATE]
proof (state)
this:
y \<squnion> rstar y * rstar y \<le> rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
hence "Sf y (rstar y) \<le> rstar y"
[PROOF STATE]
proof (prove)
using this:
y \<squnion> rstar y * rstar y \<le> rstar y

goal (1 subgoal):
 1. Sf y (rstar y) \<le> rstar y
[PROOF STEP]
using assms(1) pmu_unfold
[PROOF STATE]
proof (prove)
using this:
y \<squnion> rstar y * rstar y \<le> rstar y
has_least_prefixpoint (Rf y)
has_least_prefixpoint ?f \<Longrightarrow> ?f (p\<mu> ?f) \<le> p\<mu> ?f

goal (1 subgoal):
 1. Sf y (rstar y) \<le> rstar y
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
Sf y (rstar y) \<le> rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
hence "sstar y \<le> rstar y"
[PROOF STATE]
proof (prove)
using this:
Sf y (rstar y) \<le> rstar y

goal (1 subgoal):
 1. sstar y \<le> rstar y
[PROOF STEP]
using assms(2) is_least_prefixpoint_def least_prefixpoint
[PROOF STATE]
proof (prove)
using this:
Sf y (rstar y) \<le> rstar y
has_least_prefixpoint (Sf y)
is_least_prefixpoint ?f ?x \<equiv> ?f ?x \<le> ?x \<and> (\<forall>y. ?f y \<le> y \<longrightarrow> ?x \<le> y)
has_least_prefixpoint ?f \<Longrightarrow> is_least_prefixpoint ?f (p\<mu> ?f)

goal (1 subgoal):
 1. sstar y \<le> rstar y
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
sstar y \<le> rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
sstar y \<le> rstar y

goal (1 subgoal):
 1. rstar y = sstar y
[PROOF STEP]
by (simp add: assms order.antisym rstar_below_sstar)
[PROOF STATE]
proof (state)
this:
rstar y = sstar y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma zero_right_mult_decreasing:
  "x * bot \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * bot \<le> x
[PROOF STEP]
by (metis bot_least mult_1_right mult_right_isotone)


[STATEMENT]
lemma test_preserves_equation:
  assumes "dense_rel p"
      and "coreflexive p"
    shows "p * x \<le> x * p \<longleftrightarrow> p * x = p * x * p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p * x \<le> x * p) = (p * x = p * x * p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p * x \<le> x * p \<Longrightarrow> p * x = p * x * p
 2. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
assume 1: "p * x \<le> x * p"
[PROOF STATE]
proof (state)
this:
p * x \<le> x * p

goal (2 subgoals):
 1. p * x \<le> x * p \<Longrightarrow> p * x = p * x * p
 2. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
have "p * x \<le> p * p * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * x \<le> p * p * x
[PROOF STEP]
by (simp add: assms(1) mult_left_isotone)
[PROOF STATE]
proof (state)
this:
p * x \<le> p * p * x

goal (2 subgoals):
 1. p * x \<le> x * p \<Longrightarrow> p * x = p * x * p
 2. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
p * x \<le> p * p * x

goal (2 subgoals):
 1. p * x \<le> x * p \<Longrightarrow> p * x = p * x * p
 2. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
have "... \<le> p * x * p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p * p * x \<le> p * x * p
[PROOF STEP]
using 1
[PROOF STATE]
proof (prove)
using this:
p * x \<le> x * p

goal (1 subgoal):
 1. p * p * x \<le> p * x * p
[PROOF STEP]
by (simp add: mult_right_isotone mult_assoc)
[PROOF STATE]
proof (state)
this:
p * p * x \<le> p * x * p

goal (2 subgoals):
 1. p * x \<le> x * p \<Longrightarrow> p * x = p * x * p
 2. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
p * x \<le> p * x * p
[PROOF STEP]
show "p * x = p * x * p"
[PROOF STATE]
proof (prove)
using this:
p * x \<le> p * x * p

goal (1 subgoal):
 1. p * x = p * x * p
[PROOF STEP]
using assms(2) order.antisym mult_right_isotone
[PROOF STATE]
proof (prove)
using this:
p * x \<le> p * x * p
coreflexive p
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y

goal (1 subgoal):
 1. p * x = p * x * p
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
p * x = p * x * p

goal (1 subgoal):
 1. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
assume "p * x = p * x * p"
[PROOF STATE]
proof (state)
this:
p * x = p * x * p

goal (1 subgoal):
 1. p * x = p * x * p \<Longrightarrow> p * x \<le> x * p
[PROOF STEP]
thus "p * x \<le> x * p"
[PROOF STATE]
proof (prove)
using this:
p * x = p * x * p

goal (1 subgoal):
 1. p * x \<le> x * p
[PROOF STEP]
by (metis assms(2) mult_left_isotone mult_left_one)
[PROOF STATE]
proof (state)
this:
p * x \<le> x * p

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma case_split_right:
  assumes "1 \<le> w \<squnion> z"
      and "x * w \<le> y"
      and "x * z \<le> y"
    shows "x \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
have "x * (w \<squnion> z) \<le> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * (w \<squnion> z) \<le> y
[PROOF STEP]
by (simp add: assms(2-3) mult_left_dist_sup)
[PROOF STATE]
proof (state)
this:
x * (w \<squnion> z) \<le> y

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
x * (w \<squnion> z) \<le> y

goal (1 subgoal):
 1. x \<le> y
[PROOF STEP]
by (metis assms(1) dual_order.trans mult_1_right mult_right_isotone)
[PROOF STATE]
proof (state)
this:
x \<le> y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma case_split_right_equal:
  "w \<squnion> z = 1 \<Longrightarrow> x * w = y * w \<Longrightarrow> x * z = y * z \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w \<squnion> z = (1::'a); x * w = y * w; x * z = y * z\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis mult_1_right mult_left_dist_sup)


[STATEMENT]
lemma sup_left_top [simp]:
  "top \<squnion> x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top \<squnion> x = top
[PROOF STEP]
using sup_right_top sup.commute
[PROOF STATE]
proof (prove)
using this:
?x \<squnion> top = top
?a \<squnion> ?b = ?b \<squnion> ?a

goal (1 subgoal):
 1. top \<squnion> x = top
[PROOF STEP]
by fastforce


[STATEMENT]
lemma top_greatest [simp]:
  "x \<le> top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> top
[PROOF STEP]
by (simp add: le_iff_sup)


[STATEMENT]
lemma top_left_mult_increasing:
  "x \<le> top * x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> top * x
[PROOF STEP]
by (metis mult_left_isotone mult_left_one top_greatest)


[STATEMENT]
lemma top_right_mult_increasing:
  "x \<le> x * top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x \<le> x * top
[PROOF STEP]
using mult_right_isotone mult_sub_right_one order_trans top_greatest
[PROOF STATE]
proof (prove)
using this:
?x \<le> ?y \<Longrightarrow> ?z * ?x \<le> ?z * ?y
?x \<le> ?x * (1::'a)
\<lbrakk>?x \<le> ?y; ?y \<le> ?z\<rbrakk> \<Longrightarrow> ?x \<le> ?z
?x \<le> top

goal (1 subgoal):
 1. x \<le> x * top
[PROOF STEP]
by blast


[STATEMENT]
lemma top_mult_top [simp]:
  "top * top = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by (simp add: order.antisym top_left_mult_increasing)


[STATEMENT]
lemma vector_bot_closed:
  "vector bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector bot
[PROOF STEP]
by simp


[STATEMENT]
lemma vector_top_closed:
  "vector top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma vector_sup_closed:
  "vector x \<Longrightarrow> vector y \<Longrightarrow> vector (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vector x; vector y\<rbrakk> \<Longrightarrow> vector (x \<squnion> y)
[PROOF STEP]
by (simp add: mult_right_dist_sup)


[STATEMENT]
lemma covector_top_closed:
  "covector top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma total_one_closed:
  "total 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total (1::'a)
[PROOF STEP]
by simp


[STATEMENT]
lemma total_top_closed:
  "total top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma total_sup_closed:
  "total x \<Longrightarrow> total (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. times_top_class.total x \<Longrightarrow> times_top_class.total (x \<squnion> y)
[PROOF STEP]
by (simp add: mult_right_dist_sup)


[STATEMENT]
lemma surjective_one_closed:
  "surjective 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective (1::'a)
[PROOF STEP]
by (simp add: order.antisym mult_sub_right_one)


[STATEMENT]
lemma surjective_top_closed:
  "surjective top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma surjective_sup_closed:
  "surjective x \<Longrightarrow> surjective (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective x \<Longrightarrow> surjective (x \<squnion> y)
[PROOF STEP]
by (metis le_iff_sup mult_left_sub_dist_sup_left sup_left_top)


[STATEMENT]
lemma reflexive_top_closed:
  "reflexive top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. reflexive top
[PROOF STEP]
by simp


[STATEMENT]
lemma transitive_top_closed:
  "transitive top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. transitive top
[PROOF STEP]
by simp


[STATEMENT]
lemma dense_top_closed:
  "dense_rel top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dense_rel top
[PROOF STEP]
by simp


[STATEMENT]
lemma idempotent_top_closed:
  "idempotent top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. surjective top
[PROOF STEP]
by simp


[STATEMENT]
lemma preorder_top_closed:
  "preorder top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. preorder top
[PROOF STEP]
by simp


[STATEMENT]
lemma vector_mult_closed:
  "vector y \<Longrightarrow> vector (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vector y \<Longrightarrow> vector (x * y)
[PROOF STEP]
by (metis order.antisym mult_semi_associative top_right_mult_increasing)


[STATEMENT]
lemma surjective_mult_closed:
  "surjective x \<Longrightarrow> surjective y \<Longrightarrow> surjective (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>surjective x; surjective y\<rbrakk> \<Longrightarrow> surjective (x * y)
[PROOF STEP]
by (metis order.antisym mult_semi_associative top_greatest)


[STATEMENT]
lemma lres_top_decreasing:
  "x / top \<le> x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x / top \<le> x
[PROOF STEP]
using lres_inverse order.trans top_right_mult_increasing
[PROOF STATE]
proof (prove)
using this:
?x / ?y * ?y \<le> ?x
\<lbrakk>?a \<le> ?b; ?b \<le> ?c\<rbrakk> \<Longrightarrow> ?a \<le> ?c
?x \<le> ?x * top

goal (1 subgoal):
 1. x / top \<le> x
[PROOF STEP]
by blast


[STATEMENT]
lemma top_lres_absorb [simp]:
  "top / x = top"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. top / x = top
[PROOF STEP]
using order.antisym lres_galois top_greatest
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?a \<le> ?b; ?b \<le> ?a\<rbrakk> \<Longrightarrow> ?a = ?b
(?x * ?y \<le> ?z) = (?x \<le> ?z / ?y)
?x \<le> top

goal (1 subgoal):
 1. top / x = top
[PROOF STEP]
by blast


[STATEMENT]
lemma covector_lres_closed:
  "covector x \<Longrightarrow> covector (x / y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector x \<Longrightarrow> covector (x / y)
[PROOF STEP]
by (metis order.antisym mult_lres_sub_assoc top_left_mult_increasing)


[STATEMENT]
lemma covector_mult_closed:
  "covector x \<Longrightarrow> covector (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector x \<Longrightarrow> covector (x * y)
[PROOF STEP]
by (metis mult_assoc)


[STATEMENT]
lemma total_mult_closed:
  "total x \<Longrightarrow> total y \<Longrightarrow> total (x * y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>times_top_class.total x; times_top_class.total y\<rbrakk> \<Longrightarrow> times_top_class.total (x * y)
[PROOF STEP]
by (simp add: mult_assoc)


[STATEMENT]
lemma covector_sup_closed:
  "covector x \<Longrightarrow> covector y \<Longrightarrow> covector (x \<squnion> y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>covector x; covector y\<rbrakk> \<Longrightarrow> covector (x \<squnion> y)
[PROOF STEP]
by (simp add: mult_left_dist_sup)


[STATEMENT]
lemma covector_bot_closed:
  "covector bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. covector bot
[PROOF STEP]
by simp


[STATEMENT]
lemma (in is_dghm) dghm_ArrMap_is_arr''[dg_cs_intros]:
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" and "\<FF>f = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
  shows "\<FF>f : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>f : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>f : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
unfolding assms(2)
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (rule dghm_ArrMap_is_arr)


[STATEMENT]
lemma (in is_dghm) dghm_ArrMap_is_arr'[dg_cs_intros]:
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
    and "A = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
    and "B = \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
  shows "\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : A \<mapsto>\<^bsub>\<BB>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : A \<mapsto>\<^bsub>\<BB>\<^esub> B
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : A \<mapsto>\<^bsub>\<BB>\<^esub> B
[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (rule dghm_ArrMap_is_arr)


[STATEMENT]
lemma (in is_dghm) is_dghm_axioms'[dg_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>"
  shows "\<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule is_dghm_axioms)


[STATEMENT]
lemma dghm_eqI:
  assumes "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
    and "\<GG>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>"
    and "\<GG>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>"
    and "\<AA> = \<CC>"
    and "\<BB> = \
"
  shows "\<GG> = \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> = \<FF>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> = \<FF>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<AA> \<BB> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> = \<FF>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<CC> \
 \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> = \<FF>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> = \<FF>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv \<GG>
 2. vsv \<FF>
 3. \<D>\<^sub>\<circ> \<GG> = \<D>\<^sub>\<circ> \<FF>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<GG> \<Longrightarrow> \<GG>\<lparr>a\<rparr> = \<FF>\<lparr>a\<rparr>
[PROOF STEP]
have dom: "\<D>\<^sub>\<circ> \<GG> = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<GG> = 4\<^sub>\<nat>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<GG> = 4\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<GG>
 2. vsv \<FF>
 3. \<D>\<^sub>\<circ> \<GG> = \<D>\<^sub>\<circ> \<FF>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<GG> \<Longrightarrow> \<GG>\<lparr>a\<rparr> = \<FF>\<lparr>a\<rparr>
[PROOF STEP]
from assms(5,6)
[PROOF STATE]
proof (chain)
picking this:
\<AA> = \<CC>
\<BB> = \

[PROOF STEP]
have sup: "\<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>" "\<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<AA> = \<CC>
\<BB> = \

goal (1 subgoal):
 1. \<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr> &&& \<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>
[PROOF STEP]
by (simp_all add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>
\<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>

goal (4 subgoals):
 1. vsv \<GG>
 2. vsv \<FF>
 3. \<D>\<^sub>\<circ> \<GG> = \<D>\<^sub>\<circ> \<FF>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<GG> \<Longrightarrow> \<GG>\<lparr>a\<rparr> = \<FF>\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<GG> \<Longrightarrow> \<GG>\<lparr>a\<rparr> = \<FF>\<lparr>a\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<GG> \<Longrightarrow> \<GG>\<lparr>a\<rparr> = \<FF>\<lparr>a\<rparr>
[PROOF STEP]
by (unfold dom, elim_in_numeral, insert assms(3,4) sup)
        (auto simp: dghm_field_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<GG> \<Longrightarrow> \<GG>\<lparr>?a\<rparr> = \<FF>\<lparr>?a\<rparr>

goal (3 subgoals):
 1. vsv \<GG>
 2. vsv \<FF>
 3. \<D>\<^sub>\<circ> \<GG> = \<D>\<^sub>\<circ> \<FF>
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps cs_intro: V_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<GG> = \<FF>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_dghm) dghm_def: "\<FF> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv \<FF>
 2. vsv [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<FF> = \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> \<FF> = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<FF> = 4\<^sub>\<nat>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<FF> = 4\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<FF>
 2. vsv [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<FF> = \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<FF>
 2. vsv [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<FF> = \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
show "\<D>\<^sub>\<circ> \<FF> = \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 4\<^sub>\<nat>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<FF> = \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
using this:
4\<^sub>\<nat> = 4\<^sub>\<nat>

goal (1 subgoal):
 1. 4\<^sub>\<nat> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<FF> = \<D>\<^sub>\<circ> [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>

goal (3 subgoals):
 1. vsv \<FF>
 2. vsv [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
by (unfold dom_lhs, elim_in_numeral, unfold dghm_field_simps)
      (simp_all add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<FF> \<Longrightarrow> \<FF>\<lparr>?a\<rparr> = [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv \<FF>
 2. vsv [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<FF>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
qed (auto simp: vsv_axioms)


[STATEMENT]
lemma (in is_dghm) dghm_ObjMap_app_in_HomCod_Obj[dg_cs_intros]:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
using assms dghm_ObjMap_vrange
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by (blast dest: ObjMap.vsv_vimageI2)


[STATEMENT]
lemma (in is_dghm) dghm_ArrMap_vrange: "\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
proof(rule vsv.vsv_vrange_vsubset, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
assume "f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
obtain a b where "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<And>a b. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (2 subgoals):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have "\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (2 subgoals):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
show "\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. vsv (\<FF>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
qed auto


[STATEMENT]
lemma (in is_dghm) dghm_ArrMap_app_in_HomCod_Arr[dg_cs_intros]:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>"
  shows "\<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
using assms dghm_ArrMap_vrange
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Arr\<rparr>
\<R>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by (blast dest: ArrMap.vsv_vimageI2)


[STATEMENT]
lemma (in is_dghm) dghm_ObjMap_vsubset_Vset: "\<FF>\<lparr>ObjMap\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by
    (
      rule ObjMap.vbrelation_Limit_vsubset_VsetI,
      insert dghm_ObjMap_vrange HomCod.dg_Obj_vsubset_Vset
    )
    (auto intro!: HomDom.dg_Obj_vsubset_Vset)


[STATEMENT]
lemma (in is_dghm) dghm_ArrMap_vsubset_Vset: "\<FF>\<lparr>ArrMap\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by
    (
      rule ArrMap.vbrelation_Limit_vsubset_VsetI,
      insert dghm_ArrMap_vrange HomCod.dg_Arr_vsubset_Vset
    )
    (auto intro!: HomDom.dg_Arr_vsubset_Vset)


[STATEMENT]
lemma (in is_dghm) dghm_ObjMap_in_Vset:
  assumes "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<FF>\<lparr>ObjMap\<rparr> \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (meson assms dghm_ObjMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)


[STATEMENT]
lemma (in is_dghm) dghm_ArrMap_in_Vset:
  assumes  "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<FF>\<lparr>ArrMap\<rparr> \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (meson assms dghm_ArrMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)


[STATEMENT]
lemma (in is_dghm) dghm_in_Vset:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<FF> \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
note [dg_cs_intros] =
    dghm_ObjMap_in_Vset dghm_ArrMap_in_Vset HomDom.dg_in_Vset HomCod.dg_in_Vset
[PROOF STATE]
proof (state)
this:
\<alpha> \<in>\<^sub>\<circ> ?\<beta> \<Longrightarrow> \<FF>\<lparr>ObjMap\<rparr> \<in>\<^sub>\<circ> Vset ?\<beta>
\<alpha> \<in>\<^sub>\<circ> ?\<beta> \<Longrightarrow> \<FF>\<lparr>ArrMap\<rparr> \<in>\<^sub>\<circ> Vset ?\<beta>
\<lbrakk>\<Z> ?\<beta>; \<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> \<AA> \<in>\<^sub>\<circ> Vset ?\<beta>
\<lbrakk>\<Z> ?\<beta>; \<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> \<BB> \<in>\<^sub>\<circ> Vset ?\<beta>

goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (subst dghm_def)
      (
        cs_concl cs_shallow
          cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros
      )
[PROOF STATE]
proof (state)
this:
\<FF> \<in>\<^sub>\<circ> Vset \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_dghm) dghm_is_dghm_if_ge_Limit:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> \<BB>
[PROOF STEP]
proof(rule is_dghmI)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<FF>
 3. digraph \<beta> \<AA>
 4. digraph \<beta> \<BB>
 5. vcard \<FF> = 4\<^sub>\<nat>
 6. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 7. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 8. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 9. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
from is_dghm_axioms assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show "digraph \<beta> \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. digraph \<beta> \<AA>
[PROOF STEP]
by (cs_concl cs_intro: digraph.dg_digraph_if_ge_Limit dg_cs_intros)
[PROOF STATE]
proof (state)
this:
digraph \<beta> \<AA>

goal (12 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<FF>
 3. digraph \<beta> \<BB>
 4. vcard \<FF> = 4\<^sub>\<nat>
 5. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 6. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 7. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 8. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
from is_dghm_axioms assms
[PROOF STATE]
proof (chain)
picking this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show "digraph \<beta> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
\<Z> \<beta>
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. digraph \<beta> \<BB>
[PROOF STEP]
by (cs_concl cs_intro: digraph.dg_digraph_if_ge_Limit dg_cs_intros)
[PROOF STATE]
proof (state)
this:
digraph \<beta> \<BB>

goal (11 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<FF>
 3. vcard \<FF> = 4\<^sub>\<nat>
 4. \<FF>\<lparr>HomDom\<rparr> = \<AA>
 5. \<FF>\<lparr>HomCod\<rparr> = \<BB>
 6. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
qed
  (
    cs_concl
      cs_simp: dg_cs_simps
      cs_intro: assms(1) dg_cs_intros V_cs_intros dghm_ObjMap_vrange
  )+


[STATEMENT]
lemma small_all_dghms[simp]: "small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
proof(cases \<open>\<Z> \<alpha>\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
 2. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
\<Z> \<alpha>

goal (2 subgoals):
 1. \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
 2. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
from is_dghm.dghm_in_Vset
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>; \<Z> ?\<beta>; ?\<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> ?\<FF> \<in>\<^sub>\<circ> Vset ?\<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>; \<Z> ?\<beta>; ?\<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> ?\<FF> \<in>\<^sub>\<circ> Vset ?\<beta>

goal (1 subgoal):
 1. small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by (intro down[of _ \<open>Vset (\<alpha> + \<omega>)\<close>] subsetI)
      (auto simp: True \<Z>.\<Z>_Limit_\<alpha>\<omega> \<Z>.\<Z>_\<omega>_\<alpha>\<omega> \<Z>.intro \<Z>.\<Z>_\<alpha>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<Z> \<alpha>

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<Z> \<alpha>
[PROOF STEP]
have "{\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}"
[PROOF STATE]
proof (prove)
using this:
\<not> \<Z> \<alpha>

goal (1 subgoal):
 1. {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}

goal (1 subgoal):
 1. small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
small {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_dghm) dghm_in_Vset_7: "\<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
note [folded VPow_iff, folded Vset_succ[OF Ord_\<alpha>], dg_cs_intros] =
    dghm_ObjMap_vsubset_Vset
    dghm_ArrMap_vsubset_Vset
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ObjMap\<rparr> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)
\<FF>\<lparr>ArrMap\<rparr> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ \<alpha>)

goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
from HomDom.dg_digraph_in_Vset_4
[PROOF STATE]
proof (chain)
picking this:
\<AA> \<in>\<^sub>\<circ> Vset (\<alpha> + 4\<^sub>\<nat>)
[PROOF STEP]
have [dg_cs_intros]:
    "\<AA> \<in>\<^sub>\<circ> Vset (succ (succ (succ (succ \<alpha>))))"
[PROOF STATE]
proof (prove)
using this:
\<AA> \<in>\<^sub>\<circ> Vset (\<alpha> + 4\<^sub>\<nat>)

goal (1 subgoal):
 1. \<AA> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))))
[PROOF STEP]
by (succ_of_numeral)
      (cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<AA> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))))

goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
from HomCod.dg_digraph_in_Vset_4
[PROOF STATE]
proof (chain)
picking this:
\<BB> \<in>\<^sub>\<circ> Vset (\<alpha> + 4\<^sub>\<nat>)
[PROOF STEP]
have [dg_cs_intros]:
    "\<BB> \<in>\<^sub>\<circ> Vset (succ (succ (succ (succ \<alpha>))))"
[PROOF STATE]
proof (prove)
using this:
\<BB> \<in>\<^sub>\<circ> Vset (\<alpha> + 4\<^sub>\<nat>)

goal (1 subgoal):
 1. \<BB> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))))
[PROOF STEP]
by (succ_of_numeral)
      (cs_prems cs_shallow cs_simp: plus_V_succ_right V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<BB> \<in>\<^sub>\<circ> Vset (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ (ZFC_in_HOL.succ \<alpha>))))

goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
by (subst dghm_def, succ_of_numeral)
      (
        cs_concl
          cs_simp: plus_V_succ_right V_cs_simps dg_cs_simps
          cs_intro: dg_cs_intros V_cs_intros
      )
[PROOF STATE]
proof (state)
this:
\<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in \<Z>) all_dghms_in_Vset:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "all_dghms \<alpha> \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_dghms \<alpha> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
proof(rule vsubset_in_VsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. all_dghms \<alpha> \<subseteq>\<^sub>\<circ> ?A
 2. ?A \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. all_dghms \<alpha> \<subseteq>\<^sub>\<circ> ?A
 2. ?A \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
show "all_dghms \<alpha> \<subseteq>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. all_dghms \<alpha> \<subseteq>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> all_dghms \<alpha> \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
fix \<FF>
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> all_dghms \<alpha> \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
assume "\<FF> \<in>\<^sub>\<circ> all_dghms \<alpha>"
[PROOF STATE]
proof (state)
this:
\<FF> \<in>\<^sub>\<circ> all_dghms \<alpha>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> all_dghms \<alpha> \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> \<in>\<^sub>\<circ> all_dghms \<alpha>
[PROOF STEP]
obtain \<AA> \<BB> where \<FF>: "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
using this:
\<FF> \<in>\<^sub>\<circ> all_dghms \<alpha>

goal (1 subgoal):
 1. (\<And>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by clarsimp
[PROOF STATE]
proof (state)
this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> all_dghms \<alpha> \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
interpret is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using \<FF>
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> all_dghms \<alpha> \<Longrightarrow> x \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
show "\<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)
[PROOF STEP]
by (rule dghm_in_Vset_7)
[PROOF STATE]
proof (state)
this:
\<FF> \<in>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
all_dghms \<alpha> \<subseteq>\<^sub>\<circ> Vset (\<alpha> + 7\<^sub>\<nat>)

goal (1 subgoal):
 1. Vset (\<alpha> + 7\<^sub>\<nat>) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
\<alpha> \<in>\<^sub>\<circ> \<beta>
[PROOF STEP]
show "Vset (\<alpha> + 7\<^sub>\<nat>) \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
using this:
\<alpha> \<in>\<^sub>\<circ> \<beta>

goal (1 subgoal):
 1. Vset (\<alpha> + 7\<^sub>\<nat>) \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: V_cs_intros Ord_cs_intros)
[PROOF STATE]
proof (state)
this:
Vset (\<alpha> + 7\<^sub>\<nat>) \<in>\<^sub>\<circ> Vset \<beta>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_dghms[simp]: "small {\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. small {\<FF>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
[PROOF STEP]
by (rule down[of _ \<open>set {\<FF>. \<exists>\<AA> \<BB>. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}\<close>]) auto


[STATEMENT]
lemma (in is_dghm) dghm_is_arr_HomCod:
  assumes "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
  shows "\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>" "\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>" "\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> &&& \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> &&& \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr> &&& \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr> &&& \<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+


[STATEMENT]
lemma (in is_dghm) dghm_vimage_dghm_ArrMap_vsubset_Hom:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "\<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<subseteq>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<subseteq>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
fix g
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
assume "g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b"
[PROOF STATE]
proof (state)
this:
g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b
[PROOF STEP]
obtain f where "f \<in>\<^sub>\<circ> Hom (\<FF>\<lparr>HomDom\<rparr>) a b" and "g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>"
[PROOF STATE]
proof (prove)
using this:
g \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b

goal (1 subgoal):
 1. (\<And>f. \<lbrakk>f \<in>\<^sub>\<circ> Hom (\<FF>\<lparr>HomDom\<rparr>) a b; g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> Hom (\<FF>\<lparr>HomDom\<rparr>) a b
g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr> `\<^sub>\<circ> Hom \<AA> a b \<Longrightarrow> x \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f \<in>\<^sub>\<circ> Hom (\<FF>\<lparr>HomDom\<rparr>) a b
g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>
[PROOF STEP]
show "g \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
f \<in>\<^sub>\<circ> Hom (\<FF>\<lparr>HomDom\<rparr>) a b
g = \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>

goal (1 subgoal):
 1. g \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
[PROOF STEP]
by (simp add: dghm_ArrMap_is_arr dg_cs_simps)
[PROOF STATE]
proof (state)
this:
g \<in>\<^sub>\<circ> Hom \<BB> (\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) (\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_dghm_components[dg_op_simps]:
  shows "op_dghm \<FF>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>"
    and "op_dghm \<FF>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>"
    and "op_dghm \<FF>\<lparr>HomDom\<rparr> = op_dg (\<FF>\<lparr>HomDom\<rparr>)"
    and "op_dghm \<FF>\<lparr>HomCod\<rparr> = op_dg (\<FF>\<lparr>HomCod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_dghm \<FF>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr> &&& op_dghm \<FF>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>) &&& op_dghm \<FF>\<lparr>HomDom\<rparr> = op_dg (\<FF>\<lparr>HomDom\<rparr>) &&& op_dghm \<FF>\<lparr>HomCod\<rparr> = op_dg (\<FF>\<lparr>HomCod\<rparr>)
[PROOF STEP]
unfolding op_dghm_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = \<FF>\<lparr>[]\<^sub>\<circ>\<rparr> &&& [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = \<FF>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>) &&& [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma (in is_dghm) is_dghm_op: "op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
proof(intro is_dghmI, unfold dg_op_simps)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (op_dghm \<FF>)
 3. digraph \<alpha> (op_dg \<AA>)
 4. digraph \<alpha> (op_dg \<BB>)
 5. vcard (op_dghm \<FF>) = 4\<^sub>\<nat>
 6. op_dg (\<FF>\<lparr>HomDom\<rparr>) = op_dg \<AA>
 7. op_dg (\<FF>\<lparr>HomCod\<rparr>) = op_dg \<BB>
 8. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 9. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (op_dghm \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (op_dghm \<FF>)
[PROOF STEP]
unfolding op_dghm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, op_dg (\<FF>\<lparr>HomDom\<rparr>), op_dg (\<FF>\<lparr>HomCod\<rparr>)]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (op_dghm \<FF>)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (op_dg \<AA>)
 3. digraph \<alpha> (op_dg \<BB>)
 4. vcard (op_dghm \<FF>) = 4\<^sub>\<nat>
 5. op_dg (\<FF>\<lparr>HomDom\<rparr>) = op_dg \<AA>
 6. op_dg (\<FF>\<lparr>HomCod\<rparr>) = op_dg \<BB>
 7. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 8. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (op_dghm \<FF>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (op_dghm \<FF>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding op_dghm_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<FF>\<lparr>ObjMap\<rparr>, \<FF>\<lparr>ArrMap\<rparr>, op_dg (\<FF>\<lparr>HomDom\<rparr>), op_dg (\<FF>\<lparr>HomCod\<rparr>)]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (auto simp: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (op_dghm \<FF>) = 4\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (op_dg \<AA>)
 3. digraph \<alpha> (op_dg \<BB>)
 4. op_dg (\<FF>\<lparr>HomDom\<rparr>) = op_dg \<AA>
 5. op_dg (\<FF>\<lparr>HomCod\<rparr>) = op_dg \<BB>
 6. vsv (\<FF>\<lparr>ObjMap\<rparr>)
 7. vsv (\<FF>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
qed
  (
    cs_concl cs_shallow
      cs_intro: dghm_ObjMap_vrange dg_cs_intros dg_op_intros V_cs_intros
      cs_simp: dg_cs_simps dg_op_simps
  )+


[STATEMENT]
lemma (in is_dghm) is_dghm_op'[dg_op_intros]:
  assumes "\<AA>' = op_dg \<AA>" and "\<BB>' = op_dg \<BB>" and "\<alpha>' = \<alpha>"
  shows "op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>'\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>'\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule is_dghm_op)


[STATEMENT]
lemma (in is_dghm) dghm_op_dghm_op_dghm[dg_op_simps]: "op_dghm (op_dghm \<FF>) = \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm (op_dghm \<FF>) = \<FF>
[PROOF STEP]
using is_dghm_axioms
[PROOF STATE]
proof (prove)
using this:
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. op_dghm (op_dghm \<FF>) = \<FF>
[PROOF STEP]
by
    (
      cs_concl cs_shallow
        cs_simp: dg_op_simps
        cs_intro: dg_op_intros dghm_eqI[where \<FF>=\<FF>]
    )


[STATEMENT]
lemma eq_op_dghm_iff[dg_op_simps]:
  assumes "\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>" and "\<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
  shows "op_dghm \<GG> = op_dghm \<FF> \<longleftrightarrow> \<GG> = \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_dghm \<GG> = op_dghm \<FF>) = (\<GG> = \<FF>)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_dghm \<GG> = op_dghm \<FF> \<Longrightarrow> \<GG> = \<FF>
 2. \<GG> = \<FF> \<Longrightarrow> op_dghm \<GG> = op_dghm \<FF>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<AA> \<BB> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_dghm \<GG> = op_dghm \<FF> \<Longrightarrow> \<GG> = \<FF>
 2. \<GG> = \<FF> \<Longrightarrow> op_dghm \<GG> = op_dghm \<FF>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<CC> \
 \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_dghm \<GG> = op_dghm \<FF> \<Longrightarrow> \<GG> = \<FF>
 2. \<GG> = \<FF> \<Longrightarrow> op_dghm \<GG> = op_dghm \<FF>
[PROOF STEP]
assume prems: "op_dghm \<GG> = op_dghm \<FF>"
[PROOF STATE]
proof (state)
this:
op_dghm \<GG> = op_dghm \<FF>

goal (2 subgoals):
 1. op_dghm \<GG> = op_dghm \<FF> \<Longrightarrow> \<GG> = \<FF>
 2. \<GG> = \<FF> \<Longrightarrow> op_dghm \<GG> = op_dghm \<FF>
[PROOF STEP]
show "\<GG> = \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> = \<FF>
[PROOF STEP]
proof(rule dghm_eqI[OF assms])
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<GG>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
 2. \<GG>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
 3. \<AA> = \<CC>
 4. \<BB> = \

[PROOF STEP]
from prems R.dghm_op_dghm_op_dghm L.dghm_op_dghm_op_dghm
[PROOF STATE]
proof (chain)
picking this:
op_dghm \<GG> = op_dghm \<FF>
op_dghm (op_dghm \<FF>) = \<FF>
op_dghm (op_dghm \<GG>) = \<GG>
[PROOF STEP]
show
      "\<GG>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>" and "\<GG>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
op_dghm \<GG> = op_dghm \<FF>
op_dghm (op_dghm \<FF>) = \<FF>
op_dghm (op_dghm \<GG>) = \<GG>

goal (1 subgoal):
 1. \<GG>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr> &&& \<GG>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<GG>\<lparr>ObjMap\<rparr> = \<FF>\<lparr>ObjMap\<rparr>
\<GG>\<lparr>ArrMap\<rparr> = \<FF>\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. \<AA> = \<CC>
 2. \<BB> = \

[PROOF STEP]
from prems R.dghm_op_dghm_op_dghm L.dghm_op_dghm_op_dghm
[PROOF STATE]
proof (chain)
picking this:
op_dghm \<GG> = op_dghm \<FF>
op_dghm (op_dghm \<FF>) = \<FF>
op_dghm (op_dghm \<GG>) = \<GG>
[PROOF STEP]
have
      "\<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>" "\<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
op_dghm \<GG> = op_dghm \<FF>
op_dghm (op_dghm \<FF>) = \<FF>
op_dghm (op_dghm \<GG>) = \<GG>

goal (1 subgoal):
 1. \<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr> &&& \<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>
\<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>

goal (2 subgoals):
 1. \<AA> = \<CC>
 2. \<BB> = \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>
\<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>
[PROOF STEP]
show "\<AA> = \<CC>" "\<BB> = \
"
[PROOF STATE]
proof (prove)
using this:
\<GG>\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>
\<GG>\<lparr>HomCod\<rparr> = \<FF>\<lparr>HomCod\<rparr>

goal (1 subgoal):
 1. \<AA> = \<CC> &&& \<BB> = \

[PROOF STEP]
by (auto simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<AA> = \<CC>
\<BB> = \

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<GG> = \<FF>

goal (1 subgoal):
 1. \<GG> = \<FF> \<Longrightarrow> op_dghm \<GG> = op_dghm \<FF>
[PROOF STEP]
qed auto


[STATEMENT]
lemma dghm_comp_components:
  shows "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = \<GG>\<lparr>ObjMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr>"
    and "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>"
    and [dg_shared_cs_simps, dg_cs_simps]: "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr>"
    and [dg_shared_cs_simps, dg_cs_simps]: "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>HomCod\<rparr> = \<GG>\<lparr>HomCod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = \<GG>\<lparr>ObjMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr> &&& (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = \<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>) &&& (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>HomDom\<rparr> = \<FF>\<lparr>HomDom\<rparr> &&& (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>HomCod\<rparr> = \<GG>\<lparr>HomCod\<rparr>
[PROOF STEP]
unfolding dghm_comp_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = \<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr> &&& [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<FF>\<lparr>2\<^sub>\<nat>\<rparr> &&& [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<GG>\<lparr>3\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma dghm_comp_ObjMap_vsv[dg_cs_intros]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
interpret L: is_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
interpret R: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
by (cs_concl cs_simp: dghm_comp_components cs_intro: V_cs_intros)
[PROOF STATE]
proof (state)
this:
vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_comp_ObjMap_vdomain[dg_cs_simps]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by
    (
      cs_concl
        cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
        cs_intro: is_dghm.dghm_ObjMap_vrange
    )


[STATEMENT]
lemma dghm_comp_ObjMap_vrange:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by
    (
      cs_concl cs_shallow
        cs_simp: dghm_comp_components
        cs_intro: is_dghm.dghm_ObjMap_vrange V_cs_intros
    )


[STATEMENT]
lemma dghm_comp_ObjMap_app[dg_cs_simps]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>" and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by
      (
        cs_concl
          cs_simp: dghm_comp_components dg_cs_simps V_cs_simps
          cs_intro: V_cs_intros dg_cs_intros
      )
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = \<GG>\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_comp_ArrMap_vsv[dg_cs_intros]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
interpret L: is_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
interpret R: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by (cs_concl cs_simp: dghm_comp_components cs_intro: V_cs_intros)
[PROOF STATE]
proof (state)
this:
vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed