Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../9ffc3..
PUR2U../3fa8a..
vout
PrPhD../d9460.. 102.63 bars
TMcm9../9de6d.. ownership of c08e5.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMcrH../9b500.. ownership of f111c.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUbJz../04f66.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c08e5.. : ∀ 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 . x50 x52 ⟶ (x52 = x51 ⟶ False) ⟶ x50 x51 ⟶ False) ⟶ (∀ x51 x52 . x0 x51 x52 ⟶ x50 x52 ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x51 = x49 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x0 x51 x52 ⟶ x2 x52 (x1 x53) ⟶ x50 x53 ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x48 x54 ⟶ x45 x54 ⟶ x48 x53 ⟶ x45 x53 ⟶ x48 x52 ⟶ x45 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ x47 x54 = x47 x53 ⟶ x47 x51 = x47 x52 ⟶ x46 x54 x53 = x46 x51 x52 ⟶ (x53 = x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x48 x54 ⟶ x45 x54 ⟶ x48 x53 ⟶ x45 x53 ⟶ x48 x52 ⟶ x45 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ x47 x54 = x47 x53 ⟶ x47 x51 = x47 x52 ⟶ x46 x54 x53 = x46 x51 x52 ⟶ (x54 = x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x0 x52 x53 ⟶ x2 x53 (x1 x51) ⟶ (x2 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x3 x52 x51 ⟶ (x2 x52 (x1 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x2 x52 (x1 x51) ⟶ (x3 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x2 x51 x52 ⟶ (x50 x52 ⟶ False) ⟶ (x0 x51 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x0 x52 x51 ⟶ (x2 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x45 x54 ⟶ x6 x54 x51 x52 ⟶ x2 x54 (x1 (x4 x51 x52)) ⟶ x45 x53 ⟶ x6 x53 x51 x52 ⟶ x2 x53 (x1 (x4 x51 x52)) ⟶ x5 x51 x52 x54 x53 ⟶ (x5 x51 x52 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x45 x54 ⟶ x6 x54 x51 x52 ⟶ x2 x54 (x1 (x4 x51 x52)) ⟶ x45 x53 ⟶ x6 x53 x51 x52 ⟶ x2 x53 (x1 (x4 x51 x52)) ⟶ (x5 x51 x52 x54 x54 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x3 x51 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x45 x54 ⟶ x6 x54 x51 x52 ⟶ x2 x54 (x1 (x4 x51 x52)) ⟶ x45 x53 ⟶ x6 x53 x51 x52 ⟶ x2 x53 (x1 (x4 x51 x52)) ⟶ x54 = x53 ⟶ (x5 x51 x52 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x45 x54 ⟶ x6 x54 x51 x52 ⟶ x2 x54 (x1 (x4 x51 x52)) ⟶ x45 x53 ⟶ x6 x53 x51 x52 ⟶ x2 x53 (x1 (x4 x51 x52)) ⟶ x5 x51 x52 x54 x53 ⟶ (x54 = x53 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x43 x52 x51 ⟶ (x44 x51 x52 = x47 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x45 (x7 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x43 (x7 x51) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x8 (x7 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x48 (x7 x51) ⟶ False) ⟶ False) ⟶ ((x9 x10 ⟶ False) ⟶ False) ⟶ (x50 x10 ⟶ False) ⟶ (∀ x51 . (x11 x51 ⟶ False) ⟶ x11 (x12 x51) ⟶ False) ⟶ (∀ x51 . (x11 x51 ⟶ False) ⟶ (x2 (x12 x51) (x1 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x45 (x13 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x42 (x13 x51 x52) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x43 (x13 x52 x51) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x48 (x13 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ (x11 (x14 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x50 (x14 x51) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ (x2 (x14 x51) (x1 x51) ⟶ False) ⟶ False) ⟶ (x41 x40 ⟶ False) ⟶ ((x45 x40 ⟶ False) ⟶ False) ⟶ ((x48 x40 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ (x16 (x15 x51) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ (x2 (x15 x51) (x1 x51) ⟶ False) ⟶ False) ⟶ ((x45 x17 ⟶ False) ⟶ False) ⟶ ((x8 x17 ⟶ False) ⟶ False) ⟶ ((x48 x17 ⟶ False) ⟶ False) ⟶ (x50 x17 ⟶ False) ⟶ (∀ x51 . x16 (x18 x51) x51 ⟶ False) ⟶ (∀ x51 . (x2 (x18 x51) (x1 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x42 (x19 x51 x52) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x43 (x19 x52 x51) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x48 (x19 x51 x52) ⟶ False) ⟶ False) ⟶ ((x45 x39 ⟶ False) ⟶ False) ⟶ ((x8 x39 ⟶ False) ⟶ False) ⟶ ((x48 x39 ⟶ False) ⟶ False) ⟶ (x50 x20 ⟶ False) ⟶ (∀ x51 . (x50 (x38 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x2 (x38 x51) (x1 x51) ⟶ False) ⟶ False) ⟶ ((x8 x37 ⟶ False) ⟶ False) ⟶ ((x48 x37 ⟶ False) ⟶ False) ⟶ ((x36 x35 ⟶ False) ⟶ False) ⟶ ((x45 x35 ⟶ False) ⟶ False) ⟶ ((x48 x35 ⟶ False) ⟶ False) ⟶ ((x50 x21 ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x50 (x34 x51) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ (x2 (x34 x51) (x1 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x42 (x33 x51 x52) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x43 (x33 x52 x51) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x48 (x33 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x50 (x33 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x2 (x33 x51 x52) (x1 (x4 x52 x51)) ⟶ False) ⟶ False) ⟶ ((x48 x22 ⟶ False) ⟶ False) ⟶ (x50 x22 ⟶ False) ⟶ ((x45 x23 ⟶ False) ⟶ False) ⟶ ((x48 x23 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 x54 . x2 x54 (x1 (x4 (x4 x52 x51) x53)) ⟶ (x48 (x47 x54) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x50 x51 ⟶ False) ⟶ x48 x51 ⟶ x50 (x47 x51) ⟶ False) ⟶ (∀ x51 x52 . (x48 (x4 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x50 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x50 (x46 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x50 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x45 (x46 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x50 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x48 (x46 x51 x52) ⟶ False) ⟶ False) ⟶ (∀ x51 . x11 x51 ⟶ x48 x51 ⟶ (x11 (x47 x51) ⟶ False) ⟶ False) ⟶ ((x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 (x1 x51) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x50 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x50 (x46 x52 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x50 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x45 (x46 x52 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x50 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x48 (x46 x52 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x11 x51 ⟶ False) ⟶ x48 x51 ⟶ x45 x51 ⟶ x11 (x47 x51) ⟶ False) ⟶ (∀ x51 x52 . (x50 x52 ⟶ False) ⟶ (x50 x51 ⟶ False) ⟶ x50 (x4 x52 x51) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x50 (x47 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 . (x2 (x32 x51) x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x43 x52 x51 ⟶ (x2 (x44 x51 x52) (x1 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x45 (x46 x52 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x48 (x46 x52 x51) ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x51 (x1 (x4 x52 x53)) ⟶ x53 = x49 ⟶ x51 = x49 ⟶ (x6 x51 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x51 (x1 (x4 x52 x53)) ⟶ x53 = x49 ⟶ x6 x51 x52 x53 ⟶ (x51 = x49 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x52 (x1 (x4 x51 x53)) ⟶ (x53 = x49 ⟶ False) ⟶ x51 = x44 x51 x52 ⟶ (x6 x52 x51 x53 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x51 (x1 (x4 x52 x53)) ⟶ (x53 = x49 ⟶ False) ⟶ x6 x51 x52 x53 ⟶ (x52 = x44 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x9 x52 ⟶ x2 x51 (x1 x52) ⟶ (x9 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x48 x51 ⟶ x42 x51 x52 ⟶ (x42 x51 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x48 x51 ⟶ x42 x51 x52 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x48 x51 ⟶ x42 x51 x52 ⟶ (x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x9 x52 ⟶ x2 x51 x52 ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x9 x52 ⟶ x2 x51 x52 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x48 x51 ⟶ x43 x51 x52 ⟶ (x43 x51 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x48 x51 ⟶ x43 x51 x52 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x48 x51 ⟶ x43 x51 x52 ⟶ (x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x9 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x42 x53 x51 ⟶ x2 x52 (x1 x53) ⟶ (x42 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x11 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x41 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x11 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x11 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x11 x52 ⟶ x2 x51 (x1 x52) ⟶ (x11 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x48 x53 ⟶ x43 x53 x51 ⟶ x2 x52 (x1 x53) ⟶ (x43 x52 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x45 x51 ⟶ (x41 x51 ⟶ False) ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x45 x51 ⟶ (x41 x51 ⟶ False) ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x48 x51 ⟶ x45 x51 ⟶ (x41 x51 ⟶ False) ⟶ x11 x51 ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x2 x51 (x1 x52) ⟶ x16 x51 x52 ⟶ False) ⟶ (∀ x51 x52 x53 . x50 x53 ⟶ x2 x51 (x1 (x4 x52 x53)) ⟶ (x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ (x8 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x41 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x50 x52 ⟶ False) ⟶ x2 x51 (x1 x52) ⟶ x50 x51 ⟶ (x16 x51 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x50 x53 ⟶ x2 x51 (x1 (x4 x53 x52)) ⟶ (x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ (x31 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x45 x52 ⟶ x2 x51 (x1 x52) ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . (x50 x52 ⟶ False) ⟶ x2 x51 (x1 x52) ⟶ (x16 x51 x52 ⟶ False) ⟶ x50 x51 ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x53 (x1 (x4 x51 x52)) ⟶ (x42 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x53 (x1 (x4 x52 x51)) ⟶ (x43 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x48 x52 ⟶ x2 x51 (x1 x52) ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x36 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ x48 x51 ⟶ x45 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x50 x52 ⟶ x2 x51 (x1 x52) ⟶ (x50 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 x53 . x2 x53 (x1 (x4 x51 x52)) ⟶ (x48 x53 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x48 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 . x50 x51 ⟶ (x45 x51 ⟶ False) ⟶ False) ⟶ (∀ x51 x52 . x0 x51 x52 ⟶ x0 x52 x51 ⟶ False) ⟶ (x5 x24 x30 x29 x28 ⟶ x5 x24 x27 x26 x25 ⟶ False) ⟶ (x27 = x49 ⟶ (x24 = x49 ⟶ False) ⟶ False) ⟶ (x30 = x49 ⟶ (x24 = x49 ⟶ False) ⟶ False) ⟶ ((x46 x29 x26 = x46 x28 x25 ⟶ False) ⟶ False) ⟶ ((x2 x25 (x1 (x4 x24 x27)) ⟶ False) ⟶ False) ⟶ ((x6 x25 x24 x27 ⟶ False) ⟶ False) ⟶ ((x45 x25 ⟶ False) ⟶ False) ⟶ ((x2 x26 (x1 (x4 x24 x27)) ⟶ False) ⟶ False) ⟶ ((x6 x26 x24 x27 ⟶ False) ⟶ False) ⟶ ((x45 x26 ⟶ False) ⟶ False) ⟶ ((x2 x28 (x1 (x4 x24 x30)) ⟶ False) ⟶ False) ⟶ ((x6 x28 x24 x30 ⟶ False) ⟶ False) ⟶ ((x45 x28 ⟶ False) ⟶ False) ⟶ ((x2 x29 (x1 (x4 x24 x30)) ⟶ False) ⟶ False) ⟶ ((x6 x29 x24 x30 ⟶ False) ⟶ False) ⟶ ((x45 x29 ⟶ False) ⟶ False) ⟶ False (proof)