Initial stacks lie in program support

For every machine $M$ and every finite word $w$ over its input alphabet $\Gamma_{k_0}$, initialize the configuration with the main label, the initial control state, $w$ on stack $k_0$, and the empty list on every other stack. Every tagged symbol in every stack of this initial configuration belongs to $U_M$: $\forall k\in K,\ \forall a\in\Gamma_k$, membership of $a$ in that initialized stack implies $(k,a)\in U_M$. The word may be empty and is not required to satisfy any separate input-encoding promise. 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.