Results — Mathlib

English

Results s a n holds iff there is a membership a ∈ s and the computation terminates after exactly n steps with result a.

Русский

Results s a n выполняется тогда, когда a ∈ s и вычисление s завершается ровно за n шагов с результатом a.

LaTeX

$$$\text{Results } s\ a\ n := \exists h:\, a \in s, \text{length}(s) = n$$$

Lean4

/-- `Results s a n` completely characterizes a terminating computation:
  it asserts that `s` terminates after exactly `n` steps, with result `a`. -/
def Results (s : Computation α) (a : α) (n : ℕ) :=
  ∃ h : a ∈ s, @length _ s (terminates_of_mem h) = n

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