Search for blocks/addresses/...

Proofgold Asset

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