Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
crtcl
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cint
(
cab
(
λ x2 .
w3a
(
wss
(
cres
cid
(
cun
(
cdm
(
cv
x1
)
)
(
crn
(
cv
x1
)
)
)
)
(
cv
x2
)
)
(
wss
(
cv
x1
)
(
cv
x2
)
)
(
wss
(
ccom
(
cv
x2
)
(
cv
x2
)
)
(
cv
x2
)
)
)
)
)
)
⟶
wceq
crelexp
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cif
(
wceq
(
cv
x2
)
cc0
)
(
cres
cid
(
cun
(
cdm
(
cv
x1
)
)
(
crn
(
cv
x1
)
)
)
)
(
cfv
(
cv
x2
)
(
cseq
(
cmpt2
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
ccom
(
cv
x3
)
(
cv
x1
)
)
)
(
cmpt
(
λ x3 .
cvv
)
(
λ x3 .
cv
x1
)
)
c1
)
)
)
)
⟶
wceq
crtrcl
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
ciun
(
λ x2 .
cn0
)
(
λ x2 .
co
(
cv
x1
)
(
cv
x2
)
crelexp
)
)
)
⟶
wceq
cshi
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
copab
(
λ x3 x4 .
wa
(
wcel
(
cv
x3
)
cc
)
(
wbr
(
co
(
cv
x3
)
(
cv
x2
)
cmin
)
(
cv
x4
)
(
cv
x1
)
)
)
)
)
⟶
wceq
csgn
(
cmpt
(
λ x1 .
cxr
)
(
λ x1 .
cif
(
wceq
(
cv
x1
)
cc0
)
cc0
(
cif
(
wbr
(
cv
x1
)
cc0
clt
)
(
cneg
c1
)
c1
)
)
)
⟶
wceq
ccj
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
crio
(
λ x2 .
wa
(
wcel
(
co
(
cv
x1
)
(
cv
x2
)
caddc
)
cr
)
(
wcel
(
co
ci
(
co
(
cv
x1
)
(
cv
x2
)
cmin
)
cmul
)
cr
)
)
(
λ x2 .
cc
)
)
)
⟶
wceq
cre
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
co
(
co
(
cv
x1
)
(
cfv
(
cv
x1
)
ccj
)
caddc
)
c2
cdiv
)
)
⟶
wceq
cim
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
cfv
(
co
(
cv
x1
)
ci
cdiv
)
cre
)
)
⟶
wceq
csqrt
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
crio
(
λ x2 .
w3a
(
wceq
(
co
(
cv
x2
)
c2
cexp
)
(
cv
x1
)
)
(
wbr
cc0
(
cfv
(
cv
x2
)
cre
)
cle
)
(
wnel
(
co
ci
(
cv
x2
)
cmul
)
crp
)
)
(
λ x2 .
cc
)
)
)
⟶
wceq
cabs
(
cmpt
(
λ x1 .
cc
)
(
λ x1 .
cfv
(
co
(
cv
x1
)
(
cfv
(
cv
x1
)
ccj
)
cmul
)
csqrt
)
)
⟶
wceq
clsp
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cinf
(
crn
(
cmpt
(
λ x2 .
cr
)
(
λ x2 .
csup
(
cin
(
cima
(
cv
x1
)
(
co
(
cv
x2
)
cpnf
cico
)
)
cxr
)
cxr
clt
)
)
)
cxr
clt
)
)
⟶
wceq
cli
(
copab
(
λ x1 x2 .
wa
(
wcel
(
cv
x2
)
cc
)
(
wral
(
λ x3 .
wrex
(
λ x4 .
wral
(
λ x5 .
wa
(
wcel
(
cfv
(
cv
x5
)
(
cv
x1
)
)
cc
)
(
wbr
(
cfv
(
co
(
cfv
(
cv
x5
)
(
cv
x1
)
)
(
cv
x2
)
cmin
)
cabs
)
(
cv
x3
)
clt
)
)
(
λ x5 .
cfv
(
cv
x4
)
cuz
)
)
(
λ x4 .
cz
)
)
(
λ x3 .
crp
)
)
)
)
⟶
wceq
crli
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
(
co
cc
cr
cpm
)
)
(
wcel
(
cv
x2
)
cc
)
)
(
wral
(
λ x3 .
wrex
(
λ x4 .
wral
(
λ x5 .
wbr
(
cv
x4
)
(
cv
x5
)
cle
⟶
wbr
(
cfv
(
co
(
cfv
(
cv
x5
)
(
cv
x1
)
)
(
cv
x2
)
cmin
)
cabs
)
(
cv
x3
)
clt
)
(
λ x5 .
cdm
(
cv
x1
)
)
)
(
λ x4 .
cr
)
)
(
λ x3 .
crp
)
)
)
)
⟶
wceq
co1
(
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wral
(
λ x4 .
wbr
(
cfv
(
cfv
(
cv
x4
)
(
cv
x1
)
)
cabs
)
(
cv
x3
)
cle
)
(
λ x4 .
cin
(
cdm
(
cv
x1
)
)
(
co
(
cv
x2
)
cpnf
cico
)
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
cr
)
)
(
λ x1 .
co
cc
cr
cpm
)
)
⟶
wceq
clo1
(
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wral
(
λ x4 .
wbr
(
cfv
(
cv
x4
)
(
cv
x1
)
)
(
cv
x3
)
cle
)
(
λ x4 .
cin
(
cdm
(
cv
x1
)
)
(
co
(
cv
x2
)
cpnf
cico
)
)
)
(
λ x3 .
cr
)
)
(
λ x2 .
cr
)
)
(
λ x1 .
co
cr
cr
cpm
)
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wceq
(
csu
(
x1
x3
)
x2
)
(
cio
(
λ x4 .
wo
(
wrex
(
λ x5 .
wa
(
wss
(
x1
x3
)
(
cfv
(
cv
x5
)
cuz
)
)
(
wbr
(
cseq
caddc
(
cmpt
(
λ x6 .
cz
)
(
λ x6 .
cif
(
wcel
(
cv
x6
)
(
x1
x3
)
)
(
csb
(
cv
x6
)
x2
)
cc0
)
)
(
cv
x5
)
)
(
cv
x4
)
cli
)
)
(
λ x5 .
cz
)
)
(
wrex
(
λ x5 .
wex
(
λ x6 .
wa
(
wf1o
(
co
c1
(
cv
x5
)
cfz
)
(
x1
x3
)
(
cv
x6
)
)
(
wceq
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cseq
caddc
(
cmpt
(
λ x7 .
cn
)
(
λ x7 .
csb
(
cfv
(
cv
x7
)
(
cv
x6
)
)
x2
)
)
c1
)
)
)
)
)
(
λ x5 .
cn
)
)
)
)
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wceq
(
cprod
x1
x2
)
(
cio
(
λ x4 .
wo
(
wrex
(
λ x5 .
w3a
(
wss
(
x1
x3
)
(
cfv
(
cv
x5
)
cuz
)
)
(
wrex
(
λ x6 .
wex
(
λ x7 .
wa
(
wne
(
cv
x7
)
cc0
)
(
wbr
(
cseq
cmul
(
cmpt
(
λ x8 .
cz
)
(
λ x8 .
cif
(
wcel
(
cv
x8
)
(
x1
x8
)
)
(
x2
x8
)
c1
)
)
(
cv
x6
)
)
(
cv
x7
)
cli
)
)
)
(
λ x6 .
cfv
(
cv
x5
)
cuz
)
)
(
wbr
(
cseq
cmul
(
cmpt
(
λ x6 .
cz
)
(
λ x6 .
cif
(
wcel
(
cv
x6
)
(
x1
x6
)
)
(
x2
x6
)
c1
)
)
(
cv
x5
)
)
(
cv
x4
)
cli
)
)
(
λ x5 .
cz
)
)
(
wrex
(
λ x5 .
wex
(
λ x6 .
wa
(
wf1o
(
co
c1
(
cv
x5
)
cfz
)
(
x1
x3
)
(
cv
x6
)
)
(
wceq
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cseq
cmul
(
cmpt
(
λ x7 .
cn
)
(
λ x7 .
csb
(
cfv
(
cv
x7
)
(
cv
x6
)
)
x2
)
)
c1
)
)
)
)
)
(
λ x5 .
cn
)
)
)
)
)
⟶
wceq
crisefac
(
cmpt2
(
λ x1 x2 .
cc
)
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cprod
(
λ x3 .
co
cc0
(
co
(
cv
x2
)
c1
cmin
)
cfz
)
(
λ x3 .
co
(
cv
x1
)
(
cv
x3
)
caddc
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_rtrcl__df_relexp__df_rtrclrec__df_shft__df_sgn__df_cj__df_re__df_im__df_sqrt__df_abs__df_limsup__df_clim__df_rlim__df_o1__df_lo1__df_sum__df_prod__df_risefac
proof
PUV1k..
Megalodon
-
proofgold address
TMSPK..
creator
36224
PrCmT..
/
0f694..
owner
36224
PrCmT..
/
0f694..
term root
270cf..