Search for blocks/addresses/...
Proofgold Asset
asset id
ebaa85f4fca7ae6c9ac8cbf67f83152f8cea135986668f29c5c3366959866b3d
asset hash
9e99968ee31fd06727342024a1358a48031dddd5246bf00530046252bace6f1b
bday / block
21533
tx
f9088..
preasset
doc published by
Pr4zB..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Known
FalseE
FalseE
:
False
⟶
∀ x0 : ο .
x0
Theorem
7c344..
:
∀ x0 :
ι → ο
.
∀ x1 x2 x3 x4 x5 x6 .
(
∀ x7 :
ι → ο
.
x7
x1
⟶
x7
x2
⟶
x7
x3
⟶
x7
x4
⟶
x7
x5
⟶
x7
x6
⟶
∀ x8 .
x0
x8
⟶
x7
x8
)
⟶
x0
x1
⟶
x0
x2
⟶
x0
x3
⟶
x0
x4
⟶
x0
x5
⟶
x0
x6
⟶
∀ x7 :
ι →
ι →
ι →
ι → ο
.
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x2
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x3
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x4
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x1
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x3
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x4
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x2
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x4
x9
x3
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x3
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x3
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x5
x9
x4
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x4
)
)
⟶
(
∀ x8 .
x0
x8
⟶
∀ x9 .
x0
x9
⟶
not
(
x7
x8
x6
x9
x5
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x1
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x2
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x3
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x1
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x2
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x3
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x2
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x3
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x3
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x4
x8
x4
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x4
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x4
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x5
x8
x5
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x5
x8
)
)
⟶
(
∀ x8 .
x0
x8
⟶
not
(
x7
x6
x8
x6
x8
)
)
⟶
∀ x8 :
ι →
ι →
ι →
ι → ο
.
(
∀ x9 x10 x11 x12 .
x0
x9
⟶
x0
x10
⟶
x0
x11
⟶
x0
x12
⟶
x8
x9
x10
x11
x12
⟶
x8
x11
x12
x9
x10
)
⟶
(
∀ x9 x10 .
x0
x9
⟶
x0
x10
⟶
x8
x9
x10
x6
x6
)
⟶
(
∀ x9 .
x0
x9
⟶
x8
x5
x5
x6
x9
)
⟶
(
∀ x9 .
x0
x9
⟶
x8
x5
x6
x6
x9
)
⟶
x8
x1
x1
x1
x3
⟶
x8
x1
x1
x1
x5
⟶
x8
x1
x1
x2
x1
⟶
x8
x1
x1
x2
x2
⟶
x8
x1
x1
x2
x5
⟶
x8
x1
x1
x3
x3
⟶
x8
x1
x1
x3
x4
⟶
x8
x1
x1
x3
x5
⟶
x8
x1
x1
x4
x2
⟶
x8
x1
x1
x4
x3
⟶
x8
x1
x1
x4
x5
⟶
x8
x1
x1
x5
x3
⟶
x8
x1
x1
x5
x4
⟶
x8
x1
x1
x6
x1
⟶
x8
x1
x1
x6
x3
⟶
x8
x1
x1
x6
x4
⟶
x8
x1
x2
x1
x4
⟶
x8
x1
x2
x1
x6
⟶
x8
x1
x2
x2
x1
⟶
x8
x1
x2
x2
x2
⟶
x8
x1
x2
x2
x6
⟶
x8
x1
x2
x3
x3
⟶
x8
x1
x2
x3
x4
⟶
x8
x1
x2
x3
x6
⟶
x8
x1
x2
x4
x1
⟶
x8
x1
x2
x4
x4
⟶
x8
x1
x2
x4
x6
⟶
x8
x1
x2
x5
x3
⟶
x8
x1
x2
x5
x4
⟶
x8
x1
x2
x6
x2
⟶
x8
x1
x2
x6
x3
⟶
x8
x1
x2
x6
x4
⟶
x8
x1
x3
x1
x6
⟶
x8
x1
x3
x2
x3
⟶
x8
x1
x3
x2
x4
⟶
x8
x1
x3
x2
x5
⟶
x8
x1
x3
x3
x1
⟶
x8
x1
x3
x3
x2
⟶
x8
x1
x3
x3
x5
⟶
x8
x1
x3
x4
x1
⟶
x8
x1
x3
x4
x4
⟶
x8
x1
x3
x4
x6
⟶
x8
x1
x3
x5
x1
⟶
x8
x1
x3
x5
x2
⟶
x8
x1
x3
x6
x1
⟶
x8
x1
x3
x6
x2
⟶
x8
x1
x3
x6
x3
⟶
x8
x1
x4
x1
x5
⟶
x8
x1
x4
x2
x3
⟶
x8
x1
x4
x2
x4
⟶
x8
x1
x4
x2
x6
⟶
x8
x1
x4
x3
x1
⟶
x8
x1
x4
x3
x2
⟶
x8
x1
x4
x3
x6
⟶
x8
x1
x4
x4
x2
⟶
x8
x1
x4
x4
x3
⟶
x8
x1
x4
x4
x5
⟶
x8
x1
x4
x5
x1
⟶
x8
x1
x4
x5
x2
⟶
x8
x1
x4
x6
x1
⟶
x8
x1
x4
x6
x2
⟶
x8
x1
x4
x6
x4
⟶
x8
x1
x5
x2
x2
⟶
x8
x1
x5
x2
x3
⟶
x8
x1
x5
x3
x1
⟶
x8
x1
x5
x3
x4
⟶
x8
x1
x5
x3
x5
⟶
x8
x1
x5
x3
x6
⟶
x8
x1
x5
x4
x1
⟶
x8
x1
x5
x4
x4
⟶
x8
x1
x5
x4
x5
⟶
x8
x1
x5
x4
x6
⟶
x8
x1
x5
x5
x2
⟶
x8
x1
x5
x5
x3
⟶
x8
x1
x5
x6
x5
⟶
x8
x1
x6
x2
x1
⟶
x8
x1
x6
x2
x4
⟶
x8
x1
x6
x3
x2
⟶
x8
x1
x6
x3
x3
⟶
x8
x1
x6
x3
x5
⟶
x8
x1
x6
x3
x6
⟶
x8
x1
x6
x4
x2
⟶
x8
x1
x6
x4
x3
⟶
x8
x1
x6
x4
x5
⟶
x8
x1
x6
x4
x6
⟶
x8
x1
x6
x5
x1
⟶
x8
x1
x6
x5
x4
⟶
x8
x1
x6
x6
x5
⟶
x8
x2
x1
x2
x3
⟶
x8
x2
x1
x2
x6
⟶
x8
x2
x1
x3
x1
⟶
x8
x2
x1
x3
x5
⟶
x8
x2
x1
x4
x2
⟶
x8
x2
x1
x4
x3
⟶
x8
x2
x1
x4
x4
⟶
x8
x2
x1
x4
x5
⟶
x8
x2
x1
x5
x2
⟶
x8
x2
x1
x5
x3
⟶
x8
x2
x1
x5
x6
⟶
x8
x2
x1
x6
x2
⟶
x8
x2
x2
x2
x4
⟶
x8
x2
x2
x2
x5
⟶
x8
x2
x2
x3
x2
⟶
x8
x2
x2
x3
x6
⟶
x8
x2
x2
x4
x1
⟶
x8
x2
x2
x4
x3
⟶
x8
x2
x2
x4
x4
⟶
x8
x2
x2
x4
x6
⟶
x8
x2
x2
x5
x1
⟶
x8
x2
x2
x5
x4
⟶
x8
x2
x2
x5
x5
⟶
x8
x2
x2
x6
x1
⟶
x8
x2
x3
x2
x6
⟶
x8
x2
x3
x3
x3
⟶
x8
x2
x3
x3
x5
⟶
x8
x2
x3
x4
x1
⟶
x8
x2
x3
x4
x2
⟶
x8
x2
x3
x4
x4
⟶
x8
x2
x3
x4
x6
⟶
x8
x2
x3
x5
x1
⟶
x8
x2
x3
x5
x4
⟶
x8
x2
x3
x5
x6
⟶
x8
x2
x3
x6
x4
⟶
x8
x2
x4
x2
x5
⟶
x8
x2
x4
x3
x4
⟶
x8
x2
x4
x3
x6
⟶
x8
x2
x4
x4
x1
⟶
x8
x2
x4
x4
x2
⟶
x8
x2
x4
x4
x3
⟶
x8
x2
x4
x4
x5
⟶
x8
x2
x4
x5
x2
⟶
x8
x2
x4
x5
x3
⟶
x8
x2
x4
x5
x5
⟶
x8
x2
x4
x6
x3
⟶
x8
x2
x5
x2
x6
⟶
x8
x2
x5
x3
x2
⟶
x8
x2
x5
x3
x4
⟶
x8
x2
x5
x4
x5
⟶
x8
x2
x5
x4
x6
⟶
x8
x2
x5
x5
x6
⟶
x8
x2
x5
x6
x2
⟶
x8
x2
x5
x6
x4
⟶
x8
x2
x5
x6
x5
⟶
x8
x2
x6
x3
x1
⟶
x8
x2
x6
x3
x3
⟶
x8
x2
x6
x4
x5
⟶
x8
x2
x6
x4
x6
⟶
x8
x2
x6
x5
x5
⟶
x8
x2
x6
x6
x1
⟶
x8
x2
x6
x6
x3
⟶
x8
x2
x6
x6
x5
⟶
x8
x3
x1
x3
x2
⟶
x8
x3
x1
x3
x5
⟶
x8
x3
x1
x4
x2
⟶
x8
x3
x1
x4
x3
⟶
x8
x3
x1
x4
x6
⟶
x8
x3
x1
x5
x3
⟶
x8
x3
x1
x5
x4
⟶
x8
x3
x1
x6
x3
⟶
x8
x3
x1
x6
x5
⟶
x8
x3
x2
x3
x6
⟶
x8
x3
x2
x4
x1
⟶
x8
x3
x2
x4
x4
⟶
x8
x3
x2
x4
x5
⟶
x8
x3
x2
x5
x3
⟶
x8
x3
x2
x5
x4
⟶
x8
x3
x2
x6
x4
⟶
x8
x3
x2
x6
x5
⟶
x8
x3
x3
x3
x4
⟶
x8
x3
x3
x3
x5
⟶
x8
x3
x3
x4
x1
⟶
x8
x3
x3
x4
x4
⟶
x8
x3
x3
x4
x5
⟶
x8
x3
x3
x5
x1
⟶
x8
x3
x3
x5
x2
⟶
x8
x3
x3
x6
x1
⟶
x8
x3
x3
x6
x5
⟶
x8
x3
x4
x3
x6
⟶
x8
x3
x4
x4
x2
⟶
x8
x3
x4
x4
x3
⟶
x8
x3
x4
x4
x6
⟶
x8
x3
x4
x5
x1
⟶
x8
x3
x4
x5
x2
⟶
x8
x3
x4
x6
x2
⟶
x8
x3
x4
x6
x5
⟶
x8
x3
x5
x1
x6
⟶
x8
x3
x5
x3
x6
⟶
x8
x3
x5
x5
x2
⟶
x8
x3
x5
x5
x4
⟶
x8
x3
x6
x5
x1
⟶
x8
x3
x6
x5
x3
⟶