Proofgold Object

λ x0 . λ x1 : ι → ο . λ x2 x3 : ι → ι . λ x4 x5 : ι → ι → ι . λ x6 . nat_primrec 1 (λ x7 . CD_mul x0 x1 x2 x3 x4 x5 x6)

type
ι → (ι → ο) → (ι → ι) → (ι → ι) → (ι → ι → ι) → (ι → ι → ι) → ι → ι → ι

theory
HotG

name
CD_exp_nat

definition
PUYQJ..

Megalodon
CD_exp_nat

proofgold address
TMFs9..^CD_exp_nat

creator
28412 PrQUS../b168d..

owner
28412 PrQUS../b168d..

term root
7fdc7..