Search for blocks/addresses/...

Proofgold Object

λ x0 x1 x2 . λ x3 x4 : ι → ι → ι . λ x5 : ι → ι → ο . and (and (and (and (and (explicit_Field x0 x1 x2 x3 x4) (∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x5 x6 x7x5 x7 x8x5 x6 x8)) (∀ x6 . x6x0∀ x7 . x7x0iff (and (x5 x6 x7) (x5 x7 x6)) (x6 = x7))) (∀ x6 . x6x0∀ x7 . x7x0or (x5 x6 x7) (x5 x7 x6))) (∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0x5 x6 x7x5 (x3 x6 x8) (x3 x7 x8))) (∀ x6 . x6x0∀ x7 . x7x0x5 x1 x6x5 x1 x7x5 x1 (x4 x6 x7))
type
ιιι(ιιι) → (ιιι) → (ιιο) → ο
theory
HotG
name
explicit_OrderedField
definition
PUefP..
Megalodon
explicit_OrderedField
proofgold address
TMUVE..explicit_OrderedField
creator
4913 Pr6Pc../e3308..
owner
4913 Pr6Pc../e3308..
term root
a18f7..