Proofgold Object

λ x0 . ap (nat_primrec (lam omega (λ x1 . If_i (x1 = 0) 1 0)) (λ x1 x2 . lam omega (λ x3 . If_i (x3 = 0) 1 (add_nat (ap x2 (prim3 x3)) (ap x2 x3)))) x0)

type
ι → ι → ι

theory
HotG

name
-

definition
PUfRN..

Megalodon
-

proofgold address
TMVNC..

creator
4972 Pr6Pc../01929..

owner
4972 Pr6Pc../01929..

term root
a2a94..