[STATEMENT]
lemma op_ntsmcf_ntsmcf_smcf_comp[smc_op_simps]:
  "op_ntsmcf (\<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>) = op_ntsmcf \<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F op_smcf \<HH>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_ntsmcf (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) = op_ntsmcf \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_smcf \<HH>
[PROOF STEP]
unfolding
    tdghm_dghm_comp_def
    dghm_comp_def
    op_ntsmcf_def
    op_smcf_def
    op_smc_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip ([\<lambda>a\<in>\<^sub>\<circ>\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ> = [\<lambda>a\<in>\<^sub>\<circ>[\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>[\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [[\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr>, [\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>, [\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>, [\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, fflip (\<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>4\<^sub>\<nat>\<rparr>)]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


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

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

goal (1 subgoal):
 1. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

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

goal (1 subgoal):
 1. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (cs_concl cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

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

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

goal (1 subgoal):
 1. ntsmcf_tdghm (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) : smcf_dghm (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>
[PROOF STEP]
by
        (
          cs_concl
            cs_simp: slicing_commute[symmetric]
            cs_intro: slicing_intros dg_cs_intros
        )
[PROOF STATE]
proof (state)
this:
ntsmcf_tdghm (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) : smcf_dghm (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M smcf_dghm (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) : smc_dg \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> smc_dg \<CC>

goal (6 subgoals):
 1. \<Z> \<alpha>
 2. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTDom\<rparr> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 3. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTCod\<rparr> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 4. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTDGDom\<rparr> = \<AA>
 5. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTDGCod\<rparr> = \<CC>
 6. \<And>a b f. f : a \<mapsto>\<^bsub>\<AA>\<^esub> b \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show
      "(\<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> =
        (\<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
      if "f : a \<mapsto>\<^bsub>\<AA>\<^esub> b" for a b f
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
using that
[PROOF STATE]
proof (prove)
using this:
f : a \<mapsto>\<^bsub>\<AA>\<^esub> b

goal (1 subgoal):
 1. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by (cs_concl cs_simp: smc_cs_simps cs_intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
?f : ?a \<mapsto>\<^bsub>\<AA>\<^esub> ?b \<Longrightarrow> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>?b\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> = (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ArrMap\<rparr>\<lparr>?f\<rparr> \<circ>\<^sub>A\<^bsub>\<CC>\<^esub> (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTMap\<rparr>\<lparr>?a\<rparr>

goal (5 subgoals):
 1. \<Z> \<alpha>
 2. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTDom\<rparr> = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 3. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTCod\<rparr> = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>
 4. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTDGDom\<rparr> = \<AA>
 5. (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>NTDGCod\<rparr> = \<CC>
[PROOF STEP]
qed (auto simp: smc_cs_simps)
[PROOF STATE]
proof (state)
this:
\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma ntsmcf_smcf_comp_is_semifunctor'[smc_cs_intros]:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<FF>' = \<FF> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>"
    and "\<GG>' = \<GG> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>"
  shows "\<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

goal (1 subgoal):
 1. \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
unfolding assms(3,4)
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>

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