English
The finite set of states codeSupp for Code.zero' on k equals the union of the states reached by trStmts₁ after trNormal, together with contSupp k.
Русский
Конечное множество состояний codeSupp для Code.zero' на k состоит из объединения состояний, достигаемых через trStmts₁ после trNormal, и contSupp k.
LaTeX
$$$\forall k\; codeSupp\; Code.zero'\; k = trStmts₁( trNormal( Code.zero', k)) \cup contSupp k$$$
Lean4
/-- The (finite!) set of machine states visited during the course of evaluation of `c` in
continuation `k`. This is actually closed under forward simulation (see `tr_supports`), and the
existence of this set means that the machine constructed in this section is in fact a proper
Turing machine, with a finite set of states. -/
def codeSupp (c : Code) (k : Cont') : Finset Λ' :=
codeSupp' c k ∪ contSupp k
