zero_rmatch

Mathlib.Computability.RegularExpressions

URI: https://scilib.ai/kg/mathlib#RegularExpression.zero_rmatch

English

The zero expression matches nothing: for every input x, rmatch 0 x is false.

Русский

Нулевое выражение не соответствует ни одному входу: для любого x выполняется rmatch 0 x = ложь.

LaTeX

$$$$ rmatch(0, x) = \\text{false} \\quad \\forall x. $$$$

Lean4

@[simp]
theorem zero_rmatch (x : List α) : rmatch 0 x = false := by induction x <;> simp [rmatch, matchEpsilon, *]

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

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

Разделы

Аффилиация

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