prec' — Mathlib

English

A recursive construction combining f,g,h yields a Partrec function.

Русский

Замыкание на операцию рекурсии с f,g,h даёт частично-рекурсивную функцию.

LaTeX

$$$\text{prec' }(f,g,h)$ is Partrec, i.e. the function defined by a nested recursion using f,g,h is Partrec.$$

Lean4

theorem prec' {f g h} (hf : Partrec f) (hg : Partrec g) (hh : Partrec h) :
    Partrec fun a =>
      (f a).bind fun n =>
        n.rec (g a) fun y IH => do {
          let i ← IH;
          h (Nat.pair a (Nat.pair y i))
          } :=
  ((prec hg hh).comp (pair Partrec.some hf)).of_eq fun a => ext fun s => by simp [Seq.seq]

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