Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../e0032..
PUcs3../61cd5..
vout
PrPhD../6886d.. 3.39 bars
TMHUg../355d3.. ownership of 5ca77.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMWrB../d2320.. ownership of 1117d.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUYoV../fe64d.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 5ca77.. : ∀ 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 . x3 x60 x59 ⟶ (x2 x60 (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x59) ⟶ (x3 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) ⟶ ((x2 x57 x4 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x3 x59 x59 ⟶ False) ⟶ False) ⟶ ((x5 = x4 ⟶ False) ⟶ False) ⟶ ((x56 x55 ⟶ False) ⟶ False) ⟶ (x58 x55 ⟶ False) ⟶ ((x54 x53 ⟶ False) ⟶ False) ⟶ (x58 x53 ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ x52 (x51 x59) ⟶ False) ⟶ (∀ x59 . (x52 x59 ⟶ False) ⟶ (x2 (x51 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x52 (x50 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ x58 (x50 x59) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x50 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ (x58 x7 ⟶ False) ⟶ (x8 x9 ⟶ False) ⟶ ((x49 x9 ⟶ False) ⟶ False) ⟶ ((x10 x9 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x47 (x48 x59) x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x48 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x6 x46 ⟶ False) ⟶ False) ⟶ ((x11 x12 ⟶ False) ⟶ False) ⟶ ((x45 x12 ⟶ False) ⟶ False) ⟶ ((x13 x12 ⟶ False) ⟶ False) ⟶ (x58 x12 ⟶ False) ⟶ ((x49 x12 ⟶ False) ⟶ False) ⟶ ((x44 x12 x5 ⟶ False) ⟶ False) ⟶ ((x10 x12 ⟶ False) ⟶ False) ⟶ (∀ x59 . x47 (x43 x59) x59 ⟶ False) ⟶ (∀ x59 . (x2 (x43 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x11 x42 ⟶ False) ⟶ False) ⟶ ((x49 x42 ⟶ False) ⟶ False) ⟶ ((x10 x42 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 (x14 x59) ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x14 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x41 x16 ⟶ False) ⟶ False) ⟶ ((x17 x16 ⟶ False) ⟶ False) ⟶ (x58 x16 ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x49 x19 ⟶ False) ⟶ False) ⟶ ((x10 x19 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ x58 (x40 x59) ⟶ False) ⟶ (∀ x59 . (x58 x59 ⟶ False) ⟶ (x2 (x40 x59) (x1 x59) ⟶ False) ⟶ False) ⟶ ((x15 x39 ⟶ False) ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ (x58 x21 ⟶ False) ⟶ ((x49 x22 ⟶ False) ⟶ False) ⟶ ((x10 x22 ⟶ False) ⟶ False) ⟶ ((x15 x4 ⟶ False) ⟶ False) ⟶ (x58 x4 ⟶ False) ⟶ ((x54 x23 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 (x1 x59) ⟶ False) ⟶ ((x20 x23 ⟶ False) ⟶ False) ⟶ (∀ x59 . (x2 (x38 x59) x59 ⟶ False) ⟶ False) ⟶ ((x2 x5 (x1 x24) ⟶ False) ⟶ False) ⟶ (∀ x59 . x2 x59 (x1 x23) ⟶ (x2 (x37 x59) (x1 x23) ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 (x25 x59 x60) x59 ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x0 (x25 x59 x60) x60 ⟶ False) ⟶ (x3 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x3 x60 x61 ⟶ x0 x59 x60 ⟶ (x0 x59 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x2 x60 (x1 x23) ⟶ x35 x60 ⟶ x3 x61 x60 ⟶ (x0 (x36 x59 x61) x60 ⟶ False) ⟶ (x0 (x36 x59 x61) x59 ⟶ False) ⟶ (x59 = x37 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x0 (x36 x59 x60) x59 ⟶ x0 (x36 x59 x60) (x26 x59 x60) ⟶ (x59 = x37 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x0 (x36 x59 x60) x59 ⟶ (x3 x60 (x26 x59 x60) ⟶ False) ⟶ (x59 = x37 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x0 (x36 x59 x60) x59 ⟶ (x35 (x26 x59 x60) ⟶ False) ⟶ (x59 = x37 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x0 (x36 x59 x60) x59 ⟶ (x2 (x26 x59 x60) (x1 x23) ⟶ False) ⟶ (x59 = x37 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x2 x60 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ (x2 (x36 x59 x60) x23 ⟶ False) ⟶ (x59 = x37 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x59 = x37 x61 ⟶ x2 x60 x23 ⟶ x0 x60 (x34 x60 x59 x61) ⟶ (x0 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x59 = x37 x61 ⟶ x2 x60 x23 ⟶ (x3 x61 (x34 x60 x59 x61) ⟶ False) ⟶ (x0 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x59 = x37 x61 ⟶ x2 x60 x23 ⟶ (x35 (x34 x60 x59 x61) ⟶ False) ⟶ (x0 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 . x2 x61 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x59 = x37 x61 ⟶ x2 x60 x23 ⟶ (x2 (x34 x60 x59 x61) (x1 x23) ⟶ False) ⟶ (x0 x60 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 x61 x62 . x2 x62 (x1 x23) ⟶ x2 x59 (x1 x23) ⟶ x59 = x37 x62 ⟶ x2 x60 x23 ⟶ x0 x60 x59 ⟶ x2 x61 (x1 x23) ⟶ x35 x61 ⟶ x3 x62 x61 ⟶ (x0 x60 x61 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x27 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x54 x60 ⟶ x2 x59 (x1 x60) ⟶ (x54 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x56 x59 ⟶ (x54 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x2 x59 x4 ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x54 x60 ⟶ x2 x59 x60 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x54 x60 ⟶ x2 x59 x60 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x56 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x6 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x54 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x11 x59 ⟶ (x11 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x11 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x11 x59 ⟶ (x44 x59 x5 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x11 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x6 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x52 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x8 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x52 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x52 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x11 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x52 x60 ⟶ x2 x59 (x1 x60) ⟶ (x52 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x15 x60 ⟶ x2 x59 x60 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ (x8 x59 ⟶ False) ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ (x8 x59 ⟶ False) ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ (x8 x59 ⟶ False) ⟶ x52 x59 ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x45 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x44 x59 x5 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x58 x60 ⟶ x2 x59 (x1 x60) ⟶ x47 x59 x60 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x28 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x8 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x58 x59 ⟶ (x45 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x58 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ x58 x59 ⟶ (x47 x59 x60 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x2 x59 x23 ⟶ (x45 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x10 x60 ⟶ x49 x60 ⟶ x2 x59 (x1 x60) ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . (x58 x60 ⟶ False) ⟶ x2 x59 (x1 x60) ⟶ (x47 x59 x60 ⟶ False) ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 . x17 x59 ⟶ x41 x59 ⟶ (x15 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x18 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ x10 x59 ⟶ x49 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x13 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x49 x59 ⟶ x45 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x58 x60 ⟶ x2 x59 (x1 x60) ⟶ (x58 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x15 x59 ⟶ (x41 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x15 x59 ⟶ (x17 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x20 x59 ⟶ (x33 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x20 x59 ⟶ (x29 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x20 x59 ⟶ (x32 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x20 x59 ⟶ (x30 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x20 x59 ⟶ x58 x59 ⟶ False) ⟶ (∀ x59 . x58 x59 ⟶ (x49 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x58 x59 ⟶ (x45 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 . x10 x59 ⟶ x58 x59 ⟶ (x10 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x56 x60 ⟶ x2 x59 (x1 x60) ⟶ (x56 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x27 x60 ⟶ x2 x59 (x1 x60) ⟶ (x27 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x56 x60 ⟶ x2 x59 x60 ⟶ (x45 x59 ⟶ False) ⟶ False) ⟶ (∀ x59 x60 . x0 x59 x60 ⟶ x0 x60 x59 ⟶ False) ⟶ (x3 x31 (x37 x31) ⟶ False) ⟶ ((x2 x31 (x1 x23) ⟶ False) ⟶ False) ⟶ False (proof)