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 . nat_p x4∀ x5 x6 x7 . x5x0x6x0x7x0x5 = setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)(∀ x8 . x8x6nIn x8 x5)(∀ x8 . x8x6nIn x8 x7)(∀ x8 . x8x5nIn x8 x7)(∀ x8 . x8x7x8{x9 ∈ setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x3) (Sing x3))|equip (binintersect (DirGraphOutNeighbors x0 x1 x9) (DirGraphOutNeighbors x0 x1 x3)) x4})∀ x8 x9 . x8x6x9x7x9setminus x0 (binunion (DirGraphOutNeighbors x0 x1 x2) (Sing x2))x1 x8 x9∀ x10 : ι → ι . (∀ x11 . x11x6x10 x11x5)(∀ x11 . x11x6x1 x11 (x10 x11))(∀ x11 . x11x5∀ x12 : ο . (∀ x13 . and (x13x6) (x10 x13 = x11)x12)x12)atleastp x4 {x11 ∈ setminus x6 (Sing x8)|x1 (x10 x11) x9}
type
prop
theory
HotG
name
-
proof
PUNHu..
Megalodon
-
proofgold address
TMcGs..
creator
30188 Pr4zB../bfda4..
owner
30194 Pr4zB../2116b..
term root
a7807..