Search for blocks/addresses/...

Proofgold Asset

asset id
6950ea936aced79921616f90aeb34ffe70e1b9b9426d3d04b83f04aed78c0a22
asset hash
bdbf141c1b853236735bf9c07a59f5b01a9fa871fe0eca68fe85912d7cebbdde
bday / block
35130
tx
366c5..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem db811.. : ∀ 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 . x68 x70(x70 = x69False)x68 x69False)(∀ x69 x70 . x0 x69 x70x68 x70False)(∀ x69 . x68 x69(x69 = x67False)False)(∀ x69 x70 x71 . x0 x69 x70x2 x70 (x1 x71)x68 x71False)(∀ x69 x70 x71 . x0 x70 x71x2 x71 (x1 x69)(x2 x70 x69False)False)(∀ x69 x70 . x3 x70 x69(x2 x70 (x1 x69)False)False)(∀ x69 x70 . x2 x70 (x1 x69)(x3 x70 x69False)False)(∀ x69 x70 x71 . x4 x71x4 x69x4 x70(x5 x71 x69 (x8 (x7 x70 x6) x6) = x8 (x5 x71 x69 x70) (x5 x71 x69 (x7 x70 x6))False)False)(∀ x69 x70 . x4 x70x4 x69(x5 x70 x69 x6 = x69False)False)(∀ x69 x70 . x4 x70x4 x69(x5 x70 x69 x9 = x70False)False)(∀ x69 x70 . x2 x69 x70(x68 x70False)(x0 x69 x70False)False)(∀ x69 x70 . x0 x70 x69(x2 x70 x69False)False)((x2 x67 x66False)False)(∀ x69 . x10 x69(x11 x69 x9 = x69False)False)(∀ x69 x70 x71 . x10 x71x10 x69x10 x70(x11 (x11 x71 x69) x70 = x11 x71 (x11 x69 x70)False)False)((x2 x13 x12False)False)((x2 x13 x65False)False)((x14 x13 x12 x65False)False)((x64 x13False)False)(x68 x13False)((x2 x63 x12False)False)((x2 x63 x65False)False)((x14 x63 x12 x65False)False)((x64 x63False)False)(x68 x63False)((x2 x15 x12False)False)((x2 x15 x65False)False)((x14 x15 x12 x65False)False)((x64 x15False)False)(x68 x15False)((x2 x6 x12False)False)((x2 x6 x65False)False)((x14 x6 x12 x65False)False)((x64 x6False)False)(x68 x6False)((x11 x63 x6 = x13False)False)((x11 x15 x15 = x13False)False)((x11 x15 x6 = x63False)False)((x11 x6 x63 = x13False)False)((x11 x6 x15 = x63False)False)((x11 x6 x6 = x15False)False)(∀ x69 . (x3 x69 x69False)False)(∀ x69 x70 x71 . (x68 x71False)(x68 x69False)x2 x69 (x1 x71)x2 x70 x69(x14 x70 x71 x69False)False)(∀ x69 x70 x71 . (x68 x71False)(x68 x69False)x2 x69 (x1 x71)x14 x70 x71 x69(x2 x70 x69False)False)((x9 = x67False)False)((x65 = x66False)False)(∀ x69 x70 . x2 x70 x65x4 x69(x8 x70 x69 = x11 x70 x69False)False)(∀ x69 x70 . x4 x70x2 x69 x65(x7 x70 x69 = x11 x70 x69False)False)((x4 x62False)False)(x68 x62False)((x61 x60False)False)((x68 x60False)False)((x59 x58False)False)((x61 x58False)False)((x10 x58False)False)((x68 x58False)False)(∀ x69 . (x68 x69False)(x56 (x57 x69) x69False)False)(∀ x69 . (x68 x69False)(x2 (x57 x69) (x1 x69)False)False)((x4 x55False)False)((x16 x17False)False)((x61 x17False)False)((x59 x18False)False)((x16 x18False)False)((x61 x18False)False)((x10 x18False)False)(∀ x69 . x56 (x19 x69) x69False)(∀ x69 . (x2 (x19 x69) (x1 x69)False)False)((x20 x21False)False)((x54 x21False)False)(x68 x21False)((x64 x53False)False)((x61 x53False)False)((x59 x52False)False)((x64 x52False)False)((x61 x52False)False)((x10 x52False)False)((x10 x51False)False)(x68 x51False)(x68 x50False)(∀ x69 . (x68 (x22 x69)False)False)(∀ x69 . (x2 (x22 x69) (x1 x69)False)False)((x23 x24False)False)((x49 x24False)False)((x25 x24False)False)(x68 x24False)((x23 x26False)False)(x68 x26False)((x2 x26 (x1 x12)False)False)((x54 x48False)False)(x68 x48False)((x61 x47False)False)((x59 x27False)False)((x10 x46False)False)((x68 x28False)False)(∀ x69 . (x68 x69False)x68 (x45 x69)False)(∀ x69 . (x68 x69False)(x2 (x45 x69) (x1 x69)False)False)((x23 x44False)False)((x54 x29False)False)(x68 x29False)(∀ x69 x70 . (x16 x70False)x59 x70(x16 x69False)x59 x69x16 (x11 x70 x69)False)((x23 x66False)False)(x68 x66False)((x54 x66False)False)(∀ x69 x70 . x59 x70x59 x69(x59 (x11 x70 x69)False)False)((x20 x66False)False)((x20 x12False)False)(∀ x69 x70 . x4 x70(x68 x69False)x4 x69x68 (x11 x69 x70)False)(∀ x69 x70 . x4 x70(x68 x69False)x4 x69x68 (x11 x70 x69)False)((x43 x12False)False)(∀ x69 x70 . x10 x70x10 x69(x10 (x11 x70 x69)False)False)((x68 x67False)False)(∀ x69 . x68 (x1 x69)False)(∀ x69 x70 . x4 x70x4 x69(x4 (x11 x70 x69)False)False)(∀ x69 x70 . x16 x70x59 x70(x64 x69False)x59 x69(x16 (x11 x69 x70)False)False)(∀ x69 x70 . x16 x70x59 x70(x64 x69False)x59 x69(x16 (x11 x70 x69)False)False)(∀ x69 x70 . x64 x70x59 x70(x16 x69False)x59 x69(x64 (x11 x69 x70)False)False)(∀ x69 x70 . x64 x70x59 x70(x16 x69False)x59 x69(x64 (x11 x70 x69)False)False)(∀ x69 x70 . (x64 x70False)x59 x70(x64 x69False)x59 x69x64 (x11 x70 x69)False)(∀ x69 x70 . (x68 x70False)(x68 x69False)x2 x69 (x1 x70)(x14 (x42 x69 x70) x70 x69False)False)(∀ x69 . (x2 (x30 x69) x69False)False)(∀ x69 x70 x71 . (x68 x71False)(x68 x69False)x2 x69 (x1 x71)x14 x70 x71 x69(x2 x70 x71False)False)((x14 x9 x12 x65False)False)((x2 x65 (x1 x12)False)False)(∀ x69 x70 x71 . x4 x71x4 x69x4 x70(x2 (x5 x71 x69 x70) x65False)False)(∀ x69 x70 . x2 x70 x65x4 x69(x14 (x8 x70 x69) x12 x65False)False)(∀ x69 x70 . x4 x70x2 x69 x65(x14 (x7 x70 x69) x12 x65False)False)(∀ x69 x70 . x10 x70x10 x69(x11 x70 x69 = x11 x69 x70False)False)(∀ x69 x70 . x2 x70 x65x4 x69(x8 x70 x69 = x8 x69 x70False)False)(∀ x69 x70 . x4 x70x2 x69 x65(x7 x70 x69 = x7 x69 x70False)False)(∀ x69 . x68 x69(x31 x69False)False)(∀ x69 . x61 x69(x64 x69False)(x16 x69False)(x61 x69False)False)(∀ x69 . x61 x69(x64 x69False)(x16 x69False)(x68 x69False)False)(∀ x69 . x2 x69 x66(x4 x69False)False)(∀ x69 . x2 x69 (x1 x12)(x43 x69False)False)(∀ x69 . x68 x69x61 x69x16 x69False)(∀ x69 . x68 x69x61 x69x64 x69False)(∀ x69 . x68 x69x61 x69(x61 x69False)False)(∀ x69 . x68 x69(x4 x69False)False)(∀ x69 . (x68 x69False)x61 x69(x64 x69False)(x16 x69False)False)(∀ x69 . (x68 x69False)x61 x69(x64 x69False)(x61 x69False)False)(∀ x69 . x4 x69(x23 x69False)False)(∀ x69 . x61 x69x16 x69x64 x69False)(∀ x69 . x61 x69x16 x69(x61 x69False)False)(∀ x69 . x61 x69x16 x69x68 x69False)(∀ x69 x70 . x23 x70x2 x69 x70(x23 x69False)False)(∀ x69 . x43 x69(x32 x69False)False)(∀ x69 . (x68 x69False)x61 x69(x16 x69False)(x64 x69False)False)(∀ x69 . (x68 x69False)x61 x69(x16 x69False)(x61 x69False)False)(∀ x69 . x59 x69(x61 x69False)False)(∀ x69 x70 . x68 x70x2 x69 (x1 x70)x56 x69 x70False)(∀ x69 . x68 x69(x41 x69False)False)(∀ x69 . x43 x69(x33 x69False)False)(∀ x69 . x61 x69x64 x69x16 x69False)(∀ x69 . x61 x69x64 x69(x61 x69False)False)(∀ x69 . x61 x69x64 x69x68 x69False)(∀ x69 . x59 x69(x10 x69False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x1 x70)x68 x69(x56 x69 x70False)False)(∀ x69 . x68 x69(x23 x69False)False)(∀ x69 . x4 x69x16 x69False)(∀ x69 . x4 x69(x4 x69False)False)(∀ x69 . x40 x69(x43 x69False)False)(∀ x69 . x4 x69(x61 x69False)False)(∀ x69 . x4 x69(x59 x69False)False)(∀ x69 . x4 x69(x10 x69False)False)(∀ x69 x70 . (x68 x70False)x2 x69 (x1 x70)(x56 x69 x70False)x68 x69False)(∀ x69 . x25 x69x49 x69(x23 x69False)False)(∀ x69 . x2 x69 x65x16 x69False)(∀ x69 . x34 x69(x40 x69False)False)(∀ x69 . x68 x69(x20 x69False)False)(∀ x69 . x2 x69 x65(x54 x69False)False)(∀ x69 x70 . x54 x70x2 x69 (x1 x70)(x54 x69False)False)(∀ x69 x70 . x34 x70x2 x69 (x1 x70)(x34 x69False)False)(∀ x69 x70 . x40 x70x2 x69 (x1 x70)(x40 x69False)False)(∀ x69 x70 . x43 x70x2 x69 (x1 x70)(x43 x69False)False)(∀ x69 x70 . x33 x70x2 x69 (x1 x70)(x33 x69False)False)(∀ x69 . x2 x69 x12(x59 x69False)False)(∀ x69 . x2 x69 x12(x10 x69False)False)(∀ x69 x70 . x68 x70x2 x69 (x1 x70)(x68 x69False)False)(∀ x69 . x23 x69(x49 x69False)False)(∀ x69 . x23 x69(x25 x69False)False)(∀ x69 . x4 x69(x4 x69False)False)(∀ x69 . x4 x69(x23 x69False)False)(∀ x69 . x54 x69(x34 x69False)False)(∀ x69 x70 . x32 x70x2 x69 (x1 x70)(x32 x69False)False)(∀ x69 . x68 x69(x54 x69False)False)(∀ x69 x70 . x54 x70x2 x69 x70(x4 x69False)False)(∀ x69 x70 . x34 x70x2 x69 x70(x39 x69False)False)(∀ x69 x70 . x40 x70x2 x69 x70(x35 x69False)False)(∀ x69 x70 . x43 x70x2 x69 x70(x59 x69False)False)(∀ x69 x70 . x33 x70x2 x69 x70(x61 x69False)False)(∀ x69 x70 . x32 x70x2 x69 x70(x10 x69False)False)(∀ x69 . x2 x69 (x1 x65)(x54 x69False)False)(∀ x69 x70 . x31 x70x2 x69 (x1 x70)(x31 x69False)False)(∀ x69 x70 . x0 x69 x70x0 x70 x69False)(x8 (x5 x36 x37 (x8 x38 x15)) (x5 x36 x37 (x8 x38 x63)) = x5 x36 x37 (x8 x38 x13)False)((x2 x38 x65False)False)((x2 x37 x65False)False)((x2 x36 x65False)False)False (proof)