Search for blocks/addresses/...

Proofgold Address

address
PULK9pocvYvM7UPpGWM5AkY5qZs9hJVEA8J
total
0
mg
-
conjpub
-
current assets
d3770../0ad1a.. bday: 35134 doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 7a1d8.. : ∀ 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 . x71 x73(x73 = x72False)x71 x72False)(∀ x72 x73 . x0 x72 x73x71 x73False)(∀ x72 . x71 x72(x72 = x70False)False)(∀ x72 x73 x74 . x0 x72 x73x2 x73 (x1 x74)x71 x74False)(∀ x72 x73 x74 . x0 x73 x74x2 x74 (x1 x72)(x2 x73 x72False)False)(∀ x72 x73 . x3 x73x0 (x5 x72) (x6 (x4 x73))(x0 x72 (x6 x73)False)False)(∀ x72 x73 . x3 x73x0 x72 (x6 x73)(x0 (x5 x72) (x6 (x4 x73))False)False)(∀ x72 x73 x74 . x3 x74x7 x73 x72x0 x72 (x6 x74)(x0 x73 (x6 x74)False)False)(∀ x72 x73 . x7 x73 x72(x2 x73 (x1 x72)False)False)(∀ x72 x73 . x2 x73 (x1 x72)(x7 x73 x72False)False)(∀ x72 x73 . x69 x73x7 x72 (x6 (x67 x73))(x68 x72 (x6 (x67 x73))False)(x0 x72 (x6 (x67 x73))False)False)(∀ x72 x73 x74 . x3 x74x8 x74(x74 = x70False)x3 x72x0 x72 x74x0 x73 (x6 x72)(x0 x73 (x6 x74)False)False)(∀ x72 x73 . x3 x73x8 x73(x73 = x70False)x0 x72 (x6 x73)(x0 x72 (x6 (x66 x72 x73))False)False)(∀ x72 x73 . x3 x73x8 x73(x73 = x70False)x0 x72 (x6 x73)(x0 (x66 x72 x73) x73False)False)(∀ x72 x73 . x3 x73x8 x73(x73 = x70False)x0 x72 (x6 x73)(x3 (x66 x72 x73)False)False)(∀ x72 x73 . x2 x72 x73(x71 x73False)(x0 x72 x73False)False)((x6 x70 = x70False)False)(∀ x72 . x3 x72x0 (x4 (x9 x72)) x72(x8 x72False)False)(∀ x72 . x3 x72(x0 (x9 x72) x72False)(x8 x72False)False)(∀ x72 . x3 x72(x3 (x9 x72)False)(x8 x72False)False)(∀ x72 x73 . x3 x73x8 x73x3 x72x0 x72 x73(x0 (x4 x72) x73False)False)(∀ x72 x73 . x0 x73 x72(x2 x73 x72False)False)((x2 x70 x65False)False)(∀ x72 . (x10 x72 x70 = x72False)False)(∀ x72 . x69 x72(x8 (x67 x72)False)False)((x2 x12 x11False)False)((x2 x12 x64False)False)((x13 x12 x11 x64False)False)((x63 x12False)False)(x71 x12False)(∀ x72 . (x7 x72 x72False)False)(∀ x72 x73 x74 . (x71 x74False)(x71 x72False)x2 x72 (x1 x74)x2 x73 x72(x13 x73 x74 x72False)False)(∀ x72 x73 x74 . (x71 x74False)(x71 x72False)x2 x72 (x1 x74)x13 x73 x74 x72(x2 x73 x72False)False)(∀ x72 . (x5 x72 = x1 x72False)False)((x64 = x65False)False)((x14 x15False)False)(x71 x15False)(∀ x72 . (x71 x72False)(x16 (x17 x72) x12False)False)(∀ x72 . (x71 x72False)(x2 (x17 x72) (x1 x72)False)False)(∀ x72 . (x18 x72False)x18 (x19 x72)False)(∀ x72 . (x18 x72False)(x2 (x19 x72) (x1 x72)False)False)(∀ x72 . x20 x72(x16 (x21 x72) x72False)False)(∀ x72 . x20 x72(x62 (x21 x72)False)False)(∀ x72 . x20 x72(x22 (x21 x72)False)False)(∀ x72 . (x71 x72False)(x18 (x61 x72)False)False)(∀ x72 . (x71 x72False)x71 (x61 x72)False)(∀ x72 . (x71 x72False)(x2 (x61 x72) (x1 x72)False)False)((x23 x24False)False)(x71 x24False)(x25 x26False)((x62 x26False)False)((x22 x26False)False)(∀ x72 . x20 x72(x16 (x60 x72) x72False)False)(∀ x72 . (x71 x72False)(x28 (x27 x72) x72False)False)(∀ x72 . (x71 x72False)(x2 (x27 x72) (x1 x72)False)False)((x23 x29False)False)(∀ x72 . (x59 x72False)x59 (x58 x72)False)(∀ x72 . (x59 x72False)(x2 (x58 x72) (x1 x72)False)False)(∀ x72 . x28 (x57 x72) x72False)(∀ x72 . (x2 (x57 x72) (x1 x72)False)False)(x59 x56False)(x71 x30False)(∀ x72 . (x71 (x55 x72)False)False)(∀ x72 . (x2 (x55 x72) (x1 x72)False)False)((x3 x54False)False)((x31 x54False)False)((x53 x54False)False)(x71 x54False)((x52 x51False)False)((x62 x51False)False)((x22 x51False)False)((x20 x32False)False)((x59 x32False)False)((x3 x32False)False)((x31 x32False)False)((x53 x32False)False)((x71 x50False)False)(∀ x72 . (x71 x72False)x71 (x33 x72)False)(∀ x72 . (x71 x72False)(x2 (x33 x72) (x1 x72)False)False)((x3 x34False)False)((x62 x49False)False)((x22 x49False)False)((x20 x48False)False)(∀ x72 . (x67 (x67 x72) = x67 x72False)False)(∀ x72 . (x10 x72 x72 = x72False)False)(∀ x72 . (x59 x72False)x59 (x1 x72)False)(∀ x72 . (x59 x72False)(x20 (x67 x72)False)False)(∀ x72 . (x59 x72False)x59 (x67 x72)False)(∀ x72 . x3 x72x23 x72(x23 (x4 x72)False)False)(x59 x65False)((x3 x65False)False)(x71 x65False)(∀ x72 . x59 x72(x20 (x67 x72)False)False)(∀ x72 . x59 x72(x59 (x67 x72)False)False)(∀ x72 x73 . (x71 x73False)x71 (x10 x72 x73)False)((x35 x65False)False)(∀ x72 x73 . (x71 x73False)x71 (x10 x73 x72)False)((x20 x65False)False)(∀ x72 . x71 (x47 x72)False)(∀ x72 . x3 x72(x3 (x4 x72)False)False)(∀ x72 . x3 x72x71 (x4 x72)False)(∀ x72 . x3 x72(x53 (x6 x72)False)False)(∀ x72 . (x71 x72False)(x20 (x67 x72)False)False)(∀ x72 . (x71 x72False)x71 (x67 x72)False)((x71 x70False)False)(∀ x72 . x71 (x1 x72)False)(∀ x72 . x71 (x4 x72)False)(∀ x72 . x71 x72(x20 (x67 x72)False)False)(∀ x72 . x71 x72(x71 (x67 x72)False)False)(∀ x72 . x22 x72x62 x72(x14 (x47 x72)False)False)(∀ x72 . (x16 (x47 x72) x12False)False)(∀ x72 x73 . (x71 x73False)(x71 x72False)x2 x72 (x1 x73)(x13 (x36 x72 x73) x73 x72False)False)(∀ x72 . (x2 (x46 x72) x72False)False)((x71 x37False)False)(∀ x72 x73 x74 . (x71 x74False)(x71 x72False)x2 x72 (x1 x74)x13 x73 x74 x72(x2 x73 x74False)False)(∀ x72 . (x2 (x5 x72) (x1 (x1 x72))False)False)((x2 x64 (x1 x11)False)False)(∀ x72 . (x20 (x67 x72)False)False)((x70 = x37False)False)(∀ x72 . x38 x72x0 (x5 (x39 x72)) x72x0 (x40 x72) x72(x69 x72False)False)(∀ x72 . x38 x72x0 (x5 (x39 x72)) x72x68 (x40 x72) x72(x69 x72False)False)(∀ x72 . x38 x72x0 (x5 (x39 x72)) x72(x7 (x40 x72) x72False)(x69 x72False)False)(∀ x72 . x38 x72(x0 (x39 x72) x72False)x0 (x40 x72) x72(x69 x72False)False)(∀ x72 . x38 x72(x0 (x39 x72) x72False)x68 (x40 x72) x72(x69 x72False)False)(∀ x72 . x38 x72(x0 (x39 x72) x72False)(x7 (x40 x72) x72False)(x69 x72False)False)(∀ x72 x73 . x69 x73x7 x72 x73(x68 x72 x73False)(x0 x72 x73False)False)(∀ x72 x73 . x69 x73x0 x72 x73(x0 (x5 x72) x73False)False)(∀ x72 . x69 x72(x38 x72False)False)(∀ x72 . (x4 x72 = x10 x72 (x47 x72)False)False)(∀ x72 . x0 (x41 x72) x72(x38 x72False)False)(∀ x72 . (x7 (x41 x72) (x45 x72)False)(x38 x72False)False)(∀ x72 . (x0 (x45 x72) x72False)(x38 x72False)False)(∀ x72 x73 x74 . x38 x74x0 x72 x74x7 x73 x72(x0 x73 x74False)False)(∀ x72 x73 . (x10 x73 x72 = x10 x72 x73False)False)(∀ x72 . x71 x72(x44 x72False)False)(∀ x72 x73 . x14 x73x2 x72 (x1 x73)(x14 x72False)False)(∀ x72 . x16 x72 x12(x18 x72False)False)(∀ x72 . x16 x72 x12x71 x72False)(∀ x72 . x2 x72 x65(x23 x72False)False)(∀ x72 x73 . x14 x73x2 x72 x73(x62 x72False)False)(∀ x72 x73 . x14 x73x2 x72 x73(x22 x72False)False)(∀ x72 . x71 x72(x16 x72 x70False)False)(∀ x72 . x71 x72(x23 x72False)False)(∀ x72 . x71 x72(x14 x72False)False)(∀ x72 . x16 x72 x70(x71 x72False)False)(∀ x72 . x23 x72(x3 x72False)False)(∀ x72 . x18 x72x22 x72x62 x72(x25 x72False)False)(∀ x72 . x18 x72x22 x72x62 x72(x62 x72False)False)(∀ x72 . x18 x72x22 x72x62 x72(x22 x72False)False)(∀ x72 . x3 x72x59 x72(x23 x72False)False)(∀ x72 x73 . x18 x73x2 x72 (x1 x73)(x18 x72False)False)(∀ x72 x73 . x3 x73x2 x72 x73(x3 x72False)False)(∀ x72 . x22 x72x62 x72(x25 x72False)(x62 x72False)False)(∀ x72 . x22 x72x62 x72(x25 x72False)(x22 x72False)False)(∀ x72 . x22 x72x62 x72(x25 x72False)x18 x72False)(∀ x72 . x23 x72(x59 x72False)False)(∀ x72 x73 . x71 x73x2 x72 (x1 x73)x28 x72 x73False)(∀ x72 . x71 x72(x42 x72False)False)(∀ x72 . x71 x72x22 x72x62 x72(x25 x72False)False)(∀ x72 . x71 x72x22 x72x62 x72(x62 x72False)False)(∀ x72 . x71 x72x22 x72x62 x72(x22 x72False)False)(∀ x72 . x2 x72 x65(x59 x72False)False)(∀ x72 x73 . (x71 x73False)x2 x72 (x1 x73)x71 x72(x28 x72 x73False)False)(∀ x72 . x71 x72(x3 x72False)False)(∀ x72 x73 . x22 x73x62 x73x2 x72 (x1 x73)(x62 x72False)False)(∀ x72 . x23 x72(x20 x72False)False)(∀ x72 x73 . (x71 x73False)x2 x72 (x1 x73)(x28 x72 x73False)x71 x72False)(∀ x72 . x53 x72x31 x72(x3 x72False)False)(∀ x72 . x71 x72x22 x72x62 x72(x52 x72False)False)(∀ x72 . x71 x72x22 x72x62 x72(x62 x72False)False)(∀ x72 . x71 x72x22 x72x62 x72(x22 x72False)False)(∀ x72 . x71 x72(x20 x72False)False)(∀ x72 x73 . x71 x73x2 x72 (x1 x73)(x71 x72False)False)(∀ x72 . x3 x72(x31 x72False)False)(∀ x72 . x3 x72(x53 x72False)False)(∀ x72 . x71 x72(x62 x72False)False)(∀ x72 . x69 x72(x38 x72False)False)(∀ x72 . x20 x72(x3 x72False)False)(∀ x72 x73 . x44 x73x2 x72 (x1 x73)(x44 x72False)False)(∀ x72 . (x71 x72False)x18 x72(x16 x72 x12False)False)(∀ x72 x73 . x0 x72 x73x0 x73 x72False)(x69 (x6 (x67 x43))False)((x69 x43False)False)False (proof)

previous assets