results_of_terminates' — Mathlib

English

If s terminates and a ∈ s, then s terminates with a in exactly length(s) steps.

Русский

Если s завершается и a ∈ s, тогда s завершается с a за exactly length(s) шагов.

LaTeX

$$$\forall s\,[T:\, \text{Terminates } s], {a:\,\alpha}, a \in s \rightarrow \text{Results } s a (\text{length } s)$$$

Lean4

theorem results_of_terminates' (s : Computation α) [T : Terminates s] {a} (h : a ∈ s) : Results s a (length s) := by
  rw [← get_eq_of_mem _ h]; apply results_of_terminates

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