Search for blocks/addresses/...

Proofgold Asset

asset id
06d50790ddc7aefcd7ce013b268ea08a4335dbd6c8bd205d5043fa4fbc74af03
asset hash
3646f63ac51ab07c57ceea7ffb66323b8a582afe1f0b871f755de3d6ef287cfa
bday / block
34754
tx
ee957..
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 4ea7e.. := λ 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)not (x0 x2 x6)x0 x3 x6x0 x4 x6not (x0 x5 x6)x7)x7
Definition 5db61.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 . ∀ x8 : ο . (4ea7e.. 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 5cb4b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (5db61.. 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 cec27.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (5cb4b.. 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 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 a905b.. : ∀ 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 . x12x0cec27.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12∀ x13 : ο . (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 x3not (x2 x12 x3)x13)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)x13)(x2 x4 x3not (x2 x5 x3)x2 x6 x3x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)x13)x13 (proof)