Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../40adb..
PUM7c../5a54c..
vout
PrPhD../46fb9.. 102.65 bars
TMFiT../391d5.. ownership of c0597.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMVj6../98889.. ownership of 5ee0b.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUMES../2f048.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem c0597.. : ∀ 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 x55 . x51 x55 ⟶ x44 x52 (x43 x55) ⟶ x44 x54 (x50 x55) ⟶ x44 x53 (x45 (x43 x55)) ⟶ x46 x55 (x48 (x43 x55) x53 (x47 (x43 x55) x52)) x54 ⟶ (x49 x55 x52 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . x51 x55 ⟶ x44 x52 (x43 x55) ⟶ x44 x54 (x50 x55) ⟶ x44 x53 (x45 (x43 x55)) ⟶ x46 x55 (x48 (x43 x55) x53 (x47 (x43 x55) x52)) x54 ⟶ (x46 x55 x53 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . x51 x55 ⟶ x44 x52 (x43 x55) ⟶ x44 x54 (x50 x55) ⟶ x44 x53 (x45 (x43 x55)) ⟶ x46 x55 x53 x54 ⟶ x49 x55 x52 x54 ⟶ (x46 x55 (x48 (x43 x55) x53 (x47 (x43 x55) x52)) x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x0 x53 ⟶ (x53 = x52 ⟶ False) ⟶ x0 x52 ⟶ False) ⟶ (∀ x52 x53 . x42 x52 x53 ⟶ x0 x53 ⟶ False) ⟶ (∀ x52 . x0 x52 ⟶ (x52 = x1 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x42 x52 x53 ⟶ x44 x53 (x45 x54) ⟶ x0 x54 ⟶ False) ⟶ (∀ x52 x53 x54 . x42 x53 x54 ⟶ x44 x54 (x45 x52) ⟶ (x44 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . x41 x55 ⟶ x51 x55 ⟶ x44 x54 (x43 x55) ⟶ x44 x52 (x43 x55) ⟶ x44 x53 (x40 x55) ⟶ (x54 = x52 ⟶ False) ⟶ x37 (x38 (x43 x55) x54 x52 (x39 x53 x52 x54 x55)) x55 ⟶ False) ⟶ (∀ x52 x53 x54 x55 . x41 x55 ⟶ x51 x55 ⟶ x44 x54 (x43 x55) ⟶ x44 x52 (x43 x55) ⟶ x44 x53 (x40 x55) ⟶ (x54 = x52 ⟶ False) ⟶ (x2 x55 (x39 x53 x52 x54 x55) x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . x41 x55 ⟶ x51 x55 ⟶ x44 x54 (x43 x55) ⟶ x44 x52 (x43 x55) ⟶ x44 x53 (x40 x55) ⟶ (x54 = x52 ⟶ False) ⟶ (x44 (x39 x53 x52 x54 x55) (x43 x55) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x3 x53 x52 ⟶ (x44 x53 (x45 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x44 x53 (x45 x52) ⟶ (x3 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x7 x53 x52 x54 = x6 (x5 x53 x52) (x4 x54) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x44 x52 x53 ⟶ (x0 x53 ⟶ False) ⟶ (x42 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x42 x53 x52 ⟶ (x44 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x6 x52 x1 = x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x3 x52 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x0 x55 ⟶ False) ⟶ x44 x52 x55 ⟶ x44 x54 x55 ⟶ x44 x53 x55 ⟶ (x38 x55 x52 x54 x53 = x7 x52 x54 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x0 x54 ⟶ False) ⟶ x44 x52 x54 ⟶ x44 x53 x54 ⟶ (x8 x54 x52 x53 = x5 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x0 x53 ⟶ False) ⟶ x44 x52 x53 ⟶ (x47 x53 x52 = x4 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x44 x53 (x45 x54) ⟶ x44 x52 (x45 x54) ⟶ (x48 x54 x53 x52 = x6 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x0 x52 ⟶ False) ⟶ (x35 (x36 x52) x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x0 x52 ⟶ False) ⟶ (x44 (x36 x52) (x45 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 . x35 (x34 x52) x52 ⟶ False) ⟶ (∀ x52 . (x44 (x34 x52) (x45 x52) ⟶ False) ⟶ False) ⟶ (x0 x33 ⟶ False) ⟶ (∀ x52 . (x0 (x9 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 . (x44 (x9 x52) (x45 x52) ⟶ False) ⟶ False) ⟶ ((x0 x10 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x0 x52 ⟶ False) ⟶ x0 (x32 x52) ⟶ False) ⟶ (∀ x52 . (x0 x52 ⟶ False) ⟶ (x44 (x32 x52) (x45 x52) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x44 x53 (x45 x54) ⟶ x44 x52 (x45 x54) ⟶ (x48 x54 x53 x53 = x53 ⟶ False) ⟶ False) ⟶ (∀ x52 . (x6 x52 x52 = x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x0 x53 ⟶ False) ⟶ x0 (x6 x52 x53) ⟶ False) ⟶ (∀ x52 x53 . (x0 x53 ⟶ False) ⟶ x0 (x6 x53 x52) ⟶ False) ⟶ (∀ x52 x53 . x0 (x5 x52 x53) ⟶ False) ⟶ (∀ x52 . x0 (x4 x52) ⟶ False) ⟶ (∀ x52 x53 x54 . x0 (x7 x54 x53 x52) ⟶ False) ⟶ ((x0 x1 ⟶ False) ⟶ False) ⟶ (∀ x52 . x0 (x45 x52) ⟶ False) ⟶ (∀ x52 . (x44 (x11 x52) x52 ⟶ False) ⟶ False) ⟶ ((x51 x31 ⟶ False) ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x0 (x40 x52) ⟶ False) ⟶ (∀ x52 . x12 x52 ⟶ x0 (x50 x52) ⟶ False) ⟶ (∀ x52 . x12 x52 ⟶ x0 (x43 x52) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ (x12 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 x55 . (x0 x55 ⟶ False) ⟶ x44 x52 x55 ⟶ x44 x54 x55 ⟶ x44 x53 x55 ⟶ (x44 (x38 x55 x52 x54 x53) (x45 x55) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x0 x54 ⟶ False) ⟶ x44 x52 x54 ⟶ x44 x53 x54 ⟶ (x44 (x8 x54 x52 x53) (x45 x54) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x0 x53 ⟶ False) ⟶ x44 x52 x53 ⟶ (x44 (x47 x53 x52) (x45 x53) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x44 x53 (x45 x54) ⟶ x44 x52 (x45 x54) ⟶ (x44 (x48 x54 x53 x52) (x45 x54) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x12 x54 ⟶ x44 x52 (x43 x54) ⟶ x44 x53 (x43 x54) ⟶ (x52 = x53 ⟶ False) ⟶ x46 x54 (x8 (x43 x54) x52 x53) (x29 x54) ⟶ (x30 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 . x12 x52 ⟶ (x44 (x29 x52) (x50 x52) ⟶ False) ⟶ (x30 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x12 x53 ⟶ x30 x53 ⟶ x44 x52 (x50 x53) ⟶ (x46 x53 (x8 (x43 x53) (x28 x52 x53) (x27 x52 x53)) x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x12 x53 ⟶ x30 x53 ⟶ x44 x52 (x50 x53) ⟶ x28 x52 x53 = x27 x52 x53 ⟶ False) ⟶ (∀ x52 x53 . x12 x53 ⟶ x30 x53 ⟶ x44 x52 (x50 x53) ⟶ (x44 (x27 x52 x53) (x43 x53) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x12 x53 ⟶ x30 x53 ⟶ x44 x52 (x50 x53) ⟶ (x44 (x28 x52 x53) (x43 x53) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x12 x54 ⟶ x44 x52 (x45 (x43 x54)) ⟶ x44 x53 (x50 x54) ⟶ x46 x54 x52 x53 ⟶ (x37 x52 x54 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x12 x53 ⟶ x44 x52 (x45 (x43 x53)) ⟶ x37 x52 x53 ⟶ (x46 x53 x52 (x14 x52 x53) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x12 x53 ⟶ x44 x52 (x45 (x43 x53)) ⟶ x37 x52 x53 ⟶ (x44 (x14 x52 x53) (x50 x53) ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . (x0 x54 ⟶ False) ⟶ x44 x52 x54 ⟶ x44 x53 x54 ⟶ (x8 x54 x52 x53 = x8 x54 x53 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 x54 . x44 x53 (x45 x54) ⟶ x44 x52 (x45 x54) ⟶ (x48 x54 x53 x52 = x48 x54 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x6 x53 x52 = x6 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x5 x53 x52 = x5 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x0 x53 ⟶ x44 x52 (x45 x53) ⟶ x35 x52 x53 ⟶ False) ⟶ (∀ x52 x53 . (x0 x53 ⟶ False) ⟶ x44 x52 (x45 x53) ⟶ x0 x52 ⟶ (x35 x52 x53 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . (x0 x53 ⟶ False) ⟶ x44 x52 (x45 x53) ⟶ (x35 x52 x53 ⟶ False) ⟶ x0 x52 ⟶ False) ⟶ (∀ x52 x53 . x0 x53 ⟶ x44 x52 (x45 x53) ⟶ (x0 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x15 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x26 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x16 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x25 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x17 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x24 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x18 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x23 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x19 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 . x51 x52 ⟶ x41 x52 ⟶ (x30 x52 ⟶ False) ⟶ False) ⟶ (∀ x52 x53 . x42 x52 x53 ⟶ x42 x53 x52 ⟶ False) ⟶ (∀ x52 . x44 x52 (x43 x22) ⟶ x2 x22 x52 x21 ⟶ (x49 x22 x52 x20 ⟶ False) ⟶ False) ⟶ ((x44 x21 (x40 x22) ⟶ False) ⟶ False) ⟶ ((x44 x20 (x50 x22) ⟶ False) ⟶ False) ⟶ ((x51 x22 ⟶ False) ⟶ False) ⟶ ((x41 x22 ⟶ False) ⟶ False) ⟶ False (proof)