English
If f and g are Primrec' on n inputs, and h is Primrec' on n+2 inputs, then the recursion generated by f and g with step h yields a Primrec' function of n inputs.
Русский
Если f и g — Primrec' на входах n, а h — Primrec' на входах n+2, то рекурсивное построение даёт Primrec' на входах n.
LaTeX
$$$\forall {n\ f}\ {g}\ {h},\ hf:\ Primrec'\ n\ f,\ hg:\ Primrec'\ n\ g,\ hh:\ Primrec'\ (n+2)\ h\Rightarrow\ Primrec'\ fun\ v => (f\ v).rec (g\ v)\ (fun\ y\ IH : NAT => h (y ::ᵥ IH ::ᵥ v)).$$$
Lean4
theorem prec' {n f g h} (hf : @Primrec' n f) (hg : @Primrec' n g) (hh : @Primrec' (n + 2) h) :
@Primrec' n fun v => (f v).rec (g v) fun y IH : ℕ => h (y ::ᵥ IH ::ᵥ v) := by
simpa using comp' (prec hg hh) (hf.cons idv)
