[STATEMENT]
lemma ntsmcf_vcomp_components:
  shows
    "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> =
      (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> (\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>))"
    and [dg_shared_cs_simps, smc_cs_simps]: "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<NN>\<lparr>NTDom\<rparr>"
    and [dg_shared_cs_simps, smc_cs_simps]: "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<MM>\<lparr>NTCod\<rparr>"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<NN>\<lparr>NTDGDom\<rparr>"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<MM>\<lparr>NTDGCod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) &&& (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<NN>\<lparr>NTDom\<rparr>) &&& (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<MM>\<lparr>NTCod\<rparr> &&& (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<NN>\<lparr>NTDGDom\<rparr> &&& (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<MM>\<lparr>NTDGCod\<rparr>
[PROOF STEP]
unfolding nt_field_simps ntsmcf_vcomp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = \<NN>\<lparr>1\<^sub>\<nat>\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<MM>\<lparr>2\<^sub>\<nat>\<rparr> &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<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>. \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = \<MM>\<lparr>4\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma ntsmcf_vcomp_NTMap_vsv[dg_shared_cs_intros, smc_cs_intros]:
  "vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
unfolding ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
by simp


[STATEMENT]
lemma ntsmcf_vcomp_NTMap_vdomain[smc_cs_simps]:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_vcomp_NTMap_app[smc_cs_simps]:
  assumes "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<AA> \<BB> \<GG> \<HH> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_vcomp_NTMap_vrange:
  assumes "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) \<subseteq>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
proof(rule vrange_VLambda_vsubset)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr> \<Longrightarrow> \<MM>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<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> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr> \<Longrightarrow> \<MM>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
assume prems: "x \<in>\<^sub>\<circ> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
x \<in>\<^sub>\<circ> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr> \<Longrightarrow> \<MM>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
from prems assms
[PROOF STATE]
proof (chain)
picking this:
x \<in>\<^sub>\<circ> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show "\<MM>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
x \<in>\<^sub>\<circ> \<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_prems cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
      (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>x\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_vcomp_composable_commute[smc_cs_simps]:
  \<comment>\<open>See Chapter II-4 in \cite{mac_lane_categories_2010}).\<close>
  assumes "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
  shows
    "(\<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>) \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
      \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)"
    (is \<open>(?MC \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?NC) \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?R = ?T \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (?MD \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?ND)\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<AA> \<BB> \<GG> \<HH> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. \<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
by (intro \<MM>.NTDom.HomCod.smc_pattern_rectangle_left)
      (cs_concl cs_intro: smc_cs_intros cs_simp: \<NN>.ntsmcf_Comp_commute)
[PROOF STATE]
proof (state)
this:
\<MM>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_vcomp_is_ntsmcf[smc_cs_intros]:
  \<comment>\<open>See Chapter II-4 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<AA> \<BB> \<GG> \<HH> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
proof(intro is_ntsmcfI')
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
 3. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 5. vcard (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 8. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 9. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 10. vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
A total of 13 subgoals...
[PROOF STEP]
show "vfsequence (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
by (simp add: ntsmcf_vcomp_def)
[PROOF STATE]
proof (state)
this:
vfsequence (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. vcard (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 8. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 9. vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 10. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>
[PROOF STEP]
by (auto simp: nat_omega_simps ntsmcf_vcomp_def)
[PROOF STATE]
proof (state)
this:
vcard (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 8. vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 9. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 10. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
A total of 11 subgoals...
[PROOF STEP]
show "vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
unfolding ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vsv ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 8. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
show "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (
          use that in
            \<open>cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros\<close>
        )
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> : \<FF>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 8. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix f a b
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 8. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
[PROOF STATE]
proof (state)
this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 8. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show
      "(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
        \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: smc_cs_simps is_ntsmcf.ntsmcf_Comp_commute'
            cs_intro: smc_cs_intros
        )
[PROOF STATE]
proof (state)
this:
(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> \<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 3. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
 4. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>
 5. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<HH>
 6. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<BB>
 8. \<D>\<^sub>\<circ> ((\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (use assms in \<open>auto simp: smc_cs_simps ntsmcf_vcomp_NTMap_vrange\<close>)
[PROOF STATE]
proof (state)
this:
\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_vcomp_assoc[smc_cs_simps]:
  \<comment>\<open>See Chapter II-4 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<LL> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "(\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<LL>: is_ntsmcf \<alpha> \<AA> \<BB> \<HH> \<KK> \<LL>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<AA> \<BB> \<GG> \<HH> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
proof(rule ntsmcf_eqI[of \<alpha>])
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show "((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (4 subgoals):
 1. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
have "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. (\<lambda>a\<in>\<^sub>\<circ>\<MM>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<LL>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>NTDGCod\<rparr>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)

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

goal (4 subgoals):
 1. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<LL> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show
        "((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
          (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<LL> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
[PROOF STEP]
qed (simp_all add: ntsmcf_vcomp_components)
[PROOF STATE]
proof (state)
this:
(\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
[PROOF STEP]
qed (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_ntsmcf_ntsmcf_vcomp[smc_op_simps]:
  assumes "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<AA> \<BB> \<GG> \<HH> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>
[PROOF STEP]
proof(rule ntsmcf_eqI[of \<alpha>]; (intro symmetric)?)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>1 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>1 : ?\<AA>1 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>1
 2. op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM> : ?\<FF>'1 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>'1 : ?\<AA>'1 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'1
 3. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>
 4. ?\<FF>1 = ?\<FF>'1
 5. ?\<GG>1 = ?\<GG>'1
 6. ?\<AA>1 = ?\<AA>'1
 7. ?\<BB>1 = ?\<BB>'1
[PROOF STEP]
show "op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> =
      (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (4 subgoals):
 1. vsv (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
have a: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding smc_op_simps ntsmcf_vcomp_NTMap_vdomain[OF assms(2)]
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

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

goal (4 subgoals):
 1. vsv (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 4. \<And>a. a \<in>\<^sub>\<circ> \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with
        \<MM>.NTDom.HomCod.op_smc_Comp
        \<MM>.ntsmcf_NTMap_is_arr[OF a]
        \<NN>.ntsmcf_NTMap_is_arr[OF a]
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?f : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?c; ?g : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> ?f = ?f \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?g
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
\<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>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show "op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
        (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?c; ?g : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> ?f = ?f \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?g
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
\<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>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding smc_op_simps ntsmcf_vcomp_components
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?f : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?c; ?g : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b\<rbrakk> \<Longrightarrow> ?g \<circ>\<^sub>A\<^bsub>op_smc \<BB>\<^esub> ?f = ?f \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?g
\<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : \<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<BB>\<^esub> \<HH>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
\<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>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<NN>\<lparr>NTDGCod\<rparr>\<^esub> \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)\<lparr>a\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<MM>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>op_smc (\<MM>\<lparr>NTDGCod\<rparr>)\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>)\<lparr>a\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
 3. \<D>\<^sub>\<circ> (op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<D>\<^sub>\<circ> ((op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
qed (simp_all add: smc_op_simps smc_cs_simps ntsmcf_vcomp_components(1))
[PROOF STATE]
proof (state)
this:
op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>)\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>1 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>1 : ?\<AA>1 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>1
 2. op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM> : ?\<FF>'1 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>'1 : ?\<AA>'1 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'1
 3. ?\<FF>1 = ?\<FF>'1
 4. ?\<GG>1 = ?\<GG>'1
 5. ?\<AA>1 = ?\<AA>'1
 6. ?\<BB>1 = ?\<BB>'1
[PROOF STEP]
qed (auto intro: smc_cs_intros smc_op_intros)
[PROOF STATE]
proof (state)
this:
op_ntsmcf (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<MM>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_hcomp_components:
  shows
    "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> =
      (
        \<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>.
          (
            \<MM>\<lparr>NTCod\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>NTDGCod\<rparr>\<^esub>
            \<MM>\<lparr>NTMap\<rparr>\<lparr>\<NN>\<lparr>NTDom\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
          )
      )"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<MM>\<lparr>NTDom\<rparr> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>\<lparr>NTDom\<rparr>"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>\<lparr>NTCod\<rparr>"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<NN>\<lparr>NTDGDom\<rparr>"
    and [dg_shared_cs_simps, smc_cs_simps]:
      "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<MM>\<lparr>NTDGCod\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTCod\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>NTDGCod\<rparr>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<NN>\<lparr>NTDom\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>) &&& (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<MM>\<lparr>NTDom\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>) &&& (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTCod\<rparr> = \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> &&& (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGDom\<rparr> = \<NN>\<lparr>NTDGDom\<rparr> &&& (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<MM>\<lparr>NTDGCod\<rparr>
[PROOF STEP]
unfolding nt_field_simps ntsmcf_hcomp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<MM>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>) &&& [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<MM>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = \<MM>\<lparr>1\<^sub>\<nat>\<rparr> \<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>. \<MM>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<MM>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = \<MM>\<lparr>2\<^sub>\<nat>\<rparr> \<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>. \<MM>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<MM>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<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>. \<MM>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>4\<^sub>\<nat>\<rparr>\<^esub> \<MM>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<MM>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>1\<^sub>\<nat>\<rparr>, \<MM>\<lparr>2\<^sub>\<nat>\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<MM>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = \<MM>\<lparr>4\<^sub>\<nat>\<rparr>
[PROOF STEP]
by (auto simp: nat_omega_simps)


[STATEMENT]
lemma ntsmcf_hcomp_NTMap_vsv[smc_cs_intros]: "vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
unfolding ntsmcf_hcomp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTCod\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>NTDGCod\<rparr>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<NN>\<lparr>NTDom\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>)
[PROOF STEP]
by auto


[STATEMENT]
lemma ntsmcf_hcomp_NTMap_vdomain[smc_cs_simps]:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<D>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding ntsmcf_hcomp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTCod\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>NTDGCod\<rparr>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<NN>\<lparr>NTDom\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_hcomp_NTMap_app[smc_cs_simps]:
  assumes "\<MM> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
  shows "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
    \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<BB> \<CC> \<FF>' \<GG>' \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
unfolding ntsmcf_hcomp_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<MM>\<lparr>NTCod\<rparr>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<MM>\<lparr>NTDGCod\<rparr>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<NN>\<lparr>NTDom\<rparr>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>)\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed