A statement preserves its symbol support

For every machine $M$, set $S$ of tagged symbols, statement $q$, hypothesis $U(q)\subseteq S$, control state $v\in\sigma$, stack family $\operatorname{stk}(k)\in\Gamma_k^*$, and hypothesis $\forall k\in K,\ \forall a\in\Gamma_k,\ a\in\operatorname{stk}(k)\Rightarrow(k,a)\in S$, execute $q$ from $v$ and these stacks once as described here, and let $\operatorname{stk}^\prime$ be the stacks in its returned configuration. The conclusion is $\forall k\in K,\ \forall a\in\Gamma_k,\ a\in\operatorname{stk}^\prime(k)\Rightarrow(k,a)\in S$. The set $S$ need not be finite, no reachability hypothesis is required, and the statement proves preservation for this one statement execution, including a returned jump or halt. 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. Executing one statement pushes the symbol selected by the current state, peeks at or pops the current stack head (using an absent-head value for an empty stack and an empty tail when popping it), or changes the control state as specified, then executes the continuation; a branch executes its selected body, and jump/halt returns a configuration with a label/no label and unchanged stacks. A jump does not execute the next labeled statement within this same statement execution.