length

Mathlib.Data.Seq.Computation

URI: https://scilib.ai/kg/mathlib#Computation.Results.length

English

If s has a terminating witness, then length(s) equals the n in Results s a n.

Русский

Если у s есть завершающее свидетельство, то length(s) равно n из Results s a n.

LaTeX

$$$\forall s\, {a}\, {n},\; \text{Results } s a n \rightarrow \text{length } s = n$$$

Lean4

theorem length {s : Computation α} {a n} [_T : Terminates s] : Results s a n → length s = n
  | ⟨_, h⟩ => h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru