Search for blocks/addresses/...

Proofgold Asset

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