Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr7sm../cdd53..
PUgzR../e3a80..
vout
Pr7sm../bc00e.. 5.97 bars
TMd76../1582c.. ownership of 6a63e.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMPuj../22942.. ownership of f04d8.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUeXr../27f6e.. 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 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 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 b4c8a.. := λ 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)x0 x2 x8x0 x3 x8not (x0 x4 x8)not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)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)
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 6a63e.. : ∀ 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 . x11x0b4c8a.. x2 x4 x5 x6 x7 x8 x9 x10 x11∀ x12 : ο . (not (x2 x4 x3)not (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)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3x2 x9 x3not (x2 x10 x3)not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)x2 x10 x3not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3x2 x10 x3not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3x2 x10 x3not (x2 x11 x3)x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3x2 x9 x3x2 x10 x3not (x2 x11 x3)x12)(not (x2 x4 x3)not (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)(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)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(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 x3x12)(not (x2 x4 x3)not (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)x2 x8 x3not (x2 x9 x3)not (x2 x10 x3)x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3not (x2 x10 x3)x2 x11 x3x12)(not (x2 x4 x3)not (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)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)not (x2 x9 x3)x2 x10 x3x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3not (x2 x9 x3)x2 x10 x3x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)not (x2 x8 x3)x2 x9 x3x2 x10 x3x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)x2 x7 x3not (x2 x8 x3)x2 x9 x3x2 x10 x3x2 x11 x3x12)(not (x2 x4 x3)not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3x2 x9 x3x2 x10 x3x2 x11 x3x12)x12 (proof)