Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../9b50a..
PUZUf../f088e..
vout
PrPhD../ce6dc.. 3.40 bars
TMH6M../f522f.. ownership of beb44.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMKeB../8e047.. ownership of 857f1.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUNu8../0cbc6.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem beb44.. : ∀ 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 . x58 x60 ⟶ (x60 = x59 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x58 x60 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x59 = x57 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x59 x60 ⟶ x2 x60 (x1 x61) ⟶ x58 x61 ⟶ False) ⟶ (∀ x59 x60 x61 . x0 x60 x61 ⟶ x2 x61 (x1 x59) ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 x64 . (x3 x64 ⟶ False) ⟶ x11 x64 ⟶ (x4 x63 ⟶ False) ⟶ x10 x63 ⟶ x5 x63 ⟶ x11 x63 ⟶ x64 = x6 x63 ⟶ x2 x59 (x9 x64) ⟶ x2 x62 (x9 x64) ⟶ x2 x60 (x9 x64) ⟶ x2 x61 (x9 x64) ⟶ (x7 x64 x59 x62 x60 x61 ⟶ False) ⟶ (x7 x64 x60 x61 x60 (x8 x61 x60 x62 x59 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 x64 . (x3 x64 ⟶ False) ⟶ x11 x64 ⟶ (x4 x63 ⟶ False) ⟶ x10 x63 ⟶ x5 x63 ⟶ x11 x63 ⟶ x64 = x6 x63 ⟶ x2 x59 (x9 x64) ⟶ x2 x62 (x9 x64) ⟶ x2 x60 (x9 x64) ⟶ x2 x61 (x9 x64) ⟶ (x7 x64 x59 x62 x60 x61 ⟶ False) ⟶ (x7 x64 x59 x62 x59 (x8 x61 x60 x62 x59 x63 x64) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 x64 . (x3 x64 ⟶ False) ⟶ x11 x64 ⟶ (x4 x63 ⟶ False) ⟶ x10 x63 ⟶ x5 x63 ⟶ x11 x63 ⟶ x64 = x6 x63 ⟶ x2 x59 (x9 x64) ⟶ x2 x62 (x9 x64) ⟶ x2 x60 (x9 x64) ⟶ x2 x61 (x9 x64) ⟶ (x7 x64 x59 x62 x60 x61 ⟶ False) ⟶ (x2 (x8 x61 x60 x62 x59 x63 x64) (x9 x64) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x10 x59 ⟶ x11 x59 ⟶ (x11 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x10 x59 ⟶ x11 x59 ⟶ (x12 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x10 x59 ⟶ x11 x59 ⟶ x4 (x6 x59) ⟶ False) ⟶ (∀ x59 x60 . x13 x60 x59 ⟶ (x2 x60 (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x59) ⟶ (x13 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x59 x60 ⟶ (x58 x60 ⟶ False) ⟶ (x0 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x60 x59 ⟶ (x2 x60 x59 ⟶ False) ⟶ False) ⟶ (x58 x14 ⟶ False) ⟶ (∀ x59 . (x13 x59 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x15 x59 ⟶ False) ⟶ x15 (x16 x59) ⟶ False) ⟶ (∀ x59 . (x15 x59 ⟶ False) ⟶ (x2 (x16 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x15 (x17 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ x58 (x17 x59) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x17 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x55 (x56 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x56 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x53 x59 ⟶ x58 (x54 x59) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x53 x59 ⟶ (x2 (x54 x59) (x1 (x9 x59)) ⟶ False) ⟶ False) ⟶ ((x5 x52 ⟶ False) ⟶ False) ⟶ ((x10 x52 ⟶ False) ⟶ False) ⟶ ((x51 x52 ⟶ False) ⟶ False) ⟶ (x4 x52 ⟶ False) ⟶ (x3 x52 ⟶ False) ⟶ ((x11 x52 ⟶ False) ⟶ False) ⟶ (∀ x59 . x55 (x50 x59) x59 ⟶ False) ⟶ (∀ x59 . (x2 (x50 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x10 x49 ⟶ False) ⟶ False) ⟶ ((x51 x49 ⟶ False) ⟶ False) ⟶ (x4 x49 ⟶ False) ⟶ (x3 x49 ⟶ False) ⟶ ((x11 x49 ⟶ False) ⟶ False) ⟶ (x58 x18 ⟶ False) ⟶ (∀ x59 . (x58 (x48 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x48 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x47 x46 ⟶ False) ⟶ False) ⟶ ((x12 x46 ⟶ False) ⟶ False) ⟶ ((x51 x46 ⟶ False) ⟶ False) ⟶ (x4 x46 ⟶ False) ⟶ (x3 x46 ⟶ False) ⟶ ((x11 x46 ⟶ False) ⟶ False) ⟶ ((x51 x45 ⟶ False) ⟶ False) ⟶ (x4 x45 ⟶ False) ⟶ ((x11 x45 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x53 x59 ⟶ x15 (x19 x59) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x53 x59 ⟶ (x2 (x19 x59) (x1 (x9 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x53 x59 ⟶ (x15 (x20 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x53 x59 ⟶ x58 (x20 x59) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x53 x59 ⟶ (x2 (x20 x59) (x1 (x9 x59)) ⟶ False) ⟶ False) ⟶ ((x58 x44 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ x58 (x21 x59) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x21 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x22 (x23 x59 x60) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x43 (x23 x60 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x24 (x23 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 (x23 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x2 (x23 x59 x60) (x1 (x25 x60 x59)) ⟶ False) ⟶ False) ⟶ ((x12 x42 ⟶ False) ⟶ False) ⟶ ((x51 x42 ⟶ False) ⟶ False) ⟶ (x4 x42 ⟶ False) ⟶ (x3 x42 ⟶ False) ⟶ ((x11 x42 ⟶ False) ⟶ False) ⟶ ((x51 x26 ⟶ False) ⟶ False) ⟶ ((x11 x26 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . x2 x61 (x1 (x25 (x25 x62 x62) (x25 x62 x62))) ⟶ x27 x62 x61 = x27 x60 x59 ⟶ (x61 = x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . x2 x61 (x1 (x25 (x25 x62 x62) (x25 x62 x62))) ⟶ x27 x62 x61 = x27 x59 x60 ⟶ (x62 = x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x28 x59 ⟶ False) ⟶ x53 x59 ⟶ x29 (x9 x59) ⟶ False) ⟶ (∀ x59 . x28 x59 ⟶ x53 x59 ⟶ (x29 (x9 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . x4 x59 ⟶ x53 x59 ⟶ (x15 (x9 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x4 x59 ⟶ False) ⟶ x53 x59 ⟶ x15 (x9 x59) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x53 x59 ⟶ x58 (x9 x59) ⟶ False) ⟶ ((x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 (x1 x59) ⟶ False) ⟶ (∀ x59 . x3 x59 ⟶ x53 x59 ⟶ (x58 (x9 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x51 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ x3 (x6 x59) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ (x58 x59 ⟶ False) ⟶ x58 (x25 x60 x59) ⟶ False) ⟶ (∀ x59 . (x2 (x41 x59) x59 ⟶ False) ⟶ False) ⟶ ((x53 x30 ⟶ False) ⟶ False) ⟶ ((x11 x40 ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x2 (x31 x59) (x1 (x25 (x25 (x9 x59) (x9 x59)) (x25 (x9 x59) (x9 x59)))) ⟶ False) ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ (x53 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x11 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x51 (x6 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 (x25 (x25 x60 x60) (x25 x60 x60))) ⟶ (x2 (x32 x60 x59) (x1 (x25 (x25 x60 x60) (x25 x60 x60))) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 (x25 (x25 x59 x59) (x25 x59 x59))) ⟶ (x11 (x27 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 (x25 (x25 x59 x59) (x25 x59 x59))) ⟶ (x51 (x27 x59 x60) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x3 x60 ⟶ False) ⟶ x11 x60 ⟶ x2 x59 (x9 x60) ⟶ x7 x60 (x36 x60) (x37 x60) (x36 x60) x59 ⟶ x7 x60 (x38 x60) (x39 x60) (x38 x60) x59 ⟶ (x47 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ x7 x59 (x36 x59) (x37 x59) (x38 x59) (x39 x59) ⟶ (x47 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x2 (x39 x59) (x9 x59) ⟶ False) ⟶ (x47 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x2 (x38 x59) (x9 x59) ⟶ False) ⟶ (x47 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x2 (x37 x59) (x9 x59) ⟶ False) ⟶ (x47 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x2 (x36 x59) (x9 x59) ⟶ False) ⟶ (x47 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 . (x3 x63 ⟶ False) ⟶ x11 x63 ⟶ x47 x63 ⟶ x2 x59 (x9 x63) ⟶ x2 x62 (x9 x63) ⟶ x2 x60 (x9 x63) ⟶ x2 x61 (x9 x63) ⟶ (x7 x63 x59 x62 x60 x61 ⟶ False) ⟶ (x7 x63 x60 x61 x60 (x35 x61 x60 x62 x59 x63) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 . (x3 x63 ⟶ False) ⟶ x11 x63 ⟶ x47 x63 ⟶ x2 x59 (x9 x63) ⟶ x2 x62 (x9 x63) ⟶ x2 x60 (x9 x63) ⟶ x2 x61 (x9 x63) ⟶ (x7 x63 x59 x62 x60 x61 ⟶ False) ⟶ (x7 x63 x59 x62 x59 (x35 x61 x60 x62 x59 x63) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 x63 . (x3 x63 ⟶ False) ⟶ x11 x63 ⟶ x47 x63 ⟶ x2 x59 (x9 x63) ⟶ x2 x62 (x9 x63) ⟶ x2 x60 (x9 x63) ⟶ x2 x61 (x9 x63) ⟶ (x7 x63 x59 x62 x60 x61 ⟶ False) ⟶ (x2 (x35 x61 x60 x62 x59 x63) (x9 x63) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 ⟶ False) ⟶ x11 x59 ⟶ (x6 x59 = x27 (x9 x59) (x32 (x9 x59) (x31 x59)) ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x34 x59 x57 ⟶ (x3 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x3 x59 ⟶ (x34 x59 x57 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ (x28 x59 ⟶ False) ⟶ x4 x59 ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x4 x59 ⟶ (x28 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x15 x60 ⟶ x2 x59 (x1 x60) ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ (x28 x59 ⟶ False) ⟶ x28 x59 ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ (x28 x59 ⟶ False) ⟶ x3 x59 ⟶ False) ⟶ (∀ x59 x60 . x58 x60 ⟶ x2 x59 (x1 x60) ⟶ x55 x59 x60 ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x3 x59 ⟶ (x28 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x3 x59 ⟶ (x3 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x58 x61 ⟶ x2 x59 (x1 (x25 x60 x61)) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ x58 x59 ⟶ (x55 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x58 x61 ⟶ x2 x59 (x1 (x25 x61 x60)) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ (x55 x59 x60 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ (x4 x59 ⟶ False) ⟶ x3 x59 ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x25 x59 x60)) ⟶ (x22 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x25 x60 x59)) ⟶ (x43 x61 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x58 x60 ⟶ x2 x59 (x1 x60) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x3 x59 ⟶ (x4 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 (x25 x59 x60)) ⟶ (x24 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ (x4 x59 ⟶ False) ⟶ x3 x59 ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x34 x59 x14 ⟶ (x4 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ x34 x59 x14 ⟶ x3 x59 ⟶ False) ⟶ (∀ x59 . x53 x59 ⟶ (x3 x59 ⟶ False) ⟶ x4 x59 ⟶ (x34 x59 x14 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x0 x60 x59 ⟶ False) ⟶ (∀ x59 . x11 x59 ⟶ x51 x59 ⟶ (x59 = x27 (x9 x59) (x31 x59) ⟶ False) ⟶ False) ⟶ ((x4 (x6 x33) ⟶ False) ⟶ x12 (x6 x33) ⟶ x47 (x6 x33) ⟶ x11 (x6 x33) ⟶ False) ⟶ ((x11 x33 ⟶ False) ⟶ False) ⟶ ((x5 x33 ⟶ False) ⟶ False) ⟶ ((x10 x33 ⟶ False) ⟶ False) ⟶ (x4 x33 ⟶ False) ⟶ False (proof)