Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../3e5f9..
PUM6e../4c645..
vout
PrPhD../3e060.. 102.61 bars
TMdUX../2ac34.. ownership of 1a212.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMSUb../8afc4.. ownership of 10bcb.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUQ9Q../d96ba.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 1a212.. : ∀ 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 : ι → ι . ((x45 (x45 x44) = x44False)False)((x45 x44 = x45 x44False)False)((x42 x44 x43False)False)((x42 x44 x0False)False)((x41 x44 x43 x0False)False)((x1 x44False)False)(x40 x44False)(∀ x46 x47 . x2 x47x2 x46(x3 (x45 x47) (x45 x46) = x3 x46 x47False)False)(∀ x46 x47 . x2 x47x2 x46(x39 (x45 x47) (x45 x46) = x45 (x39 x47 x46)False)False)(∀ x46 x47 x48 . x2 x48x2 x46x2 x47(x39 (x39 x48 x46) x47 = x39 x48 (x39 x46 x47)False)False)(∀ x46 x47 . x2 x47x2 x46(x39 x47 (x45 x46) = x3 x47 x46False)False)((x2 x4False)False)(∀ x46 x47 . x2 x47x2 x46(x2 (x3 x47 x46)False)False)(∀ x46 x47 . x2 x47x2 x46(x2 (x39 x47 x46)False)False)(∀ x46 . x2 x46(x2 (x45 x46)False)False)(∀ x46 . x2 x46(x45 (x45 x46) = x46False)False)(∀ x46 x47 . x2 x47x2 x46(x39 x47 x46 = x39 x46 x47False)False)(∀ x46 x47 . x40 x47(x47 = x46False)x40 x46False)(∀ x46 x47 . x38 x46 x47x40 x47False)(∀ x46 . x40 x46(x46 = x5False)False)(∀ x46 x47 . x42 x46 x47(x40 x47False)(x38 x46 x47False)False)((x2 x6False)False)(x40 x6False)(x40 x7False)((x40 x37False)False)(∀ x46 . (x40 x46False)x2 x46(x2 (x45 x46)False)False)(∀ x46 . (x40 x46False)x2 x46x40 (x45 x46)False)(∀ x46 . x40 x46(x8 x46False)False)(∀ x46 . x40 x46(x36 x46False)False)(∀ x46 . x40 x46(x9 x46False)False)(∀ x46 . x40 x46(x35 x46False)False)(∀ x46 . x42 x46 x43(x10 x46False)False)(∀ x46 . x42 x46 x43(x2 x46False)False)(∀ x46 x47 x48 . (x40 x48False)(x40 x46False)x42 x46 (x11 x48)x41 x47 x48 x46(x42 x47 x48False)False)((x42 x0 (x11 x43)False)False)(∀ x46 x47 x48 . (x40 x48False)(x40 x46False)x42 x46 (x11 x48)x42 x47 x46(x41 x47 x48 x46False)False)(∀ x46 x47 x48 . (x40 x48False)(x40 x46False)x42 x46 (x11 x48)x41 x47 x48 x46(x42 x47 x46False)False)((x0 = x12False)False)(∀ x46 x47 . (x40 x47False)(x40 x46False)x42 x46 (x11 x47)(x41 (x34 x46 x47) x47 x46False)False)(∀ x46 . (x42 (x13 x46) x46False)False)(∀ x46 x47 x48 . x38 x46 x47x42 x47 (x11 x48)x40 x48False)(∀ x46 x47 x48 . x38 x47 x48x42 x48 (x11 x46)(x42 x47 x46False)False)(∀ x46 x47 . x33 x47 x46(x42 x47 (x11 x46)False)False)(∀ x46 x47 . x42 x47 (x11 x46)(x33 x47 x46False)False)(∀ x46 x47 . x38 x47 x46(x42 x47 x46False)False)((x42 x5 x12False)False)((x36 x32False)False)(x40 x32False)((x36 x31False)False)((x10 x14False)False)((x35 x30False)False)(∀ x46 x47 . x10 x47x10 x46(x10 (x3 x47 x46)False)False)((x35 x12False)False)(x40 x12False)(∀ x46 x47 . x10 x47x10 x46(x10 (x39 x47 x46)False)False)(∀ x46 . x10 x46(x10 (x45 x46)False)False)(∀ x46 . x10 x46(x2 (x45 x46)False)False)(∀ x46 x47 . x1 x47x10 x47(x1 x46False)x10 x46(x15 (x3 x46 x47)False)False)((x40 x5False)False)(∀ x46 x47 . x1 x47x10 x47(x1 x46False)x10 x46(x1 (x3 x47 x46)False)False)(∀ x46 . (x1 x46False)x10 x46x15 (x45 x46)False)(∀ x46 . (x1 x46False)x10 x46(x2 (x45 x46)False)False)(∀ x46 x47 . (x1 x47False)x10 x47(x1 x46False)x10 x46x1 (x39 x47 x46)False)(∀ x46 . x42 x46 x12(x36 x46False)False)(∀ x46 . x36 x46(x35 x46False)False)(∀ x46 x47 . x35 x47x42 x46 x47(x35 x46False)False)(∀ x46 . x10 x46(x29 x46False)False)(∀ x46 . x10 x46(x2 x46False)False)(∀ x46 . x36 x46(x29 x46False)False)(∀ x46 . x36 x46(x10 x46False)False)(∀ x46 . x36 x46(x2 x46False)False)(∀ x46 . x35 x46(x16 x46False)False)(∀ x46 . x35 x46(x28 x46False)False)(∀ x46 x47 . x8 x47x42 x46 (x11 x47)(x8 x46False)False)(∀ x46 x47 . x38 x46 x47x38 x47 x46False)((x29 x17False)False)((x40 x17False)False)((x10 x18False)False)((x29 x18False)False)((x2 x18False)False)((x40 x18False)False)((x15 x19False)False)((x29 x19False)False)((x10 x20False)False)((x15 x20False)False)((x29 x20False)False)((x2 x20False)False)((x1 x21False)False)((x29 x21False)False)((x10 x22False)False)((x1 x22False)False)((x29 x22False)False)((x2 x22False)False)((x35 x23False)False)((x16 x23False)False)((x28 x23False)False)(x40 x23False)((x29 x24False)False)(∀ x46 x47 . (x15 x47False)x10 x47(x15 x46False)x10 x46x15 (x39 x47 x46)False)(∀ x46 x47 . x15 x47x10 x47(x15 x46False)x10 x46(x1 (x3 x46 x47)False)False)(∀ x46 x47 . x15 x47x10 x47(x15 x46False)x10 x46(x15 (x3 x47 x46)False)False)(∀ x46 x47 . (x15 x47False)x10 x47(x1 x46False)x10 x46x1 (x3 x46 x47)False)(∀ x46 x47 . (x15 x47False)x10 x47(x1 x46False)x10 x46x15 (x3 x47 x46)False)(∀ x46 . (x15 x46False)x10 x46x1 (x45 x46)False)(∀ x46 . (x15 x46False)x10 x46(x2 (x45 x46)False)False)(∀ x46 x47 . x15 x47x10 x47(x1 x46False)x10 x46(x15 (x39 x46 x47)False)False)(∀ x46 x47 . x15 x47x10 x47(x1 x46False)x10 x46(x15 (x39 x47 x46)False)False)(∀ x46 x47 . x1 x47x10 x47(x15 x46False)x10 x46(x1 (x39 x46 x47)False)False)(∀ x46 x47 . x1 x47x10 x47(x15 x46False)x10 x46(x1 (x39 x47 x46)False)False)(∀ x46 . x29 x46(x1 x46False)(x15 x46False)(x29 x46False)False)(∀ x46 . x29 x46(x1 x46False)(x15 x46False)(x40 x46False)False)(∀ x46 . x40 x46x29 x46x15 x46False)(∀ x46 . x40 x46x29 x46x1 x46False)(∀ x46 . x40 x46x29 x46(x29 x46False)False)(∀ x46 . (x40 x46False)x29 x46(x1 x46False)(x15 x46False)False)(∀ x46 . (x40 x46False)x29 x46(x1 x46False)(x29 x46False)False)(∀ x46 . x29 x46x15 x46x1 x46False)(∀ x46 . x29 x46x15 x46(x29 x46False)False)(∀ x46 . x29 x46x15 x46x40 x46False)(∀ x46 . (x40 x46False)x29 x46(x15 x46False)(x1 x46False)False)(∀ x46 . (x40 x46False)x29 x46(x15 x46False)(x29 x46False)False)(∀ x46 . x29 x46x1 x46x15 x46False)(∀ x46 . x29 x46x1 x46(x29 x46False)False)(∀ x46 . x29 x46x1 x46x40 x46False)(∀ x46 . x28 x46x16 x46(x35 x46False)False)(∀ x46 . (x33 x46 x46False)False)(x3 x25 (x3 (x45 x26) x27) = x39 (x39 x25 x26) x27False)((x2 x27False)False)((x2 x26False)False)((x2 x25False)False)False (proof)