Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrPhD../c9e52..
PUKBT../44905..
vout
PrPhD../bb608.. 3.41 bars
TMLE6../5c18a.. ownership of 6e6dc.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
TMQaw../3cb90.. ownership of c87ea.. as prop with payaddr PrPhD.. rightscost 0.00 controlledby PrPhD.. upto 0
PURwQ../78279.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 6e6dc.. : ∀ 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 . x38 x40 ⟶ (x40 = x39 ⟶ False) ⟶ x38 x39 ⟶ False) ⟶ (∀ x39 x40 . x0 x39 x40 ⟶ x38 x40 ⟶ False) ⟶ (∀ x39 . x38 x39 ⟶ (x39 = x37 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x0 x39 x40 ⟶ x2 x40 (x1 x41) ⟶ x38 x41 ⟶ False) ⟶ (∀ x39 x40 x41 . x0 x40 x41 ⟶ x2 x41 (x1 x39) ⟶ (x2 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x3 x40 x39 ⟶ (x2 x40 (x1 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x2 x40 (x1 x39) ⟶ (x3 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x4 x39 ⟶ (x5 x6 x39 = x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x2 x39 x40 ⟶ (x38 x40 ⟶ False) ⟶ (x0 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x0 x40 x39 ⟶ (x2 x40 x39 ⟶ False) ⟶ False) ⟶ ((x2 x37 x36 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . x4 x41 ⟶ x4 x39 ⟶ x4 x40 ⟶ (x5 (x5 x41 x39) x40 = x5 x41 (x5 x39 x40) ⟶ False) ⟶ False) ⟶ ((x2 x6 x35 ⟶ False) ⟶ False) ⟶ ((x2 x6 x7 ⟶ False) ⟶ False) ⟶ ((x34 x6 x35 x7 ⟶ False) ⟶ False) ⟶ ((x8 x6 ⟶ False) ⟶ False) ⟶ (x38 x6 ⟶ False) ⟶ ((x5 x6 x6 = x6 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x3 x39 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x38 x41 ⟶ False) ⟶ (x38 x39 ⟶ False) ⟶ x2 x39 (x1 x41) ⟶ x2 x40 x39 ⟶ (x34 x40 x41 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x38 x41 ⟶ False) ⟶ (x38 x39 ⟶ False) ⟶ x2 x39 (x1 x41) ⟶ x34 x40 x41 x39 ⟶ (x2 x40 x39 ⟶ False) ⟶ False) ⟶ ((x7 = x36 ⟶ False) ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ (x38 x32 ⟶ False) ⟶ ((x33 x31 ⟶ False) ⟶ False) ⟶ ((x4 x9 ⟶ False) ⟶ False) ⟶ (x38 x9 ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ ((x30 x11 ⟶ False) ⟶ False) ⟶ ((x12 x11 ⟶ False) ⟶ False) ⟶ (x38 x11 ⟶ False) ⟶ ((x4 x13 ⟶ False) ⟶ False) ⟶ ((x29 x28 ⟶ False) ⟶ False) ⟶ ((x10 x14 ⟶ False) ⟶ False) ⟶ (∀ x39 . x29 x39 ⟶ (x27 (x27 x39) = x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x15 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x26 x40 x40 = x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x38 x40 ⟶ False) ⟶ x4 x40 ⟶ (x38 x39 ⟶ False) ⟶ x4 x39 ⟶ x38 (x5 x40 x39) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x29 (x25 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x29 (x16 x40 x39) ⟶ False) ⟶ False) ⟶ ((x10 x36 ⟶ False) ⟶ False) ⟶ (x38 x36 ⟶ False) ⟶ (∀ x39 x40 . x4 x40 ⟶ x4 x39 ⟶ (x4 (x24 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x29 (x15 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x4 x40 ⟶ x4 x39 ⟶ (x4 (x5 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x29 (x26 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . (x38 x40 ⟶ False) ⟶ (x38 x39 ⟶ False) ⟶ x2 x39 (x1 x40) ⟶ (x34 (x23 x39 x40) x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . (x2 (x17 x39) x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 x41 . (x38 x41 ⟶ False) ⟶ (x38 x39 ⟶ False) ⟶ x2 x39 (x1 x41) ⟶ x34 x40 x41 x39 ⟶ (x2 x40 x41 ⟶ False) ⟶ False) ⟶ ((x2 x7 (x1 x35) ⟶ False) ⟶ False) ⟶ (∀ x39 . x29 x39 ⟶ (x29 (x27 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x16 x40 x39 = x27 (x26 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x15 x40 x39 = x27 (x26 (x27 x40) (x27 x39)) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x26 x40 x39 = x5 x40 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x29 x39 ⟶ (x27 x39 = x24 x6 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x25 x40 x39 = x27 (x15 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x25 x40 x39 = x25 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x16 x40 x39 = x16 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x15 x40 x39 = x15 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x29 x40 ⟶ x29 x39 ⟶ (x26 x40 x39 = x26 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x4 x40 ⟶ x4 x39 ⟶ (x5 x40 x39 = x5 x39 x40 ⟶ False) ⟶ False) ⟶ (∀ x39 . x38 x39 ⟶ (x18 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x2 x39 x36 ⟶ (x33 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x38 x39 ⟶ (x33 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x33 x39 ⟶ (x10 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x10 x40 ⟶ x2 x39 x40 ⟶ (x10 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x38 x39 ⟶ (x22 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x38 x39 ⟶ (x10 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x33 x39 ⟶ (x4 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x12 x39 ⟶ x30 x39 ⟶ (x10 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x2 x39 x35 ⟶ (x4 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x29 x39 ⟶ (x33 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x10 x39 ⟶ (x30 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 . x10 x39 ⟶ (x12 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x18 x40 ⟶ x2 x39 (x1 x40) ⟶ (x18 x39 ⟶ False) ⟶ False) ⟶ (∀ x39 x40 . x0 x39 x40 ⟶ x0 x40 x39 ⟶ False) ⟶ (x16 x19 (x25 x20 x21) = x15 (x15 (x27 x19) x20) x21 ⟶ False) ⟶ ((x29 x21 ⟶ False) ⟶ False) ⟶ ((x29 x20 ⟶ False) ⟶ False) ⟶ ((x29 x19 ⟶ False) ⟶ False) ⟶ False (proof)