Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../3223f..
PUYjd../ee5e1..
vout
PrNUD../f223b.. 0.00 bars
TMbqv../ee486.. ownership of 57953.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMZLa../78504.. ownership of d4ee5.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUTiP../c3ada.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 57953.. : ∀ 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 . x56 x58 ⟶ (x58 = x57 ⟶ False) ⟶ x56 x57 ⟶ False) ⟶ (∀ x57 x58 . x0 x57 x58 ⟶ x56 x58 ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x57 = x55 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x57 x58 ⟶ x2 x58 (x1 x59) ⟶ x56 x59 ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x58 x59 ⟶ x2 x59 (x1 x57) ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x3 x55 x57 = x55 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x54 x58 x57 ⟶ (x2 x58 (x1 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 (x1 x57) ⟶ (x54 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x3 x57 x55 = x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x58 x59 ⟶ x0 x57 x59 ⟶ x0 x57 (x4 x59 x58) ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x57 ⟶ (x0 (x4 x57 x58) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x57 x58 ⟶ (x56 x58 ⟶ False) ⟶ (x0 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x57 ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ ((x2 x55 x5 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x53 x57 x55 = x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x6 x58 ⟶ x6 x57 ⟶ x7 x58 x57 ⟶ (x7 x57 x58 ⟶ False) ⟶ False) ⟶ ((x2 x51 x52 ⟶ False) ⟶ False) ⟶ ((x2 x51 x8 ⟶ False) ⟶ False) ⟶ ((x50 x51 x52 x8 ⟶ False) ⟶ False) ⟶ ((x9 x51 ⟶ False) ⟶ False) ⟶ (x56 x51 ⟶ False) ⟶ (∀ x57 . (x54 x57 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x56 x59 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x59) ⟶ x2 x58 x57 ⟶ (x50 x58 x59 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x56 x59 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x59) ⟶ x50 x58 x59 x57 ⟶ (x2 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x49 x57 x58 = x3 x57 x58 ⟶ False) ⟶ False) ⟶ ((x8 = x5 ⟶ False) ⟶ False) ⟶ ((x48 x47 ⟶ False) ⟶ False) ⟶ (x56 x47 ⟶ False) ⟶ (∀ x57 . (x56 x57 ⟶ False) ⟶ (x45 (x46 x57) x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x56 x57 ⟶ False) ⟶ (x2 (x46 x57) (x1 x57) ⟶ False) ⟶ False) ⟶ ((x48 x44 ⟶ False) ⟶ False) ⟶ (∀ x57 . x45 (x10 x57) x57 ⟶ False) ⟶ (∀ x57 . (x2 (x10 x57) (x1 x57) ⟶ False) ⟶ False) ⟶ (x56 x11 ⟶ False) ⟶ (∀ x57 . (x56 (x43 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . (x2 (x43 x57) (x1 x57) ⟶ False) ⟶ False) ⟶ ((x6 x42 ⟶ False) ⟶ False) ⟶ ((x12 x42 ⟶ False) ⟶ False) ⟶ ((x41 x42 ⟶ False) ⟶ False) ⟶ (x56 x42 ⟶ False) ⟶ ((x56 x40 ⟶ False) ⟶ False) ⟶ ((x2 x40 x13 ⟶ False) ⟶ False) ⟶ ((x56 x39 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x56 x57 ⟶ False) ⟶ x56 (x14 x57) ⟶ False) ⟶ (∀ x57 . (x56 x57 ⟶ False) ⟶ (x2 (x14 x57) (x1 x57) ⟶ False) ⟶ False) ⟶ ((x6 x15 ⟶ False) ⟶ False) ⟶ ((x6 x38 ⟶ False) ⟶ False) ⟶ (x56 x38 ⟶ False) ⟶ ((x2 x38 x13 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x53 x57 x57 = x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 x5 ⟶ x57 = x37 x58 x51 ⟶ (x0 x57 x36 ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x36 ⟶ (x57 = x37 (x16 x57) x51 ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x36 ⟶ (x2 (x16 x57) x5 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x2 x59 x5 ⟶ x2 x57 x5 ⟶ x58 = x37 x59 x57 ⟶ x7 x59 x57 ⟶ (x57 = x55 ⟶ False) ⟶ (x0 x58 x17 ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x17 ⟶ x35 x57 = x55 ⟶ False) ⟶ (∀ x57 . x0 x57 x17 ⟶ (x7 (x18 x57) (x35 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x17 ⟶ (x57 = x37 (x18 x57) (x35 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x17 ⟶ (x2 (x35 x57) x5 ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x17 ⟶ (x2 (x18 x57) x5 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x2 x59 (x1 x13) ⟶ x57 = x59 ⟶ x0 (x19 x59 x57) x59 ⟶ x2 x58 x13 ⟶ x0 x58 x59 ⟶ (x21 x58 (x20 x59 x57) ⟶ False) ⟶ (x0 x57 x22 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x2 x59 (x1 x13) ⟶ x57 = x59 ⟶ (x21 (x19 x59 x57) (x20 x59 x57) ⟶ False) ⟶ x2 x58 x13 ⟶ x0 x58 x59 ⟶ (x21 x58 (x20 x59 x57) ⟶ False) ⟶ (x0 x57 x22 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x2 x59 (x1 x13) ⟶ x57 = x59 ⟶ (x2 (x19 x59 x57) x13 ⟶ False) ⟶ x2 x58 x13 ⟶ x0 x58 x59 ⟶ (x21 x58 (x20 x59 x57) ⟶ False) ⟶ (x0 x57 x22 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 (x1 x13) ⟶ x57 = x58 ⟶ (x0 (x20 x58 x57) x58 ⟶ False) ⟶ (x0 x57 x22 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 (x1 x13) ⟶ x57 = x58 ⟶ (x2 (x20 x58 x57) x13 ⟶ False) ⟶ (x0 x57 x22 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x22 ⟶ x2 x57 x13 ⟶ x0 x57 (x33 x58) ⟶ x21 (x34 x57 x58) x57 ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x22 ⟶ x2 x57 x13 ⟶ x0 x57 (x33 x58) ⟶ (x0 (x34 x57 x58) (x33 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 x58 x22 ⟶ x2 x57 x13 ⟶ x0 x57 (x33 x58) ⟶ (x2 (x34 x57 x58) x13 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x0 x59 x22 ⟶ x2 x57 x13 ⟶ x0 x57 (x33 x59) ⟶ x2 x58 x13 ⟶ x21 x58 x57 ⟶ (x0 x58 (x33 x59) ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x22 ⟶ (x57 = x33 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x0 x57 x22 ⟶ (x2 (x33 x57) (x1 x13) ⟶ False) ⟶ False) ⟶ ((x6 x5 ⟶ False) ⟶ False) ⟶ (x56 x5 ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ x56 (x53 x57 x58) ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ x56 (x53 x58 x57) ⟶ False) ⟶ (∀ x57 x58 . x56 (x32 x57 x58) ⟶ False) ⟶ (x56 x13 ⟶ False) ⟶ (∀ x57 . x56 (x31 x57) ⟶ False) ⟶ ((x56 x55 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 (x1 x57) ⟶ False) ⟶ (∀ x57 x58 . x6 x58 ⟶ x6 x57 ⟶ (x6 (x53 x58 x57) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x58) ⟶ (x50 (x30 x57 x58) x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . (x2 (x23 x57) x57 ⟶ False) ⟶ False) ⟶ ((x56 x29 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . (x56 x59 ⟶ False) ⟶ (x56 x57 ⟶ False) ⟶ x2 x57 (x1 x59) ⟶ x50 x58 x59 x57 ⟶ (x2 x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x2 (x49 x57 x58) (x1 x57) ⟶ False) ⟶ False) ⟶ ((x2 x8 (x1 x52) ⟶ False) ⟶ False) ⟶ ((x13 = x53 (x49 x17 x36) x5 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x37 x58 x57 = x32 (x32 x58 x57) (x31 x58) ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 (x28 x57 x58) x57 ⟶ (x54 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x0 (x28 x57 x58) x58 ⟶ False) ⟶ (x54 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 x59 . x54 x58 x59 ⟶ x0 x57 x58 ⟶ (x0 x57 x59 ⟶ False) ⟶ False) ⟶ ((x55 = x29 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x2 x58 x13 ⟶ x2 x57 x13 ⟶ (x21 x58 x57 ⟶ False) ⟶ (x21 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x53 x58 x57 = x53 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x32 x58 x57 = x32 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x24 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x2 x57 x5 ⟶ (x48 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x48 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x48 x57 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x6 x58 ⟶ x2 x57 x58 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x2 x57 (x1 x58) ⟶ x45 x57 x58 ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x25 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ x2 x57 (x1 x58) ⟶ x56 x57 ⟶ (x45 x57 x58 ⟶ False) ⟶ False) ⟶ (∀ x57 . x56 x57 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . (x56 x58 ⟶ False) ⟶ x2 x57 (x1 x58) ⟶ (x45 x57 x58 ⟶ False) ⟶ x56 x57 ⟶ False) ⟶ (∀ x57 x58 . x6 x58 ⟶ x2 x57 x58 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x41 x57 ⟶ x12 x57 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x56 x58 ⟶ x2 x57 (x1 x58) ⟶ (x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x6 x57 ⟶ (x12 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x6 x57 ⟶ (x41 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x2 x57 x13 ⟶ x6 x57 ⟶ (x48 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 . x2 x57 x13 ⟶ x6 x57 ⟶ (x6 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x24 x58 ⟶ x2 x57 (x1 x58) ⟶ (x24 x57 ⟶ False) ⟶ False) ⟶ (∀ x57 x58 . x0 x57 x58 ⟶ x0 x58 x57 ⟶ False) ⟶ (x54 x26 x27 ⟶ False) ⟶ (x54 x27 x26 ⟶ False) ⟶ ((x0 x26 x22 ⟶ False) ⟶ False) ⟶ ((x0 x27 x22 ⟶ False) ⟶ False) ⟶ False (proof)