Proofgold Object

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 x6 x7 . nat_primrec x1 (λ x8 . x3 (x4 (ap x6 x8) (explicit_Ring_with_id_exp_nat x0 x1 x2 x3 x4 x7 x8))) x5

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

theory
HotG

name
explicit_Ring_with_id_eval_poly

definition
PUXmz..

Megalodon
explicit_Ring_eval_poly

proofgold address
TMMeQ..^{explicit_Ring_eval_poly}

creator
4954 Pr6Pc../46de6..

owner
4954 Pr6Pc../46de6..

term root
7e80c..