Proving closure under complementation of languages accepted by min-heap automata
Claim: $\mathrm{HAL}$ is not closed against complement.

Proof Idea: We have agreed that $\mathrm{EPAL}$ (the language of even palindromes over a non-unary alphabet) is not in $\mathrm{HAL}$. We show that $\overline{\mathrm{EPAL}} \in \mathrm{HAL}$.
This works for type-1 only (as type-2 can accept $\mathrm{EPAL}$); the proof can be adapted to suit type-2 though, see below.

Proof: Note that

$\qquad \displaystyle \begin{align*}
  \overline{\mathrm{EPAL}} &amp;= \{vw : |v|=|w|, v\neq w^R\} \\
                           &amp;\cup\ \,\{w : |w| \in 2\mathbb{N}\!+\!1\}
\end{align*}$

We construct a min-heap automaton with two heap symbols $b &lt; a$ that works like this:


In the starting state, decide nondeterministically wether the input's length is even.
On the uneven path, use finite control to accept the input if and only if its length is odd.
On the even path, proceed like this:
$$ \underbrace{v_1\ \dots\ \mathbf{v_{i}}}_{+a}\ \underbrace{v_{i+1}\ \dots\ v_n}_{+b}\ \underbrace{w_n\ \dots\ w_{i+1}}_{-b}\ \underbrace{\mathbf{w_i}\ \dots\ w_1}_{-a}$$


Start by adding one $a$ to heap for every read symbol.
At a nondeterministically determined position, store the current symbol in finite control and start adding one $b$ (and no $a$) to heap for every read symbol.
At a nondeterministically determined position, stop adding symbols and consume one $b$ per input symbol.
When all $b$ are consumed, compare the current symbol with the one stored in control. If they are unequal, continue; else reject the input.
Consume one $a$ per input symbol. If the heap is empty at the same time the input ends, accept the word; reject otherwise.



The described min-heap automaton accepts $\overline{\mathrm{EPAL}}$. As its complement, $\mathrm{EPAL}$, is not in $\mathrm{HAL}$, we have proven the claim.

Note: The proof can be performed in the same way with $\{ww \mid w \in \{a,b\}^*\}$ (which is in $\mathrm{CSL} \setminus \mathrm{HAL}$) and its complement. This extends above result to type-2.