Search for blocks/addresses/...

Proofgold Signed Transaction

vin
PrNUD../f53f1..
PUKmx../67dc5..
vout
PrNUD../28ba4.. 0.03 bars
TMbz3../f1c90.. ownership of 57aa9.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
TMPof../bc53b.. ownership of 1a260.. as prop with payaddr PrPhD.. rights free controlledby PrPhD.. upto 0
PUWgR../90e73.. doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 57aa9.. : ∀ 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 . (x37 x42 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x42 x36 ⟶ x27 x38 (x29 (x28 x42 x36)) ⟶ x26 x41 ⟶ x35 x41 x42 x36 ⟶ x27 x41 (x29 (x28 x42 x36)) ⟶ x27 x39 (x29 (x30 x42)) ⟶ x34 x40 x42 ⟶ x31 x42 x38 x41 ⟶ (x31 x42 (x33 x42 x38 x39 x40) (x32 x42 x41 x39 x40) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x37 x39 ⟶ (x39 = x38 ⟶ False) ⟶ x37 x38 ⟶ False) ⟶ (∀ x38 x39 . x25 x38 x39 ⟶ x37 x39 ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x38 = x0 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . x25 x38 x39 ⟶ x27 x39 (x29 x40) ⟶ x37 x40 ⟶ False) ⟶ (∀ x38 x39 x40 . x25 x39 x40 ⟶ x27 x40 (x29 x38) ⟶ (x27 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x24 x39 x38 ⟶ (x27 x39 (x29 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x27 x39 (x29 x38) ⟶ (x24 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x27 x38 x39 ⟶ (x37 x39 ⟶ False) ⟶ (x25 x38 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x25 x39 x38 ⟶ (x27 x39 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 x42 . (x37 x42 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x42 x36 ⟶ x27 x38 (x29 (x28 x42 x36)) ⟶ x27 x41 (x29 (x30 x42)) ⟶ x34 x39 x42 ⟶ x34 x40 x42 ⟶ x22 x41 x42 ⟶ (x23 x42 x36 (x33 x42 (x33 x42 x38 x41 x39) x41 x40) (x33 x42 (x33 x42 x38 x41 x40) x41 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 x42 . (x37 x42 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x42 x36 ⟶ x27 x38 (x29 (x28 x42 x36)) ⟶ x26 x41 ⟶ x35 x41 x42 x36 ⟶ x27 x41 (x29 (x28 x42 x36)) ⟶ x27 x39 (x29 (x30 x42)) ⟶ x34 x40 x42 ⟶ x31 x42 x38 x41 ⟶ (x31 x42 (x33 x42 x38 x39 x40) (x33 x42 x41 x39 x40) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x26 x41 ⟶ x35 x41 x38 x39 ⟶ x27 x41 (x29 (x28 x38 x39)) ⟶ x26 x40 ⟶ x35 x40 x38 x39 ⟶ x27 x40 (x29 (x28 x38 x39)) ⟶ x23 x38 x39 x41 x40 ⟶ (x23 x38 x39 x40 x41 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x26 x41 ⟶ x35 x41 x38 x39 ⟶ x27 x41 (x29 (x28 x38 x39)) ⟶ x26 x40 ⟶ x35 x40 x38 x39 ⟶ x27 x40 (x29 (x28 x38 x39)) ⟶ (x23 x38 x39 x41 x41 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x24 x38 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 . (x37 x40 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x40 x36 ⟶ x27 x38 (x29 (x28 x40 x36)) ⟶ x26 x39 ⟶ x35 x39 x40 x36 ⟶ x27 x39 (x29 (x28 x40 x36)) ⟶ (x31 x40 x38 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x26 x41 ⟶ x35 x41 x38 x39 ⟶ x27 x41 (x29 (x28 x38 x39)) ⟶ x26 x40 ⟶ x35 x40 x38 x39 ⟶ x27 x40 (x29 (x28 x38 x39)) ⟶ x41 = x40 ⟶ (x23 x38 x39 x41 x40 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . x26 x41 ⟶ x35 x41 x38 x39 ⟶ x27 x41 (x29 (x28 x38 x39)) ⟶ x26 x40 ⟶ x35 x40 x38 x39 ⟶ x27 x40 (x29 (x28 x38 x39)) ⟶ x23 x38 x39 x41 x40 ⟶ (x41 = x40 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x21 x38 = x29 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x30 x38 = x1 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x19 (x20 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ x37 (x20 x38) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x34 (x20 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x2 (x3 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 (x3 x38) ⟶ False) ⟶ (∀ x38 . (x27 (x3 x38) (x29 (x29 (x21 x38))) ⟶ False) ⟶ False) ⟶ (x37 x18 ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x19 (x4 x38) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ x37 (x4 x38) ⟶ False) ⟶ (∀ x38 . (x37 x38 ⟶ False) ⟶ (x34 (x4 x38) x38 ⟶ False) ⟶ False) ⟶ ((x37 x17 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x2 (x5 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x27 (x5 x38) (x29 (x29 (x21 x38))) ⟶ False) ⟶ False) ⟶ (x37 x36 ⟶ False) ⟶ ((x37 x0 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x27 (x6 x38) x38 ⟶ False) ⟶ False) ⟶ (∀ x38 . (x34 (x16 x38) x38 ⟶ False) ⟶ False) ⟶ ((x37 x7 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x34 x39 x38 ⟶ (x27 x39 (x29 (x29 x38)) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x27 (x21 x38) (x29 (x29 x38)) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x37 x41 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x41 x36 ⟶ x27 x38 (x29 (x28 x41 x36)) ⟶ x27 x40 (x29 (x30 x41)) ⟶ x34 x39 x41 ⟶ (x27 (x32 x41 x38 x40 x39) (x29 (x28 x41 x36)) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x37 x41 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x41 x36 ⟶ x27 x38 (x29 (x28 x41 x36)) ⟶ x27 x40 (x29 (x30 x41)) ⟶ x34 x39 x41 ⟶ (x35 (x32 x41 x38 x40 x39) x41 x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x37 x41 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x41 x36 ⟶ x27 x38 (x29 (x28 x41 x36)) ⟶ x27 x40 (x29 (x30 x41)) ⟶ x34 x39 x41 ⟶ (x26 (x32 x41 x38 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x37 x41 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x41 x36 ⟶ x27 x38 (x29 (x28 x41 x36)) ⟶ x27 x40 (x29 (x30 x41)) ⟶ x34 x39 x41 ⟶ (x27 (x33 x41 x38 x40 x39) (x29 (x28 x41 x36)) ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x37 x41 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x41 x36 ⟶ x27 x38 (x29 (x28 x41 x36)) ⟶ x27 x40 (x29 (x30 x41)) ⟶ x34 x39 x41 ⟶ (x35 (x33 x41 x38 x40 x39) x41 x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 x40 x41 . (x37 x41 ⟶ False) ⟶ x26 x38 ⟶ x35 x38 x41 x36 ⟶ x27 x38 (x29 (x28 x41 x36)) ⟶ x27 x40 (x29 (x30 x41)) ⟶ x34 x39 x41 ⟶ (x26 (x33 x41 x38 x40 x39) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x27 (x30 x38) (x29 (x29 (x21 x38))) ⟶ False) ⟶ False) ⟶ (∀ x38 . (x2 (x30 x38) x38 ⟶ False) ⟶ False) ⟶ ((x0 = x7 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x27 x39 (x29 (x28 x38 x36)) ⟶ x26 x39 ⟶ x35 x39 x38 x36 ⟶ (x8 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x27 x39 (x29 (x28 x38 x36)) ⟶ x26 x39 ⟶ x35 x39 x38 x36 ⟶ (x35 x39 x38 x36 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x27 x39 (x29 (x28 x38 x36)) ⟶ x26 x39 ⟶ x35 x39 x38 x36 ⟶ (x26 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 . x27 x38 x36 ⟶ (x15 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . x34 x39 x38 ⟶ (x19 x39 ⟶ False) ⟶ False) ⟶ (∀ x38 . x37 x38 ⟶ (x14 x38 ⟶ False) ⟶ False) ⟶ (∀ x38 x39 . (x37 x39 ⟶ False) ⟶ x34 x38 x39 ⟶ x37 x38 ⟶ False) ⟶ (∀ x38 x39 . x25 x38 x39 ⟶ x25 x39 x38 ⟶ False) ⟶ (x31 x9 (x33 x9 (x33 x9 x10 x12 x11) x12 x13) (x33 x9 (x32 x9 x10 x12 x13) x12 x11) ⟶ False) ⟶ ((x22 x12 x9 ⟶ False) ⟶ False) ⟶ ((x34 x13 x9 ⟶ False) ⟶ False) ⟶ ((x34 x11 x9 ⟶ False) ⟶ False) ⟶ ((x27 x12 (x29 (x30 x9)) ⟶ False) ⟶ False) ⟶ ((x27 x10 (x29 (x28 x9 x36)) ⟶ False) ⟶ False) ⟶ ((x35 x10 x9 x36 ⟶ False) ⟶ False) ⟶ ((x26 x10 ⟶ False) ⟶ False) ⟶ (x37 x9 ⟶ False) ⟶ False (proof)