Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)(∀ x2 . x2x0atleastp u3 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)x1 x3 x4))(∀ x2 . x2x0atleastp u6 x2not (∀ x3 . x3x2∀ x4 . x4x2(x3 = x4∀ x5 : ο . x5)not (x1 x3 x4)))∀ x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . x9x0x11x0x8 = setminus (DirGraphOutNeighbors x0 x1 x4) (Sing x5)x10 = setminus (DirGraphOutNeighbors x0 x1 x5) (Sing x4)x9 = {x13 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x13) (DirGraphOutNeighbors x0 x1 x4)) x2}x11 = setminus {x13 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x13) (DirGraphOutNeighbors x0 x1 x4)) x3} x10(∀ x12 . x12x9nIn x12 x8)(∀ x12 . x12x9nIn x12 x11)(∀ x12 . x12x8nIn x12 x11)x6x9x7x11x1 x6 x7∀ x12 x13 : ι → ι . x1 x6 (x12 x6)(∀ x14 . x14x8x13 x14{x15 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x4) (Sing x4))|equip (binintersect (DirGraphOutNeighbors x0 x1 x15) (DirGraphOutNeighbors x0 x1 x4)) x2})(∀ x14 . x14x8x12 (x13 x14) = x14)atleastp x3 {x14 ∈ setminus x9 (Sing x6)|x1 (x12 x14) x7}
type
prop
theory
HotG
name
-
proof
PUesR..
Megalodon
-
proofgold address
TMYWE..
creator
28305 Pr4zB../fb2ac..
owner
28307 Pr4zB../dacf6..
term root
afd8b..