Search for blocks/addresses/...

Proofgold Object

λ x0 : ι → ο . λ x1 : ι → ι → ι → ο . λ x2 : ι → ι . λ x3 : ι → ι → ι → ι → ι → ι . λ x4 x5 x6 x7 x8 x9 x10 x11 . λ x12 : ι → ι → ι → ι . and (and (and (and (and (and (and (and (and (x0 x4) (x0 x5)) (x0 x6)) (x1 x4 x6 x7)) (x1 x5 x6 x8)) (x0 x9)) (x1 x9 x4 x10)) (x1 x9 x5 x11)) (x3 x9 x4 x6 x7 x10 = x3 x9 x5 x6 x8 x11)) (∀ x13 . x0 x13∀ x14 . x1 x13 x4 x14∀ x15 . x1 x13 x5 x15x3 x13 x4 x6 x7 x14 = x3 x13 x5 x6 x8 x15and (and (and (x1 x13 x9 (x12 x13 x14 x15)) (x3 x13 x9 x4 x10 (x12 x13 x14 x15) = x14)) (x3 x13 x9 x5 x11 (x12 x13 x14 x15) = x15)) (∀ x16 . x1 x13 x9 x16x3 x13 x9 x4 x10 x16 = x14x3 x13 x9 x5 x11 x16 = x15x16 = x12 x13 x14 x15))
type
(ιο) → (ιιιο) → (ιι) → (ιιιιιι) → ιιιιιιιι(ιιιι) → ο
theory
HotG
name
MetaCat_pullback_p
definition
PUh86..
Megalodon
pullback_p
proofgold address
TMZas..pullback_p
creator
9866 PrCx1../21192..
owner
9866 PrCx1../21192..
term root
aa77e..