codeSupp_succ

Mathlib.Computability.TMToPartrec

URI: https://scilib.ai/kg/mathlib#Turing.PartrecToTM2.codeSupp_succ

English

The codeSupp of Code.succ k equals the union of trStmts₁ (trNormal (Code.succ k)) with contSupp k.

Русский

Code.succ k → codeSupp = trStmts₁ (trNormal (Code.succ k)) ∪ contSupp k.

LaTeX

$$$\forall k:\; codeSupp (Code.succ k) = trStmts₁ (trNormal (Code.succ k)) \cup contSupp k$$$

Lean4

@[simp]
theorem codeSupp_succ (k) : codeSupp Code.succ k = trStmts₁ (trNormal Code.succ k) ∪ contSupp k :=
  rfl

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

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

Разделы

Аффилиация

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