Proofgold Object

λ x0 x1 x2 x3 . and (and (subfield x0 x1) (x3 ∈ setexp (field0 x0) (ordsucc x2))) (∀ x4 : ο . (∀ x5 . and (x5 ∈ setminus (field0 x0) (Sing (field3 x0))) (and (ap x3 x2 = x5) (∀ x6 : ο . (∀ x7 . and (x7 ∈ setexp (setexp (field0 x1) 2) x2) (and (∀ x8 . x8 ∈ x2 ⟶ ap (ap x7 x8) 1 = field4 x0) (∀ x8 . x8 ∈ field0 x1 ⟶ CRing_with_id_eval_poly x1 (ordsucc x2) x3 x8 = nat_primrec x5 (λ x10 x11 . field2b x1 x11 (CRing_with_id_eval_poly x1 2 (ap x7 x10) x8)) x2)) ⟶ x6) ⟶ x6)) ⟶ x4) ⟶ x4)

type
ι → ι → ι → ι → ο

theory
HotG

name
-

definition
PUXQg..

Megalodon
-

proofgold address
TMLji..

creator
5919 Pr6Pc../659bf..

owner
5919 Pr6Pc../659bf..

term root
51ff5..