Search for blocks/addresses/...

Proofgold Asset

asset id
fa92ae8e55c88ac5ec554a1edd464fcd649a8f69d069f6a808e0e8d697f97d23
asset hash
95843f1842963679abee09bdf6823c68bf94f9f2592b67d1dc1b734fb1ab6423
bday / block
35148
tx
1f8be..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 1d20f.. : ∀ 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 . x34 x36(x36 = x35False)x34 x35False)(∀ x35 x36 . x0 x35 x36x34 x36False)(∀ x35 . x34 x35(x35 = x33False)False)(∀ x35 x36 x37 . x0 x35 x36x2 x36 (x1 x37)x34 x37False)(∀ x35 x36 x37 . x0 x36 x37x2 x37 (x1 x35)(x2 x36 x35False)False)(∀ x35 x36 . x3 x36 x35(x2 x36 (x1 x35)False)False)(∀ x35 x36 . x2 x36 (x1 x35)(x3 x36 x35False)False)(∀ x35 x36 . x2 x35 x36(x34 x36False)(x0 x35 x36False)False)(∀ x35 x36 . x0 x36 x35(x2 x36 x35False)False)(∀ x35 . (x3 x35 x35False)False)(x32 x31False)(x34 x4False)((x30 x29False)False)((x5 x29False)False)((x28 x27False)False)((x6 x27False)False)((x5 x27False)False)((x32 x7False)False)(x34 x7False)((x34 x8False)False)((x5 x26False)False)(x34 x26False)((x6 x25False)False)((x5 x25False)False)(∀ x35 . (x34 x35False)x5 x35x34 (x24 x35)False)(∀ x35 . x32 x35x5 x35(x32 (x24 x35)False)False)(∀ x35 x36 . x34 x36x5 x36(x34 (x23 x36 x35)False)False)(∀ x35 x36 . x5 x36x34 x35(x34 (x23 x36 x35)False)False)(∀ x35 x36 . x34 x36x5 x36(x34 (x22 x36 x35)False)False)((x34 x33False)False)(∀ x35 x36 . x5 x36x34 x35(x34 (x22 x36 x35)False)False)(∀ x35 . x34 x35(x34 (x24 x35)False)False)(∀ x35 . (x2 (x21 x35) x35False)False)((x34 x9False)False)(∀ x35 x36 x37 . x5 x37x6 x37(x0 (x19 x37 (x20 x35 x36 x37)) x36False)(x0 (x20 x35 x36 x37) x35False)(x35 = x23 x37 x36False)False)(∀ x35 x36 x37 . x5 x37x6 x37(x0 (x20 x35 x36 x37) (x24 x37)False)(x0 (x20 x35 x36 x37) x35False)(x35 = x23 x37 x36False)False)(∀ x35 x36 x37 . x5 x37x6 x37x0 (x20 x35 x36 x37) x35x0 (x20 x35 x36 x37) (x24 x37)x0 (x19 x37 (x20 x35 x36 x37)) x36(x35 = x23 x37 x36False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x37 = x23 x38 x36x0 x35 (x24 x38)x0 (x19 x38 x35) x36(x0 x35 x37False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x37 = x23 x38 x36x0 x35 x37(x0 (x19 x38 x35) x36False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x36 = x23 x38 x35x0 x37 x36(x0 x37 (x24 x38)False)False)(∀ x35 x36 x37 . x5 x37x6 x37(x18 x35 x36 x37 = x19 x37 (x17 x35 x36 x37)False)(x0 (x18 x35 x36 x37) x35False)(x35 = x22 x37 x36False)False)(∀ x35 x36 x37 . x5 x37x6 x37(x0 (x17 x35 x36 x37) x36False)(x0 (x18 x35 x36 x37) x35False)(x35 = x22 x37 x36False)False)(∀ x35 x36 x37 . x5 x37x6 x37(x0 (x17 x35 x36 x37) (x24 x37)False)(x0 (x18 x35 x36 x37) x35False)(x35 = x22 x37 x36False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x0 (x18 x37 x36 x38) x37x0 x35 (x24 x38)x0 x35 x36x18 x37 x36 x38 = x19 x38 x35(x37 = x22 x38 x36False)False)(∀ x35 x36 x37 x38 x39 . x5 x39x6 x39x38 = x22 x39 x37x0 x35 (x24 x39)x0 x35 x37x36 = x19 x39 x35(x0 x36 x38False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x37 = x22 x38 x36x0 x35 x37(x35 = x19 x38 (x10 x35 x37 x36 x38)False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x37 = x22 x38 x36x0 x35 x37(x0 (x10 x35 x37 x36 x38) x36False)False)(∀ x35 x36 x37 x38 . x5 x38x6 x38x37 = x22 x38 x36x0 x35 x37(x0 (x10 x35 x37 x36 x38) (x24 x38)False)False)(∀ x35 . x5 x35x6 x35x16 x35 = x15 x35(x28 x35False)False)(∀ x35 . x5 x35x6 x35(x19 x35 (x16 x35) = x19 x35 (x15 x35)False)(x28 x35False)False)(∀ x35 . x5 x35x6 x35(x0 (x15 x35) (x24 x35)False)(x28 x35False)False)(∀ x35 . x5 x35x6 x35(x0 (x16 x35) (x24 x35)False)(x28 x35False)False)(∀ x35 x36 x37 . x5 x37x6 x37x28 x37x0 x35 (x24 x37)x0 x36 (x24 x37)x19 x37 x35 = x19 x37 x36(x35 = x36False)False)(∀ x35 x36 . x0 (x11 x35 x36) x35(x3 x36 x35False)False)(∀ x35 x36 . (x0 (x11 x35 x36) x36False)(x3 x36 x35False)False)(∀ x35 x36 x37 . x3 x36 x37x0 x35 x36(x0 x35 x37False)False)((x33 = x9False)False)(∀ x35 . x34 x35x5 x35(x30 x35False)False)(∀ x35 . x34 x35x5 x35(x5 x35False)False)(∀ x35 . x34 x35x5 x35(x12 x35False)False)(∀ x35 . x34 x35x5 x35(x5 x35False)False)(∀ x35 . (x32 x35False)x34 x35False)(∀ x35 x36 . x5 x36x2 x35 (x1 x36)(x5 x35False)False)(∀ x35 . x34 x35x5 x35x6 x35(x28 x35False)False)(∀ x35 . x34 x35x5 x35x6 x35(x6 x35False)False)(∀ x35 . x34 x35x5 x35x6 x35(x5 x35False)False)(∀ x35 . x34 x35(x32 x35False)False)(∀ x35 . x34 x35(x5 x35False)False)(∀ x35 . x34 x35(x6 x35False)False)(∀ x35 x36 . x0 x35 x36x0 x36 x35False)(x3 (x23 x14 (x22 x14 x13)) x13False)((x28 x14False)False)((x6 x14False)False)((x5 x14False)False)False (proof)