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