Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0SNo x1SNoLt x0 x1∀ x2 : ο . (∀ x3 . SNo x3In (SNoLev x3) (binintersect (SNoLev x0) (SNoLev x1))SNoEq_ (SNoLev x3) x3 x0SNoEq_ (SNoLev x3) x3 x1SNoLt x0 x3SNoLt x3 x1nIn (SNoLev x3) x0In (SNoLev x3) x1x2)(In (SNoLev x0) (SNoLev x1)SNoEq_ (SNoLev x0) x0 x1In (SNoLev x0) x1x2)(In (SNoLev x1) (SNoLev x0)SNoEq_ (SNoLev x1) x0 x1nIn (SNoLev x1) x0x2)x2
as obj
-
as prop
e884b..SNoLtE3
theory
HF
stx
8964b..
address
TMWZy..SNoLtE3