Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . In x0 0∀ x1 . In x1 x0∀ x2 . In x2 x1∃ x3 . ∀ x5 . (ordinal x3and (exactly2 x3) (not (exactly5 x5)))((ordinal x3exactly2 x3)atleast2 x3((not (atleast2 (Power (binrep (Power (Power 0)) 0)))x3 = x5)atleast3 x3)and (atleast5 x2) (not (exactly1of2 (SNoLt x2 (binrep (Power (Power (Power (Power 0)))) 0)) (TransSet x5))))nat_p x3
as obj
-
as prop
e9a29..
theory
HF
stx
350fd..
address
TMNa8..