Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
clo
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wceq
(
cfv
(
co
(
co
(
cv
x2
)
(
cv
x3
)
csm
)
(
cv
x4
)
cva
)
(
cv
x1
)
)
(
co
(
co
(
cv
x2
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
csm
)
(
cfv
(
cv
x4
)
(
cv
x1
)
)
cva
)
)
(
λ x4 .
chil
)
)
(
λ x3 .
chil
)
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
chil
chil
cmap
)
)
⟶
wceq
cbo
(
crab
(
λ x1 .
wbr
(
cfv
(
cv
x1
)
cnop
)
cpnf
clt
)
(
λ x1 .
clo
)
)
⟶
wceq
cuo
(
cab
(
λ x1 .
wa
(
wfo
chil
chil
(
cv
x1
)
)
(
wral
(
λ x2 .
wral
(
λ x3 .
wceq
(
co
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
csp
)
(
co
(
cv
x2
)
(
cv
x3
)
csp
)
)
(
λ x3 .
chil
)
)
(
λ x2 .
chil
)
)
)
)
⟶
wceq
cho
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wceq
(
co
(
cv
x2
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
csp
)
(
co
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cv
x3
)
csp
)
)
(
λ x3 .
chil
)
)
(
λ x2 .
chil
)
)
(
λ x1 .
co
chil
chil
cmap
)
)
⟶
wceq
cnmf
(
cmpt
(
λ x1 .
co
cc
chil
cmap
)
(
λ x1 .
csup
(
cab
(
λ x2 .
wrex
(
λ x3 .
wa
(
wbr
(
cfv
(
cv
x3
)
cno
)
c1
cle
)
(
wceq
(
cv
x2
)
(
cfv
(
cfv
(
cv
x3
)
(
cv
x1
)
)
cabs
)
)
)
(
λ x3 .
chil
)
)
)
cxr
clt
)
)
⟶
wceq
cnl
(
cmpt
(
λ x1 .
co
cc
chil
cmap
)
(
λ x1 .
cima
(
ccnv
(
cv
x1
)
)
(
csn
cc0
)
)
)
⟶
wceq
ccnfn
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wrex
(
λ x4 .
wral
(
λ x5 .
wbr
(
cfv
(
co
(
cv
x5
)
(
cv
x2
)
cmv
)
cno
)
(
cv
x4
)
clt
⟶
wbr
(
cfv
(
co
(
cfv
(
cv
x5
)
(
cv
x1
)
)
(
cfv
(
cv
x2
)
(
cv
x1
)
)
cmin
)
cabs
)
(
cv
x3
)
clt
)
(
λ x5 .
chil
)
)
(
λ x4 .
crp
)
)
(
λ x3 .
crp
)
)
(
λ x2 .
chil
)
)
(
λ x1 .
co
cc
chil
cmap
)
)
⟶
wceq
clf
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wceq
(
cfv
(
co
(
co
(
cv
x2
)
(
cv
x3
)
csm
)
(
cv
x4
)
cva
)
(
cv
x1
)
)
(
co
(
co
(
cv
x2
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
cmul
)
(
cfv
(
cv
x4
)
(
cv
x1
)
)
caddc
)
)
(
λ x4 .
chil
)
)
(
λ x3 .
chil
)
)
(
λ x2 .
cc
)
)
(
λ x1 .
co
cc
chil
cmap
)
)
⟶
wceq
cado
(
copab
(
λ x1 x2 .
w3a
(
wf
chil
chil
(
cv
x1
)
)
(
wf
chil
chil
(
cv
x2
)
)
(
wral
(
λ x3 .
wral
(
λ x4 .
wceq
(
co
(
cfv
(
cv
x3
)
(
cv
x1
)
)
(
cv
x4
)
csp
)
(
co
(
cv
x3
)
(
cfv
(
cv
x4
)
(
cv
x2
)
)
csp
)
)
(
λ x4 .
chil
)
)
(
λ x3 .
chil
)
)
)
)
⟶
wceq
cbr
(
cmpt
(
λ x1 .
chil
)
(
λ x1 .
cmpt
(
λ x2 .
chil
)
(
λ x2 .
co
(
cv
x2
)
(
cv
x1
)
csp
)
)
)
⟶
wceq
ck
(
cmpt2
(
λ x1 x2 .
chil
)
(
λ x1 x2 .
chil
)
(
λ x1 x2 .
cmpt
(
λ x3 .
chil
)
(
λ x3 .
co
(
co
(
cv
x3
)
(
cv
x2
)
csp
)
(
cv
x1
)
csm
)
)
)
⟶
wceq
cleo
(
copab
(
λ x1 x2 .
wa
(
wcel
(
co
(
cv
x2
)
(
cv
x1
)
chod
)
cho
)
(
wral
(
λ x3 .
wbr
cc0
(
co
(
cfv
(
cv
x3
)
(
co
(
cv
x2
)
(
cv
x1
)
chod
)
)
(
cv
x3
)
csp
)
cle
)
(
λ x3 .
chil
)
)
)
)
⟶
wceq
cei
(
cmpt
(
λ x1 .
co
chil
chil
cmap
)
(
λ x1 .
crab
(
λ x2 .
wrex
(
λ x3 .
wceq
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
co
(
cv
x3
)
(
cv
x2
)
csm
)
)
(
λ x3 .
cc
)
)
(
λ x2 .
cdif
chil
c0h
)
)
)
⟶
wceq
cel
(
cmpt
(
λ x1 .
co
chil
chil
cmap
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
cei
)
(
λ x2 .
co
(
co
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cv
x2
)
csp
)
(
co
(
cfv
(
cv
x2
)
cno
)
c2
cexp
)
cdiv
)
)
)
⟶
wceq
cspc
(
cmpt
(
λ x1 .
co
chil
chil
cmap
)
(
λ x1 .
crab
(
λ x2 .
wn
(
wf1
chil
chil
(
co
(
cv
x1
)
(
co
(
cv
x2
)
(
cres
cid
chil
)
chot
)
chod
)
)
)
(
λ x2 .
cc
)
)
)
⟶
wceq
cst
(
crab
(
λ x1 .
wa
(
wceq
(
cfv
chil
(
cv
x1
)
)
c1
)
(
wral
(
λ x2 .
wral
(
λ x3 .
wss
(
cv
x2
)
(
cfv
(
cv
x3
)
cort
)
⟶
wceq
(
cfv
(
co
(
cv
x2
)
(
cv
x3
)
chj
)
(
cv
x1
)
)
(
co
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
caddc
)
)
(
λ x3 .
cch
)
)
(
λ x2 .
cch
)
)
)
(
λ x1 .
co
(
co
cc0
c1
cicc
)
cch
cmap
)
)
⟶
wceq
chst
(
crab
(
λ x1 .
wa
(
wceq
(
cfv
(
cfv
chil
(
cv
x1
)
)
cno
)
c1
)
(
wral
(
λ x2 .
wral
(
λ x3 .
wss
(
cv
x2
)
(
cfv
(
cv
x3
)
cort
)
⟶
wa
(
wceq
(
co
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
csp
)
cc0
)
(
wceq
(
cfv
(
co
(
cv
x2
)
(
cv
x3
)
chj
)
(
cv
x1
)
)
(
co
(
cfv
(
cv
x2
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
cva
)
)
)
(
λ x3 .
cch
)
)
(
λ x2 .
cch
)
)
)
(
λ x1 .
co
chil
cch
cmap
)
)
⟶
wceq
ccv
(
copab
(
λ x1 x2 .
wa
(
wa
(
wcel
(
cv
x1
)
cch
)
(
wcel
(
cv
x2
)
cch
)
)
(
wa
(
wpss
(
cv
x1
)
(
cv
x2
)
)
(
wn
(
wrex
(
λ x3 .
wa
(
wpss
(
cv
x1
)
(
cv
x3
)
)
(
wpss
(
cv
x3
)
(
cv
x2
)
)
)
(
λ x3 .
cch
)
)
)
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_lnop__df_bdop__df_unop__df_hmop__df_nmfn__df_nlfn__df_cnfn__df_lnfn__df_adjh__df_bra__df_kb__df_leop__df_eigvec__df_eigval__df_spec__df_st__df_hst__df_cv
proof
PUV1k..
Megalodon
-
proofgold address
TMVnK..
creator
36224
PrCmT..
/
ece78..
owner
36224
PrCmT..
/
ece78..
term root
3eb9e..