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