Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../8e2ca..
PUbbH../13612..
vout
PrPhD../b5316.. 3.40 bars
TMWTj../fdd8f.. ownership of 54bfa.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMT6D../ccb4a.. ownership of 4381f.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUTeK../13f81.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 54bfa.. : ∀ 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 . x64 x66 ⟶ x64 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x61 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x0 x66 ⟶ (x66 = x65 ⟶ False) ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x61 x66 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x65 x66 ⟶ x0 x66 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x0 x66 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ (x62 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x4 x65 ⟶ (x63 x66 x2 ⟶ False) ⟶ x63 (x3 x66 x65) x2 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x65 = x60 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x1 x65 x66 ⟶ x6 x66 (x5 x67) ⟶ x0 x67 ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x0 x65 ⟶ False) ⟶ (x62 x66 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . x1 x66 x67 ⟶ x6 x67 (x5 x65) ⟶ (x6 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x61 x65 ⟶ False) ⟶ x61 x66 ⟶ False) ⟶ (∀ x65 x66 . x7 x66 x65 ⟶ (x6 x66 (x5 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x6 x66 (x5 x65) ⟶ (x7 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ (x62 x66 ⟶ False) ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 x66 . x6 x65 x66 ⟶ (x0 x66 ⟶ False) ⟶ (x1 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ x62 x65 ⟶ (x62 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x66 x65 ⟶ (x6 x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x64 x65 ⟶ x63 x66 x65 ⟶ x61 x66 ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ ((x6 x60 x59 ⟶ False) ⟶ False) ⟶ ((x6 x9 x8 ⟶ False) ⟶ False) ⟶ ((x6 x9 x58 ⟶ False) ⟶ False) ⟶ ((x10 x9 x8 x58 ⟶ False) ⟶ False) ⟶ ((x0 x9 ⟶ False) ⟶ False) ⟶ ((x63 x9 x9 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x57 x66 ⟶ x57 x65 ⟶ (x63 x66 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x7 x65 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x6 x65 (x5 x67) ⟶ x6 x66 x65 ⟶ (x10 x66 x67 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x6 x65 (x5 x67) ⟶ x10 x66 x67 x65 ⟶ (x6 x66 x65 ⟶ False) ⟶ False) ⟶ ((x2 = x60 ⟶ False) ⟶ False) ⟶ ((x58 = x59 ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x54 x65 = x55 x65 ⟶ False) ⟶ False) ⟶ ((x4 x11 ⟶ False) ⟶ False) ⟶ (x0 x11 ⟶ False) ⟶ ((x57 x12 ⟶ False) ⟶ False) ⟶ ((x0 x12 ⟶ False) ⟶ False) ⟶ ((x64 x13 ⟶ False) ⟶ False) ⟶ ((x57 x13 ⟶ False) ⟶ False) ⟶ ((x14 x13 ⟶ False) ⟶ False) ⟶ ((x0 x13 ⟶ False) ⟶ False) ⟶ ((x4 x15 ⟶ False) ⟶ False) ⟶ ((x62 x53 ⟶ False) ⟶ False) ⟶ ((x57 x53 ⟶ False) ⟶ False) ⟶ ((x64 x52 ⟶ False) ⟶ False) ⟶ ((x62 x52 ⟶ False) ⟶ False) ⟶ ((x57 x52 ⟶ False) ⟶ False) ⟶ ((x14 x52 ⟶ False) ⟶ False) ⟶ ((x51 x50 ⟶ False) ⟶ False) ⟶ ((x16 x50 ⟶ False) ⟶ False) ⟶ (x0 x50 ⟶ False) ⟶ ((x61 x17 ⟶ False) ⟶ False) ⟶ ((x57 x17 ⟶ False) ⟶ False) ⟶ ((x64 x18 ⟶ False) ⟶ False) ⟶ ((x61 x18 ⟶ False) ⟶ False) ⟶ ((x57 x18 ⟶ False) ⟶ False) ⟶ ((x14 x18 ⟶ False) ⟶ False) ⟶ (x0 x19 ⟶ False) ⟶ ((x49 x48 ⟶ False) ⟶ False) ⟶ ((x20 x21 ⟶ False) ⟶ False) ⟶ ((x47 x21 ⟶ False) ⟶ False) ⟶ ((x22 x21 ⟶ False) ⟶ False) ⟶ (x0 x21 ⟶ False) ⟶ ((x20 x23 ⟶ False) ⟶ False) ⟶ (x0 x23 ⟶ False) ⟶ ((x6 x23 (x5 x8) ⟶ False) ⟶ False) ⟶ ((x16 x46 ⟶ False) ⟶ False) ⟶ (x0 x46 ⟶ False) ⟶ ((x56 x45 ⟶ False) ⟶ False) ⟶ ((x57 x24 ⟶ False) ⟶ False) ⟶ ((x64 x44 ⟶ False) ⟶ False) ⟶ ((x0 x25 ⟶ False) ⟶ False) ⟶ ((x49 x43 ⟶ False) ⟶ False) ⟶ ((x64 x43 ⟶ False) ⟶ False) ⟶ ((x14 x43 ⟶ False) ⟶ False) ⟶ ((x57 x43 ⟶ False) ⟶ False) ⟶ ((x6 x43 x8 ⟶ False) ⟶ False) ⟶ ((x20 x26 ⟶ False) ⟶ False) ⟶ ((x16 x42 ⟶ False) ⟶ False) ⟶ (x0 x42 ⟶ False) ⟶ ((x56 x41 ⟶ False) ⟶ False) ⟶ ((x64 x41 ⟶ False) ⟶ False) ⟶ ((x14 x41 ⟶ False) ⟶ False) ⟶ ((x57 x41 ⟶ False) ⟶ False) ⟶ ((x6 x41 x8 ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x54 (x54 x65) = x54 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x14 x65 ⟶ (x55 (x55 x65) = x55 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x14 x65 ⟶ (x27 (x27 x65) = x65 ⟶ False) ⟶ False) ⟶ (x40 x8 ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x49 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ ((x20 x59 ⟶ False) ⟶ False) ⟶ (x0 x59 ⟶ False) ⟶ ((x16 x59 ⟶ False) ⟶ False) ⟶ ((x51 x59 ⟶ False) ⟶ False) ⟶ ((x51 x8 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x64 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x4 x66 ⟶ x4 x65 ⟶ (x4 (x3 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x14 x66 ⟶ x4 x65 ⟶ (x14 (x3 x66 x65) ⟶ False) ⟶ False) ⟶ ((x39 x8 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ x62 (x27 x65) ⟶ False) ⟶ (∀ x65 . (x62 x65 ⟶ False) ⟶ x64 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x56 x65 ⟶ (x64 (x28 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x4 x65 ⟶ (x64 (x3 x66 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x62 x65 ⟶ x64 x65 ⟶ (x62 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x62 x65 ⟶ x64 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ x61 (x27 x65) ⟶ False) ⟶ (∀ x65 . (x61 x65 ⟶ False) ⟶ x64 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x64 x65 ⟶ (x61 (x27 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x61 x65 ⟶ x64 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ ((x0 x60 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x49 (x55 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x64 (x55 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x64 (x55 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x4 (x55 x65) ⟶ False) ⟶ False) ⟶ (x0 x8 ⟶ False) ⟶ (∀ x65 x66 . (x0 x66 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x6 x65 (x5 x66) ⟶ (x10 (x29 x65 x66) x66 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x6 (x38 x65) x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 x67 . (x0 x67 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ x6 x65 (x5 x67) ⟶ x10 x66 x67 x65 ⟶ (x6 x66 x67 ⟶ False) ⟶ False) ⟶ ((x10 x2 x8 x58 ⟶ False) ⟶ False) ⟶ (∀ x65 . x14 x65 ⟶ (x14 (x27 x65) ⟶ False) ⟶ False) ⟶ ((x6 x58 (x5 x8) ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x6 (x54 x65) x58 ⟶ False) ⟶ False) ⟶ (∀ x65 . x14 x65 ⟶ (x64 (x55 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x56 x65 ⟶ (x63 x2 x65 ⟶ False) ⟶ (x28 x66 x65 = x27 (x3 x66 (x54 x65)) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x64 x66 ⟶ x56 x65 ⟶ x63 x2 x65 ⟶ (x28 x66 x65 = x3 x66 (x54 x65) ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x57 x66 ⟶ x57 x65 ⟶ (x63 x66 x65 ⟶ False) ⟶ (x63 x65 x66 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x37 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ (x0 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x6 x65 x59 ⟶ (x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x6 x65 (x5 x8) ⟶ (x39 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x57 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x57 x65 ⟶ x61 x65 ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ x57 x65 ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x57 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x62 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x57 x65 ⟶ (x61 x65 ⟶ False) ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x20 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ x62 x65 ⟶ x61 x65 ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ x62 x65 ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ x62 x65 ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 x66 . x20 x66 ⟶ x6 x65 x66 ⟶ (x20 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x39 x65 ⟶ (x36 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x57 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x61 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . (x0 x65 ⟶ False) ⟶ x57 x65 ⟶ (x62 x65 ⟶ False) ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x35 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x39 x65 ⟶ (x30 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ x61 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ x61 x65 ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x57 x65 ⟶ x61 x65 ⟶ x0 x65 ⟶ False) ⟶ (∀ x65 . x64 x65 ⟶ (x14 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x20 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x31 x65 ⟶ (x39 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x56 x65 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x22 x65 ⟶ x47 x65 ⟶ (x20 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x6 x65 x58 ⟶ x62 x65 ⟶ False) ⟶ (∀ x65 . x34 x65 ⟶ (x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x56 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x51 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x6 x65 x58 ⟶ (x16 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x16 x66 ⟶ x6 x65 (x5 x66) ⟶ (x16 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x34 x66 ⟶ x6 x65 (x5 x66) ⟶ (x34 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x31 x66 ⟶ x6 x65 (x5 x66) ⟶ (x31 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x39 x66 ⟶ x6 x65 (x5 x66) ⟶ (x39 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x30 x66 ⟶ x6 x65 (x5 x66) ⟶ (x30 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x6 x65 x8 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x49 x65 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x20 x65 ⟶ (x47 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x20 x65 ⟶ (x22 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x4 x65 ⟶ (x20 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x16 x65 ⟶ (x34 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x36 x66 ⟶ x6 x65 (x5 x66) ⟶ (x36 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x0 x65 ⟶ (x16 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x16 x66 ⟶ x6 x65 x66 ⟶ (x4 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x34 x66 ⟶ x6 x65 x66 ⟶ (x56 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x31 x66 ⟶ x6 x65 x66 ⟶ (x49 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x39 x66 ⟶ x6 x65 x66 ⟶ (x64 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x30 x66 ⟶ x6 x65 x66 ⟶ (x57 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x36 x66 ⟶ x6 x65 x66 ⟶ (x14 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 . x6 x65 (x5 x58) ⟶ (x16 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x37 x66 ⟶ x6 x65 (x5 x66) ⟶ (x37 x65 ⟶ False) ⟶ False) ⟶ (∀ x65 x66 . x1 x65 x66 ⟶ x1 x66 x65 ⟶ False) ⟶ ((x63 (x28 x33 x32) x2 ⟶ False) ⟶ False) ⟶ (x63 x33 x2 ⟶ False) ⟶ ((x56 x32 ⟶ False) ⟶ False) ⟶ ((x64 x33 ⟶ False) ⟶ False) ⟶ False (proof)