Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNLf../02f34..
PUfRa../90d5d..
vout
PrNLf../17c1c.. 24.94 bars
TMQzg../430b4.. ownership of 3ecb6.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
TMWEg../65776.. ownership of 4766a.. as prop with payaddr Pr4zB.. rightscost 0.00 controlledby Pr4zB.. upto 0
PUUtG../cfd8e.. 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 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 84d5a.. := λ 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)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 2e1d5.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (84d5a.. 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 e5411.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (2e1d5.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9(x1 = x10∀ x12 : ο . x12)(x2 = x10∀ x12 : ο . x12)(x3 = x10∀ x12 : ο . x12)(x4 = x10∀ x12 : ο . x12)(x5 = x10∀ x12 : ο . x12)(x6 = x10∀ x12 : ο . x12)(x7 = x10∀ x12 : ο . x12)(x8 = x10∀ x12 : ο . x12)(x9 = x10∀ x12 : ο . x12)x0 x1 x10not (x0 x2 x10)x0 x3 x10x0 x4 x10not (x0 x5 x10)not (x0 x6 x10)not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
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 af16d.. := λ 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)not (x0 x3 x8)x0 x4 x8not (x0 x5 x8)not (x0 x6 x8)not (x0 x7 x8)x9)x9
Definition 093ca.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (af16d.. 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)x0 x5 x9not (x0 x6 x9)not (x0 x7 x9)x0 x8 x9x10)x10
Definition 133c1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (093ca.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9(x1 = x10∀ x12 : ο . x12)(x2 = x10∀ x12 : ο . x12)(x3 = x10∀ x12 : ο . x12)(x4 = x10∀ x12 : ο . x12)(x5 = x10∀ x12 : ο . x12)(x6 = x10∀ x12 : ο . x12)(x7 = x10∀ x12 : ο . x12)(x8 = x10∀ x12 : ο . x12)(x9 = x10∀ x12 : ο . x12)not (x0 x1 x10)not (x0 x2 x10)x0 x3 x10not (x0 x4 x10)not (x0 x5 x10)x0 x6 x10not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
Definition efc7e.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (133c1.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10(x1 = x11∀ x13 : ο . x13)(x2 = x11∀ x13 : ο . x13)(x3 = x11∀ x13 : ο . x13)(x4 = x11∀ x13 : ο . x13)(x5 = x11∀ x13 : ο . x13)(x6 = x11∀ x13 : ο . x13)(x7 = x11∀ x13 : ο . x13)(x8 = x11∀ x13 : ο . x13)(x9 = x11∀ x13 : ο . x13)(x10 = x11∀ x13 : ο . x13)x0 x1 x11x0 x2 x11not (x0 x3 x11)not (x0 x4 x11)x0 x5 x11not (x0 x6 x11)not (x0 x7 x11)x0 x8 x11not (x0 x9 x11)not (x0 x10 x11)x12)x12
Definition 21422.. := λ 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)x0 x6 x7x8)x8
Definition f0d5b.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 . ∀ x9 : ο . (21422.. 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 8f55d.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 . ∀ x10 : ο . (f0d5b.. 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 5bc1a.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 . ∀ x11 : ο . (8f55d.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9(x1 = x10∀ x12 : ο . x12)(x2 = x10∀ x12 : ο . x12)(x3 = x10∀ x12 : ο . x12)(x4 = x10∀ x12 : ο . x12)(x5 = x10∀ x12 : ο . x12)(x6 = x10∀ x12 : ο . x12)(x7 = x10∀ x12 : ο . x12)(x8 = x10∀ x12 : ο . x12)(x9 = x10∀ x12 : ο . x12)x0 x1 x10x0 x2 x10x0 x3 x10not (x0 x4 x10)not (x0 x5 x10)not (x0 x6 x10)not (x0 x7 x10)x0 x8 x10not (x0 x9 x10)x11)x11
Definition 8aed1.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (5bc1a.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10(x1 = x11∀ x13 : ο . x13)(x2 = x11∀ x13 : ο . x13)(x3 = x11∀ x13 : ο . x13)(x4 = x11∀ x13 : ο . x13)(x5 = x11∀ x13 : ο . x13)(x6 = x11∀ x13 : ο . x13)(x7 = x11∀ x13 : ο . x13)(x8 = x11∀ x13 : ο . x13)(x9 = x11∀ x13 : ο . x13)(x10 = x11∀ x13 : ο . x13)x0 x1 x11x0 x2 x11x0 x3 x11not (x0 x4 x11)not (x0 x5 x11)not (x0 x6 x11)not (x0 x7 x11)x0 x8 x11not (x0 x9 x11)not (x0 x10 x11)x12)x12
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 12db5.. : ∀ 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 . x12x0∀ x13 . x13x0e5411.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . (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 x3not (x2 x12 x3)not (x2 x13 x3)x14)(x2 x4 x3not (x2 x5 x3)not (x2 x6 x3)not (x2 x7 x3)x2 x8 x3x2 x9 x3not (x2 x10 x3)x2 x11 x3not (x2 x12 x3)not (x2 x13 x3)x14)x14
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 3ecb6.. : ∀ 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 . x12x0∀ x13 . x13x0e5411.. x2 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13∀ x14 : ο . (∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x0efc7e.. x2 x15 x16 x17 x18 x19 x20 x3 x21 x22 x23 x24x14)(∀ x15 . x15x0∀ x16 . x16x0∀ x17 . x17x0∀ x18 . x18x0∀ x19 . x19x0∀ x20 . x20x0∀ x21 . x21x0∀ x22 . x22x0∀ x23 . x23x0∀ x24 . x24x08aed1.. x2 x15 x16 x17 x18 x19 x20 x3 x21 x22 x23 x24x14)x14 (proof)