Search for blocks/addresses/...
Proofgold Asset
asset id
c951c4c04fa2f0507cdc7df9d0fa8ba8b5fb8eaf44de04f20333c25707cf5876
asset hash
02cf3e9dc74161fdd82cb4ec66c8cfbe214c6f1003bfd349f63714a51872dea5
bday / block
316
tx
018c5..
preasset
doc published by
Pr8qe..
Theorem
8b648..
:
∀ x0 x1 x2 :
ι →
ι → ο
.
∀ x3 x4 x5 x6 x7 .
∀ x8 x9 :
ι → ι
.
∀ x10 x11 x12 :
ι →
ι → ι
.
∀ x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 :
ι → ο
.
x0
x3
x4
⟶
x0
x3
x5
⟶
(
∀ x24 x25 .
x1
x25
x24
⟶
x0
x25
(
x8
x24
)
)
⟶
(
∀ x24 .
x1
x24
x24
)
⟶
(
∀ x24 x25 x26 .
x1
(
x10
(
x10
x24
x25
)
x26
)
(
x10
x24
(
x10
x25
x26
)
)
)
⟶
(
∀ x24 x25 .
x2
(
x12
x24
x25
)
(
x11
x24
x25
)
)
⟶
(
∀ x24 x25 .
not
(
x0
x25
(
x9
x24
)
)
⟶
not
(
x25
=
x24
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x16
x24
⟶
x15
(
x12
x24
(
x9
x25
)
)
)
⟶
(
∀ x24 x25 .
x0
x25
x24
⟶
x15
(
x12
x24
(
x9
x25
)
)
⟶
x16
x24
)
⟶
(
∀ x24 x25 .
x2
x24
x25
⟶
x19
x24
⟶
x19
x25
⟶
x21
(
x10
x24
x25
)
)
⟶
(
∀ x24 x25 .
x22
x24
⟶
x19
(
x11
x24
x25
)
⟶
x20
(
x12
x24
x25
)
)
⟶
not
(
x1
x6
x5
)
⟶
not
(
x5
=
x6
)
⟶
x0
x4
(
x9
x4
)
⟶
x0
(
x9
x4
)
(
x12
(
x8
x5
)
x5
)
⟶
x1
x4
(
x12
x6
(
x9
x4
)
)
⟶
x0
x5
(
x12
(
x8
x5
)
x5
)
⟶
not
(
x1
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
not
(
x3
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x1
(
x9
(
x9
x4
)
)
(
x12
(
x8
x5
)
(
x9
x5
)
)
⟶
not
(
x5
=
x8
(
x9
x4
)
)
⟶
(
∀ x24 .
x1
x24
(
x8
(
x9
x4
)
)
⟶
x0
(
x9
x4
)
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x8
(
x9
x4
)
)
)
⟶
not
(
x5
=
x8
x5
)
⟶
not
(
x5
=
x9
x5
)
⟶
not
(
x6
=
x8
x5
)
⟶
x0
x3
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
⟶
not
(
x0
x6
(
x8
(
x9
x5
)
)
)
⟶
x0
x5
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
x0
(
x9
x5
)
(
x10
x6
(
x9
(
x9
x5
)
)
)
⟶
not
(
x0
x4
(
x9
x6
)
)
⟶
x0
x6
(
x10
x4
(
x9
x6
)
)
⟶
x0
x5
(
x10
(
x9
(
x9
x4
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
⟶
not
(
x0
(
x9
x5
)
(
x9
(
x8
x5
)
)
)
⟶
x0
x4
(
x10
(
x9
x4
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x0
x4
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
⟶
x2
x5
(
x10
(
x9
x6
)
(
x9
(
x8
x5
)
)
)
⟶
x0
x6
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
(
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
x4
)
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x9
x5
)
)
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
x4
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
(
x8
(
x9
x4
)
)
)
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x9
x5
)
)
⟶
or
(
or
(
x24
=
x3
)
(
x24
=
x4
)
)
(
x24
=
x6
)
)
⟶
not
(
x1
(
x10
x6
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
x6
)
⟶
x1
x7
(
x10
(
x9
(
x8
(
x9
x4
)
)
)
x7
)
⟶
x1
x7
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
⟶
not
(
x1
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
x7
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
not
(
x24
=
x3
)
⟶
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x12
x6
(
x9
x3
)
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
not
(
x24
=
x5
)
⟶
x0
x24
x5
)
⟶
x1
(
x12
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
x4
)
)
(
x12
(
x8
x5
)
x5
)
⟶
x12
(
x8
x5
)
(
x9
x3
)
=
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
⟶
x1
(
x12
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
(
x9
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
⟶
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x9
x4
)
)
=
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x4
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
⟶
x1
(
x8
x5
)
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x9
(
x9
x4
)
)
)
)
⟶
x1
(
x12
(
x12
x7
(
x9
x5
)
)
(
x9
x4
)
)
(
x10
x4
(
x9
x6
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
x5
)
⟶
not
(
x24
=
x5
)
⟶
x0
x24
(
x9
x6
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
x7
(
x8
(
x9
x5
)
)
)
⟶
not
(
x24
=
x4
)
⟶
x0
x24
(
x12
x7
x5
)
)
⟶
x1
(
x12
x6
(
x9
x4
)
)
(
x10
(
x9
(
x9
x4
)
)
x7
)
⟶
(
∀ x24 .
x0
x24
x6
⟶
x0
x24
(
x8
(
x12
x6
(
x9
x4
)
)
)
⟶
x0
x24
x5
)
⟶
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
=
x8
x5
⟶
x11
(
x10
x7
(
x9
(
x12
(
x8
x5
)
x5
)
)
)
(
x10
(
x9
(
x9
x4
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
=
x7
⟶
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x12
x7
(
x9
x4
)
)
=
x12
x6
(
x9
x4
)
⟶
not
(
x15
(
x12
(
x8
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
(
x9
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
)
)
)
⟶
not
(
x16
(
x10
(
x12
(
x8
x5
)
(
x9
x5
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
)
⟶
(
∀ x24 .
x16
(
x12
(
x10
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
(
x8
(
x9
(
x9
x4
)
)
)
)
(
x9
x24
)
)
⟶
not
(
x24
=
x9
(
x9
x4
)
)
)
⟶
x14
(
x12
(
x8
(
x8
(
x9
x4
)
)
)
(
x9
(
x8
(
x9
x4
)
)
)
)
⟶
x20
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x20
(
x11
(
x10
(
x8
x5
)
(
x9
(
x9
x5
)
)
)
(
x10
(
x10
(
x9
x5
)
(
x8
(
x9
x5
)
)
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
)
⟶
x1
(
x12
(
x11
(
x10
x6
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
(
x8
(
x12
x6
(
x9
x4
)
)
)
)
(
x9
x3
)
)
(
x10
(
x9
x4
)
(
x9
(
x12
x6
(
x9
x4
)
)
)
)
⟶
x21
(
x10
(
x12
(
x8
x5
)
(
x9
x4
)
)
(
x9
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
)
)
⟶
x20
(
x12
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
(
x10
x5
(
x9
(
x8
x5
)
)
)
)
(
x9
x3
)
)
⟶
x22
(
x10
(
x9
(
x9
(
x9
x4
)
)
)
x7
)
⟶
x1
(
x12
(
x11
(
x10
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
x6
)
)
)
(
x10
(
x9
(
x9
x5
)
)
x7
)
)
(
x9
x3
)
)
(
x12
(
x10
(
x9
(
x9
x5
)
)
x7
)
(
x12
(
x8
x5
)
(
x9
x4
)
)
)
⟶
(
∀ x24 .
x0
x24
(
x12
(
x8
x5
)
(
x8
(
x9
x5
)
)
)
⟶
x0
x24
(
x10
(
x9
(
x9
x5
)
)
(
x10
x7
(
x9
(
x8
x5
)
)
)
)
⟶
not
(
x0
x24
(
x9
x5
)
)
⟶
x0
x24
(
x10
(
x9
x4
)
(
x10
(
x8
(
x9
x5
)
)
(
x9
(
x8
x5
)
)
)
)
)
⟶
∀ x24 .
x1
x24
(
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
⟶
x0
(
x9
x4
)
x24
⟶
x0
x4
x24
⟶
or
(
or
(
or
(
x24
=
x3
)
(
x24
=
x9
x4
)
)
(
x24
=
x9
(
x9
x4
)
)
)
(
x24
=
x10
(
x9
x4
)
(
x9
(
x9
x4
)
)
)
(proof)