Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
cminmar1
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmat
)
cbs
)
(
λ x3 .
cmpt2
(
λ x4 x5 .
cv
x1
)
(
λ x4 x5 .
cv
x1
)
(
λ x4 x5 .
cmpt2
(
λ x6 x7 .
cv
x1
)
(
λ x6 x7 .
cv
x1
)
(
λ x6 x7 .
cif
(
wceq
(
cv
x6
)
(
cv
x4
)
)
(
cif
(
wceq
(
cv
x7
)
(
cv
x5
)
)
(
cfv
(
cv
x2
)
cur
)
(
cfv
(
cv
x2
)
c0g
)
)
(
co
(
cv
x6
)
(
cv
x7
)
(
cv
x3
)
)
)
)
)
)
)
⟶
wceq
ccpmat
(
cmpt2
(
λ x1 x2 .
cfn
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
crab
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wral
(
λ x6 .
wceq
(
cfv
(
cv
x6
)
(
cfv
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x3
)
)
cco1
)
)
(
cfv
(
cv
x2
)
c0g
)
)
(
λ x6 .
cn
)
)
(
λ x5 .
cv
x1
)
)
(
λ x4 .
cv
x1
)
)
(
λ x3 .
cfv
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
cpl1
)
cmat
)
cbs
)
)
)
⟶
wceq
cmat2pmat
(
cmpt2
(
λ x1 x2 .
cfn
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmat
)
cbs
)
(
λ x3 .
cmpt2
(
λ x4 x5 .
cv
x1
)
(
λ x4 x5 .
cv
x1
)
(
λ x4 x5 .
cfv
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x3
)
)
(
cfv
(
cfv
(
cv
x2
)
cpl1
)
cascl
)
)
)
)
)
⟶
wceq
ccpmat2mat
(
cmpt2
(
λ x1 x2 .
cfn
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
co
(
cv
x1
)
(
cv
x2
)
ccpmat
)
(
λ x3 .
cmpt2
(
λ x4 x5 .
cv
x1
)
(
λ x4 x5 .
cv
x1
)
(
λ x4 x5 .
cfv
cc0
(
cfv
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x3
)
)
cco1
)
)
)
)
)
⟶
wceq
cdecpmat
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cn0
)
(
λ x1 x2 .
cmpt2
(
λ x3 x4 .
cdm
(
cdm
(
cv
x1
)
)
)
(
λ x3 x4 .
cdm
(
cdm
(
cv
x1
)
)
)
(
λ x3 x4 .
cfv
(
cv
x2
)
(
cfv
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x1
)
)
cco1
)
)
)
)
⟶
wceq
cpm2mp
(
cmpt2
(
λ x1 x2 .
cfn
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cfv
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
cpl1
)
cmat
)
cbs
)
(
λ x3 .
csb
(
co
(
cv
x1
)
(
cv
x2
)
cmat
)
(
λ x4 .
csb
(
cfv
(
cv
x4
)
cpl1
)
(
λ x5 .
co
(
cv
x5
)
(
cmpt
(
λ x6 .
cn0
)
(
λ x6 .
co
(
co
(
cv
x3
)
(
cv
x6
)
cdecpmat
)
(
co
(
cv
x6
)
(
cfv
(
cv
x4
)
cv1
)
(
cfv
(
cfv
(
cv
x5
)
cmgp
)
cmg
)
)
(
cfv
(
cv
x5
)
cvsca
)
)
)
cgsu
)
)
)
)
)
⟶
wceq
cchpmat
(
cmpt2
(
λ x1 x2 .
cfn
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cmpt
(
λ x3 .
cfv
(
co
(
cv
x1
)
(
cv
x2
)
cmat
)
cbs
)
(
λ x3 .
cfv
(
co
(
co
(
cfv
(
cv
x2
)
cv1
)
(
cfv
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
cpl1
)
cmat
)
cur
)
(
cfv
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
cpl1
)
cmat
)
cvsca
)
)
(
cfv
(
cv
x3
)
(
co
(
cv
x1
)
(
cv
x2
)
cmat2pmat
)
)
(
cfv
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
cpl1
)
cmat
)
csg
)
)
(
co
(
cv
x1
)
(
cfv
(
cv
x2
)
cpl1
)
cmdat
)
)
)
)
⟶
wceq
ctop
(
cab
(
λ x1 .
wa
(
wral
(
λ x2 .
wcel
(
cuni
(
cv
x2
)
)
(
cv
x1
)
)
(
λ x2 .
cpw
(
cv
x1
)
)
)
(
wral
(
λ x2 .
wral
(
λ x3 .
wcel
(
cin
(
cv
x2
)
(
cv
x3
)
)
(
cv
x1
)
)
(
λ x3 .
cv
x1
)
)
(
λ x2 .
cv
x1
)
)
)
)
⟶
wceq
ctopon
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wceq
(
cv
x1
)
(
cuni
(
cv
x2
)
)
)
(
λ x2 .
ctop
)
)
)
⟶
wceq
ctps
(
cab
(
λ x1 .
wcel
(
cfv
(
cv
x1
)
ctopn
)
(
cfv
(
cfv
(
cv
x1
)
cbs
)
ctopon
)
)
)
⟶
wceq
ctb
(
cab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wss
(
cin
(
cv
x2
)
(
cv
x3
)
)
(
cuni
(
cin
(
cv
x1
)
(
cpw
(
cin
(
cv
x2
)
(
cv
x3
)
)
)
)
)
)
(
λ x3 .
cv
x1
)
)
(
λ x2 .
cv
x1
)
)
)
⟶
wceq
ccld
(
cmpt
(
λ x1 .
ctop
)
(
λ x1 .
crab
(
λ x2 .
wcel
(
cdif
(
cuni
(
cv
x1
)
)
(
cv
x2
)
)
(
cv
x1
)
)
(
λ x2 .
cpw
(
cuni
(
cv
x1
)
)
)
)
)
⟶
wceq
cnt
(
cmpt
(
λ x1 .
ctop
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cuni
(
cv
x1
)
)
)
(
λ x2 .
cuni
(
cin
(
cv
x1
)
(
cpw
(
cv
x2
)
)
)
)
)
)
⟶
wceq
ccl
(
cmpt
(
λ x1 .
ctop
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cuni
(
cv
x1
)
)
)
(
λ x2 .
cint
(
crab
(
λ x3 .
wss
(
cv
x2
)
(
cv
x3
)
)
(
λ x3 .
cfv
(
cv
x1
)
ccld
)
)
)
)
)
⟶
wceq
cnei
(
cmpt
(
λ x1 .
ctop
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cuni
(
cv
x1
)
)
)
(
λ x2 .
crab
(
λ x3 .
wrex
(
λ x4 .
wa
(
wss
(
cv
x2
)
(
cv
x4
)
)
(
wss
(
cv
x4
)
(
cv
x3
)
)
)
(
λ x4 .
cv
x1
)
)
(
λ x3 .
cpw
(
cuni
(
cv
x1
)
)
)
)
)
)
⟶
wceq
clp
(
cmpt
(
λ x1 .
ctop
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cuni
(
cv
x1
)
)
)
(
λ x2 .
cab
(
λ x3 .
wcel
(
cv
x3
)
(
cfv
(
cdif
(
cv
x2
)
(
csn
(
cv
x3
)
)
)
(
cfv
(
cv
x1
)
ccl
)
)
)
)
)
)
⟶
wceq
cperf
(
crab
(
λ x1 .
wceq
(
cfv
(
cuni
(
cv
x1
)
)
(
cfv
(
cv
x1
)
clp
)
)
(
cuni
(
cv
x1
)
)
)
(
λ x1 .
ctop
)
)
⟶
wceq
ccn
(
cmpt2
(
λ x1 x2 .
ctop
)
(
λ x1 x2 .
ctop
)
(
λ x1 x2 .
crab
(
λ x3 .
wral
(
λ x4 .
wcel
(
cima
(
ccnv
(
cv
x3
)
)
(
cv
x4
)
)
(
cv
x1
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
co
(
cuni
(
cv
x2
)
)
(
cuni
(
cv
x1
)
)
cmap
)
)
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_minmar1__df_cpmat__df_mat2pmat__df_cpmat2mat__df_decpmat__df_pm2mp__df_chpmat__df_top__df_topon__df_topsp__df_bases__df_cld__df_ntr__df_cls__df_nei__df_lp__df_perf__df_cn
proof
PUV1k..
Megalodon
-
proofgold address
TMX5X..
creator
36224
PrCmT..
/
e76b0..
owner
36224
PrCmT..
/
e76b0..
term root
92d11..