Search for blocks/addresses/...
Proofgold Asset
asset id
a3d630ce069968b484e7e9bfdaf322d9db3a40a6655ea31cb8190f29e584b66a
asset hash
abcace923ff9c21b30e3fedb2b5cb438ad23a2559fb60ebba7129f2abdfd7ee2
bday / block
35122
tx
48ffc..
preasset
doc published by
PrPhD..
Definition
False
False
:=
∀ x0 : ο .
x0
Definition
not
not
:=
λ x0 : ο .
x0
⟶
False
Theorem
7caba..
:
∀ 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 x34 .
∀ x35 :
ι → ι
.
∀ x36 :
ι →
ι → ο
.
∀ x37 x38 :
ι → ι
.
∀ x39 :
ι →
ι → ο
.
∀ x40 :
ι →
ι → ι
.
∀ x41 :
ι → ι
.
∀ x42 :
ι → ο
.
∀ x43 .
∀ x44 :
ι → ο
.
∀ x45 :
ι →
ι →
ι →
ι → ο
.
∀ x46 .
∀ x47 :
ι → ο
.
(
∀ x48 x49 .
x47
x49
⟶
(
x49
=
x48
⟶
False
)
⟶
x47
x48
⟶
False
)
⟶
(
∀ x48 x49 .
x0
x48
x49
⟶
x47
x49
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
(
x48
=
x46
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x0
x48
x49
⟶
x2
x49
(
x1
x50
)
⟶
x47
x50
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x0
x49
x50
⟶
x2
x50
(
x1
x48
)
⟶
(
x2
x49
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x3
x49
x48
⟶
(
x2
x49
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x2
x49
(
x1
x48
)
⟶
(
x3
x49
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x2
x48
x49
⟶
(
x47
x49
⟶
False
)
⟶
(
x0
x48
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x0
x49
x48
⟶
(
x2
x49
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x4
x51
⟶
x9
x51
x48
x49
⟶
x2
x51
(
x1
(
x5
x48
x49
)
)
⟶
x4
x50
⟶
x9
x50
x48
x49
⟶
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
x6
x51
(
x7
x50
x51
x49
x48
)
=
x6
x50
(
x7
x50
x51
x49
x48
)
⟶
(
x8
x48
x49
x51
x50
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x4
x51
⟶
x9
x51
x48
x49
⟶
x2
x51
(
x1
(
x5
x48
x49
)
)
⟶
x4
x50
⟶
x9
x50
x48
x49
⟶
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
(
x0
(
x7
x50
x51
x49
x48
)
x48
⟶
False
)
⟶
(
x8
x48
x49
x51
x50
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x2
x51
(
x1
(
x5
x50
x49
)
)
⟶
x2
x48
(
x1
(
x5
x50
x49
)
)
⟶
x8
x50
x49
x51
x48
⟶
(
x8
x50
x49
x48
x51
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x4
x51
⟶
x9
x51
x48
x49
⟶
x2
x51
(
x1
(
x5
x48
x49
)
)
⟶
x4
x50
⟶
x9
x50
x48
x49
⟶
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
x45
x48
x49
x51
x50
⟶
(
x45
x48
x49
x50
x51
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x2
x51
(
x1
(
x5
x50
x49
)
)
⟶
x2
x48
(
x1
(
x5
x50
x49
)
)
⟶
(
x8
x50
x49
x51
x51
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x4
x51
⟶
x9
x51
x48
x49
⟶
x2
x51
(
x1
(
x5
x48
x49
)
)
⟶
x4
x50
⟶
x9
x50
x48
x49
⟶
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
(
x45
x48
x49
x51
x51
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x3
x48
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x2
x51
(
x1
(
x5
x50
x49
)
)
⟶
x2
x48
(
x1
(
x5
x50
x49
)
)
⟶
x51
=
x48
⟶
(
x8
x50
x49
x51
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x2
x51
(
x1
(
x5
x50
x49
)
)
⟶
x2
x48
(
x1
(
x5
x50
x49
)
)
⟶
x8
x50
x49
x51
x48
⟶
(
x51
=
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x4
x51
⟶
x9
x51
x48
x49
⟶
x2
x51
(
x1
(
x5
x48
x49
)
)
⟶
x4
x50
⟶
x9
x50
x48
x49
⟶
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
x51
=
x50
⟶
(
x45
x48
x49
x51
x50
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x4
x51
⟶
x9
x51
x48
x49
⟶
x2
x51
(
x1
(
x5
x48
x49
)
)
⟶
x4
x50
⟶
x9
x50
x48
x49
⟶
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
x45
x48
x49
x51
x50
⟶
(
x51
=
x50
⟶
False
)
⟶
False
)
⟶
(
(
x44
x43
⟶
False
)
⟶
False
)
⟶
(
x47
x43
⟶
False
)
⟶
(
∀ x48 .
(
x42
x48
⟶
False
)
⟶
x42
(
x41
x48
)
⟶
False
)
⟶
(
∀ x48 .
(
x42
x48
⟶
False
)
⟶
(
x2
(
x41
x48
)
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x4
(
x40
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x10
(
x40
x48
x49
)
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x39
(
x40
x49
x48
)
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x11
(
x40
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
(
x42
(
x38
x48
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
x47
(
x38
x48
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
(
x2
(
x38
x48
)
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
x12
x13
⟶
False
)
⟶
(
(
x4
x13
⟶
False
)
⟶
False
)
⟶
(
(
x11
x13
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
(
x36
(
x37
x48
)
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
(
x2
(
x37
x48
)
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x36
(
x35
x48
)
x48
⟶
False
)
⟶
(
∀ x48 .
(
x2
(
x35
x48
)
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
x47
x34
⟶
False
)
⟶
(
∀ x48 .
(
x47
(
x14
x48
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x2
(
x14
x48
)
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
(
x15
x16
⟶
False
)
⟶
False
)
⟶
(
(
x4
x16
⟶
False
)
⟶
False
)
⟶
(
(
x11
x16
⟶
False
)
⟶
False
)
⟶
(
(
x47
x33
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
x47
(
x17
x48
)
⟶
False
)
⟶
(
∀ x48 .
(
x47
x48
⟶
False
)
⟶
(
x2
(
x17
x48
)
(
x1
x48
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x10
(
x18
x48
x49
)
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x39
(
x18
x49
x48
)
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x11
(
x18
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x47
(
x18
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x2
(
x18
x48
x49
)
(
x1
(
x5
x49
x48
)
)
⟶
False
)
⟶
False
)
⟶
(
(
x4
x32
⟶
False
)
⟶
False
)
⟶
(
(
x11
x32
⟶
False
)
⟶
False
)
⟶
(
(
x47
x46
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
(
x1
x48
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x44
x50
⟶
x11
x48
⟶
x10
x48
x50
⟶
x4
x48
⟶
(
x4
(
x6
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x44
x50
⟶
x11
x48
⟶
x10
x48
x50
⟶
x4
x48
⟶
(
x11
(
x6
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x47
x49
⟶
False
)
⟶
(
x47
x48
⟶
False
)
⟶
x47
(
x5
x49
x48
)
⟶
False
)
⟶
(
∀ x48 .
(
x2
(
x19
x48
)
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
(
x31
x48
x49
x50
=
x28
(
x29
x48
x49
x50
)
(
x30
x48
x49
x50
)
⟶
False
)
⟶
(
x0
(
x31
x48
x49
x50
)
x48
⟶
False
)
⟶
(
x48
=
x5
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
(
x0
(
x30
x48
x49
x50
)
x49
⟶
False
)
⟶
(
x0
(
x31
x48
x49
x50
)
x48
⟶
False
)
⟶
(
x48
=
x5
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
(
x0
(
x29
x48
x49
x50
)
x50
⟶
False
)
⟶
(
x0
(
x31
x48
x49
x50
)
x48
⟶
False
)
⟶
(
x48
=
x5
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 x52 .
x0
(
x31
x52
x50
x51
)
x52
⟶
x0
x48
x51
⟶
x0
x49
x50
⟶
x31
x52
x50
x51
=
x28
x48
x49
⟶
(
x52
=
x5
x51
x50
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 x52 x53 .
x53
=
x5
x51
x52
⟶
x0
x48
x51
⟶
x0
x50
x52
⟶
x49
=
x28
x48
x50
⟶
(
x0
x49
x53
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x51
=
x5
x49
x50
⟶
x0
x48
x51
⟶
(
x48
=
x28
(
x21
x48
x51
x50
x49
)
(
x20
x48
x51
x50
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x51
=
x5
x49
x50
⟶
x0
x48
x51
⟶
(
x0
(
x20
x48
x51
x50
x49
)
x50
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 x51 .
x51
=
x5
x49
x50
⟶
x0
x48
x51
⟶
(
x0
(
x21
x48
x51
x50
x49
)
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x11
x50
⟶
x4
x50
⟶
(
x27
x50
x48
x49
=
x6
x50
(
x28
x48
x49
)
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x44
x49
⟶
x2
x48
(
x1
x49
)
⟶
(
x44
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x44
x49
⟶
x2
x48
x49
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x44
x49
⟶
x2
x48
x49
⟶
(
x11
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
(
x44
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x42
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x12
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x42
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x42
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x11
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x42
x49
⟶
x2
x48
(
x1
x49
)
⟶
(
x42
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x11
x48
⟶
x4
x48
⟶
(
x12
x48
⟶
False
)
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x11
x48
⟶
x4
x48
⟶
(
x12
x48
⟶
False
)
⟶
(
x11
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x11
x48
⟶
x4
x48
⟶
(
x12
x48
⟶
False
)
⟶
x42
x48
⟶
False
)
⟶
(
∀ x48 x49 .
x47
x49
⟶
x2
x48
(
x1
x49
)
⟶
x36
x48
x49
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x47
x50
⟶
x2
x48
(
x1
(
x5
x49
x50
)
)
⟶
(
x47
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x12
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x11
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x47
x49
⟶
False
)
⟶
x2
x48
(
x1
x49
)
⟶
x47
x48
⟶
(
x36
x48
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x47
x50
⟶
x2
x48
(
x1
(
x5
x50
x49
)
)
⟶
(
x47
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x11
x49
⟶
x4
x49
⟶
x2
x48
(
x1
x49
)
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
(
x47
x49
⟶
False
)
⟶
x2
x48
(
x1
x49
)
⟶
(
x36
x48
x49
⟶
False
)
⟶
x47
x48
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
(
x10
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x2
x50
(
x1
(
x5
x49
x48
)
)
⟶
(
x39
x50
x49
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x15
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
x11
x48
⟶
x4
x48
⟶
(
x11
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x47
x49
⟶
x2
x48
(
x1
x49
)
⟶
(
x47
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 x50 .
x2
x50
(
x1
(
x5
x48
x49
)
)
⟶
(
x11
x50
⟶
False
)
⟶
False
)
⟶
(
∀ x48 .
x47
x48
⟶
(
x4
x48
⟶
False
)
⟶
False
)
⟶
(
∀ x48 x49 .
x0
x48
x49
⟶
x0
x49
x48
⟶
False
)
⟶
(
x45
(
x5
x22
x23
)
x26
x25
x24
⟶
False
)
⟶
(
∀ x48 x49 .
x0
x49
x22
⟶
x0
x48
x23
⟶
(
x27
x25
x49
x48
=
x27
x24
x49
x48
⟶
False
)
⟶
False
)
⟶
(
(
x2
x24
(
x1
(
x5
(
x5
x22
x23
)
x26
)
)
⟶
False
)
⟶
False
)
⟶
(
(
x9
x24
(
x5
x22
x23
)
x26
⟶
False
)
⟶
False
)
⟶
(
(
x4
x24
⟶
False
)
⟶
False
)
⟶
(
(
x2
x25
(
x1
(
x5
(
x5
x22
x23
)
x26
)
)
⟶
False
)
⟶
False
)
⟶
(
(
x9
x25
(
x5
x22
x23
)
x26
⟶
False
)
⟶
False
)
⟶
(
(
x4
x25
⟶
False
)
⟶
False
)
⟶
False
(proof)