Search for blocks/addresses/...

Proofgold Address

address
PUaMpnejimxjmLhzPFxVJ239RuhTkKdDQzL
total
0
mg
-
conjpub
-
current assets
561f7../b695c.. bday: 35482 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 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 a542b.. := λ 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)not (x0 x2 x6)x0 x3 x6not (x0 x4 x6)x0 x5 x6x7)x7
Definition 1d4b1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (a542b.. 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 2f869.. := λ 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)x0 x3 x4x5)x5
Definition 87c36.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. 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 x5not (x0 x3 x5)x0 x4 x5x6)x6
Definition f201d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. 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 x6not (x0 x4 x6)x0 x5 x6x7)x7
Definition 81638.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f201d.. 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 14240.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (81638.. 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)not (x0 x4 x8)not (x0 x5 x8)x0 x6 x8not (x0 x7 x8)x9)x9
Definition 110e1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (81638.. 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)x0 x6 x8not (x0 x7 x8)x9)x9
Definition 6648a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. 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 df271.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. 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 7b2a6.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (df271.. 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)not (x0 x4 x8)not (x0 x5 x8)x0 x6 x8not (x0 x7 x8)x9)x9
Definition db744.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (df271.. 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)x0 x6 x8not (x0 x7 x8)x9)x9
Definition f6f09.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (87c36.. 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 x6x0 x2 x6x0 x3 x6not (x0 x4 x6)not (x0 x5 x6)x7)x7
Definition 88b7c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f6f09.. 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 x7not (x0 x4 x7)not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition b33d3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (88b7c.. 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)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)x0 x7 x8x9)x9
Definition 5a3b5.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 . ∀ x6 : ο . (2f869.. 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 x5not (x0 x3 x5)not (x0 x4 x5)x6)x6
Definition 455db.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 . ∀ x7 : ο . (5a3b5.. 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)not (x0 x3 x6)x0 x4 x6x0 x5 x6x7)x7
Definition 70d65.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (455db.. 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 x7not (x0 x4 x7)not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition 478f3.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (70d65.. 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)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)x0 x7 x8x9)x9
Definition 2452c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (f201d.. 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)x0 x4 x7not (x0 x5 x7)not (x0 x6 x7)x8)x8
Definition cb643.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (2452c.. 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)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)x0 x7 x8x9)x9
Definition 86c47.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (70d65.. 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)not (x0 x4 x8)x0 x5 x8not (x0 x6 x8)x0 x7 x8x9)x9
Definition 737dc.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (2452c.. 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)not (x0 x4 x8)x0 x5 x8not (x0 x6 x8)x0 x7 x8x9)x9
Definition 836ee.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (6648a.. 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 8df3f.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (836ee.. 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)not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)x0 x7 x8x9)x9
Definition bc747.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (88b7c.. 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)not (x0 x4 x8)not (x0 x5 x8)x0 x6 x8x0 x7 x8x9)x9
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 f9a36.. : ∀ 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 . x10x01d4b1.. x2 x4 x5 x6 x7 x8 x9 x10∀ x11 : ο . (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)x11)(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)x11)(x2 x4 x3x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3x2 x6 x3not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(not (x2 x4 x3)not (x2 x5 x3)x2 x6 x3x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)x2 x6 x3x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3x2 x6 x3x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3x2 x6 x3x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)x2 x6 x3not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3x2 x6 x3not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3x2 x6 x3not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x11)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x11)(not (x2 x4 x3)x2 x5 x3not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x11)(x2 x4 x3x2 x5 x3not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x11)x11
Known neq_i_symneq_i_sym : ∀ x0 x1 . (x0 = x1∀ x2 : ο . x2)x1 = x0∀ x2 : ο . x2
Known Subq_traSubq_tra : ∀ x0 x1 x2 . x0x1x1x2x0x2
Known setminus_Subqsetminus_Subq : ∀ x0 x1 . setminus x0 x1x0
Known SingISingI : ∀ x0 . x0Sing x0
Theorem f21e7.. : ∀ 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 . x10x01d4b1.. x2 x4 x5 x6 x7 x8 x9 x10∀ x11 : ο . (∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x014240.. x2 x12 x13 x14 x3 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0110e1.. x2 x12 x13 x14 x3 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x07b2a6.. x2 x3 x12 x13 x14 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0db744.. x2 x3 x12 x13 x14 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0b33d3.. x2 x12 x13 x14 x15 x16 x3 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0478f3.. x2 x12 x13 x14 x15 x3 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0cb643.. x2 x12 x13 x14 x15 x3 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x086c47.. x2 x12 x13 x14 x15 x3 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0737dc.. x2 x12 x13 x14 x15 x3 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x08df3f.. x2 x12 x3 x13 x14 x15 x16 x17 x18x11)(∀ x12 . x12x0∀ x13 . x13x0∀ x14 . x14x0∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0bc747.. x2 x12 x13 x14 x15 x16 x17 x3 x18x11)x11 (proof)

previous assets