[STATEMENT]
lemma tdghm_dghm_comp_tdghm_dghm_comp_assoc:
  assumes "\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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 "(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> \<CC> \
 \<HH> \<HH>' \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<CC> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
interpret \<GG>: 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(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
interpret \<FF>: 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(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)
[PROOF STEP]
proof(rule tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>
[PROOF STEP]
show
      "(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \
"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

goal (6 subgoals):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>
 3. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = ?\<FF>'
 4. \<HH>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \
 = ?\<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>
 3. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = ?\<FF>'
 4. \<HH>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \
 = ?\<BB>'
[PROOF STEP]
show "\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \
"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

goal (5 subgoals):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>
 2. \<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>
 3. \<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>
 4. \<AA> = \<AA>
 5. \
 = \

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^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> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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> \

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (5 subgoals):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>
 2. \<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>
 3. \<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>
 4. \<AA> = \<AA>
 5. \
 = \

[PROOF STEP]
show
      "((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> =
        (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show
        "((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
          (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

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

goal (3 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>NTMap\<rparr> = (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>))\<lparr>NTMap\<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> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 2. \<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>
 3. \<AA> = \<AA>
 4. \
 = \

[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_tdghm) tdghm_tdghm_dghm_comp_dghm_id[dg_cs_simps]:
  "\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> = \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> = \<NN>
[PROOF STEP]
proof(rule tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. \<NN> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show "\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (6 subgoals):
 1. \<NN> : ?\<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 3. \<FF> = ?\<FF>'
 4. \<GG> = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \<BB> = ?\<BB>'
[PROOF STEP]
show "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>

goal (5 subgoals):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 2. \<FF> = \<FF>
 3. \<GG> = \<GG>
 4. \<AA> = \<AA>
 5. \<BB> = \<BB>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (5 subgoals):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 2. \<FF> = \<FF>
 3. \<GG> = \<GG>
 4. \<AA> = \<AA>
 5. \<BB> = \<BB>
[PROOF STEP]
show "(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dg_cs_simps)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>)
 2. vsv (\<NN>\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>)
 2. vsv (\<NN>\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>)
 2. vsv (\<NN>\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr>)
 2. vsv (\<NN>\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_intro: dg_cs_intros V_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M dghm_id \<AA>)\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. \<FF> = \<FF>
 2. \<GG> = \<GG>
 3. \<AA> = \<AA>
 4. \<BB> = \<BB>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma dghm_tdghm_comp_components:
  shows "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> =
    (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>)"
    and [dg_shared_cs_simps, dg_cs_simps]:
      "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>"
    and [dg_shared_cs_simps, dg_cs_simps]:
      "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr>"
    and [dg_shared_cs_simps, dg_cs_simps]:
      "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<NN>\<lparr>NTDGDom\<rparr>"
    and [dg_shared_cs_simps, dg_cs_simps]:
      "(\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<HH>\<lparr>HomCod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>) &&& (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>) &&& (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> &&& (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<NN>\<lparr>NTDGDom\<rparr> &&& (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<HH>\<lparr>HomCod\<rparr>
[PROOF STEP]
unfolding dghm_tdghm_comp_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr> &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<NN>\<lparr>3\<^sub>\<nat>\<rparr> &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = \<HH>\<lparr>HomCod\<rparr>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma dghm_tdghm_comp_NTMap_vrange:
  assumes "\<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<HH>: is_dghm \<alpha> \<BB> \<CC> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<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. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<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. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dghm_tdghm_comp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof(rule vrange_VLambda_vsubset, unfold dg_cs_simps)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
assume "x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
\<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr>\<rparr> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed