Search for blocks/addresses/...

Proofgold Asset

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