Search for blocks/addresses/...

Proofgold Asset

asset id
3de27afe8ccce5ce16ac93c3dbc7fbb442de4f715ee2be08a7a9374c41c3be6d
asset hash
ffa21e0f13420c01c064776c667164e866a3f6cdd6c9bdc4cbdcc3851b64e652
bday / block
35162
tx
ad80e..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 4dd7a.. : ∀ 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 . (x28 x32False)x19 x32x27 x32x20 x32x26 x32x21 x32x24 x31 (x25 x32)x24 x29 (x25 x32)x24 x30 (x25 x32)x23 x32 x31 x29x23 x32 x31 x30(x23 x32 x31 (x22 x32 x29 x30)False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x20 x31x21 x31x24 x30 (x25 x31)x24 x29 (x25 x31)(x0 x31 (x22 x31 x30 x29) x30False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x18 x31 x29 x30(x18 x31 x30 x29False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x20 x31x26 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)(x23 x31 x29 x29False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)(x18 x31 x29 x29False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x20 x31x26 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x0 x31 x29 x30(x23 x31 x29 x30False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x20 x31x26 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x23 x31 x29 x30(x0 x31 x29 x30False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x29 = x30(x18 x31 x29 x30False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x18 x31 x29 x30(x29 = x30False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x1 x31x24 x29 (x25 x31)x24 x30 (x25 x31)(x22 x31 x29 x30 = x2 x31 x29 x30False)False)(∀ x29 x30 . (x28 x30False)x19 x30x20 x30x26 x30x21 x30x24 x29 (x25 x30)(x22 x30 x29 x29 = x29False)False)(∀ x29 . (x24 (x3 x29) x29False)False)((x21 x16False)False)((x4 x5False)False)((x15 x14False)False)((x1 x6False)False)(∀ x29 . x21 x29(x4 x29False)False)(∀ x29 . x21 x29(x1 x29False)False)(∀ x29 . x4 x29(x15 x29False)False)(∀ x29 . x1 x29(x15 x29False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x1 x31x24 x29 (x25 x31)x24 x30 (x25 x31)(x24 (x22 x31 x29 x30) (x25 x31)False)False)(∀ x29 x30 x31 . (x28 x31False)x1 x31x24 x30 (x25 x31)x24 x29 (x25 x31)(x24 (x2 x31 x30 x29) (x25 x31)False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x23 x31 x29 x30x23 x31 x30 x29(x18 x31 x29 x30False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x18 x31 x29 x30(x23 x31 x30 x29False)False)(∀ x29 x30 x31 . (x28 x31False)x17 x31x21 x31x24 x29 (x25 x31)x24 x30 (x25 x31)x18 x31 x29 x30(x23 x31 x29 x30False)False)(∀ x29 x30 x31 . (x28 x31False)x19 x31x1 x31x24 x29 (x25 x31)x24 x30 (x25 x31)(x22 x31 x29 x30 = x22 x31 x30 x29False)False)(∀ x29 . x21 x29(x28 x29False)x13 x29x12 x29x19 x29x27 x29x20 x29x26 x29(x17 x29False)False)(∀ x29 . x21 x29(x28 x29False)x13 x29x12 x29x19 x29x27 x29x20 x29x26 x29x28 x29False)(∀ x29 . x21 x29(x28 x29False)x17 x29(x26 x29False)False)(∀ x29 . x21 x29(x28 x29False)x17 x29(x20 x29False)False)(∀ x29 . x21 x29(x28 x29False)x17 x29(x27 x29False)False)(∀ x29 . x21 x29(x28 x29False)x17 x29(x19 x29False)False)(∀ x29 . x21 x29(x28 x29False)x17 x29(x12 x29False)False)(∀ x29 . x21 x29(x28 x29False)x17 x29(x13 x29False)False)(∀ x29 . x21 x29(x28 x29False)x17 x29x28 x29False)(∀ x29 . x24 x29 (x25 x7)x23 x7 x29 x10x23 x7 x29 x8(x23 x7 x29 x9False)(x18 x7 x9 (x22 x7 x10 x8)False)False)((x23 x7 x9 x8False)(x18 x7 x9 (x22 x7 x10 x8)False)False)((x23 x7 x9 x10False)(x18 x7 x9 (x22 x7 x10 x8)False)False)(x18 x7 x9 (x22 x7 x10 x8)x23 x7 x9 x10x23 x7 x9 x8x23 x7 x11 x9False)(x18 x7 x9 (x22 x7 x10 x8)x23 x7 x9 x10x23 x7 x9 x8(x23 x7 x11 x8False)False)(x18 x7 x9 (x22 x7 x10 x8)x23 x7 x9 x10x23 x7 x9 x8(x23 x7 x11 x10False)False)(x18 x7 x9 (x22 x7 x10 x8)x23 x7 x9 x10x23 x7 x9 x8(x24 x11 (x25 x7)False)False)((x24 x8 (x25 x7)False)False)((x24 x10 (x25 x7)False)False)((x24 x9 (x25 x7)False)False)((x21 x7False)False)((x17 x7False)False)(x28 x7False)False (proof)