Search for blocks/addresses/...

Proofgold Address

address
PUYsehh86NpZM1ye1Yi42Lpt8TAk5tsqYNq
total
0
mg
-
conjpub
-
current assets
a2de3../c9e68.. bday: 20383 doc published by PrCnV..
Known andEandE : ∀ x0 x1 : ο . and x0 x1∀ x2 : ο . (x0x1x2)x2
Known FalseEFalseE : False∀ x0 : ο . x0
Known 218d1..atleast3_E : ∀ x0 . atleast3 x0∀ x1 : ο . (∀ x2 . and (Subq x2 x0) (and (not (Subq x0 x2)) (atleast2 x2))x1)x1
Known notEnotE : ∀ x0 : ο . not x0x0False
Known 39854..andEL : ∀ x0 x1 : ο . and x0 x1x0
Known b41a2..Subq_Empty : ∀ x0 . Subq 0 x0
Known 151e5..exactly3_E : ∀ x0 . exactly3 x0and (atleast3 x0) (not (atleast4 x0))
Theorem 21033.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 : ο . (∀ x3 . (∀ x4 . (∃ x5 . and (exactly3 0) (not (x0 x4)))∀ x5 : ο . (∀ x6 . and (and (x0 0) (x0 x4)) (reflexive_i (λ x7 x8 . x0 x7)and (x0 x3) (and (x0 (x1 x4)) (not (atleast6 x6))))x5)x5)x2)x2 (proof)
Known 8106d..notI : ∀ x0 : ο . (x0False)not x0
Known 1358f..nat_TransSet : ∀ x0 . nat_p x0TransSet x0
Known 08405..nat_0 : nat_p 0
Known b4782..contra : ∀ x0 : ο . (not x0False)x0
Known b0dce..SubqI : ∀ x0 x1 . (∀ x2 . In x2 x0In x2 x1)Subq x0 x1
Theorem 5fbd2.. : ∀ x0 : ι → ο . ∀ x1 : ι → ι . ∀ x2 . (∀ x3 . In x3 x2∀ x4 . Subq x4 x2and (not (TransSet x4)) (and (and (atleast6 x3) (x0 (x1 x4))) (nat_p (SetAdjoin x2 (binrep (binrep (Power (Power (Power (Power 0)))) (Power 0)) 0)))))not (exactly3 x2) (proof)

previous assets