Computational power of nondeterministic type-1 min-heap automata with multiple heaps
Let $\mathrm{SDL}_k$ the shuffled Dyck language with $k$ types of parentheses, i.e.

$\qquad \displaystyle \mathrm{SDL}_k = \mathrm{DL}([_1,]_1) \, ш\, \dots \, ш\, \mathrm{DL}([_k,]_k)$

with $ш$ the shuffle of languages and $\mathrm{DL}(\_,\_)$ the Dyck language with matching parenthesis as specified. Intuitively, any word in $\mathrm{SDL}_k$ contains of $k$ properly nested words of parentheses interleaved arbitrarily; for instance, $[_3 [_1 [_1 [_3 [_2 ]_1 ]_3 ]_2 [_1 ]_1 [_2 ]_1 ]_3 ]_2\in \mathrm{SDL}_3$.

Fact 0: $\mathrm{HAL}_1^{(k)} \subseteq \mathrm{HAL}_1^{(k+1)}$ for $k\geq 1$

Claim 1: $\mathrm{SDL}_k \in \mathrm{HAL}_1^{(k)}$ for $k\geq 1$

Claim 2: $\mathrm{SDL}_{k+1} \notin \mathrm{HAL}_1^{(k)}$ for $k\geq 1$ (the claim is wrong; see below)

Together, fact and claims show that $\mathrm{HAL}_1^{(k)} \subset \mathrm{HAL}_1^{(k+1)}$ and $\mathrm{HAL}_1^{(k)} \subset \mathrm{RE}$ for for $k\geq 1$.



Ad Claim 1: It is clear that $\mathrm{DL}([,]) \in \mathrm{HAL}_1$; min-heaps can implement a counter that is increased by one on $[$ and decreased by one on $]$. A word is accepted if and only if the counter never becomes negative and is zero at the end.

The same principle is used for $\mathrm{SDL}_k$ on a $k$-heap automaton; we maintain one counter per parenthesis type on a dedicated heap each and accept if and only if no counter becomes negative and all counters are zero at the end.

Ad Claim 2: This is more a sketch. In order to accept $\mathrm{SDL}_{k+1}$ an automaton has to be able to check at any time wether $]_i$ is allowed next for any $i=1,\dots,k+1$. As nesting depth and "shuffle depth" are unbounded, finite control can not do this (not even for one parenthesis type). Since a $k$-heap automaton can only access $k$ bits of (heap) information at any time, it has no way of doing the necessary checks.





Claim 2 is in fact false. We have to be remember that type-1 heap automata can essentially store a finite amount of counters but can only access the top most. With two heaps, we can access all counters of the first heap: if we want to access counter $i$, move the symbols encoding counters $1,\dots,i-1$ to the second heap, access counter $i$ and move everything back. That leads us to the following claims:

Claim I: $\mathrm{HAL}_1 \subset \mathrm{HAL}_1^{(2)}$

Claim II: $\mathrm{HAL}_1^{(2)} = \mathrm{HAL}_1^{(3)} = \dots$

Claim I follows from above reasoning with $\mathrm{SDL}_2$. Claim II holds because $k$-heap automata can only manage finitely many counters, no matter the $k$, which can be simulated by a $2$-heap automata as outlined above.

This train of thought leads us to

Claim III: $\mathrm{HAL}_1^{(2)} \subset RE$

as Turing machines can handle unbounded numbers of counters, outclassing $2$-heap automata. As a concrete example, consider

$\qquad \displaystyle \mathrm{SDL} = \bigcup\limits_{k\geq 1} \mathrm{SDL}_k.$

Note that $\mathrm{SDL}$ can be expressed using a finite alphabet by encoding $[_i$ as e.g. $[\{\overline{i}\}$ with $\overline{i}$ the binary representation of $i$ and $]_i$ similarly.