Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 x2 . ∀ x3 : ι → ι → ο . (∀ x4 x5 . x3 x4 x5x3 x5 x4)or (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x0 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)x3 x6 x7))x4)x4) (∀ x4 : ο . (∀ x5 . and (x5x2) (and (atleastp x1 x5) (∀ x6 . x6x5∀ x7 . x7x5(x6 = x7∀ x8 : ο . x8)not (x3 x6 x7)))x4)x4)
as obj
f88df..
as prop
-
theory
HotG
stx
ea22c..
address
TMXhy..