Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../2004a..
PUaA1../8a57a..
vout
PrNUD../f0f05.. 0.02 bars
TMbWv../fb251.. ownership of 73a9e.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMFY5../bfa58.. ownership of a2bce.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUKfR../b924c.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 73a9e.. : ∀ 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 . x45 x50 ⟶ x45 x48 ⟶ x45 x49 ⟶ (x43 x50 x48 ⟶ False) ⟶ (x43 x49 x50 ⟶ False) ⟶ (x0 x50 (x44 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x45 x49 ⟶ x0 x50 (x44 x48 x49) ⟶ x43 x49 x50 ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x45 x49 ⟶ x0 x50 (x44 x48 x49) ⟶ x43 x50 x48 ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x49 x50 ⟶ x2 x50 (x1 x48) ⟶ (x2 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x42 x49 x48 ⟶ (x2 x49 (x1 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x2 x49 (x1 x48) ⟶ (x42 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x45 x49 ⟶ x43 x50 x48 ⟶ x43 x48 x49 ⟶ (x43 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x0 x49 x50 ⟶ x0 x48 x50 ⟶ x0 x48 (x3 x50 x49) ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x48 ⟶ (x0 (x3 x48 x49) x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x2 x48 x49 ⟶ (x47 x49 ⟶ False) ⟶ (x0 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x43 x48 x49 ⟶ False) ⟶ x43 x48 (x41 x48 x49) ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x43 x48 x49 ⟶ False) ⟶ x43 (x41 x48 x49) x49 ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x43 x48 x49 ⟶ False) ⟶ (x45 (x41 x48 x49) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x49 x48 ⟶ (x2 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x43 x49 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x42 x48 x48 ⟶ False) ⟶ False) ⟶ ((x45 x40 ⟶ False) ⟶ False) ⟶ ((x47 x40 ⟶ False) ⟶ False) ⟶ ((x39 x38 ⟶ False) ⟶ False) ⟶ ((x45 x38 ⟶ False) ⟶ False) ⟶ ((x37 x38 ⟶ False) ⟶ False) ⟶ ((x47 x38 ⟶ False) ⟶ False) ⟶ ((x36 x35 ⟶ False) ⟶ False) ⟶ ((x45 x35 ⟶ False) ⟶ False) ⟶ ((x39 x34 ⟶ False) ⟶ False) ⟶ ((x36 x34 ⟶ False) ⟶ False) ⟶ ((x45 x34 ⟶ False) ⟶ False) ⟶ ((x37 x34 ⟶ False) ⟶ False) ⟶ ((x33 x32 ⟶ False) ⟶ False) ⟶ ((x4 x32 ⟶ False) ⟶ False) ⟶ (x47 x32 ⟶ False) ⟶ ((x5 x6 ⟶ False) ⟶ False) ⟶ ((x45 x6 ⟶ False) ⟶ False) ⟶ ((x39 x7 ⟶ False) ⟶ False) ⟶ ((x5 x7 ⟶ False) ⟶ False) ⟶ ((x45 x7 ⟶ False) ⟶ False) ⟶ ((x37 x7 ⟶ False) ⟶ False) ⟶ (x47 x8 ⟶ False) ⟶ ((x4 x31 ⟶ False) ⟶ False) ⟶ (x47 x31 ⟶ False) ⟶ ((x45 x30 ⟶ False) ⟶ False) ⟶ ((x39 x9 ⟶ False) ⟶ False) ⟶ ((x47 x29 ⟶ False) ⟶ False) ⟶ ((x4 x10 ⟶ False) ⟶ False) ⟶ (x47 x10 ⟶ False) ⟶ (∀ x48 x49 x50 x51 . x45 x51 ⟶ x45 x48 ⟶ x2 x50 x11 ⟶ x49 = x50 ⟶ (x43 x50 x51 ⟶ False) ⟶ (x43 x48 x50 ⟶ False) ⟶ (x0 x49 (x12 x51 x48) ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x0 x49 (x12 x50 x48) ⟶ x43 x48 (x28 x48 x50 x49) ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x0 x49 (x12 x50 x48) ⟶ x43 (x28 x48 x50 x49) x50 ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x0 x49 (x12 x50 x48) ⟶ (x49 = x28 x48 x50 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x45 x50 ⟶ x45 x48 ⟶ x0 x49 (x12 x50 x48) ⟶ (x2 (x28 x48 x50 x49) x11 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ (x47 (x44 x48 x48) ⟶ False) ⟶ False) ⟶ (x47 x11 ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x27 (x44 x49 x48) ⟶ False) ⟶ False) ⟶ ((x27 x11 ⟶ False) ⟶ False) ⟶ ((x47 x46 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x2 (x13 x48) x48 ⟶ False) ⟶ False) ⟶ ((x47 x26 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x27 x49 ⟶ x0 (x14 x48 x49) x48 ⟶ (x42 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x27 x49 ⟶ (x0 (x14 x48 x49) x49 ⟶ False) ⟶ (x42 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x27 x49 ⟶ (x45 (x14 x48 x49) ⟶ False) ⟶ (x42 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 x50 . x27 x50 ⟶ x42 x50 x48 ⟶ x45 x49 ⟶ x0 x49 x50 ⟶ (x0 x49 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x44 x49 x48 = x12 x49 x48 ⟶ False) ⟶ False) ⟶ ((x46 = x26 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x45 x49 ⟶ x45 x48 ⟶ (x43 x49 x48 ⟶ False) ⟶ (x43 x48 x49 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ (x5 x48 ⟶ False) ⟶ (x36 x48 ⟶ False) ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ (x5 x48 ⟶ False) ⟶ (x36 x48 ⟶ False) ⟶ (x47 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x45 x48 ⟶ x36 x48 ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x45 x48 ⟶ x5 x48 ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ x45 x48 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x2 x48 (x1 x11) ⟶ (x27 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ x45 x48 ⟶ (x5 x48 ⟶ False) ⟶ (x36 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ x45 x48 ⟶ (x5 x48 ⟶ False) ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ x36 x48 ⟶ x5 x48 ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ x36 x48 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ x36 x48 ⟶ x47 x48 ⟶ False) ⟶ (∀ x48 . x16 x48 ⟶ (x15 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ x45 x48 ⟶ (x36 x48 ⟶ False) ⟶ (x5 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . (x47 x48 ⟶ False) ⟶ x45 x48 ⟶ (x36 x48 ⟶ False) ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x39 x48 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x16 x48 ⟶ (x27 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ x5 x48 ⟶ x36 x48 ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ x5 x48 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x45 x48 ⟶ x5 x48 ⟶ x47 x48 ⟶ False) ⟶ (∀ x48 . x39 x48 ⟶ (x37 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x25 x48 ⟶ (x16 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x17 x48 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x17 x48 ⟶ (x39 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x18 x48 ⟶ (x25 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x33 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x4 x49 ⟶ x2 x48 (x1 x49) ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x18 x49 ⟶ x2 x48 (x1 x49) ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x25 x49 ⟶ x2 x48 (x1 x49) ⟶ (x25 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x16 x49 ⟶ x2 x48 (x1 x49) ⟶ (x16 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x27 x49 ⟶ x2 x48 (x1 x49) ⟶ (x27 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x2 x48 x11 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x4 x48 ⟶ (x18 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x15 x49 ⟶ x2 x48 (x1 x49) ⟶ (x15 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 . x47 x48 ⟶ (x4 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x4 x49 ⟶ x2 x48 x49 ⟶ (x17 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x18 x49 ⟶ x2 x48 x49 ⟶ (x19 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x25 x49 ⟶ x2 x48 x49 ⟶ (x24 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x16 x49 ⟶ x2 x48 x49 ⟶ (x39 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x27 x49 ⟶ x2 x48 x49 ⟶ (x45 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x15 x49 ⟶ x2 x48 x49 ⟶ (x37 x48 ⟶ False) ⟶ False) ⟶ (∀ x48 x49 . x0 x48 x49 ⟶ x0 x49 x48 ⟶ False) ⟶ ((x42 (x44 x20 x21) (x44 x23 x22) ⟶ False) ⟶ False) ⟶ (x43 x21 x20 ⟶ False) ⟶ (x43 x23 x20 ⟶ False) ⟶ ((x45 x22 ⟶ False) ⟶ False) ⟶ ((x45 x21 ⟶ False) ⟶ False) ⟶ ((x45 x23 ⟶ False) ⟶ False) ⟶ ((x45 x20 ⟶ False) ⟶ False) ⟶ False (proof)