Finite symbol support of a fixed program

For every machine $M$, the set $U_M$ of all its input-alphabet symbols together with all syntactically possible pushed tagged symbols of all labeled statements is finite. This is one set depending only on the machine, with no particular input or execution selected. 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. Put $U_M=\{(k_0,a):a\in\Gamma_{k_0}\}\cup\bigcup_{\ell\in\Lambda}U(m(\ell))$, including every input-alphabet symbol and all syntactically possible pushes from every labeled statement.