[STATEMENT]
lemma smcf_ntsmcf_comp_is_ntsmcf[intro]:
  assumes "\<HH> : \<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 "\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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 \<HH>: is_semifunctor \<alpha> \<BB> \<CC> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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(rule is_ntsmcfI)
[PROOF STATE]
proof (state)
goal (11 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
 3. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<HH> \<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 (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = 5\<^sub>\<nat>
 6. ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
 7. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 8. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 9. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 10. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
A total of 11 subgoals...
[PROOF STEP]
show "vfsequence (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
unfolding dghm_tdghm_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)

goal (10 subgoals):
 1. \<Z> \<alpha>
 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<HH> \<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 (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = 5\<^sub>\<nat>
 5. ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
 6. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 7. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 8. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 9. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 10. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<HH> : \<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 "\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
using this:
\<HH> : \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. vcard (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = 5\<^sub>\<nat>
 4. ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
 5. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 6. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 7. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 8. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 9. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<HH> : \<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 "\<HH> \<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)
using this:
\<HH> : \<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. \<HH> \<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 (cs_concl cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. vcard (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = 5\<^sub>\<nat>
 3. ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 5. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 6. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 7. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 8. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "vcard (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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 (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding dghm_tdghm_comp_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTDom\<rparr>, \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>\<lparr>NTCod\<rparr>, \<NN>\<lparr>NTDGDom\<rparr>, \<HH>\<lparr>HomCod\<rparr>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = 5\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 5. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 6. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 7. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<HH> : \<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 "ntsmcf_tdghm (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) :
      smcf_dghm (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>) :
      smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>"
[PROOF STATE]
proof (prove)
using this:
\<HH> : \<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. ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: slicing_commute[symmetric]
            cs_intro: dg_cs_intros slicing_intros
        )
[PROOF STATE]
proof (state)
this:
ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>

goal (6 subgoals):
 1. \<Z> \<alpha>
 2. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 5. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 6. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
have [smc_cs_simps]:
      "\<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> =
        \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>"
      if "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
\<HH> : \<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. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<GG>\<lparr>ArrMap\<rparr>\<lparr>f\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp:
              is_ntsmcf.ntsmcf_Comp_commute
              is_semifunctor.smcf_ArrMap_Comp[symmetric]
            cs_intro: smc_cs_intros
        )
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b \<Longrightarrow> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>?b\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<FF>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr>\<rparr> = \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<GG>\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr>\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>\<rparr>

goal (6 subgoals):
 1. \<Z> \<alpha>
 2. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 5. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
 6. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<HH> : \<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
      "(\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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> (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
        (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
      if "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
using this:
\<HH> : \<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. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using assms that
[PROOF STATE]
proof (prove)
using this:
\<HH> : \<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>
\<HH> : \<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. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b \<Longrightarrow> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>

goal (5 subgoals):
 1. \<Z> \<alpha>
 2. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDom\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF>
 3. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTCod\<rparr> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG>
 4. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGDom\<rparr> = \<AA>
 5. (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
qed (auto simp: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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 smcf_ntsmcf_comp_is_semifunctor'[smc_cs_intros]:
  assumes "\<HH> : \<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 "\<FF>' = \<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>"
    and "\<GG>' = \<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>"
  shows "\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<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:
\<HH> : \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<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:
\<HH> : \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<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]
..


[STATEMENT]
lemma smcf_comp_smcf_ntsmcf_comp_assoc:
  assumes "\<NN> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
  shows "(\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>) \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
proof(rule ntsmcf_tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>'
 7. ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<HH> \<HH>' \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<HH> \<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 (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>'
 7. ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))
[PROOF STEP]
interpret \<FF>: is_semifunctor \<alpha> \<BB> \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>'
 7. ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))
[PROOF STEP]
interpret \<GG>: is_semifunctor \<alpha> \<CC> \
 \<GG>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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>'
 7. ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show "(\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>) \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> :
    \<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

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

[PROOF STEP]
show "\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) :
    \<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \
"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
by (cs_concl cs_shallow cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) : \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (5 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>'
 3. \<AA> = \<AA>
 4. \
 = \

 5. ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<NN> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

[PROOF STEP]
show
    "ntsmcf_tdghm (\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) =
      ntsmcf_tdghm (\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))"
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<FF> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<GG> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \

goal (1 subgoal):
 1. ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))
[PROOF STEP]
by
      (
        cs_concl
          cs_simp: slicing_commute[symmetric]
          cs_intro: slicing_intros dghm_comp_dghm_tdghm_comp_assoc
      )
[PROOF STATE]
proof (state)
this:
ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))

goal (4 subgoals):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 2. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>' = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>'
 3. \<AA> = \<AA>
 4. \
 = \

[PROOF STEP]
qed simp_all


[STATEMENT]
lemma (in is_ntsmcf) ntsmcf_smcf_ntsmcf_comp_smcf_id[smc_cs_simps]:
  "smcf_id \<BB> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> = \<NN>
[PROOF STEP]
proof(rule ntsmcf_tdghm_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<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>'
 7. ntsmcf_tdghm (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm \<NN>
[PROOF STEP]
show "smcf_id \<BB> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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 (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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 (6 subgoals):
 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>'
 2. \<FF> = ?\<FF>'
 3. \<GG> = ?\<GG>'
 4. \<AA> = ?\<AA>'
 5. \<BB> = ?\<BB>'
 6. ntsmcf_tdghm (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm \<NN>
[PROOF STEP]
show "\<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 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 (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
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 (5 subgoals):
 1. \<FF> = \<FF>
 2. \<GG> = \<GG>
 3. \<AA> = \<AA>
 4. \<BB> = \<BB>
 5. ntsmcf_tdghm (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm \<NN>
[PROOF STEP]
show "ntsmcf_tdghm (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm \<NN>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntsmcf_tdghm (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm \<NN>
[PROOF STEP]
by
      (
        cs_concl cs_shallow
          cs_simp: slicing_simps slicing_commute[symmetric]
          cs_intro: smc_cs_intros slicing_intros dg_cs_simps
      )
[PROOF STATE]
proof (state)
this:
ntsmcf_tdghm (dghm_id \<BB> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>) = ntsmcf_tdghm \<NN>

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


[STATEMENT]
lemma smcf_ntsmcf_comp_ntsmcf_smcf_comp_assoc:
  assumes "\<NN> : \<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 "\<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<DD>"
    and "\<KK> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "(\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<KK> = \<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<KK>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<BB> \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret \<HH>: is_semifunctor \<alpha> \<CC> \<DD> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<CC> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<DD>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
interpret \<KK>: is_semifunctor \<alpha> \<AA> \<BB> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<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. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)
[PROOF STEP]
by (rule ntsmcf_tdghm_eqI)
      (
        use assms in
          \<open>
            cs_concl
              cs_simp: smc_cs_simps slicing_commute[symmetric]
              cs_intro:
                smc_cs_intros
                slicing_intros
                dghm_tdghm_comp_tdghm_dghm_comp_assoc
          \<close>
      )+
[PROOF STATE]
proof (state)
this:
\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK> = \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<KK>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma smcf_ntsmcf_comp_ntsmcf_vcomp:
  assumes "\<KK> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    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
    "\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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>) =
      (\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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 (\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
interpret \<KK>: is_semifunctor \<alpha> \<BB> \<CC> \<KK>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> : \<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. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
show
    "\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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>) = \<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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 (\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
proof(rule ntsmcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<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. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> = (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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>) = \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<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 dghm_tdghm_comp_components smc_cs_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<AA>\<lparr>Obj\<rparr>. \<KK>\<lparr>ArrMap\<rparr>\<lparr>(\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

goal (7 subgoals):
 1. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<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. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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. (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> = (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
have dom_rhs:
      "\<D>\<^sub>\<circ> ((\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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 (\<KK> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^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> ((\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding ntsmcf_vcomp_components smc_cs_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<AA>\<lparr>Obj\<rparr>. (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>) = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>) = \<AA>\<lparr>Obj\<rparr>

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

goal (1 subgoal):
 1. (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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:
(\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 2. vsv ((\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (cs_concl cs_shallow cs_intro: smc_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> = (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>))\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<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. \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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 (cs_concl cs_shallow cs_intro: smc_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<KK> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Or_Some: "(e1 OR e2) = Some x \<longleftrightarrow> e1 = Some x \<or> (e1 = None \<and> e2 = Some x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e1 OR e2 = Some x) = (e1 = Some x \<or> e1 = None \<and> e2 = Some x)
[PROOF STEP]
by(auto split: option.split)


[STATEMENT]
lemma Or_None: "(e1 OR e2) = None \<longleftrightarrow> e1 = None \<and> e2 = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (e1 OR e2 = None) = (e1 = None \<and> e2 = None)
[PROOF STEP]
by(auto split: option.split)


[STATEMENT]
lemma lift2_option_not_None: "lift2_option f x y \<noteq> None \<longleftrightarrow> (x \<noteq> None \<and> y \<noteq> None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lift2_option f x y \<noteq> None) = (x \<noteq> None \<and> y \<noteq> None)
[PROOF STEP]
using lift2_option.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>lift2_option ?x ?xa ?xb = ?y; \<And>uu_ uv_. \<lbrakk>?x = uu_; ?xa = None; ?xb = uv_; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>uw_ v. \<lbrakk>?x = uw_; ?xa = Some v; ?xb = None; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>f x y. \<lbrakk>?x = f; ?xa = Some x; ?xb = Some y; ?y = Some (f x y)\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (lift2_option f x y \<noteq> None) = (x \<noteq> None \<and> y \<noteq> None)
[PROOF STEP]
by blast


[STATEMENT]
lemma lift2_option_None: "lift2_option f x y = None \<longleftrightarrow> (x = None \<or> y = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lift2_option f x y = None) = (x = None \<or> y = None)
[PROOF STEP]
using lift2_option.elims
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>lift2_option ?x ?xa ?xb = ?y; \<And>uu_ uv_. \<lbrakk>?x = uu_; ?xa = None; ?xb = uv_; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>uw_ v. \<lbrakk>?x = uw_; ?xa = Some v; ?xb = None; ?y = None\<rbrakk> \<Longrightarrow> ?P; \<And>f x y. \<lbrakk>?x = f; ?xa = Some x; ?xb = Some y; ?y = Some (f x y)\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. (lift2_option f x y = None) = (x = None \<or> y = None)
[PROOF STEP]
by blast


[STATEMENT]
lemma findD:
  "find f xs = Some p \<Longrightarrow> \<exists>x \<in> set xs. f x = Some p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Preliminaries.find f xs = Some p \<Longrightarrow> \<exists>x\<in>set xs. f x = Some p
[PROOF STEP]
by(induction xs arbitrary: p) (auto split: option.splits)


[STATEMENT]
lemma find_None:
  "find f xs = None \<longleftrightarrow> (\<forall>x \<in> set xs. f x = None)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (Preliminaries.find f xs = None) = (\<forall>x\<in>set xs. f x = None)
[PROOF STEP]
by(induction xs) (auto split: option.splits)


[STATEMENT]
lemma find_ListFind: "find f l = Option.bind (List.find (\<lambda>x. case f x of None \<Rightarrow> False | _ \<Rightarrow> True) l) f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Preliminaries.find f l = Option.bind (List.find (\<lambda>x. case f x of None \<Rightarrow> False | Some a \<Rightarrow> True) l) f
[PROOF STEP]
by (induction l) (auto split: option.split)


[STATEMENT]
lemma "List.find P l = Some p \<Longrightarrow> \<exists>p \<in> set l . P p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.find P l = Some p \<Longrightarrow> \<exists>p\<in>set l. P p
[PROOF STEP]
by (induction l) (auto split: if_splits)


[STATEMENT]
lemma find_the_pair:
  assumes "distinct (map fst pairs)"
    and "\<And>x y. x\<in>set (map fst pairs) \<Longrightarrow> y\<in>set (map fst pairs) \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
    and "(x,y) \<in> set pairs" and "P x"
  shows "List.find (\<lambda>(x,_) . P x) pairs = Some (x,y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
[PROOF STEP]
using assms(1-3)
[PROOF STATE]
proof (prove)
using this:
distinct (map fst pairs)
\<lbrakk>?x \<in> set (map fst pairs); ?y \<in> set (map fst pairs); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set pairs

goal (1 subgoal):
 1. List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
[PROOF STEP]
proof (induction pairs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>distinct (map fst []); \<And>x y. \<lbrakk>x \<in> set (map fst []); y \<in> set (map fst []); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set []\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) [] = Some (x, y)
 2. \<And>a pairs. \<lbrakk>\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y); distinct (map fst (a # pairs)); \<And>x y. \<lbrakk>x \<in> set (map fst (a # pairs)); y \<in> set (map fst (a # pairs)); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set (a # pairs)\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) (a # pairs) = Some (x, y)
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
distinct (map fst [])
\<lbrakk>?x \<in> set (map fst []); ?y \<in> set (map fst []); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set []

goal (2 subgoals):
 1. \<lbrakk>distinct (map fst []); \<And>x y. \<lbrakk>x \<in> set (map fst []); y \<in> set (map fst []); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set []\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) [] = Some (x, y)
 2. \<And>a pairs. \<lbrakk>\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y); distinct (map fst (a # pairs)); \<And>x y. \<lbrakk>x \<in> set (map fst (a # pairs)); y \<in> set (map fst (a # pairs)); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set (a # pairs)\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) (a # pairs) = Some (x, y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct (map fst [])
\<lbrakk>?x \<in> set (map fst []); ?y \<in> set (map fst []); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct (map fst [])
\<lbrakk>?x \<in> set (map fst []); ?y \<in> set (map fst []); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set []

goal (1 subgoal):
 1. List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) [] = Some (x, y)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) [] = Some (x, y)

goal (1 subgoal):
 1. \<And>a pairs. \<lbrakk>\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y); distinct (map fst (a # pairs)); \<And>x y. \<lbrakk>x \<in> set (map fst (a # pairs)); y \<in> set (map fst (a # pairs)); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set (a # pairs)\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) (a # pairs) = Some (x, y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a pairs. \<lbrakk>\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y); distinct (map fst (a # pairs)); \<And>x y. \<lbrakk>x \<in> set (map fst (a # pairs)); y \<in> set (map fst (a # pairs)); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set (a # pairs)\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) (a # pairs) = Some (x, y)
[PROOF STEP]
case (Cons pair pairs)
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) pairs = Some (x, y)
distinct (map fst (pair # pairs))
\<lbrakk>?x \<in> set (map fst (pair # pairs)); ?y \<in> set (map fst (pair # pairs)); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set (pair # pairs)

goal (1 subgoal):
 1. \<And>a pairs. \<lbrakk>\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y); distinct (map fst (a # pairs)); \<And>x y. \<lbrakk>x \<in> set (map fst (a # pairs)); y \<in> set (map fst (a # pairs)); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set (a # pairs)\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) (a # pairs) = Some (x, y)
[PROOF STEP]
thm Cons.prems
[PROOF STATE]
proof (state)
this:
\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) pairs = Some (x, y)
distinct (map fst (pair # pairs))
\<lbrakk>?x \<in> set (map fst (pair # pairs)); ?y \<in> set (map fst (pair # pairs)); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set (pair # pairs)

goal (1 subgoal):
 1. \<And>a pairs. \<lbrakk>\<lbrakk>distinct (map fst pairs); \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set pairs\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y); distinct (map fst (a # pairs)); \<And>x y. \<lbrakk>x \<in> set (map fst (a # pairs)); y \<in> set (map fst (a # pairs)); P x; P y\<rbrakk> \<Longrightarrow> x = y; (x, y) \<in> set (a # pairs)\<rbrakk> \<Longrightarrow> List.find (\<lambda>(x, uu_). P x) (a # pairs) = Some (x, y)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
proof(cases "fst pair = x")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. fst pair = x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
 2. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
fst pair = x

goal (2 subgoals):
 1. fst pair = x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
 2. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
fst pair = x
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
fst pair = x

goal (1 subgoal):
 1. List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
using eq_key_imp_eq_value[OF Cons.prems(1,3)] assms(4)
[PROOF STATE]
proof (prove)
using this:
fst pair = x
(x, ?v2.0) \<in> set (pair # pairs) \<Longrightarrow> y = ?v2.0
P x

goal (1 subgoal):
 1. List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
by force
[PROOF STATE]
proof (state)
this:
List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
fst pair \<noteq> x

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
hence "(x,y) \<in> set pairs"
[PROOF STATE]
proof (prove)
using this:
fst pair \<noteq> x

goal (1 subgoal):
 1. (x, y) \<in> set pairs
[PROOF STEP]
using Cons.prems(3)
[PROOF STATE]
proof (prove)
using this:
fst pair \<noteq> x
(x, y) \<in> set (pair # pairs)

goal (1 subgoal):
 1. (x, y) \<in> set pairs
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
(x, y) \<in> set pairs

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
(x, y) \<in> set pairs

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
have "\<And>x y. x \<in> set (map fst pairs) \<Longrightarrow> y \<in> set (map fst pairs) \<Longrightarrow> P x \<Longrightarrow> P y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using Cons.prems(2)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set (map fst (pair # pairs)); ?y \<in> set (map fst (pair # pairs)); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set (map fst pairs); y \<in> set (map fst pairs); P x; P y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis list.set_intros(2) list.simps(9))
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x \<in> set (map fst pairs); ?y \<in> set (map fst pairs); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
(x, y) \<in> set pairs
\<lbrakk>?x \<in> set (map fst pairs); ?y \<in> set (map fst pairs); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
[PROOF STEP]
have I: "List.find (\<lambda>(x,_) . P x) pairs = Some (x,y)"
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> set pairs
\<lbrakk>?x \<in> set (map fst pairs); ?y \<in> set (map fst pairs); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y

goal (1 subgoal):
 1. List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
[PROOF STEP]
using Cons.prems(1,3)
[PROOF STATE]
proof (prove)
using this:
(x, y) \<in> set pairs
\<lbrakk>?x \<in> set (map fst pairs); ?y \<in> set (map fst pairs); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
distinct (map fst (pair # pairs))
(x, y) \<in> set (pair # pairs)

goal (1 subgoal):
 1. List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
[PROOF STEP]
by (auto intro!: Cons.IH)
[PROOF STATE]
proof (state)
this:
List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
have "\<And>y. y \<in> set (map fst (pair # pairs)) \<Longrightarrow> P y \<Longrightarrow> x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> set (map fst (pair # pairs)); P y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
using Cons.prems(2,3) assms(4)
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x \<in> set (map fst (pair # pairs)); ?y \<in> set (map fst (pair # pairs)); P ?x; P ?y\<rbrakk> \<Longrightarrow> ?x = ?y
(x, y) \<in> set (pair # pairs)
P x

goal (1 subgoal):
 1. \<And>y. \<lbrakk>y \<in> set (map fst (pair # pairs)); P y\<rbrakk> \<Longrightarrow> x = y
[PROOF STEP]
by (metis set_zip_leftD zip_map_fst_snd)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?y \<in> set (map fst (pair # pairs)); P ?y\<rbrakk> \<Longrightarrow> x = ?y

goal (1 subgoal):
 1. fst pair \<noteq> x \<Longrightarrow> List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
\<lbrakk>?y \<in> set (map fst (pair # pairs)); P ?y\<rbrakk> \<Longrightarrow> x = ?y
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
\<lbrakk>?y \<in> set (map fst (pair # pairs)); P ?y\<rbrakk> \<Longrightarrow> x = ?y

goal (1 subgoal):
 1. List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
using False
[PROOF STATE]
proof (prove)
using this:
List.find (\<lambda>(x, uu_). P x) pairs = Some (x, y)
\<lbrakk>?y \<in> set (map fst (pair # pairs)); P ?y\<rbrakk> \<Longrightarrow> x = ?y
fst pair \<noteq> x

goal (1 subgoal):
 1. List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
List.find (\<lambda>a. case a of (x, uu_) \<Rightarrow> P x) (pair # pairs) = Some (x, y)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma "remdups_on (=) xs = remdups xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. remdups_on (=) xs = remdups xs
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma remdups_on_antimono:
  "(\<And>x y . f x y \<Longrightarrow> g x y) \<Longrightarrow> set (remdups_on g xs) \<subseteq> set (remdups_on f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. f x y \<Longrightarrow> g x y) \<Longrightarrow> set (remdups_on g xs) \<subseteq> set (remdups_on f xs)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma remdups_on_subset_input: "set (remdups_on f xs) \<subseteq> set xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (remdups_on f xs) \<subseteq> set xs
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma distinct_on_remdups_on: "distinct_on f (remdups_on f xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_on f (remdups_on f xs)
[PROOF STEP]
proof (induction xs)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. distinct_on f (remdups_on f [])
 2. \<And>a xs. distinct_on f (remdups_on f xs) \<Longrightarrow> distinct_on f (remdups_on f (a # xs))
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:

goal (2 subgoals):
 1. distinct_on f (remdups_on f [])
 2. \<And>a xs. distinct_on f (remdups_on f xs) \<Longrightarrow> distinct_on f (remdups_on f (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct_on f (remdups_on f [])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
distinct_on f (remdups_on f [])

goal (1 subgoal):
 1. \<And>a xs. distinct_on f (remdups_on f xs) \<Longrightarrow> distinct_on f (remdups_on f (a # xs))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a xs. distinct_on f (remdups_on f xs) \<Longrightarrow> distinct_on f (remdups_on f (a # xs))
[PROOF STEP]
case (Cons x xs)
[PROOF STATE]
proof (state)
this:
distinct_on f (remdups_on f xs)

goal (1 subgoal):
 1. \<And>a xs. distinct_on f (remdups_on f xs) \<Longrightarrow> distinct_on f (remdups_on f (a # xs))
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
distinct_on f (remdups_on f xs)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
distinct_on f (remdups_on f xs)

goal (1 subgoal):
 1. distinct_on f (remdups_on f (x # xs))
[PROOF STEP]
using remdups_on_subset_input
[PROOF STATE]
proof (prove)
using this:
distinct_on f (remdups_on f xs)
set (remdups_on ?f ?xs) \<subseteq> set ?xs

goal (1 subgoal):
 1. distinct_on f (remdups_on f (x # xs))
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
distinct_on f (remdups_on f (x # xs))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma distinct_on_no_compare: "(\<And>x y . f x y \<Longrightarrow> f y x)\<Longrightarrow>
  distinct_on f xs \<Longrightarrow> x\<in>set xs \<Longrightarrow> y\<in>set xs \<Longrightarrow> x\<noteq>y \<Longrightarrow> \<not> f x y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. f x y \<Longrightarrow> f y x; distinct_on f xs; x \<in> set xs; y \<in> set xs; x \<noteq> y\<rbrakk> \<Longrightarrow> \<not> f x y
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma lookup_present_eq_key: "distinct (map fst al) \<Longrightarrow> (k, v) \<in> set al \<longleftrightarrow> lookup (\<lambda>x. x=k) al = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map fst al) \<Longrightarrow> ((k, v) \<in> set al) = (lookup (\<lambda>x. x = k) al = Some v)
[PROOF STEP]
by (induction al) (auto simp add: rev_image_eqI split: if_splits)


[STATEMENT]
lemma lookup_None_iff: "lookup P xs = None \<longleftrightarrow> \<not> (\<exists>x. x \<in> set (map fst xs) \<and> P x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lookup P xs = None) = (\<nexists>x. x \<in> set (map fst xs) \<and> P x)
[PROOF STEP]
by (induction xs) (auto split: if_splits)


[STATEMENT]
lemma find_Some: "List.find P l = Some p \<Longrightarrow> p\<in>set l \<and> P p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.find P l = Some p \<Longrightarrow> p \<in> set l \<and> P p
[PROOF STEP]
by (induction l) (auto split: if_splits)


[STATEMENT]
lemma find_Some_imp_lookup_Some:
  "List.find (\<lambda>(k,_). P k) xs = Some (k,v) \<Longrightarrow> lookup P xs = Some v"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. List.find (\<lambda>(k, uu_). P k) xs = Some (k, v) \<Longrightarrow> lookup P xs = Some v
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma lookup_Some_imp_find_Some:
  "lookup P xs = Some v \<Longrightarrow> \<exists>x. List.find (\<lambda>(k,_). P k) xs = Some (x,v)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. lookup P xs = Some v \<Longrightarrow> \<exists>x. List.find (\<lambda>(k, uu_). P k) xs = Some (x, v)
[PROOF STEP]
by (induction xs) auto


[STATEMENT]
lemma lookup_None_iff_find_None: "lookup P xs = None \<longleftrightarrow> List.find (\<lambda>(k,_). P k) xs = None"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (lookup P xs = None) = (List.find (\<lambda>(k, uu_). P k) xs = None)
[PROOF STEP]
by (induction xs) auto