[STATEMENT]
lemma ntsmcf_tdghm_smcf_ntsmcf_comp[slicing_commute]:
  "smcf_dghm \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntsmcf_tdghm \<NN> = ntsmcf_tdghm (\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. smcf_dghm \<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M ntsmcf_tdghm \<NN> = ntsmcf_tdghm (\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)
[PROOF STEP]
unfolding
    dghm_tdghm_comp_def
    dghm_comp_def
    ntsmcf_tdghm_def
    smcf_dghm_def
    smc_dg_def
    dg_field_simps
    dghm_field_simps
    nt_field_simps
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. [\<lambda>a\<in>\<^sub>\<circ>[\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [\<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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<NN>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^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>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ> = [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>[]\<^sub>\<circ>\<rparr>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^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>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^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>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^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>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^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>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [[\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, [\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>3\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>. \<HH>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>\<NN>\<lparr>[]\<^sub>\<circ>\<rparr>\<lparr>a\<rparr>\<rparr>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>1\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, [\<HH>\<lparr>[]\<^sub>\<circ>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>[]\<^sub>\<circ>\<rparr>, \<HH>\<lparr>1\<^sub>\<nat>\<rparr> \<circ>\<^sub>\<circ> \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>1\<^sub>\<nat>\<rparr>, \<NN>\<lparr>2\<^sub>\<nat>\<rparr>\<lparr>2\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>, \<NN>\<lparr>3\<^sub>\<nat>\<rparr>, \<HH>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>\<lparr>3\<^sub>\<nat>\<rparr>]\<^sub>\<circ>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma smcf_ntsmcf_comp_NTMap_vrange:
  assumes "\<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>" and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<HH>: is_semifunctor \<alpha> \<BB> \<CC> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding dghm_tdghm_comp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<lambda>a\<in>\<^sub>\<circ>\<NN>\<lparr>NTDGDom\<rparr>\<lparr>Obj\<rparr>. \<HH>\<lparr>ArrMap\<rparr>\<lparr>\<NN>\<lparr>NTMap\<rparr>\<lparr>a\<rparr>\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by (auto simp: smc_cs_simps intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> ((\<HH> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<NN>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed