Search for blocks/addresses/...

Proofgold Asset

asset id
43b769ae92936812c8f0b71c4a34ef046c29b8b93546176fd791252472f2f508
asset hash
85b40a49e8e1ebe8cbb7ad57c7cd39aaa488422122874fd577960f8cd602c7d0
bday / block
36137
tx
7cd3d..
preasset
doc published by Pr4zB..
Param 4402e.. : ι(ιιο) → ο
Param cf2df.. : ι(ιιο) → ο
Definition SubqSubq := λ x0 x1 . ∀ x2 . x2x0x2x1
Param setminussetminus : ιιι
Param SingSing : ιι
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Definition 8b6ad.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 . ∀ x5 : ο . ((x1 = x2∀ x6 : ο . x6)(x1 = x3∀ x6 : ο . x6)(x2 = x3∀ x6 : ο . x6)(x1 = x4∀ x6 : ο . x6)(x2 = x4∀ x6 : ο . x6)(x3 = x4∀ x6 : ο . x6)not (x0 x1 x2)not (x0 x1 x3)not (x0 x2 x3)not (x0 x1 x4)not (x0 x2 x4)not (x0 x3 x4)x5)x5
Definition c5756.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (8b6ad.. x0 x1 x2 x3 x4(x1 = x5∀ x7 : ο . x7)(x2 = x5∀ x7 : ο . x7)(x3 = x5∀ x7 : ο . x7)(x4 = x5∀ x7 : ο . x7)not (x0 x1 x5)not (x0 x2 x5)x0 x3 x5x0 x4 x5x6)x6
Definition 2de86.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (c5756.. x0 x1 x2 x3 x4 x5(x1 = x6∀ x8 : ο . x8)(x2 = x6∀ x8 : ο . x8)(x3 = x6∀ x8 : ο . x8)(x4 = x6∀ x8 : ο . x8)(x5 = x6∀ x8 : ο . x8)not (x0 x1 x6)x0 x2 x6not (x0 x3 x6)x0 x4 x6not (x0 x5 x6)x7)x7
Definition 21422.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (2de86.. x0 x1 x2 x3 x4 x5 x6(x1 = x7∀ x9 : ο . x9)(x2 = x7∀ x9 : ο . x9)(x3 = x7∀ x9 : ο . x9)(x4 = x7∀ x9 : ο . x9)(x5 = x7∀ x9 : ο . x9)(x6 = x7∀ x9 : ο . x9)x0 x1 x7not (x0 x2 x7)x0 x3 x7not (x0 x4 x7)not (x0 x5 x7)x0 x6 x7x8)x8
Definition f0d5b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (21422.. x0 x1 x2 x3 x4 x5 x6 x7(x1 = x8∀ x10 : ο . x10)(x2 = x8∀ x10 : ο . x10)(x3 = x8∀ x10 : ο . x10)(x4 = x8∀ x10 : ο . x10)(x5 = x8∀ x10 : ο . x10)(x6 = x8∀ x10 : ο . x10)(x7 = x8∀ x10 : ο . x10)not (x0 x1 x8)not (x0 x2 x8)not (x0 x3 x8)x0 x4 x8not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 8f55d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (f0d5b.. x0 x1 x2 x3 x4 x5 x6 x7 x8(x1 = x9∀ x11 : ο . x11)(x2 = x9∀ x11 : ο . x11)(x3 = x9∀ x11 : ο . x11)(x4 = x9∀ x11 : ο . x11)(x5 = x9∀ x11 : ο . x11)(x6 = x9∀ x11 : ο . x11)(x7 = x9∀ x11 : ο . x11)(x8 = x9∀ x11 : ο . x11)not (x0 x1 x9)x0 x2 x9not (x0 x3 x9)not (x0 x4 x9)x0 x5 x9not (x0 x6 x9)x0 x7 x9x0 x8 x9x10)x10
Definition e68b8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (8f55d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9(x1 = x10∀ x12 : ο . x12)(x2 = x10∀ x12 : ο . x12)(x3 = x10∀ x12 : ο . x12)(x4 = x10∀ x12 : ο . x12)(x5 = x10∀ x12 : ο . x12)(x6 = x10∀ x12 : ο . x12)(x7 = x10∀ x12 : ο . x12)(x8 = x10∀ x12 : ο . x12)(x9 = x10∀ x12 : ο . x12)not (x0 x1 x10)x0 x2 x10x0 x3 x10not (x0 x4 x10)not (x0 x5 x10)not (x0 x6 x10)not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
Definition 36e27.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (e68b8.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10(x1 = x11∀ x13 : ο . x13)(x2 = x11∀ x13 : ο . x13)(x3 = x11∀ x13 : ο . x13)(x4 = x11∀ x13 : ο . x13)(x5 = x11∀ x13 : ο . x13)(x6 = x11∀ x13 : ο . x13)(x7 = x11∀ x13 : ο . x13)(x8 = x11∀ x13 : ο . x13)(x9 = x11∀ x13 : ο . x13)(x10 = x11∀ x13 : ο . x13)x0 x1 x11not (x0 x2 x11)not (x0 x3 x11)not (x0 x4 x11)not (x0 x5 x11)not (x0 x6 x11)not (x0 x7 x11)x0 x8 x11not (x0 x9 x11)not (x0 x10 x11)x12)x12
Definition andand := λ x0 x1 : ο . ∀ x2 : ο . (x0x1x2)x2
Definition nInnIn := λ x0 x1 . not (x0x1)
Known setminusEsetminusE : ∀ x0 x1 x2 . x2setminus x0 x1and (x2x0) (nIn x2 x1)
Definition oror := λ x0 x1 : ο . ∀ x2 : ο . (x0x2)(x1x2)x2
Known xmxm : ∀ x0 : ο . or x0 (not x0)
Known FalseEFalseE : False∀ x0 : ο . x0
Known 53a3c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0not (x1 x2 x3)not (x1 x3 x2))cf2df.. x0 x1∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0(x2 = x3∀ x7 : ο . x7)(x2 = x4∀ x7 : ο . x7)(x3 = x4∀ x7 : ο . x7)(x2 = x5∀ x7 : ο . x7)(x3 = x5∀ x7 : ο . x7)(x4 = x5∀ x7 : ο . x7)(x2 = x6∀ x7 : ο . x7)(x3 = x6∀ x7 : ο . x7)(x4 = x6∀ x7 : ο . x7)(x5 = x6∀ x7 : ο . x7)not (x1 x2 x3)not (x1 x2 x4)not (x1 x3 x4)not (x1 x2 x5)not (x1 x3 x5)not (x1 x4 x5)not (x1 x2 x6)not (x1 x3 x6)not (x1 x4 x6)not (x1 x5 x6)False
Known 61345.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)4402e.. x0 x1∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0(x2 = x3∀ x5 : ο . x5)(x2 = x4∀ x5 : ο . x5)(x3 = x4∀ x5 : ο . x5)x1 x2 x3x1 x2 x4x1 x3 x4False
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known SingISingI : ∀ x0 . x0Sing x0
Theorem 7fef1.. : ∀ x0 x1 . ∀ x2 : ι → ι → ο . (∀ x3 . x3x1∀ x4 . x4x1x2 x3 x4x2 x4 x3)4402e.. x1 x2cf2df.. x1 x2∀ x3 . x3x1x0setminus x1 (Sing x3)∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x036e27.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14∀ x15 : ο . x15 (proof)