Search for blocks/addresses/...

Proofgold Asset

asset id
302e2ac6ca98f69cfd92436bc9d800fcd55e0b052e1dc5aaf1a831e54c459b6a
asset hash
294d14e0fcee889724061ee86998c16ab3f69154625aa8e81f24b476ad636ece
bday / block
35136
tx
3df9b..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 3f448.. : ∀ 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 . ∀ x68 : ι → ο . ∀ x69 : ι → ι → ι . ∀ x70 x71 . ∀ x72 : ι → ι → ο . ∀ x73 : ι → ι . ∀ x74 x75 : ι → ο . ∀ x76 : ι → ι → ο . ∀ x77 : ι → ο . (∀ x78 x79 . x77 x79x77 x78(x76 x79 x78False)(x75 x78False)(x74 x79False)False)(∀ x78 x79 . x0 x79(x79 = x78False)x0 x78False)(∀ x78 x79 . x77 x79x77 x78(x76 x79 x78False)(x74 x79False)(x75 x78False)False)(∀ x78 x79 . x1 x78 x79x0 x79False)(∀ x78 x79 . x77 x79x77 x78x76 x79 x78(x0 x79False)(x74 x78False)(x75 x79False)False)(∀ x78 . x0 x78(x78 = x2False)False)(∀ x78 x79 x80 . x1 x78 x79x72 x79 (x73 x80)x0 x80False)(∀ x78 x79 . x77 x79x77 x78x76 x79 x78(x0 x78False)(x75 x79False)(x74 x78False)False)(∀ x78 x79 x80 . x1 x79 x80x72 x80 (x73 x78)(x72 x79 x78False)False)(∀ x78 x79 . x77 x79x77 x78x76 x79 x78(x74 x78False)x74 x79False)(∀ x78 x79 x80 . x77 x80x77 x78x77 x79(x76 x78 x80False)(x76 x79 x71False)(x76 x70 x79False)x76 (x69 x79 x80) (x69 x79 x78)False)(∀ x78 x79 . x3 x79 x78(x72 x79 (x73 x78)False)False)(∀ x78 x79 . x72 x79 (x73 x78)(x3 x79 x78False)False)(∀ x78 x79 . x77 x79x77 x78x76 x79 x78(x75 x79False)x75 x78False)(∀ x78 x79 . x72 x78 x79(x0 x79False)(x1 x78 x79False)False)(∀ x78 x79 . x77 x79x77 x78x76 x79 x78x75 x78(x75 x79False)False)(∀ x78 x79 . x68 x79x68 x78x76 x79 x78x76 x78 x79(x79 = x78False)False)(∀ x78 x79 . x1 x79 x78(x72 x79 x78False)False)(∀ x78 x79 . x77 x79x77 x78x76 x79 x78x74 x79(x74 x78False)False)((x72 x2 x4False)False)((x72 x70 x67False)False)((x72 x70 x5False)False)((x66 x70 x67 x5False)False)((x74 x70False)False)(x0 x70False)((x72 x6 x67False)False)((x72 x6 x5False)False)((x66 x6 x67 x5False)False)((x0 x6False)False)((x76 x70 x70False)False)(x76 x70 x6False)((x76 x6 x70False)False)((x76 x6 x6False)False)(∀ x78 x79 . x68 x79x68 x78(x76 x79 x79False)False)(∀ x78 . (x3 x78 x78False)False)(∀ x78 x79 x80 . (x0 x80False)(x0 x78False)x72 x78 (x73 x80)x72 x79 x78(x66 x79 x80 x78False)False)(∀ x78 x79 x80 . (x0 x80False)(x0 x78False)x72 x78 (x73 x80)x66 x79 x80 x78(x72 x79 x78False)False)((x71 = x2False)False)((x5 = x4False)False)(∀ x78 x79 . x72 x79 x67x72 x78 x67(x7 x79 x78 = x69 x79 x78False)False)((x65 x64False)False)((x8 x64False)False)(x0 x64False)((x9 x10False)False)(x0 x10False)(∀ x78 . (x11 x78False)(x8 (x12 x78)False)False)(∀ x78 . (x11 x78False)x11 (x12 x78)False)(∀ x78 . (x11 x78False)(x72 (x12 x78) (x73 x78)False)False)(∀ x78 . (x11 x78False)x11 (x63 x78)False)(∀ x78 . (x11 x78False)(x72 (x63 x78) (x73 x78)False)False)(∀ x78 . (x0 x78False)(x11 (x62 x78)False)False)(∀ x78 . (x0 x78False)x0 (x62 x78)False)(∀ x78 . (x0 x78False)(x72 (x62 x78) (x73 x78)False)False)((x13 x14False)False)(x0 x14False)((x68 x15False)False)((x0 x15False)False)((x77 x16False)False)((x68 x16False)False)((x17 x16False)False)((x0 x16False)False)(∀ x78 . (x0 x78False)(x19 (x18 x78) x78False)False)(∀ x78 . (x0 x78False)(x72 (x18 x78) (x73 x78)False)False)((x13 x20False)False)((x75 x61False)False)((x68 x61False)False)((x77 x60False)False)((x75 x60False)False)((x68 x60False)False)((x17 x60False)False)(∀ x78 . x19 (x59 x78) x78False)(∀ x78 . (x72 (x59 x78) (x73 x78)False)False)((x58 x57False)False)((x21 x57False)False)(x0 x57False)((x74 x22False)False)((x68 x22False)False)((x77 x23False)False)((x74 x23False)False)((x68 x23False)False)((x17 x23False)False)(x0 x24False)(∀ x78 . (x0 (x56 x78)False)False)(∀ x78 . (x72 (x56 x78) (x73 x78)False)False)((x55 x54False)False)((x25 x54False)False)((x53 x54False)False)(x0 x54False)((x55 x52False)False)(x0 x52False)((x72 x52 (x73 x67)False)False)((x21 x26False)False)(x0 x26False)(∀ x78 . (x0 x78False)(x8 (x27 x78)False)False)(∀ x78 . (x0 x78False)x0 (x27 x78)False)(∀ x78 . (x0 x78False)(x72 (x27 x78) (x73 x78)False)False)((x68 x51False)False)((x77 x28False)False)((x0 x50False)False)(∀ x78 . (x0 x78False)x0 (x29 x78)False)(∀ x78 . (x0 x78False)(x72 (x29 x78) (x73 x78)False)False)((x55 x30False)False)((x21 x49False)False)(x0 x49False)((x8 x48False)False)(x0 x48False)(x8 x67False)((x55 x4False)False)(x0 x4False)((x21 x4False)False)((x58 x4False)False)((x58 x67False)False)((x47 x67False)False)(∀ x78 . x8 x78(x65 (x73 x78)False)False)((x0 x2False)False)(∀ x78 . x0 (x73 x78)False)(x0 x67False)(∀ x78 . x8 x78(x8 (x73 x78)False)False)(∀ x78 x79 . (x0 x79False)(x0 x78False)x72 x78 (x73 x79)(x66 (x46 x78 x79) x79 x78False)False)(∀ x78 . (x72 (x31 x78) x78False)False)((x0 x45False)False)(∀ x78 x79 x80 . (x0 x80False)(x0 x78False)x72 x78 (x73 x80)x66 x79 x80 x78(x72 x79 x80False)False)((x66 x71 x67 x5False)False)((x72 x5 (x73 x67)False)False)(∀ x78 x79 . x72 x79 x67x72 x78 x67(x72 (x7 x79 x78) x67False)False)(∀ x78 x79 . x77 x79x77 x78(x77 (x69 x79 x78)False)False)((x2 = x45False)False)(∀ x78 x79 . x68 x79x68 x78(x76 x79 x78False)(x76 x78 x79False)False)(∀ x78 . x0 x78(x44 x78False)False)(∀ x78 . x9 x78(x32 x78False)False)(∀ x78 . x68 x78(x74 x78False)(x75 x78False)(x68 x78False)False)(∀ x78 . x68 x78(x74 x78False)(x75 x78False)(x0 x78False)False)(∀ x78 . x72 x78 x4(x13 x78False)False)(∀ x78 . x72 x78 (x73 x67)(x47 x78False)False)(∀ x78 x79 . x65 x79x72 x78 (x73 x79)(x65 x78False)False)(∀ x78 . x0 x78(x9 x78False)False)(∀ x78 . x0 x78x68 x78x75 x78False)(∀ x78 . x0 x78x68 x78x74 x78False)(∀ x78 . x0 x78x68 x78(x68 x78False)False)(∀ x78 . x0 x78(x13 x78False)False)(∀ x78 x79 . x65 x79x72 x78 x79(x8 x78False)False)(∀ x78 . (x0 x78False)x68 x78(x74 x78False)(x75 x78False)False)(∀ x78 . (x0 x78False)x68 x78(x74 x78False)(x68 x78False)False)(∀ x78 . x13 x78(x55 x78False)False)(∀ x78 . x0 x78(x65 x78False)False)(∀ x78 . x68 x78x75 x78x74 x78False)(∀ x78 . x68 x78x75 x78(x68 x78False)False)(∀ x78 . x68 x78x75 x78x0 x78False)(∀ x78 x79 . x11 x79x72 x78 (x73 x79)(x11 x78False)False)(∀ x78 x79 . x55 x79x72 x78 x79(x55 x78False)False)(∀ x78 . x47 x78(x43 x78False)False)(∀ x78 . (x8 x78False)x11 x78False)(∀ x78 . (x0 x78False)x68 x78(x75 x78False)(x74 x78False)False)(∀ x78 . (x0 x78False)x68 x78(x75 x78False)(x68 x78False)False)(∀ x78 . x77 x78(x68 x78False)False)(∀ x78 x79 . x0 x79x72 x78 (x73 x79)x19 x78 x79False)(∀ x78 . x0 x78(x42 x78False)False)(∀ x78 . x47 x78(x33 x78False)False)(∀ x78 . x11 x78(x8 x78False)False)(∀ x78 . x68 x78x74 x78x75 x78False)(∀ x78 . x68 x78x74 x78(x68 x78False)False)(∀ x78 . x68 x78x74 x78x0 x78False)(∀ x78 . x77 x78(x17 x78False)False)(∀ x78 x79 . (x0 x79False)x72 x78 (x73 x79)x0 x78(x19 x78 x79False)False)(∀ x78 . x0 x78(x55 x78False)False)(∀ x78 . x13 x78x75 x78False)(∀ x78 . x13 x78(x13 x78False)False)(∀ x78 . x34 x78(x47 x78False)False)(∀ x78 . x13 x78(x68 x78False)False)(∀ x78 . x13 x78(x77 x78False)False)(∀ x78 x79 . (x0 x79False)x72 x78 (x73 x79)(x19 x78 x79False)x0 x78False)(∀ x78 . x53 x78x25 x78(x55 x78False)False)(∀ x78 . x72 x78 x5x75 x78False)(∀ x78 . x35 x78(x34 x78False)False)(∀ x78 x79 . x8 x79x72 x78 (x73 x79)(x8 x78False)False)(∀ x78 . x0 x78(x58 x78False)False)(∀ x78 . x72 x78 x5(x21 x78False)False)(∀ x78 x79 . x21 x79x72 x78 (x73 x79)(x21 x78False)False)(∀ x78 x79 . x35 x79x72 x78 (x73 x79)(x35 x78False)False)(∀ x78 x79 . x34 x79x72 x78 (x73 x79)(x34 x78False)False)(∀ x78 x79 . x47 x79x72 x78 (x73 x79)(x47 x78False)False)(∀ x78 x79 . x33 x79x72 x78 (x73 x79)(x33 x78False)False)(∀ x78 . x72 x78 x67(x77 x78False)False)(∀ x78 x79 . x0 x79x72 x78 (x73 x79)(x0 x78False)False)(∀ x78 . x55 x78(x25 x78False)False)(∀ x78 . x55 x78(x53 x78False)False)(∀ x78 . x13 x78(x13 x78False)False)(∀ x78 . x13 x78(x55 x78False)False)(∀ x78 . x21 x78(x35 x78False)False)(∀ x78 . x0 x78(x8 x78False)False)(∀ x78 x79 . x43 x79x72 x78 (x73 x79)(x43 x78False)False)(∀ x78 . x0 x78(x21 x78False)False)(∀ x78 x79 . x21 x79x72 x78 x79(x13 x78False)False)(∀ x78 x79 . x35 x79x72 x78 x79(x36 x78False)False)(∀ x78 x79 . x34 x79x72 x78 x79(x41 x78False)False)(∀ x78 x79 . x47 x79x72 x78 x79(x77 x78False)False)(∀ x78 x79 . x33 x79x72 x78 x79(x68 x78False)False)(∀ x78 x79 . x43 x79x72 x78 x79(x17 x78False)False)(∀ x78 . x72 x78 (x73 x5)(x21 x78False)False)(∀ x78 x79 . x9 x79x72 x78 (x73 x79)(x9 x78False)False)(∀ x78 x79 . x44 x79x72 x78 (x73 x79)(x44 x78False)False)(∀ x78 x79 . x9 x79x72 x78 x79(x37 x78False)False)(∀ x78 x79 . x1 x78 x79x1 x79 x78False)(x76 (x7 x39 x40) (x7 x39 x38)False)((x76 x38 x40False)False)((x66 x40 x67 x5False)False)((x66 x38 x67 x5False)False)(x76 x70 x39False)(x76 x39 x71False)((x72 x39 x67False)False)False (proof)