Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)not (or (∀ x1 : ο . (∀ x2 . and (x2u9) (and (equip u3 x2) (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x0 x3 x4))x1)x1) (∀ x1 : ο . (∀ x2 . and (x2u9) (and (equip u4 x2) (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)not (x0 x3 x4)))x1)x1))∀ x1 . x1u9∀ x2 : ο . (∀ x3 . x3u9∀ x4 . x4u9∀ x5 . x5u9(x1 = x3∀ x6 : ο . x6)(x1 = x4∀ x6 : ο . x6)(x1 = x5∀ x6 : ο . x6)(x3 = x4∀ x6 : ο . x6)(x3 = x5∀ x6 : ο . x6)(x4 = x5∀ x6 : ο . x6)x0 x1 x3x0 x1 x4x0 x1 x5not (x0 x3 x4)not (x0 x3 x5)not (x0 x4 x5)(∀ x6 . x6u9x0 x1 x6x6SetAdjoin (SetAdjoin (UPair x1 x3) x4) x5)x2)x2
as obj
-
as prop
e041c..
theory
HotG
stx
3dc23..
address
TMSA3..