Search for blocks/addresses/...
Proofgold Asset
asset id
ae1212752815eb0969236f71ff1fd8718ad0d88d652dd8efd50d2734d8ac63b7
asset hash
f52b8551f8e830f13eb5be18f8b3d6656319a866383ce418d16e236006f477d7
bday / block
36397
tx
a0443..
preasset
doc published by
PrCmT..
Known
df_sub__df_neg__df_div__df_nn__df_2__df_3__df_4__df_5__df_6__df_7__df_8__df_9__df_10OLD__df_n0__df_xnn0__df_z__df_dec__df_uz
:
∀ x0 : ο .
(
wceq
cmin
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
caddc
)
(
cv
x1
)
)
(
λ x3 .
cc
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cneg
x1
)
(
co
cc0
x1
cmin
)
)
⟶
wceq
cdiv
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cdif
cc
(
csn
cc0
)
)
(
λ x1 x2 .
crio
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cv
x3
)
cmul
)
(
cv
x1
)
)
(
λ x3 .
cc
)
)
)
⟶
wceq
cn
(
cima
(
crdg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
(
cv
x1
)
c1
caddc
)
)
c1
)
com
)
⟶
wceq
c2
(
co
c1
c1
caddc
)
⟶
wceq
c3
(
co
c2
c1
caddc
)
⟶
wceq
c4
(
co
c3
c1
caddc
)
⟶
wceq
c5
(
co
c4
c1
caddc
)
⟶
wceq
c6
(
co
c5
c1
caddc
)
⟶
wceq
c7
(
co
c6
c1
caddc
)
⟶
wceq
c8
(
co
c7
c1
caddc
)
⟶
wceq
c9
(
co
c8
c1
caddc
)
⟶
wceq
c10
(
co
c9
c1
caddc
)
⟶
wceq
cn0
(
cun
cn
(
csn
cc0
)
)
⟶
wceq
cxnn0
(
cun
cn0
(
csn
cpnf
)
)
⟶
wceq
cz
(
crab
(
λ x1 .
w3o
(
wceq
(
cv
x1
)
cc0
)
(
wcel
(
cv
x1
)
cn
)
(
wcel
(
cneg
(
cv
x1
)
)
cn
)
)
(
λ x1 .
cr
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cdc
x1
x2
)
(
co
(
co
(
co
c9
c1
caddc
)
x1
cmul
)
x2
caddc
)
)
⟶
wceq
cuz
(
cmpt
(
λ x1 .
cz
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cv
x1
)
(
cv
x2
)
cle
)
(
λ x2 .
cz
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_sub
:
wceq
cmin
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
(
cv
x0
)
)
(
λ x2 .
cc
)
)
)
(proof)
Theorem
df_neg
:
∀ x0 :
ι → ο
.
wceq
(
cneg
x0
)
(
co
cc0
x0
cmin
)
(proof)
Theorem
df_div
:
wceq
cdiv
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cdif
cc
(
csn
cc0
)
)
(
λ x0 x1 .
crio
(
λ x2 .
wceq
(
co
(
cv
x1
)
(
cv
x2
)
cmul
)
(
cv
x0
)
)
(
λ x2 .
cc
)
)
)
(proof)
Theorem
df_nn
:
wceq
cn
(
cima
(
crdg
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
co
(
cv
x0
)
c1
caddc
)
)
c1
)
com
)
(proof)
Theorem
df_2
:
wceq
c2
(
co
c1
c1
caddc
)
(proof)
Theorem
df_3
:
wceq
c3
(
co
c2
c1
caddc
)
(proof)
Theorem
df_4
:
wceq
c4
(
co
c3
c1
caddc
)
(proof)
Theorem
df_5
:
wceq
c5
(
co
c4
c1
caddc
)
(proof)
Theorem
df_6
:
wceq
c6
(
co
c5
c1
caddc
)
(proof)
Theorem
df_7
:
wceq
c7
(
co
c6
c1
caddc
)
(proof)
Theorem
df_8
:
wceq
c8
(
co
c7
c1
caddc
)
(proof)
Theorem
df_9
:
wceq
c9
(
co
c8
c1
caddc
)
(proof)
Theorem
df_10OLD
:
wceq
c10
(
co
c9
c1
caddc
)
(proof)
Theorem
df_n0
:
wceq
cn0
(
cun
cn
(
csn
cc0
)
)
(proof)
Theorem
df_xnn0
:
wceq
cxnn0
(
cun
cn0
(
csn
cpnf
)
)
(proof)
Theorem
df_z
:
wceq
cz
(
crab
(
λ x0 .
w3o
(
wceq
(
cv
x0
)
cc0
)
(
wcel
(
cv
x0
)
cn
)
(
wcel
(
cneg
(
cv
x0
)
)
cn
)
)
(
λ x0 .
cr
)
)
(proof)
Theorem
df_dec
:
∀ x0 x1 :
ι → ο
.
wceq
(
cdc
x0
x1
)
(
co
(
co
(
co
c9
c1
caddc
)
x0
cmul
)
x1
caddc
)
(proof)
Theorem
df_uz
:
wceq
cuz
(
cmpt
(
λ x0 .
cz
)
(
λ x0 .
crab
(
λ x1 .
wbr
(
cv
x0
)
(
cv
x1
)
cle
)
(
λ x1 .
cz
)
)
)
(proof)