Supports — Mathlib

English

For a finite set S of states and a state q in Λ', the predicate Supports(S, q) holds exactly when every terminal continuation k reachable from q has its contSupp(k) contained in S.

Русский

Для конечного множества состояний S и состояния q в Λ' предикат Supports(S, q) истинен тогда и только тогда, когда для каждого конечного продолжения k, достижимого из q, множество contSupp(k) содержится в S.

LaTeX

$$$\\mathrm{Supports}(S,q) \\iff \\forall k,\\; \\text{reachable}(q, \\mathrm{ret}(k)) \\Rightarrow \\mathrm{contSupp}(k) \\subseteq S$$$

Lean4

/-- The statement `Λ'.Supports S q` means that `contSupp k ⊆ S` for any `ret k`
reachable from `q`.
(This is a technical condition used in the proof that the machine is supported.) -/
def Supports (S : Finset Λ') : Λ' → Prop
  | Λ'.move _ _ _ q => Λ'.Supports S q
  | Λ'.push _ _ q => Λ'.Supports S q
  | Λ'.read q => ∀ s, Λ'.Supports S (q s)
  | Λ'.clear _ _ q => Λ'.Supports S q
  | Λ'.copy q => Λ'.Supports S q
  | Λ'.succ q => Λ'.Supports S q
  | Λ'.pred q₁ q₂ => Λ'.Supports S q₁ ∧ Λ'.Supports S q₂
  | Λ'.ret k => contSupp k ⊆ S

Похожие утверждения