Search for blocks/addresses/...
Proofgold Asset
asset id
57f7e9f30673a96a1d842533dd1bd12c816804fc4aba3c34df6efa9a4291977b
asset hash
0da8011050851dfa6eb9781f2d75699c057e7eb42db1ba65e53440d58af3457b
bday / block
36396
tx
33c8c..
preasset
doc published by
PrCmT..
Known
df_q__df_rp__df_xneg__df_xadd__df_xmul__df_ioo__df_ioc__df_ico__df_icc__df_fz__df_fzo__df_fl__df_ceil__df_mod__df_seq__df_exp__df_fac__df_bc
:
∀ x0 : ο .
(
wceq
cq
(
cima
cdiv
(
cxp
cz
cn
)
)
⟶
wceq
crp
(
crab
(
λ x1 .
wbr
cc0
(
cv
x1
)
clt
)
(
λ x1 .
cr
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cxne
x1
)
(
cif
(
wceq
x1
cpnf
)
cmnf
(
cif
(
wceq
x1
cmnf
)
cpnf
(
cneg
x1
)
)
)
)
⟶
wceq
cxad
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x1
)
cpnf
)
(
cif
(
wceq
(
cv
x2
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x2
)
cmnf
)
cmnf
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
)
)
)
)
)
⟶
wceq
cxmu
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cif
(
wo
(
wceq
(
cv
x1
)
cc0
)
(
wceq
(
cv
x2
)
cc0
)
)
cc0
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x2
)
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
(
wa
(
wbr
(
cv
x2
)
cc0
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x2
)
cpnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x2
)
cmnf
)
)
)
)
cpnf
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x2
)
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
(
wa
(
wbr
(
cv
x2
)
cc0
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x2
)
cmnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x2
)
cpnf
)
)
)
)
cmnf
(
co
(
cv
x1
)
(
cv
x2
)
cmul
)
)
)
)
)
⟶
wceq
cioo
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
clt
)
(
wbr
(
cv
x3
)
(
cv
x2
)
clt
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cioc
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
clt
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cico
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
clt
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cicc
(
cmpt2
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
cxr
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cxr
)
)
)
⟶
wceq
cfz
(
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
crab
(
λ x3 .
wa
(
wbr
(
cv
x1
)
(
cv
x3
)
cle
)
(
wbr
(
cv
x3
)
(
cv
x2
)
cle
)
)
(
λ x3 .
cz
)
)
)
⟶
wceq
cfzo
(
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cv
x2
)
c1
cmin
)
cfz
)
)
⟶
wceq
cfl
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
crio
(
λ x2 .
wa
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
(
wbr
(
cv
x1
)
(
co
(
cv
x2
)
c1
caddc
)
clt
)
)
(
λ x2 .
cz
)
)
)
⟶
wceq
cceil
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
cneg
(
cfv
(
cneg
(
cv
x1
)
)
cfl
)
)
)
⟶
wceq
cmo
(
cmpt2
(
λ x1 x2 .
cr
)
(
λ x1 x2 .
crp
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cv
x2
)
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cdiv
)
cfl
)
cmul
)
cmin
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
cseq
x1
x2
x3
)
(
cima
(
crdg
(
cmpt2
(
λ x4 x5 .
cvv
)
(
λ x4 x5 .
cvv
)
(
λ x4 x5 .
cop
(
co
(
cv
x4
)
c1
caddc
)
(
co
(
cv
x5
)
(
cfv
(
co
(
cv
x4
)
c1
caddc
)
x2
)
x1
)
)
)
(
cop
x3
(
cfv
x3
x2
)
)
)
com
)
)
⟶
wceq
cexp
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x2
)
cc0
)
c1
(
cif
(
wbr
cc0
(
cv
x2
)
clt
)
(
cfv
(
cv
x2
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x1
)
)
)
c1
)
)
(
co
c1
(
cfv
(
cneg
(
cv
x2
)
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x1
)
)
)
c1
)
)
cdiv
)
)
)
)
⟶
wceq
cfa
(
cun
(
csn
(
cop
cc0
c1
)
)
(
cseq
cmul
cid
c1
)
)
⟶
wceq
cbc
(
cmpt2
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
cif
(
wcel
(
cv
x2
)
(
co
cc0
(
cv
x1
)
cfz
)
)
(
co
(
cfv
(
cv
x1
)
cfa
)
(
co
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmin
)
cfa
)
(
cfv
(
cv
x2
)
cfa
)
cmul
)
cdiv
)
cc0
)
)
⟶
x0
)
⟶
x0
Theorem
df_q
:
wceq
cq
(
cima
cdiv
(
cxp
cz
cn
)
)
(proof)
Theorem
df_rp
:
wceq
crp
(
crab
(
λ x0 .
wbr
cc0
(
cv
x0
)
clt
)
(
λ x0 .
cr
)
)
(proof)
Theorem
df_xneg
:
∀ x0 :
ι → ο
.
wceq
(
cxne
x0
)
(
cif
(
wceq
x0
cpnf
)
cmnf
(
cif
(
wceq
x0
cmnf
)
cpnf
(
cneg
x0
)
)
)
(proof)
Theorem
df_xadd
:
wceq
cxad
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x0
)
cpnf
)
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cc0
cpnf
)
(
cif
(
wceq
(
cv
x0
)
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cc0
cmnf
)
(
cif
(
wceq
(
cv
x1
)
cpnf
)
cpnf
(
cif
(
wceq
(
cv
x1
)
cmnf
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
caddc
)
)
)
)
)
)
(proof)
Theorem
df_xmul
:
wceq
cxmu
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cif
(
wo
(
wceq
(
cv
x0
)
cc0
)
(
wceq
(
cv
x1
)
cc0
)
)
cc0
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x0
)
cpnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x0
)
cmnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x0
)
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
(
wa
(
wbr
(
cv
x0
)
cc0
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
)
)
cpnf
(
cif
(
wo
(
wo
(
wa
(
wbr
cc0
(
cv
x1
)
clt
)
(
wceq
(
cv
x0
)
cmnf
)
)
(
wa
(
wbr
(
cv
x1
)
cc0
clt
)
(
wceq
(
cv
x0
)
cpnf
)
)
)
(
wo
(
wa
(
wbr
cc0
(
cv
x0
)
clt
)
(
wceq
(
cv
x1
)
cmnf
)
)
(
wa
(
wbr
(
cv
x0
)
cc0
clt
)
(
wceq
(
cv
x1
)
cpnf
)
)
)
)
cmnf
(
co
(
cv
x0
)
(
cv
x1
)
cmul
)
)
)
)
)
(proof)
Theorem
df_ioo
:
wceq
cioo
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
clt
)
(
wbr
(
cv
x2
)
(
cv
x1
)
clt
)
)
(
λ x2 .
cxr
)
)
)
(proof)
Theorem
df_ioc
:
wceq
cioc
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
clt
)
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
)
(
λ x2 .
cxr
)
)
)
(proof)
Theorem
df_ico
:
wceq
cico
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
cle
)
(
wbr
(
cv
x2
)
(
cv
x1
)
clt
)
)
(
λ x2 .
cxr
)
)
)
(proof)
Theorem
df_icc
:
wceq
cicc
(
cmpt2
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
cxr
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
cle
)
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
)
(
λ x2 .
cxr
)
)
)
(proof)
Theorem
df_fz
:
wceq
cfz
(
cmpt2
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
crab
(
λ x2 .
wa
(
wbr
(
cv
x0
)
(
cv
x2
)
cle
)
(
wbr
(
cv
x2
)
(
cv
x1
)
cle
)
)
(
λ x2 .
cz
)
)
)
(proof)
Theorem
df_fzo
:
wceq
cfzo
(
cmpt2
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
co
(
cv
x0
)
(
co
(
cv
x1
)
c1
cmin
)
cfz
)
)
(proof)
Theorem
df_fl
:
wceq
cfl
(
cmpt
(
λ x0 .
cr
)
(
λ x0 .
crio
(
λ x1 .
wa
(
wbr
(
cv
x1
)
(
cv
x0
)
cle
)
(
wbr
(
cv
x0
)
(
co
(
cv
x1
)
c1
caddc
)
clt
)
)
(
λ x1 .
cz
)
)
)
(proof)
Theorem
df_ceil
:
wceq
cceil
(
cmpt
(
λ x0 .
cr
)
(
λ x0 .
cneg
(
cfv
(
cneg
(
cv
x0
)
)
cfl
)
)
)
(proof)
Theorem
df_mod
:
wceq
cmo
(
cmpt2
(
λ x0 x1 .
cr
)
(
λ x0 x1 .
crp
)
(
λ x0 x1 .
co
(
cv
x0
)
(
co
(
cv
x1
)
(
cfv
(
co
(
cv
x0
)
(
cv
x1
)
cdiv
)
cfl
)
cmul
)
cmin
)
)
(proof)
Theorem
df_seq
:
∀ x0 x1 x2 :
ι → ο
.
wceq
(
cseq
x0
x1
x2
)
(
cima
(
crdg
(
cmpt2
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
cop
(
co
(
cv
x3
)
c1
caddc
)
(
co
(
cv
x4
)
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
x1
)
x0
)
)
)
(
cop
x2
(
cfv
x2
x1
)
)
)
com
)
(proof)
Theorem
df_exp
:
wceq
cexp
(
cmpt2
(
λ x0 x1 .
cc
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
c1
(
cif
(
wbr
cc0
(
cv
x1
)
clt
)
(
cfv
(
cv
x1
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x0
)
)
)
c1
)
)
(
co
c1
(
cfv
(
cneg
(
cv
x1
)
)
(
cseq
cmul
(
cxp
cn
(
csn
(
cv
x0
)
)
)
c1
)
)
cdiv
)
)
)
)
(proof)
Theorem
df_fac
:
wceq
cfa
(
cun
(
csn
(
cop
cc0
c1
)
)
(
cseq
cmul
cid
c1
)
)
(proof)
Theorem
df_bc
:
wceq
cbc
(
cmpt2
(
λ x0 x1 .
cn0
)
(
λ x0 x1 .
cz
)
(
λ x0 x1 .
cif
(
wcel
(
cv
x1
)
(
co
cc0
(
cv
x0
)
cfz
)
)
(
co
(
cfv
(
cv
x0
)
cfa
)
(
co
(
cfv
(
co
(
cv
x0
)
(
cv
x1
)
cmin
)
cfa
)
(
cfv
(
cv
x1
)
cfa
)
cmul
)
cdiv
)
cc0
)
)
(proof)