Search for blocks/addresses/...

Proofgold Asset

asset id
905f8e5347755002e8ae87abd19c0bb757a1577d7a43d65040828aeec80658fd
asset hash
aeea09573932cad28dbb028cdc1cf26561c33300418c28cf56d7b70991f454d2
bday / block
36788
tx
3a59c..
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 5f015.. := λ 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)x0 x1 x10not (x0 x2 x10)not (x0 x3 x10)not (x0 x4 x10)x0 x5 x10x0 x6 x10not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
Definition a4abc.. := λ 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)not (x0 x7 x9)x0 x8 x9x10)x10
Definition b019a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (a4abc.. 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)x0 x1 x10not (x0 x2 x10)x0 x3 x10not (x0 x4 x10)not (x0 x5 x10)x0 x6 x10not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
Definition 04c7a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (b019a.. 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 x11x0 x2 x11x0 x3 x11x0 x4 x11not (x0 x5 x11)not (x0 x6 x11)not (x0 x7 x11)not (x0 x8 x11)not (x0 x9 x11)not (x0 x10 x11)x12)x12
Definition 25ef3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (5f015.. 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 x11x0 x2 x11x0 x3 x11x0 x4 x11not (x0 x5 x11)not (x0 x6 x11)not (x0 x7 x11)not (x0 x8 x11)not (x0 x9 x11)not (x0 x10 x11)x12)x12
Definition f8709.. := λ 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 x6x0 x3 x6x0 x4 x6not (x0 x5 x6)x7)x7
Definition 27260.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f8709.. 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 x7x0 x2 x7not (x0 x3 x7)not (x0 x4 x7)x0 x5 x7not (x0 x6 x7)x8)x8
Definition dfcf9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (27260.. 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)x0 x2 x8not (x0 x3 x8)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 1668d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (dfcf9.. 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)x0 x1 x9not (x0 x2 x9)not (x0 x3 x9)not (x0 x4 x9)x0 x5 x9x0 x6 x9not (x0 x7 x9)x0 x8 x9x10)x10
Definition 87bb9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (1668d.. 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)x0 x1 x10not (x0 x2 x10)x0 x3 x10x0 x4 x10not (x0 x5 x10)not (x0 x6 x10)not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
Definition fd9fb.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (87bb9.. 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)not (x0 x1 x11)not (x0 x2 x11)not (x0 x3 x11)x0 x4 x11not (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)
Known 3b7d8.. : ∀ 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 . x13x05f015.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . (x2 x4 x3x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)not (x2 x11 x3)not (x2 x12 x3)not (x2 x13 x3)x14)(x2 x4 x3x2 x5 x3not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)not (x2 x11 x3)not (x2 x12 x3)not (x2 x13 x3)x14)(x2 x4 x3x2 x5 x3x2 x6 x3x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)not (x2 x11 x3)not (x2 x12 x3)not (x2 x13 x3)x14)(not (x2 x4 x3)x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)not (x2 x13 x3)x14)(x2 x4 x3x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)not (x2 x13 x3)x14)x14
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known 21da7.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x05f015.. x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x115f015.. x1 x4 x3 x2 x9 x11 x10 x8 x5 x7 x6
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known SingISingI : ∀ x0 . x0Sing x0
Theorem 40e52.. : ∀ 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 . x13x05f015.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . (∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x004c7a.. x2 x15 x16 x17 x18 x19 x20 x21 x22 x3 x23 x24x14)(∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x025ef3.. x2 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x3x14)(∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x0fd9fb.. x2 x15 x16 x17 x18 x19 x20 x3 x21 x22 x23 x24x14)x14 (proof)