Search for blocks/addresses/...

Proofgold Asset

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