Proofgold Object

λ x0 x1 . λ x2 : ι → ι . λ x3 . explicit_Nats_primrec x0 x1 x2 x3 (λ x4 . explicit_Nats_one_plus x0 x1 x2 x3)

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

theory
HotG

name
explicit_Nats_one_mult_alt

definition
PUfRN..

Megalodon
-

proofgold address
TMc44..

creator
4972 Pr6Pc../24d69..

owner
4972 Pr6Pc../24d69..

term root
4999b..