encode_lt_rfind'

Mathlib.Computability.PartrecCode

URI: https://scilib.ai/kg/mathlib#Nat.Partrec.Code.encode_lt_rfind'

English

For cf, encoding cf is less than encoding of rfind' cf.

Русский

Для cf код cf меньше кодирования rfind' cf.

LaTeX

$$$\\operatorname{encodeCode}(cf) < \\operatorname{encodeCode}(\\mathrm{rfind}'(cf))$$$

Lean4

theorem encode_lt_rfind' (cf) : encode cf < encode (rfind' cf) :=
  by
  simp only [encodeCode_eq, encodeCode]
  cutsat

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

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

Разделы

Аффилиация

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