Search for blocks/addresses/...

Proofgold Object

λ x0 . λ x1 x2 : ι → ι . λ x3 x4 x5 . λ x6 x7 : ι → ι → ι . and (and (and (and (and (and (and (and (explicit_Field x0 x3 x4 x6 x7) (∀ x8 : ο . (∀ x9 : ι → ι → ο . explicit_Reals {x10 ∈ x0|x1 x10 = x10} x3 x4 x6 x7 x9x8)x8)) (∀ x8 . x8x0x2 x8{x9 ∈ x0|x1 x9 = x9})) (x5x0)) (∀ x8 . x8x0x1 x8x0)) (∀ x8 . x8x0x2 x8x0)) (∀ x8 . x8x0x8 = x6 (x1 x8) (x7 x5 (x2 x8)))) (∀ x8 . x8x0∀ x9 . x9x0x1 x8 = x1 x9x2 x8 = x2 x9x8 = x9)) (x6 (x7 x5 x5) x4 = x3)
type
ι(ιι) → (ιι) → ιιι(ιιι) → (ιιι) → ο
theory
HotG
name
explicit_Complex
definition
PUefP..
Megalodon
explicit_Complex
proofgold address
TMRhn..explicit_Complex
creator
4913 Pr6Pc../46214..
owner
4913 Pr6Pc../46214..
term root
bacb8..