Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../3bf61..
PUPkc../da490..
vout
PrPhD../b32c7.. 3.40 bars
TMJmF../052bb.. ownership of 1e12d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMJwy../daa30.. ownership of b92e0.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUK8a../69f50.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 1e12d.. : ∀ 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 : ι → ο . ∀ x65 : ι → ι → ο . ∀ x66 : ι → ο . (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ (x65 x68 x67 ⟶ False) ⟶ (x64 x67 ⟶ False) ⟶ (x63 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x0 x68 ⟶ (x68 = x67 ⟶ False) ⟶ x0 x67 ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ (x65 x68 x67 ⟶ False) ⟶ (x63 x68 ⟶ False) ⟶ (x64 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x1 x67 x68 ⟶ x0 x68 ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ x65 x68 x67 ⟶ (x0 x68 ⟶ False) ⟶ (x63 x67 ⟶ False) ⟶ (x64 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x67 = x2 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . x1 x67 x68 ⟶ x61 x68 (x62 x69) ⟶ x0 x69 ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ x65 x68 x67 ⟶ (x0 x67 ⟶ False) ⟶ (x64 x68 ⟶ False) ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . x1 x68 x69 ⟶ x61 x69 (x62 x67) ⟶ (x61 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ x65 x68 x67 ⟶ (x63 x67 ⟶ False) ⟶ x63 x68 ⟶ False) ⟶ (∀ x67 x68 . x60 x68 x67 ⟶ (x61 x68 (x62 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x61 x68 (x62 x67) ⟶ (x60 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ x65 x68 x67 ⟶ (x64 x68 ⟶ False) ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 x68 x69 . x66 x69 ⟶ x66 x67 ⟶ x66 x68 ⟶ (x65 x67 x69 ⟶ False) ⟶ (x65 x68 x4 ⟶ False) ⟶ x65 (x3 x68 x67) (x3 x68 x69) ⟶ False) ⟶ (∀ x67 x68 . x61 x67 x68 ⟶ (x0 x68 ⟶ False) ⟶ (x1 x67 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ x65 x68 x67 ⟶ x64 x67 ⟶ (x64 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x59 x68 ⟶ x59 x67 ⟶ x65 x68 x67 ⟶ x65 x67 x68 ⟶ (x68 = x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x1 x68 x67 ⟶ (x61 x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ x65 x68 x67 ⟶ x63 x68 ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ ((x61 x2 x5 ⟶ False) ⟶ False) ⟶ ((x61 x4 x58 ⟶ False) ⟶ False) ⟶ ((x61 x4 x6 ⟶ False) ⟶ False) ⟶ ((x57 x4 x58 x6 ⟶ False) ⟶ False) ⟶ ((x63 x4 ⟶ False) ⟶ False) ⟶ (x0 x4 ⟶ False) ⟶ ((x65 x4 x4 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x59 x68 ⟶ x59 x67 ⟶ (x65 x68 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x60 x67 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . (x0 x69 ⟶ False) ⟶ (x0 x67 ⟶ False) ⟶ x61 x67 (x62 x69) ⟶ x61 x68 x67 ⟶ (x57 x68 x69 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . (x0 x69 ⟶ False) ⟶ (x0 x67 ⟶ False) ⟶ x61 x67 (x62 x69) ⟶ x57 x68 x69 x67 ⟶ (x61 x68 x67 ⟶ False) ⟶ False) ⟶ ((x6 = x5 ⟶ False) ⟶ False) ⟶ ((x7 x8 ⟶ False) ⟶ False) ⟶ (x0 x8 ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ (x0 x10 ⟶ False) ⟶ ((x59 x11 ⟶ False) ⟶ False) ⟶ ((x0 x11 ⟶ False) ⟶ False) ⟶ ((x66 x12 ⟶ False) ⟶ False) ⟶ ((x59 x12 ⟶ False) ⟶ False) ⟶ ((x13 x12 ⟶ False) ⟶ False) ⟶ ((x0 x12 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ (x15 (x14 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ (x61 (x14 x67) (x62 x67) ⟶ False) ⟶ False) ⟶ ((x9 x16 ⟶ False) ⟶ False) ⟶ ((x64 x56 ⟶ False) ⟶ False) ⟶ ((x59 x56 ⟶ False) ⟶ False) ⟶ ((x66 x55 ⟶ False) ⟶ False) ⟶ ((x64 x55 ⟶ False) ⟶ False) ⟶ ((x59 x55 ⟶ False) ⟶ False) ⟶ ((x13 x55 ⟶ False) ⟶ False) ⟶ (∀ x67 . x15 (x54 x67) x67 ⟶ False) ⟶ (∀ x67 . (x61 (x54 x67) (x62 x67) ⟶ False) ⟶ False) ⟶ ((x53 x52 ⟶ False) ⟶ False) ⟶ ((x17 x52 ⟶ False) ⟶ False) ⟶ (x0 x52 ⟶ False) ⟶ ((x63 x18 ⟶ False) ⟶ False) ⟶ ((x59 x18 ⟶ False) ⟶ False) ⟶ ((x66 x19 ⟶ False) ⟶ False) ⟶ ((x63 x19 ⟶ False) ⟶ False) ⟶ ((x59 x19 ⟶ False) ⟶ False) ⟶ ((x13 x19 ⟶ False) ⟶ False) ⟶ (x0 x20 ⟶ False) ⟶ (∀ x67 . (x0 (x51 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 . (x61 (x51 x67) (x62 x67) ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ ((x21 x49 ⟶ False) ⟶ False) ⟶ ((x48 x49 ⟶ False) ⟶ False) ⟶ (x0 x49 ⟶ False) ⟶ ((x50 x47 ⟶ False) ⟶ False) ⟶ (x0 x47 ⟶ False) ⟶ ((x61 x47 (x62 x58) ⟶ False) ⟶ False) ⟶ ((x17 x22 ⟶ False) ⟶ False) ⟶ (x0 x22 ⟶ False) ⟶ ((x23 x24 ⟶ False) ⟶ False) ⟶ ((x59 x46 ⟶ False) ⟶ False) ⟶ ((x66 x25 ⟶ False) ⟶ False) ⟶ ((x0 x45 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ x0 (x26 x67) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ (x61 (x26 x67) (x62 x67) ⟶ False) ⟶ False) ⟶ ((x50 x27 ⟶ False) ⟶ False) ⟶ ((x17 x44 ⟶ False) ⟶ False) ⟶ (x0 x44 ⟶ False) ⟶ ((x23 x43 ⟶ False) ⟶ False) ⟶ ((x66 x43 ⟶ False) ⟶ False) ⟶ ((x13 x43 ⟶ False) ⟶ False) ⟶ ((x59 x43 ⟶ False) ⟶ False) ⟶ ((x61 x43 x58 ⟶ False) ⟶ False) ⟶ ((x50 x5 ⟶ False) ⟶ False) ⟶ (x0 x5 ⟶ False) ⟶ ((x17 x5 ⟶ False) ⟶ False) ⟶ ((x53 x5 ⟶ False) ⟶ False) ⟶ ((x53 x58 ⟶ False) ⟶ False) ⟶ ((x42 x58 ⟶ False) ⟶ False) ⟶ ((x0 x2 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 (x62 x67) ⟶ False) ⟶ (∀ x67 x68 . (x0 x68 ⟶ False) ⟶ (x0 x67 ⟶ False) ⟶ x61 x67 (x62 x68) ⟶ (x57 (x28 x67 x68) x68 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x61 (x41 x67) x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 x69 . (x0 x69 ⟶ False) ⟶ (x0 x67 ⟶ False) ⟶ x61 x67 (x62 x69) ⟶ x57 x68 x69 x67 ⟶ (x61 x68 x69 ⟶ False) ⟶ False) ⟶ ((x61 x6 (x62 x58) ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x66 x68 ⟶ x66 x67 ⟶ (x66 (x3 x68 x67) ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x59 x68 ⟶ x59 x67 ⟶ (x65 x68 x67 ⟶ False) ⟶ (x65 x67 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x29 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x7 x67 ⟶ (x40 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ (x63 x67 ⟶ False) ⟶ (x64 x67 ⟶ False) ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ (x63 x67 ⟶ False) ⟶ (x64 x67 ⟶ False) ⟶ (x0 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x61 x67 x5 ⟶ (x9 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x61 x67 (x62 x58) ⟶ (x42 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x7 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ x59 x67 ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ x59 x67 ⟶ x63 x67 ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ x59 x67 ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x9 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ x59 x67 ⟶ (x63 x67 ⟶ False) ⟶ (x64 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ x59 x67 ⟶ (x63 x67 ⟶ False) ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x50 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ x64 x67 ⟶ x63 x67 ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ x64 x67 ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ x64 x67 ⟶ x0 x67 ⟶ False) ⟶ (∀ x67 x68 . x50 x68 ⟶ x61 x67 x68 ⟶ (x50 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x42 x67 ⟶ (x30 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ x59 x67 ⟶ (x64 x67 ⟶ False) ⟶ (x63 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . (x0 x67 ⟶ False) ⟶ x59 x67 ⟶ (x64 x67 ⟶ False) ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x0 x68 ⟶ x61 x67 (x62 x68) ⟶ x15 x67 x68 ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x39 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x42 x67 ⟶ (x31 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ x63 x67 ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ x63 x67 ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x59 x67 ⟶ x63 x67 ⟶ x0 x67 ⟶ False) ⟶ (∀ x67 . x66 x67 ⟶ (x13 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . (x0 x68 ⟶ False) ⟶ x61 x67 (x62 x68) ⟶ x0 x67 ⟶ (x15 x67 x68 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x50 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x9 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x38 x67 ⟶ (x42 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x23 x67 ⟶ (x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . (x0 x68 ⟶ False) ⟶ x61 x67 (x62 x68) ⟶ (x15 x67 x68 ⟶ False) ⟶ x0 x67 ⟶ False) ⟶ (∀ x67 . x48 x67 ⟶ x21 x67 ⟶ (x50 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x61 x67 x6 ⟶ x64 x67 ⟶ False) ⟶ (∀ x67 . x32 x67 ⟶ (x38 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x23 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x53 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x61 x67 x6 ⟶ (x17 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x17 x68 ⟶ x61 x67 (x62 x68) ⟶ (x17 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x32 x68 ⟶ x61 x67 (x62 x68) ⟶ (x32 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x38 x68 ⟶ x61 x67 (x62 x68) ⟶ (x38 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x42 x68 ⟶ x61 x67 (x62 x68) ⟶ (x42 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x31 x68 ⟶ x61 x67 (x62 x68) ⟶ (x31 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x61 x67 x58 ⟶ (x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x0 x68 ⟶ x61 x67 (x62 x68) ⟶ (x0 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x50 x67 ⟶ (x21 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x50 x67 ⟶ (x48 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x9 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x9 x67 ⟶ (x50 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x17 x67 ⟶ (x32 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x30 x68 ⟶ x61 x67 (x62 x68) ⟶ (x30 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x0 x67 ⟶ (x17 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x17 x68 ⟶ x61 x67 x68 ⟶ (x9 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x32 x68 ⟶ x61 x67 x68 ⟶ (x23 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x38 x68 ⟶ x61 x67 x68 ⟶ (x33 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x42 x68 ⟶ x61 x67 x68 ⟶ (x66 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x31 x68 ⟶ x61 x67 x68 ⟶ (x59 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x30 x68 ⟶ x61 x67 x68 ⟶ (x13 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 . x61 x67 (x62 x6) ⟶ (x17 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x7 x68 ⟶ x61 x67 (x62 x68) ⟶ (x7 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x29 x68 ⟶ x61 x67 (x62 x68) ⟶ (x29 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x7 x68 ⟶ x61 x67 x68 ⟶ (x37 x67 ⟶ False) ⟶ False) ⟶ (∀ x67 x68 . x1 x67 x68 ⟶ x1 x68 x67 ⟶ False) ⟶ (x65 (x3 x35 x34) (x3 x35 x36) ⟶ False) ⟶ (x65 x35 x4 ⟶ False) ⟶ ((x65 x34 x36 ⟶ False) ⟶ False) ⟶ ((x66 x35 ⟶ False) ⟶ False) ⟶ ((x66 x36 ⟶ False) ⟶ False) ⟶ ((x66 x34 ⟶ False) ⟶ False) ⟶ False (proof)