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 . x2x0x3x0x4x0x5x0(∀ x6 . x6x2nIn x6 x5)(∀ x6 . x6x2nIn x6 x3)(∀ x6 . x6x4nIn x6 x2)(∀ x6 . x6x4nIn x6 x3)(∀ x6 . x6x4nIn x6 x5)(∀ x6 . x6x3nIn x6 x5)∀ x6 x7 x8 x9 x10 . x4 = SetAdjoin (SetAdjoin (UPair x6 x7) x8) x9x10x5(x7 = x6∀ x11 : ο . x11)(x8 = x6∀ x11 : ο . x11)(x9 = x6∀ x11 : ο . x11)(x8 = x7∀ x11 : ο . x11)(x9 = x7∀ x11 : ο . x11)(x9 = x8∀ x11 : ο . x11)x1 x6 x7x1 x7 x8x1 x8 x9x1 x9 x6(∀ x11 . x11x4(x11 = x10∀ x12 : ο . x12)not (x1 x11 x10)atleastp (binintersect (DirGraphOutNeighbors x0 x1 x11) (DirGraphOutNeighbors x0 x1 x10)) u2)x6binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x10)x6binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x10)not (x1 x7 x10)not (x1 x9 x10)∀ x11 x12 : ι → ι . (∀ x13 . x13x4x11 x13x2)(∀ x13 . x13x4x11 x13DirGraphOutNeighbors x0 x1 x13)(∀ x13 . x13x4x12 x13x3)(∀ x13 . x13x4x12 x13DirGraphOutNeighbors x0 x1 x13)∀ x13 . x13x4x13{x14 ∈ setminus x4 (Sing x6)|x1 (x11 x14) x10}x13{x14 ∈ setminus x4 (Sing x6)|x1 (x12 x14) x10}x13 = x8
type
prop
theory
HotG
name
-
proof
PURdm..
Megalodon
-
proofgold address
TMdzq..
creator
29938 Pr4zB../3f859..
owner
29941 Pr4zB../c6079..
term root
3fef0..