English
For finite sets K and S of Λ', the predicate Supports(K,S) asserts that every q in K has its trace TM2-structure tr(q) that is TM2-supported with respect to S.
Русский
Для конечных множеств K и S Λ' предикат Supports(K,S) утверждает, что каждый элемент q из K имеет трейс TM2-структуры tr(q), который поддерживается TM2 относительно S.
LaTeX
$$$\\mathrm{Supports}(K,S) \\iff \\forall q \\in K,\\; \\mathrm{TM2.SupportsStmt}(S, \\mathrm{tr}(q)).$$$
Lean4
/-- A shorthand for the predicate that we are proving in the main theorems `trStmts₁_supports`,
`codeSupp'_supports`, `contSupp_supports`, `codeSupp_supports`. The set `S` is fixed throughout
the proof, and denotes the full set of states in the machine, while `K` is a subset that we are
currently proving a property about. The predicate asserts that every state in `K` is closed in `S`
under forward simulation, i.e. stepping forward through evaluation starting from any state in `K`
stays entirely within `S`. -/
def Supports (K S : Finset Λ') :=
∀ q ∈ K, TM2.SupportsStmt S (tr q)
