Search for blocks/addresses/...

Proofgold Asset

asset id
61cc365d8e63c31b924747524f12d82da569a17f1a68c949f03638a3951717fb
asset hash
45793df942b0cd4bd77de6d14a1d658bc070a1d99f1262056778ae03bd2b09cc
bday / block
35124
tx
c6843..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem f819c.. : ∀ 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 . x58 x60(x60 = x59False)x58 x59False)(∀ x59 x60 . x0 x59 x60x58 x60False)(∀ x59 . x58 x59(x59 = x57False)False)(∀ x59 x60 x61 . x0 x59 x60x2 x60 (x1 x61)x58 x61False)(∀ x59 x60 x61 . x0 x60 x61x2 x61 (x1 x59)(x2 x60 x59False)False)(∀ x59 x60 . x3 x60 x59(x2 x60 (x1 x59)False)False)(∀ x59 x60 . x2 x60 (x1 x59)(x3 x60 x59False)False)(∀ x59 x60 x61 . x0 x60 x61x0 x59 x61x0 x59 (x4 x61 x60)False)(∀ x59 x60 . x0 x60 x59(x0 (x4 x59 x60) x59False)False)(∀ x59 x60 . x2 x59 x60(x58 x60False)(x0 x59 x60False)False)(∀ x59 x60 x61 x62 x63 x64 x65 x66 . (x56 x66False)(x45 x66False)x55 x66x46 x66x54 x66x47 x66x53 x66x48 x66x2 x65 (x52 x66)x2 x59 (x52 x66)x2 x64 (x52 x66)x2 x60 (x52 x66)x51 x63 x66 x65 x59x51 x61 x66 x59 x64x51 x62 x66 x64 x60(x49 x66 x65 x59 = x57False)(x49 x66 x59 x64 = x57False)(x49 x66 x64 x60 = x57False)(x50 x66 x65 x59 x60 x63 (x50 x66 x59 x64 x60 x61 x62) = x50 x66 x65 x64 x60 (x50 x66 x65 x59 x64 x63 x61) x62False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x55 x62x46 x62x54 x62x47 x62x53 x62x48 x62x2 x61 (x52 x62)x2 x59 (x52 x62)x2 x60 (x52 x62)(x49 x62 x61 x59 = x57False)(x49 x62 x59 x60 = x57False)x49 x62 x61 x60 = x57False)(∀ x59 x60 . x0 x60 x59(x2 x60 x59False)False)(x58 x5False)(∀ x59 . (x3 x59 x59False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x6 x60x2 x59 (x7 x60)(x9 x60 x59 = x8 x60 x59False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x6 x60x2 x59 (x7 x60)(x43 x60 x59 = x44 x60 x59False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x55 x60x46 x60x54 x60x47 x60x53 x60x48 x60x2 x59 (x52 x60)(x9 x60 (x10 x60 x59) = x59False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x55 x60x46 x60x54 x60x47 x60x53 x60x48 x60x2 x59 (x52 x60)(x43 x60 (x10 x60 x59) = x59False)False)(∀ x59 x60 x61 . (x56 x61False)(x45 x61False)x55 x61x46 x61x54 x61x47 x61x53 x61x48 x61x2 x60 (x52 x61)x51 x59 x61 x60 x60(x50 x61 x60 x60 x60 x59 (x10 x61 x60) = x59False)False)(∀ x59 x60 x61 . (x56 x61False)(x45 x61False)x55 x61x46 x61x54 x61x47 x61x53 x61x48 x61x2 x60 (x52 x61)x51 x59 x61 x60 x60(x50 x61 x60 x60 x60 (x10 x61 x60) x59 = x59False)False)(∀ x59 . (x56 x59False)x12 x59x58 (x11 x59)False)(∀ x59 . (x56 x59False)x12 x59(x2 (x11 x59) (x1 (x52 x59))False)False)(x58 x13False)(x45 x42False)(x56 x42False)((x48 x42False)False)(x14 x15False)((x41 x15False)False)(∀ x59 . (x16 x59False)x12 x59x17 (x18 x59)False)(∀ x59 . (x16 x59False)x12 x59(x2 (x18 x59) (x1 (x52 x59))False)False)(∀ x59 . (x56 x59False)x12 x59(x17 (x19 x59)False)False)(∀ x59 . (x56 x59False)x12 x59x58 (x19 x59)False)(∀ x59 . (x56 x59False)x12 x59(x2 (x19 x59) (x1 (x52 x59))False)False)((x58 x40False)False)(∀ x59 x60 x61 x62 x63 . (x56 x63False)(x45 x63False)x48 x63x2 x59 (x52 x63)x2 x62 (x52 x63)x2 x60 (x7 x63)x61 = x60x43 x63 x60 = x59x9 x63 x60 = x62(x0 x61 (x20 x63 x59 x62)False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x48 x62x2 x59 (x52 x62)x2 x61 (x52 x62)x0 x60 (x20 x62 x59 x61)(x9 x62 (x39 x61 x59 x62 x60) = x61False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x48 x62x2 x59 (x52 x62)x2 x61 (x52 x62)x0 x60 (x20 x62 x59 x61)(x43 x62 (x39 x61 x59 x62 x60) = x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x48 x62x2 x59 (x52 x62)x2 x61 (x52 x62)x0 x60 (x20 x62 x59 x61)(x60 = x39 x61 x59 x62 x60False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x48 x62x2 x59 (x52 x62)x2 x61 (x52 x62)x0 x60 (x20 x62 x59 x61)(x2 (x39 x61 x59 x62 x60) (x7 x62)False)False)(∀ x59 . (x38 x59False)x12 x59x37 (x52 x59)False)(∀ x59 . x38 x59x12 x59(x37 (x52 x59)False)False)(∀ x59 . x16 x59x12 x59(x17 (x52 x59)False)False)(∀ x59 . (x16 x59False)x12 x59x17 (x52 x59)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x47 x60x48 x60x2 x59 (x52 x60)x58 (x49 x60 x59 x59)False)(∀ x59 . (x56 x59False)x12 x59x58 (x52 x59)False)(∀ x59 . (x14 x59False)x41 x59x17 (x7 x59)False)(∀ x59 . x14 x59x41 x59(x17 (x7 x59)False)False)((x58 x57False)False)(∀ x59 . x56 x59x12 x59(x58 (x52 x59)False)False)(∀ x59 . (x45 x59False)x41 x59x58 (x7 x59)False)(∀ x59 . x45 x59x41 x59(x58 (x7 x59)False)False)(∀ x59 . (x2 (x36 x59) x59False)False)(∀ x59 x60 x61 . (x56 x61False)(x45 x61False)x48 x61x2 x59 (x52 x61)x2 x60 (x52 x61)(x51 (x21 x60 x59 x61) x61 x59 x60False)False)((x41 x35False)False)((x12 x22False)False)((x6 x34False)False)((x48 x23False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x48 x62x2 x59 (x52 x62)x2 x61 (x52 x62)x51 x60 x62 x59 x61(x2 x60 (x7 x62)False)False)(∀ x59 . x41 x59(x12 x59False)False)(∀ x59 . x6 x59(x41 x59False)False)(∀ x59 . x48 x59(x6 x59False)False)(∀ x59 x60 x61 x62 x63 x64 . (x56 x64False)(x45 x64False)x55 x64x46 x64x54 x64x47 x64x53 x64x48 x64x2 x63 (x52 x64)x2 x59 (x52 x64)x2 x62 (x52 x64)x51 x60 x64 x63 x59x51 x61 x64 x59 x62(x51 (x50 x64 x63 x59 x62 x60 x61) x64 x63 x62False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x6 x60x2 x59 (x7 x60)(x2 (x9 x60 x59) (x52 x60)False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x47 x60x53 x60x48 x60x2 x59 (x52 x60)(x51 (x10 x60 x59) x60 x59 x59False)False)(∀ x59 x60 . (x56 x60False)(x45 x60False)x6 x60x2 x59 (x7 x60)(x2 (x43 x60 x59) (x52 x60)False)False)(∀ x59 x60 . x6 x60x2 x59 (x7 x60)(x2 (x8 x60 x59) (x52 x60)False)False)(∀ x59 x60 x61 . (x56 x61False)(x45 x61False)x48 x61x2 x59 (x52 x61)x2 x60 (x52 x61)(x2 (x49 x61 x59 x60) (x1 (x7 x61))False)False)(∀ x59 x60 . x6 x60x2 x59 (x7 x60)(x2 (x44 x60 x59) (x52 x60)False)False)(∀ x59 x60 x61 x62 x63 . (x56 x63False)(x45 x63False)x55 x63x46 x63x54 x63x47 x63x53 x63x48 x63x2 x62 (x52 x63)x2 x59 (x52 x63)x51 x61 x63 x62 x59(x49 x63 x62 x59 = x57False)(x49 x63 x59 x62 = x57False)x51 x60 x63 x59 x62x50 x63 x59 x62 x59 x60 x61 = x10 x63 x59(x24 x61 x63 x62 x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x55 x62x46 x62x54 x62x47 x62x53 x62x48 x62x2 x61 (x52 x62)x2 x59 (x52 x62)x51 x60 x62 x61 x59x24 x60 x62 x61 x59(x50 x62 x59 x61 x59 (x33 x60 x59 x61 x62) x60 = x10 x62 x59False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x55 x62x46 x62x54 x62x47 x62x53 x62x48 x62x2 x61 (x52 x62)x2 x59 (x52 x62)x51 x60 x62 x61 x59x24 x60 x62 x61 x59(x51 (x33 x60 x59 x61 x62) x62 x59 x61False)False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x55 x62x46 x62x54 x62x47 x62x53 x62x48 x62x2 x61 (x52 x62)x2 x59 (x52 x62)x51 x60 x62 x61 x59x24 x60 x62 x61 x59x49 x62 x59 x61 = x57False)(∀ x59 x60 x61 x62 . (x56 x62False)(x45 x62False)x55 x62x46 x62x54 x62x47 x62x53 x62x48 x62x2 x61 (x52 x62)x2 x59 (x52 x62)x51 x60 x62 x61 x59x24 x60 x62 x61 x59x49 x62 x61 x59 = x57False)(∀ x59 x60 x61 . (x56 x61False)(x45 x61False)x48 x61x2 x59 (x52 x61)x2 x60 (x52 x61)(x49 x61 x59 x60 = x20 x61 x59 x60False)False)(∀ x59 . x12 x59x25 x59 x57(x56 x59False)False)(∀ x59 . x12 x59x56 x59(x25 x59 x57False)False)(∀ x59 . x12 x59(x38 x59False)x16 x59False)(∀ x59 . x12 x59x16 x59(x38 x59False)False)(∀ x59 . x12 x59(x38 x59False)x38 x59False)(∀ x59 . x12 x59(x38 x59False)x56 x59False)(∀ x59 . x12 x59x56 x59(x38 x59False)False)(∀ x59 . x12 x59x56 x59(x56 x59False)False)(∀ x59 . x12 x59(x16 x59False)x56 x59False)(∀ x59 . x48 x59(x56 x59False)(x45 x59False)x14 x59(x53 x59False)False)(∀ x59 . x48 x59(x56 x59False)(x45 x59False)x14 x59(x54 x59False)False)(∀ x59 . x48 x59(x56 x59False)(x45 x59False)x14 x59x45 x59False)(∀ x59 . x48 x59(x56 x59False)(x45 x59False)x14 x59x56 x59False)(∀ x59 . x12 x59x56 x59(x16 x59False)False)(∀ x59 . x48 x59(x56 x59False)x16 x59(x45 x59False)(x47 x59False)False)(∀ x59 . x48 x59(x56 x59False)x16 x59(x45 x59False)(x46 x59False)False)(∀ x59 . x48 x59(x56 x59False)x16 x59(x45 x59False)x45 x59False)(∀ x59 . x48 x59(x56 x59False)x16 x59(x45 x59False)x56 x59False)(∀ x59 . x12 x59(x16 x59False)x56 x59False)(∀ x59 . x41 x59x45 x59(x14 x59False)False)(∀ x59 . x41 x59(x45 x59False)x26 x59x56 x59False)(∀ x59 . x41 x59x56 x59x26 x59(x45 x59False)False)(∀ x59 . x41 x59x45 x59(x26 x59False)False)(∀ x59 . x41 x59(x56 x59False)(x26 x59False)False)(∀ x59 . x12 x59x25 x59 x5(x16 x59False)False)(∀ x59 . x12 x59x25 x59 x5x56 x59False)(∀ x59 . x12 x59(x56 x59False)x16 x59(x25 x59 x5False)False)(∀ x59 x60 . x0 x59 x60x0 x60 x59False)(x24 x27 x30 x29 x28False)(x49 x30 x29 x32 = x57False)(x49 x30 x32 x29 = x57False)((x24 (x50 x30 x32 x29 x28 x31 x27) x30 x32 x28False)False)((x51 x27 x30 x29 x28False)False)((x51 x31 x30 x32 x29False)False)((x2 x29 (x52 x30)False)False)((x2 x32 (x52 x30)False)False)((x2 x28 (x52 x30)False)False)((x48 x30False)False)((x53 x30False)False)((x47 x30False)False)((x54 x30False)False)((x46 x30False)False)((x55 x30False)False)(x45 x30False)(x56 x30False)False (proof)