Search for blocks/addresses/...

Proofgold Asset

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