Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../40b5d..
PUNjb../acc5d..
vout
PrPhD../baf58.. 3.37 bars
TMRVe../2102f.. ownership of 86b6f.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMHNR../87119.. ownership of cee3a.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUZFM../82fed.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 86b6f.. : ∀ 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 . x60 x62 ⟶ (x62 = x61 ⟶ False) ⟶ x60 x61 ⟶ False) ⟶ (∀ x61 x62 . x0 x61 x62 ⟶ x60 x62 ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x61 = x59 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 x1 ⟶ x2 x61 x1 ⟶ x2 x62 x1 ⟶ x3 x63 x61 = x3 x62 x61 ⟶ (x63 = x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x0 x61 x62 ⟶ x2 x62 (x58 x63) ⟶ x60 x63 ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 x1 ⟶ x2 x61 x1 ⟶ x2 x62 x1 ⟶ (x3 (x3 x63 x61) x62 = x3 x63 (x3 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x0 x62 x63 ⟶ x2 x63 (x58 x61) ⟶ (x2 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x4 x59 x61 = x59 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x57 x62 x61 ⟶ (x2 x62 (x58 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 (x58 x61) ⟶ (x57 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x4 x61 x59 = x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x0 x62 x63 ⟶ x0 x61 x63 ⟶ x0 x61 (x5 x63 x62) ⟶ False) ⟶ (∀ x61 x62 . x0 x62 x61 ⟶ (x0 (x5 x61 x62) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x61 x62 ⟶ (x60 x62 ⟶ False) ⟶ (x0 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x0 x62 x61 ⟶ (x2 x62 x61 ⟶ False) ⟶ False) ⟶ ((x2 x59 x6 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x56 x61 x59 = x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x7 x61 ⟶ x8 x62 x61 ⟶ (x8 x61 x62 ⟶ False) ⟶ False) ⟶ ((x2 x54 x55 ⟶ False) ⟶ False) ⟶ ((x2 x54 x9 ⟶ False) ⟶ False) ⟶ ((x53 x54 x55 x9 ⟶ False) ⟶ False) ⟶ ((x10 x54 ⟶ False) ⟶ False) ⟶ (x60 x54 ⟶ False) ⟶ (∀ x61 . (x57 x61 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x58 x63) ⟶ x2 x62 x61 ⟶ (x53 x62 x63 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x58 x63) ⟶ x53 x62 x63 x61 ⟶ (x2 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x52 x62 x61 = x51 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x11 x62 x61 = x12 x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x49 x61 x62 = x4 x61 x62 ⟶ False) ⟶ False) ⟶ ((x9 = x6 ⟶ False) ⟶ False) ⟶ ((x50 x48 ⟶ False) ⟶ False) ⟶ (x60 x48 ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x46 (x47 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x2 (x47 x61) (x58 x61) ⟶ False) ⟶ False) ⟶ ((x50 x45 ⟶ False) ⟶ False) ⟶ (∀ x61 . x46 (x13 x61) x61 ⟶ False) ⟶ (∀ x61 . (x2 (x13 x61) (x58 x61) ⟶ False) ⟶ False) ⟶ (x60 x14 ⟶ False) ⟶ (∀ x61 . (x60 (x44 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . (x2 (x44 x61) (x58 x61) ⟶ False) ⟶ False) ⟶ ((x7 x43 ⟶ False) ⟶ False) ⟶ ((x15 x43 ⟶ False) ⟶ False) ⟶ ((x42 x43 ⟶ False) ⟶ False) ⟶ (x60 x43 ⟶ False) ⟶ ((x60 x41 ⟶ False) ⟶ False) ⟶ ((x2 x41 x1 ⟶ False) ⟶ False) ⟶ ((x60 x40 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ x60 (x16 x61) ⟶ False) ⟶ (∀ x61 . (x60 x61 ⟶ False) ⟶ (x2 (x16 x61) (x58 x61) ⟶ False) ⟶ False) ⟶ ((x7 x17 ⟶ False) ⟶ False) ⟶ ((x7 x39 ⟶ False) ⟶ False) ⟶ (x60 x39 ⟶ False) ⟶ ((x2 x39 x1 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x56 x61 x61 = x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x6 ⟶ x61 = x38 x62 x54 ⟶ (x0 x61 x37 ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 x37 ⟶ (x61 = x38 (x18 x61) x54 ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 x37 ⟶ (x2 (x18 x61) x6 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 x6 ⟶ x2 x61 x6 ⟶ x62 = x38 x63 x61 ⟶ x8 x63 x61 ⟶ (x61 = x59 ⟶ False) ⟶ (x0 x62 x19 ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 x19 ⟶ x36 x61 = x59 ⟶ False) ⟶ (∀ x61 . x0 x61 x19 ⟶ (x8 (x20 x61) (x36 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 x19 ⟶ (x61 = x38 (x20 x61) (x36 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 x19 ⟶ (x2 (x36 x61) x6 ⟶ False) ⟶ False) ⟶ (∀ x61 . x0 x61 x19 ⟶ (x2 (x20 x61) x6 ⟶ False) ⟶ False) ⟶ ((x7 x6 ⟶ False) ⟶ False) ⟶ (x60 x6 ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x60 (x56 x61 x62) ⟶ False) ⟶ (∀ x61 x62 . x50 x62 ⟶ x50 x61 ⟶ (x50 (x12 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x50 x62 ⟶ x50 x61 ⟶ (x7 (x12 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x60 (x56 x62 x61) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x50 (x51 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x7 (x51 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 (x21 x61 x62) ⟶ False) ⟶ (x60 x1 ⟶ False) ⟶ (∀ x61 . x60 (x22 x61) ⟶ False) ⟶ ((x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 (x58 x61) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x7 x61 ⟶ (x7 (x56 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x58 x62) ⟶ (x53 (x23 x61 x62) x62 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . (x2 (x35 x61) x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . (x60 x63 ⟶ False) ⟶ (x60 x61 ⟶ False) ⟶ x2 x61 (x58 x63) ⟶ x53 x62 x63 x61 ⟶ (x2 x62 x63 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x7 (x52 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x1 ⟶ x2 x61 x1 ⟶ (x2 (x3 x62 x61) x1 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x7 (x11 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x2 (x24 x62 x61) x1 ⟶ False) ⟶ False) ⟶ (∀ x61 . x2 x61 x1 ⟶ (x2 (x34 x61) x6 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x2 (x49 x61 x62) (x58 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 . x2 x61 x1 ⟶ (x2 (x33 x61) x6 ⟶ False) ⟶ False) ⟶ ((x2 x9 (x58 x55) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x7 x61 ⟶ (x7 (x51 x62 x61) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x7 x61 ⟶ (x7 (x12 x62 x61) ⟶ False) ⟶ False) ⟶ ((x1 = x56 (x49 x19 x37) x6 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x38 x62 x61 = x21 (x21 x62 x61) (x22 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 x63 . x2 x63 x1 ⟶ x2 x61 x1 ⟶ x2 x62 x1 ⟶ x61 = x3 x63 x62 ⟶ (x32 x63 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x1 ⟶ x2 x61 x1 ⟶ x32 x62 x61 ⟶ (x61 = x3 x62 (x25 x61 x62) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x1 ⟶ x2 x61 x1 ⟶ x32 x62 x61 ⟶ (x2 (x25 x61 x62) x1 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x1 ⟶ x2 x61 x1 ⟶ (x3 x62 x61 = x24 (x11 (x52 (x33 x62) (x34 x61)) (x52 (x33 x61) (x34 x62))) (x52 (x34 x62) (x34 x61)) ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x1 ⟶ x2 x61 x1 ⟶ (x32 x62 x61 ⟶ False) ⟶ (x32 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x52 x62 x61 = x52 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x2 x62 x1 ⟶ x2 x61 x1 ⟶ (x3 x62 x61 = x3 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x50 x62 ⟶ x7 x61 ⟶ x50 x61 ⟶ (x11 x62 x61 = x11 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x56 x62 x61 = x56 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x21 x62 x61 = x21 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x31 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x2 x61 x6 ⟶ (x50 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x50 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x50 x61 ⟶ (x7 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x2 x61 x62 ⟶ (x7 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x2 x61 (x58 x62) ⟶ x46 x61 x62 ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x30 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x2 x61 (x58 x62) ⟶ x60 x61 ⟶ (x46 x61 x62 ⟶ False) ⟶ False) ⟶ (∀ x61 . x60 x61 ⟶ (x7 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . (x60 x62 ⟶ False) ⟶ x2 x61 (x58 x62) ⟶ (x46 x61 x62 ⟶ False) ⟶ x60 x61 ⟶ False) ⟶ (∀ x61 x62 . x7 x62 ⟶ x2 x61 x62 ⟶ (x7 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x42 x61 ⟶ x15 x61 ⟶ (x7 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x60 x62 ⟶ x2 x61 (x58 x62) ⟶ (x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x7 x61 ⟶ (x15 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x7 x61 ⟶ (x42 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x2 x61 x1 ⟶ x7 x61 ⟶ (x50 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 . x2 x61 x1 ⟶ x7 x61 ⟶ (x7 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x31 x62 ⟶ x2 x61 (x58 x62) ⟶ (x31 x61 ⟶ False) ⟶ False) ⟶ (∀ x61 x62 . x0 x61 x62 ⟶ x0 x62 x61 ⟶ False) ⟶ (x32 x27 x26 ⟶ False) ⟶ ((x32 x28 x29 ⟶ False) ⟶ False) ⟶ ((x3 x28 x26 = x3 x29 x27 ⟶ False) ⟶ False) ⟶ ((x2 x27 x1 ⟶ False) ⟶ False) ⟶ ((x2 x29 x1 ⟶ False) ⟶ False) ⟶ ((x2 x26 x1 ⟶ False) ⟶ False) ⟶ ((x2 x28 x1 ⟶ False) ⟶ False) ⟶ False (proof)