Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../96df6..
PUcC8../1994f..
vout
PrPhD../35d67.. 3.40 bars
TMbT7../00b70.. ownership of 73cf8.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMHZn../9848e.. ownership of ca8ef.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUWKb../27237.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 73cf8.. : ∀ 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 . x52 x54(x54 = x53False)x52 x53False)(∀ x53 x54 . x0 x54x0 x53(x2 x54 = x1False)(x2 x53 = x1False)(x7 (x8 x54 x53) = x6 (x8 (x7 x54) (x7 x53)) (x3 x5 (x4 (x7 x54) (x7 x53)))False)False)(∀ x53 x54 . x51 x53 x54x52 x54False)(∀ x53 . x52 x53(x53 = x9False)False)(∀ x53 . x50 x53(x6 x53 x5 = x53False)False)(∀ x53 x54 x55 . x51 x53 x54x11 x54 (x10 x55)x52 x55False)(∀ x53 . x50 x53(x6 x1 x53 = x1False)False)(∀ x53 x54 x55 . x51 x54 x55x11 x55 (x10 x53)(x11 x54 x53False)False)(∀ x53 . x50 x53(x3 x53 x1 = x53False)False)(∀ x53 x54 . x12 x54 x53(x11 x54 (x10 x53)False)False)(∀ x53 x54 . x11 x54 (x10 x53)(x12 x54 x53False)False)(∀ x53 . x50 x53(x4 x5 x53 = x53False)False)(∀ x53 x54 . x11 x53 x54(x52 x54False)(x51 x53 x54False)False)(∀ x53 . x50 x53(x4 x53 x1 = x1False)False)(∀ x53 x54 . x51 x54 x53(x11 x54 x53False)False)((x11 x9 x13False)False)(∀ x53 . x50 x53(x8 x53 x1 = x53False)False)(∀ x53 x54 . x50 x54x50 x53(x3 (x14 x54) (x14 x53) = x3 x53 x54False)False)(∀ x53 x54 . x50 x54x50 x53(x8 (x14 x54) (x14 x53) = x14 (x8 x54 x53)False)False)(∀ x53 x54 x55 . x50 x55x50 x53x50 x54(x4 (x4 x55 x53) x54 = x4 x55 (x4 x53 x54)False)False)(∀ x53 x54 x55 . x50 x55x50 x53x50 x54(x8 (x8 x55 x53) x54 = x8 x55 (x8 x53 x54)False)False)(∀ x53 x54 x55 . x50 x55x50 x53x50 x54(x4 (x8 x55 x53) x54 = x8 (x4 x55 x54) (x4 x53 x54)False)False)(∀ x53 x54 x55 . x50 x55x50 x53x50 x54(x4 x55 (x6 x53 x54) = x6 (x4 x55 x53) x54False)False)((x11 x16 x15False)False)((x11 x16 x49False)False)((x17 x16 x15 x49False)False)((x48 x16False)False)(x52 x16False)(∀ x53 . x50 x53(x4 x53 (x14 x5) = x14 x53False)False)((x11 x5 x15False)False)((x11 x5 x49False)False)((x17 x5 x15 x49False)False)((x48 x5False)False)(x52 x5False)(∀ x53 x54 . x50 x54x50 x53(x8 x54 (x14 x53) = x3 x54 x53False)False)((x11 x18 x15False)False)((x11 x18 x49False)False)((x17 x18 x15 x49False)False)((x52 x18False)False)((x14 (x6 (x14 x5) x16) = x6 x5 x16False)False)((x14 (x6 x5 x16) = x6 (x14 x5) x16False)False)((x14 (x14 x16) = x16False)False)((x14 (x14 x5) = x5False)False)((x14 x16 = x14 x16False)False)((x14 x5 = x14 x5False)False)((x14 x18 = x18False)False)((x4 (x6 (x14 x5) x16) (x14 x16) = x5False)False)((x4 (x6 (x14 x5) x16) x16 = x14 x5False)False)((x4 (x6 (x14 x5) x16) x5 = x6 (x14 x5) x16False)False)((x4 (x6 x5 x16) (x14 x16) = x14 x5False)False)((x4 (x6 x5 x16) x16 = x5False)False)((x4 (x6 x5 x16) x5 = x6 x5 x16False)False)((x4 (x6 x5 x16) x18 = x18False)False)((x4 (x14 x16) (x6 (x14 x5) x16) = x5False)False)((x4 (x14 x16) (x6 x5 x16) = x14 x5False)False)((x4 (x14 x16) x5 = x14 x16False)False)((x4 (x14 x16) x18 = x18False)False)((x4 x16 (x6 (x14 x5) x16) = x14 x5False)False)((x4 x16 (x6 x5 x16) = x5False)False)((x4 x16 x5 = x16False)False)((x4 x16 x18 = x18False)False)((x4 x5 (x6 (x14 x5) x16) = x6 (x14 x5) x16False)False)((x4 x5 (x6 x5 x16) = x6 x5 x16False)False)((x4 x5 (x14 x16) = x14 x16False)False)((x4 x5 x16 = x16False)False)((x4 x5 x5 = x5False)False)((x4 x5 x18 = x18False)False)((x4 x18 (x6 x5 x16) = x18False)False)((x4 x18 (x14 x16) = x18False)False)((x4 x18 x16 = x18False)False)((x4 x18 x5 = x18False)False)((x4 x18 x18 = x18False)False)((x6 (x14 x16) x16 = x14 x5False)False)((x6 (x14 x5) x16 = x6 (x14 x5) x16False)False)((x6 (x14 x5) x5 = x14 x5False)False)((x6 x16 x16 = x5False)False)((x6 x16 x5 = x16False)False)((x6 x5 (x6 (x14 x5) x16) = x14 x16False)False)((x6 x5 (x6 x5 x16) = x16False)False)((x6 x5 (x14 x16) = x6 (x14 x5) x16False)False)((x6 x5 (x14 x5) = x14 x5False)False)((x6 x5 x16 = x6 x5 x16False)False)((x6 x5 x5 = x5False)False)((x3 (x6 (x14 x5) x16) (x6 (x14 x5) x16) = x18False)False)((x3 (x6 (x14 x5) x16) (x6 x5 x16) = x14 x5False)False)((x3 (x6 (x14 x5) x16) (x14 x5) = x6 x5 x16False)False)((x3 (x6 (x14 x5) x16) x18 = x6 (x14 x5) x16False)False)((x3 (x6 x5 x16) (x6 (x14 x5) x16) = x5False)False)((x3 (x6 x5 x16) (x6 x5 x16) = x18False)False)((x3 (x6 x5 x16) x5 = x6 (x14 x5) x16False)False)((x3 (x6 x5 x16) x18 = x6 x5 x16False)False)((x3 (x14 x16) (x14 x16) = x18False)False)((x3 (x14 x16) (x14 x5) = x14 x5False)False)((x3 (x14 x16) x18 = x14 x16False)False)((x3 (x14 x5) (x6 (x14 x5) x16) = x6 (x14 x5) x16False)False)((x3 (x14 x5) (x14 x16) = x5False)False)((x3 (x14 x5) (x14 x5) = x18False)False)((x3 (x14 x5) x5 = x14 x16False)False)((x3 (x14 x5) x18 = x14 x5False)False)((x3 x16 x16 = x18False)False)((x3 x16 x5 = x5False)False)((x3 x16 x18 = x16False)False)((x3 x5 (x6 x5 x16) = x6 x5 x16False)False)((x3 x5 (x14 x5) = x16False)False)((x3 x5 x16 = x14 x5False)False)((x3 x5 x5 = x18False)False)((x3 x5 x18 = x5False)False)((x3 x18 (x6 (x14 x5) x16) = x6 x5 x16False)False)((x3 x18 (x6 x5 x16) = x6 (x14 x5) x16False)False)((x3 x18 (x14 x16) = x16False)False)((x3 x18 (x14 x5) = x5False)False)((x3 x18 x16 = x14 x16False)False)((x3 x18 x5 = x14 x5False)False)((x3 x18 x18 = x18False)False)((x8 (x6 (x14 x5) x16) (x6 (x14 x5) x16) = x14 x5False)False)((x8 (x6 (x14 x5) x16) (x6 x5 x16) = x18False)False)((x8 (x6 (x14 x5) x16) x5 = x6 x5 x16False)False)((x8 (x6 x5 x16) (x6 (x14 x5) x16) = x18False)False)((x8 (x6 x5 x16) (x6 x5 x16) = x5False)False)((x8 (x6 x5 x16) (x14 x5) = x6 (x14 x5) x16False)False)((x8 (x6 x5 x16) x18 = x6 x5 x16False)False)((x8 (x14 x16) x16 = x18False)False)((x8 (x14 x16) x5 = x14 x5False)False)((x8 (x14 x5) (x6 x5 x16) = x6 (x14 x5) x16False)False)((x8 (x14 x5) (x14 x5) = x14 x16False)False)((x8 (x14 x5) x16 = x5False)False)((x8 (x14 x5) x5 = x18False)False)((x8 (x14 x5) x18 = x14 x5False)False)((x8 x16 (x14 x16) = x18False)False)((x8 x16 (x14 x5) = x5False)False)((x8 x16 x18 = x16False)False)((x8 x5 (x6 (x14 x5) x16) = x6 x5 x16False)False)((x8 x5 (x14 x16) = x14 x5False)False)((x8 x5 (x14 x5) = x18False)False)((x8 x5 x5 = x16False)False)((x8 x5 x18 = x5False)False)((x8 x18 (x6 (x14 x5) x16) = x6 (x14 x5) x16False)False)((x8 x18 (x6 x5 x16) = x6 x5 x16False)False)((x8 x18 (x14 x16) = x14 x16False)False)((x8 x18 (x14 x5) = x14 x5False)False)((x8 x18 x16 = x16False)False)((x8 x18 x5 = x5False)False)((x8 x18 x18 = x18False)False)(∀ x53 . (x12 x53 x53False)False)(∀ x53 x54 x55 . (x52 x55False)(x52 x53False)x11 x53 (x10 x55)x11 x54 x53(x17 x54 x55 x53False)False)(∀ x53 x54 x55 . (x52 x55False)(x52 x53False)x11 x53 (x10 x55)x17 x54 x55 x53(x11 x54 x53False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x47 x54 x53 = x3 x54 x53False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x19 x54 x53 = x4 x54 x53False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x46 x54 x53 = x8 x54 x53False)False)((x1 = x9False)False)(∀ x53 . x11 x53 x15(x45 x53 = x44 x53False)False)((x49 = x13False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x43 x54 x53 = x6 x54 x53False)False)((x0 x20False)False)((x42 x20False)False)((x50 x20False)False)((x52 x20False)False)((x0 x21False)False)((x41 x21False)False)((x42 x21False)False)((x50 x21False)False)((x22 x23False)False)((x40 x23False)False)(x52 x23False)((x0 x39False)False)((x48 x39False)False)((x42 x39False)False)((x50 x39False)False)((x40 x38False)False)(x52 x38False)((x0 x37False)False)((x40 x24False)False)(x52 x24False)(∀ x53 . x50 x53(x14 (x14 x53) = x53False)False)(∀ x53 x54 . (x41 x54False)x0 x54(x41 x53False)x0 x53x41 (x8 x54 x53)False)(∀ x53 x54 . x0 x54x0 x53(x0 (x6 x54 x53)False)False)(∀ x53 x54 . x0 x54x0 x53(x0 (x3 x54 x53)False)False)(∀ x53 x54 . x0 x54x0 x53(x0 (x4 x54 x53)False)False)((x40 x13False)False)(∀ x53 x54 . x0 x54x0 x53(x0 (x8 x54 x53)False)False)((x22 x13False)False)((x22 x15False)False)(∀ x53 . x0 x53(x0 (x2 x53)False)False)(∀ x53 . x0 x53(x0 (x14 x53)False)False)(∀ x53 . x0 x53(x50 (x14 x53)False)False)(∀ x53 . x0 x53(x0 (x25 x53)False)False)((x36 x15False)False)(∀ x53 x54 . (x48 x54False)x0 x54(x48 x53False)x0 x53x41 (x6 x54 x53)False)(∀ x53 x54 . (x41 x54False)x0 x54(x41 x53False)x0 x53x41 (x6 x54 x53)False)(∀ x53 x54 . (x41 x54False)x0 x54(x48 x53False)x0 x53x48 (x6 x53 x54)False)(∀ x53 x54 . (x41 x54False)x0 x54(x48 x53False)x0 x53x48 (x6 x54 x53)False)(∀ x53 . x0 x53(x0 (x44 x53)False)False)(∀ x53 x54 . (x41 x54False)x0 x54(x41 x53False)x0 x53x41 (x4 x54 x53)False)(∀ x53 x54 . (x48 x54False)x0 x54(x48 x53False)x0 x53x41 (x4 x54 x53)False)(∀ x53 x54 . (x48 x54False)x0 x54(x41 x53False)x0 x53x48 (x4 x53 x54)False)(∀ x53 x54 . (x48 x54False)x0 x54(x41 x53False)x0 x53x48 (x4 x54 x53)False)(∀ x53 x54 . x41 x54x0 x54(x41 x53False)x0 x53(x48 (x3 x53 x54)False)False)(∀ x53 x54 . x41 x54x0 x54(x41 x53False)x0 x53(x41 (x3 x54 x53)False)False)(∀ x53 x54 . x48 x54x0 x54(x48 x53False)x0 x53(x41 (x3 x53 x54)False)False)(∀ x53 . x50 x53(x50 (x44 x53)False)False)(∀ x53 x54 . x48 x54x0 x54(x48 x53False)x0 x53(x48 (x3 x54 x53)False)False)(∀ x53 x54 . (x41 x54False)x0 x54(x48 x53False)x0 x53x48 (x3 x53 x54)False)(∀ x53 x54 . (x41 x54False)x0 x54(x48 x53False)x0 x53x41 (x3 x54 x53)False)(∀ x53 . (x41 x53False)x0 x53x48 (x14 x53)False)(∀ x53 . (x41 x53False)x0 x53(x50 (x14 x53)False)False)(∀ x53 . (x48 x53False)x0 x53x41 (x14 x53)False)(∀ x53 . (x48 x53False)x0 x53(x50 (x14 x53)False)False)(∀ x53 x54 . x41 x54x0 x54(x48 x53False)x0 x53(x41 (x8 x53 x54)False)False)(∀ x53 x54 . x41 x54x0 x54(x48 x53False)x0 x53(x41 (x8 x54 x53)False)False)(∀ x53 x54 . x48 x54x0 x54(x41 x53False)x0 x53(x48 (x8 x53 x54)False)False)(∀ x53 x54 . x48 x54x0 x54(x41 x53False)x0 x53(x48 (x8 x54 x53)False)False)(∀ x53 x54 . (x48 x54False)x0 x54(x48 x53False)x0 x53x48 (x8 x54 x53)False)(∀ x53 x54 . (x52 x54False)(x52 x53False)x11 x53 (x10 x54)(x17 (x35 x53 x54) x54 x53False)False)(∀ x53 . (x11 (x26 x53) x53False)False)(∀ x53 x54 x55 . (x52 x55False)(x52 x53False)x11 x53 (x10 x55)x17 x54 x55 x53(x11 x54 x55False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x11 (x47 x54 x53) x15False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x11 (x19 x54 x53) x15False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x11 (x46 x54 x53) x15False)False)((x17 x1 x15 x49False)False)(∀ x53 . x11 x53 x15(x11 (x45 x53) x15False)False)((x11 x49 (x10 x15)False)False)(∀ x53 . x50 x53(x50 (x14 x53)False)False)(∀ x53 . x0 x53(x11 (x7 x53) x15False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x11 (x43 x54 x53) x15False)False)(∀ x53 . x50 x53(x44 x53 = x4 x53 x53False)False)(∀ x53 . x0 x53(x7 x53 = x6 (x25 x53) (x2 x53)False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x19 x54 x53 = x19 x53 x54False)False)(∀ x53 x54 . x11 x54 x15x0 x53(x46 x54 x53 = x46 x53 x54False)False)(∀ x53 x54 . x50 x54x50 x53(x4 x54 x53 = x4 x53 x54False)False)(∀ x53 x54 . x50 x54x50 x53(x8 x54 x53 = x8 x53 x54False)False)(∀ x53 . x11 x53 (x10 x15)(x36 x53False)False)(∀ x53 . x36 x53(x27 x53False)False)(∀ x53 . x0 x53(x42 x53False)False)(∀ x53 . x36 x53(x28 x53False)False)(∀ x53 . x0 x53(x50 x53False)False)(∀ x53 . x29 x53(x36 x53False)False)(∀ x53 . x34 x53(x0 x53False)False)(∀ x53 . x30 x53(x29 x53False)False)(∀ x53 . x52 x53(x22 x53False)False)(∀ x53 . x11 x53 x49(x40 x53False)False)(∀ x53 x54 . x40 x54x11 x53 (x10 x54)(x40 x53False)False)(∀ x53 x54 . x30 x54x11 x53 (x10 x54)(x30 x53False)False)(∀ x53 x54 . x29 x54x11 x53 (x10 x54)(x29 x53False)False)(∀ x53 x54 . x36 x54x11 x53 (x10 x54)(x36 x53False)False)(∀ x53 x54 . x28 x54x11 x53 (x10 x54)(x28 x53False)False)(∀ x53 . x11 x53 x15(x0 x53False)False)(∀ x53 . x40 x53(x30 x53False)False)(∀ x53 x54 . x27 x54x11 x53 (x10 x54)(x27 x53False)False)(∀ x53 . x52 x53(x40 x53False)False)(∀ x53 x54 . x40 x54x11 x53 x54(x34 x53False)False)(∀ x53 x54 . x30 x54x11 x53 x54(x33 x53False)False)(∀ x53 x54 . x29 x54x11 x53 x54(x31 x53False)False)(∀ x53 x54 . x36 x54x11 x53 x54(x0 x53False)False)(∀ x53 x54 . x28 x54x11 x53 x54(x42 x53False)False)(∀ x53 x54 . x27 x54x11 x53 x54(x50 x53False)False)(∀ x53 . x11 x53 (x10 x49)(x40 x53False)False)(∀ x53 x54 . x51 x53 x54x51 x54 x53False)(x7 (x19 x16 x32) = x43 (x19 x16 (x7 x32)) (x47 x5 (x45 (x7 x32)))False)(x2 x32 = x1False)((x0 x32False)False)False (proof)