Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../221c9..
PUdcK../03c2a..
vout
PrNUD../5cd03.. 0.03 bars
TMRiB../64af8.. ownership of 553e0.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMFdP../2d249.. ownership of a74c7.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PUQq9../6c17a.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 553e0.. : ∀ 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 . x45 x47 ⟶ (x47 = x46 ⟶ False) ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x45 x47 ⟶ False) ⟶ (∀ x46 . x45 x46 ⟶ (x46 = x44 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x0 x46 x47 ⟶ x2 x47 (x1 x48) ⟶ x45 x48 ⟶ False) ⟶ (∀ x46 x47 x48 . x0 x47 x48 ⟶ x2 x48 (x1 x46) ⟶ (x2 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x3 x47 x46 ⟶ (x2 x47 (x1 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x47 (x1 x46) ⟶ (x3 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . (x4 x48 x48 x47 x46 = x5 x48 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x2 x46 x47 ⟶ (x45 x47 ⟶ False) ⟶ (x0 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x47 x46 ⟶ (x2 x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x3 x46 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 x50 . (x45 x50 ⟶ False) ⟶ x2 x46 x50 ⟶ x2 x49 x50 ⟶ x2 x47 x50 ⟶ x2 x48 x50 ⟶ (x6 x50 x46 x49 x47 x48 = x4 x46 x49 x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . (x45 x49 ⟶ False) ⟶ x2 x46 x49 ⟶ x2 x48 x49 ⟶ x2 x47 x49 ⟶ (x43 x49 x46 x48 x47 = x5 x46 x48 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ (x8 (x7 x46) x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ (x2 (x7 x46) (x1 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . x8 (x9 x46) x46 ⟶ False) ⟶ (∀ x46 . (x2 (x9 x46) (x1 x46) ⟶ False) ⟶ False) ⟶ (x45 x10 ⟶ False) ⟶ (∀ x46 . (x45 (x42 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 . (x2 (x42 x46) (x1 x46) ⟶ False) ⟶ False) ⟶ ((x45 x41 ⟶ False) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ x45 (x11 x46) ⟶ False) ⟶ (∀ x46 . (x45 x46 ⟶ False) ⟶ (x2 (x11 x46) (x1 x46) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . x45 (x4 x49 x46 x47 x48) ⟶ False) ⟶ (∀ x46 x47 x48 . x45 (x5 x48 x47 x46) ⟶ False) ⟶ ((x45 x44 ⟶ False) ⟶ False) ⟶ (∀ x46 . x45 (x1 x46) ⟶ False) ⟶ (∀ x46 . (x2 (x12 x46) x46 ⟶ False) ⟶ False) ⟶ ((x40 x39 ⟶ False) ⟶ False) ⟶ ((x13 x14 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x45 (x38 x46) ⟶ False) ⟶ (∀ x46 . x13 x46 ⟶ x45 (x15 x46) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x13 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 x50 . (x45 x50 ⟶ False) ⟶ x2 x46 x50 ⟶ x2 x49 x50 ⟶ x2 x47 x50 ⟶ x2 x48 x50 ⟶ (x2 (x6 x50 x46 x49 x47 x48) (x1 x50) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . (x45 x49 ⟶ False) ⟶ x2 x46 x49 ⟶ x2 x48 x49 ⟶ x2 x47 x49 ⟶ (x2 (x43 x49 x46 x48 x47) (x1 x49) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 . x40 x48 ⟶ x2 x46 (x1 (x15 x48)) ⟶ x2 x47 (x38 x48) ⟶ x17 x48 x46 x47 ⟶ (x16 x46 x48 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x40 x47 ⟶ x2 x46 (x1 (x15 x47)) ⟶ x16 x46 x47 ⟶ (x17 x47 x46 (x37 x46 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x40 x47 ⟶ x2 x46 (x1 (x15 x47)) ⟶ x16 x46 x47 ⟶ (x2 (x37 x46 x47) (x38 x47) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x40 x47 ⟶ x2 x46 (x38 x47) ⟶ x17 x47 (x43 (x15 x47) (x35 x47) (x34 x47) (x33 x47)) x46 ⟶ (x36 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x2 (x33 x46) (x15 x46) ⟶ False) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x2 (x34 x46) (x15 x46) ⟶ False) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ (x2 (x35 x46) (x15 x46) ⟶ False) ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . x40 x49 ⟶ x36 x49 ⟶ x2 x48 (x15 x49) ⟶ x2 x46 (x15 x49) ⟶ x2 x47 (x15 x49) ⟶ (x17 x49 (x43 (x15 x49) x48 x46 x47) (x32 x47 x46 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 x48 x49 . x40 x49 ⟶ x36 x49 ⟶ x2 x48 (x15 x49) ⟶ x2 x46 (x15 x49) ⟶ x2 x47 (x15 x49) ⟶ (x2 (x32 x47 x46 x48 x49) (x38 x49) ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x45 x47 ⟶ x2 x46 (x1 x47) ⟶ x8 x46 x47 ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x2 x46 (x1 x47) ⟶ x45 x46 ⟶ (x8 x46 x47 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . (x45 x47 ⟶ False) ⟶ x2 x46 (x1 x47) ⟶ (x8 x46 x47 ⟶ False) ⟶ x45 x46 ⟶ False) ⟶ (∀ x46 x47 . x45 x47 ⟶ x2 x46 (x1 x47) ⟶ (x45 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x30 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x18 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x29 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x19 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x28 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x36 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x27 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x20 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x26 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 . x40 x46 ⟶ x31 x46 ⟶ (x21 x46 ⟶ False) ⟶ False) ⟶ (∀ x46 x47 . x0 x46 x47 ⟶ x0 x47 x46 ⟶ False) ⟶ (x16 (x6 (x15 x22) x25 x25 x23 x24) x22 ⟶ False) ⟶ ((x2 x24 (x15 x22) ⟶ False) ⟶ False) ⟶ ((x2 x23 (x15 x22) ⟶ False) ⟶ False) ⟶ ((x2 x25 (x15 x22) ⟶ False) ⟶ False) ⟶ ((x40 x22 ⟶ False) ⟶ False) ⟶ ((x31 x22 ⟶ False) ⟶ False) ⟶ False (proof)