Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cdip
(
cmpt
(
λ x1 .
cnv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cba
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cba
)
(
λ x2 x3 .
co
(
csu
(
co
c1
c4
cfz
)
(
λ x4 .
co
(
co
ci
(
cv
x4
)
cexp
)
(
co
(
cfv
(
co
(
cv
x2
)
(
co
(
co
ci
(
cv
x4
)
cexp
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cns
)
)
(
cfv
(
cv
x1
)
cpv
)
)
(
cfv
(
cv
x1
)
cnmcv
)
)
c2
cexp
)
cmul
)
)
c4
cdiv
)
)
)
⟶
wceq
css
(
cmpt
(
λ x1 .
cnv
)
(
λ x1 .
crab
(
λ x2 .
w3a
(
wss
(
cfv
(
cv
x2
)
cpv
)
(
cfv
(
cv
x1
)
cpv
)
)
(
wss
(
cfv
(
cv
x2
)
cns
)
(
cfv
(
cv
x1
)
cns
)
)
(
wss
(
cfv
(
cv
x2
)
cnmcv
)
(
cfv
(
cv
x1
)
cnmcv
)
)
)
(
λ x2 .
cnv
)
)
)
⟶
wceq
clno
(
cmpt2
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
crab
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wral
(
λ x6 .
wceq
(
cfv
(
co
(
co
(
cv
x4
)
(
cv
x5
)
(
cfv
(
cv
x1
)
cns
)
)
(
cv
x6
)
(
cfv
(
cv
x1
)
cpv
)
)
(
cv
x3
)
)
(
co
(
co
(
cv
x4
)
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cfv
(
cv
x2
)
cns
)
)
(
cfv
(
cv
x6
)
(
cv
x3
)
)
(
cfv
(
cv
x2
)
cpv
)
)
)
(
λ x6 .
cfv
(
cv
x1
)
cba
)
)
(
λ x5 .
cfv
(
cv
x1
)
cba
)
)
(
λ x4 .
cc
)
)
(
λ x3 .
co
(
cfv
(
cv
x2
)
cba
)
(
cfv
(
cv
x1
)
cba
)
cmap
)
)
)
⟶
wceq
cnmoo
(
cmpt2
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
co
(
cfv
(
cv
x2
)
cba
)
(
cfv
(
cv
x1
)
cba
)
cmap
)
(
λ x3 .
csup
(
cab
(
λ x4 .
wrex
(
λ x5 .
wa
(
wbr
(
cfv
(
cv
x5
)
(
cfv
(
cv
x1
)
cnmcv
)
)
c1
cle
)
(
wceq
(
cv
x4
)
(
cfv
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cfv
(
cv
x2
)
cnmcv
)
)
)
)
(
λ x5 .
cfv
(
cv
x1
)
cba
)
)
)
cxr
clt
)
)
)
⟶
wceq
cblo
(
cmpt2
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
crab
(
λ x3 .
wbr
(
cfv
(
cv
x3
)
(
co
(
cv
x1
)
(
cv
x2
)
cnmoo
)
)
cpnf
clt
)
(
λ x3 .
co
(
cv
x1
)
(
cv
x2
)
clno
)
)
)
⟶
wceq
c0o
(
cmpt2
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cxp
(
cfv
(
cv
x1
)
cba
)
(
csn
(
cfv
(
cv
x2
)
cn0v
)
)
)
)
⟶
wceq
caj
(
cmpt2
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
cnv
)
(
λ x1 x2 .
copab
(
λ x3 x4 .
w3a
(
wf
(
cfv
(
cv
x1
)
cba
)
(
cfv
(
cv
x2
)
cba
)
(
cv
x3
)
)
(
wf
(
cfv
(
cv
x2
)
cba
)
(
cfv
(
cv
x1
)
cba
)
(
cv
x4
)
)
(
wral
(
λ x5 .
wral
(
λ x6 .
wceq
(
co
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cv
x6
)
(
cfv
(
cv
x2
)
cdip
)
)
(
co
(
cv
x5
)
(
cfv
(
cv
x6
)
(
cv
x4
)
)
(
cfv
(
cv
x1
)
cdip
)
)
)
(
λ x6 .
cfv
(
cv
x2
)
cba
)
)
(
λ x5 .
cfv
(
cv
x1
)
cba
)
)
)
)
)
⟶
wceq
chmo
(
cmpt
(
λ x1 .
cnv
)
(
λ x1 .
crab
(
λ x2 .
wceq
(
cfv
(
cv
x2
)
(
co
(
cv
x1
)
(
cv
x1
)
caj
)
)
(
cv
x2
)
)
(
λ x2 .
cdm
(
co
(
cv
x1
)
(
cv
x1
)
caj
)
)
)
)
⟶
wceq
ccphlo
(
cin
cnv
(
coprab
(
λ x1 x2 x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wceq
(
co
(
co
(
cfv
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x1
)
)
(
cv
x3
)
)
c2
cexp
)
(
co
(
cfv
(
co
(
cv
x4
)
(
co
(
cneg
c1
)
(
cv
x5
)
(
cv
x2
)
)
(
cv
x1
)
)
(
cv
x3
)
)
c2
cexp
)
caddc
)
(
co
c2
(
co
(
co
(
cfv
(
cv
x4
)
(
cv
x3
)
)
c2
cexp
)
(
co
(
cfv
(
cv
x5
)
(
cv
x3
)
)
c2
cexp
)
caddc
)
cmul
)
)
(
λ x5 .
crn
(
cv
x1
)
)
)
(
λ x4 .
crn
(
cv
x1
)
)
)
)
)
⟶
wceq
ccbn
(
crab
(
λ x1 .
wcel
(
cfv
(
cv
x1
)
cims
)
(
cfv
(
cfv
(
cv
x1
)
cba
)
cms
)
)
(
λ x1 .
cnv
)
)
⟶
wceq
chlo
(
cin
ccbn
ccphlo
)
⟶
wceq
cno
(
cmpt
(
λ x1 .
cdm
(
cdm
csp
)
)
(
λ x1 .
cfv
(
co
(
cv
x1
)
(
cv
x1
)
csp
)
csqrt
)
)
⟶
wceq
chil
(
cfv
(
cop
(
cop
cva
csm
)
cno
)
cba
)
⟶
wceq
c0v
(
cfv
(
cop
(
cop
cva
csm
)
cno
)
cn0v
)
⟶
wceq
cmv
(
cmpt2
(
λ x1 x2 .
chil
)
(
λ x1 x2 .
chil
)
(
λ x1 x2 .
co
(
cv
x1
)
(
co
(
cneg
c1
)
(
cv
x2
)
csm
)
cva
)
)
⟶
wceq
chli
(
copab
(
λ x1 x2 .
wa
(
wa
(
wf
cn
chil
(
cv
x1
)
)
(
wcel
(
cv
x2
)
chil
)
)
(
wral
(
λ x3 .
wrex
(
λ x4 .
wral
(
λ x5 .
wbr
(
cfv
(
co
(
cfv
(
cv
x5
)
(
cv
x1
)
)
(
cv
x2
)
cmv
)
cno
)
(
cv
x3
)
clt
)
(
λ x5 .
cfv
(
cv
x4
)
cuz
)
)
(
λ x4 .
cn
)
)
(
λ x3 .
crp
)
)
)
)
⟶
wceq
ccau
(
crab
(
λ x1 .
wral
(
λ x2 .
wrex
(
λ x3 .
wral
(
λ x4 .
wbr
(
cfv
(
co
(
cfv
(
cv
x3
)
(
cv
x1
)
)
(
cfv
(
cv
x4
)
(
cv
x1
)
)
cmv
)
cno
)
(
cv
x2
)
clt
)
(
λ x4 .
cfv
(
cv
x3
)
cuz
)
)
(
λ x3 .
cn
)
)
(
λ x2 .
crp
)
)
(
λ x1 .
co
chil
cn
cmap
)
)
⟶
wcel
chil
cvv
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_dip__df_ssp__df_lno__df_nmoo__df_blo__df_0o__df_aj__df_hmo__df_ph__df_cbn__df_hlo__df_hnorm__df_hba__df_h0v__df_hvsub__df_hlim__df_hcau__ax_hilex
proof
PUV1k..
Megalodon
-
proofgold address
TMMwN..
creator
36224
PrCmT..
/
53926..
owner
36224
PrCmT..
/
53926..
term root
ab248..