Search for blocks/addresses/...

Proofgold Asset

asset id
e7dbfc44709c6efa0f36dba47b5eb36452c4322977d732541f6bce8908fa9b90
asset hash
64516d9323563062f5f3107a4a6985e5df96d7f476f16ca8cb5af46cae8f98bd
bday / block
35131
tx
e6f9d..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem e4055.. : ∀ 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 . x61 x63(x63 = x62False)x61 x62False)(∀ x62 x63 . x0 x62 x63x61 x63False)(∀ x62 . x61 x62(x62 = x60False)False)(∀ x62 x63 x64 . x0 x62 x63x2 x63 (x1 x64)x61 x64False)(∀ x62 x63 x64 x65 x66 . (x59 x66False)x49 x66x58 x66x2 x62 (x50 x66)x2 x65 (x50 x66)x2 x63 (x50 x66)x57 x64x51 x64 (x50 x66) (x50 x66)x56 x64 (x50 x66) (x50 x66)x2 x64 (x1 (x55 (x50 x66) (x50 x66)))x52 x64 x66x54 (x50 x66) (x50 x66) x64 x62 = x62x53 x66 x65 x62 (x54 (x50 x66) (x50 x66) x64 x65)(x65 = x62False)(x53 x66 x63 x62 (x54 (x50 x66) (x50 x66) x64 x63)False)False)(∀ x62 x63 x64 . x0 x63 x64x2 x64 (x1 x62)(x2 x63 x62False)False)(∀ x62 x63 . x48 x63 x62(x2 x63 (x1 x62)False)False)(∀ x62 x63 . x2 x63 (x1 x62)(x48 x63 x62False)False)(∀ x62 x63 . (x59 x63False)x49 x63x58 x63x57 x62x51 x62 (x50 x63) (x50 x63)x56 x62 (x50 x63) (x50 x63)x2 x62 (x1 (x55 (x50 x63) (x50 x63)))x47 x63 (x46 x62 x63) (x45 x62 x63) (x54 (x50 x63) (x50 x63) x62 (x46 x62 x63)) (x54 (x50 x63) (x50 x63) x62 (x45 x62 x63))(x52 x62 x63False)False)(∀ x62 x63 . (x59 x63False)x49 x63x58 x63x57 x62x51 x62 (x50 x63) (x50 x63)x56 x62 (x50 x63) (x50 x63)x2 x62 (x1 (x55 (x50 x63) (x50 x63)))(x2 (x45 x62 x63) (x50 x63)False)(x52 x62 x63False)False)(∀ x62 x63 . (x59 x63False)x49 x63x58 x63x57 x62x51 x62 (x50 x63) (x50 x63)x56 x62 (x50 x63) (x50 x63)x2 x62 (x1 (x55 (x50 x63) (x50 x63)))(x2 (x46 x62 x63) (x50 x63)False)(x52 x62 x63False)False)(∀ x62 x63 x64 x65 . (x59 x65False)x49 x65x58 x65x57 x62x51 x62 (x50 x65) (x50 x65)x56 x62 (x50 x65) (x50 x65)x2 x62 (x1 (x55 (x50 x65) (x50 x65)))x52 x62 x65x2 x64 (x50 x65)x2 x63 (x50 x65)(x47 x65 x64 x63 (x54 (x50 x65) (x50 x65) x62 x64) (x54 (x50 x65) (x50 x65) x62 x63)False)False)(∀ x62 x63 . x2 x62 x63(x61 x63False)(x0 x62 x63False)False)(∀ x62 x63 . x0 x63 x62(x2 x63 x62False)False)(∀ x62 x63 x64 x65 x66 x67 . (x59 x67False)x49 x67x58 x67x2 x62 (x50 x67)x2 x66 (x50 x67)x2 x63 (x50 x67)x2 x65 (x50 x67)x2 x64 (x50 x67)x44 x67 x66 x62 x62 x65x44 x67 x63 x62 x62 x64x47 x67 x66 x63 x65 x64(x43 x67 x62 x66 x63False)(x44 x67 x66 x63 x64 x65False)False)(x61 x3False)(∀ x62 . (x48 x62 x62False)False)(∀ x62 x63 x64 x65 . (x61 x65False)x57 x62x51 x62 x65 x64x2 x62 (x1 (x55 x65 x64))x2 x63 x65(x54 x65 x64 x62 x63 = x4 x62 x63False)False)((x42 x41False)False)(x61 x41False)(∀ x62 x63 . (x57 (x40 x62 x63)False)False)(∀ x62 x63 . (x5 (x40 x62 x63) x62False)False)(∀ x62 x63 . (x39 (x40 x63 x62) x62False)False)(∀ x62 x63 . (x6 (x40 x62 x63)False)False)(x38 x37False)((x57 x37False)False)((x6 x37False)False)(∀ x62 . (x7 x62False)x9 x62x61 (x8 x62)False)(∀ x62 . (x7 x62False)x9 x62(x2 (x8 x62) (x1 (x50 x62))False)False)(∀ x62 x63 . (x61 x63False)(x61 x62False)x61 (x10 x62 x63)False)(∀ x62 x63 . (x61 x63False)(x61 x62False)(x57 (x10 x62 x63)False)False)(∀ x62 x63 . (x61 x63False)(x61 x62False)(x5 (x10 x62 x63) x62False)False)(∀ x62 x63 . (x61 x63False)(x61 x62False)(x39 (x10 x62 x63) x63False)False)(∀ x62 x63 . (x61 x63False)(x61 x62False)(x6 (x10 x62 x63)False)False)(∀ x62 x63 . (x61 x63False)(x61 x62False)(x2 (x10 x62 x63) (x1 (x55 x63 x62))False)False)(x61 x11False)(∀ x62 . (x56 (x36 x62) x62 x62False)False)(∀ x62 . (x51 (x36 x62) x62 x62False)False)(∀ x62 . (x35 (x36 x62) x62False)False)(∀ x62 . (x57 (x36 x62)False)False)(∀ x62 . (x5 (x36 x62) x62False)False)(∀ x62 . (x39 (x36 x62) x62False)False)(∀ x62 . (x6 (x36 x62)False)False)(∀ x62 . (x2 (x36 x62) (x1 (x55 x62 x62))False)False)((x34 x33False)False)((x57 x33False)False)((x6 x33False)False)(∀ x62 . (x59 x62False)x9 x62x12 (x13 x62)False)(∀ x62 . (x59 x62False)x9 x62(x2 (x13 x62) (x1 (x50 x62))False)False)(∀ x62 . (x7 x62False)x9 x62(x12 (x14 x62)False)False)(∀ x62 . (x7 x62False)x9 x62x61 (x14 x62)False)(∀ x62 . (x7 x62False)x9 x62(x2 (x14 x62) (x1 (x50 x62))False)False)((x61 x32False)False)(∀ x62 x63 . (x5 (x15 x62 x63) x62False)False)(∀ x62 x63 . (x39 (x15 x63 x62) x62False)False)(∀ x62 x63 . (x6 (x15 x62 x63)False)False)(∀ x62 x63 . (x61 (x15 x62 x63)False)False)(∀ x62 x63 . (x2 (x15 x62 x63) (x1 (x55 x63 x62))False)False)(∀ x62 x63 . (x57 (x31 x62 x63)False)False)(∀ x62 x63 . (x5 (x31 x62 x63) x62False)False)(∀ x62 x63 . (x39 (x31 x63 x62) x62False)False)(∀ x62 x63 . (x6 (x31 x62 x63)False)False)(∀ x62 x63 . (x2 (x31 x62 x63) (x1 (x55 x63 x62))False)False)(∀ x62 x63 . (x51 (x16 x62 x63) x63 x62False)False)(∀ x62 x63 . (x57 (x16 x62 x63)False)False)(∀ x62 x63 . (x5 (x16 x62 x63) x62False)False)(∀ x62 x63 . (x39 (x16 x63 x62) x62False)False)(∀ x62 x63 . (x6 (x16 x62 x63)False)False)(∀ x62 x63 . (x2 (x16 x62 x63) (x1 (x55 x63 x62))False)False)((x57 x17False)False)((x6 x17False)False)(∀ x62 . (x18 x62False)x9 x62x19 (x50 x62)False)(∀ x62 . x18 x62x9 x62(x19 (x50 x62)False)False)(∀ x62 . x59 x62x9 x62(x12 (x50 x62)False)False)(∀ x62 . (x59 x62False)x9 x62x12 (x50 x62)False)(∀ x62 . (x7 x62False)x9 x62x61 (x50 x62)False)((x61 x60False)False)(∀ x62 . x7 x62x9 x62(x61 (x50 x62)False)False)(∀ x62 x63 x64 . x42 x64x6 x62x5 x62 x64x57 x62(x57 (x4 x62 x63)False)False)(∀ x62 x63 x64 . x42 x64x6 x62x5 x62 x64x57 x62(x6 (x4 x62 x63)False)False)(∀ x62 . (x2 (x30 x62) x62False)False)((x9 x20False)False)((x58 x29False)False)(∀ x62 . x58 x62(x9 x62False)False)(∀ x62 x63 x64 x65 . (x61 x65False)x57 x62x51 x62 x65 x64x2 x62 (x1 (x55 x65 x64))x2 x63 x65(x2 (x54 x65 x64 x62 x63) x64False)False)(∀ x62 x63 x64 x65 . (x7 x65False)x58 x65x2 x64 (x50 x65)x2 x62 (x50 x65)x2 x63 (x50 x65)x44 x65 x64 x62 x62 x63(x53 x65 x64 x62 x63False)False)(∀ x62 x63 x64 x65 . (x7 x65False)x58 x65x2 x64 (x50 x65)x2 x62 (x50 x65)x2 x63 (x50 x65)x53 x65 x64 x62 x63(x44 x65 x64 x62 x62 x63False)False)(∀ x62 . x9 x62x21 x62 x60(x7 x62False)False)(∀ x62 x63 . x42 x63x2 x62 (x1 x63)(x42 x62False)False)(∀ x62 . x9 x62x7 x62(x21 x62 x60False)False)(∀ x62 x63 x64 . (x61 x64False)(x61 x62False)x2 x63 (x1 (x55 x64 x62))x57 x63x51 x63 x64 x62(x51 x63 x64 x62False)False)(∀ x62 x63 x64 . (x61 x64False)(x61 x62False)x2 x63 (x1 (x55 x64 x62))x57 x63x51 x63 x64 x62x61 x63False)(∀ x62 x63 x64 . (x61 x64False)(x61 x62False)x2 x63 (x1 (x55 x64 x62))x57 x63x51 x63 x64 x62(x57 x63False)False)(∀ x62 x63 . x42 x63x2 x62 x63(x57 x62False)False)(∀ x62 x63 . x42 x63x2 x62 x63(x6 x62False)False)(∀ x62 . x9 x62(x18 x62False)x59 x62False)(∀ x62 . x61 x62(x42 x62False)False)(∀ x62 . x9 x62x59 x62(x18 x62False)False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63))x57 x64x34 x64x28 x64 x63(x56 x64 x62 x63False)False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63))x57 x64x34 x64x28 x64 x63(x57 x64False)False)(∀ x62 . x12 x62x6 x62x57 x62(x38 x62False)False)(∀ x62 . x12 x62x6 x62x57 x62(x57 x62False)False)(∀ x62 . x12 x62x6 x62x57 x62(x6 x62False)False)(∀ x62 . x9 x62(x18 x62False)x18 x62False)(∀ x62 . x9 x62(x18 x62False)x7 x62False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62))x57 x64x56 x64 x63 x62(x28 x64 x62False)False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62))x57 x64x56 x64 x63 x62(x34 x64False)False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62))x57 x64x56 x64 x63 x62(x57 x64False)False)(∀ x62 . x6 x62x57 x62(x38 x62False)(x57 x62False)False)(∀ x62 . x6 x62x57 x62(x38 x62False)(x6 x62False)False)(∀ x62 . x6 x62x57 x62(x38 x62False)x12 x62False)(∀ x62 . x9 x62x7 x62(x18 x62False)False)(∀ x62 . x9 x62x7 x62(x7 x62False)False)(∀ x62 x63 x64 . x61 x64x2 x62 (x1 (x55 x63 x64))(x61 x62False)False)(∀ x62 x63 . x2 x63 (x1 (x55 x62 x62))x51 x63 x62 x62(x35 x63 x62False)False)(∀ x62 . x61 x62x6 x62x57 x62(x38 x62False)False)(∀ x62 . x61 x62x6 x62x57 x62(x57 x62False)False)(∀ x62 . x61 x62x6 x62x57 x62(x6 x62False)False)(∀ x62 x63 x64 . x61 x64x2 x62 (x1 (x55 x64 x63))(x61 x62False)False)(∀ x62 x63 x64 . (x61 x64False)x2 x62 (x1 (x55 x63 x64))x51 x62 x63 x64(x35 x62 x63False)False)(∀ x62 x63 . x6 x63x57 x63x2 x62 (x1 x63)(x57 x62False)False)(∀ x62 . x9 x62(x59 x62False)x7 x62False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63))(x5 x64 x63False)False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x63 x62))(x39 x64 x63False)False)(∀ x62 x63 x64 . (x61 x64False)x61 x62x2 x63 (x1 (x55 x64 x62))x35 x63 x64False)(∀ x62 x63 x64 . x61 x64x2 x62 (x1 (x55 x64 x63))x51 x62 x64 x63(x35 x62 x64False)False)(∀ x62 . x61 x62x6 x62x57 x62(x34 x62False)False)(∀ x62 . x61 x62x6 x62x57 x62(x57 x62False)False)(∀ x62 . x61 x62x6 x62x57 x62(x6 x62False)False)(∀ x62 . x9 x62x7 x62(x59 x62False)False)(∀ x62 x63 x64 . x2 x64 (x1 (x55 x62 x63))(x6 x64False)False)(∀ x62 x63 x64 . x61 x64x2 x62 (x1 (x55 x64 x63))(x35 x62 x64False)False)(∀ x62 x63 x64 . x2 x63 (x1 (x55 x64 x62))x35 x63 x64(x51 x63 x64 x62False)False)(∀ x62 . x61 x62(x57 x62False)False)(∀ x62 . x9 x62(x59 x62False)x7 x62False)(∀ x62 . x9 x62x21 x62 x3(x59 x62False)False)(∀ x62 . x9 x62x21 x62 x3x7 x62False)(∀ x62 . x9 x62(x7 x62False)x59 x62(x21 x62 x3False)False)(∀ x62 x63 . x0 x62 x63x0 x63 x62False)(x44 x22 x25 x23 (x54 (x50 x22) (x50 x22) x24 x23) (x54 (x50 x22) (x50 x22) x24 x25)False)(x43 x22 x27 x25 x23False)(x26 = x27False)((x53 x22 x26 x27 (x54 (x50 x22) (x50 x22) x24 x26)False)False)((x54 (x50 x22) (x50 x22) x24 x27 = x27False)False)((x52 x24 x22False)False)((x2 x24 (x1 (x55 (x50 x22) (x50 x22)))False)False)((x56 x24 (x50 x22) (x50 x22)False)False)((x51 x24 (x50 x22) (x50 x22)False)False)((x57 x24False)False)((x2 x23 (x50 x22)False)False)((x2 x25 (x50 x22)False)False)((x2 x26 (x50 x22)False)False)((x2 x27 (x50 x22)False)False)((x58 x22False)False)((x49 x22False)False)(x59 x22False)False (proof)