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