Search for blocks/addresses/...

Proofgold Asset

asset id
93b073a735b6332511c14fd7ecb638cdb4d0206bd35f1d2811d0a5c5a37de178
asset hash
3408c2eecc07d7f68a794c5e46e36e7e730ad445c6adba5c934f45ede293eb41
bday / block
35164
tx
6940a..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem f3acb.. : ∀ 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)(x34 x4False)(∀ x35 . (x3 x35 x35False)False)(∀ x35 . x5 x35(x7 (x6 x35) x35False)False)(∀ x35 . x5 x35(x2 (x6 x35) (x1 (x32 x35))False)False)(∀ x35 . (x8 x35False)x10 x35x34 (x9 x35)False)(∀ x35 . (x8 x35False)x10 x35(x2 (x9 x35) (x1 (x32 x35))False)False)(∀ x35 . (x11 x35False)x10 x35x12 (x13 x35)False)(∀ x35 . (x11 x35False)x10 x35(x2 (x13 x35) (x1 (x32 x35))False)False)(∀ x35 . (x8 x35False)x10 x35(x12 (x14 x35)False)False)(∀ x35 . (x8 x35False)x10 x35x34 (x14 x35)False)(∀ x35 . (x8 x35False)x10 x35(x2 (x14 x35) (x1 (x32 x35))False)False)((x31 x30False)False)((x5 x30False)False)((x31 x29False)False)((x8 x29False)False)((x5 x29False)False)(∀ x35 x36 x37 x38 . x2 x37 (x1 (x1 x38))x15 x38 x37 = x15 x36 x35(x37 = x35False)False)(∀ x35 x36 x37 x38 . x2 x37 (x1 (x1 x38))x15 x38 x37 = x15 x35 x36(x38 = x35False)False)(∀ x35 . (x16 x35False)x10 x35x17 (x32 x35)False)(∀ x35 x36 . (x34 x36False)x2 x35 (x1 (x1 x36))(x31 (x15 x36 x35)False)False)(∀ x35 x36 . (x34 x36False)x2 x35 (x1 (x1 x36))x8 (x15 x36 x35)False)(∀ x35 . x16 x35x10 x35(x17 (x32 x35)False)False)(∀ x35 . x11 x35x10 x35(x12 (x32 x35)False)False)(∀ x35 . (x8 x35False)x5 x35(x31 (x15 (x32 x35) (x28 x35))False)False)(∀ x35 . (x8 x35False)x5 x35x8 (x15 (x32 x35) (x28 x35))False)(∀ x35 . (x11 x35False)x10 x35x12 (x32 x35)False)(∀ x35 . (x8 x35False)x10 x35x34 (x32 x35)False)(∀ x35 . x8 x35x10 x35(x34 (x32 x35)False)False)(∀ x35 . (x2 (x18 x35) x35False)False)((x10 x27False)False)((x5 x19False)False)(∀ x35 . x5 x35(x2 (x28 x35) (x1 (x1 (x32 x35)))False)False)((x34 x20False)False)(∀ x35 . x5 x35(x10 x35False)False)(∀ x35 x36 . x2 x36 (x1 (x1 x35))(x5 (x15 x35 x36)False)False)(∀ x35 x36 . x2 x36 (x1 (x1 x35))(x31 (x15 x35 x36)False)False)(∀ x35 x36 . x0 (x21 x35 x36) x35(x3 x36 x35False)False)(∀ x35 x36 . (x0 (x21 x35 x36) x36False)(x3 x36 x35False)False)(∀ x35 x36 x37 . x3 x36 x37x0 x35 x36(x0 x35 x37False)False)((x33 = x20False)False)(∀ x35 x36 . x5 x36x2 x35 (x1 (x32 x36))x0 x35 (x28 x36)(x22 x35 x36False)False)(∀ x35 x36 . x5 x36x2 x35 (x1 (x32 x36))x22 x35 x36(x0 x35 (x28 x36)False)False)(∀ x35 x36 . x3 x36 x35x3 x35 x36(x36 = x35False)False)(∀ x35 x36 . x35 = x36(x3 x36 x35False)False)(∀ x35 x36 . x36 = x35(x3 x36 x35False)False)(∀ x35 . x10 x35x26 x35 x33(x8 x35False)False)(∀ x35 . x5 x35x8 x35(x23 x35False)False)(∀ x35 . x10 x35x8 x35(x26 x35 x33False)False)(∀ x35 . x10 x35(x16 x35False)x11 x35False)(∀ x35 . x10 x35x11 x35(x16 x35False)False)(∀ x35 . x10 x35(x16 x35False)x16 x35False)(∀ x35 . x10 x35(x16 x35False)x8 x35False)(∀ x35 . x10 x35x8 x35(x16 x35False)False)(∀ x35 . x10 x35x8 x35(x8 x35False)False)(∀ x35 x36 . x5 x36x2 x35 (x1 (x32 x36))x34 x35(x7 x35 x36False)False)(∀ x35 . x10 x35(x11 x35False)x8 x35False)(∀ x35 . x10 x35x8 x35(x11 x35False)False)(∀ x35 . x10 x35(x11 x35False)x8 x35False)(∀ x35 . x10 x35x26 x35 x4(x11 x35False)False)(∀ x35 . x10 x35x26 x35 x4x8 x35False)(∀ x35 . x10 x35(x8 x35False)x11 x35(x26 x35 x4False)False)(∀ x35 x36 . x0 x35 x36x0 x36 x35False)(∀ x35 . x5 x35x31 x35(x35 = x15 (x32 x35) (x28 x35)False)False)(x15 (x32 x25) (x28 x25) = x15 (x32 x24) (x28 x24)False)(∀ x35 x36 . x2 x36 (x1 (x32 x25))x2 x35 (x1 (x32 x24))x36 = x35x22 x35 x24(x22 x36 x25False)False)(∀ x35 x36 . x2 x36 (x1 (x32 x25))x2 x35 (x1 (x32 x24))x36 = x35x22 x36 x25(x22 x35 x24False)False)((x32 x25 = x32 x24False)False)((x5 x24False)False)((x5 x25False)False)False (proof)