Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
ctayl
(
cmpt2
(
λ x1 x2 .
cpr
cr
cc
)
(
λ x1 x2 .
co
cc
(
cv
x1
)
cpm
)
(
λ x1 x2 .
cmpt2
(
λ x3 x4 .
cun
cn0
(
csn
cpnf
)
)
(
λ x3 x4 .
ciin
(
λ x5 .
cin
(
co
cc0
(
cv
x3
)
cicc
)
cz
)
(
λ x5 .
cdm
(
cfv
(
cv
x5
)
(
co
(
cv
x1
)
(
cv
x2
)
cdvn
)
)
)
)
(
λ x3 x4 .
ciun
(
λ x5 .
cc
)
(
λ x5 .
cxp
(
csn
(
cv
x5
)
)
(
co
ccnfld
(
cmpt
(
λ x6 .
cin
(
co
cc0
(
cv
x3
)
cicc
)
cz
)
(
λ x6 .
co
(
co
(
cfv
(
cv
x4
)
(
cfv
(
cv
x6
)
(
co
(
cv
x1
)
(
cv
x2
)
cdvn
)
)
)
(
cfv
(
cv
x6
)
cfa
)
cdiv
)
(
co
(
co
(
cv
x5
)
(
cv
x4
)
cmin
)
(
cv
x6
)
cexp
)
cmul
)
)
ctsu
)
)
)
)
)
⟶
wceq
cana
(
cmpt
(
λ x1 .
cpr
cr
cc
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wcel
(
cv
x3
)
(
cfv
(
cdm
(
cin
(
cv
x2
)
(
co
cpnf
(
cv
x3
)
(
co
(
cv
x1
)
(
cv
x2
)
ctayl
)
)
)
)
(
cfv
(
co
(
cfv
ccnfld
ctopn
)
(
cv
x1
)
crest
)
cnt
)
)
)
(
λ x3 .
cdm
(
cv
x2
)
)
)
(
λ x2 .
co
cc
(
cv
x1
)
cpm
)
)
)
⟶
wceq
culm
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wrex
(
λ x4 .
w3a
(
wf
(
cfv
(
cv
x4
)
cuz
)
(
co
cc
(
cv
x1
)
cmap
)
(
cv
x2
)
)
(
wf
(
cv
x1
)
cc
(
cv
x3
)
)
(
wral
(
λ x5 .
wrex
(
λ x6 .
wral
(
λ x7 .
wral
(
λ x8 .
wbr
(
cfv
(
co
(
cfv
(
cv
x8
)
(
cfv
(
cv
x7
)
(
cv
x2
)
)
)
(
cfv
(
cv
x8
)
(
cv
x3
)
)
cmin
)
cabs
)
(
cv
x5
)
clt
)
(
λ x8 .
cv
x1
)
)
(
λ x7 .
cfv
(
cv
x6
)
cuz
)
)
(
λ x6 .
cfv
(
cv
x4
)
cuz
)
)
(
λ x5 .
crp
)
)
)
(
λ x4 .
cz
)
)
)
)
⟶
wceq
clog
(
ccnv
(
cres
ce
(
cima
(
ccnv
cim
)
(
co
(
cneg
cpi
)
cpi
cioc
)
)
)
)
⟶
wceq
ccxp
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x1
)
cc0
)
(
cif
(
wceq
(
cv
x2
)
cc0
)
c1
cc0
)
(
cfv
(
co
(
cv
x2
)
(
cfv
(
cv
x1
)
clog
)
cmul
)
ce
)
)
)
⟶
wceq
clogb
(
cmpt2
(
λ x1 x2 .
cdif
cc
(
cpr
cc0
c1
)
)
(
λ x1 x2 .
cdif
cc
(
csn
cc0
)
)
(
λ x1 x2 .
co
(
cfv
(
cv
x2
)
clog
)
(
cfv
(
cv
x1
)
clog
)
cdiv
)
)
⟶
wceq
casin
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
co
(
cneg
ci
)
(
cfv
(
co
(
co
ci
(
cv
x1
)
cmul
)
(
cfv
(
co
c1
(
co
(
cv
x1
)
c2
cexp
)
cmin
)
csqrt
)
caddc
)
clog
)
cmul
)
)
⟶
wceq
cacos
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
co
(
co
cpi
c2
cdiv
)
(
cfv
(
cv
x1
)
casin
)
cmin
)
)
⟶
wceq
catan
(
cmpt
(
λ x1 .
cdif
cc
(
cpr
(
cneg
ci
)
ci
)
)
(
λ x1 .
co
(
co
ci
c2
cdiv
)
(
co
(
cfv
(
co
c1
(
co
ci
(
cv
x1
)
cmul
)
cmin
)
clog
)
(
cfv
(
co
c1
(
co
ci
(
cv
x1
)
cmul
)
caddc
)
clog
)
cmin
)
cmul
)
)
⟶
wceq
carea
(
cmpt
(
λ x1 .
crab
(
λ x2 .
wa
(
wral
(
λ x3 .
wcel
(
cima
(
cv
x2
)
(
csn
(
cv
x3
)
)
)
(
cima
(
ccnv
cvol
)
cr
)
)
(
λ x3 .
cr
)
)
(
wcel
(
cmpt
(
λ x3 .
cr
)
(
λ x3 .
cfv
(
cima
(
cv
x2
)
(
csn
(
cv
x3
)
)
)
cvol
)
)
cibl
)
)
(
λ x2 .
cpw
(
cxp
cr
cr
)
)
)
(
λ x1 .
citg
(
λ x2 .
cr
)
(
λ x2 .
cfv
(
cima
(
cv
x1
)
(
csn
(
cv
x2
)
)
)
cvol
)
)
)
⟶
wceq
cem
(
csu
cn
(
λ x1 .
co
(
co
c1
(
cv
x1
)
cdiv
)
(
cfv
(
co
c1
(
co
c1
(
cv
x1
)
cdiv
)
caddc
)
clog
)
cmin
)
)
⟶
wceq
czeta
(
crio
(
λ x1 .
wral
(
λ x2 .
wceq
(
co
(
co
c1
(
co
c2
(
co
c1
(
cv
x2
)
cmin
)
ccxp
)
cmin
)
(
cfv
(
cv
x2
)
(
cv
x1
)
)
cmul
)
(
csu
cn0
(
λ x3 .
co
(
csu
(
co
cc0
(
cv
x3
)
cfz
)
(
λ x4 .
co
(
co
(
co
(
cneg
c1
)
(
cv
x4
)
cexp
)
(
co
(
cv
x3
)
(
cv
x4
)
cbc
)
cmul
)
(
co
(
co
(
cv
x4
)
c1
caddc
)
(
cv
x2
)
ccxp
)
cmul
)
)
(
co
c2
(
co
(
cv
x3
)
c1
caddc
)
cexp
)
cdiv
)
)
)
(
λ x2 .
cdif
cc
(
csn
c1
)
)
)
(
λ x1 .
co
(
cdif
cc
(
csn
c1
)
)
cc
ccncf
)
)
⟶
wceq
clgam
(
cmpt
(
λ x1 .
cdif
cc
(
cdif
cz
cn
)
)
(
λ x1 .
co
(
csu
cn
(
λ x2 .
co
(
co
(
cv
x1
)
(
cfv
(
co
(
co
(
cv
x2
)
c1
caddc
)
(
cv
x2
)
cdiv
)
clog
)
cmul
)
(
cfv
(
co
(
co
(
cv
x1
)
(
cv
x2
)
cdiv
)
c1
caddc
)
clog
)
cmin
)
)
(
cfv
(
cv
x1
)
clog
)
cmin
)
)
⟶
wceq
cgam
(
ccom
ce
clgam
)
⟶
wceq
cigam
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
(
cdif
cz
cn
)
)
cc0
(
co
c1
(
cfv
(
cv
x1
)
cgam
)
cdiv
)
)
)
⟶
wceq
ccht
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
csu
(
cin
(
co
cc0
(
cv
x1
)
cicc
)
cprime
)
(
λ x2 .
cfv
(
cv
x2
)
clog
)
)
)
⟶
wceq
cvma
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
csb
(
crab
(
λ x2 .
wbr
(
cv
x2
)
(
cv
x1
)
cdvds
)
(
λ x2 .
cprime
)
)
(
λ x2 .
cif
(
wceq
(
cfv
(
cv
x2
)
chash
)
c1
)
(
cfv
(
cuni
(
cv
x2
)
)
clog
)
cc0
)
)
)
⟶
wceq
cchp
(
cmpt
(
λ x1 .
cr
)
(
λ x1 .
csu
(
co
c1
(
cfv
(
cv
x1
)
cfl
)
cfz
)
(
λ x2 .
cfv
(
cv
x2
)
cvma
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_tayl__df_ana__df_ulm__df_log__df_cxp__df_logb__df_asin__df_acos__df_atan__df_area__df_em__df_zeta__df_lgam__df_gam__df_igam__df_cht__df_vma__df_chp
proof
PUV1k..
Megalodon
-
proofgold address
TMPpr..
creator
36224
PrCmT..
/
7e150..
owner
36224
PrCmT..
/
7e150..
term root
4955a..