Search for blocks/addresses/...

Proofgold Asset

asset id
82877fbf63b105e5b745cb58d19d6b42094b156244641fd3955a95cabcb1dfac
asset hash
95b5b0f8d58521b6b962896da279a141d6ccce4335ed657c4321e2192763619c
bday / block
35159
tx
8ac18..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 0497a.. : ∀ 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 . x64 x66x64 x65(x63 x66 x65False)(x62 x65False)(x61 x66False)False)(∀ x65 x66 . x0 x66(x66 = x65False)x0 x65False)(∀ x65 x66 . x64 x66x64 x65(x63 x66 x65False)(x61 x66False)(x62 x65False)False)(∀ x65 x66 . x1 x65 x66x0 x66False)(∀ x65 x66 . x64 x66x64 x65x63 x66 x65(x0 x66False)(x61 x65False)(x62 x66False)False)(∀ x65 . x0 x65(x65 = x2False)False)(∀ x65 x66 . x60 x66x60 x65x66 = x65(x58 (x57 x66 x65) = x59False)False)(∀ x65 x66 . x60 x66x60 x65x58 (x57 x66 x65) = x59(x66 = x65False)False)(∀ x65 x66 x67 . x1 x65 x66x55 x66 (x56 x67)x0 x67False)(∀ x65 x66 . x64 x66x64 x65x63 x66 x65(x0 x65False)(x62 x66False)(x61 x65False)False)(∀ x65 x66 x67 . x1 x66 x67x55 x67 (x56 x65)(x55 x66 x65False)False)(∀ x65 x66 . x64 x66x64 x65x63 x66 x65(x61 x65False)x61 x66False)(∀ x65 . x60 x65(x57 x65 x59 = x65False)False)(∀ x65 x66 . x3 x66 x65(x55 x66 (x56 x65)False)False)(∀ x65 x66 . x55 x66 (x56 x65)(x3 x66 x65False)False)(∀ x65 x66 . x64 x66x64 x65x63 x66 x65(x62 x66False)x62 x65False)(∀ x65 . x60 x65(x54 x53 x65 = x65False)False)(∀ x65 x66 . x55 x65 x66(x0 x66False)(x1 x65 x66False)False)(∀ x65 x66 . x64 x66x64 x65x63 x66 x65x62 x65(x62 x66False)False)(∀ x65 . x60 x65(x54 x65 x59 = x59False)False)(∀ x65 x66 . x1 x66 x65(x55 x66 x65False)False)(∀ x65 x66 . x64 x66x64 x65x63 x66 x65x61 x66(x61 x65False)False)((x55 x2 x52False)False)(∀ x65 . x60 x65(x4 x65 x59 = x65False)False)(∀ x65 x66 . x60 x66x60 x65(x57 (x51 x66) (x51 x65) = x57 x65 x66False)False)(∀ x65 x66 . x60 x66x60 x65(x4 (x51 x66) (x51 x65) = x51 (x4 x66 x65)False)False)(∀ x65 x66 x67 . x60 x67x60 x65x60 x66(x54 (x54 x67 x65) x66 = x54 x67 (x54 x65 x66)False)False)(∀ x65 x66 x67 . x60 x67x60 x65x60 x66(x4 (x4 x67 x65) x66 = x4 x67 (x4 x65 x66)False)False)(∀ x65 x66 x67 . x60 x67x60 x65x60 x66(x54 (x4 x67 x65) x66 = x4 (x54 x67 x66) (x54 x65 x66)False)False)((x55 x6 x5False)False)((x55 x6 x50False)False)((x7 x6 x5 x50False)False)((x61 x6False)False)(x0 x6False)(∀ x65 . x60 x65(x54 x65 (x51 x53) = x51 x65False)False)((x55 x53 x5False)False)((x55 x53 x50False)False)((x7 x53 x5 x50False)False)((x61 x53False)False)(x0 x53False)(∀ x65 x66 . x60 x66x60 x65(x4 x66 (x51 x65) = x57 x66 x65False)False)((x55 x8 x5False)False)((x55 x8 x50False)False)((x7 x8 x5 x50False)False)((x0 x8False)False)((x51 (x51 x6) = x6False)False)((x51 (x51 x53) = x53False)False)((x51 x6 = x51 x6False)False)((x51 x53 = x51 x53False)False)((x51 x8 = x8False)False)((x54 (x51 x6) x53 = x51 x6False)False)((x54 (x51 x6) x8 = x8False)False)((x54 x6 x53 = x6False)False)((x54 x6 x8 = x8False)False)((x54 x53 (x51 x6) = x51 x6False)False)((x54 x53 x6 = x6False)False)((x54 x53 x53 = x53False)False)((x54 x53 x8 = x8False)False)((x54 x8 (x51 x6) = x8False)False)((x54 x8 x6 = x8False)False)((x54 x8 x53 = x8False)False)((x54 x8 x8 = x8False)False)((x57 (x51 x6) (x51 x6) = x8False)False)((x57 (x51 x6) (x51 x53) = x51 x53False)False)((x57 (x51 x6) x8 = x51 x6False)False)((x57 (x51 x53) (x51 x6) = x53False)False)((x57 (x51 x53) (x51 x53) = x8False)False)((x57 (x51 x53) x53 = x51 x6False)False)((x57 (x51 x53) x8 = x51 x53False)False)((x57 x6 x6 = x8False)False)((x57 x6 x53 = x53False)False)((x57 x6 x8 = x6False)False)((x57 x53 (x51 x53) = x6False)False)((x57 x53 x6 = x51 x53False)False)((x57 x53 x53 = x8False)False)((x57 x53 x8 = x53False)False)((x57 x8 (x51 x6) = x6False)False)((x57 x8 (x51 x53) = x53False)False)((x57 x8 x6 = x51 x6False)False)((x57 x8 x53 = x51 x53False)False)((x57 x8 x8 = x8False)False)((x4 (x51 x6) x6 = x8False)False)((x4 (x51 x6) x53 = x51 x53False)False)((x4 (x51 x53) (x51 x53) = x51 x6False)False)((x4 (x51 x53) x6 = x53False)False)((x4 (x51 x53) x53 = x8False)False)((x4 (x51 x53) x8 = x51 x53False)False)((x4 x6 (x51 x6) = x8False)False)((x4 x6 (x51 x53) = x53False)False)((x4 x6 x8 = x6False)False)((x4 x53 (x51 x6) = x51 x53False)False)((x4 x53 (x51 x53) = x8False)False)((x4 x53 x53 = x6False)False)((x4 x53 x8 = x53False)False)((x4 x8 (x51 x6) = x51 x6False)False)((x4 x8 (x51 x53) = x51 x53False)False)((x4 x8 x6 = x6False)False)((x4 x8 x53 = x53False)False)((x4 x8 x8 = x8False)False)((x63 (x51 x6) (x51 x6)False)False)((x63 (x51 x6) (x51 x53)False)False)((x63 (x51 x6) x6False)False)((x63 (x51 x6) x53False)False)((x63 (x51 x6) x8False)False)(x63 (x51 x53) (x51 x6)False)((x63 (x51 x53) (x51 x53)False)False)((x63 (x51 x53) x6False)False)((x63 (x51 x53) x53False)False)((x63 (x51 x53) x8False)False)(x63 x6 (x51 x6)False)(x63 x6 (x51 x53)False)((x63 x6 x6False)False)(x63 x6 x53False)(x63 x6 x8False)(x63 x53 (x51 x6)False)(x63 x53 (x51 x53)False)((x63 x53 x6False)False)((x63 x53 x53False)False)(x63 x53 x8False)(x63 x8 (x51 x6)False)(x63 x8 (x51 x53)False)((x63 x8 x6False)False)((x63 x8 x53False)False)((x63 x8 x8False)False)(∀ x65 x66 . x49 x66x49 x65(x63 x66 x66False)False)(∀ x65 . (x3 x65 x65False)False)(∀ x65 x66 x67 . (x0 x67False)(x0 x65False)x55 x65 (x56 x67)x55 x66 x65(x7 x66 x67 x65False)False)(∀ x65 x66 x67 . (x0 x67False)(x0 x65False)x55 x65 (x56 x67)x7 x66 x67 x65(x55 x66 x65False)False)(∀ x65 . x55 x65 x5(x48 x65 = x47 x65False)False)(∀ x65 x66 . x55 x66 x5x64 x65(x9 x66 x65 = x4 x66 x65False)False)((x59 = x2False)False)(∀ x65 . x55 x65 x5(x10 x65 = x11 x65False)False)((x50 = x52False)False)(∀ x65 . x60 x65(x13 x65 = x12 x65False)False)(∀ x65 . x60 x65(x45 x65 = x46 x65False)False)(∀ x65 . x60 x65(x58 x65 = x14 x65False)False)((x49 x44False)False)((x0 x44False)False)((x64 x43False)False)((x49 x43False)False)((x60 x43False)False)((x0 x43False)False)((x62 x42False)False)((x49 x42False)False)((x64 x41False)False)((x62 x41False)False)((x49 x41False)False)((x60 x41False)False)((x40 x39False)False)((x15 x39False)False)(x0 x39False)((x61 x16False)False)((x49 x16False)False)((x64 x17False)False)((x61 x17False)False)((x49 x17False)False)((x60 x17False)False)((x60 x18False)False)(x0 x18False)(x0 x19False)((x15 x38False)False)(x0 x38False)((x49 x37False)False)((x64 x20False)False)((x60 x36False)False)((x0 x21False)False)((x15 x35False)False)(x0 x35False)(∀ x65 . x60 x65(x58 (x58 x65) = x58 x65False)False)(∀ x65 . x60 x65(x14 (x14 x65) = x14 x65False)False)(∀ x65 . x60 x65(x51 (x51 x65) = x65False)False)(∀ x65 x66 . (x62 x66False)x64 x66(x62 x65False)x64 x65x62 (x4 x66 x65)False)(∀ x65 x66 . (x0 x66False)x60 x66(x0 x65False)x60 x65x0 (x54 x66 x65)False)(x22 x5False)(∀ x65 x66 . x64 x66x64 x65(x64 (x57 x66 x65)False)False)(∀ x65 x66 . x64 x66x64 x65(x64 (x54 x66 x65)False)False)(∀ x65 . (x0 x65False)x60 x65(x60 (x51 x65)False)False)(∀ x65 . (x0 x65False)x60 x65x0 (x51 x65)False)((x15 x52False)False)(∀ x65 x66 . x64 x66x64 x65(x64 (x4 x66 x65)False)False)(∀ x65 . x60 x65x62 (x14 x65)False)(∀ x65 . x60 x65(x64 (x14 x65)False)False)((x40 x52False)False)((x40 x5False)False)(∀ x65 x66 . x60 x66x60 x65(x60 (x57 x66 x65)False)False)(∀ x65 . (x0 x65False)x60 x65(x64 (x14 x65)False)False)(∀ x65 . (x0 x65False)x60 x65x0 (x14 x65)False)(∀ x65 . x64 x65(x64 (x51 x65)False)False)(∀ x65 . x64 x65(x60 (x51 x65)False)False)(∀ x65 x66 . x60 x66x60 x65(x60 (x54 x66 x65)False)False)((x34 x5False)False)((x64 (x14 x59)False)False)((x0 (x14 x59)False)False)(∀ x65 x66 . x60 x66x60 x65(x60 (x4 x66 x65)False)False)(∀ x65 . x64 x65(x64 (x11 x65)False)False)(∀ x65 . x60 x65(x64 (x12 x65)False)False)(∀ x65 x66 . (x62 x66False)x64 x66(x62 x65False)x64 x65x62 (x54 x66 x65)False)(∀ x65 x66 . (x61 x66False)x64 x66(x61 x65False)x64 x65x62 (x54 x66 x65)False)(∀ x65 x66 . (x61 x66False)x64 x66(x62 x65False)x64 x65x61 (x54 x65 x66)False)(∀ x65 x66 . (x61 x66False)x64 x66(x62 x65False)x64 x65x61 (x54 x66 x65)False)(∀ x65 x66 . x62 x66x64 x66(x62 x65False)x64 x65(x61 (x57 x65 x66)False)False)(∀ x65 x66 . x62 x66x64 x66(x62 x65False)x64 x65(x62 (x57 x66 x65)False)False)(∀ x65 x66 . x61 x66x64 x66(x61 x65False)x64 x65(x62 (x57 x65 x66)False)False)((x0 x2False)False)(∀ x65 . x60 x65(x60 (x11 x65)False)False)(x0 x5False)(∀ x65 . x60 x65(x64 (x46 x65)False)False)(∀ x65 x66 . x61 x66x64 x66(x61 x65False)x64 x65(x61 (x57 x66 x65)False)False)(∀ x65 x66 . (x62 x66False)x64 x66(x61 x65False)x64 x65x61 (x57 x65 x66)False)(∀ x65 x66 . (x62 x66False)x64 x66(x61 x65False)x64 x65x62 (x57 x66 x65)False)(∀ x65 . (x62 x65False)x64 x65x61 (x51 x65)False)(∀ x65 . (x62 x65False)x64 x65(x60 (x51 x65)False)False)(∀ x65 . (x61 x65False)x64 x65x62 (x51 x65)False)(∀ x65 . (x61 x65False)x64 x65(x60 (x51 x65)False)False)(∀ x65 x66 . x62 x66x64 x66(x61 x65False)x64 x65(x62 (x4 x65 x66)False)False)(∀ x65 x66 . x62 x66x64 x66(x61 x65False)x64 x65(x62 (x4 x66 x65)False)False)(∀ x65 x66 . x61 x66x64 x66(x62 x65False)x64 x65(x61 (x4 x65 x66)False)False)(∀ x65 x66 . x61 x66x64 x66(x62 x65False)x64 x65(x61 (x4 x66 x65)False)False)(∀ x65 x66 . (x61 x66False)x64 x66(x61 x65False)x64 x65x61 (x4 x66 x65)False)(∀ x65 x66 . (x0 x66False)(x0 x65False)x55 x65 (x56 x66)(x7 (x23 x65 x66) x66 x65False)False)(∀ x65 . (x55 (x33 x65) x65False)False)(∀ x65 x66 x67 . (x0 x67False)(x0 x65False)x55 x65 (x56 x67)x7 x66 x67 x65(x55 x66 x67False)False)(∀ x65 . x55 x65 x5(x55 (x48 x65) x5False)False)(∀ x65 x66 . x55 x66 x5x64 x65(x55 (x9 x66 x65) x5False)False)(∀ x65 . x64 x65(x64 (x47 x65)False)False)((x7 x59 x5 x50False)False)(∀ x65 . x55 x65 x5(x55 (x10 x65) x5False)False)((x55 x50 (x56 x5)False)False)(∀ x65 . x60 x65(x60 (x51 x65)False)False)(∀ x65 . x60 x65(x55 (x13 x65) x5False)False)(∀ x65 . x60 x65(x55 (x45 x65) x5False)False)(∀ x65 . x60 x65(x55 (x58 x65) x5False)False)(∀ x65 . x60 x65(x64 (x14 x65)False)False)(∀ x65 . x60 x65(x11 x65 = x54 x65 x65False)False)(∀ x65 . x60 x65(x14 x65 = x48 (x9 (x10 (x45 x65)) (x10 (x13 x65)))False)False)(∀ x65 x66 . x49 x66x49 x65(x63 x66 x65False)(x63 x65 x66False)False)(∀ x65 x66 . x55 x66 x5x64 x65(x9 x66 x65 = x9 x65 x66False)False)(∀ x65 x66 . x60 x66x60 x65(x54 x66 x65 = x54 x65 x66False)False)(∀ x65 x66 . x60 x66x60 x65(x4 x66 x65 = x4 x65 x66False)False)(∀ x65 . x49 x65(x61 x65False)(x62 x65False)(x49 x65False)False)(∀ x65 . x49 x65(x61 x65False)(x62 x65False)(x0 x65False)False)(∀ x65 . x55 x65 (x56 x5)(x34 x65False)False)(∀ x65 . x0 x65x49 x65x62 x65False)(∀ x65 . x0 x65x49 x65x61 x65False)(∀ x65 . x0 x65x49 x65(x49 x65False)False)(∀ x65 . (x0 x65False)x49 x65(x61 x65False)(x62 x65False)False)(∀ x65 . (x0 x65False)x49 x65(x61 x65False)(x49 x65False)False)(∀ x65 . x49 x65x62 x65x61 x65False)(∀ x65 . x49 x65x62 x65(x49 x65False)False)(∀ x65 . x49 x65x62 x65x0 x65False)(∀ x65 . x34 x65(x32 x65False)False)(∀ x65 . (x0 x65False)x49 x65(x62 x65False)(x61 x65False)False)(∀ x65 . (x0 x65False)x49 x65(x62 x65False)(x49 x65False)False)(∀ x65 . x64 x65(x49 x65False)False)(∀ x65 . x34 x65(x31 x65False)False)(∀ x65 . x49 x65x61 x65x62 x65False)(∀ x65 . x49 x65x61 x65(x49 x65False)False)(∀ x65 . x49 x65x61 x65x0 x65False)(∀ x65 . x64 x65(x60 x65False)False)(∀ x65 . x24 x65(x34 x65False)False)(∀ x65 . x30 x65(x49 x65False)False)(∀ x65 . x30 x65(x64 x65False)False)(∀ x65 . x30 x65(x60 x65False)False)(∀ x65 . x25 x65(x24 x65False)False)(∀ x65 . x0 x65(x40 x65False)False)(∀ x65 . x55 x65 x50(x15 x65False)False)(∀ x65 x66 . x15 x66x55 x65 (x56 x66)(x15 x65False)False)(∀ x65 x66 . x25 x66x55 x65 (x56 x66)(x25 x65False)False)(∀ x65 x66 . x24 x66x55 x65 (x56 x66)(x24 x65False)False)(∀ x65 x66 . x34 x66x55 x65 (x56 x66)(x34 x65False)False)(∀ x65 x66 . x31 x66x55 x65 (x56 x66)(x31 x65False)False)(∀ x65 . x55 x65 x5(x64 x65False)False)(∀ x65 . x55 x65 x5(x60 x65False)False)(∀ x65 . x15 x65(x25 x65False)False)(∀ x65 x66 . x32 x66x55 x65 (x56 x66)(x32 x65False)False)(∀ x65 . x0 x65(x15 x65False)False)(∀ x65 x66 . x15 x66x55 x65 x66(x30 x65False)False)(∀ x65 x66 . x25 x66x55 x65 x66(x26 x65False)False)(∀ x65 x66 . x24 x66x55 x65 x66(x29 x65False)False)(∀ x65 x66 . x34 x66x55 x65 x66(x64 x65False)False)(∀ x65 x66 . x31 x66x55 x65 x66(x49 x65False)False)(∀ x65 x66 . x32 x66x55 x65 x66(x60 x65False)False)(∀ x65 . x55 x65 (x56 x50)(x15 x65False)False)(∀ x65 x66 . x1 x65 x66x1 x66 x65False)((x63 (x58 (x57 x28 x27)) x59False)(x28 = x27False)False)((x63 (x58 (x57 x28 x27)) x59False)x63 (x58 (x57 x28 x27)) x59False)(x28 = x27(x28 = x27False)False)(x28 = x27x63 (x58 (x57 x28 x27)) x59False)((x60 x27False)False)((x60 x28False)False)False (proof)