Search for blocks/addresses/...

Proofgold Asset

asset id
a0a54690799799387c7512a6ef5316edcc4d0f5125f162fccfd8ca5a37383623
asset hash
7c96e5a3206d2617393f08405f206ca4b3dc1f6c1e83eba93b42fba66b2934a1
bday / block
23121
tx
f7c28..
preasset
doc published by Pr4zB..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param atleastpatleastp : ιιο
Param u3 : ι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param SetAdjoinSetAdjoin : ιιι
Param UPairUPair : ιιι
Param binintersectbinintersect : ιιι
Param SepSep : ι(ιο) → ι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3∀ x4 : ο . x4) (x1 x2 x3)}
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0x4 x1x4 x2x4 x3∀ x5 . x5SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3x4 x5
Known FalseEFalseE : False∀ x0 : ο . x0
Known binintersectEbinintersectE : ∀ x0 x1 x2 . x2binintersect x0 x1and (x2x0) (x2x1)
Known 7fc90.. : ∀ 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 . x2x0∀ x3 . x3DirGraphOutNeighbors x0 x1 x2∀ x4 . x4DirGraphOutNeighbors x0 x1 x2(x3 = x4∀ x5 : ο . x5)not (x1 x3 x4)
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known cfabd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3DirGraphOutNeighbors x0 x1 x2x2DirGraphOutNeighbors x0 x1 x3
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Known binintersect_combinintersect_com : ∀ x0 x1 . binintersect x0 x1 = binintersect x1 x0
Known b253c.. : ∀ x0 x1 x2 x3 . x3SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known 14338.. : ∀ x0 x1 x2 x3 . x2SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known e588e.. : ∀ x0 x1 x2 x3 . x1SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Known 69a9c.. : ∀ x0 x1 x2 x3 . x0SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3
Theorem 782e4.. : ∀ 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 . x2x0∀ x3 x4 x5 x6 . x2 = SetAdjoin (SetAdjoin (UPair x3 x4) x5) x6(x4 = x3∀ x7 : ο . x7)(x5 = x3∀ x7 : ο . x7)(x6 = x3∀ x7 : ο . x7)(x5 = x4∀ x7 : ο . x7)(x6 = x4∀ x7 : ο . x7)(x6 = x5∀ x7 : ο . x7)x1 x3 x4x1 x4 x5x1 x5 x6x1 x6 x3(∀ x7 . x7binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x5)or (x7 = x4) (x7 = x6))(∀ x7 . x7binintersect (DirGraphOutNeighbors x0 x1 x4) (DirGraphOutNeighbors x0 x1 x6)or (x7 = x3) (x7 = x5))∀ x7 . x7x2∀ x8 . x8x2(x7 = x8∀ x9 : ο . x9)∀ x9 . x9binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x8)x9x2 (proof)
Param u6 : ι
Theorem 49b78.. : ∀ 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 . x2x0∀ x3 x4 x5 x6 . x2 = SetAdjoin (SetAdjoin (UPair x3 x4) x5) x6(x4 = x3∀ x7 : ο . x7)(x5 = x3∀ x7 : ο . x7)(x6 = x3∀ x7 : ο . x7)(x5 = x4∀ x7 : ο . x7)(x6 = x4∀ x7 : ο . x7)(x6 = x5∀ x7 : ο . x7)x1 x3 x4x1 x4 x5x1 x5 x6x1 x6 x3(∀ x7 . x7binintersect (DirGraphOutNeighbors x0 x1 x3) (DirGraphOutNeighbors x0 x1 x5)or (x7 = x4) (x7 = x6))(∀ x7 . x7binintersect (DirGraphOutNeighbors x0 x1 x4) (DirGraphOutNeighbors x0 x1 x6)or (x7 = x3) (x7 = x5))∀ x7 . x7x2∀ x8 . x8x2(x7 = x8∀ x9 : ο . x9)∀ x9 . x9binintersect (DirGraphOutNeighbors x0 x1 x7) (DirGraphOutNeighbors x0 x1 x8)x9x2 (proof)