Proofgold Object

λ x0 . λ x1 : ι → ι . nat_primrec 0 (λ x2 x3 . add_SNo x3 (x1 x2)) x0

type
ι → (ι → ι) → ι

theory
HotG

name
finite_add_SNo

definition
PULfh..

Megalodon
finite_add_SNo

proofgold address
TMHPx..^{finite_add_SNo}

creator
16612 PrGxv../b75a4..

owner
16612 PrGxv../b75a4..

term root
73933..