[STATEMENT]
lemma ntsmcf_hcomp_NTMap_vrange:
  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>"
  shows "\<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<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. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<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. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
assume "f \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
with ntsmcf_hcomp_NTMap_vdomain
[PROOF STATE]
proof (chain)
picking 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> \<Longrightarrow> \<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>
f \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
[PROOF STEP]
obtain a
    where a: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and f_def: "f = (\<MM> \<circ>\<^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:
?\<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> \<Longrightarrow> \<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>
f \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; f = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
unfolding ntsmcf_hcomp_components
[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> \<Longrightarrow> \<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>
f \<in>\<^sub>\<circ> \<R>\<^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>)

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>; f = (\<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>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
f = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
have \<FF>a: "\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: \<NN>.NTDom.smcf_ObjMap_app_in_HomCod_Obj a)
[PROOF STATE]
proof (state)
this:
\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<in>\<^sub>\<circ> \<BB>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
from \<NN>.ntsmcf_NTMap_is_arr[OF a]
[PROOF STATE]
proof (chain)
picking this:
\<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]
have "\<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> :
    \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<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. \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by (force intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
have "\<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr> : \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> \<GG>'\<lparr>ObjMap\<rparr>\<lparr>\<GG>\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>\<rparr>

goal (1 subgoal):
 1. \<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by
      (
        meson
          \<MM>.ntsmcf_NTMap_is_arr[OF \<FF>a]
          \<MM>.NTDom.HomCod.smc_is_arrE
          \<MM>.NTDom.HomCod.smc_Comp_is_arr
      )
[PROOF STATE]
proof (state)
this:
\<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. \<And>x. x \<in>\<^sub>\<circ> \<R>\<^sub>\<circ> ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<Longrightarrow> x \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
with a
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show "f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal (1 subgoal):
 1. f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding f_def ntsmcf_hcomp_components
[PROOF STATE]
proof (prove)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<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> \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
f \<in>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_hcomp_composable_commute:
  \<comment>\<open>See Chapter II-5 in \cite{mac_lane_categories_2010}.\<close>
  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 "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b"
  shows
    "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
      (\<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<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>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<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>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<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>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms(3)
[PROOF STATE]
proof (chain)
picking this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
have [simp]: "b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" and a: "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> &&& a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
b \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
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>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from \<MM>.is_ntsmcf_axioms \<NN>.is_ntsmcf_axioms
[PROOF STATE]
proof (chain)
picking this:
\<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>
\<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]
have \<MM>\<NN>b:
    "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> =
      (\<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr>) \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>)"
[PROOF STATE]
proof (prove)
using this:
\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>
[PROOF STEP]
by (auto simp: 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>b\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr>

goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
let ?\<GG>'\<FF>f = \<open>\<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr>\<close>
[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>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from a \<MM>.is_ntsmcf_axioms \<NN>.is_ntsmcf_axioms
[PROOF STATE]
proof (chain)
picking this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
\<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>
\<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]
have \<MM>\<NN>a:
    "(\<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)
using this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
\<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>
\<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> \<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]
by (cs_concl cs_shallow cs_simp: 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 (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
note \<MM>.NTCod.smcf_ArrMap_Comp[smc_cs_simps del]
[PROOF STATE]
proof (state)
this:
\<lbrakk>?g : ?b \<mapsto>\<^bsub>\<BB>\<^esub> ?c; ?f : ?a \<mapsto>\<^bsub>\<BB>\<^esub> ?b\<rbrakk> \<Longrightarrow> \<GG>'\<lparr>ArrMap\<rparr>\<lparr>?g \<circ>\<^sub>A\<^bsub>\<BB>\<^esub> ?f\<rparr> = \<GG>'\<lparr>ArrMap\<rparr>\<lparr>?g\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<GG>'\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr>

goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^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> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<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> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
unfolding \<MM>\<NN>b \<MM>\<NN>a
[PROOF STATE]
proof (prove)
using this:
\<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>
\<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. \<GG>'\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<MM>\<lparr>NTMap\<rparr>\<lparr>\<FF>\<lparr>ObjMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<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 (intro \<MM>.NTDom.HomCod.smc_pattern_rectangle_left)
      (
        cs_concl
          cs_simp: smc_cs_simps is_semifunctor.smcf_ArrMap_Comp[symmetric]
          cs_intro: smc_cs_intros
      )+
[PROOF STATE]
proof (state)
this:
(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_hcomp_is_ntsmcf:
  \<comment>\<open>See Chapter II-5 in \cite{mac_lane_categories_2010}.\<close>
  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>"
  shows "\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[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> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[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> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[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> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_ntsmcfI', unfold ntsmcf_hcomp_components(3,4))
[PROOF STATE]
proof (state)
goal (13 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
 3. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 5. vcard (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>
 6. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 7. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 8. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 9. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 10. vsv ((\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
unfolding ntsmcf_hcomp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<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>\<lparr>NTDom\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>, \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<MM>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
vfsequence (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)

goal (12 subgoals):
 1. \<Z> \<alpha>
 2. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. vcard (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>
 5. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 6. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 7. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 8. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 9. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 10. \<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>
A total of 12 subgoals...
[PROOF STEP]
show "vcard (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding ntsmcf_hcomp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<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>\<lparr>NTDom\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>, \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<MM>\<lparr>NTDGCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = 5\<^sub>\<nat>

goal (11 subgoals):
 1. \<Z> \<alpha>
 2. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 5. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 6. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 8. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 9. \<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>
 10. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
A total of 11 subgoals...
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> :
      (\<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" for a
[PROOF STATE]
proof (prove)
using this:
\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> : (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>?a\<rparr> : (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 5. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 6. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 8. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 9. \<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>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^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 (10 subgoals):
 1. \<Z> \<alpha>
 2. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 5. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 6. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 8. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 9. \<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>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^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 (10 subgoals):
 1. \<Z> \<alpha>
 2. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 5. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 6. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 8. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 9. \<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>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with ntsmcf_hcomp_composable_commute[OF assms]
[PROOF STATE]
proof (chain)
picking this:
?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b \<Longrightarrow> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b
[PROOF STEP]
show "(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
      (\<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^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:
?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b \<Longrightarrow> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDom\<rparr> = \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 5. \<MM>\<lparr>NTCod\<rparr> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr> = \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 6. \<NN>\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 8. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 9. \<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]
qed (auto simp: ntsmcf_hcomp_components(1) smc_cs_simps intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_hcomp_is_ntsmcf'[smc_cs_intros]:
  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 "\<SS> = \<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>"
    and "\<SS>' = \<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>"
  shows "\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<SS> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<SS>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<SS> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<SS>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<SS> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<SS>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
unfolding assms(3,4)
[PROOF STATE]
proof (prove)
using this:
\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule ntsmcf_hcomp_is_ntsmcf)


[STATEMENT]
lemma ntsmcf_hcomp_assoc[smc_cs_simps]:
  \<comment>\<open>See Chapter II-5 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<LL> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
    and "\<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>"
  shows "(\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>) \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<LL>: is_ntsmcf \<alpha> \<CC> \
 \<FF>'' \<GG>'' \<LL>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[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(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<LL>\<MM>: is_ntsmcf \<alpha> \<BB> \
 \<open>\<FF>'' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>'\<close> \<open>\<GG>'' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'\<close> \<open>\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> : \<FF>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<MM>\<NN>: is_ntsmcf \<alpha> \<AA> \<CC> \<open>\<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>\<close> \<open>\<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>\<close> \<open>\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
note smcf_axioms =
    \<LL>.NTDom.is_semifunctor_axioms
    \<LL>.NTCod.is_semifunctor_axioms
    \<MM>.NTDom.is_semifunctor_axioms
    \<MM>.NTCod.is_semifunctor_axioms
    \<NN>.NTDom.is_semifunctor_axioms
    \<NN>.NTCod.is_semifunctor_axioms
[PROOF STATE]
proof (state)
this:
\<FF>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<FF>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
proof(rule ntsmcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<LL> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<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>
\<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
      "\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> :
        (\<FF>'' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>') \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<GG>'' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>') \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> :
        \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
using this:
\<LL> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<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>
\<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. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

\<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]
have dom_lhs:
      "\<D>\<^sub>\<circ> ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<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)
using this:
\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> : \<FF>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<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. \<D>\<^sub>\<circ> ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

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

[PROOF STEP]
have dom_rhs:
      "\<D>\<^sub>\<circ> ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<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)
using this:
\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<LL> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by (simp add: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (6 subgoals):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>
 3. \<FF>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = ?\<FF>'
 4. \<GG>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = ?\<GG>'
 5. \<AA> = ?\<AA>'
 6. \
 = ?\<BB>'
[PROOF STEP]
show "(\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<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. (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>
[PROOF STEP]
proof(rule vsv_eqI, unfold dom_lhs dom_rhs)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
          (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> : \<FF>'' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>'' : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

\<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>
\<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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (simp_all add: ntsmcf_hcomp_components)
[PROOF STATE]
proof (state)
this:
(\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr> = (\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>

goal (5 subgoals):
 1. \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^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. \<FF>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> = ?\<FF>'
 3. \<GG>'' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> = ?\<GG>'
 4. \<AA> = ?\<AA>'
 5. \
 = ?\<BB>'
[PROOF STEP]
qed
    (
      insert smcf_axioms,
      auto simp: smcf_comp_assoc intro!: smc_cs_intros
    )
[PROOF STATE]
proof (state)
this:
\<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<LL> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma op_ntsmcf_ntsmcf_hcomp[smc_op_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>"
  shows "op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>
[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. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<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(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>
[PROOF STEP]
have op_\<MM>: "op_ntsmcf \<MM> :
    op_smcf \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' : op_smc \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>"
    and op_\<NN>: "op_ntsmcf \<NN> :
    op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf \<MM> : op_smcf \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' : op_smc \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC> &&& op_ntsmcf \<NN> : op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: smc_op_simps cs_intro: smc_cs_intros smc_op_intros
      )
[PROOF STATE]
proof (state)
this:
op_ntsmcf \<MM> : op_smcf \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' : op_smc \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>
op_ntsmcf \<NN> : op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<BB>

goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>
[PROOF STEP]
proof(rule sym, rule ntsmcf_eqI, unfold smc_op_simps slicing_simps)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN> : ?\<FF>2 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>2 : ?\<AA>2 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>?\<alpha>2\<^esub> ?\<BB>2
 2. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>'2 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>'2 : ?\<AA>'2 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>?\<alpha>2\<^esub> ?\<BB>'2
 3. (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr> = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>
 4. ?\<FF>2 = ?\<FF>'2
 5. ?\<GG>2 = ?\<GG>'2
 6. ?\<AA>2 = ?\<AA>'2
 7. ?\<BB>2 = ?\<BB>'2
[PROOF STEP]
show
      "op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN> :
        op_smcf \<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> :
        op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN> : op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: smc_op_simps cs_intro: smc_cs_intros smc_op_intros
        )
[PROOF STATE]
proof (state)
this:
op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN> : op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>

goal (6 subgoals):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>'2 \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>'2 : ?\<AA>'2 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'2
 2. (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr> = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>
 3. op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> = ?\<FF>'2
 4. op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> = ?\<GG>'2
 5. op_smc \<AA> = ?\<AA>'2
 6. op_smc \<CC> = ?\<BB>'2
[PROOF STEP]
show "op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) :
      op_smcf \<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF> :
      op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>
[PROOF STEP]
by
        (
          cs_concl cs_shallow
            cs_simp: smc_op_simps cs_intro: smc_cs_intros smc_op_intros
        )
[PROOF STATE]
proof (state)
this:
op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> : op_smc \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> op_smc \<CC>

goal (5 subgoals):
 1. (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr> = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>
 2. op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> = op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG>
 3. op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> = op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF>
 4. op_smc \<AA> = op_smc \<AA>
 5. op_smc \<CC> = op_smc \<CC>
[PROOF STEP]
show "(op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr> = (\<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. (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr> = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>
[PROOF STEP]
proof
      (
        rule vsv_eqI,
        unfold
          ntsmcf_hcomp_NTMap_vdomain[OF assms(2)]
          ntsmcf_hcomp_NTMap_vdomain[OF op_\<NN>]
          smc_op_simps
      )
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<circ>\<^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 ((op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<circ>\<^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> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<circ>\<^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> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<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
        "(op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<circ>\<^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> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<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. (op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<circ>\<^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 smc_op_simps
              cs_intro: smc_cs_intros smc_op_intros
          )
[PROOF STATE]
proof (state)
this:
(op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (auto simp: ntsmcf_hcomp_components)
[PROOF STATE]
proof (state)
this:
(op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>)\<lparr>NTMap\<rparr> = (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>

goal (4 subgoals):
 1. op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG> = op_smcf \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<GG>
 2. op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF> = op_smcf \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<FF>
 3. op_smc \<AA> = op_smc \<AA>
 4. op_smc \<CC> = op_smc \<CC>
[PROOF STEP]
qed simp_all
[PROOF STATE]
proof (state)
this:
op_ntsmcf (\<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = op_ntsmcf \<MM> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_ntsmcf \<NN>

goal:
No subgoals!
[PROOF STEP]
qed