Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 x3 . x2x0∀ x4 . nat_p x4(∀ x5 . x5x0(x5 = x2∀ x6 : ο . x6)not (x1 x5 x2)or (equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) x4) (equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) (ordsucc x4)))(∀ x5 . x5{x6 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))|equip (binintersect (DirGraphOutNeighbors x0 x1 x6) (DirGraphOutNeighbors x0 x1 x2)) x4}not (x1 x3 x5))(∀ x5 . x5setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)not (x1 x2 x5))∀ x5 . x5setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)equip (binintersect (DirGraphOutNeighbors x0 x1 x5) (DirGraphOutNeighbors x0 x1 x2)) (ordsucc x4)
as obj
-
as prop
94e32..
theory
HotG
stx
1810e..
address
TMGR6..