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

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


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

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


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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_dghm_dghm_comp[dg_op_simps]:
  "op_dghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = op_dghm \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = op_dghm \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF>
[PROOF STEP]
unfolding dghm_comp_def op_dghm_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg ([\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg ([\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, \<FF>\<lparr>2\<^sub>\<nat>\<rparr>, \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ> = [[\<GG>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<GG>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<GG>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<GG>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<GG>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>, [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<GG>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<GG>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma dghm_comp_is_dghm[dg_cs_intros]:
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<BB> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_dghmI is_dghmI, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
 3. digraph \<alpha> \<AA>
 4. digraph \<alpha> \<CC>
 5. vcard (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) = 4\<^sub>\<nat>
 6. \<AA> = \<AA>
 7. \<CC> = \<CC>
 8. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 9. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
unfolding dghm_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<GG>\<lparr>ObjMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr>, \<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>, \<FF>\<lparr>HomDom\<rparr>, \<GG>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)

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

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
fix f a b
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
assume "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show "(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> :
      (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
qed
    (
      use assms in
        \<open>
          cs_concl cs_shallow
            cs_intro: dg_cs_intros dghm_comp_ObjMap_vrange
            cs_simp: dg_cs_simps
        \<close>
    )+
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_comp_assoc[dg_cs_simps]:
  assumes "\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \
" and "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
proof(rule dghm_eqI [of \<alpha> \<AA> \
 _ \<AA> \
])
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 5. \<AA> = \<AA>
 6. \
 = \

[PROOF STEP]
show "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

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

goal (3 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>) = \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>)
[PROOF STEP]
qed (use assms in \<open>cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros\<close>)+
[PROOF STATE]
proof (state)
this:
(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ObjMap\<rparr>

goal (5 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
 4. \<AA> = \<AA>
 5. \
 = \

[PROOF STEP]
show "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (cs_prems cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
        (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>\<lparr>?a\<rparr>

goal (3 subgoals):
 1. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>)
 2. vsv ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>) = \<D>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>)
[PROOF STEP]
qed
    (
      use assms in
        \<open>cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros\<close>
    )+
[PROOF STATE]
proof (state)
this:
(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>ArrMap\<rparr>

goal (4 subgoals):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

 3. \<AA> = \<AA>
 4. \
 = \

[PROOF STEP]
qed (use assms in \<open>cs_concl cs_shallow cs_intro: dg_cs_intros\<close>)+


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


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

goal:
No subgoals!
[PROOF STEP]
qed


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

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


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

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


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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by
    (
      cs_concl
        cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
        cs_intro: is_dghm.dghm_ArrMap_vrange
    )


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

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


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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal:
No subgoals!
[PROOF STEP]
qed


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

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


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

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


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

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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal:
No subgoals!
[PROOF STEP]
qed


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

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
by
    (
      cs_concl
        cs_simp: dghm_cn_comp_components dg_cs_simps dg_op_simps V_cs_simps
        cs_intro: is_dghm.dghm_ArrMap_vrange
    )


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

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


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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_dghm_dghm_cn_comp[dg_op_simps]:
  "op_dghm (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>) = op_dghm \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> op_dghm \<FF>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>) = op_dghm \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> op_dghm \<FF>
[PROOF STEP]
unfolding op_dghm_def dghm_cn_comp_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg ([\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg ([\<GG>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), \<GG>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ> = [[\<GG>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<GG>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<GG>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<GG>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<GG>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> [\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg ([\<FF>\<lparr>[]\<^sub>\<circ>\<rparr>, \<FF>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<FF>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<FF>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>), [\<GG>\<lparr>[]\<^sub>\<circ>\<rparr>, \<GG>\<lparr>1\<^sub>\<nat>\<rparr>, op_dg (\<GG>\<lparr>2\<^sub>\<nat>\<rparr>), op_dg (\<GG>\<lparr>3\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma dghm_cn_comp_is_dghm[dg_cn_cs_intros]:
  \<comment>\<open>See section 1.2 in \cite{bodo_categories_1970}.\<close>
  assumes "digraph \<alpha> \<AA>" and "\<GG> : \<BB> \<^sub>D\<^sub>G\<mapsto>\<mapsto>\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<^sub>D\<^sub>G\<mapsto>\<mapsto>\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<AA>: digraph \<alpha> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digraph \<alpha> \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<open>op_dg \<BB>\<close> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<open>op_dg \<AA>\<close> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms(3)
[PROOF STATE]
proof (prove)
using this:
\<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_dghmI, unfold dg_op_simps dg_cs_simps dg_cn_cs_simps)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)
 3. digraph \<alpha> \<AA>
 4. digraph \<alpha> \<CC>
 5. vcard (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>) = 4\<^sub>\<nat>
 6. \<AA> = \<AA>
 7. \<CC> = \<CC>
 8. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 9. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)
[PROOF STEP]
unfolding dghm_cn_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<GG>\<lparr>ObjMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr>, \<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>, op_dg (\<FF>\<lparr>HomDom\<rparr>), \<GG>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)

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

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
fix f a b
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
assume "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
digraph \<alpha> \<AA>
\<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show "(\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> :
      (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
digraph \<alpha> \<AA>
\<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: dg_cn_cs_simps
            cs_intro: dg_cs_intros dg_op_intros
        )
[PROOF STATE]
proof (state)
this:
(\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<AA>
 3. digraph \<alpha> \<CC>
 4. \<AA> = \<AA>
 5. \<CC> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
qed
    (
      cs_concl
        cs_simp: dg_cs_simps dg_cn_cs_simps
        cs_intro: dghm_cn_comp_ObjMap_vrange dg_cs_intros dg_cn_cs_intros
    )+
[PROOF STATE]
proof (state)
this:
\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_cn_cov_comp_is_dghm[dg_cn_cs_intros]:
  \<comment>\<open>See section 1.2 in \cite{bodo_categories_1970}.\<close>
  assumes "\<GG> : \<BB> \<^sub>D\<^sub>G\<mapsto>\<mapsto>\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : \<AA> \<^sub>D\<^sub>G\<mapsto>\<mapsto>\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret L: is_dghm \<alpha> \<open>op_dg \<BB>\<close> \<CC> \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret R: is_dghm \<alpha> \<AA> \<BB> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_dghmI, unfold dg_op_simps dg_cs_simps)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)
 3. digraph \<alpha> (op_dg \<AA>)
 4. digraph \<alpha> \<CC>
 5. vcard (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>) = 4\<^sub>\<nat>
 6. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomDom\<rparr> = op_dg \<AA>
 7. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomCod\<rparr> = \<CC>
 8. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 9. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)
[PROOF STEP]
unfolding dghm_cn_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<GG>\<lparr>ObjMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ObjMap\<rparr>, \<GG>\<lparr>ArrMap\<rparr> \<circ>\<^sub>\<circ> \<FF>\<lparr>ArrMap\<rparr>, op_dg (\<FF>\<lparr>HomDom\<rparr>), \<GG>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)

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

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (op_dg \<AA>)
 3. digraph \<alpha> \<CC>
 4. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomDom\<rparr> = op_dg \<AA>
 5. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomCod\<rparr> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
fix f b a
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (op_dg \<AA>)
 3. digraph \<alpha> \<CC>
 4. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomDom\<rparr> = op_dg \<AA>
 5. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomCod\<rparr> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
assume "f : b \<mapsto>\<^bsub>\<AA>\<^esub> a"
[PROOF STATE]
proof (state)
this:
f : b \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (op_dg \<AA>)
 3. digraph \<alpha> \<CC>
 4. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomDom\<rparr> = op_dg \<AA>
 5. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomCod\<rparr> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
f : b \<mapsto>\<^bsub>\<AA>\<^esub> a
[PROOF STEP]
show "(\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> :
      (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<GG> : op_dg \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
f : b \<mapsto>\<^bsub>\<AA>\<^esub> a

goal (1 subgoal):
 1. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cn_cs_simps dg_op_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> : (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> (op_dg \<AA>)
 3. digraph \<alpha> \<CC>
 4. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomDom\<rparr> = op_dg \<AA>
 5. (\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>HomCod\<rparr> = \<CC>
 6. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>)
 7. vsv ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>)
 8. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<R>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ObjMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<D>\<^sub>\<circ> ((\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF>)\<lparr>ArrMap\<rparr>) = \<AA>\<lparr>Arr\<rparr>
[PROOF STEP]
qed
    (
      cs_concl cs_shallow
        cs_simp: dg_cs_simps dg_cn_cs_simps
        cs_intro:
          dghm_cn_cov_comp_ObjMap_vrange
          dg_cs_intros dg_cn_cs_intros dg_op_intros
    )+
[PROOF STATE]
proof (state)
this:
\<GG> \<^sub>D\<^sub>G\<^sub>H\<^sub>M\<circ> \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma dghm_cov_cn_comp_is_dghm:
  \<comment>\<open>See section 1.2 in \cite{bodo_categories_1970}\<close>
  assumes "\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<FF> : \<AA> \<^sub>D\<^sub>G\<mapsto>\<mapsto>\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<^sub>D\<^sub>G\<mapsto>\<mapsto>\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule dghm_comp_is_dghm)


[STATEMENT]
lemma dghm_id_components:
  shows "dghm_id \<CC>\<lparr>ObjMap\<rparr> = vid_on (\<CC>\<lparr>Obj\<rparr>)"
    and "dghm_id \<CC>\<lparr>ArrMap\<rparr> = vid_on (\<CC>\<lparr>Arr\<rparr>)"
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_id \<CC>\<lparr>HomDom\<rparr> = \<CC>"
    and [dg_shared_cs_simps, dg_cs_simps]: "dghm_id \<CC>\<lparr>HomCod\<rparr> = \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (dghm_id \<CC>\<lparr>ObjMap\<rparr> = vid_on (\<CC>\<lparr>Obj\<rparr>) &&& dghm_id \<CC>\<lparr>ArrMap\<rparr> = vid_on (\<CC>\<lparr>Arr\<rparr>)) &&& dghm_id \<CC>\<lparr>HomDom\<rparr> = \<CC> &&& dghm_id \<CC>\<lparr>HomCod\<rparr> = \<CC>
[PROOF STEP]
unfolding dghm_id_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([vid_on (\<CC>\<lparr>Obj\<rparr>), vid_on (\<CC>\<lparr>Arr\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = vid_on (\<CC>\<lparr>Obj\<rparr>) &&& [vid_on (\<CC>\<lparr>Obj\<rparr>), vid_on (\<CC>\<lparr>Arr\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = vid_on (\<CC>\<lparr>Arr\<rparr>)) &&& [vid_on (\<CC>\<lparr>Obj\<rparr>), vid_on (\<CC>\<lparr>Arr\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<CC> &&& [vid_on (\<CC>\<lparr>Obj\<rparr>), vid_on (\<CC>\<lparr>Arr\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<CC>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma dghm_id_ObjMap_vrange[dg_shared_cs_simps, dg_cs_simps]:
  "\<R>\<^sub>\<circ> (dghm_id \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_id \<CC>\<lparr>ObjMap\<rparr>) = \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding dghm_id_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (vid_on (\<CC>\<lparr>Obj\<rparr>)) = \<CC>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma dghm_id_ArrMap_vrange[dg_shared_cs_simps, dg_cs_simps]:
  "\<R>\<^sub>\<circ> (dghm_id \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (dghm_id \<CC>\<lparr>ArrMap\<rparr>) = \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dghm_id_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (vid_on (\<CC>\<lparr>Arr\<rparr>)) = \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by simp


[STATEMENT]
lemma op_dghm_dghm_id[dg_op_simps]: "op_dghm (dghm_id \<CC>) = dghm_id (op_dg \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_dghm (dghm_id \<CC>) = dghm_id (op_dg \<CC>)
[PROOF STEP]
unfolding dghm_id_def op_dg_def op_dghm_def dghm_field_simps dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [vid_on (\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on (\<CC>\<lparr>1\<^sub>\<nat>\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [vid_on ([\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>), vid_on ([\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>), [\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma (in digraph) dg_dghm_id_is_dghm: "dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<CC> : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_dghmI, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (dghm_id \<CC>)
 3. digraph \<alpha> \<CC>
 4. digraph \<alpha> \<CC>
 5. vcard (dghm_id \<CC>) = 4\<^sub>\<nat>
 6. \<CC> = \<CC>
 7. \<CC> = \<CC>
 8. vsv (dghm_id \<CC>\<lparr>ObjMap\<rparr>)
 9. vsv (dghm_id \<CC>\<lparr>ArrMap\<rparr>)
 10. \<CC>\<lparr>Obj\<rparr> = \<CC>\<lparr>Obj\<rparr>
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (dghm_id \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (dghm_id \<CC>)
[PROOF STEP]
unfolding dghm_id_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [vid_on (\<CC>\<lparr>Obj\<rparr>), vid_on (\<CC>\<lparr>Arr\<rparr>), \<CC>, \<CC>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (dghm_id \<CC>)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> \<CC>
 4. vcard (dghm_id \<CC>) = 4\<^sub>\<nat>
 5. \<CC> = \<CC>
 6. \<CC> = \<CC>
 7. vsv (dghm_id \<CC>\<lparr>ObjMap\<rparr>)
 8. vsv (dghm_id \<CC>\<lparr>ArrMap\<rparr>)
 9. \<CC>\<lparr>Obj\<rparr> = \<CC>\<lparr>Obj\<rparr>
 10. \<CC>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (dghm_id \<CC>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (dghm_id \<CC>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_id_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [vid_on (\<CC>\<lparr>Obj\<rparr>), vid_on (\<CC>\<lparr>Arr\<rparr>), \<CC>, \<CC>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (dghm_id \<CC>) = 4\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. digraph \<alpha> \<CC>
 3. digraph \<alpha> \<CC>
 4. \<CC> = \<CC>
 5. \<CC> = \<CC>
 6. vsv (dghm_id \<CC>\<lparr>ObjMap\<rparr>)
 7. vsv (dghm_id \<CC>\<lparr>ArrMap\<rparr>)
 8. \<CC>\<lparr>Obj\<rparr> = \<CC>\<lparr>Obj\<rparr>
 9. \<CC>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Obj\<rparr>
 10. \<CC>\<lparr>Arr\<rparr> = \<CC>\<lparr>Arr\<rparr>
A total of 11 subgoals...
[PROOF STEP]
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros V_cs_intros)+


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