[STATEMENT]
lemma op_tdghm_tdghm_dghm_comp[dg_op_simps]:
  "op_tdghm (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) = op_tdghm \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<HH>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. op_tdghm (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>) = op_tdghm \<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M op_dghm \<HH>
[PROOF STEP]
unfolding
    tdghm_dghm_comp_def
    dghm_comp_def
    op_tdghm_def
    op_dghm_def
    op_dg_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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^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>]\<^sub>\<circ>]\<^sub>\<circ>\<lparr>4\<^sub>\<nat>\<rparr>]\<^sub>\<circ>
[PROOF STEP]
by (simp add: nat_omega_simps)


[STATEMENT]
lemma tdghm_dghm_comp_is_tdghm:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>" and "\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<NN>: is_tdghm \<alpha> \<BB> \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
interpret \<HH>: is_dghm \<alpha> \<AA> \<BB> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
proof(rule is_tdghmI)
[PROOF STATE]
proof (state)
goal (12 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>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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. vsv ((\<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>)
 7. \<D>\<^sub>\<circ> ((\<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>) = \<AA>\<lparr>Obj\<rparr>
 8. (\<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>
 9. (\<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>
 10. (\<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>
A total of 12 subgoals...
[PROOF STEP]
show "vfsequence (\<NN> \<circ>\<^sub>T\<^sub>D\<^sub>G\<^sub>H\<^sub>M\<^sub>-\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<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
[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 (11 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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. vsv ((\<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>)
 6. \<D>\<^sub>\<circ> ((\<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>) = \<AA>\<lparr>Obj\<rparr>
 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 "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 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 (10 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. vsv ((\<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>)
 5. \<D>\<^sub>\<circ> ((\<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>) = \<AA>\<lparr>Obj\<rparr>
 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. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<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>a\<rparr> : (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
show "(\<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> :
      (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>"
      if "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>" for a
[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>a\<rparr> : (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
        (
          use that in
            \<open>cs_concl cs_shallow cs_simp: dg_cs_simps cs_intro: dg_cs_intros\<close>
        )
[PROOF STATE]
proof (state)
this:
?a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<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>?a\<rparr> : (\<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr> \<mapsto>\<^bsub>\<CC>\<^esub> (\<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>)\<lparr>ObjMap\<rparr>\<lparr>?a\<rparr>

goal (9 subgoals):
 1. \<Z> \<alpha>
 2. \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 3. \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
 4. vsv ((\<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>)
 5. \<D>\<^sub>\<circ> ((\<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>) = \<AA>\<lparr>Obj\<rparr>
 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>
[PROOF STEP]
qed (cs_concl cs_simp: dg_cs_simps cs_intro: dg_cs_intros)+
[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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma tdghm_dghm_comp_is_tdghm'[dg_cs_intros]:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<FF>' = \<FF> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>"
    and "\<GG>' = \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH>"
  shows "\<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>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
using assms(1,2)
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG>' : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
unfolding assms(3,4)
[PROOF STATE]
proof (prove)
using this:
\<NN> : \<FF> \<mapsto>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^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>D\<^sub>G\<^sub>H\<^sub>M \<GG> \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>D\<^sub>G\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule tdghm_dghm_comp_is_tdghm)