Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../00976..
PUYk9../16286..
vout
PrPhD../e0e2b.. 3.40 bars
TMZ3u../bbfdb.. ownership of d176f.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMJEC../3a9a0.. ownership of 6b566.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUMyU../4d71b.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem d176f.. : ∀ x0 : ι → ι → ο . ∀ x1 : ι → ι . ∀ x2 x3 : ι → ι → ο . ∀ x4 x5 : ι → ι → ι . ∀ x6 : ι → ο . ∀ x7 . ∀ x8 : ι → ο . ∀ x9 : ι → ι → ο . ∀ x10 : ι → ι . ∀ x11 : ι → ι → ο . ∀ x12 x13 : ι → ι . ∀ x14 : ι → ι → ο . ∀ x15 : ι → ο . ∀ x16 . ∀ x17 : ι → ο . ∀ x18 : ι → ι . ∀ x19 : ι → ι → ο . ∀ x20 : ι → ι . ∀ x21 : ι → ο . ∀ x22 . ∀ x23 : ι → ι . ∀ x24 : ι → ο . ∀ x25 . ∀ x26 x27 x28 x29 : ι → ο . ∀ x30 . ∀ x31 x32 x33 : ι → ο . ∀ x34 x35 . ∀ x36 x37 x38 : ι → ο . ∀ x39 . ∀ x40 : ι → ι . ∀ x41 x42 : ι → ο . ∀ x43 : ι → ι . ∀ x44 x45 . ∀ x46 x47 : ι → ι . ∀ x48 x49 x50 . ∀ x51 : ι → ο . ∀ x52 : ι → ι . ∀ x53 : ι → ι → ο . ∀ x54 . ∀ x55 x56 : ι → ο . ∀ x57 : ι → ι . ∀ x58 : ι → ι → ι → ι . ∀ x59 : ι → ι → ι . ∀ x60 : ι → ο . ∀ x61 . ∀ x62 : ι → ο . (∀ x63 x64 . x62 x64 ⟶ (x64 = x63 ⟶ False) ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 x64 . x0 x63 x64 ⟶ x62 x64 ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x63 = x61 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x0 x63 x64 ⟶ x2 x64 (x1 x65) ⟶ x62 x65 ⟶ False) ⟶ (∀ x63 x64 x65 . x0 x64 x65 ⟶ x2 x65 (x1 x63) ⟶ (x2 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x64 x63 ⟶ (x2 x64 (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x2 x64 (x1 x63) ⟶ (x3 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x2 x63 x64 ⟶ (x62 x64 ⟶ False) ⟶ (x0 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x60 x65 ⟶ x2 x63 (x1 (x57 x65)) ⟶ x2 x64 (x1 (x57 x65)) ⟶ (x3 (x58 (x57 x65) (x59 x65 x63) (x59 x65 x64)) (x59 x65 (x58 (x57 x65) x63 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x3 x64 x65 ⟶ x3 x65 x63 ⟶ (x3 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x0 x64 x63 ⟶ (x2 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x4 x63 x61 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x60 x65 ⟶ x2 x63 (x1 (x57 x65)) ⟶ x2 x64 (x1 (x57 x65)) ⟶ x3 x63 x64 ⟶ (x3 (x59 x65 x63) (x59 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x60 x65 ⟶ x2 x63 (x1 (x57 x65)) ⟶ x2 x64 (x1 (x57 x65)) ⟶ x3 x63 x64 ⟶ (x3 (x5 x65 x63) (x5 x65 x64) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x3 x63 (x5 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 x66 . x3 x65 x66 ⟶ x3 x64 x63 ⟶ (x3 (x4 x65 x64) (x4 x66 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x3 x64 x63 ⟶ (x4 x64 x63 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x3 x63 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x58 x65 x64 x63 = x4 x64 x63 ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ (x62 x7 ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x9 (x10 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x2 (x10 x63) (x1 (x57 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x11 (x12 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x2 (x12 x63) (x1 (x57 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 . x60 x63 ⟶ (x14 (x13 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x60 x63 ⟶ (x2 (x13 x63) (x1 (x57 x63)) ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x56 x16 ⟶ False) ⟶ False) ⟶ ((x17 x16 ⟶ False) ⟶ False) ⟶ ((x62 x16 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x19 (x18 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x2 (x18 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . x19 (x20 x63) x63 ⟶ False) ⟶ (∀ x63 . (x2 (x20 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ ((x21 x22 ⟶ False) ⟶ False) ⟶ ((x55 x22 ⟶ False) ⟶ False) ⟶ (x62 x22 ⟶ False) ⟶ (x62 x54 ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x11 (x23 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x53 (x23 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x2 (x23 x63) (x1 (x57 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 (x52 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x2 (x52 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ ((x51 x50 ⟶ False) ⟶ False) ⟶ ((x24 x50 ⟶ False) ⟶ False) ⟶ ((x55 x49 ⟶ False) ⟶ False) ⟶ (x62 x49 ⟶ False) ⟶ ((x15 x48 ⟶ False) ⟶ False) ⟶ ((x62 x25 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x53 (x47 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x2 (x47 x63) (x1 (x57 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ x62 (x46 x63) ⟶ False) ⟶ (∀ x63 . (x62 x63 ⟶ False) ⟶ (x2 (x46 x63) (x1 x63) ⟶ False) ⟶ False) ⟶ ((x24 x45 ⟶ False) ⟶ False) ⟶ (x62 x45 ⟶ False) ⟶ ((x55 x44 ⟶ False) ⟶ False) ⟶ (x62 x44 ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x53 (x43 x63) x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x8 x63 ⟶ x60 x63 ⟶ (x2 (x43 x63) (x1 (x57 x63)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x5 x64 (x5 x64 x63) = x5 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x59 x64 (x59 x64 x63) = x59 x64 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x58 x65 x64 x64 = x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . (x4 x63 x63 = x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x53 (x59 x64 x63) x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x8 x65 ⟶ x60 x65 ⟶ x53 x64 x65 ⟶ x2 x64 (x1 (x57 x65)) ⟶ x53 x63 x65 ⟶ x2 x63 (x1 (x57 x65)) ⟶ (x53 (x4 x64 x63) x65 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x62 (x4 x63 x64) ⟶ False) ⟶ (∀ x63 x64 x65 . x8 x65 ⟶ x60 x65 ⟶ x11 x64 x65 ⟶ x2 x64 (x1 (x57 x65)) ⟶ x11 x63 x65 ⟶ x2 x63 (x1 (x57 x65)) ⟶ (x11 (x4 x64 x63) x65 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x62 (x4 x64 x63) ⟶ False) ⟶ (∀ x63 x64 . x24 x64 ⟶ x24 x63 ⟶ (x24 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x55 x64 ⟶ x55 x63 ⟶ (x55 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x26 x64 ⟶ x26 x63 ⟶ (x26 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x42 x64 ⟶ x42 x63 ⟶ (x42 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x27 x64 ⟶ x27 x63 ⟶ (x27 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x41 x64 ⟶ x41 x63 ⟶ (x41 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x28 x64 ⟶ x28 x63 ⟶ (x28 (x4 x64 x63) ⟶ False) ⟶ False) ⟶ ((x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x11 (x5 x64 x63) x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 (x1 x63) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x14 x63 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x62 (x59 x64 x63) ⟶ False) ⟶ False) ⟶ (∀ x63 . (x2 (x40 x63) x63 ⟶ False) ⟶ False) ⟶ ((x29 x30 ⟶ False) ⟶ False) ⟶ ((x60 x39 ⟶ False) ⟶ False) ⟶ (∀ x63 . x60 x63 ⟶ (x29 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x2 (x58 x65 x64 x63) (x1 x65) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x2 (x5 x64 x63) (x1 (x57 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ (x2 (x59 x64 x63) (x1 (x57 x64)) ⟶ False) ⟶ False) ⟶ (∀ x63 x64 x65 . x2 x64 (x1 x65) ⟶ x2 x63 (x1 x65) ⟶ (x58 x65 x64 x63 = x58 x65 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x4 x64 x63 = x4 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x6 x63 ⟶ (x31 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x6 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x53 x63 x64 ⟶ x9 x63 x64 ⟶ (x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x11 x63 x64 ⟶ x14 x63 x64 ⟶ (x9 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x27 x63 ⟶ (x28 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x15 x63 ⟶ (x56 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x9 x63 x64 ⟶ (x14 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x62 x64 ⟶ x2 x63 (x1 x64) ⟶ x19 x63 x64 ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x24 x63 ⟶ (x51 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x24 x63 ⟶ (x24 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x27 x63 ⟶ (x41 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x24 x63 ⟶ x62 x63 ⟶ (x38 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x24 x63 ⟶ x62 x63 ⟶ (x24 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x15 x63 ⟶ (x17 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x62 x63 ⟶ (x9 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x2 x63 (x1 x64) ⟶ x62 x63 ⟶ (x19 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x24 x63 ⟶ (x32 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ x24 x63 ⟶ (x24 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x42 x63 ⟶ (x27 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x37 x63 ⟶ (x15 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x62 x63 ⟶ (x14 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . (x62 x64 ⟶ False) ⟶ x2 x63 (x1 x64) ⟶ (x19 x63 x64 ⟶ False) ⟶ x62 x63 ⟶ False) ⟶ (∀ x63 x64 . x24 x64 ⟶ x2 x63 (x1 x64) ⟶ (x24 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x62 x63 ⟶ (x11 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 . x26 x63 ⟶ (x42 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x21 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x55 x64 ⟶ x2 x63 (x1 x64) ⟶ (x55 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x26 x64 ⟶ x2 x63 (x1 x64) ⟶ (x26 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x42 x64 ⟶ x2 x63 (x1 x64) ⟶ (x42 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x27 x64 ⟶ x2 x63 (x1 x64) ⟶ (x27 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x41 x64 ⟶ x2 x63 (x1 x64) ⟶ (x41 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x8 x64 ⟶ x60 x64 ⟶ x2 x63 (x1 (x57 x64)) ⟶ x62 x63 ⟶ (x53 x63 x64 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x62 x64 ⟶ x2 x63 (x1 x64) ⟶ (x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x24 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x55 x63 ⟶ (x26 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x24 x63 ⟶ x62 x63 ⟶ (x38 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x24 x63 ⟶ x62 x63 ⟶ (x24 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x28 x64 ⟶ x2 x63 (x1 x64) ⟶ (x28 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 . x62 x63 ⟶ (x55 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x55 x64 ⟶ x2 x63 x64 ⟶ (x37 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x26 x64 ⟶ x2 x63 x64 ⟶ (x33 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x42 x64 ⟶ x2 x63 x64 ⟶ (x36 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x27 x64 ⟶ x2 x63 x64 ⟶ (x15 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x41 x64 ⟶ x2 x63 x64 ⟶ (x56 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x28 x64 ⟶ x2 x63 x64 ⟶ (x17 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x6 x64 ⟶ x2 x63 (x1 x64) ⟶ (x6 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x6 x64 ⟶ x2 x63 x64 ⟶ (x38 x63 ⟶ False) ⟶ False) ⟶ (∀ x63 x64 . x0 x63 x64 ⟶ x0 x64 x63 ⟶ False) ⟶ (x3 (x58 (x57 x34) x35 (x59 x34 (x5 x34 x35))) (x5 x34 (x59 x34 (x58 (x57 x34) x35 (x59 x34 (x5 x34 x35))))) ⟶ False) ⟶ ((x3 x35 (x5 x34 (x59 x34 x35)) ⟶ False) ⟶ False) ⟶ ((x2 x35 (x1 (x57 x34)) ⟶ False) ⟶ False) ⟶ ((x60 x34 ⟶ False) ⟶ False) ⟶ ((x8 x34 ⟶ False) ⟶ False) ⟶ False (proof)