Search for blocks/addresses/...

Proofgold Asset

asset id
4e8b79e3bba44f00b455beddb07f84d874fab566ffca1d512ff82dfa396fe1a8
asset hash
b51a8f2723b1ff4a777f7981c55fb15ecd3cb1cfa8f0affd8ac257bfda957163
bday / block
35136
tx
6d6a7..
preasset
doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 49180.. : ∀ 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 . x46 x48(x48 = x47False)x46 x47False)(∀ x47 x48 . x0 x47 x48x46 x48False)(∀ x47 . x46 x47(x47 = x45False)False)(∀ x47 . x1 x47(x2 x47 x3 = x47False)False)(∀ x47 x48 x49 . x0 x47 x48x43 x48 (x44 x49)x46 x49False)(∀ x47 . x1 x47(x2 x4 x47 = x4False)False)(∀ x47 x48 x49 . x0 x48 x49x43 x49 (x44 x47)(x43 x48 x47False)False)(∀ x47 . x1 x47(x5 x47 x4 = x47False)False)(∀ x47 x48 . x42 x48 x47(x43 x48 (x44 x47)False)False)(∀ x47 x48 . x43 x48 (x44 x47)(x42 x48 x47False)False)(∀ x47 . x1 x47(x41 x3 x47 = x47False)False)(∀ x47 x48 . x43 x47 x48(x46 x48False)(x0 x47 x48False)False)(∀ x47 . x1 x47(x41 x47 x4 = x4False)False)(∀ x47 x48 . x0 x48 x47(x43 x48 x47False)False)((x43 x45 x40False)False)(∀ x47 . x1 x47(x6 x47 x4 = x47False)False)(∀ x47 x48 . x1 x48x1 x47(x5 (x39 x48) (x39 x47) = x5 x47 x48False)False)(∀ x47 x48 . x1 x48x1 x47(x6 (x39 x48) (x39 x47) = x39 (x6 x48 x47)False)False)(∀ x47 x48 x49 . x1 x49x1 x47x1 x48(x41 (x41 x49 x47) x48 = x41 x49 (x41 x47 x48)False)False)(∀ x47 x48 x49 . x1 x49x1 x47x1 x48(x6 (x6 x49 x47) x48 = x6 x49 (x6 x47 x48)False)False)(∀ x47 x48 x49 . x1 x49x1 x47x1 x48(x41 (x6 x49 x47) x48 = x6 (x41 x49 x48) (x41 x47 x48)False)False)(∀ x47 x48 x49 . x1 x49x1 x47x1 x48(x41 x49 (x2 x47 x48) = x2 (x41 x49 x47) x48False)False)((x43 x37 x38False)False)((x43 x37 x7False)False)((x36 x37 x38 x7False)False)((x8 x37False)False)(x46 x37False)(∀ x47 . x1 x47(x41 x47 (x39 x3) = x39 x47False)False)((x43 x3 x38False)False)((x43 x3 x7False)False)((x36 x3 x38 x7False)False)((x8 x3False)False)(x46 x3False)(∀ x47 x48 . x1 x48x1 x47(x6 x48 (x39 x47) = x5 x48 x47False)False)((x43 x35 x38False)False)((x43 x35 x7False)False)((x36 x35 x38 x7False)False)((x46 x35False)False)((x39 (x2 (x39 x3) x37) = x2 x3 x37False)False)((x39 (x2 x3 x37) = x2 (x39 x3) x37False)False)((x39 (x39 x37) = x37False)False)((x39 (x39 x3) = x3False)False)((x39 x37 = x39 x37False)False)((x39 x3 = x39 x3False)False)((x39 x35 = x35False)False)((x41 (x2 (x39 x3) x37) (x39 x37) = x3False)False)((x41 (x2 (x39 x3) x37) x37 = x39 x3False)False)((x41 (x2 (x39 x3) x37) x3 = x2 (x39 x3) x37False)False)((x41 (x2 x3 x37) (x39 x37) = x39 x3False)False)((x41 (x2 x3 x37) x37 = x3False)False)((x41 (x2 x3 x37) x3 = x2 x3 x37False)False)((x41 (x2 x3 x37) x35 = x35False)False)((x41 (x39 x37) (x2 (x39 x3) x37) = x3False)False)((x41 (x39 x37) (x2 x3 x37) = x39 x3False)False)((x41 (x39 x37) x3 = x39 x37False)False)((x41 (x39 x37) x35 = x35False)False)((x41 x37 (x2 (x39 x3) x37) = x39 x3False)False)((x41 x37 (x2 x3 x37) = x3False)False)((x41 x37 x3 = x37False)False)((x41 x37 x35 = x35False)False)((x41 x3 (x2 (x39 x3) x37) = x2 (x39 x3) x37False)False)((x41 x3 (x2 x3 x37) = x2 x3 x37False)False)((x41 x3 (x39 x37) = x39 x37False)False)((x41 x3 x37 = x37False)False)((x41 x3 x3 = x3False)False)((x41 x3 x35 = x35False)False)((x41 x35 (x2 x3 x37) = x35False)False)((x41 x35 (x39 x37) = x35False)False)((x41 x35 x37 = x35False)False)((x41 x35 x3 = x35False)False)((x41 x35 x35 = x35False)False)((x2 (x39 x37) x37 = x39 x3False)False)((x2 (x39 x3) x37 = x2 (x39 x3) x37False)False)((x2 (x39 x3) x3 = x39 x3False)False)((x2 x37 x37 = x3False)False)((x2 x37 x3 = x37False)False)((x2 x3 (x2 (x39 x3) x37) = x39 x37False)False)((x2 x3 (x2 x3 x37) = x37False)False)((x2 x3 (x39 x37) = x2 (x39 x3) x37False)False)((x2 x3 (x39 x3) = x39 x3False)False)((x2 x3 x37 = x2 x3 x37False)False)((x2 x3 x3 = x3False)False)((x5 (x2 (x39 x3) x37) (x2 (x39 x3) x37) = x35False)False)((x5 (x2 (x39 x3) x37) (x2 x3 x37) = x39 x3False)False)((x5 (x2 (x39 x3) x37) (x39 x3) = x2 x3 x37False)False)((x5 (x2 (x39 x3) x37) x35 = x2 (x39 x3) x37False)False)((x5 (x2 x3 x37) (x2 (x39 x3) x37) = x3False)False)((x5 (x2 x3 x37) (x2 x3 x37) = x35False)False)((x5 (x2 x3 x37) x3 = x2 (x39 x3) x37False)False)((x5 (x2 x3 x37) x35 = x2 x3 x37False)False)((x5 (x39 x37) (x39 x37) = x35False)False)((x5 (x39 x37) (x39 x3) = x39 x3False)False)((x5 (x39 x37) x35 = x39 x37False)False)((x5 (x39 x3) (x2 (x39 x3) x37) = x2 (x39 x3) x37False)False)((x5 (x39 x3) (x39 x37) = x3False)False)((x5 (x39 x3) (x39 x3) = x35False)False)((x5 (x39 x3) x3 = x39 x37False)False)((x5 (x39 x3) x35 = x39 x3False)False)((x5 x37 x37 = x35False)False)((x5 x37 x3 = x3False)False)((x5 x37 x35 = x37False)False)((x5 x3 (x2 x3 x37) = x2 x3 x37False)False)((x5 x3 (x39 x3) = x37False)False)((x5 x3 x37 = x39 x3False)False)((x5 x3 x3 = x35False)False)((x5 x3 x35 = x3False)False)((x5 x35 (x2 (x39 x3) x37) = x2 x3 x37False)False)((x5 x35 (x2 x3 x37) = x2 (x39 x3) x37False)False)((x5 x35 (x39 x37) = x37False)False)((x5 x35 (x39 x3) = x3False)False)((x5 x35 x37 = x39 x37False)False)((x5 x35 x3 = x39 x3False)False)((x5 x35 x35 = x35False)False)((x6 (x2 (x39 x3) x37) (x2 (x39 x3) x37) = x39 x3False)False)((x6 (x2 (x39 x3) x37) (x2 x3 x37) = x35False)False)((x6 (x2 (x39 x3) x37) x3 = x2 x3 x37False)False)((x6 (x2 x3 x37) (x2 (x39 x3) x37) = x35False)False)((x6 (x2 x3 x37) (x2 x3 x37) = x3False)False)((x6 (x2 x3 x37) (x39 x3) = x2 (x39 x3) x37False)False)((x6 (x2 x3 x37) x35 = x2 x3 x37False)False)((x6 (x39 x37) x37 = x35False)False)((x6 (x39 x37) x3 = x39 x3False)False)((x6 (x39 x3) (x2 x3 x37) = x2 (x39 x3) x37False)False)((x6 (x39 x3) (x39 x3) = x39 x37False)False)((x6 (x39 x3) x37 = x3False)False)((x6 (x39 x3) x3 = x35False)False)((x6 (x39 x3) x35 = x39 x3False)False)((x6 x37 (x39 x37) = x35False)False)((x6 x37 (x39 x3) = x3False)False)((x6 x37 x35 = x37False)False)((x6 x3 (x2 (x39 x3) x37) = x2 x3 x37False)False)((x6 x3 (x39 x37) = x39 x3False)False)((x6 x3 (x39 x3) = x35False)False)((x6 x3 x3 = x37False)False)((x6 x3 x35 = x3False)False)((x6 x35 (x2 (x39 x3) x37) = x2 (x39 x3) x37False)False)((x6 x35 (x2 x3 x37) = x2 x3 x37False)False)((x6 x35 (x39 x37) = x39 x37False)False)((x6 x35 (x39 x3) = x39 x3False)False)((x6 x35 x37 = x37False)False)((x6 x35 x3 = x3False)False)((x6 x35 x35 = x35False)False)(∀ x47 . (x42 x47 x47False)False)(∀ x47 x48 x49 . (x46 x49False)(x46 x47False)x43 x47 (x44 x49)x43 x48 x47(x36 x48 x49 x47False)False)(∀ x47 x48 x49 . (x46 x49False)(x46 x47False)x43 x47 (x44 x49)x36 x48 x49 x47(x43 x48 x47False)False)((x4 = x45False)False)((x7 = x40False)False)((x9 x10False)False)(x46 x10False)((x9 x11False)False)((x1 x34False)False)(x46 x34False)((x33 x32False)False)((x12 x32False)False)((x31 x32False)False)(x46 x32False)((x1 x30False)False)((x13 x14False)False)((x33 x29False)False)(∀ x47 . x1 x47(x39 (x39 x47) = x47False)False)(∀ x47 . x13 x47(x28 (x28 x47) = x47False)False)(∀ x47 x48 . x13 x48x13 x47(x15 x48 x48 = x48False)False)(∀ x47 x48 . x13 x48x13 x47(x27 x48 x48 = x48False)False)(∀ x47 x48 . (x46 x48False)x1 x48(x46 x47False)x1 x47x46 (x2 x48 x47)False)(∀ x47 x48 . (x46 x48False)x1 x48(x46 x47False)x1 x47x46 (x41 x48 x47)False)(∀ x47 . (x46 x47False)x1 x47(x1 (x39 x47)False)False)(∀ x47 . (x46 x47False)x1 x47x46 (x39 x47)False)(∀ x47 x48 . x13 x48x13 x47(x13 (x16 x48 x47)False)False)((x33 x40False)False)(x46 x40False)(∀ x47 x48 . x1 x48x1 x47(x1 (x2 x48 x47)False)False)(∀ x47 x48 . x13 x48x13 x47(x13 (x17 x48 x47)False)False)(∀ x47 x48 . x1 x48x1 x47(x1 (x5 x48 x47)False)False)(∀ x47 x48 . x13 x48x13 x47(x13 (x15 x48 x47)False)False)(∀ x47 x48 . x1 x48x1 x47(x1 (x41 x48 x47)False)False)(∀ x47 x48 . x13 x48x13 x47(x13 (x27 x48 x47)False)False)(∀ x47 x48 . x1 x48x1 x47(x1 (x6 x48 x47)False)False)((x13 x18False)False)((x13 x26False)False)(∀ x47 x48 . (x46 x48False)(x46 x47False)x43 x47 (x44 x48)(x36 (x19 x47 x48) x48 x47False)False)(∀ x47 . (x43 (x25 x47) x47False)False)(∀ x47 x48 x49 . (x46 x49False)(x46 x47False)x43 x47 (x44 x49)x36 x48 x49 x47(x43 x48 x49False)False)((x36 x4 x38 x7False)False)((x43 x7 (x44 x38)False)False)(∀ x47 . x1 x47(x1 (x39 x47)False)False)(∀ x47 . x13 x47(x13 (x28 x47)False)False)(∀ x47 x48 . x13 x48x13 x47(x16 x48 x47 = x27 (x17 x48 x47) (x17 x47 x48)False)False)(∀ x47 x48 . x13 x48x13 x47(x17 x48 x47 = x15 (x28 x48) x47False)False)(∀ x47 x48 . x13 x48x13 x47(x15 x48 x47 = x28 (x27 (x28 x48) (x28 x47))False)False)(∀ x47 x48 . x13 x48x13 x47(x27 x48 x47 = x41 x48 x47False)False)(∀ x47 . x13 x47(x28 x47 = x5 x3 x47False)False)(∀ x47 . x47 = x18(x13 x47False)False)(∀ x47 . x47 = x26(x13 x47False)False)(∀ x47 . x13 x47(x47 = x26False)(x47 = x18False)False)((x18 = x3False)False)((x26 = x4False)False)(∀ x47 x48 . x13 x48x13 x47(x16 x48 x47 = x16 x47 x48False)False)(∀ x47 x48 . x13 x48x13 x47(x15 x48 x47 = x15 x47 x48False)False)(∀ x47 x48 . x13 x48x13 x47(x27 x48 x47 = x27 x47 x48False)False)(∀ x47 x48 . x1 x48x1 x47(x41 x48 x47 = x41 x47 x48False)False)(∀ x47 x48 . x1 x48x1 x47(x6 x48 x47 = x6 x47 x48False)False)(∀ x47 . x46 x47(x20 x47False)False)(∀ x47 . x43 x47 x40(x9 x47False)False)(∀ x47 . x46 x47(x9 x47False)False)(∀ x47 . x9 x47(x33 x47False)False)(∀ x47 x48 . x33 x48x43 x47 x48(x33 x47False)False)(∀ x47 . x46 x47(x24 x47False)False)(∀ x47 . x46 x47(x33 x47False)False)(∀ x47 . x9 x47(x1 x47False)False)(∀ x47 . x31 x47x12 x47(x33 x47False)False)(∀ x47 . x43 x47 x38(x1 x47False)False)(∀ x47 . x13 x47(x9 x47False)False)(∀ x47 . x33 x47(x12 x47False)False)(∀ x47 . x33 x47(x31 x47False)False)(∀ x47 x48 . x20 x48x43 x47 (x44 x48)(x20 x47False)False)(∀ x47 x48 . x0 x47 x48x0 x48 x47False)(x16 x23 x22 = x18False)((x16 x21 x22 = x18False)False)((x16 x23 x21 = x18False)False)((x13 x22False)False)((x13 x21False)False)((x13 x23False)False)False (proof)