Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 : ι → ι → ο . λ x1 . inv {x2 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x2) (DirGraphOutNeighbors u18 x0 x1)) u1} (4b3fa.. x0 x1)
as obj
31e20..
as prop
-
theory
HotG
stx
ccf27..
address
TMJa8..