Deciding whether a 2nfa halts on every input on every branch A 2nfa is a nondeterministic finite automaton that can move its head left or right on the input tape, or not.  Is the following language known to be decidable?
$$
\textit{H}_{\mathsf{2nfa}} = \{ \langle M \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every input and on every branch} \}
$$

Note:
This is not the same as the halting problem on 2nfa's:
$$ \mathit{HALT}_{\mathsf{2nfa}} = \{ \langle M, x \rangle \mid M \textit{ is a } \mathsf{2nfa} \textit{ that halts on every branch, running on } x \} $$
Albeit the two are related, and as follows:
$$ \langle M \rangle \in \textit{H}_{\mathsf{2nfa}} \iff \forall x, \langle M, x \rangle \in \textit{HALT}_{\mathsf{2nfa}} $$

I have attempted to write an algorithm deciding $\textit{H}_{\mathsf{2nfa}}$.  It looks for the sequence of transitions of $M$, that start and end at the same state and the overall displacement of the head along the sequence is $0$.  If there is such a loop, and some further details are satisfied, the algorithm decides that $M$ is not halting.
The problem is that I could not establish any bound on the length of the sequences to look for.  I guess that looking for sequences of length up to some function of $M$'s number of states should be enough.
Is there perhaps another, more elegant way? Even better, a known result to refer?
Lemma 1. $H_{\textsf{2nfa}}$ is decidable.

Proof.  Decide it as follows.  Given as input a two-way non-deterministic finite automaton $M_{\textsf{2nfa}}$:


Convert $M_{\textsf{2nfa}}$ into a two-way alternating finite automaton $M_{\textsf{2wafa}}$ such that the language of $M_{\textsf{2wafa}}$ is
$$L(M_{\textsf{2wafa}}) = \{x \in \Sigma^* : \text{ all execution paths of $M_{\textsf{2nfa}}$ on input $x$ halt }\},$$
that is, the set of inputs $x$ to $M_{\textsf{2nfa}}$ such that all execution paths of $M_{\textsf{2nfa}}$ on $x$ halt.  (An alternating finite automata has $\exists$-transitions and $\forall$-transitions.  Here we make every (non-deterministic) transition of $M_{\textsf{2nfa}}$ into a $\forall$-transition in $M_{\textsf{2wafa}}$, we don't use $\exists$-transitions, and we make the accept states of $M_{\textsf{2wafa}}$ be the halting states of $M_{\textsf{2nfa}}$.)
Convert $M_{\textsf{2wafa}}$ into an equivalent one-way NFA $M_{\textsf{nfa}}$. (See e.g. here.  I assume but have not verified that this conversion is computable. It appears to be computable, see the proof of Lemma 1, p. 296.)
Convert $M_{\textsf{nfa}}$ into an equivalent DFA $M_{\textsf{dfa}}$, and check whether $L(M_{\textsf{dfa}}) = \Sigma^*$ (all using standard techniques). Accept if so.  $~~\Box$