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 : ο . x0False
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 = x66False)x65 x66False)(∀ x66 x67 . x0 x66 x67x65 x67False)(∀ x66 . x65 x66(x66 = x64False)False)(∀ x66 x67 x68 . x0 x66 x67x2 x67 (x1 x68)x65 x68False)(∀ x66 . (x63 x66False)x55 x66x62 x66x56 x66x61 x66x57 x66x59 x66 (x59 x66 (x58 x66)) = x58 x66(x60 x66False)False)(∀ x66 . (x63 x66False)x55 x66x62 x66x56 x66x61 x66x57 x66(x2 (x58 x66) (x3 x66)False)(x60 x66False)False)(∀ x66 x67 . (x63 x67False)x55 x67x62 x67x56 x67x61 x67x57 x67x60 x67x2 x66 (x3 x67)(x59 x67 (x59 x67 x66) = x66False)False)(∀ x66 x67 x68 . x0 x67 x68x2 x68 (x1 x66)(x2 x67 x66False)False)(∀ x66 x67 . x54 x67 x66(x2 x67 (x1 x66)False)False)(∀ x66 x67 . x2 x67 (x1 x66)(x54 x67 x66False)False)(∀ x66 x67 . x2 x66 x67(x65 x67False)(x0 x66 x67False)False)(∀ x66 x67 . (x63 x67False)x55 x67x62 x67x56 x67x61 x67x57 x67x2 x66 (x3 x67)(x5 x67 x66 (x4 x67) = x66False)False)(∀ x66 x67 . x0 x67 x66(x2 x67 x66False)False)(x65 x6False)(∀ x66 . (x54 x66 x66False)False)(∀ x66 x67 x68 x69 . x7 x69x10 x69 (x11 x66 x66) x66x2 x69 (x1 (x11 (x11 x66 x66) x66))x2 x67 x66x2 x68 x66(x8 x66 x69 x67 x68 = x9 x69 x67 x68False)False)(∀ x66 . (x65 x66False)(x53 (x52 x66) x6False)False)(∀ x66 . (x65 x66False)(x2 (x52 x66) (x1 x66)False)False)(∀ x66 . x51 x66(x53 (x50 x66) x66False)False)(∀ x66 . x51 x66(x7 (x50 x66)False)False)(∀ x66 . x51 x66(x49 (x50 x66)False)False)(∀ x66 . x51 x66(x53 (x12 x66) x66False)False)(∀ x66 . (x63 x66False)x47 x66x65 (x48 x66)False)(∀ x66 . (x63 x66False)x47 x66(x2 (x48 x66) (x1 (x3 x66))False)False)(∀ x66 . (x46 x66False)x46 (x45 x66)False)(∀ x66 . (x46 x66False)(x2 (x45 x66) (x1 x66)False)False)(x46 x44False)((x13 x14False)False)((x49 x14False)False)(∀ x66 . x51 x66(x16 (x15 x66) x66False)False)(∀ x66 . x51 x66(x47 (x15 x66)False)False)(∀ x66 . (x17 x66False)x47 x66x18 (x19 x66)False)(∀ x66 . (x17 x66False)x47 x66(x2 (x19 x66) (x1 (x3 x66))False)False)(∀ x66 . (x63 x66False)x47 x66(x18 (x20 x66)False)False)(∀ x66 . (x63 x66False)x47 x66x65 (x20 x66)False)(∀ x66 . (x63 x66False)x47 x66(x2 (x20 x66) (x1 (x3 x66))False)False)((x17 x43False)False)(x63 x43False)((x42 x43False)False)((x49 x21False)False)(x65 x21False)((x51 x22False)False)(∀ x66 . (x17 x66False)x42 x66x41 (x40 x66) x66False)(∀ x66 . (x17 x66False)x42 x66(x2 (x40 x66) (x3 x66)False)False)(∀ x66 . x42 x66(x41 (x39 x66) x66False)False)(∀ x66 . x42 x66(x2 (x39 x66) (x3 x66)False)False)(∀ x66 x67 x68 . (x63 x68False)x55 x68x62 x68x56 x68x61 x68x57 x68x60 x68x2 x66 (x3 x68)x2 x67 (x3 x68)(x5 x68 (x59 x68 x67) (x5 x68 (x4 x68) x66) = x5 x68 x66 x67False)False)(∀ x66 . (x23 x66False)x47 x66x46 (x3 x66)False)(∀ x66 . (x46 x66False)x46 (x1 x66)False)(∀ x66 . x23 x66x47 x66(x46 (x3 x66)False)False)(∀ x66 . x17 x66x47 x66(x18 (x3 x66)False)False)(∀ x66 . (x17 x66False)x47 x66x18 (x3 x66)False)(∀ x66 x67 . (x49 (x11 x66 x67)False)False)(∀ x66 . (x63 x66False)x47 x66x65 (x3 x66)False)(∀ x66 . x63 x66x47 x66(x65 (x3 x66)False)False)(∀ x66 x67 . x51 x67x16 x66 x67x47 x66(x53 (x3 x66) x67False)False)(∀ x66 x67 . (x46 x67False)(x65 x66False)x46 (x11 x66 x67)False)(∀ x66 . x42 x66(x41 (x4 x66) x66False)False)(∀ x66 x67 . (x46 x67False)(x65 x66False)x46 (x11 x67 x66)False)(∀ x66 . (x2 (x24 x66) x66False)False)((x42 x38False)False)((x57 x25False)False)((x47 x37False)False)((x26 x27False)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 x35False)False)(∀ x66 . x42 x66(x47 x66False)False)(∀ x66 . x57 x66(x42 x66False)False)(∀ x66 . x57 x66(x26 x66False)False)(∀ x66 . x26 x66(x47 x66False)False)(∀ x66 x67 x68 x69 . x7 x69x10 x69 (x11 x66 x66) x66x2 x69 (x1 (x11 (x11 x66 x66) x66))x2 x67 x66x2 x68 x66(x2 (x8 x66 x69 x67 x68) x66False)False)(∀ x66 . x42 x66(x2 (x4 x66) (x3 x66)False)False)(∀ x66 x67 . (x63 x67False)x57 x67x2 x66 (x3 x67)(x2 (x59 x67 x66) (x3 x67)False)False)(∀ x66 x67 x68 . x26 x68x2 x66 (x3 x68)x2 x67 (x3 x68)(x2 (x5 x68 x66 x67) (x3 x68)False)False)(∀ x66 . x42 x66(x4 x66 = x36 x66False)False)((x64 = x35False)False)(∀ x66 x67 . (x63 x67False)x57 x67x2 x66 (x3 x67)(x59 x67 x66 = x5 x67 (x4 x67) x66False)False)(∀ x66 x67 x68 . x26 x68x2 x66 (x3 x68)x2 x67 (x3 x68)(x5 x68 x66 x67 = x8 (x3 x68) (x28 x68) x66 x67False)False)(∀ x66 . x47 x66x16 x66 x64(x63 x66False)False)(∀ x66 . x53 x66 x6(x18 x66False)False)(∀ x66 . x53 x66 x6x65 x66False)(∀ x66 . x47 x66x63 x66(x16 x66 x64False)False)(∀ x66 . x65 x66(x53 x66 x64False)False)(∀ x66 . x47 x66(x23 x66False)x17 x66False)(∀ x66 . x53 x66 x64(x65 x66False)False)(∀ x66 . x47 x66x17 x66(x23 x66False)False)(∀ x66 . x29 x66x46 x66(x30 x66False)False)(∀ x66 . x47 x66(x23 x66False)x23 x66False)(∀ x66 . x47 x66(x23 x66False)x63 x66False)(∀ x66 . x30 x66(x46 x66False)False)(∀ x66 . x47 x66x63 x66(x23 x66False)False)(∀ x66 . x47 x66x63 x66(x63 x66False)False)(∀ x66 . x65 x66x49 x66(x13 x66False)False)(∀ x66 . x65 x66x49 x66(x49 x66False)False)(∀ x66 . x65 x66x49 x66(x31 x66False)False)(∀ x66 . x65 x66x49 x66(x49 x66False)False)(∀ x66 . x30 x66(x51 x66False)False)(∀ x66 . x47 x66(x17 x66False)x63 x66False)(∀ x66 x67 . x49 x67x2 x66 (x1 x67)(x49 x66False)False)(∀ x66 . x65 x66(x51 x66False)False)(∀ x66 . x47 x66x63 x66(x17 x66False)False)(∀ x66 . x65 x66(x49 x66False)False)(∀ x66 . x51 x66(x29 x66False)False)(∀ x66 . x47 x66(x17 x66False)x63 x66False)(∀ x66 . x47 x66x16 x66 x6(x17 x66False)False)(∀ x66 . x47 x66x16 x66 x6x63 x66False)(∀ x66 . x47 x66(x63 x66False)x17 x66(x16 x66 x6False)False)(∀ x66 . (x65 x66False)x18 x66(x53 x66 x6False)False)(∀ x66 x67 . x0 x66 x67x0 x67 x66False)(∀ x66 x67 . x2 x67 (x3 x34)x2 x66 (x3 x34)(x5 x34 (x59 x34 x66) (x59 x34 x67) = x5 x34 x67 x66False)(x60 x34False)False)(x60 x34x5 x34 (x59 x34 x33) (x59 x34 x32) = x5 x34 x32 x33False)(x60 x34(x2 x33 (x3 x34)False)False)(x60 x34(x2 x32 (x3 x34)False)False)((x57 x34False)False)((x61 x34False)False)((x56 x34False)False)((x62 x34False)False)((x55 x34False)False)(x63 x34False)False (proof)