English
If q is S-supported, then trStmts₁ q ∪ K is S-supported provided K ⊆ S and the supports of K are guaranteed.
Русский
Если q поддерживается S, тогда trStmts₁ q ∪ K поддерживается S при условии K ⊆ S и гарантии поддержки K.
LaTeX
$$$\\mathrm{Supports}(\\mathrm{trStmts₁}(q) \\cup K, S) \\Leftarrow \\mathrm{Supports}(\\mathrm{trStmts₁}(q), S) \\text{ и } (K \\subseteq S \\to \\mathrm{Supports}(K,S)).$$$
Lean4
/-- The set `codeSupp c k` is a finite set that witnesses the effective finiteness of the `tr`
Turing machine. Starting from the initial state `trNormal c k`, forward simulation uses only
states in `codeSupp c k`, so this is a finite state machine. Even though the underlying type of
state labels `Λ'` is infinite, for a given partial recursive function `c` and continuation `k`,
only finitely many states are accessed, corresponding roughly to subterms of `c`. -/
theorem tr_supports (c k) : @TM2.Supports _ _ _ _ ⟨trNormal c k⟩ tr (codeSupp c k) :=
⟨codeSupp_self _ _ (trStmts₁_self _), fun _ => codeSupp_supports (Finset.Subset.refl _) _⟩
