Search for blocks/addresses/...
Proofgold Asset
asset id
7b219995b90858fa1682e4136359fd1317bb82586cd8d403a41229e390d6eb22
asset hash
c7a9efaabee90f97663e2d5df5eedec4ec052cf09f70aec669cd8a4a83e1cd9d
bday / block
20308
tx
35fdb..
preasset
doc published by
PrCnV..
Theorem
8ddd3..
:
∀ x0 :
ι →
ι → ο
.
∀ x1 :
ι →
ι → ι
.
∀ x2 x3 :
ι → ο
.
∀ x4 :
ι → ι
.
∀ x5 x6 x7 .
and
(
not
(
x0
x7
(
x1
x7
(
x1
(
x1
(
x1
(
x1
(
x1
(
x1
(
x1
x6
x6
)
x7
)
x6
)
(
x1
(
x4
(
x1
(
x4
(
x1
(
x1
x6
(
x1
(
x4
x6
)
x5
)
)
(
x1
(
x1
(
x1
(
x4
(
x4
(
x4
(
x4
(
x1
x5
(
x1
(
x4
(
x1
x6
(
x1
x6
(
x4
x6
)
)
)
)
x6
)
)
)
)
)
)
x7
)
x7
)
(
x1
x6
(
x4
x6
)
)
)
)
)
x5
)
)
(
x1
(
x4
(
x4
(
x4
x7
)
)
)
x6
)
)
)
x5
)
x6
)
x6
)
)
)
)
(
x6
=
x6
)
⟶
∀ x8 : ο .
(
∀ x9 .
(
∀ x10 .
x9
=
x4
x5
)
⟶
x8
)
⟶
x8
(proof)
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Known
notE
notE
:
∀ x0 : ο .
not
x0
⟶
x0
⟶
False
Known
e3ec9..
neq_0_1
:
not
(
0
=
1
)
Theorem
88343..
:
∀ x0 :
ι →
ι → ο
.
∀ x1 :
ι →
ι → ι
.
∀ x2 x3 :
ι → ο
.
∀ x4 :
ι → ι
.
∀ x5 x6 x7 x8 .
(
∀ x9 x10 .
(
∃ x11 .
∀ x13 .
(
∀ x14 .
x8
=
x5
)
⟶
∀ x14 : ο .
(
∀ x15 .
(
not
(
x3
x10
)
⟶
not
(
x3
x15
)
)
⟶
x14
)
⟶
x14
)
⟶
x7
=
x9
)
⟶
x1
(
x4
(
x4
(
x4
x6
)
)
)
(
x1
(
x1
x8
(
x4
x5
)
)
x6
)
=
x4
x8
(proof)