Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ι → ι → ο . (∀ x1 x2 . x0 x1 x2x0 x2 x1)(∀ x1 . x1u18atleastp u3 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)x0 x2 x3))(∀ x1 . x1u18atleastp u6 x1not (∀ x2 . x2x1∀ x3 . x3x1(x2 = x3∀ x4 : ο . x4)not (x0 x2 x3)))∀ x1 . x1u18∀ x2 : ο . (∀ x3 . x3DirGraphOutNeighbors u18 x0 x1∀ x4 . x4u18∀ x5 . x5u18∀ x6 . x6u18∀ x7 . x7u18x4 = setminus (DirGraphOutNeighbors u18 x0 x1) (Sing x3)x6 = setminus (DirGraphOutNeighbors u18 x0 x3) (Sing x1)x5 = {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u1}x7 = setminus {x9 ∈ setminus u18 (binunion (DirGraphOutNeighbors u18 x0 x1) (Sing x1))|equip (binintersect (DirGraphOutNeighbors u18 x0 x9) (DirGraphOutNeighbors u18 x0 x1)) u2} x6(∀ x8 . x8u18∀ x9 : ο . (x8 = x1x9)(x8 = x3x9)(x8x4x9)(x8x6x9)(x8x5x9)(x8x7x9)x9)(∀ x8 . x8x5not (x0 x3 x8))equip x4 u4equip x5 u4equip x6 u4equip x7 u4(∀ x8 . x8x6nIn x8 x7)(∀ x8 . x8x5∀ x9 : ο . (∀ x10 . and (x10x6) (x0 x8 x10)x9)x9)(∀ x8 . x8x6not (x0 x1 x8))(∀ x8 . x8x6equip (binintersect (DirGraphOutNeighbors u18 x0 x8) (DirGraphOutNeighbors u18 x0 x1)) u2)f1360.. x0 u3 x5x2)x2
type
prop
theory
HotG
name
-
proof
PUcra..
Megalodon
-
proofgold address
TMWnA..
creator
31062 Pr4zB../91983..
owner
31062 Pr4zB../91983..
term root
31a48..