Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../f9cf7..
PULP7../9ea7b..
vout
PrNUD../4e540.. 0.04 bars
TMJq1../fbaa3.. ownership of 7caba.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMLtj../548a3.. ownership of 941d9.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUSVJ../a3d63.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7caba.. : ∀ 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 . x47 x49 ⟶ (x49 = x48 ⟶ False) ⟶ x47 x48 ⟶ False) ⟶ (∀ x48 x49 . x0 x48 x49 ⟶ x47 x49 ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x48 = x46 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x48 x49 ⟶ x2 x49 (x1 x50) ⟶ x47 x50 ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x49 x50 ⟶ x2 x50 (x1 x48) ⟶ (x2 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x3 x49 x48 ⟶ (x2 x49 (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x2 x49 (x1 x48) ⟶ (x3 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x2 x48 x49 ⟶ (x47 x49 ⟶ False) ⟶ (x0 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x48 ⟶ (x2 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x4 x51 ⟶ x9 x51 x48 x49 ⟶ x2 x51 (x1 (x5 x48 x49)) ⟶ x4 x50 ⟶ x9 x50 x48 x49 ⟶ x2 x50 (x1 (x5 x48 x49)) ⟶ x6 x51 (x7 x50 x51 x49 x48) = x6 x50 (x7 x50 x51 x49 x48) ⟶ (x8 x48 x49 x51 x50 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x4 x51 ⟶ x9 x51 x48 x49 ⟶ x2 x51 (x1 (x5 x48 x49)) ⟶ x4 x50 ⟶ x9 x50 x48 x49 ⟶ x2 x50 (x1 (x5 x48 x49)) ⟶ (x0 (x7 x50 x51 x49 x48) x48 ⟶ False) ⟶ (x8 x48 x49 x51 x50 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x2 x51 (x1 (x5 x50 x49)) ⟶ x2 x48 (x1 (x5 x50 x49)) ⟶ x8 x50 x49 x51 x48 ⟶ (x8 x50 x49 x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x4 x51 ⟶ x9 x51 x48 x49 ⟶ x2 x51 (x1 (x5 x48 x49)) ⟶ x4 x50 ⟶ x9 x50 x48 x49 ⟶ x2 x50 (x1 (x5 x48 x49)) ⟶ x45 x48 x49 x51 x50 ⟶ (x45 x48 x49 x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x2 x51 (x1 (x5 x50 x49)) ⟶ x2 x48 (x1 (x5 x50 x49)) ⟶ (x8 x50 x49 x51 x51 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x4 x51 ⟶ x9 x51 x48 x49 ⟶ x2 x51 (x1 (x5 x48 x49)) ⟶ x4 x50 ⟶ x9 x50 x48 x49 ⟶ x2 x50 (x1 (x5 x48 x49)) ⟶ (x45 x48 x49 x51 x51 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x3 x48 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x2 x51 (x1 (x5 x50 x49)) ⟶ x2 x48 (x1 (x5 x50 x49)) ⟶ x51 = x48 ⟶ (x8 x50 x49 x51 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x2 x51 (x1 (x5 x50 x49)) ⟶ x2 x48 (x1 (x5 x50 x49)) ⟶ x8 x50 x49 x51 x48 ⟶ (x51 = x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x4 x51 ⟶ x9 x51 x48 x49 ⟶ x2 x51 (x1 (x5 x48 x49)) ⟶ x4 x50 ⟶ x9 x50 x48 x49 ⟶ x2 x50 (x1 (x5 x48 x49)) ⟶ x51 = x50 ⟶ (x45 x48 x49 x51 x50 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x4 x51 ⟶ x9 x51 x48 x49 ⟶ x2 x51 (x1 (x5 x48 x49)) ⟶ x4 x50 ⟶ x9 x50 x48 x49 ⟶ x2 x50 (x1 (x5 x48 x49)) ⟶ x45 x48 x49 x51 x50 ⟶ (x51 = x50 ⟶ False) ⟶ False) ⟶ ((x44 x43 ⟶ False) ⟶ False) ⟶ (x47 x43 ⟶ False) ⟶ (∀ x48 . (x42 x48 ⟶ False) ⟶ x42 (x41 x48) ⟶ False) ⟶ (∀ x48 . (x42 x48 ⟶ False) ⟶ (x2 (x41 x48) (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x4 (x40 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x10 (x40 x48 x49) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x39 (x40 x49 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x11 (x40 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ (x42 (x38 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ x47 (x38 x48) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ (x2 (x38 x48) (x1 x48) ⟶ False) ⟶ False) ⟶ (x12 x13 ⟶ False) ⟶ ((x4 x13 ⟶ False) ⟶ False) ⟶ ((x11 x13 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ (x36 (x37 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ (x2 (x37 x48) (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . x36 (x35 x48) x48 ⟶ False) ⟶ (∀ x48 . (x2 (x35 x48) (x1 x48) ⟶ False) ⟶ False) ⟶ (x47 x34 ⟶ False) ⟶ (∀ x48 . (x47 (x14 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x2 (x14 x48) (x1 x48) ⟶ False) ⟶ False) ⟶ ((x15 x16 ⟶ False) ⟶ False) ⟶ ((x4 x16 ⟶ False) ⟶ False) ⟶ ((x11 x16 ⟶ False) ⟶ False) ⟶ ((x47 x33 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ x47 (x17 x48) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ (x2 (x17 x48) (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x10 (x18 x48 x49) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x39 (x18 x49 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x11 (x18 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x47 (x18 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x2 (x18 x48 x49) (x1 (x5 x49 x48)) ⟶ False) ⟶ False) ⟶ ((x4 x32 ⟶ False) ⟶ False) ⟶ ((x11 x32 ⟶ False) ⟶ False) ⟶ ((x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 (x1 x48) ⟶ False) ⟶ (∀ x48 x49 x50 . x44 x50 ⟶ x11 x48 ⟶ x10 x48 x50 ⟶ x4 x48 ⟶ (x4 (x6 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x44 x50 ⟶ x11 x48 ⟶ x10 x48 x50 ⟶ x4 x48 ⟶ (x11 (x6 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x47 x49 ⟶ False) ⟶ (x47 x48 ⟶ False) ⟶ x47 (x5 x49 x48) ⟶ False) ⟶ (∀ x48 . (x2 (x19 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . (x31 x48 x49 x50 = x28 (x29 x48 x49 x50) (x30 x48 x49 x50) ⟶ False) ⟶ (x0 (x31 x48 x49 x50) x48 ⟶ False) ⟶ (x48 = x5 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . (x0 (x30 x48 x49 x50) x49 ⟶ False) ⟶ (x0 (x31 x48 x49 x50) x48 ⟶ False) ⟶ (x48 = x5 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . (x0 (x29 x48 x49 x50) x50 ⟶ False) ⟶ (x0 (x31 x48 x49 x50) x48 ⟶ False) ⟶ (x48 = x5 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 x52 . x0 (x31 x52 x50 x51) x52 ⟶ x0 x48 x51 ⟶ x0 x49 x50 ⟶ x31 x52 x50 x51 = x28 x48 x49 ⟶ (x52 = x5 x51 x50 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 x52 x53 . x53 = x5 x51 x52 ⟶ x0 x48 x51 ⟶ x0 x50 x52 ⟶ x49 = x28 x48 x50 ⟶ (x0 x49 x53 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x51 = x5 x49 x50 ⟶ x0 x48 x51 ⟶ (x48 = x28 (x21 x48 x51 x50 x49) (x20 x48 x51 x50 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x51 = x5 x49 x50 ⟶ x0 x48 x51 ⟶ (x0 (x20 x48 x51 x50 x49) x50 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x51 = x5 x49 x50 ⟶ x0 x48 x51 ⟶ (x0 (x21 x48 x51 x50 x49) x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x11 x50 ⟶ x4 x50 ⟶ (x27 x50 x48 x49 = x6 x50 (x28 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x44 x49 ⟶ x2 x48 (x1 x49) ⟶ (x44 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x44 x49 ⟶ x2 x48 x49 ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x44 x49 ⟶ x2 x48 x49 ⟶ (x11 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x44 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x42 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x12 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x42 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x42 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x11 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x42 x49 ⟶ x2 x48 (x1 x49) ⟶ (x42 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x11 x48 ⟶ x4 x48 ⟶ (x12 x48 ⟶ False) ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x11 x48 ⟶ x4 x48 ⟶ (x12 x48 ⟶ False) ⟶ (x11 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x11 x48 ⟶ x4 x48 ⟶ (x12 x48 ⟶ False) ⟶ x42 x48 ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x2 x48 (x1 x49) ⟶ x36 x48 x49 ⟶ False) ⟶ (∀ x48 x49 x50 . x47 x50 ⟶ x2 x48 (x1 (x5 x49 x50)) ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x12 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x11 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x47 x49 ⟶ False) ⟶ x2 x48 (x1 x49) ⟶ x47 x48 ⟶ (x36 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x47 x50 ⟶ x2 x48 (x1 (x5 x50 x49)) ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x11 x49 ⟶ x4 x49 ⟶ x2 x48 (x1 x49) ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x47 x49 ⟶ False) ⟶ x2 x48 (x1 x49) ⟶ (x36 x48 x49 ⟶ False) ⟶ x47 x48 ⟶ False) ⟶ (∀ x48 x49 x50 . x2 x50 (x1 (x5 x48 x49)) ⟶ (x10 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x2 x50 (x1 (x5 x49 x48)) ⟶ (x39 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x15 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x11 x48 ⟶ x4 x48 ⟶ (x11 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x47 x49 ⟶ x2 x48 (x1 x49) ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x2 x50 (x1 (x5 x48 x49)) ⟶ (x11 x50 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x48 x49 ⟶ x0 x49 x48 ⟶ False) ⟶ (x45 (x5 x22 x23) x26 x25 x24 ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x22 ⟶ x0 x48 x23 ⟶ (x27 x25 x49 x48 = x27 x24 x49 x48 ⟶ False) ⟶ False) ⟶ ((x2 x24 (x1 (x5 (x5 x22 x23) x26)) ⟶ False) ⟶ False) ⟶ ((x9 x24 (x5 x22 x23) x26 ⟶ False) ⟶ False) ⟶ ((x4 x24 ⟶ False) ⟶ False) ⟶ ((x2 x25 (x1 (x5 (x5 x22 x23) x26)) ⟶ False) ⟶ False) ⟶ ((x9 x25 (x5 x22 x23) x26 ⟶ False) ⟶ False) ⟶ ((x4 x25 ⟶ False) ⟶ False) ⟶ False (proof)