Search for blocks/addresses/...

Proofgold Asset

asset id
ef8d31904ffcb09e44af8ff456e12ba4ef394da2606912c6f847b37a77fa6c7f
asset hash
4ed67d8c6202e2d217d71cc5a9255c0117c443f147a5aa6d476da5d0d71c45d0
bday / block
28786
tx
ff216..
preasset
doc published by Pr4zB..
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param atleastpatleastp : ιιο
Param ordsuccordsucc : ιι
Definition u1 := 1
Definition u2 := ordsucc u1
Definition u3 := ordsucc u2
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Param binintersectbinintersect : ιιι
Param SepSep : ι(ιο) → ι
Param andand : οοο
Definition DirGraphOutNeighbors := λ x0 . λ x1 : ι → ι → ο . λ x2 . {x3 ∈ x0|and (x2 = x3∀ x4 : ο . x4) (x1 x2 x3)}
Definition nInnIn := λ x0 x1 . not (x0x1)
Param SetAdjoinSetAdjoin : ιιι
Param UPairUPair : ιιι
Known 8698a.. : ∀ x0 x1 x2 x3 . ∀ x4 : ι → ο . x4 x0x4 x1x4 x2x4 x3∀ x5 . x5SetAdjoin (SetAdjoin (UPair x0 x1) x2) x3x4 x5
Param nat_pnat_p : ιο
Known 4fb58..Pigeonhole_not_atleastp_ordsucc : ∀ x0 . nat_p x0not (atleastp (ordsucc x0) x0)
Known nat_2nat_2 : nat_p 2
Known atleastp_traatleastp_tra : ∀ x0 x1 x2 . atleastp x0 x1atleastp x1 x2atleastp x0 x2
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 Subq_atleastpSubq_atleastp : ∀ x0 x1 . x0x1atleastp x0 x1
Known aa241.. : ∀ x0 x1 x2 . ∀ x3 : ι → ο . x3 x0x3 x1x3 x2∀ x4 . x4SetAdjoin (UPair x0 x1) x2x3 x4
Known binintersectIbinintersectI : ∀ x0 x1 x2 . x2x0x2x1x2binintersect x0 x1
Known cfabd.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 x3 . x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3DirGraphOutNeighbors x0 x1 x2x2DirGraphOutNeighbors x0 x1 x3
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
Known FalseEFalseE : False∀ x0 : ο . x0
Known SepISepI : ∀ x0 . ∀ x1 : ι → ο . ∀ x2 . x2x0x1 x2x2Sep x0 x1
Known andIandI : ∀ x0 x1 : ο . x0x1and x0 x1
Theorem f0ba0.. : ∀ 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 . x3x0(x2 = x3∀ x4 : ο . x4)not (x1 x2 x3)atleastp (binintersect (DirGraphOutNeighbors x0 x1 x2) (DirGraphOutNeighbors x0 x1 x3)) u2)∀ x2 x3 x4 x5 . x2x0x3x0x4x0x5x0(∀ x6 . x6x4nIn x6 x2)(∀ x6 . x6x4nIn x6 x3)(∀ x6 . x6x4nIn x6 x5)(∀ x6 . x6x2nIn x6 x3)(∀ x6 . x6x2nIn x6 x5)(∀ x6 . x6x3nIn x6 x5)∀ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6x4x7x4x3 = SetAdjoin (SetAdjoin (UPair x10 x11) x12) x13x14x2x15x5(x6 = x7∀ x16 : ο . x16)x1 x6 x7x1 x6 x10x1 x6 x15x1 x7 x14x1 x7 x11x1 x12 x15not (x1 x14 x6)x1 x14 x15x1 x13 x15∀ x16 . x16x3not (x1 x14 x16) (proof)
Param u6 : ι
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Theorem 50435.. : ∀ 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 . x3x0(x2 = x3∀ x4 : ο . x4)not (x1 x2 x3)atleastp (binintersect (DirGraphOutNeighbors x0 x1 x2) (DirGraphOutNeighbors x0 x1 x3)) u2)∀ x2 x3 x4 x5 . x2x0x3x0x4x0x5x0(∀ x6 . x6x4nIn x6 x2)(∀ x6 . x6x4nIn x6 x3)(∀ x6 . x6x4nIn x6 x5)(∀ x6 . x6x2nIn x6 x3)(∀ x6 . x6x2nIn x6 x5)(∀ x6 . x6x3nIn x6 x5)∀ x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 . x6x4x7x4x3 = SetAdjoin (SetAdjoin (UPair x10 x11) x12) x13x14x2x15x5(x7 = x6∀ x16 : ο . x16)(x8 = x6∀ x16 : ο . x16)(x9 = x6∀ x16 : ο . x16)(x8 = x7∀ x16 : ο . x16)(x9 = x7∀ x16 : ο . x16)(x9 = x8∀ x16 : ο . x16)x1 x6 x7x1 x7 x8x1 x8 x9x1 x9 x6x1 x6 x10x1 x6 x15x1 x7 x14x1 x7 x11x1 x12 x15not (x1 x14 x6)x1 x14 x15x1 x13 x15∀ x16 . x16x3not (x1 x14 x16) (proof)