halting_problem_re — Mathlib

English

For each n, the set of programs c that halt on input n is recursively enumerable.

Русский

Для каждого фиксированного n множество кодов программ c, которые останавливаются на входе n, перечислимо.

LaTeX

$$$$\forall n:\mathbb{N},\; \mathrm{REPred}(\lambda c. \text{halt}_{n}(c)),$$$$

Lean4

/-- The Halting problem is recursively enumerable -/
theorem halting_problem_re (n) : REPred fun c => (eval c n).Dom :=
  (eval_part.comp Computable.id (Computable.const _)).dom_re

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