[STATEMENT]
lemma ntsmcf_comp_interchange_law:
  \<comment>\<open>See Chapter II-5 in \cite{mac_lane_categories_2010}.\<close>
  assumes "\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
    and "\<MM>' : \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
    and "\<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>"
  shows
    "((\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>') \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)) =
      (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<MM>: is_ntsmcf \<alpha> \<AA> \<BB> \<GG> \<HH> \<MM>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<MM>': is_ntsmcf \<alpha> \<BB> \<CC> \<GG>' \<HH>' \<MM>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM>' : \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(3))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<NN>': is_ntsmcf \<alpha> \<BB> \<CC> \<FF>' \<GG>' \<NN>'
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(4))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<NN>'\<NN>:
    is_ntsmcf \<alpha> \<AA> \<CC> \<open>\<FF>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<FF>\<close> \<open>\<GG>' \<circ>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>\<close> \<open>\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' \<circ>\<^sub>D\<^sub>G\<^sub>H\<^sub>M \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
interpret \<MM>\<NN>: is_ntsmcf \<alpha> \<AA> \<BB> \<FF> \<HH> \<open>\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)
[PROOF STEP]
proof(rule ntsmcf_eqI[of \<alpha>])
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. (\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>
 4. ?\<FF> = ?\<FF>'
 5. ?\<GG> = ?\<GG>'
 6. ?\<AA> = ?\<AA>'
 7. ?\<BB> = ?\<BB>'
[PROOF STEP]
show
      "(\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> =
        (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>
[PROOF STEP]
proof
      (
        rule vsv_eqI,
        unfold
          ntsmcf_vcomp_NTMap_vdomain[OF \<NN>'\<NN>.is_ntsmcf_axioms]
          ntsmcf_hcomp_NTMap_vdomain[OF \<MM>\<NN>.is_ntsmcf_axioms]
      )
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
fix a
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. vsv ((\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
assume "a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>"
[PROOF STATE]
proof (state)
this:
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (4 subgoals):
 1. vsv ((\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
 4. \<And>a. a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr> \<Longrightarrow> (\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
with assms
[PROOF STATE]
proof (chain)
picking this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<MM>' : \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
show
        "(\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> =
          ((\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM>) \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>"
[PROOF STATE]
proof (prove)
using this:
\<MM> : \<GG> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
\<MM>' : \<GG>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
\<NN>' : \<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG>' : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
a \<in>\<^sub>\<circ> \<AA>\<lparr>Obj\<rparr>

goal (1 subgoal):
 1. (\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>
[PROOF STEP]
by
          (
            cs_concl
              cs_simp: smc_cs_simps is_ntsmcf.ntsmcf_Comp_commute'
              cs_intro: smc_cs_intros
          )
[PROOF STATE]
proof (state)
this:
(\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>\<lparr>a\<rparr>

goal (3 subgoals):
 1. vsv ((\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 2. vsv ((\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>)
 3. \<AA>\<lparr>Obj\<rparr> = \<AA>\<lparr>Obj\<rparr>
[PROOF STEP]
qed (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
(\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr> = (\<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>))\<lparr>NTMap\<rparr>

goal (6 subgoals):
 1. \<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG> : ?\<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>
 2. \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) : ?\<FF>' \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F ?\<GG>' : ?\<AA>' \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> ?\<BB>'
 3. ?\<FF> = ?\<FF>'
 4. ?\<GG> = ?\<GG>'
 5. ?\<AA> = ?\<AA>'
 6. ?\<BB> = ?\<BB>'
[PROOF STEP]
qed (auto intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<MM>' \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>) = \<MM>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<MM> \<bullet>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F (\<NN>' \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<NN>)

goal:
No subgoals!
[PROOF STEP]
qed


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


[STATEMENT]
lemma ntsmcf_smcf_comp_NTMap_vrange:
  assumes "\<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>" and "\<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>"
  shows "\<R>\<^sub>\<circ> ((\<NN> \<circ>\<^sub>N\<^sub>T\<^sub>S\<^sub>M\<^sub>C\<^sub>F\<^sub>-\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<HH>)\<lparr>NTMap\<rparr>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<NN>: is_ntsmcf \<alpha> \<BB> \<CC> \<FF> \<GG> \<NN>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<NN> : \<FF> \<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^sub>F \<GG> : \<BB> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<CC>
[PROOF STEP]
by (rule assms(1))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
interpret \<HH>: is_semifunctor \<alpha> \<AA> \<BB> \<HH>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<HH> : \<AA> \<mapsto>\<mapsto>\<^sub>S\<^sub>M\<^sub>C\<^bsub>\<alpha>\<^esub> \<BB>
[PROOF STEP]
by (rule assms(2))
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<R>\<^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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
unfolding tdghm_dghm_comp_components
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<R>\<^sub>\<circ> (\<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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>
[PROOF STEP]
by (auto simp: smc_cs_simps intro: smc_cs_intros)
[PROOF STATE]
proof (state)
this:
\<R>\<^sub>\<circ> ((\<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>) \<subseteq>\<^sub>\<circ> \<CC>\<lparr>Arr\<rparr>

goal:
No subgoals!
[PROOF STEP]
qed