Search for blocks/addresses/...

Proofgold Asset

asset id
19be1c222cc0e0e310cf71f082f6fbe270b60dc2dff0879b2ed5195a8e4c03b3
asset hash
5ad2814c1b2664e9be5740deafdb076c1ab70a45f0530ad3f1db781986fbd964
bday / block
35132
tx
e689d..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0 ⟶ False
Theorem 81bc9.. : ∀ 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 . ∀ x66 : ι → ι → ο . ∀ x67 : ι → ι . ∀ x68 : ι → ο . ∀ x69 . ∀ x70 : ι → ο . ∀ x71 . ∀ x72 : ι → ο . ∀ x73 x74 : ι → ι . ∀ x75 . ∀ x76 : ι → ο . ∀ x77 : ι → ι → ι → ο . ∀ x78 . ∀ x79 : ι → ο . (∀ x80 x81 . x79 x81 ⟶ (x81 = x80 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x79 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x80 = x78 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x80 x81 ⟶ x2 x81 (x1 x82) ⟶ x79 x82 ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x2 x82 (x1 x80) ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x3 x81 x80 ⟶ (x2 x81 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x81 (x1 x80) ⟶ (x3 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 x81 x82 ⟶ x0 x80 x82 ⟶ x0 x80 (x4 x82 x81) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x0 (x4 x80 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x2 x80 x81 ⟶ (x79 x81 ⟶ False) ⟶ (x0 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x81 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x3 x80 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x82) ⟶ x2 x81 x80 ⟶ (x77 x81 x82 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x82) ⟶ x77 x81 x82 x80 ⟶ (x2 x81 x80 ⟶ False) ⟶ False) ⟶ ((x76 x75 ⟶ False) ⟶ False) ⟶ ((x5 x75 ⟶ False) ⟶ False) ⟶ (x79 x75 ⟶ False) ⟶ ((x6 x7 ⟶ False) ⟶ False) ⟶ (x79 x7 ⟶ False) ⟶ (∀ x80 . (x8 x80 ⟶ False) ⟶ (x5 (x9 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x8 x80 ⟶ False) ⟶ x8 (x9 x80) ⟶ False) ⟶ (∀ x80 . (x8 x80 ⟶ False) ⟶ (x2 (x9 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x8 x80 ⟶ False) ⟶ x8 (x74 x80) ⟶ False) ⟶ (∀ x80 . (x8 x80 ⟶ False) ⟶ (x2 (x74 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x8 (x73 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x73 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x73 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x10 x11 ⟶ False) ⟶ False) ⟶ (x79 x11 ⟶ False) ⟶ ((x12 x13 ⟶ False) ⟶ False) ⟶ ((x72 x71 ⟶ False) ⟶ False) ⟶ ((x79 x71 ⟶ False) ⟶ False) ⟶ ((x70 x69 ⟶ False) ⟶ False) ⟶ ((x72 x69 ⟶ False) ⟶ False) ⟶ ((x68 x69 ⟶ False) ⟶ False) ⟶ ((x79 x69 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x66 (x67 x80) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x67 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x10 x65 ⟶ False) ⟶ False) ⟶ ((x14 x15 ⟶ False) ⟶ False) ⟶ ((x72 x15 ⟶ False) ⟶ False) ⟶ ((x70 x16 ⟶ False) ⟶ False) ⟶ ((x14 x16 ⟶ False) ⟶ False) ⟶ ((x72 x16 ⟶ False) ⟶ False) ⟶ ((x68 x16 ⟶ False) ⟶ False) ⟶ (∀ x80 . x66 (x17 x80) x80 ⟶ False) ⟶ (∀ x80 . (x2 (x17 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x18 x19 ⟶ False) ⟶ False) ⟶ ((x72 x19 ⟶ False) ⟶ False) ⟶ ((x70 x20 ⟶ False) ⟶ False) ⟶ ((x18 x20 ⟶ False) ⟶ False) ⟶ ((x72 x20 ⟶ False) ⟶ False) ⟶ ((x68 x20 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 (x21 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x21 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x22 x23 ⟶ False) ⟶ False) ⟶ ((x64 x23 ⟶ False) ⟶ False) ⟶ ((x24 x25 ⟶ False) ⟶ False) ⟶ ((x63 x25 ⟶ False) ⟶ False) ⟶ ((x26 x25 ⟶ False) ⟶ False) ⟶ (x79 x25 ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x5 (x27 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x27 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x27 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x72 x62 ⟶ False) ⟶ False) ⟶ ((x70 x28 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x79 (x61 x80) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ (x2 (x61 x80) (x1 x80) ⟶ False) ⟶ False) ⟶ ((x64 x60 ⟶ False) ⟶ False) ⟶ (x79 x60 ⟶ False) ⟶ ((x24 x59 ⟶ False) ⟶ False) ⟶ ((x29 x30 ⟶ False) ⟶ False) ⟶ ((x58 x30 ⟶ False) ⟶ False) ⟶ ((x5 x31 ⟶ False) ⟶ False) ⟶ (x79 x31 ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x58 x83 ⟶ x2 x80 (x1 (x35 x83)) ⟶ x77 x82 (x34 x83) (x35 x83) ⟶ x81 = x32 x83 x82 ⟶ x0 x82 x80 ⟶ (x0 x81 (x33 x83 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x58 x82 ⟶ x2 x80 (x1 (x35 x82)) ⟶ x0 x81 (x33 x82 x80) ⟶ (x0 (x57 x80 x82 x81) x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x58 x82 ⟶ x2 x80 (x1 (x35 x82)) ⟶ x0 x81 (x33 x82 x80) ⟶ (x81 = x32 x82 (x57 x80 x82 x81) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x58 x82 ⟶ x2 x80 (x1 (x35 x82)) ⟶ x0 x81 (x33 x82 x80) ⟶ (x77 (x57 x80 x82 x81) (x34 x82) (x35 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 . x24 x80 ⟶ (x24 (x36 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x5 x80 ⟶ x76 x80 ⟶ (x5 (x36 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x5 x80 ⟶ (x76 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ x79 (x35 x80) ⟶ False) ⟶ (∀ x80 . x79 (x1 x80) ⟶ False) ⟶ (∀ x80 . x5 x80 ⟶ (x5 (x1 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ (x77 (x37 x80 x81) x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x2 (x56 x80) x80 ⟶ False) ⟶ False) ⟶ ((x58 x38 ⟶ False) ⟶ False) ⟶ ((x79 x55 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . (x79 x82 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ x2 x80 (x1 x82) ⟶ x77 x81 x82 x80 ⟶ (x2 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ x79 (x34 x80) ⟶ False) ⟶ (∀ x80 x81 . x58 x81 ⟶ x2 x80 (x1 (x35 x81)) ⟶ (x2 (x39 x81 x80) (x1 (x40 x81)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ (x2 (x40 x80) (x1 (x54 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 . x58 x80 ⟶ (x2 (x35 x80) (x1 (x34 x80)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x58 x81 ⟶ x2 x80 (x34 x81) ⟶ (x2 (x32 x81 x80) (x1 (x40 x81)) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x58 x81 ⟶ x2 x80 (x1 (x35 x81)) ⟶ (x39 x81 x80 = x36 (x33 x81 x80) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x0 (x53 x81 x80) x80 ⟶ False) ⟶ (x0 (x52 x81 x80) x81 ⟶ False) ⟶ (x81 = x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x0 (x52 x81 x80) (x53 x81 x80) ⟶ False) ⟶ (x0 (x52 x81 x80) x81 ⟶ False) ⟶ (x81 = x36 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x0 (x52 x82 x81) x82 ⟶ x0 (x52 x82 x81) x80 ⟶ x0 x80 x81 ⟶ (x82 = x36 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 x83 . x82 = x36 x83 ⟶ x0 x81 x80 ⟶ x0 x80 x83 ⟶ (x0 x81 x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x81 = x36 x82 ⟶ x0 x80 x81 ⟶ (x0 (x51 x80 x81 x82) x82 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x81 = x36 x82 ⟶ x0 x80 x81 ⟶ (x0 x80 (x51 x80 x81 x82) ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 (x50 x80 x81) x80 ⟶ (x3 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x0 (x50 x80 x81) x81 ⟶ False) ⟶ (x3 x81 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 x82 . x3 x81 x82 ⟶ x0 x80 x81 ⟶ (x0 x80 x82 ⟶ False) ⟶ False) ⟶ ((x78 = x55 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x64 x80 ⟶ (x41 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x64 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x6 x80 ⟶ (x42 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x18 x80 ⟶ False) ⟶ (x14 x80 ⟶ False) ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ (x18 x80 ⟶ False) ⟶ (x14 x80 ⟶ False) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x2 x80 (x1 x81) ⟶ (x76 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x6 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x72 x80 ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x72 x80 ⟶ x18 x80 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x72 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x10 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x76 x81 ⟶ x2 x80 x81 ⟶ (x5 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x29 x81 ⟶ x2 x80 (x1 x81) ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x72 x80 ⟶ (x18 x80 ⟶ False) ⟶ (x14 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x72 x80 ⟶ (x18 x80 ⟶ False) ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x10 x80 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x76 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x5 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x14 x80 ⟶ x18 x80 ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x14 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x14 x80 ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x8 x81 ⟶ x2 x80 (x1 x81) ⟶ (x8 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x24 x81 ⟶ x2 x80 x81 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x5 x80 ⟶ False) ⟶ x8 x80 ⟶ False) ⟶ (∀ x80 . (x5 x80 ⟶ False) ⟶ x29 x80 ⟶ (x12 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x72 x80 ⟶ (x14 x80 ⟶ False) ⟶ (x18 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . (x79 x80 ⟶ False) ⟶ x72 x80 ⟶ (x14 x80 ⟶ False) ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x70 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ x66 x80 x81 ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x64 x80 ⟶ (x22 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x64 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x48 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x8 x80 ⟶ (x5 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ x79 x80 ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ x79 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x12 x80 ⟶ (x29 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x12 x80 ⟶ x5 x80 ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x18 x80 ⟶ x14 x80 ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x18 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x72 x80 ⟶ x18 x80 ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 . x70 x80 ⟶ (x68 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ x79 x80 ⟶ (x66 x80 x81 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x64 x80 ⟶ (x43 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ x64 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x10 x80 ⟶ (x72 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x10 x80 ⟶ (x70 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . (x79 x81 ⟶ False) ⟶ x2 x80 (x1 x81) ⟶ (x66 x80 x81 ⟶ False) ⟶ x79 x80 ⟶ False) ⟶ (∀ x80 x81 . x64 x81 ⟶ x2 x80 (x1 x81) ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x26 x80 ⟶ x63 x80 ⟶ (x24 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x5 x81 ⟶ x2 x80 (x1 x81) ⟶ (x5 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x79 x81 ⟶ x2 x80 (x1 x81) ⟶ (x79 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x24 x80 ⟶ (x63 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x24 x80 ⟶ (x26 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x79 x80 ⟶ (x5 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ x79 x80 ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 . x64 x80 ⟶ x79 x80 ⟶ (x64 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x6 x81 ⟶ x2 x80 (x1 x81) ⟶ (x6 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x49 x81 ⟶ x2 x80 (x1 x81) ⟶ (x49 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x6 x81 ⟶ x2 x80 x81 ⟶ (x47 x80 ⟶ False) ⟶ False) ⟶ (∀ x80 x81 . x0 x80 x81 ⟶ x0 x81 x80 ⟶ False) ⟶ (x3 (x39 x45 x46) (x39 x45 x44) ⟶ False) ⟶ ((x3 x46 x44 ⟶ False) ⟶ False) ⟶ ((x2 x44 (x1 (x35 x45)) ⟶ False) ⟶ False) ⟶ ((x2 x46 (x1 (x35 x45)) ⟶ False) ⟶ False) ⟶ ((x58 x45 ⟶ False) ⟶ False) ⟶ False (proof)