Search for blocks/addresses/...

Proofgold Asset

asset id
47a3aa18a9cc3c844b42bb70901e121449d48fff97da34d96faa79e42377f552
asset hash
7a165fbfd70cee48e0759ceea6cb48aa1625c0753df8b9e8eb1799a1afe1a082
bday / block
35132
tx
929ac..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 246a2.. : ∀ 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 . x54 x56(x56 = x55False)x54 x55False)(∀ x55 x56 . (x0 x55 (x1 x55 x56)False)False)(∀ x55 x56 . x53 x55 x56x54 x56False)(∀ x55 . x54 x55(x55 = x2False)False)(∀ x55 x56 x57 . x53 x55 x56x51 x56 (x52 x57)x54 x57False)(∀ x55 x56 x57 . x53 x56 x57x51 x57 (x52 x55)(x51 x56 x55False)False)(∀ x55 x56 . x0 x56 x55(x51 x56 (x52 x55)False)False)(∀ x55 x56 . x51 x56 (x52 x55)(x0 x56 x55False)False)(∀ x55 x56 x57 . x53 x56 x57x53 x55 x57x53 x55 (x50 x57 x56)False)(∀ x55 x56 . x53 x56 x55(x53 (x50 x55 x56) x55False)False)(∀ x55 x56 . x51 x55 x56(x54 x56False)(x53 x55 x56False)False)(∀ x55 x56 x57 . (x3 x57False)x6 x57x51 x56 (x52 (x4 x57))x51 x55 (x52 (x4 x57))x0 x56 x55(x0 (x5 x57 x56) (x5 x57 x55)False)False)(∀ x55 x56 . x53 x56 x55(x51 x56 x55False)False)(∀ x55 . (x1 x55 x2 = x55False)False)(x54 x49False)(∀ x55 . (x0 x55 x55False)False)(∀ x55 x56 x57 . x51 x56 (x52 x57)x51 x55 (x52 x57)(x48 x57 x56 x55 = x1 x56 x55False)False)(∀ x55 x56 x57 x58 . (x54 x58False)x11 x55x7 x55 x58 x57x51 x55 (x52 (x8 x58 x57))x51 x56 x58(x9 x58 x57 x55 x56 = x10 x55 x56False)False)(∀ x55 . (x47 x55False)x47 (x46 x55)False)(∀ x55 . (x47 x55False)(x51 (x46 x55) (x52 x55)False)False)(∀ x55 . (x54 x55False)(x47 (x45 x55)False)False)(∀ x55 . (x54 x55False)x54 (x45 x55)False)(∀ x55 . (x54 x55False)(x51 (x45 x55) (x52 x55)False)False)(∀ x55 . (x54 x55False)(x13 (x12 x55) x55False)False)(∀ x55 . (x54 x55False)(x51 (x12 x55) (x52 x55)False)False)(∀ x55 . (x3 x55False)x15 x55x54 (x14 x55)False)(∀ x55 . (x3 x55False)x15 x55(x51 (x14 x55) (x52 (x4 x55))False)False)(∀ x55 . x13 (x16 x55) x55False)(∀ x55 . (x51 (x16 x55) (x52 x55)False)False)(x54 x17False)(∀ x55 . (x54 (x44 x55)False)False)(∀ x55 . (x51 (x44 x55) (x52 x55)False)False)(∀ x55 . (x43 x55False)x15 x55x47 (x42 x55)False)(∀ x55 . (x43 x55False)x15 x55(x51 (x42 x55) (x52 (x4 x55))False)False)(∀ x55 . (x3 x55False)x15 x55(x47 (x41 x55)False)False)(∀ x55 . (x3 x55False)x15 x55x54 (x41 x55)False)(∀ x55 . (x3 x55False)x15 x55(x51 (x41 x55) (x52 (x4 x55))False)False)((x54 x18False)False)(∀ x55 . (x54 x55False)x54 (x40 x55)False)(∀ x55 . (x54 x55False)(x51 (x40 x55) (x52 x55)False)False)(∀ x55 x56 . (x39 (x38 x55 x56) x55False)False)(∀ x55 x56 . (x19 (x38 x56 x55) x55False)False)(∀ x55 x56 . (x37 (x38 x55 x56)False)False)(∀ x55 x56 . (x54 (x38 x55 x56)False)False)(∀ x55 x56 . (x51 (x38 x55 x56) (x52 (x8 x56 x55))False)False)(∀ x55 x56 x57 . x51 x56 (x52 x57)x51 x55 (x52 x57)(x48 x57 x56 x56 = x56False)False)(∀ x55 . (x1 x55 x55 = x55False)False)(∀ x55 x56 x57 x58 x59 . (x3 x59False)x6 x59x51 x58 (x52 (x4 x59))x51 x55 (x4 x59)x57 = x55x51 x56 (x52 (x4 x59))x53 x56 (x20 x59 x55)x0 x56 x58(x53 x57 (x21 x59 x58)False)False)(∀ x55 x56 x57 . (x3 x57False)x6 x57x51 x56 (x52 (x4 x57))x53 x55 (x21 x57 x56)(x0 (x36 x56 x57 x55) x56False)False)(∀ x55 x56 x57 . (x3 x57False)x6 x57x51 x56 (x52 (x4 x57))x53 x55 (x21 x57 x56)(x53 (x36 x56 x57 x55) (x20 x57 (x22 x56 x57 x55))False)False)(∀ x55 x56 x57 . (x3 x57False)x6 x57x51 x56 (x52 (x4 x57))x53 x55 (x21 x57 x56)(x51 (x36 x56 x57 x55) (x52 (x4 x57))False)False)(∀ x55 x56 x57 . (x3 x57False)x6 x57x51 x56 (x52 (x4 x57))x53 x55 (x21 x57 x56)(x55 = x22 x56 x57 x55False)False)(∀ x55 x56 x57 . (x3 x57False)x6 x57x51 x56 (x52 (x4 x57))x53 x55 (x21 x57 x56)(x51 (x22 x56 x57 x55) (x4 x57)False)False)(∀ x55 . (x23 x55False)x15 x55x24 (x4 x55)False)(∀ x55 . x23 x55x15 x55(x24 (x4 x55)False)False)(∀ x55 . x43 x55x15 x55(x47 (x4 x55)False)False)(∀ x55 . (x43 x55False)x15 x55x47 (x4 x55)False)(∀ x55 x56 . (x54 x56False)x54 (x1 x55 x56)False)(∀ x55 x56 . (x54 x56False)x54 (x1 x56 x55)False)(∀ x55 x56 x57 . x37 x57x39 x57 x55x37 x56x39 x56 x55(x39 (x1 x57 x56) x55False)False)(∀ x55 . (x3 x55False)x15 x55x54 (x4 x55)False)((x54 x2False)False)(∀ x55 . x54 (x52 x55)False)(∀ x55 . x3 x55x15 x55(x54 (x4 x55)False)False)(∀ x55 x56 x57 . x37 x57x19 x57 x55x37 x56x19 x56 x55(x19 (x1 x57 x56) x55False)False)(∀ x55 x56 . (x54 x56False)(x54 x55False)x54 (x8 x56 x55)False)(∀ x55 . (x51 (x35 x55) x55False)False)((x15 x25False)False)((x6 x34False)False)(∀ x55 . x6 x55(x51 (x26 x55) (x52 (x8 (x4 x55) (x52 (x52 (x4 x55)))))False)False)(∀ x55 . x6 x55(x7 (x26 x55) (x4 x55) (x52 (x52 (x4 x55)))False)False)(∀ x55 . x6 x55(x11 (x26 x55)False)False)((x54 x33False)False)(∀ x55 . x6 x55(x15 x55False)False)(∀ x55 x56 . (x3 x56False)x6 x56x51 x55 (x4 x56)(x51 (x20 x56 x55) (x52 (x52 (x4 x56)))False)False)(∀ x55 x56 x57 . x51 x56 (x52 x57)x51 x55 (x52 x57)(x51 (x48 x57 x56 x55) (x52 x57)False)False)(∀ x55 x56 x57 x58 . (x54 x58False)x11 x55x7 x55 x58 x57x51 x55 (x52 (x8 x58 x57))x51 x56 x58(x51 (x9 x58 x57 x55 x56) x57False)False)(∀ x55 x56 . (x3 x56False)x6 x56x51 x55 (x52 (x4 x56))(x51 (x5 x56 x55) (x52 (x4 x56))False)False)(∀ x55 x56 . (x3 x56False)x6 x56x51 x55 (x4 x56)(x20 x56 x55 = x9 (x4 x56) (x52 (x52 (x4 x56))) (x26 x56) x55False)False)(∀ x55 x56 x57 . (x53 (x27 x55 x56 x57) x57False)(x53 (x27 x55 x56 x57) x56False)(x53 (x27 x55 x56 x57) x55False)(x55 = x1 x57 x56False)False)(∀ x55 x56 x57 . x53 (x27 x55 x56 x57) x55x53 (x27 x55 x56 x57) x56(x55 = x1 x57 x56False)False)(∀ x55 x56 x57 . x53 (x27 x55 x56 x57) x55x53 (x27 x55 x56 x57) x57(x55 = x1 x57 x56False)False)(∀ x55 x56 x57 x58 . x57 = x1 x55 x56x53 x58 x56(x53 x58 x57False)False)(∀ x55 x56 x57 x58 . x57 = x1 x56 x55x53 x58 x56(x53 x58 x57False)False)(∀ x55 x56 x57 x58 . x58 = x1 x56 x57x53 x55 x58(x53 x55 x56False)(x53 x55 x57False)False)(∀ x55 x56 . x53 (x28 x55 x56) x55(x0 x56 x55False)False)(∀ x55 x56 . (x53 (x28 x55 x56) x56False)(x0 x56 x55False)False)(∀ x55 x56 x57 . x0 x56 x57x53 x55 x56(x53 x55 x57False)False)((x2 = x33False)False)(∀ x55 x56 . (x3 x56False)x6 x56x51 x55 (x52 (x4 x56))(x5 x56 x55 = x21 x56 x55False)False)(∀ x55 x56 x57 . x51 x56 (x52 x57)x51 x55 (x52 x57)(x48 x57 x56 x55 = x48 x57 x55 x56False)False)(∀ x55 x56 . (x1 x56 x55 = x1 x55 x56False)False)(∀ x55 . x15 x55x32 x55 x2(x3 x55False)False)(∀ x55 . x15 x55x3 x55(x32 x55 x2False)False)(∀ x55 . x15 x55(x23 x55False)x43 x55False)(∀ x55 . x15 x55x43 x55(x23 x55False)False)(∀ x55 x56 . x47 x56x51 x55 (x52 x56)(x47 x55False)False)(∀ x55 . x15 x55(x23 x55False)x23 x55False)(∀ x55 . x15 x55(x23 x55False)x3 x55False)(∀ x55 x56 . x54 x56x51 x55 (x52 x56)x13 x55 x56False)(∀ x55 . x15 x55x3 x55(x23 x55False)False)(∀ x55 . x15 x55x3 x55(x3 x55False)False)(∀ x55 x56 x57 . x54 x57x51 x55 (x52 (x8 x56 x57))(x54 x55False)False)(∀ x55 x56 . (x54 x56False)x51 x55 (x52 x56)x54 x55(x13 x55 x56False)False)(∀ x55 x56 x57 . x54 x57x51 x55 (x52 (x8 x57 x56))(x54 x55False)False)(∀ x55 x56 . (x54 x56False)x51 x55 (x52 x56)(x13 x55 x56False)x54 x55False)(∀ x55 . x15 x55(x43 x55False)x3 x55False)(∀ x55 x56 x57 . x51 x57 (x52 (x8 x55 x56))(x39 x57 x56False)False)(∀ x55 x56 x57 . x51 x57 (x52 (x8 x56 x55))(x19 x57 x56False)False)(∀ x55 x56 . x54 x56x51 x55 (x52 x56)(x54 x55False)False)(∀ x55 . x15 x55x3 x55(x43 x55False)False)(∀ x55 x56 x57 . x51 x57 (x52 (x8 x55 x56))(x37 x57False)False)(∀ x55 . x15 x55(x43 x55False)x3 x55False)(∀ x55 . x15 x55x32 x55 x49(x43 x55False)False)(∀ x55 . x15 x55x32 x55 x49x3 x55False)(∀ x55 . x15 x55(x3 x55False)x43 x55(x32 x55 x49False)False)(∀ x55 x56 . x53 x55 x56x53 x56 x55False)(x0 (x48 (x4 x29) (x5 x29 x30) (x5 x29 x31)) (x5 x29 (x48 (x4 x29) x30 x31))False)((x51 x31 (x52 (x4 x29))False)False)((x51 x30 (x52 (x4 x29))False)False)((x6 x29False)False)(x3 x29False)False (proof)