Search for blocks/addresses/...

Proofgold Asset

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