Search for blocks/addresses/...
Proofgold Asset
asset id
8bcc660a33414308e451de433a56a3778c3e27762fc118e871ac69e1293efdec
asset hash
a082e1a7bde092324acd602b9e5947041a8837660ce5647482a83521495afdf2
bday / block
35159
tx
d7645..
preasset
doc published by
PrPhD..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Theorem
7fddd..
:
∀ 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 .
(
x29
x33
⟶
False
)
⟶
x22
x33
⟶
x28
x33
⟶
x23
x33
⟶
x27
x33
⟶
x25
x30
(
x24
x33
)
⟶
x25
x32
(
x24
x33
)
⟶
x25
x31
(
x24
x33
)
⟶
(
x26
x33
(
x26
x33
x31
x32
)
(
x26
x33
(
x26
x33
x30
x30
)
x32
)
=
x26
x33
(
x26
x33
x32
(
x26
x33
(
x26
x33
x31
x31
)
x30
)
)
(
x26
x33
x32
(
x26
x33
(
x26
x33
x31
x31
)
x30
)
)
⟶
False
)
⟶
False
)
⟶
(
(
x2
x1
x0
⟶
False
)
⟶
False
)
⟶
(
(
x27
x1
⟶
False
)
⟶
False
)
⟶
(
(
x3
x4
⟶
False
)
⟶
False
)
⟶
(
(
x23
x4
⟶
False
)
⟶
False
)
⟶
(
(
x28
x4
⟶
False
)
⟶
False
)
⟶
(
(
x22
x4
⟶
False
)
⟶
False
)
⟶
(
x29
x4
⟶
False
)
⟶
(
(
x27
x4
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x5
x30
⟶
False
)
⟶
x7
x30
⟶
x6
(
x24
x30
)
⟶
False
)
⟶
(
∀ x30 .
x5
x30
⟶
x7
x30
⟶
(
x6
(
x24
x30
)
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x8
x30
⟶
x7
x30
⟶
(
x9
(
x24
x30
)
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x8
x30
⟶
False
)
⟶
x7
x30
⟶
x9
(
x24
x30
)
⟶
False
)
⟶
(
∀ x30 .
(
x29
x30
⟶
False
)
⟶
x7
x30
⟶
x10
(
x24
x30
)
⟶
False
)
⟶
(
∀ x30 .
x29
x30
⟶
x7
x30
⟶
(
x10
(
x24
x30
)
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x25
(
x11
x30
)
x30
⟶
False
)
⟶
False
)
⟶
(
(
x7
x21
⟶
False
)
⟶
False
)
⟶
(
(
x27
x12
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
(
x7
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 x31 x32 .
(
x29
x32
⟶
False
)
⟶
x27
x32
⟶
x25
x31
(
x24
x32
)
⟶
x25
x30
(
x24
x32
)
⟶
(
x25
(
x26
x32
x31
x30
)
(
x24
x32
)
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x29
x30
⟶
False
)
⟶
x27
x30
⟶
x26
x30
(
x26
x30
(
x19
x30
)
(
x26
x30
(
x18
x30
)
(
x20
x30
)
)
)
(
x26
x30
(
x19
x30
)
(
x26
x30
(
x18
x30
)
(
x20
x30
)
)
)
=
x26
x30
(
x26
x30
(
x26
x30
(
x18
x30
)
(
x18
x30
)
)
(
x19
x30
)
)
(
x26
x30
(
x26
x30
(
x20
x30
)
(
x20
x30
)
)
(
x19
x30
)
)
⟶
(
x23
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x29
x30
⟶
False
)
⟶
x27
x30
⟶
(
x25
(
x20
x30
)
(
x24
x30
)
⟶
False
)
⟶
(
x23
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x29
x30
⟶
False
)
⟶
x27
x30
⟶
(
x25
(
x18
x30
)
(
x24
x30
)
⟶
False
)
⟶
(
x23
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
(
x29
x30
⟶
False
)
⟶
x27
x30
⟶
(
x25
(
x19
x30
)
(
x24
x30
)
⟶
False
)
⟶
(
x23
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 x31 x32 x33 .
(
x29
x33
⟶
False
)
⟶
x27
x33
⟶
x23
x33
⟶
x25
x30
(
x24
x33
)
⟶
x25
x32
(
x24
x33
)
⟶
x25
x31
(
x24
x33
)
⟶
(
x26
x33
(
x26
x33
x30
(
x26
x33
x32
x31
)
)
(
x26
x33
x30
(
x26
x33
x32
x31
)
)
=
x26
x33
(
x26
x33
(
x26
x33
x32
x32
)
x30
)
(
x26
x33
(
x26
x33
x31
x31
)
x30
)
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x2
x30
x13
⟶
(
x29
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x29
x30
⟶
(
x2
x30
x13
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
(
x5
x30
⟶
False
)
⟶
x8
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x8
x30
⟶
(
x5
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
(
x5
x30
⟶
False
)
⟶
x5
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
(
x5
x30
⟶
False
)
⟶
x29
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x29
x30
⟶
(
x5
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x29
x30
⟶
(
x29
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
x2
x30
x0
⟶
(
x23
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
x2
x30
x0
⟶
(
x28
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
x2
x30
x0
⟶
(
x22
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
x2
x30
x0
⟶
(
x2
x30
x0
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
(
x8
x30
⟶
False
)
⟶
x29
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x29
x30
⟶
(
x8
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
(
x29
x30
⟶
False
)
⟶
x8
x30
⟶
(
x3
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x27
x30
⟶
(
x29
x30
⟶
False
)
⟶
x8
x30
⟶
x29
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
(
x8
x30
⟶
False
)
⟶
x29
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x2
x30
x0
⟶
(
x8
x30
⟶
False
)
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
x2
x30
x0
⟶
x29
x30
⟶
False
)
⟶
(
∀ x30 .
x7
x30
⟶
(
x29
x30
⟶
False
)
⟶
x8
x30
⟶
(
x2
x30
x0
⟶
False
)
⟶
False
)
⟶
(
x26
x17
(
x26
x17
(
x26
x17
x16
x16
)
(
x26
x17
(
x26
x17
x14
x14
)
x15
)
)
(
x26
x17
(
x26
x17
x15
(
x26
x17
(
x26
x17
x15
x15
)
x14
)
)
(
x26
x17
x15
(
x26
x17
(
x26
x17
x15
x15
)
x14
)
)
)
=
x26
x17
(
x26
x17
(
x26
x17
(
x26
x17
x14
x14
)
x15
)
(
x26
x17
x16
x15
)
)
(
x26
x17
(
x26
x17
(
x26
x17
x14
x14
)
x15
)
(
x26
x17
x16
x15
)
)
⟶
False
)
⟶
(
(
x25
x14
(
x24
x17
)
⟶
False
)
⟶
False
)
⟶
(
(
x25
x15
(
x24
x17
)
⟶
False
)
⟶
False
)
⟶
(
(
x25
x16
(
x24
x17
)
⟶
False
)
⟶
False
)
⟶
(
(
x27
x17
⟶
False
)
⟶
False
)
⟶
(
(
x23
x17
⟶
False
)
⟶
False
)
⟶
(
(
x28
x17
⟶
False
)
⟶
False
)
⟶
(
(
x22
x17
⟶
False
)
⟶
False
)
⟶
(
x29
x17
⟶
False
)
⟶
False
(proof)