[STATEMENT]
lemma (in is_tdghm) tdghm_NTMap_is_arr'[dg_cs_intros]:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
    and "A = \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
    and "B = \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
  shows "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : A \<mapsto>\<^bsub>\<BB>\<^esub> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : A \<mapsto>\<^bsub>\<BB>\<^esub> B
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : A \<mapsto>\<^bsub>\<BB>\<^esub> B
[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (rule tdghm_NTMap_is_arr)


[STATEMENT]
lemma (in is_tdghm) is_tdghm_axioms'[dg_cs_intros]:
  assumes "\<alpha>' = \<alpha>" and "\<AA>' = \<AA>" and "\<BB>' = \<BB>" and "\<FF>' = \<FF>" and "\<GG>' = \<GG>"
  shows "\<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]
unfolding assms
[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 is_tdghm_axioms)


[STATEMENT]
lemma tdghm_eqI:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN>' : \<FF>' \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>'"
    and "\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>"
    and "\<FF> = \<FF>'"
    and "\<GG> = \<GG>'"
    and "\<AA> = \<AA>'"
    and "\<BB> = \<BB>'"
  shows "\<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
interpret L: 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(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
interpret R: 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. \<NN> = \<NN>'
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
have dom: "\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
show "\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> \<NN>'

goal (3 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = \<NN>'\<lparr>a\<rparr>
[PROOF STEP]
from assms(4-7)
[PROOF STATE]
proof (chain)
picking this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'
[PROOF STEP]
have sup:
      "\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>" "\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>"
      "\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>" "\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'

goal (1 subgoal):
 1. (\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr> &&& \<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>) &&& \<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr> &&& \<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>
[PROOF STEP]
by (simp_all add: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>

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

goal (2 subgoals):
 1. vsv \<NN>
 2. vsv \<NN>'
[PROOF STEP]
qed (auto simp: L.vsv_axioms R.vsv_axioms)
[PROOF STATE]
proof (state)
this:
\<NN> = \<NN>'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_tdghm) tdghm_def:
  "\<NN> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: dg_cs_simps V_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
have dom_rhs:
    "\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>

goal (4 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
show
    "\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>"
[PROOF STATE]
proof (prove)
using this:
\<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
unfolding dom_lhs dom_rhs
[PROOF STATE]
proof (prove)
using this:
5\<^sub>\<nat> = 5\<^sub>\<nat>

goal (1 subgoal):
 1. 5\<^sub>\<nat> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> \<NN> = \<D>\<^sub>\<circ> [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>

goal (3 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
 3. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
show "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow>
    \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>"
    for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>a\<rparr>
[PROOF STEP]
by (unfold dom_lhs, elim_in_numeral, unfold nt_field_simps)
      (simp_all add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> \<NN> \<Longrightarrow> \<NN>\<lparr>?a\<rparr> = [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>\<lparr>?a\<rparr>

goal (2 subgoals):
 1. vsv \<NN>
 2. vsv [\<NN>\<lparr>NTMap\<rparr>, \<NN>\<lparr>NTDom\<rparr>, \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<NN>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
qed (auto simp: vsv_axioms)


[STATEMENT]
lemma (in is_tdghm) tdghm_NTMap_app_in_Arr[dg_cs_intros]:
  assumes "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
using tdghm_NTMap_is_arr
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by auto


[STATEMENT]
lemma (in is_tdghm) tdghm_NTMap_vrange_vifunion:
  "\<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> (\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>). Hom \<BB> a b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))
[PROOF STEP]
proof(intro NTMap.vsv_vrange_vsubset)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))
[PROOF STEP]
assume prems: "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> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))
[PROOF STEP]
note \<NN>x = tdghm_NTMap_is_arr[OF prems]
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>x\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))
[PROOF STEP]
from prems
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show
    "\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> (\<Union>\<^sub>\<circ>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ>b\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>). Hom \<BB> a b)"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))
[PROOF STEP]
by (intro vifunionI, unfold in_Hom_iff)
      (
        auto intro:
          dg_cs_intros NTDom.ObjMap.vsv_vimageI2' NTCod.ObjMap.vsv_vimageI2'
      )
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<Union>\<^sub>\<circ> ((\<lambda>a\<in>\<^sub>\<circ>\<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>). \<Union>\<^sub>\<circ> (VLambda (\<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>)) (Hom \<BB> a) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<GG>\<lparr>ObjMap\<rparr>))) `\<^sub>\<circ> \<R>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_tdghm) tdghm_NTMap_vrange: "\<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
proof(intro NTMap.vsv_vrange_vsubset)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<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> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<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> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
with is_tdghm_axioms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
x \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_tdghm) tdghm_NTMap_vsubset_Vset: "\<NN>\<lparr>NTMap\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
proof(intro NTMap.vbrelation_Limit_vsubset_VsetI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. Limit \<alpha>
 2. \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
 3. \<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "\<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> Vset \<alpha>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
by
      (
        rule vsubset_transitive,
        rule tdghm_NTMap_vrange,
        rule NTDom.HomCod.dg_Arr_vsubset_Vset
      )
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> Vset \<alpha>

goal (2 subgoals):
 1. Limit \<alpha>
 2. \<AA>\<lparr>Obj\<rparr> \<subseteq>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
qed (simp_all add: NTDom.HomDom.dg_Obj_vsubset_Vset)


[STATEMENT]
lemma (in is_tdghm) tdghm_NTMap_in_Vset:
  assumes "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<NN>\<lparr>NTMap\<rparr> \<in>\<^sub>\<circ> Vset \<beta>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> \<in>\<^sub>\<circ> Vset \<beta>
[PROOF STEP]
by (meson assms tdghm_NTMap_vsubset_Vset Vset_in_mono vsubset_in_VsetI)


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

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

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma (in is_tdghm) tdghm_is_tdghm_if_ge_Limit:
  assumes "\<Z> \<beta>" and "\<alpha> \<in>\<^sub>\<circ> \<beta>"
  shows "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^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>\<beta>\<^esub> \<BB>
[PROOF STEP]
proof(rule is_tdghmI)
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<NN>
 3. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> \<BB>
 4. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> \<BB>
 5. vcard \<NN> = 5\<^sub>\<nat>
 6. vsv (\<NN>\<lparr>NTMap\<rparr>)
 7. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 8. \<NN>\<lparr>NTDom\<rparr> = \<FF>
 9. \<NN>\<lparr>NTCod\<rparr> = \<GG>
 10. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
A total of 12 subgoals...
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>" if "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (11 subgoals):
 1. \<Z> \<beta>
 2. vfsequence \<NN>
 3. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> \<BB>
 4. \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<beta>\<^esub> \<BB>
 5. vcard \<NN> = 5\<^sub>\<nat>
 6. vsv (\<NN>\<lparr>NTMap\<rparr>)
 7. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 8. \<NN>\<lparr>NTDom\<rparr> = \<FF>
 9. \<NN>\<lparr>NTCod\<rparr> = \<GG>
 10. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
A total of 11 subgoals...
[PROOF STEP]
qed
  (
    cs_concl cs_shallow
      cs_simp: dg_cs_simps
      cs_intro:
        V_cs_intros
        assms NTDom.dghm_is_dghm_if_ge_Limit NTCod.dghm_is_dghm_if_ge_Limit
   )+


[STATEMENT]
lemma small_all_tdghms[simp]:
  "small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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. small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
proof(cases \<open>\<Z> \<alpha>\<close>)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
 2. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
case True
[PROOF STATE]
proof (state)
this:
\<Z> \<alpha>

goal (2 subgoals):
 1. \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}
 2. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
from is_tdghm.tdghm_in_Vset
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?\<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>; \<Z> ?\<beta>; ?\<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> ?\<NN> \<in>\<^sub>\<circ> Vset ?\<beta>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?\<NN> : ?\<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>?\<alpha>\<^esub> ?\<BB>; \<Z> ?\<beta>; ?\<alpha> \<in>\<^sub>\<circ> ?\<beta>\<rbrakk> \<Longrightarrow> ?\<NN> \<in>\<^sub>\<circ> Vset ?\<beta>

goal (1 subgoal):
 1. small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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 (intro down[of _ \<open>Vset (\<alpha> + \<omega>)\<close>])
      (auto simp: True \<Z>.\<Z>_Limit_\<alpha>\<omega> \<Z>.\<Z>_\<omega>_\<alpha>\<omega> \<Z>.intro \<Z>.\<Z>_\<alpha>_\<alpha>\<omega>)
[PROOF STATE]
proof (state)
this:
small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
case False
[PROOF STATE]
proof (state)
this:
\<not> \<Z> \<alpha>

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> \<Z> \<alpha>
[PROOF STEP]
have "{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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)
using this:
\<not> \<Z> \<alpha>

goal (1 subgoal):
 1. {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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 auto
[PROOF STATE]
proof (state)
this:
{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}

goal (1 subgoal):
 1. \<not> \<Z> \<alpha> \<Longrightarrow> small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
then
[PROOF STATE]
proof (chain)
picking this:
{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
{\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>} = {}

goal (1 subgoal):
 1. small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<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 simp
[PROOF STATE]
proof (state)
this:
small {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma small_tdghms[simp]: "small {\<NN>. \<exists>\<FF> \<GG>. \<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. small {\<NN>. \<exists>\<FF> \<GG>. \<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 down[of _ \<open>set {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}\<close>])
    auto


[STATEMENT]
lemma small_these_tdghms[simp]: "small {\<NN>. \<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. small {\<NN>. \<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 down[of _ \<open>set {\<NN>. \<exists>\<FF> \<GG> \<AA> \<BB>. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>}\<close>])
    auto


[STATEMENT]
lemma these_tdghms_iff(*not simp*):
  "\<NN> \<in>\<^sub>\<circ> these_tdghms \<alpha> \<AA> \<BB> \<FF> \<GG> \<longleftrightarrow> \<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> \<in>\<^sub>\<circ> these_tdghms \<alpha> \<AA> \<BB> \<FF> \<GG>) = \<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 auto


[STATEMENT]
lemma op_tdghm_components[dg_op_simps]:
  shows "op_tdghm \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>"
    and "op_tdghm \<NN>\<lparr>NTDom\<rparr> = op_dghm (\<NN>\<lparr>NTCod\<rparr>)"
    and "op_tdghm \<NN>\<lparr>NTCod\<rparr> = op_dghm (\<NN>\<lparr>NTDom\<rparr>)"
    and "op_tdghm \<NN>\<lparr>NTDGDom\<rparr> = op_dg (\<NN>\<lparr>NTDGDom\<rparr>)"
    and "op_tdghm \<NN>\<lparr>NTDGCod\<rparr> = op_dg (\<NN>\<lparr>NTDGCod\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_tdghm \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr> &&& op_tdghm \<NN>\<lparr>NTDom\<rparr> = op_dghm (\<NN>\<lparr>NTCod\<rparr>)) &&& op_tdghm \<NN>\<lparr>NTCod\<rparr> = op_dghm (\<NN>\<lparr>NTDom\<rparr>) &&& op_tdghm \<NN>\<lparr>NTDGDom\<rparr> = op_dg (\<NN>\<lparr>NTDGDom\<rparr>) &&& op_tdghm \<NN>\<lparr>NTDGCod\<rparr> = op_dg (\<NN>\<lparr>NTDGCod\<rparr>)
[PROOF STEP]
unfolding op_tdghm_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = \<NN>\<lparr>[]\<^sub>\<circ>\<rparr> &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = op_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>)) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = op_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = op_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>) &&& [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, op_dghm (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>), op_dghm (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>), op_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = op_dg (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>)
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma (in is_tdghm) is_tdghm_op:
  "op_tdghm \<NN> : op_dghm \<GG> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm \<NN> : op_dghm \<GG> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
proof(rule is_tdghmI, unfold dg_op_simps)
[PROOF STATE]
proof (state)
goal (12 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (op_tdghm \<NN>)
 3. op_dghm \<GG> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 4. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 5. vcard (op_tdghm \<NN>) = 5\<^sub>\<nat>
 6. vsv (\<NN>\<lparr>NTMap\<rparr>)
 7. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 8. op_dghm (\<NN>\<lparr>NTCod\<rparr>) = op_dghm \<GG>
 9. op_dghm (\<NN>\<lparr>NTDom\<rparr>) = op_dghm \<FF>
 10. op_dg (\<NN>\<lparr>NTDGDom\<rparr>) = op_dg \<AA>
A total of 12 subgoals...
[PROOF STEP]
show "vfsequence (op_tdghm \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (op_tdghm \<NN>)
[PROOF STEP]
by (simp add: op_tdghm_def)
[PROOF STATE]
proof (state)
this:
vfsequence (op_tdghm \<NN>)

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. op_dghm \<GG> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 3. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 4. vcard (op_tdghm \<NN>) = 5\<^sub>\<nat>
 5. vsv (\<NN>\<lparr>NTMap\<rparr>)
 6. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 7. op_dghm (\<NN>\<lparr>NTCod\<rparr>) = op_dghm \<GG>
 8. op_dghm (\<NN>\<lparr>NTDom\<rparr>) = op_dghm \<FF>
 9. op_dg (\<NN>\<lparr>NTDGDom\<rparr>) = op_dg \<AA>
 10. op_dg (\<NN>\<lparr>NTDGCod\<rparr>) = op_dg \<BB>
A total of 11 subgoals...
[PROOF STEP]
show "vcard (op_tdghm \<NN>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (op_tdghm \<NN>) = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: op_tdghm_def nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (op_tdghm \<NN>) = 5\<^sub>\<nat>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. op_dghm \<GG> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 3. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 4. vsv (\<NN>\<lparr>NTMap\<rparr>)
 5. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 6. op_dghm (\<NN>\<lparr>NTCod\<rparr>) = op_dghm \<GG>
 7. op_dghm (\<NN>\<lparr>NTDom\<rparr>) = op_dghm \<FF>
 8. op_dg (\<NN>\<lparr>NTDGDom\<rparr>) = op_dg \<AA>
 9. op_dg (\<NN>\<lparr>NTDGCod\<rparr>) = op_dg \<BB>
 10. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>" if "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: dg_cs_intros)
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> \<NN>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<GG>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. op_dghm \<GG> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 3. op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
 4. vsv (\<NN>\<lparr>NTMap\<rparr>)
 5. \<D>\<^sub>\<circ> (\<NN>\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 6. op_dghm (\<NN>\<lparr>NTCod\<rparr>) = op_dghm \<GG>
 7. op_dghm (\<NN>\<lparr>NTDom\<rparr>) = op_dghm \<FF>
 8. op_dg (\<NN>\<lparr>NTDGDom\<rparr>) = op_dg \<AA>
 9. op_dg (\<NN>\<lparr>NTDGCod\<rparr>) = op_dg \<BB>
[PROOF STEP]
qed
  (
    cs_concl cs_shallow
      cs_simp: dg_cs_simps cs_intro: dg_cs_intros dg_op_intros V_cs_intros
  )+


[STATEMENT]
lemma (in is_tdghm) tdghm_op_tdghm_op_tdghm[dg_op_simps]:
  "op_tdghm (op_tdghm \<NN>) = \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm (op_tdghm \<NN>) = \<NN>
[PROOF STEP]
proof(rule tdghm_eqI[of \<alpha> \<AA> \<BB> \<FF> \<GG> _ \<AA> \<BB> \<FF> \<GG>], unfold dg_op_simps)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. op_tdghm (op_tdghm \<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> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 4. \<FF> = \<FF>
 5. \<GG> = \<GG>
 6. \<AA> = \<AA>
 7. \<BB> = \<BB>
[PROOF STEP]
interpret op:
    is_tdghm \<alpha> \<open>op_dg \<AA>\<close> \<open>op_dg \<BB>\<close> \<open>op_dghm \<GG>\<close> \<open>op_dghm \<FF>\<close> \<open>op_tdghm \<NN>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm \<NN> : op_dghm \<GG> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<FF> : op_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg \<BB>
[PROOF STEP]
by (rule is_tdghm_op)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. op_tdghm (op_tdghm \<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> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<NN>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 4. \<FF> = \<FF>
 5. \<GG> = \<GG>
 6. \<AA> = \<AA>
 7. \<BB> = \<BB>
[PROOF STEP]
from op.is_tdghm_op
[PROOF STATE]
proof (chain)
picking this:
op_tdghm (op_tdghm \<NN>) : op_dghm (op_dghm \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm (op_dghm \<GG>) : op_dg (op_dg \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg (op_dg \<BB>)
[PROOF STEP]
show
    "op_tdghm (op_tdghm \<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)
using this:
op_tdghm (op_tdghm \<NN>) : op_dghm (op_dghm \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm (op_dghm \<GG>) : op_dg (op_dg \<AA>) \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> op_dg (op_dg \<BB>)

goal (1 subgoal):
 1. op_tdghm (op_tdghm \<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 (simp add: dg_op_simps)
[PROOF STATE]
proof (state)
this:
op_tdghm (op_tdghm \<NN>) : \<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>\<lparr>NTMap\<rparr> = \<NN>\<lparr>NTMap\<rparr>
 3. \<FF> = \<FF>
 4. \<GG> = \<GG>
 5. \<AA> = \<AA>
 6. \<BB> = \<BB>
[PROOF STEP]
qed (auto simp: dg_cs_intros)


[STATEMENT]
lemma eq_op_tdghm_iff:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    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 "op_tdghm \<NN> = op_tdghm \<NN>' \<longleftrightarrow> \<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (op_tdghm \<NN> = op_tdghm \<NN>') = (\<NN> = \<NN>')
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_tdghm \<NN> = op_tdghm \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_tdghm \<NN> = op_tdghm \<NN>'
[PROOF STEP]
interpret L: 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(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. op_tdghm \<NN> = op_tdghm \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_tdghm \<NN> = op_tdghm \<NN>'
[PROOF STEP]
interpret R: 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 (2 subgoals):
 1. op_tdghm \<NN> = op_tdghm \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_tdghm \<NN> = op_tdghm \<NN>'
[PROOF STEP]
assume prems: "op_tdghm \<NN> = op_tdghm \<NN>'"
[PROOF STATE]
proof (state)
this:
op_tdghm \<NN> = op_tdghm \<NN>'

goal (2 subgoals):
 1. op_tdghm \<NN> = op_tdghm \<NN>' \<Longrightarrow> \<NN> = \<NN>'
 2. \<NN> = \<NN>' \<Longrightarrow> op_tdghm \<NN> = op_tdghm \<NN>'
[PROOF STEP]
show "\<NN> = \<NN>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = \<NN>'
[PROOF STEP]
proof(rule tdghm_eqI[OF assms])
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
 2. \<FF> = \<FF>'
 3. \<GG> = \<GG>'
 4. \<AA> = \<AA>'
 5. \<BB> = \<BB>'
[PROOF STEP]
from prems L.tdghm_op_tdghm_op_tdghm R.tdghm_op_tdghm_op_tdghm
[PROOF STATE]
proof (chain)
picking this:
op_tdghm \<NN> = op_tdghm \<NN>'
op_tdghm (op_tdghm \<NN>) = \<NN>
op_tdghm (op_tdghm \<NN>') = \<NN>'
[PROOF STEP]
show
      "\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
using this:
op_tdghm \<NN> = op_tdghm \<NN>'
op_tdghm (op_tdghm \<NN>) = \<NN>
op_tdghm (op_tdghm \<NN>') = \<NN>'

goal (1 subgoal):
 1. \<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTMap\<rparr> = \<NN>'\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. \<FF> = \<FF>'
 2. \<GG> = \<GG>'
 3. \<AA> = \<AA>'
 4. \<BB> = \<BB>'
[PROOF STEP]
from prems L.tdghm_op_tdghm_op_tdghm R.tdghm_op_tdghm_op_tdghm
[PROOF STATE]
proof (chain)
picking this:
op_tdghm \<NN> = op_tdghm \<NN>'
op_tdghm (op_tdghm \<NN>) = \<NN>
op_tdghm (op_tdghm \<NN>') = \<NN>'
[PROOF STEP]
have "\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>"
      and "\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>"
      and "\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>"
      and "\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>"
[PROOF STATE]
proof (prove)
using this:
op_tdghm \<NN> = op_tdghm \<NN>'
op_tdghm (op_tdghm \<NN>) = \<NN>
op_tdghm (op_tdghm \<NN>') = \<NN>'

goal (1 subgoal):
 1. (\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr> &&& \<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>) &&& \<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr> &&& \<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>
[PROOF STEP]
by metis+
[PROOF STATE]
proof (state)
this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>

goal (4 subgoals):
 1. \<FF> = \<FF>'
 2. \<GG> = \<GG>'
 3. \<AA> = \<AA>'
 4. \<BB> = \<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>
[PROOF STEP]
show "\<FF> = \<FF>'" "\<GG> = \<GG>'" "\<AA> = \<AA>'" "\<BB> = \<BB>'"
[PROOF STATE]
proof (prove)
using this:
\<NN>\<lparr>NTDom\<rparr> = \<NN>'\<lparr>NTDom\<rparr>
\<NN>\<lparr>NTCod\<rparr> = \<NN>'\<lparr>NTCod\<rparr>
\<NN>\<lparr>NTDGDom\<rparr> = \<NN>'\<lparr>NTDGDom\<rparr>
\<NN>\<lparr>NTDGCod\<rparr> = \<NN>'\<lparr>NTDGCod\<rparr>

goal (1 subgoal):
 1. (\<FF> = \<FF>' &&& \<GG> = \<GG>') &&& \<AA> = \<AA>' &&& \<BB> = \<BB>'
[PROOF STEP]
by (auto simp: dg_cs_simps)
[PROOF STATE]
proof (state)
this:
\<FF> = \<FF>'
\<GG> = \<GG>'
\<AA> = \<AA>'
\<BB> = \<BB>'

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

goal (1 subgoal):
 1. \<NN> = \<NN>' \<Longrightarrow> op_tdghm \<NN> = op_tdghm \<NN>'
[PROOF STEP]
qed auto


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


[STATEMENT]
lemma tdghm_dghm_comp_NTMap_vrange:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> \<BB> \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<R>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<HH>: is_dghm \<alpha> \<AA> \<BB> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<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> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<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> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding tdghm_dghm_comp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>HomDom\<rparr>\<lparr>Obj\<rparr>. \<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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> \<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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> \<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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> \<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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 "\<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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. \<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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:
\<NN>\<lparr>NTMap\<rparr>\<lparr>\<HH>\<lparr>ObjMap\<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> ((\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed