Search for blocks/addresses/...

Proofgold Asset

asset id
489f354410b0455535c52e3146a0d47e9e536972582546e3682bd9adf592a46f
asset hash
43e893e45768ea8cdbea713122b97810e0a56290a335a53d1e1c893b4f718b63
bday / block
35136
tx
003d1..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem da898.. : ∀ 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 : ι → ο . (∀ x56 x57 . x55 x57 ⟶ (x57 = x56 ⟶ False) ⟶ x55 x56 ⟶ False) ⟶ (∀ x56 x57 . (x0 x56 (x1 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x54 x56 x57 ⟶ x55 x57 ⟶ False) ⟶ (∀ x56 . x55 x56 ⟶ (x56 = x2 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x54 x56 x57 ⟶ x52 x57 (x53 x58) ⟶ x55 x58 ⟶ False) ⟶ (∀ x56 x57 x58 . x3 x58 ⟶ x6 x58 ⟶ x4 x57 x58 ⟶ x4 x56 x58 ⟶ x4 x57 x56 ⟶ (x0 (x5 x57) (x5 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x3 x58 ⟶ x6 x58 ⟶ x4 x57 x58 ⟶ x4 x56 x58 ⟶ x0 (x5 x57) (x5 x56) ⟶ (x4 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x54 x57 x58 ⟶ x52 x58 (x53 x56) ⟶ (x52 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x0 x57 x56 ⟶ (x52 x57 (x53 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x52 x57 (x53 x56) ⟶ (x0 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x52 x56 x57 ⟶ (x55 x57 ⟶ False) ⟶ (x54 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x54 x57 x56 ⟶ (x52 x57 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x1 x56 x2 = x56 ⟶ False) ⟶ False) ⟶ (x55 x7 ⟶ False) ⟶ (∀ x56 . (x0 x56 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x8 (x9 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x52 (x9 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ (x12 (x11 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ x55 (x11 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ (x52 (x11 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ x50 (x51 x56) x56 ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ x55 (x51 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ (x52 (x51 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x12 (x13 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x52 (x13 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x50 (x14 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x52 (x14 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x3 (x15 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x49 (x15 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x4 (x15 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x47 x56 ⟶ x55 (x48 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x47 x56 ⟶ (x52 (x48 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x6 x56 ⟶ (x49 (x46 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x6 x56 ⟶ x10 (x46 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x6 x56 ⟶ (x4 (x46 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ (x12 (x16 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ (x45 (x16 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ x55 (x16 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x3 x56 ⟶ x6 x56 ⟶ (x52 (x16 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x49 (x17 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x4 (x17 x56) x56 ⟶ False) ⟶ False) ⟶ (x55 x18 ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x12 (x44 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x45 (x44 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x52 (x44 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ ((x3 x19 ⟶ False) ⟶ False) ⟶ ((x49 x19 ⟶ False) ⟶ False) ⟶ (x10 x19 ⟶ False) ⟶ ((x6 x19 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x20 x56 ⟶ False) ⟶ x47 x56 ⟶ x21 (x22 x56) ⟶ False) ⟶ (∀ x56 . (x20 x56 ⟶ False) ⟶ x47 x56 ⟶ (x52 (x22 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x47 x56 ⟶ (x21 (x23 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x47 x56 ⟶ x55 (x23 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x47 x56 ⟶ (x52 (x23 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ ((x55 x43 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x45 (x24 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x52 (x24 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ ((x49 x25 ⟶ False) ⟶ False) ⟶ ((x6 x25 ⟶ False) ⟶ False) ⟶ ((x3 x26 ⟶ False) ⟶ False) ⟶ ((x49 x26 ⟶ False) ⟶ False) ⟶ ((x10 x26 ⟶ False) ⟶ False) ⟶ ((x6 x26 ⟶ False) ⟶ False) ⟶ ((x49 x27 ⟶ False) ⟶ False) ⟶ ((x10 x27 ⟶ False) ⟶ False) ⟶ ((x6 x27 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x45 (x42 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x52 (x42 x56) (x53 (x5 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x1 x56 x56 = x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x52 x58 (x53 (x53 x59)) ⟶ x28 x59 x58 = x28 x57 x56 ⟶ (x58 = x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . x52 x58 (x53 (x53 x59)) ⟶ x28 x59 x58 = x28 x56 x57 ⟶ (x59 = x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . (x29 x56 ⟶ False) ⟶ x47 x56 ⟶ x30 (x5 x56) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ x52 x56 (x53 (x53 x57)) ⟶ (x49 (x28 x57 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ x52 x56 (x53 (x53 x57)) ⟶ x10 (x28 x57 x56) ⟶ False) ⟶ (∀ x56 . x29 x56 ⟶ x47 x56 ⟶ (x30 (x5 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . x3 x58 ⟶ x6 x58 ⟶ x45 x57 x58 ⟶ x52 x57 (x53 (x5 x58)) ⟶ x45 x56 x58 ⟶ x52 x56 (x53 (x5 x58)) ⟶ (x45 (x1 x57 x56) x58 ⟶ False) ⟶ False) ⟶ (∀ x56 . x20 x56 ⟶ x47 x56 ⟶ (x21 (x5 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x6 x56 ⟶ (x49 (x28 (x5 x56) (x31 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x6 x56 ⟶ x10 (x28 (x5 x56) (x31 x56)) ⟶ False) ⟶ (∀ x56 . (x20 x56 ⟶ False) ⟶ x47 x56 ⟶ x21 (x5 x56) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x3 (x28 (x5 x56) (x31 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ (x49 (x28 (x5 x56) (x31 x56)) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ x55 (x1 x56 x57) ⟶ False) ⟶ (∀ x56 x57 x58 . x3 x58 ⟶ x6 x58 ⟶ x12 x57 x58 ⟶ x52 x57 (x53 (x5 x58)) ⟶ x12 x56 x58 ⟶ x52 x56 (x53 (x5 x58)) ⟶ (x12 (x1 x57 x56) x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x55 x57 ⟶ False) ⟶ x55 (x1 x57 x56) ⟶ False) ⟶ (∀ x56 . (x10 x56 ⟶ False) ⟶ x47 x56 ⟶ x55 (x5 x56) ⟶ False) ⟶ ((x55 x2 ⟶ False) ⟶ False) ⟶ (∀ x56 . x10 x56 ⟶ x47 x56 ⟶ (x55 (x5 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 . x3 x56 ⟶ x6 x56 ⟶ x55 (x31 x56) ⟶ False) ⟶ (∀ x56 . (x52 (x32 x56) x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x4 (x41 x56) x56 ⟶ False) ⟶ False) ⟶ ((x47 x33 ⟶ False) ⟶ False) ⟶ ((x6 x40 ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x52 (x31 x56) (x53 (x53 (x5 x56))) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x6 x57 ⟶ x4 x56 x57 ⟶ (x6 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ (x47 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x10 x58 ⟶ False) ⟶ x6 x58 ⟶ (x10 x57 ⟶ False) ⟶ x4 x57 x58 ⟶ (x10 x56 ⟶ False) ⟶ x4 x56 x58 ⟶ (x4 (x39 x58 x57 x56) x58 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x10 x58 ⟶ False) ⟶ x6 x58 ⟶ (x10 x57 ⟶ False) ⟶ x4 x57 x58 ⟶ (x10 x56 ⟶ False) ⟶ x4 x56 x58 ⟶ (x49 (x39 x58 x57 x56) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x10 x58 ⟶ False) ⟶ x6 x58 ⟶ (x10 x57 ⟶ False) ⟶ x4 x57 x58 ⟶ (x10 x56 ⟶ False) ⟶ x4 x56 x58 ⟶ x10 (x39 x58 x57 x56) ⟶ False) ⟶ (∀ x56 x57 . x52 x57 (x53 (x53 x56)) ⟶ (x6 (x28 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x52 x57 (x53 (x53 x56)) ⟶ (x49 (x28 x56 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . (x10 x59 ⟶ False) ⟶ x6 x59 ⟶ (x10 x58 ⟶ False) ⟶ x4 x58 x59 ⟶ (x10 x57 ⟶ False) ⟶ x4 x57 x59 ⟶ (x10 x56 ⟶ False) ⟶ x49 x56 ⟶ x4 x56 x59 ⟶ x5 x56 = x1 (x5 x58) (x5 x57) ⟶ (x56 = x39 x59 x58 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 x59 . (x10 x59 ⟶ False) ⟶ x6 x59 ⟶ (x10 x58 ⟶ False) ⟶ x4 x58 x59 ⟶ (x10 x57 ⟶ False) ⟶ x4 x57 x59 ⟶ (x10 x56 ⟶ False) ⟶ x49 x56 ⟶ x4 x56 x59 ⟶ x56 = x39 x59 x58 x57 ⟶ (x5 x56 = x1 (x5 x58) (x5 x57) ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . (x1 x57 x56 = x1 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 x58 . (x10 x58 ⟶ False) ⟶ x6 x58 ⟶ (x10 x57 ⟶ False) ⟶ x4 x57 x58 ⟶ (x10 x56 ⟶ False) ⟶ x4 x56 x58 ⟶ (x39 x58 x57 x56 = x39 x58 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x34 x56 x2 ⟶ (x10 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ x10 x56 ⟶ (x38 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x10 x56 ⟶ (x34 x56 x2 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ (x29 x56 ⟶ False) ⟶ x20 x56 ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x45 x56 x57 ⟶ x8 x56 x57 ⟶ (x55 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x20 x56 ⟶ (x29 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x12 x56 x57 ⟶ x50 x56 x57 ⟶ (x8 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ (x29 x56 ⟶ False) ⟶ x29 x56 ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ (x29 x56 ⟶ False) ⟶ x10 x56 ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x8 x56 x57 ⟶ (x50 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x10 x56 ⟶ (x29 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x10 x56 ⟶ (x10 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x55 x56 ⟶ (x8 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x55 x56 ⟶ (x50 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ (x20 x56 ⟶ False) ⟶ x10 x56 ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x55 x56 ⟶ (x12 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x52 x56 (x53 (x5 x57)) ⟶ x55 x56 ⟶ (x45 x56 x57 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x10 x56 ⟶ (x20 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x3 x57 ⟶ x6 x57 ⟶ x4 x56 x57 ⟶ (x3 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ (x20 x56 ⟶ False) ⟶ x10 x56 ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x34 x56 x7 ⟶ (x20 x56 ⟶ False) ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ x34 x56 x7 ⟶ x10 x56 ⟶ False) ⟶ (∀ x56 . x47 x56 ⟶ (x10 x56 ⟶ False) ⟶ x20 x56 ⟶ (x34 x56 x7 ⟶ False) ⟶ False) ⟶ (∀ x56 x57 . x54 x56 x57 ⟶ x54 x57 x56 ⟶ False) ⟶ (∀ x56 . x6 x56 ⟶ x49 x56 ⟶ (x56 = x28 (x5 x56) (x31 x56) ⟶ False) ⟶ False) ⟶ (x4 x37 (x39 x35 x37 x36) ⟶ False) ⟶ ((x4 x36 x35 ⟶ False) ⟶ False) ⟶ (x10 x36 ⟶ False) ⟶ ((x4 x37 x35 ⟶ False) ⟶ False) ⟶ (x10 x37 ⟶ False) ⟶ ((x6 x35 ⟶ False) ⟶ False) ⟶ ((x3 x35 ⟶ False) ⟶ False) ⟶ (x10 x35 ⟶ False) ⟶ False (proof)