Search for blocks/addresses/...

Proofgold Asset

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