Search for blocks/addresses/...

Proofgold Address

address
PUKy4d9ecfet3uPHv9YnB5tS9CaCC94R9yt
total
0
mg
-
conjpub
-
current assets
99c60../96805.. bday: 36570 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 9ab39.. := λ 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)not (x0 x1 x6)x0 x2 x6x0 x3 x6x0 x4 x6not (x0 x5 x6)x7)x7
Definition 468d8.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (9ab39.. 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 x7x0 x4 x7not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition 3b6e0.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (468d8.. 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 d0e1f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (3b6e0.. 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 x9x0 x2 x9not (x0 x3 x9)not (x0 x4 x9)not (x0 x5 x9)not (x0 x6 x9)not (x0 x7 x9)x0 x8 x9x10)x10
Definition df50d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (3b6e0.. 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)x0 x3 x9not (x0 x4 x9)not (x0 x5 x9)not (x0 x6 x9)not (x0 x7 x9)x0 x8 x9x10)x10
Definition 95ba7.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (3b6e0.. 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 x9x0 x2 x9x0 x3 x9not (x0 x4 x9)not (x0 x5 x9)not (x0 x6 x9)not (x0 x7 x9)x0 x8 x9x10)x10
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 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 182cc.. := λ 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)not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition 0b76b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (182cc.. 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 x8not (x0 x2 x8)not (x0 x3 x8)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 23b40.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (0b76b.. 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 x9x0 x3 x9x0 x4 x9not (x0 x5 x9)not (x0 x6 x9)not (x0 x7 x9)x0 x8 x9x10)x10
Definition c705c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (3b6e0.. 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)not (x0 x5 x9)x0 x6 x9not (x0 x7 x9)x0 x8 x9x10)x10
Definition 6e051.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (3b6e0.. 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 62523.. := λ 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)not (x0 x3 x5)x0 x4 x5x6)x6
Definition fba9e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (62523.. 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 x6not (x0 x4 x6)not (x0 x5 x6)x7)x7
Definition 948b9.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (fba9e.. x0 x1 x3 x4 x2 x6 x5(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 x7x0 x4 x7not (x0 x5 x7)x0 x6 x7x8)x8
Definition 0881d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (948b9.. 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 x8not (x0 x2 x8)not (x0 x3 x8)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition dd43e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (0881d.. 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 x9x0 x4 x9not (x0 x5 x9)x0 x6 x9not (x0 x7 x9)x0 x8 x9x10)x10
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 76a6c.. := λ 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)not (x0 x1 x9)not (x0 x2 x9)x0 x3 x9x0 x4 x9not (x0 x5 x9)not (x0 x6 x9)x0 x7 x9x0 x8 x9x10)x10
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 36d58.. := λ 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 x7x0 x4 x7not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition d2827.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (36d58.. 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)x0 x3 x8not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 14be0.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (d2827.. 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 796c4.. := λ 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)not (x0 x6 x7)x8)x8
Definition 79f22.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (796c4.. 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)x0 x3 x8x0 x4 x8not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 076b3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (79f22.. 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 7f522.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (9ab39.. 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)not (x0 x3 x7)not (x0 x4 x7)not (x0 x5 x7)x0 x6 x7x8)x8
Definition 24054.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (7f522.. 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 49901.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (24054.. 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 x9x0 x3 x9not (x0 x4 x9)not (x0 x5 x9)not (x0 x6 x9)x0 x7 x9x0 x8 x9x10)x10
Definition 1c500.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (9ab39.. 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)not (x0 x3 x7)not (x0 x4 x7)x0 x5 x7x0 x6 x7x8)x8
Definition 25f2f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (1c500.. 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 e5063.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (25f2f.. 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)x0 x7 x9x0 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 68225.. : ∀ 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 . x11x03b6e0.. 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)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)not (x2 x11 x3)x12)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3x2 x9 x3not (x2 x10 x3)not (x2 x11 x3)x12)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(x2 x4 x3x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(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)(x2 x4 x3not (x2 x5 x3)x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(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 x3x12)(x2 x4 x3x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x2 x11 x3x12)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3x2 x9 x3not (x2 x10 x3)x2 x11 x3x12)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3x2 x11 x3x12)x12
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known 2f2c4.. : ∀ 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 . x9x03b6e0.. x1 x2 x3 x4 x5 x6 x7 x8 x93b6e0.. x1 x2 x3 x4 x5 x7 x6 x8 x9
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known SingISingI : ∀ x0 . x0Sing x0
Theorem 5a3dc.. : ∀ 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 . x11x03b6e0.. 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 . x20x0d0e1f.. x2 x13 x14 x15 x16 x17 x18 x19 x20 x3x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0df50d.. x2 x13 x14 x15 x16 x17 x18 x19 x20 x3x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x095ba7.. x2 x13 x14 x15 x16 x17 x18 x19 x20 x3x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x023b40.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0c705c.. x2 x13 x14 x15 x16 x17 x18 x19 x20 x3x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x06e051.. x2 x13 x14 x15 x16 x17 x18 x19 x20 x3x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0dd43e.. x2 x3 x13 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x076a6c.. x2 x13 x3 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x014be0.. x2 x13 x3 x14 x15 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0076b3.. x2 x13 x14 x15 x16 x17 x3 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x049901.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)(∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0e5063.. x2 x13 x14 x15 x3 x16 x17 x18 x19 x20x12)x12 (proof)

previous assets