Search for blocks/addresses/...

Proofgold Address

address
PUcyP63Xbytcbtp7pgqAMdVQxrpdtne2xXa
total
0
mg
-
conjpub
-
current assets
c1e27../a6adc.. bday: 36226 doc published by Pr4zB..
Param 94275.. : (ιιο) → ιιιιιιιιιιο
Param notnot : οο
Definition ce66c.. := λ x0 : ι → ι → ο . λ x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 . ∀ x12 : ο . (94275.. x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10(x1 = x11∀ x13 : ο . x13)(x2 = x11∀ x13 : ο . x13)(x3 = x11∀ x13 : ο . x13)(x4 = x11∀ x13 : ο . x13)(x5 = x11∀ x13 : ο . x13)(x6 = x11∀ x13 : ο . x13)(x7 = x11∀ x13 : ο . x13)(x8 = x11∀ x13 : ο . x13)(x9 = x11∀ x13 : ο . x13)(x10 = x11∀ x13 : ο . x13)not (x0 x1 x11)x0 x2 x11not (x0 x3 x11)not (x0 x4 x11)not (x0 x5 x11)not (x0 x6 x11)not (x0 x7 x11)x0 x8 x11not (x0 x9 x11)not (x0 x10 x11)x12)x12
Known 8e08c.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x094275.. x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x1194275.. x1 x7 x9 x6 x8 x4 x2 x5 x3 x11 x10
Theorem ec2a5.. : ∀ x0 . ∀ x1 : ι → ι → ο . (∀ x2 . x2x0∀ x3 . x3x0x1 x2 x3x1 x3 x2)∀ x2 . x2x0∀ x3 . x3x0∀ x4 . x4x0∀ x5 . x5x0∀ x6 . x6x0∀ x7 . x7x0∀ x8 . x8x0∀ x9 . x9x0∀ x10 . x10x0∀ x11 . x11x0∀ x12 . x12x0ce66c.. x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12ce66c.. x1 x7 x9 x6 x8 x4 x2 x5 x3 x11 x10 x12 (proof)

previous assets