Search for blocks/addresses/...

Proofgold Asset

asset id
ec81a83b641d95388f68a8aa94efcc174e795ac61f750dafc746ef7a82368775
asset hash
474e9aece45692532966ac95f62e9c9b49d2c1acd9b79e135955e7b80527ecb8
bday / block
29486
tx
229d5..
preasset
doc published by Pr4zB..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param atleastpatleastp : ιιο
Param u3 : ι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param SepSep : ι(ιο) → ι
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3∀ x4 : ο . x4) (x1 x2 x3)}
Param setminussetminus : ιιι
Param SingSing : ιι
Definition nInnIn := λ x0 x1 . not (x0x1)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Known SepESepE : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1and (x2x0) (x1 x2)
Param SetAdjoinSetAdjoin : ιιι
Param UPairUPair : ιιι
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0x3 x1x3 x2∀ x4 . x4SetAdjoin (UPair x0 x1) x2x3 x4
Known SepE1SepE1 : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2Sep x0 x1x2x0
Known 5d098.. : ∀ x0 x1 . x1x0∀ x2 . x2x0∀ x3 . x3x0(x1 = x2∀ x4 : ο . x4)(x1 = x3∀ x4 : ο . x4)(x2 = x3∀ x4 : ο . x4)atleastp u3 x0
Known 6be8c.. : ∀ x0 x1 x2 . x0SetAdjoin (UPair x0 x1) x2
Known 535ce.. : ∀ x0 x1 x2 . x1SetAdjoin (UPair x0 x1) x2
Known f4e2f.. : ∀ x0 x1 x2 . x2SetAdjoin (UPair x0 x1) x2
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known SingISingI : ∀ x0 . x0Sing x0
Known FalseEFalseE : False∀ x0 : ο . x0
Theorem c82b0.. : ∀ 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 x3 . x2x0x3DirGraphOutNeighbors x0 x1 x2(x2 = x3∀ x4 : ο . x4)x1 x2 x3∀ x4 . x4setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)not (x1 x2 x4) (proof)
Param u6 : ι
Theorem 29078.. : ∀ 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 . x2x0x3DirGraphOutNeighbors x0 x1 x2(x2 = x3∀ x4 : ο . x4)x1 x2 x3∀ x4 . x4setminus (DirGraphOutNeighbors x0 x1 x3) (Sing x2)not (x1 x2 x4) (proof)