Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../b05c8..
PUQzx../9a541..
vout
PrPhD../5a3d9.. 102.64 bars
TMSJk../a3fd1.. ownership of 7a175.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMdYy../d2fb4.. ownership of ad025.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PULVD../24d88.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 7a175.. : ∀ 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 x50 x51 . x3 x51 ⟶ x16 x51 ⟶ x4 x51 ⟶ x15 x51 ⟶ x5 x51 ⟶ x14 x51 ⟶ x6 x51 ⟶ x13 x51 ⟶ x2 x50 (x7 x51) ⟶ x2 x48 (x12 x51) ⟶ x2 x49 (x12 x51) ⟶ (x11 x51 x50 x48 ⟶ False) ⟶ (x11 x51 x50 x49 ⟶ False) ⟶ (x10 (x7 x51) (x9 x51 x48 x49 x50) = x8 x51 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x45 x49 x48 ⟶ (x2 x49 (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x2 x49 (x1 x48) ⟶ (x45 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x49 x50 ⟶ x0 x48 x50 ⟶ x0 x48 (x44 x50 x49) ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x48 ⟶ (x0 (x44 x48 x49) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x2 x48 x49 ⟶ (x47 x49 ⟶ False) ⟶ (x0 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 x52 x53 x54 x55 . x3 x55 ⟶ x16 x55 ⟶ x4 x55 ⟶ x15 x55 ⟶ x5 x55 ⟶ x14 x55 ⟶ x6 x55 ⟶ x13 x55 ⟶ x2 x54 (x7 x55) ⟶ x2 x48 (x12 x55) ⟶ x2 x53 (x12 x55) ⟶ x2 x49 (x7 x55) ⟶ x2 x52 (x7 x55) ⟶ x2 x50 (x7 x55) ⟶ x2 x51 (x7 x55) ⟶ x11 x55 x49 x48 ⟶ x11 x55 x52 x48 ⟶ x17 (x9 x55 x48 x53 x54) x49 = x50 ⟶ x17 (x9 x55 x48 x53 x54) x52 = x51 ⟶ x50 = x51 ⟶ (x11 x55 x54 x48 ⟶ False) ⟶ (x11 x55 x54 x53 ⟶ False) ⟶ (x49 = x52 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x48 ⟶ (x2 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 x52 . x3 x52 ⟶ x16 x52 ⟶ x4 x52 ⟶ x15 x52 ⟶ x5 x52 ⟶ x14 x52 ⟶ x6 x52 ⟶ x13 x52 ⟶ x2 x51 (x7 x52) ⟶ x2 x48 (x7 x52) ⟶ x2 x50 (x12 x52) ⟶ x2 x49 (x12 x52) ⟶ x11 x52 x48 x50 ⟶ (x11 x52 x51 x50 ⟶ False) ⟶ (x11 x52 x51 x49 ⟶ False) ⟶ (x2 (x17 (x9 x52 x50 x49 x51) x48) (x7 x52) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x45 x48 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x18 x49 ⟶ x20 x49 x48 ⟶ (x10 x48 x49 = x19 x49 ⟶ False) ⟶ False) ⟶ ((x43 x42 ⟶ False) ⟶ False) ⟶ (x47 x42 ⟶ False) ⟶ (∀ x48 x49 . (x41 (x40 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x21 (x40 x48 x49) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x20 (x40 x49 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x18 (x40 x48 x49) ⟶ False) ⟶ False) ⟶ (x39 x38 ⟶ False) ⟶ ((x41 x38 ⟶ False) ⟶ False) ⟶ ((x18 x38 ⟶ False) ⟶ False) ⟶ ((x22 x23 ⟶ False) ⟶ False) ⟶ ((x41 x23 ⟶ False) ⟶ False) ⟶ ((x18 x23 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x21 (x37 x48 x49) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x20 (x37 x49 x48) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x18 (x37 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x47 (x37 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . (x2 (x37 x48 x49) (x1 (x36 x49 x48)) ⟶ False) ⟶ False) ⟶ ((x41 x24 ⟶ False) ⟶ False) ⟶ ((x18 x24 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x3 x51 ⟶ x16 x51 ⟶ x4 x51 ⟶ x15 x51 ⟶ x5 x51 ⟶ x13 x51 ⟶ x2 x50 (x12 x51) ⟶ x2 x48 (x7 x51) ⟶ x49 = x48 ⟶ x11 x51 x48 x50 ⟶ (x0 x49 (x25 x51 x50) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x3 x50 ⟶ x16 x50 ⟶ x4 x50 ⟶ x15 x50 ⟶ x5 x50 ⟶ x13 x50 ⟶ x2 x49 (x12 x50) ⟶ x0 x48 (x25 x50 x49) ⟶ (x11 x50 (x35 x49 x50 x48) x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x3 x50 ⟶ x16 x50 ⟶ x4 x50 ⟶ x15 x50 ⟶ x5 x50 ⟶ x13 x50 ⟶ x2 x49 (x12 x50) ⟶ x0 x48 (x25 x50 x49) ⟶ (x48 = x35 x49 x50 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x3 x50 ⟶ x16 x50 ⟶ x4 x50 ⟶ x15 x50 ⟶ x5 x50 ⟶ x13 x50 ⟶ x2 x49 (x12 x50) ⟶ x0 x48 (x25 x50 x49) ⟶ (x2 (x35 x49 x50 x48) (x7 x50) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x2 x51 (x1 (x36 (x36 x49 x48) x50)) ⟶ (x18 (x19 x51) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x34 x48 ⟶ False) ⟶ x18 x48 ⟶ x41 x48 ⟶ x34 (x19 x48) ⟶ False) ⟶ (∀ x48 x49 x50 . x43 x50 ⟶ x18 x48 ⟶ x21 x48 x50 ⟶ x41 x48 ⟶ (x41 (x17 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x43 x50 ⟶ x18 x48 ⟶ x21 x48 x50 ⟶ x41 x48 ⟶ (x18 (x17 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 . (x2 (x26 x48) x48 ⟶ False) ⟶ False) ⟶ ((x13 x33 ⟶ False) ⟶ False) ⟶ (∀ x48 . x13 x48 ⟶ x47 (x12 x48) ⟶ False) ⟶ (∀ x48 . x13 x48 ⟶ x47 (x7 x48) ⟶ False) ⟶ (∀ x48 x49 . x18 x49 ⟶ x20 x49 x48 ⟶ (x2 (x10 x48 x49) (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x3 x49 ⟶ x16 x49 ⟶ x4 x49 ⟶ x15 x49 ⟶ x5 x49 ⟶ x13 x49 ⟶ x2 x48 (x12 x49) ⟶ (x2 (x8 x49 x48) (x1 (x7 x49)) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x3 x51 ⟶ x16 x51 ⟶ x4 x51 ⟶ x15 x51 ⟶ x5 x51 ⟶ x14 x51 ⟶ x6 x51 ⟶ x13 x51 ⟶ x2 x50 (x12 x51) ⟶ x2 x48 (x12 x51) ⟶ x2 x49 (x7 x51) ⟶ (x2 (x9 x51 x50 x48 x49) (x1 (x36 (x7 x51) (x7 x51))) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x3 x51 ⟶ x16 x51 ⟶ x4 x51 ⟶ x15 x51 ⟶ x5 x51 ⟶ x14 x51 ⟶ x6 x51 ⟶ x13 x51 ⟶ x2 x50 (x12 x51) ⟶ x2 x48 (x12 x51) ⟶ x2 x49 (x7 x51) ⟶ (x41 (x9 x51 x50 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ x27 x48 = x28 x48 ⟶ (x22 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ (x17 x48 (x27 x48) = x17 x48 (x28 x48) ⟶ False) ⟶ (x22 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ (x0 (x28 x48) (x19 x48) ⟶ False) ⟶ (x22 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ (x0 (x27 x48) (x19 x48) ⟶ False) ⟶ (x22 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x18 x50 ⟶ x41 x50 ⟶ x22 x50 ⟶ x0 x48 (x19 x50) ⟶ x0 x49 (x19 x50) ⟶ x17 x50 x48 = x17 x50 x49 ⟶ (x48 = x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x3 x49 ⟶ x16 x49 ⟶ x4 x49 ⟶ x15 x49 ⟶ x5 x49 ⟶ x13 x49 ⟶ x2 x48 (x12 x49) ⟶ (x8 x49 x48 = x25 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x43 x49 ⟶ x2 x48 (x1 x49) ⟶ (x43 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x43 x49 ⟶ x2 x48 x49 ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x43 x49 ⟶ x2 x48 x49 ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x43 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x34 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x39 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x34 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x34 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ (x39 x48 ⟶ False) ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ (x39 x48 ⟶ False) ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ x41 x48 ⟶ (x39 x48 ⟶ False) ⟶ x34 x48 ⟶ False) ⟶ (∀ x48 x49 x50 . x47 x50 ⟶ x2 x48 (x1 (x36 x49 x50)) ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x39 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x47 x50 ⟶ x2 x48 (x1 (x36 x50 x49)) ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x18 x49 ⟶ x41 x49 ⟶ x2 x48 (x1 x49) ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x2 x50 (x1 (x36 x48 x49)) ⟶ (x21 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x2 x50 (x1 (x36 x49 x48)) ⟶ (x20 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x22 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x18 x48 ⟶ x41 x48 ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x2 x50 (x1 (x36 x48 x49)) ⟶ (x18 x50 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x41 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x48 x49 ⟶ x0 x49 x48 ⟶ False) ⟶ (x22 (x9 x29 x32 x31 x30) ⟶ False) ⟶ (x11 x29 x30 x31 ⟶ False) ⟶ (x11 x29 x30 x32 ⟶ False) ⟶ ((x2 x31 (x12 x29) ⟶ False) ⟶ False) ⟶ ((x2 x32 (x12 x29) ⟶ False) ⟶ False) ⟶ ((x2 x30 (x7 x29) ⟶ False) ⟶ False) ⟶ ((x13 x29 ⟶ False) ⟶ False) ⟶ ((x6 x29 ⟶ False) ⟶ False) ⟶ ((x14 x29 ⟶ False) ⟶ False) ⟶ ((x5 x29 ⟶ False) ⟶ False) ⟶ ((x15 x29 ⟶ False) ⟶ False) ⟶ ((x4 x29 ⟶ False) ⟶ False) ⟶ ((x16 x29 ⟶ False) ⟶ False) ⟶ ((x3 x29 ⟶ False) ⟶ False) ⟶ False (proof)