[STATEMENT]
lemma op_cat_cat_0[cat_op_simps]: "op_cat (cat_0) = cat_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cat cat_0 = cat_0
[PROOF STEP]
proof(rule cat_smc_eqI)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. category ?\<alpha> (op_cat cat_0)
 2. category ?\<alpha> cat_0
 3. op_cat cat_0\<lparr>CId\<rparr> = cat_0\<lparr>CId\<rparr>
 4. cat_smc (op_cat cat_0) = cat_smc cat_0
[PROOF STEP]
define \<beta> where "\<beta> = \<omega> + \<omega>"
[PROOF STATE]
proof (state)
this:
\<beta> = \<omega> + \<omega>

goal (4 subgoals):
 1. category ?\<alpha> (op_cat cat_0)
 2. category ?\<alpha> cat_0
 3. op_cat cat_0\<lparr>CId\<rparr> = cat_0\<lparr>CId\<rparr>
 4. cat_smc (op_cat cat_0) = cat_smc cat_0
[PROOF STEP]
interpret \<beta>: \<Z> \<beta>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> \<beta>
[PROOF STEP]
unfolding \<beta>_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Z> (\<omega> + \<omega>)
[PROOF STEP]
by (rule \<Z>_\<omega>\<omega>)
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. category ?\<alpha> (op_cat cat_0)
 2. category ?\<alpha> cat_0
 3. op_cat cat_0\<lparr>CId\<rparr> = cat_0\<lparr>CId\<rparr>
 4. cat_smc (op_cat cat_0) = cat_smc cat_0
[PROOF STEP]
show "category \<beta> (op_cat cat_0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<beta> (op_cat cat_0)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
[PROOF STATE]
proof (state)
this:
category \<beta> (op_cat cat_0)

goal (3 subgoals):
 1. category (\<omega> + \<omega>) cat_0
 2. op_cat cat_0\<lparr>CId\<rparr> = cat_0\<lparr>CId\<rparr>
 3. cat_smc (op_cat cat_0) = cat_smc cat_0
[PROOF STEP]
show "category \<beta> cat_0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<beta> cat_0
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
category \<beta> cat_0

goal (2 subgoals):
 1. op_cat cat_0\<lparr>CId\<rparr> = cat_0\<lparr>CId\<rparr>
 2. cat_smc (op_cat cat_0) = cat_smc cat_0
[PROOF STEP]
qed
  (
    simp_all add:
      cat_0_components op_cat_components cat_smc_cat_0
      slicing_commute[symmetric] smc_op_simps
  )


[STATEMENT]
lemma cf_0_components:
  shows "cf_0 \<AA>\<lparr>ObjMap\<rparr> = 0"
    and "cf_0 \<AA>\<lparr>ArrMap\<rparr> = 0"
    and "cf_0 \<AA>\<lparr>HomDom\<rparr> = cat_0"
    and "cf_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cf_0 \<AA>\<lparr>ObjMap\<rparr> = []\<^sub>\<circ> &&& cf_0 \<AA>\<lparr>ArrMap\<rparr> = []\<^sub>\<circ>) &&& cf_0 \<AA>\<lparr>HomDom\<rparr> = cat_0 &&& cf_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
[PROOF STEP]
unfolding cf_0_def dghm_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]\<^sub>\<circ>, []\<^sub>\<circ>, cat_0, \<AA>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, cat_0, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = []\<^sub>\<circ>) &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, cat_0, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = cat_0 &&& [[]\<^sub>\<circ>, []\<^sub>\<circ>, cat_0, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = \<AA>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma cf_smcf_cf_0: "cf_smcf (cf_0 \<AA>) = smcf_0 (cat_smc \<AA>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_smcf (cf_0 \<AA>) = smcf_0 (cat_smc \<AA>)
[PROOF STEP]
unfolding
    dg_field_simps dghm_field_simps
    cf_smcf_def cf_0_def smc_0_def cat_0_def smcf_0_def cat_smc_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, [\<AA>\<lparr>[]\<^sub>\<circ>\<rparr>, \<AA>\<lparr>1\<^sub>\<nat>\<rparr>, \<AA>\<lparr>2\<^sub>\<nat>\<rparr>, \<AA>\<lparr>3\<^sub>\<nat>\<rparr>, \<AA>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma op_cf_cf_0: "op_cf (cf_0 \<CC>) = cf_0 (op_cat \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cf (cf_0 \<CC>) = cf_0 (op_cat \<CC>)
[PROOF STEP]
unfolding
    cf_0_def op_cat_def op_cf_def cat_0_def dghm_field_simps dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>), [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>5\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>), [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>5\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, [\<CC>\<lparr>[]\<^sub>\<circ>\<rparr>, \<CC>\<lparr>1\<^sub>\<nat>\<rparr>, \<CC>\<lparr>3\<^sub>\<nat>\<rparr>, \<CC>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<CC>\<lparr>4\<^sub>\<nat>\<rparr>), \<CC>\<lparr>5\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma cf_0_ObjMap_vsv[cat_cs_intros]: "vsv (cf_0 \<CC>\<lparr>ObjMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (cf_0 \<CC>\<lparr>ObjMap\<rparr>)
[PROOF STEP]
unfolding cf_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma cf_0_ArrMap_vsv[cat_cs_intros]: "vsv (cf_0 \<CC>\<lparr>ArrMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (cf_0 \<CC>\<lparr>ArrMap\<rparr>)
[PROOF STEP]
unfolding cf_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma cf_0_is_ft_functor:
  assumes "category \<alpha> \<AA>"
  shows "cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(rule is_ft_functorI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. cf_smcf (cf_0 \<AA>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
[PROOF STEP]
interpret \<AA>: category \<alpha> \<AA>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> \<AA>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
 2. cf_smcf (cf_0 \<AA>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
[PROOF STEP]
show "cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
proof(rule is_functorI, unfold cat_smc_cat_0 cf_smcf_cf_0)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (cf_0 \<AA>)
 3. category \<alpha> cat_0
 4. category \<alpha> \<AA>
 5. vcard (cf_0 \<AA>) = 4\<^sub>\<nat>
 6. smcf_0 (cat_smc \<AA>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
 7. cf_0 \<AA>\<lparr>HomDom\<rparr> = cat_0
 8. cf_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 9. \<And>c. c \<in>\<^sub>\<circ> cat_0\<lparr>Obj\<rparr> \<Longrightarrow> cf_0 \<AA>\<lparr>ArrMap\<rparr>\<lparr>cat_0\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<AA>\<lparr>CId\<rparr>\<lparr>cf_0 \<AA>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
show "vfsequence (cf_0 \<AA>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (cf_0 \<AA>)
[PROOF STEP]
unfolding cf_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [[]\<^sub>\<circ>, []\<^sub>\<circ>, cat_0, \<AA>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (cf_0 \<AA>)

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> cat_0
 3. category \<alpha> \<AA>
 4. vcard (cf_0 \<AA>) = 4\<^sub>\<nat>
 5. smcf_0 (cat_smc \<AA>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
 6. cf_0 \<AA>\<lparr>HomDom\<rparr> = cat_0
 7. cf_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 8. \<And>c. c \<in>\<^sub>\<circ> cat_0\<lparr>Obj\<rparr> \<Longrightarrow> cf_0 \<AA>\<lparr>ArrMap\<rparr>\<lparr>cat_0\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<AA>\<lparr>CId\<rparr>\<lparr>cf_0 \<AA>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
show "vcard (cf_0 \<AA>) = 4\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (cf_0 \<AA>) = 4\<^sub>\<nat>
[PROOF STEP]
unfolding cf_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [[]\<^sub>\<circ>, []\<^sub>\<circ>, cat_0, \<AA>]\<^sub>\<circ> = 4\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (cf_0 \<AA>) = 4\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> cat_0
 3. category \<alpha> \<AA>
 4. smcf_0 (cat_smc \<AA>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
 5. cf_0 \<AA>\<lparr>HomDom\<rparr> = cat_0
 6. cf_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 7. \<And>c. c \<in>\<^sub>\<circ> cat_0\<lparr>Obj\<rparr> \<Longrightarrow> cf_0 \<AA>\<lparr>ArrMap\<rparr>\<lparr>cat_0\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<AA>\<lparr>CId\<rparr>\<lparr>cf_0 \<AA>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
from \<Z>.smcf_0_is_ft_semifunctor assms
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>\<Z> ?\<alpha>; semicategory ?\<alpha> ?\<AA>\<rbrakk> \<Longrightarrow> smcf_0 ?\<AA> : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>?\<alpha>\<^esub> ?\<AA>
category \<alpha> \<AA>
[PROOF STEP]
show
      "smcf_0 (cat_smc \<AA>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<AA>"
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<Z> ?\<alpha>; semicategory ?\<alpha> ?\<AA>\<rbrakk> \<Longrightarrow> smcf_0 ?\<AA> : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>?\<alpha>\<^esub> ?\<AA>
category \<alpha> \<AA>

goal (1 subgoal):
 1. smcf_0 (cat_smc \<AA>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
smcf_0 (cat_smc \<AA>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<AA>

goal (6 subgoals):
 1. \<Z> \<alpha>
 2. category \<alpha> cat_0
 3. category \<alpha> \<AA>
 4. cf_0 \<AA>\<lparr>HomDom\<rparr> = cat_0
 5. cf_0 \<AA>\<lparr>HomCod\<rparr> = \<AA>
 6. \<And>c. c \<in>\<^sub>\<circ> cat_0\<lparr>Obj\<rparr> \<Longrightarrow> cf_0 \<AA>\<lparr>ArrMap\<rparr>\<lparr>cat_0\<lparr>CId\<rparr>\<lparr>c\<rparr>\<rparr> = \<AA>\<lparr>CId\<rparr>\<lparr>cf_0 \<AA>\<lparr>ObjMap\<rparr>\<lparr>c\<rparr>\<rparr>
[PROOF STEP]
qed (auto simp: assms \<AA>.category_cat_0 cat_0_components cf_0_components)
[PROOF STATE]
proof (state)
this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_smcf (cf_0 \<AA>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
[PROOF STEP]
show "cf_smcf (cf_0 \<AA>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> cat_smc \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_smcf (cf_0 \<AA>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> cat_smc \<AA>
[PROOF STEP]
by
      (
        auto simp:
          assms
          \<AA>.\<Z>_axioms
          \<AA>.smcf_0_is_ft_semifunctor
          category.cat_semicategory
          cf_smcf_cf_0
          cat_smc_cat_0
      )
[PROOF STATE]
proof (state)
this:
cf_smcf (cf_0 \<AA>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> cat_smc \<AA>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma cf_0_is_ft_functor'[cf_cs_intros]:
  assumes "category \<alpha> \<AA>"
    and "\<BB>' = \<AA>"
    and "\<AA>' = cat_0"
  shows "cf_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule cf_0_is_ft_functor)


[STATEMENT]
lemma cf_0_is_functor:
  assumes "category \<alpha> \<AA>"
  shows "cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
using cf_0_is_ft_functor[OF assms]
[PROOF STATE]
proof (prove)
using this:
cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^sub>.\<^sub>f\<^sub>a\<^sub>i\<^sub>t\<^sub>h\<^sub>f\<^sub>u\<^sub>l\<^bsub>\<alpha>\<^esub> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by auto


[STATEMENT]
lemma cf_0_is_functor'[cat_cs_intros]:
  assumes "category \<alpha> \<AA>"
    and "\<BB>' = \<AA>"
    and "\<AA>' = cat_0"
  shows "cf_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms(2,3)
[PROOF STATE]
proof (prove)
using this:
category \<alpha> \<AA>

goal (1 subgoal):
 1. cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<AA>
[PROOF STEP]
by (rule cf_0_is_functor)


[STATEMENT]
lemma is_functor_is_cf_0_if_cat_0:
  assumes "\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<FF> = cf_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> = cf_0 \<CC>
[PROOF STEP]
proof(rule cf_smcf_eqI)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. cf_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. ?\<AA> = ?\<CC>
 4. ?\<BB> = ?\

 5. cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)
[PROOF STEP]
interpret \<FF>: is_functor \<alpha> cat_0 \<CC> \<FF>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<FF> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. cf_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. ?\<AA> = ?\<CC>
 4. ?\<BB> = ?\

 5. cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)
[PROOF STEP]
show "\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (4 subgoals):
 1. cf_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. cat_0 = ?\<CC>
 3. \<CC> = ?\

 4. cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = 0" "\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
using this:
\<FF> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ> &&& \<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cat_0_components)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (\<FF>\<lparr>ObjMap\<rparr>) = []\<^sub>\<circ>
\<D>\<^sub>\<circ> (\<FF>\<lparr>ArrMap\<rparr>) = []\<^sub>\<circ>

goal (4 subgoals):
 1. cf_0 \<CC> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. cat_0 = ?\<CC>
 3. \<CC> = ?\

 4. cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)
[PROOF STEP]
show "cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (3 subgoals):
 1. cat_0 = cat_0
 2. \<CC> = \<CC>
 3. cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)
[PROOF STEP]
show "cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)
[PROOF STEP]
unfolding cf_smcf_cf_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_smcf \<FF> = smcf_0 (cat_smc \<CC>)
[PROOF STEP]
by
      (
        rule is_semifunctor_is_smcf_0_if_smc_0,
        rule \<FF>.cf_is_semifunctor[unfolded slicing_simps cat_smc_cat_0]
      )
[PROOF STATE]
proof (state)
this:
cf_smcf \<FF> = cf_smcf (cf_0 \<CC>)

goal (2 subgoals):
 1. cat_0 = cat_0
 2. \<CC> = \<CC>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma (in is_functor) cf_comp_cf_cf_0[cat_cs_simps]: "\<FF> \<circ>\<^sub>C\<^sub>F cf_0 \<AA> = cf_0 \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA> = cf_0 \<BB>
[PROOF STEP]
proof(rule cf_eqI)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. cf_0 \<BB> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\

 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>
 4. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
 5. ?\<AA> = ?\<CC>
 6. ?\<BB> = ?\

[PROOF STEP]
show "\<FF> \<circ>\<^sub>C\<^sub>F cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (5 subgoals):
 1. cf_0 \<BB> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
 4. cat_0 = ?\<CC>
 5. \<BB> = ?\

[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have ObjMap_dom_lhs: "\<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>C\<^sub>F cf_0 \<AA>)\<lparr>ObjMap\<rparr>) = cat_0\<lparr>Obj\<rparr>"
    and ArrMap_dom_lhs: "\<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>C\<^sub>F cf_0 \<AA>)\<lparr>ArrMap\<rparr>) = cat_0\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr>) = cat_0\<lparr>Obj\<rparr> &&& \<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr>) = cat_0\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr>) = cat_0\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr>) = cat_0\<lparr>Arr\<rparr>

goal (5 subgoals):
 1. cf_0 \<BB> : ?\<CC> \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\

 2. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
 4. cat_0 = ?\<CC>
 5. \<BB> = ?\

[PROOF STEP]
show "cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (4 subgoals):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>
 2. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
 3. cat_0 = cat_0
 4. \<BB> = \<BB>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have ObjMap_dom_rhs: "\<D>\<^sub>\<circ> (cf_0 \<BB>\<lparr>ObjMap\<rparr>) = cat_0\<lparr>Obj\<rparr>"
    and ArrMap_dom_rhs: "\<D>\<^sub>\<circ> (cf_0 \<BB>\<lparr>ArrMap\<rparr>) = cat_0\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
using this:
cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (cf_0 \<BB>\<lparr>ObjMap\<rparr>) = cat_0\<lparr>Obj\<rparr> &&& \<D>\<^sub>\<circ> (cf_0 \<BB>\<lparr>ArrMap\<rparr>) = cat_0\<lparr>Arr\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps)+
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (cf_0 \<BB>\<lparr>ObjMap\<rparr>) = cat_0\<lparr>Obj\<rparr>
\<D>\<^sub>\<circ> (cf_0 \<BB>\<lparr>ArrMap\<rparr>) = cat_0\<lparr>Arr\<rparr>

goal (4 subgoals):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>
 2. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
 3. cat_0 = cat_0
 4. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>C\<^sub>F cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>
[PROOF STEP]
by
      (
        rule vsv_eqI,
        unfold ObjMap_dom_lhs ObjMap_dom_rhs ArrMap_dom_lhs ArrMap_dom_rhs
      )
      (auto simp: cat_0_components intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ObjMap\<rparr> = cf_0 \<BB>\<lparr>ObjMap\<rparr>

goal (3 subgoals):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
 2. cat_0 = cat_0
 3. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>C\<^sub>F cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>
[PROOF STEP]
by
      (
        rule vsv_eqI,
        unfold ObjMap_dom_lhs ObjMap_dom_rhs ArrMap_dom_lhs ArrMap_dom_rhs
      )
      (auto simp: cat_0_components intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M cf_0 \<AA>)\<lparr>ArrMap\<rparr> = cf_0 \<BB>\<lparr>ArrMap\<rparr>

goal (2 subgoals):
 1. cat_0 = cat_0
 2. \<BB> = \<BB>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma ntcf_0_components:
  shows "ntcf_0 \<CC>\<lparr>NTMap\<rparr> = 0"
    and [cat_cs_simps]: "ntcf_0 \<CC>\<lparr>NTDom\<rparr> = cf_0 \<CC>"
    and [cat_cs_simps]: "ntcf_0 \<CC>\<lparr>NTCod\<rparr> = cf_0 \<CC>"
    and [cat_cs_simps]: "ntcf_0 \<CC>\<lparr>NTDGDom\<rparr> = cat_0"
    and [cat_cs_simps]: "ntcf_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (ntcf_0 \<CC>\<lparr>NTMap\<rparr> = []\<^sub>\<circ> &&& ntcf_0 \<CC>\<lparr>NTDom\<rparr> = cf_0 \<CC>) &&& ntcf_0 \<CC>\<lparr>NTCod\<rparr> = cf_0 \<CC> &&& ntcf_0 \<CC>\<lparr>NTDGDom\<rparr> = cat_0 &&& ntcf_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
unfolding ntcf_0_def nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = []\<^sub>\<circ> &&& [[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = cf_0 \<CC>) &&& [[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = cf_0 \<CC> &&& [[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = cat_0 &&& [[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = \<CC>
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma ntcf_ntsmcf_ntcf_0: "ntcf_ntsmcf (ntcf_0 \<AA>) = ntsmcf_0 (cat_smc \<AA>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf (ntcf_0 \<AA>) = ntsmcf_0 (cat_smc \<AA>)
[PROOF STEP]
unfolding
    ntcf_ntsmcf_def ntcf_0_def ntsmcf_0_def cat_smc_def
    cf_smcf_def smcf_0_def cf_0_def cat_0_def smc_0_def
    dg_field_simps dghm_field_simps nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, \<AA>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ> = [[]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, [\<AA>\<lparr>[]\<^sub>\<circ>\<rparr>, \<AA>\<lparr>1\<^sub>\<nat>\<rparr>, \<AA>\<lparr>2\<^sub>\<nat>\<rparr>, \<AA>\<lparr>3\<^sub>\<nat>\<rparr>, \<AA>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, [\<AA>\<lparr>[]\<^sub>\<circ>\<rparr>, \<AA>\<lparr>1\<^sub>\<nat>\<rparr>, \<AA>\<lparr>2\<^sub>\<nat>\<rparr>, \<AA>\<lparr>3\<^sub>\<nat>\<rparr>, \<AA>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [[]\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>, []\<^sub>\<circ>]\<^sub>\<circ>, [\<AA>\<lparr>[]\<^sub>\<circ>\<rparr>, \<AA>\<lparr>1\<^sub>\<nat>\<rparr>, \<AA>\<lparr>2\<^sub>\<nat>\<rparr>, \<AA>\<lparr>3\<^sub>\<nat>\<rparr>, \<AA>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma op_ntcf_ntcf_0: "op_ntcf (ntcf_0 \<CC>) = ntcf_0 (op_cat \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntcf (ntcf_0 \<CC>) = ntcf_0 (op_cat \<CC>)
[PROOF STEP]
by
    (
      simp_all add:
        op_ntcf_def ntcf_0_def op_cat_def op_cf_cf_0 cat_0_def
        nt_field_simps dg_field_simps nat_omega_simps
    )


[STATEMENT]
lemma ntcf_0_NTMap_vsv[cat_cs_intros]: "vsv (ntcf_0 \<CC>\<lparr>NTMap\<rparr>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv (ntcf_0 \<CC>\<lparr>NTMap\<rparr>)
[PROOF STEP]
unfolding ntcf_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vsv []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma ntcf_0_NTMap_vdomain[cat_cs_simps]: "\<D>\<^sub>\<circ> (ntcf_0 \<CC>\<lparr>NTMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (ntcf_0 \<CC>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
unfolding ntcf_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<D>\<^sub>\<circ> []\<^sub>\<circ> = []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma ntcf_0_NTMap_vrange[cat_cs_simps]: "\<R>\<^sub>\<circ> (ntcf_0 \<CC>\<lparr>NTMap\<rparr>) = 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (ntcf_0 \<CC>\<lparr>NTMap\<rparr>) = []\<^sub>\<circ>
[PROOF STEP]
unfolding ntcf_0_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> []\<^sub>\<circ> = []\<^sub>\<circ>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in category) cat_ntcf_0_is_ntcfI:
  "ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(intro is_ntcfI)
[PROOF STATE]
proof (state)
goal (10 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (ntcf_0 \<CC>)
 3. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 5. vcard (ntcf_0 \<CC>) = 5\<^sub>\<nat>
 6. ntcf_ntsmcf (ntcf_0 \<CC>) : cf_smcf (cf_0 \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf (cf_0 \<CC>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>
 7. ntcf_0 \<CC>\<lparr>NTDom\<rparr> = cf_0 \<CC>
 8. ntcf_0 \<CC>\<lparr>NTCod\<rparr> = cf_0 \<CC>
 9. ntcf_0 \<CC>\<lparr>NTDGDom\<rparr> = cat_0
 10. ntcf_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
show "vfsequence (ntcf_0 \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (ntcf_0 \<CC>)
[PROOF STEP]
unfolding ntcf_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
vfsequence (ntcf_0 \<CC>)

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. vcard (ntcf_0 \<CC>) = 5\<^sub>\<nat>
 5. ntcf_ntsmcf (ntcf_0 \<CC>) : cf_smcf (cf_0 \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf (cf_0 \<CC>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>
 6. ntcf_0 \<CC>\<lparr>NTDom\<rparr> = cf_0 \<CC>
 7. ntcf_0 \<CC>\<lparr>NTCod\<rparr> = cf_0 \<CC>
 8. ntcf_0 \<CC>\<lparr>NTDGDom\<rparr> = cat_0
 9. ntcf_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
show "vcard (ntcf_0 \<CC>) = 5\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (ntcf_0 \<CC>) = 5\<^sub>\<nat>
[PROOF STEP]
unfolding ntcf_0_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [[]\<^sub>\<circ>, cf_0 \<CC>, cf_0 \<CC>, cat_0, \<CC>]\<^sub>\<circ> = 5\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (ntcf_0 \<CC>) = 5\<^sub>\<nat>

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. ntcf_ntsmcf (ntcf_0 \<CC>) : cf_smcf (cf_0 \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf (cf_0 \<CC>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>
 5. ntcf_0 \<CC>\<lparr>NTDom\<rparr> = cf_0 \<CC>
 6. ntcf_0 \<CC>\<lparr>NTCod\<rparr> = cf_0 \<CC>
 7. ntcf_0 \<CC>\<lparr>NTDGDom\<rparr> = cat_0
 8. ntcf_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
show "ntcf_ntsmcf (ntcf_0 \<CC>) :
    cf_smcf (cf_0 \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf (cf_0 \<CC>) :
    cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf (ntcf_0 \<CC>) : cf_smcf (cf_0 \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf (cf_0 \<CC>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>
[PROOF STEP]
unfolding ntcf_ntsmcf_ntcf_0 cf_smcf_cf_0 cat_smc_cat_0
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntsmcf_0 (cat_smc \<CC>) : smcf_0 (cat_smc \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F smcf_0 (cat_smc \<CC>) : smc_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: smc_cs_intros slicing_intros)
[PROOF STATE]
proof (state)
this:
ntcf_ntsmcf (ntcf_0 \<CC>) : cf_smcf (cf_0 \<CC>) \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F cf_smcf (cf_0 \<CC>) : cat_smc cat_0 \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> cat_smc \<CC>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 3. cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
 4. ntcf_0 \<CC>\<lparr>NTDom\<rparr> = cf_0 \<CC>
 5. ntcf_0 \<CC>\<lparr>NTCod\<rparr> = cf_0 \<CC>
 6. ntcf_0 \<CC>\<lparr>NTDGDom\<rparr> = cat_0
 7. ntcf_0 \<CC>\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
qed (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)+


[STATEMENT]
lemma (in category) cat_ntcf_0_is_ntcfI'[cat_cs_intros]:
  assumes "\<FF>' = cf_0 \<CC>"
    and "\<GG>' = cf_0 \<CC>"
    and "\<AA>' = cat_0"
    and "\<BB>' = \<CC>"
    and "\<FF>' = \<FF>"
    and "\<GG>' = \<GG>"
  shows "ntcf_0 \<CC> : \<FF>' \<mapsto>\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> : \<FF>' \<mapsto>\<^sub>C\<^sub>F \<GG>' : \<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>'
[PROOF STEP]
unfolding assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule cat_ntcf_0_is_ntcfI)


[STATEMENT]
lemma is_ntcf_is_ntcf_0_if_cat_0:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<NN> = ntcf_0 \<CC>" and "\<FF> = cf_0 \<CC>" and "\<GG> = cf_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = ntcf_0 \<CC> &&& \<FF> = cf_0 \<CC> &&& \<GG> = cf_0 \<CC>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<NN> = ntcf_0 \<CC>
 2. \<FF> = cf_0 \<CC>
 3. \<GG> = cf_0 \<CC>
[PROOF STEP]
interpret \<NN>: is_ntcf \<alpha> cat_0 \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<NN> = ntcf_0 \<CC>
 2. \<FF> = cf_0 \<CC>
 3. \<GG> = cf_0 \<CC>
[PROOF STEP]
note is_ntsmcf_is_ntsmcf_0_if_smc_0 = is_ntsmcf_is_ntsmcf_0_if_smc_0
    [
      OF \<NN>.ntcf_is_ntsmcf[unfolded cat_smc_cat_0],
      folded smcf_dghm_smcf_0 ntsmcf_tdghm_ntsmcf_0
    ]
[PROOF STATE]
proof (state)
this:
ntcf_ntsmcf \<NN> = ntsmcf_0 (cat_smc \<CC>)
cf_smcf \<FF> = smcf_0 (cat_smc \<CC>)
cf_smcf \<GG> = smcf_0 (cat_smc \<CC>)

goal (3 subgoals):
 1. \<NN> = ntcf_0 \<CC>
 2. \<FF> = cf_0 \<CC>
 3. \<GG> = cf_0 \<CC>
[PROOF STEP]
show \<FF>_def: "\<FF> = cf_0 \<CC>" and \<GG>_def: "\<GG> = cf_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> = cf_0 \<CC> &&& \<GG> = cf_0 \<CC>
[PROOF STEP]
by (all\<open>intro is_functor_is_cf_0_if_cat_0\<close>)
      (cs_concl cs_shallow cs_intro: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
\<FF> = cf_0 \<CC>
\<GG> = cf_0 \<CC>

goal (1 subgoal):
 1. \<NN> = ntcf_0 \<CC>
[PROOF STEP]
show "\<NN> = ntcf_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> = ntcf_0 \<CC>
[PROOF STEP]
proof(rule ntcf_ntsmcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
 7. ntcf_ntsmcf \<NN> = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
this:
\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (6 subgoals):
 1. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. \<FF> = ?\<FF>'
 3. \<GG> = ?\<GG>'
 4. cat_0 = ?\<AA>'
 5. \<CC> = ?\<BB>'
 6. ntcf_ntsmcf \<NN> = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "ntcf_0 \<CC> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: \<FF>_def \<GG>_def cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_0 \<CC> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. \<FF> = \<FF>
 2. \<GG> = \<GG>
 3. cat_0 = cat_0
 4. \<CC> = \<CC>
 5. ntcf_ntsmcf \<NN> = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
qed
    (
      simp_all add:
        \<FF>_def \<GG>_def is_ntsmcf_is_ntsmcf_0_if_smc_0 ntcf_ntsmcf_ntcf_0
    )
[PROOF STATE]
proof (state)
this:
\<NN> = ntcf_0 \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntcf_vcomp_ntcf_ntcf_0[cat_cs_simps]:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_0 \<CC> = ntcf_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> = ntcf_0 \<CC>
[PROOF STEP]
proof(rule ntcf_ntsmcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
 7. ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
interpret \<NN>: is_ntcf \<alpha> cat_0 \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
 7. ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
unfolding is_ntcf_is_ntcf_0_if_cat_0[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (6 subgoals):
 1. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. cf_0 \<CC> = ?\<FF>'
 3. cf_0 \<CC> = ?\<GG>'
 4. cat_0 = ?\<AA>'
 5. \<CC> = ?\<BB>'
 6. ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. cf_0 \<CC> = cf_0 \<CC>
 2. cf_0 \<CC> = cf_0 \<CC>
 3. cat_0 = cat_0
 4. \<CC> = \<CC>
 5. ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
unfolding
      slicing_commute[symmetric]
      ntsmcf_vcomp_ntsmcf_ntsmcf_0
        [
          OF \<NN>.ntcf_is_ntsmcf[unfolded cat_smc_cat_0],
          folded ntcf_ntsmcf_ntcf_0
        ]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf (ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ntcf_ntsmcf (\<NN> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)

goal (4 subgoals):
 1. cf_0 \<CC> = cf_0 \<CC>
 2. cf_0 \<CC> = cf_0 \<CC>
 3. cat_0 = cat_0
 4. \<CC> = \<CC>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma ntcf_vcomp_ntcf_0_ntcf[cat_cs_simps]:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows "ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<NN> = ntcf_0 \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> = ntcf_0 \<CC>
[PROOF STEP]
proof(rule ntcf_ntsmcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
 7. ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
interpret \<NN>: is_ntcf \<alpha> cat_0 \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>C\<^sub>F \<GG> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
 7. ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<NN> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
unfolding is_ntcf_is_ntcf_0_if_cat_0[OF assms]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (6 subgoals):
 1. ntcf_0 \<CC> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. cf_0 \<CC> = ?\<FF>'
 3. cf_0 \<CC> = ?\<GG>'
 4. cat_0 = ?\<AA>'
 5. \<CC> = ?\<BB>'
 6. ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
ntcf_0 \<CC> : cf_0 \<CC> \<mapsto>\<^sub>C\<^sub>F cf_0 \<CC> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal (5 subgoals):
 1. cf_0 \<CC> = cf_0 \<CC>
 2. cf_0 \<CC> = cf_0 \<CC>
 3. cat_0 = cat_0
 4. \<CC> = \<CC>
 5. ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
show "ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
unfolding
      slicing_commute[symmetric]
      ntsmcf_vcomp_ntsmcf_0_ntsmcf
        [
          OF \<NN>.ntcf_is_ntsmcf[unfolded cat_smc_cat_0],
          folded ntcf_ntsmcf_ntcf_0
        ]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ntcf_ntsmcf (ntcf_0 \<CC>) = ntcf_ntsmcf (ntcf_0 \<CC>)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
ntcf_ntsmcf (ntcf_0 \<CC> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = ntcf_ntsmcf (ntcf_0 \<CC>)

goal (4 subgoals):
 1. cf_0 \<CC> = cf_0 \<CC>
 2. cf_0 \<CC> = cf_0 \<CC>
 3. cat_0 = cat_0
 4. \<CC> = \<CC>
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma (in is_functor) cf_ntcf_comp_cf_ntcf_0[cat_cs_simps]:
  "\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_0 \<AA> = ntcf_0 \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA> = ntcf_0 \<BB>
[PROOF STEP]
proof(rule ntcf_eqI)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA> : ?\<FF> \<mapsto>\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>
 2. ntcf_0 \<BB> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>?\<alpha>\<^esub> ?\<BB>'
 3. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show "\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_0 \<AA> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (cs_concl cs_shallow cs_simp: cat_cs_simps cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (6 subgoals):
 1. ntcf_0 \<BB> : ?\<FF>' \<mapsto>\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 2. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>
 3. cf_0 \<BB> = ?\<FF>'
 4. cf_0 \<BB> = ?\<GG>'
 5. cat_0 = ?\<AA>'
 6. \<BB> = ?\<BB>'
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have dom_lhs: "\<D>\<^sub>\<circ> ((\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_0 \<AA>)\<lparr>NTMap\<rparr>) = cat_0\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

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

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

goal (5 subgoals):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>
 2. cf_0 \<BB> = cf_0 \<BB>
 3. cf_0 \<BB> = cf_0 \<BB>
 4. cat_0 = cat_0
 5. \<BB> = \<BB>
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ntcf_0 \<BB> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
have dom_rhs: "\<D>\<^sub>\<circ> (ntcf_0 \<BB>\<lparr>NTMap\<rparr>) = cat_0\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
using this:
ntcf_0 \<BB> : cf_0 \<BB> \<mapsto>\<^sub>C\<^sub>F cf_0 \<BB> : cat_0 \<mapsto>\<mapsto>\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<D>\<^sub>\<circ> (ntcf_0 \<BB>\<lparr>NTMap\<rparr>) = cat_0\<lparr>Obj\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: cat_cs_simps)
[PROOF STATE]
proof (state)
this:
\<D>\<^sub>\<circ> (ntcf_0 \<BB>\<lparr>NTMap\<rparr>) = cat_0\<lparr>Obj\<rparr>

goal (5 subgoals):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>
 2. cf_0 \<BB> = cf_0 \<BB>
 3. cf_0 \<BB> = cf_0 \<BB>
 4. cat_0 = cat_0
 5. \<BB> = \<BB>
[PROOF STEP]
show "(\<FF> \<circ>\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>C\<^sub>F ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>
[PROOF STEP]
by (rule vsv_eqI, unfold dom_lhs dom_rhs)
      (auto simp: cat_0_components intro!: cat_cs_intros)+
[PROOF STATE]
proof (state)
this:
(\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntcf_0 \<AA>)\<lparr>NTMap\<rparr> = ntcf_0 \<BB>\<lparr>NTMap\<rparr>

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


[STATEMENT]
lemma cat_1_components:
  shows "cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = set {\<aa>}"
    and "cat_1 \<aa> \<ff>\<lparr>Arr\<rparr> = set {\<ff>}"
    and "cat_1 \<aa> \<ff>\<lparr>Dom\<rparr> = set {\<langle>\<ff>, \<aa>\<rangle>}"
    and "cat_1 \<aa> \<ff>\<lparr>Cod\<rparr> = set {\<langle>\<ff>, \<aa>\<rangle>}"
    and "cat_1 \<aa> \<ff>\<lparr>Comp\<rparr> = set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}"
    and "cat_1 \<aa> \<ff>\<lparr>CId\<rparr> = set {\<langle>\<aa>, \<ff>\<rangle>}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = ZFC_in_HOL.set {\<aa>} &&& cat_1 \<aa> \<ff>\<lparr>Arr\<rparr> = ZFC_in_HOL.set {\<ff>} &&& cat_1 \<aa> \<ff>\<lparr>Dom\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}) &&& cat_1 \<aa> \<ff>\<lparr>Cod\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>} &&& cat_1 \<aa> \<ff>\<lparr>Comp\<rparr> = ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>} &&& cat_1 \<aa> \<ff>\<lparr>CId\<rparr> = ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}
[PROOF STEP]
unfolding cat_1_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ([ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> = ZFC_in_HOL.set {\<aa>} &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<ff>} &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}) &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>} &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>} &&& [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>5\<^sub>\<nat>\<rparr> = ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}
[PROOF STEP]
by (simp_all add: nat_omega_simps)


[STATEMENT]
lemma smc_cat_1: "cat_smc (cat_1 \<aa> \<ff>) = smc_1 \<aa> \<ff>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_smc (cat_1 \<aa> \<ff>) = smc_1 \<aa> \<ff>
[PROOF STEP]
unfolding cat_smc_def cat_1_def smc_1_def dg_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>, [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>, [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma cat_1_ObjI[cat_cs_intros]:
  assumes "a = \<aa>"
  shows "a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff> \<lparr>Obj\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
[PROOF STEP]
unfolding cat_1_components(1) assms
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<aa> \<in>\<^sub>\<circ> ZFC_in_HOL.set {\<aa>}
[PROOF STEP]
by simp


[STATEMENT]
lemma cat_1_CId_app: "cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr> = \<ff>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>\<aa>\<rparr> = \<ff>
[PROOF STEP]
unfolding cat_1_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}\<lparr>\<aa>\<rparr> = \<ff>
[PROOF STEP]
by simp


[STATEMENT]
lemma (in \<Z>) category_cat_1:
  assumes "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>" and "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "category \<alpha> (cat_1 \<aa> \<ff>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. category \<alpha> (cat_1 \<aa> \<ff>)
[PROOF STEP]
proof(intro categoryI, unfold smc_cat_1)
[PROOF STATE]
proof (state)
goal (9 subgoals):
 1. \<Z> \<alpha>
 2. vfsequence (cat_1 \<aa> \<ff>)
 3. vsv (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>)
 4. vcard (cat_1 \<aa> \<ff>) = 6\<^sub>\<nat>
 5. semicategory \<alpha> (smc_1 \<aa> \<ff>)
 6. \<D>\<^sub>\<circ> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 7. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> a
 8. \<And>a b f. f : a \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> b \<Longrightarrow> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_1 \<aa> \<ff>\<^esub> f = f
 9. \<And>b c f. f : b \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_1 \<aa> \<ff>\<^esub> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vfsequence (cat_1 \<aa> \<ff>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence (cat_1 \<aa> \<ff>)
[PROOF STEP]
unfolding cat_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vfsequence [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vfsequence (cat_1 \<aa> \<ff>)

goal (8 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>)
 3. vcard (cat_1 \<aa> \<ff>) = 6\<^sub>\<nat>
 4. semicategory \<alpha> (smc_1 \<aa> \<ff>)
 5. \<D>\<^sub>\<circ> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 6. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> a
 7. \<And>a b f. f : a \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> b \<Longrightarrow> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_1 \<aa> \<ff>\<^esub> f = f
 8. \<And>b c f. f : b \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_1 \<aa> \<ff>\<^esub> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
show "vcard (cat_1 \<aa> \<ff>) = 6\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard (cat_1 \<aa> \<ff>) = 6\<^sub>\<nat>
[PROOF STEP]
unfolding cat_1_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. vcard [ZFC_in_HOL.set {\<aa>}, ZFC_in_HOL.set {\<ff>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>\<ff>, \<aa>\<rangle>}, ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}, ZFC_in_HOL.set {\<langle>\<aa>, \<ff>\<rangle>}]\<^sub>\<circ> = 6\<^sub>\<nat>
[PROOF STEP]
by (simp add: nat_omega_simps)
[PROOF STATE]
proof (state)
this:
vcard (cat_1 \<aa> \<ff>) = 6\<^sub>\<nat>

goal (7 subgoals):
 1. \<Z> \<alpha>
 2. vsv (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>)
 3. semicategory \<alpha> (smc_1 \<aa> \<ff>)
 4. \<D>\<^sub>\<circ> (cat_1 \<aa> \<ff>\<lparr>CId\<rparr>) = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 5. \<And>a. a \<in>\<^sub>\<circ> cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> \<Longrightarrow> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>a\<rparr> : a \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> a
 6. \<And>a b f. f : a \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> b \<Longrightarrow> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>cat_1 \<aa> \<ff>\<^esub> f = f
 7. \<And>b c f. f : b \<mapsto>\<^bsub>cat_1 \<aa> \<ff>\<^esub> c \<Longrightarrow> f \<circ>\<^sub>A\<^bsub>cat_1 \<aa> \<ff>\<^esub> cat_1 \<aa> \<ff>\<lparr>CId\<rparr>\<lparr>b\<rparr> = f
[PROOF STEP]
qed (auto simp: assms semicategory_smc_1 cat_1_is_arr_iff cat_1_components)


[STATEMENT]
lemma (in \<Z>) finite_category_cat_1:
  assumes "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>" and "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "finite_category \<alpha> (cat_1 \<aa> \<ff>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite_category \<alpha> (cat_1 \<aa> \<ff>)
[PROOF STEP]
by (intro finite_categoryI')
    (auto simp: cat_1_components intro: category_cat_1[OF assms])


[STATEMENT]
lemma (in \<Z>) cat_1_op[cat_op_simps]:
  assumes "\<aa> \<in>\<^sub>\<circ> Vset \<alpha>" and "\<ff> \<in>\<^sub>\<circ> Vset \<alpha>"
  shows "op_cat (cat_1 \<aa> \<ff>) = cat_1 \<aa> \<ff>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cat (cat_1 \<aa> \<ff>) = cat_1 \<aa> \<ff>
[PROOF STEP]
proof(rule cat_eqI, unfold cat_op_simps)
[PROOF STATE]
proof (state)
goal (8 subgoals):
 1. category ?\<alpha> (op_cat (cat_1 \<aa> \<ff>))
 2. category ?\<alpha> (cat_1 \<aa> \<ff>)
 3. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 4. cat_1 \<aa> \<ff>\<lparr>Arr\<rparr> = cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 5. cat_1 \<aa> \<ff>\<lparr>Cod\<rparr> = cat_1 \<aa> \<ff>\<lparr>Dom\<rparr>
 6. cat_1 \<aa> \<ff>\<lparr>Dom\<rparr> = cat_1 \<aa> \<ff>\<lparr>Cod\<rparr>
 7. op_cat (cat_1 \<aa> \<ff>)\<lparr>Comp\<rparr> = cat_1 \<aa> \<ff>\<lparr>Comp\<rparr>
 8. cat_1 \<aa> \<ff>\<lparr>CId\<rparr> = cat_1 \<aa> \<ff>\<lparr>CId\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "category \<alpha> (op_cat (cat_1 \<aa> \<ff>))"
[PROOF STATE]
proof (prove)
using this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. category \<alpha> (op_cat (cat_1 \<aa> \<ff>))
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros cat_op_intros)
[PROOF STATE]
proof (state)
this:
category \<alpha> (op_cat (cat_1 \<aa> \<ff>))

goal (7 subgoals):
 1. category \<alpha> (cat_1 \<aa> \<ff>)
 2. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 3. cat_1 \<aa> \<ff>\<lparr>Arr\<rparr> = cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 4. cat_1 \<aa> \<ff>\<lparr>Cod\<rparr> = cat_1 \<aa> \<ff>\<lparr>Dom\<rparr>
 5. cat_1 \<aa> \<ff>\<lparr>Dom\<rparr> = cat_1 \<aa> \<ff>\<lparr>Cod\<rparr>
 6. op_cat (cat_1 \<aa> \<ff>)\<lparr>Comp\<rparr> = cat_1 \<aa> \<ff>\<lparr>Comp\<rparr>
 7. cat_1 \<aa> \<ff>\<lparr>CId\<rparr> = cat_1 \<aa> \<ff>\<lparr>CId\<rparr>
[PROOF STEP]
from assms
[PROOF STATE]
proof (chain)
picking this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>
[PROOF STEP]
show "category \<alpha> (cat_1 \<aa> \<ff>)"
[PROOF STATE]
proof (prove)
using this:
\<aa> \<in>\<^sub>\<circ> Vset \<alpha>
\<ff> \<in>\<^sub>\<circ> Vset \<alpha>

goal (1 subgoal):
 1. category \<alpha> (cat_1 \<aa> \<ff>)
[PROOF STEP]
by (cs_concl cs_shallow cs_intro: cat_cs_intros)
[PROOF STATE]
proof (state)
this:
category \<alpha> (cat_1 \<aa> \<ff>)

goal (6 subgoals):
 1. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 2. cat_1 \<aa> \<ff>\<lparr>Arr\<rparr> = cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 3. cat_1 \<aa> \<ff>\<lparr>Cod\<rparr> = cat_1 \<aa> \<ff>\<lparr>Dom\<rparr>
 4. cat_1 \<aa> \<ff>\<lparr>Dom\<rparr> = cat_1 \<aa> \<ff>\<lparr>Cod\<rparr>
 5. op_cat (cat_1 \<aa> \<ff>)\<lparr>Comp\<rparr> = cat_1 \<aa> \<ff>\<lparr>Comp\<rparr>
 6. cat_1 \<aa> \<ff>\<lparr>CId\<rparr> = cat_1 \<aa> \<ff>\<lparr>CId\<rparr>
[PROOF STEP]
show "op_cat (cat_1 \<aa> \<ff>)\<lparr>Comp\<rparr> = cat_1 \<aa> \<ff>\<lparr>Comp\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cat (cat_1 \<aa> \<ff>)\<lparr>Comp\<rparr> = cat_1 \<aa> \<ff>\<lparr>Comp\<rparr>
[PROOF STEP]
unfolding cat_1_components op_cat_components fflip_vsingleton
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>} = ZFC_in_HOL.set {\<langle>[\<ff>, \<ff>]\<^sub>\<circ>, \<ff>\<rangle>}
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
op_cat (cat_1 \<aa> \<ff>)\<lparr>Comp\<rparr> = cat_1 \<aa> \<ff>\<lparr>Comp\<rparr>

goal (5 subgoals):
 1. cat_1 \<aa> \<ff>\<lparr>Obj\<rparr> = cat_1 \<aa> \<ff>\<lparr>Obj\<rparr>
 2. cat_1 \<aa> \<ff>\<lparr>Arr\<rparr> = cat_1 \<aa> \<ff>\<lparr>Arr\<rparr>
 3. cat_1 \<aa> \<ff>\<lparr>Cod\<rparr> = cat_1 \<aa> \<ff>\<lparr>Dom\<rparr>
 4. cat_1 \<aa> \<ff>\<lparr>Dom\<rparr> = cat_1 \<aa> \<ff>\<lparr>Cod\<rparr>
 5. cat_1 \<aa> \<ff>\<lparr>CId\<rparr> = cat_1 \<aa> \<ff>\<lparr>CId\<rparr>
[PROOF STEP]
qed (simp_all add: cat_1_components)


[STATEMENT]
lemma (in \<Z>) cat_1_op_0[cat_op_simps]: "op_cat (cat_1 0 0) = cat_1 0 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_cat (cat_1 []\<^sub>\<circ> []\<^sub>\<circ>) = cat_1 []\<^sub>\<circ> []\<^sub>\<circ>
[PROOF STEP]
by
    (
      cs_concl cs_shallow
        cs_simp: cat_op_simps cs_intro: V_cs_intros cat_cs_intros
    )