Search for blocks/addresses/...
Proofgold Asset
asset id
ae2642ddab4e549bf6735dc826dfbeb4f91ba7637e75f78ea48e6b3eb60b3efa
asset hash
ae99238e2ac2298bc149443e7fe550ed06b7cf1388c1b6bfa3f44d6adb990295
bday / block
36378
tx
3e5e5..
preasset
doc published by
PrCmT..
Known
df_bigo__df_blen__df_dig__df_setrecs__df_pg__df_gte__df_gt__df_sinh__df_cosh__df_tanh__df_sec__df_csc__df_cot__df_logbALT__df_reflexive__df_irreflexive__df_alsi__df_alsc
:
∀ x0 : ο .
(
wceq
cbigo
(
cmpt
(
λ x1 .
co
cr
cr
cpm
)
(
λ x1 .
crab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wral
(
λ x5 .
wbr
(
cfv
(
cv
x5
)
(
cv
x2
)
)
(
co
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cv
x1
)
)
cmul
)
cle
)
(
λ x5 .
cin
(
cdm
(
cv
x2
)
)
(
co
(
cv
x3
)
cpnf
cico
)
)
)
(
λ x4 .
cr
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
co
cr
cr
cpm
)
)
)
⟶
wceq
cblen
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
c1
(
co
(
cfv
(
co
c2
(
cfv
(
cv
x1
)
cabs
)
clogb
)
cfl
)
c1
caddc
)
)
)
⟶
wceq
cdig
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cz
)
(
λ x2 x3 .
co
cc0
cpnf
cico
)
(
λ x2 x3 .
co
(
cfv
(
co
(
co
(
cv
x1
)
(
cneg
(
cv
x2
)
)
cexp
)
(
cv
x3
)
cmul
)
cfl
)
(
cv
x1
)
cmo
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
csetrecs
x1
)
(
cuni
(
cab
(
λ x2 .
∀ x3 .
(
∀ x4 .
wss
(
cv
x4
)
(
cv
x2
)
⟶
wss
(
cv
x4
)
(
cv
x3
)
⟶
wss
(
cfv
(
cv
x4
)
x1
)
(
cv
x3
)
)
⟶
wss
(
cv
x2
)
(
cv
x3
)
)
)
)
)
⟶
wceq
cpg
(
csetrecs
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cxp
(
cpw
(
cv
x1
)
)
(
cpw
(
cv
x1
)
)
)
)
)
⟶
wceq
cge_real
(
ccnv
cle
)
⟶
wceq
cgt
(
ccnv
clt
)
⟶
wceq
csinh
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
co
(
cfv
(
co
ci
(
cv
x1
)
cmul
)
csin
)
ci
cdiv
)
)
⟶
wceq
ccosh
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
cfv
(
co
ci
(
cv
x1
)
cmul
)
ccos
)
)
⟶
wceq
ctanh
(
cmpt
(
λ x1 .
cima
(
ccnv
ccosh
)
(
cdif
cc
(
csn
cc0
)
)
)
(
λ x1 .
co
(
cfv
(
co
ci
(
cv
x1
)
cmul
)
ctan
)
ci
cdiv
)
)
⟶
wceq
csec
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wne
(
cfv
(
cv
x2
)
ccos
)
cc0
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
c1
(
cfv
(
cv
x1
)
ccos
)
cdiv
)
)
⟶
wceq
ccsc
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wne
(
cfv
(
cv
x2
)
csin
)
cc0
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
c1
(
cfv
(
cv
x1
)
csin
)
cdiv
)
)
⟶
wceq
ccot
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wne
(
cfv
(
cv
x2
)
csin
)
cc0
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
(
cfv
(
cv
x1
)
ccos
)
(
cfv
(
cv
x1
)
csin
)
cdiv
)
)
⟶
wceq
clog_
(
cmpt
(
λ x1 .
cdif
cc
(
cpr
cc0
c1
)
)
(
λ x1 .
cmpt
(
λ x2 .
cdif
cc
(
csn
cc0
)
)
(
λ x2 .
co
(
cfv
(
cv
x2
)
clog
)
(
cfv
(
cv
x1
)
clog
)
cdiv
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wreflexive
x1
x2
)
(
wa
(
wss
x2
(
cxp
x1
x1
)
)
(
wral
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x3
)
x2
)
(
λ x3 .
x1
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wirreflexive
x1
x2
)
(
wa
(
wss
x2
(
cxp
x1
x1
)
)
(
wral
(
λ x3 .
wn
(
wbr
(
cv
x3
)
(
cv
x3
)
x2
)
)
(
λ x3 .
x1
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
walsi
x1
x2
)
(
wa
(
∀ x3 .
x1
x3
⟶
x2
x3
)
(
wex
x1
)
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wb
(
walsc
x1
x2
)
(
wa
(
wral
x1
x2
)
(
wex
(
λ x3 .
wcel
(
cv
x3
)
(
x2
x3
)
)
)
)
)
⟶
x0
)
⟶
x0
Theorem
df_bigo
:
wceq
cbigo
(
cmpt
(
λ x0 .
co
cr
cr
cpm
)
(
λ x0 .
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wral
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
(
cv
x1
)
)
(
co
(
cv
x3
)
(
cfv
(
cv
x4
)
(
cv
x0
)
)
cmul
)
cle
)
(
λ x4 .
cin
(
cdm
(
cv
x1
)
)
(
co
(
cv
x2
)
cpnf
cico
)
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
cr
)
)
(
λ x1 .
co
cr
cr
cpm
)
)
)
(proof)
Theorem
df_blen
:
wceq
cblen
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cif
(
wceq
(
cv
x0
)
cc0
)
c1
(
co
(
cfv
(
co
c2
(
cfv
(
cv
x0
)
cabs
)
clogb
)
cfl
)
c1
caddc
)
)
)
(proof)
Theorem
df_dig
:
wceq
cdig
(
cmpt
(
λ x0 .
cn
)
(
λ x0 .
cmpt2
(
λ x1 x2 .
cz
)
(
λ x1 x2 .
co
cc0
cpnf
cico
)
(
λ x1 x2 .
co
(
cfv
(
co
(
co
(
cv
x0
)
(
cneg
(
cv
x1
)
)
cexp
)
(
cv
x2
)
cmul
)
cfl
)
(
cv
x0
)
cmo
)
)
)
(proof)
Theorem
df_setrecs
:
∀ x0 :
ι → ο
.
wceq
(
csetrecs
x0
)
(
cuni
(
cab
(
λ x1 .
∀ x2 .
(
∀ x3 .
wss
(
cv
x3
)
(
cv
x1
)
⟶
wss
(
cv
x3
)
(
cv
x2
)
⟶
wss
(
cfv
(
cv
x3
)
x0
)
(
cv
x2
)
)
⟶
wss
(
cv
x1
)
(
cv
x2
)
)
)
)
(proof)
Theorem
df_pg
:
wceq
cpg
(
csetrecs
(
cmpt
(
λ x0 .
cvv
)
(
λ x0 .
cxp
(
cpw
(
cv
x0
)
)
(
cpw
(
cv
x0
)
)
)
)
)
(proof)
Theorem
df_gte
:
wceq
cge_real
(
ccnv
cle
)
(proof)
Theorem
df_gt
:
wceq
cgt
(
ccnv
clt
)
(proof)
Theorem
df_sinh
:
wceq
csinh
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
co
(
cfv
(
co
ci
(
cv
x0
)
cmul
)
csin
)
ci
cdiv
)
)
(proof)
Theorem
df_cosh
:
wceq
ccosh
(
cmpt
(
λ x0 .
cc
)
(
λ x0 .
cfv
(
co
ci
(
cv
x0
)
cmul
)
ccos
)
)
(proof)
Theorem
df_tanh
:
wceq
ctanh
(
cmpt
(
λ x0 .
cima
(
ccnv
ccosh
)
(
cdif
cc
(
csn
cc0
)
)
)
(
λ x0 .
co
(
cfv
(
co
ci
(
cv
x0
)
cmul
)
ctan
)
ci
cdiv
)
)
(proof)
Theorem
df_sec
:
wceq
csec
(
cmpt
(
λ x0 .
crab
(
λ x1 .
wne
(
cfv
(
cv
x1
)
ccos
)
cc0
)
(
λ x1 .
cc
)
)
(
λ x0 .
co
c1
(
cfv
(
cv
x0
)
ccos
)
cdiv
)
)
(proof)
Theorem
df_csc
:
wceq
ccsc
(
cmpt
(
λ x0 .
crab
(
λ x1 .
wne
(
cfv
(
cv
x1
)
csin
)
cc0
)
(
λ x1 .
cc
)
)
(
λ x0 .
co
c1
(
cfv
(
cv
x0
)
csin
)
cdiv
)
)
(proof)
Theorem
df_cot
:
wceq
ccot
(
cmpt
(
λ x0 .
crab
(
λ x1 .
wne
(
cfv
(
cv
x1
)
csin
)
cc0
)
(
λ x1 .
cc
)
)
(
λ x0 .
co
(
cfv
(
cv
x0
)
ccos
)
(
cfv
(
cv
x0
)
csin
)
cdiv
)
)
(proof)
Theorem
df_logbALT
:
wceq
clog_
(
cmpt
(
λ x0 .
cdif
cc
(
cpr
cc0
c1
)
)
(
λ x0 .
cmpt
(
λ x1 .
cdif
cc
(
csn
cc0
)
)
(
λ x1 .
co
(
cfv
(
cv
x1
)
clog
)
(
cfv
(
cv
x0
)
clog
)
cdiv
)
)
)
(proof)
Theorem
df_reflexive
:
∀ x0 x1 :
ι → ο
.
wb
(
wreflexive
x0
x1
)
(
wa
(
wss
x1
(
cxp
x0
x0
)
)
(
wral
(
λ x2 .
wbr
(
cv
x2
)
(
cv
x2
)
x1
)
(
λ x2 .
x0
)
)
)
(proof)
Theorem
df_irreflexive
:
∀ x0 x1 :
ι → ο
.
wb
(
wirreflexive
x0
x1
)
(
wa
(
wss
x1
(
cxp
x0
x0
)
)
(
wral
(
λ x2 .
wn
(
wbr
(
cv
x2
)
(
cv
x2
)
x1
)
)
(
λ x2 .
x0
)
)
)
(proof)
Theorem
df_alsi
:
∀ x0 x1 :
ι → ο
.
wb
(
walsi
x0
x1
)
(
wa
(
∀ x2 .
x0
x2
⟶
x1
x2
)
(
wex
x0
)
)
(proof)
Theorem
df_alsc
:
∀ x0 :
ι → ο
.
∀ x1 :
ι →
ι → ο
.
wb
(
walsc
x0
x1
)
(
wa
(
wral
x0
x1
)
(
wex
(
λ x2 .
wcel
(
cv
x2
)
(
x1
x2
)
)
)
)
(proof)