English
Primrec_recOn confirms that recursion on Nat.Partrec.Code is primitive recursive.
Русский
Primrec_recOn подтверждает примитивную рекурсивность рекурсии над Nat.Partrec.Code.
LaTeX
$$$\\operatorname{Primrec\_recOn}$$$
Lean4
/-- Recursion on `Nat.Partrec.Code` is primitive recursive. -/
theorem primrec_recOn {α σ} [Primcodable α] [Primcodable σ] {c : α → Code} (hc : Primrec c) {z : α → σ} (hz : Primrec z)
{s : α → σ} (hs : Primrec s) {l : α → σ} (hl : Primrec l) {r : α → σ} (hr : Primrec r)
{pr : α → Code → Code → σ → σ → σ}
(hpr : Primrec fun a : α × Code × Code × σ × σ => pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2)
{co : α → Code → Code → σ → σ → σ}
(hco : Primrec fun a : α × Code × Code × σ × σ => co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2)
{pc : α → Code → Code → σ → σ → σ}
(hpc : Primrec fun a : α × Code × Code × σ × σ => pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) {rf : α → Code → σ → σ}
(hrf : Primrec fun a : α × Code × σ => rf a.1 a.2.1 a.2.2) :
let F (a : α) (c : Code) : σ := Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a)
Primrec fun a => F a (c a) :=
primrec_recOn' hc hz hs hl hr (pr := fun a b => pr a b.1 b.2.1 b.2.2.1 b.2.2.2) (.mk hpr) (co := fun a b =>
co a b.1 b.2.1 b.2.2.1 b.2.2.2) (.mk hco) (pc := fun a b => pc a b.1 b.2.1 b.2.2.1 b.2.2.2) (.mk hpc) (rf :=
fun a b => rf a b.1 b.2) (.mk hrf)
