Search for blocks/addresses/...

Proofgold Address

address
PUVe4x2jrTxFpLESUu1bvopZVvKuQu9zDBh
total
0
mg
-
conjpub
-
current assets
ca07c../a715d.. bday: 35824 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 2b028.. := λ 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)x0 x2 x5x0 x3 x5x0 x4 x5x6)x6
Definition 170ba.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (2b028.. 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)x0 x1 x6not (x0 x2 x6)x0 x3 x6x0 x4 x6not (x0 x5 x6)x7)x7
Definition 58615.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (170ba.. 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 x7x0 x3 x7x0 x4 x7not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition 6a4fb.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (58615.. 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)x0 x1 x8x0 x2 x8not (x0 x3 x8)x0 x4 x8not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 5d8ad.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (6a4fb.. 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)not (x0 x2 x9)x0 x3 x9not (x0 x4 x9)not (x0 x5 x9)not (x0 x6 x9)not (x0 x7 x9)x0 x8 x9x10)x10
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 62e88.. : ∀ 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 . x11x06a4fb.. x2 x4 x5 x6 x7 x8 x9 x10 x11∀ x12 : ο . (x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)not (x2 x11 x3)x12)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)x12
Known c3f08.. : ∀ 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 . x9x06a4fb.. x1 x2 x3 x4 x5 x6 x7 x8 x96a4fb.. x1 x3 x4 x2 x5 x7 x9 x8 x6
Known 41356.. : ∀ 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 . x9x06a4fb.. x1 x2 x3 x4 x5 x6 x7 x8 x96a4fb.. x1 x2 x4 x3 x5 x6 x9 x8 x7
Known 1e6be.. : ∀ 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 . x9x06a4fb.. x1 x2 x3 x4 x5 x6 x7 x8 x96a4fb.. x1 x9 x7 x6 x8 x4 x3 x5 x2
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known SingISingI : ∀ x0 . x0Sing x0
Theorem db804.. : ∀ 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 . x11x06a4fb.. x2 x4 x5 x6 x7 x8 x9 x10 x11∀ x12 : ο . (∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x05d8ad.. x2 x13 x14 x15 x16 x17 x18 x19 x20 x3x12)x12 (proof)

previous assets