Search for blocks/addresses/...

Proofgold Address

address
PUaXw4HzGNfrXXZseWZ5YiGgrpzcYXVHvab
total
0
mg
-
conjpub
-
current assets
c85f2../a74f1.. bday: 35159 doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 025bf.. : ∀ 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 . x47 x49(x49 = x48False)x47 x48False)(∀ x48 x49 . x0 x48 x49x47 x49False)(∀ x48 . x47 x48(x48 = x46False)False)(∀ x48 . x1 x48(x2 x48 x3 = x48False)False)(∀ x48 x49 x50 . x0 x48 x49x44 x49 (x45 x50)x47 x50False)(∀ x48 x49 x50 . x0 x49 x50x44 x50 (x45 x48)(x44 x49 x48False)False)(∀ x48 x49 . x43 x49 x48(x44 x49 (x45 x48)False)False)(∀ x48 x49 . x44 x49 (x45 x48)(x43 x49 x48False)False)(∀ x48 . x1 x48(x42 x3 x48 = x48False)False)(∀ x48 x49 . x44 x48 x49(x47 x49False)(x0 x48 x49False)False)(∀ x48 x49 . x0 x49 x48(x44 x49 x48False)False)((x44 x46 x4False)False)(∀ x48 x49 . x1 x49x1 x48(x40 (x41 x49) (x41 x48) = x40 x48 x49False)False)(∀ x48 x49 x50 . x1 x50x1 x48x1 x49(x42 (x42 x50 x48) x49 = x42 x50 (x42 x48 x49)False)False)(∀ x48 x49 x50 . x1 x50x1 x48x1 x49(x42 x50 (x2 x48 x49) = x2 (x42 x50 x48) x49False)False)(∀ x48 . x1 x48(x42 x48 (x41 x3) = x41 x48False)False)((x44 x3 x39False)False)((x44 x3 x5False)False)((x38 x3 x39 x5False)False)((x6 x3False)False)(x47 x3False)((x44 x7 x39False)False)((x44 x7 x5False)False)((x38 x7 x39 x5False)False)((x47 x7False)False)((x41 (x41 x3) = x3False)False)((x41 x3 = x41 x3False)False)((x41 x7 = x7False)False)((x42 x3 x3 = x3False)False)((x42 x3 x7 = x7False)False)((x42 x7 x3 = x7False)False)((x42 x7 x7 = x7False)False)((x2 (x41 x3) x3 = x41 x3False)False)((x2 x3 (x41 x3) = x41 x3False)False)((x2 x3 x3 = x3False)False)((x40 (x41 x3) (x41 x3) = x7False)False)((x40 (x41 x3) x7 = x41 x3False)False)((x40 x3 x3 = x7False)False)((x40 x3 x7 = x3False)False)((x40 x7 (x41 x3) = x3False)False)((x40 x7 x3 = x41 x3False)False)((x40 x7 x7 = x7False)False)(∀ x48 . (x43 x48 x48False)False)(∀ x48 x49 x50 . (x47 x50False)(x47 x48False)x44 x48 (x45 x50)x44 x49 x48(x38 x49 x50 x48False)False)(∀ x48 x49 x50 . (x47 x50False)(x47 x48False)x44 x48 (x45 x50)x38 x49 x50 x48(x44 x49 x48False)False)((x5 = x4False)False)((x37 x36False)False)(x47 x36False)((x35 x34False)False)((x47 x34False)False)((x33 x32False)False)((x35 x32False)False)((x1 x32False)False)((x47 x32False)False)((x37 x31False)False)((x8 x9False)False)((x35 x9False)False)((x33 x10False)False)((x8 x10False)False)((x35 x10False)False)((x1 x10False)False)((x6 x11False)False)((x35 x11False)False)((x33 x12False)False)((x6 x12False)False)((x35 x12False)False)((x1 x12False)False)((x1 x13False)False)(x47 x13False)(x47 x14False)((x30 x29False)False)((x15 x29False)False)((x28 x29False)False)(x47 x29False)((x35 x27False)False)((x33 x16False)False)((x1 x26False)False)((x47 x17False)False)((x30 x25False)False)(∀ x48 x49 . x1 x49x1 x48(x42 x49 (x2 x3 x48) = x2 x49 x48False)False)(∀ x48 . x1 x48(x41 (x41 x48) = x48False)False)(∀ x48 x49 . (x47 x49False)x1 x49(x47 x48False)x1 x48x47 (x2 x49 x48)False)(∀ x48 x49 . x33 x49x33 x48(x33 (x2 x49 x48)False)False)(∀ x48 x49 . (x47 x49False)x1 x49(x47 x48False)x1 x48x47 (x42 x49 x48)False)(∀ x48 x49 . x33 x49x33 x48(x33 (x40 x49 x48)False)False)(∀ x48 x49 . x33 x49x33 x48(x33 (x42 x49 x48)False)False)(∀ x48 . (x47 x48False)x1 x48(x1 (x41 x48)False)False)(∀ x48 . (x47 x48False)x1 x48x47 (x41 x48)False)((x30 x4False)False)(x47 x4False)(∀ x48 x49 . x1 x49x1 x48(x1 (x2 x49 x48)False)False)(∀ x48 x49 . x1 x49x1 x48(x1 (x40 x49 x48)False)False)(∀ x48 . x33 x48(x33 (x41 x48)False)False)(∀ x48 . x33 x48(x1 (x41 x48)False)False)(∀ x48 x49 . x1 x49x1 x48(x1 (x42 x49 x48)False)False)(∀ x48 x49 . (x6 x49False)x33 x49(x6 x48False)x33 x48x8 (x2 x49 x48)False)(∀ x48 x49 . (x8 x49False)x33 x49(x8 x48False)x33 x48x8 (x2 x49 x48)False)(∀ x48 x49 . (x8 x49False)x33 x49(x6 x48False)x33 x48x6 (x2 x48 x49)False)(∀ x48 x49 . (x8 x49False)x33 x49(x6 x48False)x33 x48x6 (x2 x49 x48)False)(∀ x48 x49 . (x8 x49False)x33 x49(x8 x48False)x33 x48x8 (x42 x49 x48)False)(∀ x48 x49 . (x6 x49False)x33 x49(x6 x48False)x33 x48x8 (x42 x49 x48)False)(∀ x48 x49 . (x6 x49False)x33 x49(x8 x48False)x33 x48x6 (x42 x48 x49)False)(∀ x48 x49 . (x6 x49False)x33 x49(x8 x48False)x33 x48x6 (x42 x49 x48)False)(∀ x48 x49 . x8 x49x33 x49(x8 x48False)x33 x48(x6 (x40 x48 x49)False)False)(∀ x48 x49 . x8 x49x33 x49(x8 x48False)x33 x48(x8 (x40 x49 x48)False)False)(∀ x48 x49 . x6 x49x33 x49(x6 x48False)x33 x48(x8 (x40 x48 x49)False)False)((x47 x46False)False)(∀ x48 x49 . x6 x49x33 x49(x6 x48False)x33 x48(x6 (x40 x49 x48)False)False)(∀ x48 x49 . (x8 x49False)x33 x49(x6 x48False)x33 x48x6 (x40 x48 x49)False)(∀ x48 x49 . (x8 x49False)x33 x49(x6 x48False)x33 x48x8 (x40 x49 x48)False)(∀ x48 . (x8 x48False)x33 x48x6 (x41 x48)False)(∀ x48 . (x8 x48False)x33 x48(x1 (x41 x48)False)False)(∀ x48 . (x6 x48False)x33 x48x8 (x41 x48)False)(∀ x48 . (x6 x48False)x33 x48(x1 (x41 x48)False)False)(∀ x48 x49 . (x47 x49False)(x47 x48False)x44 x48 (x45 x49)(x38 (x24 x48 x49) x49 x48False)False)(∀ x48 . (x44 (x18 x48) x48False)False)(∀ x48 x49 x50 . (x47 x50False)(x47 x48False)x44 x48 (x45 x50)x38 x49 x50 x48(x44 x49 x50False)False)((x44 x5 (x45 x39)False)False)(∀ x48 . x1 x48(x1 (x41 x48)False)False)(∀ x48 x49 . x1 x49x1 x48(x42 x49 x48 = x42 x48 x49False)False)(∀ x48 . x47 x48(x23 x48False)False)(∀ x48 . x35 x48(x6 x48False)(x8 x48False)(x35 x48False)False)(∀ x48 . x35 x48(x6 x48False)(x8 x48False)(x47 x48False)False)(∀ x48 . x44 x48 x4(x37 x48False)False)(∀ x48 . x47 x48x35 x48x8 x48False)(∀ x48 . x47 x48x35 x48x6 x48False)(∀ x48 . x47 x48x35 x48(x35 x48False)False)(∀ x48 . x47 x48(x37 x48False)False)(∀ x48 . (x47 x48False)x35 x48(x6 x48False)(x8 x48False)False)(∀ x48 . (x47 x48False)x35 x48(x6 x48False)(x35 x48False)False)(∀ x48 . x37 x48(x30 x48False)False)(∀ x48 . x35 x48x8 x48x6 x48False)(∀ x48 . x35 x48x8 x48(x35 x48False)False)(∀ x48 . x35 x48x8 x48x47 x48False)(∀ x48 x49 . x30 x49x44 x48 x49(x30 x48False)False)(∀ x48 . (x47 x48False)x35 x48(x8 x48False)(x6 x48False)False)(∀ x48 . (x47 x48False)x35 x48(x8 x48False)(x35 x48False)False)(∀ x48 . x33 x48(x35 x48False)False)(∀ x48 . x47 x48(x22 x48False)False)(∀ x48 . x35 x48x6 x48x8 x48False)(∀ x48 . x35 x48x6 x48(x35 x48False)False)(∀ x48 . x35 x48x6 x48x47 x48False)(∀ x48 . x33 x48(x1 x48False)False)(∀ x48 . x47 x48(x30 x48False)False)(∀ x48 . x37 x48(x35 x48False)False)(∀ x48 . x37 x48(x33 x48False)False)(∀ x48 . x37 x48(x1 x48False)False)(∀ x48 . x28 x48x15 x48(x30 x48False)False)(∀ x48 . x44 x48 x39(x33 x48False)False)(∀ x48 . x44 x48 x39(x1 x48False)False)(∀ x48 . x30 x48(x15 x48False)False)(∀ x48 . x30 x48(x28 x48False)False)(∀ x48 x49 . x23 x49x44 x48 (x45 x49)(x23 x48False)False)(∀ x48 x49 . x0 x48 x49x0 x49 x48False)(x42 (x2 x19 x20) x21 = x42 (x42 (x2 x3 x20) x21) x19False)((x1 x21False)False)((x1 x20False)False)((x1 x19False)False)False (proof)

previous assets