Search for blocks/addresses/...

Proofgold Asset

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