Search for blocks/addresses/...

Proofgold Asset

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