[STATEMENT]
lemma (in pdigraph) pdg_dghm_proj_is_dghm:
  assumes "i \<in>\<^sub>\<circ> I"
  shows "\<pi>\<^sub>D\<^sub>G I \<AA> i : (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
proof(intro is_dghmI)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<pi>\<^sub>D\<^sub>G I \<AA> i)
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. digraph \<alpha> (\<AA> i)
 5. vcard (\<pi>\<^sub>D\<^sub>G I \<AA> i) = 4\<^sub>\<nat>
 6. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = dg_prod I \<AA>
 7. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
 8. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 9. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (\<pi>\<^sub>D\<^sub>G I \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<pi>\<^sub>D\<^sub>G I \<AA> i)
[PROOF STEP]
unfolding dghm_proj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, dg_prod I \<AA>, \<AA> i]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequence (\<pi>\<^sub>D\<^sub>G I \<AA> i)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. vcard (\<pi>\<^sub>D\<^sub>G I \<AA> i) = 4\<^sub>\<nat>
 5. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = dg_prod I \<AA>
 6. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
 7. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 8. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (\<pi>\<^sub>D\<^sub>G I \<AA> i) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (\<pi>\<^sub>D\<^sub>G I \<AA> i) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_proj_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>, \<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>, dg_prod I \<AA>, \<AA> i]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (\<pi>\<^sub>D\<^sub>G I \<AA> i) = 4\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = dg_prod I \<AA>
 5. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
 6. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 7. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
show "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = dg_prod I \<AA>
[PROOF STEP]
unfolding dghm_proj_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dg_prod I \<AA> = dg_prod I \<AA>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomDom\<rparr> = dg_prod I \<AA>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
 5. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 6. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 7. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 8. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b \<Longrightarrow> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
show "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i
[PROOF STEP]
unfolding dghm_proj_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<AA> i = \<AA> i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>HomCod\<rparr> = \<AA> i

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 5. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 6. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 7. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b \<Longrightarrow> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
fix f a b
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 5. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 6. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 7. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b \<Longrightarrow> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
assume "f : a \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<^esub> b"
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 5. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 6. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 7. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b \<Longrightarrow> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
with assms pdg_digraph_dg_prod
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
digraph \<alpha> (dg_prod I \<AA>)
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b
[PROOF STEP]
show
    "\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I
digraph \<alpha> (dg_prod I \<AA>)
f : a \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> b

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_prod_is_arrD(7))
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> \<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (dg_prod I \<AA>)
 3. digraph \<alpha> (\<AA> i)
 4. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
 5. vsv (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
 6. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) = dg_prod I \<AA>\<lparr>Obj\<rparr>
 7. \<R>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
 8. \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>) = dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
qed
  (
    auto simp:
      dg_cs_simps dg_cs_intros dg_prod_cs_intros
      assms pdg_digraph_dg_prod dghm_proj_ObjMap_vrange
  )


[STATEMENT]
lemma (in pdigraph) pdg_dghm_proj_is_dghm':
  assumes "i \<in>\<^sub>\<circ> I" and "\<CC> = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)" and "\
 = \<AA> i"
  shows "\<pi>\<^sub>D\<^sub>G I \<AA> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule pdg_dghm_proj_is_dghm)


[STATEMENT]
lemma dghm_up_components:
  shows "dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>))"
    and "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>))"
    and "dghm_up I \<AA> \<CC> \<phi>\<lparr>HomDom\<rparr> = \<CC>"
    and "dghm_up I \<AA> \<CC> \<phi>\<lparr>HomCod\<rparr> = (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) &&& dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)) &&& dghm_up I \<AA> \<CC> \<phi>\<lparr>HomDom\<rparr> = \<CC> &&& dghm_up I \<AA> \<CC> \<phi>\<lparr>HomCod\<rparr> = dg_prod I \<AA>
[PROOF STEP]
unfolding dghm_up_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>f\<rparr>, \<CC>, dg_prod I \<AA>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>f\<rparr>, \<CC>, dg_prod I \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>f\<rparr>)) &&& [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>f\<rparr>, \<CC>, dg_prod I \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<CC> &&& [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>f\<rparr>, \<CC>, dg_prod I \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = dg_prod I \<AA>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma dghm_up_ObjMap_vrange:
  assumes "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
  shows "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dghm_up_components dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)
[PROOF STEP]
proof(intro vrange_VLambda_vsubset vproductI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>) = I
 3. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>) = I
 3. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (3 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>) = I
 3. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
proof(intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
assume prems': "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
interpret \<phi>: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms[OF prems'])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
from prems prems'
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: \<phi>.dghm_ObjMap_app_in_HomCod_Obj)
[PROOF STATE]
proof (state)
this:
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>) = I
[PROOF STEP]
qed auto


[STATEMENT]
lemma dghm_up_ObjMap_app_vdomain[dg_cs_simps]:
  assumes "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
  shows "\<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
[PROOF STEP]
unfolding dghm_up_ObjMap_app[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_up_ObjMap_app_component[dg_cs_simps]:
  assumes "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>" and "i \<in>\<^sub>\<circ> I"
  shows "dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding dghm_up_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_up_ObjMap_app_vrange:
  assumes "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
  shows "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<subseteq>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
assume prems: "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
have "vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
unfolding dghm_up_ObjMap_app[OF assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
obtain i where b_def: "b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>"
    and i: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>; i \<in>\<^sub>\<circ> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: vsv.vrange_atE simp: dghm_up_ObjMap_app[OF assms(1)])
[PROOF STATE]
proof (state)
this:
b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
interpret \<phi>i: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms(2)[OF i])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
from dghm_up_ObjMap_app_component[OF assms(1) i] b_def
[PROOF STATE]
proof (chain)
picking this:
dghm_up I ?\<AA> \<CC> ?\<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = ?\<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
have b_def':
    "b = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
dghm_up I ?\<AA> \<CC> ?\<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = ?\<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>

goal (1 subgoal):
 1. b = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
have "b \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding b_def'
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
b \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>
[PROOF STEP]
show "b \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Obj\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I
b \<in>\<^sub>\<circ> \<AA> i\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Obj\<rparr>) `\<^sub>\<circ> I)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph) dghm_up_ArrMap_vrange:
  assumes "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
  shows "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dghm_up_components dg_prod_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
proof(intro vrange_VLambda_vsubset vproductI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>) = I
 3. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>) = I
 3. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (3 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>) = I
 3. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems': "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<phi>: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms[OF prems'])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from prems prems'
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>)
 2. \<And>x. x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> \<Longrightarrow> \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>x\<rparr>) = I
[PROOF STEP]
qed auto


[STATEMENT]
lemma dghm_up_ArrMap_vrange:
  assumes "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
  shows "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
fix A
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
assume "A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
obtain a where A_def: "A = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
    and a: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding dghm_up_ArrMap_vdomain dghm_up_components
[PROOF STATE]
proof (prove)
using this:
A \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>A = (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)\<lparr>a\<rparr>; a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
A = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
have "(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
proof(intro vproductI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) = I
 3. \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
show "\<forall>i\<in>\<^sub>\<circ>I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro ballI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<phi>: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms[OF prems])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
from prems a
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show "(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>i\<in>elts I. (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)\<lparr>i\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
 2. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) = I
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
show "A \<in>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. A \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding A_def dg_prod_components dghm_up_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
(\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)\<lparr>a\<rparr> \<in>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A \<in>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_up_ArrMap_app_vdomain[dg_cs_simps]:
  assumes "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
  shows "\<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) = I"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) = I
[PROOF STEP]
unfolding dghm_up_ArrMap_app[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) = I
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_up_ArrMap_app_component[dg_cs_simps]:
  assumes "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>" and "i \<in>\<^sub>\<circ> I"
  shows "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding dghm_up_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)\<lparr>a\<rparr>\<lparr>i\<rparr> = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_up_ArrMap_app_vrange:
  assumes "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
  shows "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<subseteq>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
proof(intro vsubsetI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
fix b
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
assume prems: "b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)"
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
have "vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
unfolding dghm_up_ArrMap_app[OF assms(1)]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
with prems
[PROOF STATE]
proof (chain)
picking this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
obtain i where b_def: "b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>"
    and i: "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (prove)
using this:
b \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)
vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>)

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>; i \<in>\<^sub>\<circ> I\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (auto elim: vsv.vrange_atE simp: dghm_up_ArrMap_app[OF assms(1)])
[PROOF STATE]
proof (state)
this:
b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
interpret \<phi>i: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms(2)[OF i])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
from dghm_up_ArrMap_app_component[OF assms(1) i] b_def
[PROOF STATE]
proof (chain)
picking this:
dghm_up I ?\<AA> \<CC> ?\<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = ?\<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
have b_def':
    "b = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
dghm_up I ?\<AA> \<CC> ?\<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> = ?\<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
b = dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr>

goal (1 subgoal):
 1. b = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b = \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
from assms(1)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
have "b \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding b_def'
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
with i
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
b \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>
[PROOF STEP]
show "b \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I
b \<in>\<^sub>\<circ> \<AA> i\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>I. \<AA> a\<lparr>Arr\<rparr>) `\<^sub>\<circ> I)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph) pdg_dghm_up_is_dghm:
  assumes "digraph \<alpha> \<CC>" and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
  shows "dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
interpret \<CC>: digraph \<alpha> \<CC>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
proof(intro is_dghmI, unfold dghm_up_components(3,4))
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dghm_up I \<AA> \<CC> \<phi>)
 3. digraph \<alpha> \<CC>
 4. digraph \<alpha> (dg_prod I \<AA>)
 5. vcard (dghm_up I \<AA> \<CC> \<phi>) = 4\<^sub>\<nat>
 6. \<CC> = \<CC>
 7. dg_prod I \<AA> = dg_prod I \<AA>
 8. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 9. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (dghm_up I \<AA> \<CC> \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dghm_up I \<AA> \<CC> \<phi>)
[PROOF STEP]
unfolding dghm_up_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>, \<CC>, dg_prod I \<AA>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (dghm_up I \<AA> \<CC> \<phi>)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. vcard (dghm_up I \<AA> \<CC> \<phi>) = 4\<^sub>\<nat>
 5. \<CC> = \<CC>
 6. dg_prod I \<AA> = dg_prod I \<AA>
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 8. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 9. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 10. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (dghm_up I \<AA> \<CC> \<phi>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dghm_up I \<AA> \<CC> \<phi>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_up_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>, \<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>, \<CC>, dg_prod I \<AA>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dghm_up I \<AA> \<CC> \<phi>) = 4\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. \<CC> = \<CC>
 5. dg_prod I \<AA> = dg_prod I \<AA>
 6. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> ?i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> ?i
[PROOF STEP]
show "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
?i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> ?i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> ?i

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (intro dghm_up_ObjMap_vrange) blast
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> dg_prod I \<AA>\<lparr>Obj\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. \<CC> = \<CC>
 5. dg_prod I \<AA> = dg_prod I \<AA>
 6. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
fix f a b
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. \<CC> = \<CC>
 5. dg_prod I \<AA> = dg_prod I \<AA>
 6. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
assume prems: "f : a \<mapsto>\<^bsub>\<CC>\<^esub> b"
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. \<CC> = \<CC>
 5. dg_prod I \<AA> = dg_prod I \<AA>
 6. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
[PROOF STEP]
have f: "f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>" and a: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>" and b: "b \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr> &&& a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr> &&& b \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
b \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. \<CC> = \<CC>
 5. dg_prod I \<AA> = dg_prod I \<AA>
 6. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<CC>\<^esub> b \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> :
      dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
proof(rule dg_prod_is_arrI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = I
 3. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
 5. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = I
 7. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = I
 3. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
 5. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = I
 7. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
assume prems': "i \<in>\<^sub>\<circ> I"
[PROOF STATE]
proof (state)
this:
i \<in>\<^sub>\<circ> I

goal (7 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = I
 3. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
 5. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = I
 7. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
interpret \<phi>: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms(2)[OF prems'])
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = I
 3. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
 5. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = I
 7. \<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
from \<phi>.is_dghm_axioms \<CC>.digraph_axioms prems pdigraph_axioms prems prems'
[PROOF STATE]
proof (chain)
picking this:
\<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
digraph \<alpha> \<CC>
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
pdigraph \<alpha> I \<AA>
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
i \<in>\<^sub>\<circ> I
[PROOF STEP]
show "dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> :
        dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
digraph \<alpha> \<CC>
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
pdigraph \<alpha> I \<AA>
f : a \<mapsto>\<^bsub>\<CC>\<^esub> b
i \<in>\<^sub>\<circ> I

goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<lparr>i\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<lparr>i\<rparr> \<mapsto>\<^bsub>\<AA> i\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<lparr>i\<rparr>

goal (6 subgoals):
 1. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>)
 2. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>) = I
 3. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>)
 4. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>) = I
 5. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>)
 6. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>) = I
[PROOF STEP]
qed (simp_all add: f a b dghm_up_ArrMap_app dghm_up_ObjMap_app)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>dg_prod I \<AA>\<^esub> dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> (dg_prod I \<AA>)
 4. \<CC> = \<CC>
 5. dg_prod I \<AA> = dg_prod I \<AA>
 6. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
 9. \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
qed (auto simp: dghm_up_components pdg_digraph_dg_prod dg_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in pdigraph) pdg_dghm_comp_dghm_proj_dghm_up:
  assumes "digraph \<alpha> \<CC>"
    and "\<And>i. i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
    and "i \<in>\<^sub>\<circ> I"
  shows "\<phi> i = \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i = \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>
[PROOF STEP]
proof(rule dghm_eqI[of \<alpha> \<CC> \<open>\<AA> i\<close> _ \<CC> \<open>\<AA> i\<close>])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 2. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 3. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
 4. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 5. \<CC> = \<CC>
 6. \<AA> i = \<AA> i
[PROOF STEP]
interpret \<phi>: is_dghm \<alpha> \<CC> \<open>\<AA> i\<close> \<open>\<phi> i\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (rule assms(2)[OF assms(3)])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 2. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 3. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
 4. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 5. \<CC> = \<CC>
 6. \<AA> i = \<AA> i
[PROOF STEP]
show "\<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (auto intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<phi> i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i

goal (5 subgoals):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 2. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
 3. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 4. \<CC> = \<CC>
 5. \<AA> i = \<AA> i
[PROOF STEP]
from assms(1,2)
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<CC>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> ?i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> ?i
[PROOF STEP]
have dghm_up: "dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> (\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<CC>
?i \<in>\<^sub>\<circ> I \<Longrightarrow> \<phi> ?i : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> ?i

goal (1 subgoal):
 1. dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
[PROOF STEP]
by (simp add: pdg_dghm_up_is_dghm)
[PROOF STATE]
proof (state)
this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>

goal (5 subgoals):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 2. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
 3. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 4. \<CC> = \<CC>
 5. \<AA> i = \<AA> i
[PROOF STEP]
note dghm_proj = pdg_dghm_proj_is_dghm[OF assms(3)]
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i

goal (5 subgoals):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
 2. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
 3. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 4. \<CC> = \<CC>
 5. \<AA> i = \<AA> i
[PROOF STEP]
from assms(3) pdg_dghm_proj_is_dghm
[PROOF STATE]
proof (chain)
picking this:
i \<in>\<^sub>\<circ> I
?i \<in>\<^sub>\<circ> I \<Longrightarrow> \<pi>\<^sub>D\<^sub>G I \<AA> ?i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> ?i
[PROOF STEP]
show
    "\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i"
[PROOF STATE]
proof (prove)
using this:
i \<in>\<^sub>\<circ> I
?i \<in>\<^sub>\<circ> I \<Longrightarrow> \<pi>\<^sub>D\<^sub>G I \<AA> ?i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> ?i

goal (1 subgoal):
 1. \<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
[PROOF STEP]
by (intro dghm_comp_is_dghm[of \<alpha> \<open>(\<Prod>\<^sub>D\<^sub>Gi\<in>\<^sub>\<circ>I. \<AA> i)\<close>])
      (auto simp: assms dghm_up)
[PROOF STATE]
proof (state)
this:
\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i

goal (4 subgoals):
 1. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
 2. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 3. \<CC> = \<CC>
 4. \<AA> i = \<AA> i
[PROOF STEP]
show "\<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
unfolding dghm_comp_components dghm_proj_components dghm_up_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<lambda>a\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Obj\<rparr>. a\<lparr>i\<rparr>) \<circ>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<CC>\<lparr>Obj\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>))
[PROOF STEP]
by (rule vsv_vcomp) simp_all
[PROOF STATE]
proof (state)
this:
vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)

goal (3 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from
      dghm_up_ObjMap_vrange[
        OF assms(2), simplified, unfolded dg_prod_components
        ]
[PROOF STATE]
proof (chain)
picking this:
(\<And>i. i \<in>\<^sub>\<circ> ?I \<Longrightarrow> ?i1 i \<in>\<^sub>\<circ> I) \<Longrightarrow> \<R>\<^sub>\<circ> (dghm_up ?I (\<lambda>i. \<AA> (?i1 i)) \<CC> (\<lambda>i. \<phi> (?i1 i))\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. \<AA> (?i1 i)\<lparr>Obj\<rparr>)
[PROOF STEP]
have rd: "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
(\<And>i. i \<in>\<^sub>\<circ> ?I \<Longrightarrow> ?i1 i \<in>\<^sub>\<circ> I) \<Longrightarrow> \<R>\<^sub>\<circ> (dghm_up ?I (\<lambda>i. \<AA> (?i1 i)) \<CC> (\<lambda>i. \<phi> (?i1 i))\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>?I. \<AA> (?i1 i)\<lparr>Obj\<rparr>)

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)
[PROOF STEP]
by (simp add: dg_prod_components dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ObjMap\<rparr>)

goal (3 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)
[PROOF STEP]
unfolding dghm_comp_components vdomain_vcomp_vsubset[OF rd]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>)

goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>)

goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>)
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ObjMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with dghm_up dghm_proj assms(3)
[PROOF STATE]
proof (chain)
picking this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
i \<in>\<^sub>\<circ> I
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
show
      "\<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
i \<in>\<^sub>\<circ> I
a \<in>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<phi> i\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. vsv (\<phi> i\<lparr>ObjMap\<rparr>)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<phi> i\<lparr>ObjMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
 2. \<CC> = \<CC>
 3. \<AA> i = \<AA> i
[PROOF STEP]
show "\<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
unfolding dghm_comp_components dghm_proj_components dghm_up_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<lambda>f\<in>\<^sub>\<circ>dg_prod I \<AA>\<lparr>Arr\<rparr>. f\<lparr>i\<rparr>) \<circ>\<^sub>\<circ> (\<lambda>f\<in>\<^sub>\<circ>\<CC>\<lparr>Arr\<rparr>. \<lambda>i\<in>\<^sub>\<circ>I. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>))
[PROOF STEP]
by (rule vsv_vcomp) simp_all
[PROOF STATE]
proof (state)
this:
vsv ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)

goal (3 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from
      dghm_up_ArrMap_vrange[
        OF assms(2), simplified, unfolded dg_prod_components
        ]
[PROOF STATE]
proof (chain)
picking this:
\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)
[PROOF STEP]
have rd: "\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Prod>\<^sub>\<circ>i\<in>\<^sub>\<circ>I. \<AA> i\<lparr>Arr\<rparr>)

goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by (simp add: dg_prod_components dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>) \<subseteq>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<pi>\<^sub>D\<^sub>G I \<AA> i\<lparr>ArrMap\<rparr>)

goal (3 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)
[PROOF STEP]
unfolding dghm_comp_components vdomain_vcomp_vsubset[OF rd]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> (dghm_up I \<AA> \<CC> \<phi>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>)

goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>)

goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>)
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by (simp add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (2 subgoals):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
 2. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<phi> i\<lparr>ArrMap\<rparr>) \<Longrightarrow> \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with dghm_up dghm_proj assms(3)
[PROOF STATE]
proof (chain)
picking this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
i \<in>\<^sub>\<circ> I
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show
      "\<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
dghm_up I \<AA> \<CC> \<phi> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> dg_prod I \<AA>
\<pi>\<^sub>D\<^sub>G I \<AA> i : dg_prod I \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<AA> i
i \<in>\<^sub>\<circ> I
a \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<phi> i\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. vsv (\<phi> i\<lparr>ArrMap\<rparr>)
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<phi> i\<lparr>ArrMap\<rparr> = (\<pi>\<^sub>D\<^sub>G I \<AA> i \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_up I \<AA> \<CC> \<phi>)\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. \<CC> = \<CC>
 2. \<AA> i = \<AA> i
[PROOF STEP]
qed simp_all