Search for blocks/addresses/...

Proofgold Address

address
PUf1yE6ptvPkVz6Mrdv5i5Vjxir65GVZbhQ
total
0
mg
-
conjpub
-
current assets
98c83../a716e.. bday: 35140 doc published by PrPhD..
Definition FalseFalse := ∀ x0 : ο . x0
Definition notnot := λ x0 : ο . x0False
Theorem 745b7.. : ∀ 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 . x50 x52(x52 = x51False)x50 x51False)(∀ x51 x52 . x0 x51 x52x50 x52False)(∀ x51 . x50 x51(x51 = x49False)False)(∀ x51 x52 x53 . x0 x51 x52x2 x52 (x1 x53)x50 x53False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52(x46 x53 x51False)(x46 x52 x53False)(x0 x53 (x47 x51 x52)False)False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52x0 x53 (x47 x51 x52)x46 x52 x53False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52x0 x53 (x47 x51 x52)x46 x53 x51False)(∀ x51 x52 x53 . x0 x52 x53x2 x53 (x1 x51)(x2 x52 x51False)False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52x46 x51 x53(x46 x52 x53False)(x0 x53 (x45 x51 x52)False)False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52x0 x53 (x45 x51 x52)x46 x52 x53False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52x0 x53 (x45 x51 x52)(x46 x51 x53False)False)(∀ x51 x52 . x3 x52 x51(x2 x52 (x1 x51)False)False)(∀ x51 x52 . x2 x52 (x1 x51)(x3 x52 x51False)False)(∀ x51 x52 x53 . x48 x53x48 x51x48 x52x46 x53 x51x46 x51 x52(x46 x53 x52False)False)(∀ x51 x52 x53 . x0 x52 x53x0 x51 x53x0 x51 (x44 x53 x52)False)(∀ x51 x52 . x0 x52 x51(x0 (x44 x51 x52) x51False)False)(∀ x51 x52 . x2 x51 x52(x50 x52False)(x0 x51 x52False)False)(∀ x51 x52 . x48 x52x48 x51(x46 x51 x52False)x46 x51 (x4 x51 x52)False)(∀ x51 x52 . x48 x52x48 x51(x46 x51 x52False)x46 (x4 x51 x52) x52False)(∀ x51 x52 . x48 x52x48 x51(x46 x51 x52False)(x48 (x4 x51 x52)False)False)(∀ x51 x52 . x0 x52 x51(x2 x52 x51False)False)(∀ x51 x52 . x48 x52x48 x51(x46 x52 x52False)False)(∀ x51 . (x3 x51 x51False)False)((x48 x5False)False)((x50 x5False)False)((x6 x7False)False)((x48 x7False)False)((x8 x7False)False)((x50 x7False)False)((x9 x10False)False)((x48 x10False)False)((x6 x11False)False)((x9 x11False)False)((x48 x11False)False)((x8 x11False)False)((x12 x13False)False)((x43 x13False)False)(x50 x13False)((x42 x41False)False)((x48 x41False)False)((x6 x40False)False)((x42 x40False)False)((x48 x40False)False)((x8 x40False)False)(x50 x39False)((x43 x14False)False)(x50 x14False)((x48 x15False)False)((x6 x38False)False)((x50 x16False)False)((x43 x37False)False)(x50 x37False)(∀ x51 x52 x53 x54 . x48 x54x48 x51x2 x53 x36x52 = x53(x46 x53 x54False)(x46 x51 x53False)(x0 x52 (x35 x54 x51)False)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x35 x53 x51)x46 x51 (x17 x51 x53 x52)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x35 x53 x51)x46 (x17 x51 x53 x52) x53False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x35 x53 x51)(x52 = x17 x51 x53 x52False)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x35 x53 x51)(x2 (x17 x51 x53 x52) x36False)False)(∀ x51 x52 x53 x54 . x48 x54x48 x51x2 x53 x36x52 = x53x46 x54 x53(x46 x51 x53False)(x0 x52 (x18 x54 x51)False)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x18 x53 x51)x46 x51 (x34 x51 x53 x52)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x18 x53 x51)(x46 x53 (x34 x51 x53 x52)False)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x18 x53 x51)(x52 = x34 x51 x53 x52False)False)(∀ x51 x52 x53 . x48 x53x48 x51x0 x52 (x18 x53 x51)(x2 (x34 x51 x53 x52) x36False)False)(∀ x51 . x48 x51(x50 (x47 x51 x51)False)False)(∀ x51 . x48 x51(x50 (x45 x51 x51)False)False)(x50 x36False)(∀ x51 x52 . x48 x52x48 x51(x19 (x47 x52 x51)False)False)(∀ x51 x52 . x48 x52x48 x51(x19 (x45 x52 x51)False)False)((x19 x36False)False)((x50 x49False)False)(∀ x51 . (x2 (x20 x51) x51False)False)((x50 x33False)False)(∀ x51 x52 . x19 x52x0 (x21 x51 x52) x51(x3 x52 x51False)False)(∀ x51 x52 . x19 x52(x0 (x21 x51 x52) x52False)(x3 x52 x51False)False)(∀ x51 x52 . x19 x52(x48 (x21 x51 x52)False)(x3 x52 x51False)False)(∀ x51 x52 x53 . x19 x53x3 x53 x51x48 x52x0 x52 x53(x0 x52 x51False)False)(∀ x51 x52 . x48 x52x48 x51(x47 x52 x51 = x35 x52 x51False)False)(∀ x51 x52 . x48 x52x48 x51(x45 x52 x51 = x18 x52 x51False)False)((x49 = x33False)False)(∀ x51 x52 . x48 x52x48 x51(x46 x52 x51False)(x46 x51 x52False)False)(∀ x51 . x48 x51(x42 x51False)(x9 x51False)(x48 x51False)False)(∀ x51 . x48 x51(x42 x51False)(x9 x51False)(x50 x51False)False)(∀ x51 . x50 x51x48 x51x9 x51False)(∀ x51 . x50 x51x48 x51x42 x51False)(∀ x51 . x50 x51x48 x51(x48 x51False)False)(∀ x51 . x2 x51 (x1 x36)(x19 x51False)False)(∀ x51 . (x50 x51False)x48 x51(x42 x51False)(x9 x51False)False)(∀ x51 . (x50 x51False)x48 x51(x42 x51False)(x48 x51False)False)(∀ x51 . x48 x51x9 x51x42 x51False)(∀ x51 . x48 x51x9 x51(x48 x51False)False)(∀ x51 . x48 x51x9 x51x50 x51False)(∀ x51 . x31 x51(x32 x51False)False)(∀ x51 . (x50 x51False)x48 x51(x9 x51False)(x42 x51False)False)(∀ x51 . (x50 x51False)x48 x51(x9 x51False)(x48 x51False)False)(∀ x51 . x6 x51(x48 x51False)False)(∀ x51 . x31 x51(x19 x51False)False)(∀ x51 . x48 x51x42 x51x9 x51False)(∀ x51 . x48 x51x42 x51(x48 x51False)False)(∀ x51 . x48 x51x42 x51x50 x51False)(∀ x51 . x6 x51(x8 x51False)False)(∀ x51 . x22 x51(x31 x51False)False)(∀ x51 . x30 x51(x48 x51False)False)(∀ x51 . x30 x51(x6 x51False)False)(∀ x51 . x29 x51(x22 x51False)False)(∀ x51 . x50 x51(x12 x51False)False)(∀ x51 x52 . x43 x52x2 x51 (x1 x52)(x43 x51False)False)(∀ x51 x52 . x29 x52x2 x51 (x1 x52)(x29 x51False)False)(∀ x51 x52 . x22 x52x2 x51 (x1 x52)(x22 x51False)False)(∀ x51 x52 . x31 x52x2 x51 (x1 x52)(x31 x51False)False)(∀ x51 x52 . x19 x52x2 x51 (x1 x52)(x19 x51False)False)(∀ x51 . x2 x51 x36(x48 x51False)False)(∀ x51 . x43 x51(x29 x51False)False)(∀ x51 x52 . x32 x52x2 x51 (x1 x52)(x32 x51False)False)(∀ x51 . x50 x51(x43 x51False)False)(∀ x51 x52 . x43 x52x2 x51 x52(x30 x51False)False)(∀ x51 x52 . x29 x52x2 x51 x52(x28 x51False)False)(∀ x51 x52 . x22 x52x2 x51 x52(x23 x51False)False)(∀ x51 x52 . x31 x52x2 x51 x52(x6 x51False)False)(∀ x51 x52 . x19 x52x2 x51 x52(x48 x51False)False)(∀ x51 x52 . x32 x52x2 x51 x52(x8 x51False)False)(∀ x51 x52 . x0 x51 x52x0 x52 x51False)((x3 (x45 x27 x26) (x47 x25 x24)False)False)(x46 x26 x27False)(x46 x26 x24False)((x48 x25False)False)((x48 x27False)False)((x48 x26False)False)((x48 x24False)False)False (proof)

previous assets