Search for blocks/addresses/...

Proofgold Asset

asset id
71e590f07014c4d9cb98047a6479b642a38bda5af0446f35265c066145af58c4
asset hash
bab14de3ede4c60b44eca586623ba88fbce3daba65ae34af19b3bd02b0a3b32d
bday / block
35132
tx
f534e..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 716c9.. : ∀ 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 . x56 x58(x58 = x57False)x56 x57False)(∀ x57 x58 x59 x60 . x2 (x1 x60 x59) (x0 x58 x57)(x2 (x1 x59 x60) (x0 x57 x58)False)False)(∀ x57 x58 . x2 x57 x58x56 x58False)(∀ x57 . x56 x57(x57 = x3False)False)(∀ x57 x58 x59 . x2 x57 x58x54 x58 (x55 x59)x56 x59False)(∀ x57 x58 x59 . x2 x58 x59x54 x59 (x55 x57)(x54 x58 x57False)False)(∀ x57 x58 . x53 x58 x57(x54 x58 (x55 x57)False)False)(∀ x57 x58 . x54 x58 (x55 x57)(x53 x58 x57False)False)(∀ x57 x58 . x54 x57 x58(x56 x58False)(x2 x57 x58False)False)(∀ x57 x58 . x2 x58 x57(x54 x58 x57False)False)(∀ x57 . (x53 x57 x57False)False)(∀ x57 . (x4 (x5 x57)False)False)(∀ x57 . (x52 (x5 x57) x57False)False)(∀ x57 . (x6 (x5 x57)False)False)(∀ x57 . (x51 (x5 x57)False)False)((x7 x8False)False)(x56 x8False)(∀ x57 x58 . (x4 (x9 x57 x58)False)False)(∀ x57 x58 . (x50 (x9 x57 x58) x57False)False)(∀ x57 x58 . (x52 (x9 x58 x57) x57False)False)(∀ x57 x58 . (x51 (x9 x57 x58)False)False)(x10 x11False)((x4 x11False)False)((x51 x11False)False)((x4 x49False)False)((x6 x49False)False)((x51 x49False)False)(x56 x49False)(∀ x57 x58 . (x50 (x48 x57 x58) x57False)False)(∀ x57 x58 . (x52 (x48 x58 x57) x57False)False)(∀ x57 x58 . (x51 (x48 x57 x58)False)False)((x4 x12False)False)((x6 x12False)False)((x51 x12False)False)(x47 x46False)(x56 x13False)((x6 x45False)False)((x51 x45False)False)((x44 x43False)False)((x4 x43False)False)((x51 x43False)False)(x56 x14False)((x10 x14False)False)((x4 x14False)False)((x51 x14False)False)((x47 x15False)False)(x56 x15False)((x56 x16False)False)(∀ x57 x58 . (x50 (x42 x57 x58) x57False)False)(∀ x57 x58 . (x52 (x42 x58 x57) x57False)False)(∀ x57 x58 . (x51 (x42 x57 x58)False)False)(∀ x57 x58 . (x56 (x42 x57 x58)False)False)(∀ x57 x58 . (x54 (x42 x57 x58) (x55 (x0 x58 x57))False)False)((x51 x17False)False)(x56 x17False)((x4 x18False)False)((x51 x18False)False)((x19 x20False)False)((x4 x20False)False)((x51 x20False)False)(∀ x57 x58 x59 x60 . x54 x60 (x55 (x0 (x0 x58 x57) x59))(x51 (x41 x60)False)False)(∀ x57 . (x56 x57False)x51 x57x56 (x41 x57)False)(∀ x57 x58 . x51 x58x4 x58x19 x58(x4 (x40 x58 x57)False)False)(∀ x57 x58 . x51 x58x4 x58x19 x58(x51 (x40 x58 x57)False)False)(∀ x57 x58 x59 x60 . (x51 (x39 (x1 x58 x57) (x1 x60 x59))False)False)(∀ x57 x58 . (x51 (x0 x57 x58)False)False)(∀ x57 x58 . (x51 (x38 (x1 x58 x57))False)False)(∀ x57 x58 . x56 x58(x56 (x0 x58 x57)False)False)(∀ x57 x58 . x56 x58(x56 (x0 x57 x58)False)False)(∀ x57 x58 . x56 (x39 x57 x58)False)(∀ x57 . (x47 (x38 x57)False)False)(∀ x57 . x56 (x38 x57)False)(∀ x57 . x47 x57x51 x57(x47 (x41 x57)False)False)(∀ x57 x58 . x56 (x1 x57 x58)False)((x56 x3False)False)(∀ x57 x58 . (x4 (x38 (x1 x58 x57))False)False)(∀ x57 x58 . x51 x58x37 x58x4 x58(x56 (x40 x58 x57)False)False)(∀ x57 . (x47 x57False)x51 x57x4 x57x47 (x41 x57)False)(∀ x57 x58 x59 . x7 x59x51 x57x50 x57 x59x4 x57(x4 (x40 x57 x58)False)False)(∀ x57 x58 x59 . x7 x59x51 x57x50 x57 x59x4 x57(x51 (x40 x57 x58)False)False)(∀ x57 x58 . x51 x58x4 x58x51 x57x4 x57(x7 (x39 x58 x57)False)False)(∀ x57 . x51 x57x4 x57(x7 (x38 x57)False)False)(∀ x57 x58 . (x56 x58False)x51 x58x6 x58x4 x58x54 x57 (x41 x58)x56 (x40 x58 x57)False)(∀ x57 . x56 x57(x56 (x41 x57)False)False)(∀ x57 . (x54 (x36 x57) x57False)False)((x56 x21False)False)(∀ x57 . x51 x57x4 x57(x4 (x35 x57)False)False)(∀ x57 . x51 x57x4 x57(x51 (x35 x57)False)False)(∀ x57 x58 . (x1 x58 x57 = x39 (x39 x58 x57) (x38 x58)False)False)(∀ x57 x58 . x2 (x22 x57 x58) x57(x53 x58 x57False)False)(∀ x57 x58 . (x2 (x22 x57 x58) x58False)(x53 x58 x57False)False)(∀ x57 x58 x59 . x53 x58 x59x2 x57 x58(x2 x57 x59False)False)((x3 = x21False)False)(∀ x57 x58 . x51 x58x4 x58x51 x57x4 x57(x2 (x1 (x23 x57 x58) (x24 x57 x58)) (x41 x58)False)(x2 (x28 x57 x58) (x41 x57)False)x25 x57 (x26 x57 x58) (x27 x57 x58) = x25 x58 (x27 x57 x58) (x26 x57 x58)(x57 = x35 x58False)False)(∀ x57 x58 . x51 x58x4 x58x51 x57x4 x57(x2 (x1 (x23 x57 x58) (x24 x57 x58)) (x41 x58)False)(x2 (x28 x57 x58) (x41 x57)False)(x2 (x1 (x27 x57 x58) (x26 x57 x58)) (x41 x58)False)(x57 = x35 x58False)False)(∀ x57 x58 . x51 x58x4 x58x51 x57x4 x57(x28 x57 x58 = x1 (x24 x57 x58) (x23 x57 x58)False)(x2 (x28 x57 x58) (x41 x57)False)x25 x57 (x26 x57 x58) (x27 x57 x58) = x25 x58 (x27 x57 x58) (x26 x57 x58)(x57 = x35 x58False)False)(∀ x57 x58 . x51 x58x4 x58x51 x57x4 x57(x28 x57 x58 = x1 (x24 x57 x58) (x23 x57 x58)False)(x2 (x28 x57 x58) (x41 x57)False)(x2 (x1 (x27 x57 x58) (x26 x57 x58)) (x41 x58)False)(x57 = x35 x58False)False)(∀ x57 x58 x59 x60 . x51 x60x4 x60x51 x59x4 x59x2 (x28 x59 x60) (x41 x59)x28 x59 x60 = x1 x57 x58x2 (x1 x58 x57) (x41 x60)x25 x59 (x26 x59 x60) (x27 x59 x60) = x25 x60 (x27 x59 x60) (x26 x59 x60)(x59 = x35 x60False)False)(∀ x57 x58 x59 x60 . x51 x60x4 x60x51 x59x4 x59x2 (x28 x59 x60) (x41 x59)x28 x59 x60 = x1 x57 x58x2 (x1 x58 x57) (x41 x60)(x2 (x1 (x27 x59 x60) (x26 x59 x60)) (x41 x60)False)(x59 = x35 x60False)False)(∀ x57 x58 x59 x60 . x51 x60x4 x60x51 x59x4 x59x59 = x35 x60x2 (x1 x57 x58) (x41 x60)(x25 x59 x58 x57 = x25 x60 x57 x58False)False)(∀ x57 x58 x59 x60 x61 . x51 x61x4 x61x51 x60x4 x60x60 = x35 x61x57 = x1 x59 x58x2 (x1 x58 x59) (x41 x61)(x2 x57 (x41 x60)False)False)(∀ x57 x58 x59 . x51 x59x4 x59x51 x58x4 x58x58 = x35 x59x2 x57 (x41 x58)(x2 (x1 (x30 x57 x58 x59) (x29 x57 x58 x59)) (x41 x59)False)False)(∀ x57 x58 x59 . x51 x59x4 x59x51 x58x4 x58x58 = x35 x59x2 x57 (x41 x58)(x57 = x1 (x29 x57 x58 x59) (x30 x57 x58 x59)False)False)(∀ x57 x58 x59 . x51 x59x4 x59(x25 x59 x57 x58 = x40 x59 (x1 x57 x58)False)False)(∀ x57 x58 . (x39 x58 x57 = x39 x57 x58False)False)(∀ x57 x58 . x7 x58x54 x57 (x55 x58)(x7 x57False)False)(∀ x57 x58 . x56 x58x51 x57x50 x57 x58(x50 x57 x58False)False)(∀ x57 x58 . x56 x58x51 x57x50 x57 x58(x51 x57False)False)(∀ x57 x58 . x56 x58x51 x57x50 x57 x58(x56 x57False)False)(∀ x57 x58 . x7 x58x54 x57 x58(x4 x57False)False)(∀ x57 x58 . x7 x58x54 x57 x58(x51 x57False)False)(∀ x57 x58 . x56 x58x51 x57x52 x57 x58(x52 x57 x58False)False)(∀ x57 x58 . x56 x58x51 x57x52 x57 x58(x51 x57False)False)(∀ x57 x58 . x56 x58x51 x57x52 x57 x58(x56 x57False)False)(∀ x57 . x56 x57(x7 x57False)False)(∀ x57 x58 x59 . x51 x59x50 x59 x57x54 x58 (x55 x59)(x50 x58 x57False)False)(∀ x57 . x47 x57x51 x57x4 x57(x10 x57False)False)(∀ x57 . x47 x57x51 x57x4 x57(x4 x57False)False)(∀ x57 . x47 x57x51 x57x4 x57(x51 x57False)False)(∀ x57 x58 x59 . x51 x59x52 x59 x57x54 x58 (x55 x59)(x52 x58 x57False)False)(∀ x57 . x51 x57x4 x57(x10 x57False)(x4 x57False)False)(∀ x57 . x51 x57x4 x57(x10 x57False)(x51 x57False)False)(∀ x57 . x51 x57x4 x57(x10 x57False)x47 x57False)(∀ x57 x58 x59 . x56 x59x54 x57 (x55 (x0 x58 x59))(x56 x57False)False)(∀ x57 . x56 x57x51 x57(x6 x57False)False)(∀ x57 . x56 x57x51 x57(x51 x57False)False)(∀ x57 . x56 x57x51 x57x4 x57(x10 x57False)False)(∀ x57 . x56 x57x51 x57x4 x57(x4 x57False)False)(∀ x57 . x56 x57x51 x57x4 x57(x51 x57False)False)(∀ x57 x58 x59 . x56 x59x54 x57 (x55 (x0 x59 x58))(x56 x57False)False)(∀ x57 . x56 x57x51 x57(x37 x57False)False)(∀ x57 . x56 x57x51 x57(x51 x57False)False)(∀ x57 x58 . x51 x58x4 x58x54 x57 (x55 x58)(x4 x57False)False)(∀ x57 . x51 x57x4 x57x56 x57(x19 x57False)False)(∀ x57 . x51 x57x4 x57x56 x57(x4 x57False)False)(∀ x57 . x51 x57x4 x57x56 x57(x51 x57False)False)(∀ x57 . (x47 x57False)x56 x57False)(∀ x57 x58 x59 . x54 x59 (x55 (x0 x57 x58))(x50 x59 x58False)False)(∀ x57 x58 x59 . x54 x59 (x55 (x0 x58 x57))(x52 x59 x58False)False)(∀ x57 x58 . x51 x58x54 x57 (x55 x58)(x51 x57False)False)(∀ x57 . x56 x57x51 x57x4 x57(x44 x57False)False)(∀ x57 . x56 x57x51 x57x4 x57(x4 x57False)False)(∀ x57 . x56 x57x51 x57x4 x57(x51 x57False)False)(∀ x57 . x51 x57x4 x57x19 x57(x31 x57False)False)(∀ x57 . x51 x57x4 x57x19 x57(x4 x57False)False)(∀ x57 . x51 x57x4 x57x19 x57(x51 x57False)False)(∀ x57 . x56 x57(x47 x57False)False)(∀ x57 x58 x59 . x54 x59 (x55 (x0 x57 x58))(x51 x59False)False)(∀ x57 . x56 x57(x51 x57False)False)(∀ x57 . x56 x57(x4 x57False)False)(∀ x57 x58 . x7 x58x51 x57x50 x57 x58x4 x57(x19 x57False)False)(∀ x57 x58 . x7 x58x51 x57x50 x57 x58x4 x57(x4 x57False)False)(∀ x57 x58 . x7 x58x51 x57x50 x57 x58x4 x57(x51 x57False)False)(∀ x57 x58 . x2 x57 x58x2 x58 x57False)(x53 (x41 (x35 x32)) (x0 x33 x34)False)((x53 (x41 x32) (x0 x34 x33)False)False)((x4 x32False)False)((x51 x32False)False)False (proof)