Search for blocks/addresses/...

Proofgold Term Root Disambiguation

(∀ x0 : ι → ο . ∀ x1 : ι → ι . and ((x0 (x1 (binintersect (x1 (Power 0)) (x1 (binrep (Power (Power (Power 0))) 0))))TransSet (x1 0)∀ x2 . In x2 0∀ x3 : ο . (∀ x4 . and (Subq x4 x2) (exactly2 (ordsucc (x1 x4)))x3)x3)∀ x2 : ο . (∀ x3 . and (∀ x4 : ο . (∀ x5 . and (Subq x5 x3) (x3 = x1 x3∀ x6 : ο . (∀ x7 . and (Subq x7 x3) (not (x0 (setprod x5 (binrep (Power (binrep (Power (Power 0)) 0)) (Power (Power 0))))))x6)x6)x4)x4) (not (SNo x3))x2)x2) (not (x0 (x1 (x1 (x1 (binrep (binrep (Power (binrep (Power (Power 0)) 0)) (Power 0)) 0)))))))∀ x0 : ο . x0
as obj
-
as prop
fec13..
theory
HF
stx
6735c..
address
TMaVX..