Finite symbol support of a statement

For every machine $M$ and every one of its statements $q$, the set $U(q)$ described here is finite. This finiteness assertion concerns the tagged range of each push function over all control states and the finite statement syntax, not finiteness of every underlying stack alphabet. Here $M$ is a TM2 machine with a finite type $K$ of stack indices and decidable equality on $K$, designated input and output indices $k_0,k_1$, stack-symbol types $\Gamma_k$, a finite type $\Lambda$ of program labels with a main label, a finite type $\sigma$ of control states with an initial state, a finite input alphabet $\Gamma_{k_0}$, and a statement $m(\ell)$ for each label $\ell\in\Lambda$. No finiteness of $\Gamma_k$ for other $k$ is assumed. A tagged symbol $(k,a)$ has $k\in K$ and $a\in\Gamma_k$; tags from different stacks remain distinct. For a statement $q$, its set $U(q)$ of syntactically possible pushed tagged symbols is recursively defined: a push onto $k$ with symbol function $f:\sigma\to\Gamma_k$ and continuation $q_0$ contributes $\{(k,f(v)):v\in\sigma\}\cup U(q_0)$; a peek, pop, or control-state load contributes only its continuation’s set; a conditional branch contributes the union of both branch sets; a jump to a program label and a halt contribute the empty set. Thus both branch bodies and all control states are counted, regardless of reachability, while a jump does not recursively inspect its target.