Set_of_Sequence_Codes_is_Primitive_Recursive

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

computabilityprimitive-recursive-functionsproofwiki

Let $\operatorname{Seq}$ be the set of all code numbers of finite sequences in $\N$ . Then $\operatorname{Seq}$ is primitive recursive.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Set_of_Sequence_Codes_is_Primitive_Recursive : ∃ (encode : List ℕ → ℕ) (decode : ℕ → Option (List ℕ)), ∀ l, decode (encode l) = some l := by sorry

Source

https://proofwiki.org/wiki/Set_of_Sequence_Codes_is_Primitive_Recursive

View graph