Search for blocks/addresses/...
Proofgold Proposition
∀ x0 : ο .
(
wceq
clmat
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
co
c1
(
cfv
(
cv
x1
)
chash
)
cfz
)
(
λ x2 x3 .
co
c1
(
cfv
(
cfv
cc0
(
cv
x1
)
)
chash
)
cfz
)
(
λ x2 x3 .
cfv
(
co
(
cv
x3
)
c1
cmin
)
(
cfv
(
co
(
cv
x2
)
c1
cmin
)
(
cv
x1
)
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
ccref
x1
)
(
crab
(
λ x2 .
wral
(
λ x3 .
wceq
(
cuni
(
cv
x2
)
)
(
cuni
(
cv
x3
)
)
⟶
wrex
(
λ x4 .
wbr
(
cv
x4
)
(
cv
x3
)
cref
)
(
λ x4 .
cin
(
cpw
(
cv
x2
)
)
x1
)
)
(
λ x3 .
cpw
(
cv
x2
)
)
)
(
λ x2 .
ctop
)
)
)
⟶
wceq
cldlf
(
ccref
(
cab
(
λ x1 .
wbr
(
cv
x1
)
com
cdom
)
)
)
⟶
wceq
cpcmp
(
cab
(
λ x1 .
wcel
(
cv
x1
)
(
ccref
(
cfv
(
cv
x1
)
clocfin
)
)
)
)
⟶
wceq
cmetid
(
cmpt
(
λ x1 .
cuni
(
crn
cpsmet
)
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
cdm
(
cdm
(
cv
x1
)
)
)
)
(
wcel
(
cv
x3
)
(
cdm
(
cdm
(
cv
x1
)
)
)
)
)
(
wceq
(
co
(
cv
x2
)
(
cv
x3
)
(
cv
x1
)
)
cc0
)
)
)
)
⟶
wceq
cpstm
(
cmpt
(
λ x1 .
cuni
(
crn
cpsmet
)
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cqs
(
cdm
(
cdm
(
cv
x1
)
)
)
(
cfv
(
cv
x1
)
cmetid
)
)
(
λ x2 x3 .
cqs
(
cdm
(
cdm
(
cv
x1
)
)
)
(
cfv
(
cv
x1
)
cmetid
)
)
(
λ x2 x3 .
cuni
(
cab
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wceq
(
cv
x4
)
(
co
(
cv
x5
)
(
cv
x6
)
(
cv
x1
)
)
)
(
λ x6 .
cv
x3
)
)
(
λ x5 .
cv
x2
)
)
)
)
)
)
⟶
wceq
chcmp
(
copab
(
λ x1 x2 .
w3a
(
wa
(
wcel
(
cv
x1
)
(
cuni
(
crn
cust
)
)
)
(
wcel
(
cv
x2
)
ccusp
)
)
(
wceq
(
co
(
cfv
(
cv
x2
)
cuss
)
(
cdm
(
cuni
(
cv
x1
)
)
)
crest
)
(
cv
x1
)
)
(
wceq
(
cfv
(
cdm
(
cuni
(
cv
x1
)
)
)
(
cfv
(
cfv
(
cv
x2
)
ctopn
)
ccl
)
)
(
cfv
(
cv
x2
)
cbs
)
)
)
)
⟶
wceq
cqqh
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crn
(
cmpt2
(
λ x2 x3 .
cz
)
(
λ x2 x3 .
cima
(
ccnv
(
cfv
(
cv
x1
)
czrh
)
)
(
cfv
(
cv
x1
)
cui
)
)
(
λ x2 x3 .
cop
(
co
(
cv
x2
)
(
cv
x3
)
cdiv
)
(
co
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
czrh
)
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
czrh
)
)
(
cfv
(
cv
x1
)
cdvr
)
)
)
)
)
)
⟶
wceq
crrh
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cfv
(
cfv
(
cv
x1
)
cqqh
)
(
co
(
cfv
(
crn
cioo
)
ctg
)
(
cfv
(
cv
x1
)
ctopn
)
ccnext
)
)
)
⟶
wceq
crrext
(
crab
(
λ x1 .
wa
(
wa
(
wcel
(
cfv
(
cv
x1
)
czlm
)
cnlm
)
(
wceq
(
cfv
(
cv
x1
)
cchr
)
cc0
)
)
(
wa
(
wcel
(
cv
x1
)
ccusp
)
(
wceq
(
cfv
(
cv
x1
)
cuss
)
(
cfv
(
cres
(
cfv
(
cv
x1
)
cds
)
(
cxp
(
cfv
(
cv
x1
)
cbs
)
(
cfv
(
cv
x1
)
cbs
)
)
)
cmetu
)
)
)
)
(
λ x1 .
cin
cnrg
cdr
)
)
⟶
wceq
cxrh
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cxr
)
(
λ x2 .
cif
(
wcel
(
cv
x2
)
cr
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
crrh
)
)
(
cif
(
wceq
(
cv
x2
)
cpnf
)
(
cfv
(
cima
(
cfv
(
cv
x1
)
crrh
)
cr
)
(
cfv
(
cv
x1
)
club
)
)
(
cfv
(
cima
(
cfv
(
cv
x1
)
crrh
)
cr
)
(
cfv
(
cv
x1
)
cglb
)
)
)
)
)
)
⟶
wceq
cmntop
(
copab
(
λ x1 x2 .
wa
(
wcel
(
cv
x1
)
cn0
)
(
w3a
(
wcel
(
cv
x2
)
c2ndc
)
(
wcel
(
cv
x2
)
cha
)
(
wcel
(
cv
x2
)
(
clly
(
cec
(
cfv
(
cfv
(
cv
x1
)
cehl
)
ctopn
)
chmph
)
)
)
)
)
)
⟶
wceq
cind
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cv
x1
)
)
(
λ x2 .
cmpt
(
λ x3 .
cv
x1
)
(
λ x3 .
cif
(
wcel
(
cv
x3
)
(
cv
x2
)
)
c1
cc0
)
)
)
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
wceq
(
cesum
x1
x2
)
(
cuni
(
co
(
co
cxrs
(
co
cc0
cpnf
cicc
)
cress
)
(
cmpt
x1
x2
)
ctsu
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cofc
x1
)
(
cmpt2
(
λ x2 x3 .
cvv
)
(
λ x2 x3 .
cvv
)
(
λ x2 x3 .
cmpt
(
λ x4 .
cdm
(
cv
x2
)
)
(
λ x4 .
co
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cv
x3
)
x1
)
)
)
)
⟶
wceq
csiga
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cab
(
λ x2 .
wa
(
wss
(
cv
x2
)
(
cpw
(
cv
x1
)
)
)
(
w3a
(
wcel
(
cv
x1
)
(
cv
x2
)
)
(
wral
(
λ x3 .
wcel
(
cdif
(
cv
x1
)
(
cv
x3
)
)
(
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
(
wral
(
λ x3 .
wbr
(
cv
x3
)
com
cdom
⟶
wcel
(
cuni
(
cv
x3
)
)
(
cv
x2
)
)
(
λ x3 .
cpw
(
cv
x2
)
)
)
)
)
)
)
⟶
wceq
csigagen
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cint
(
crab
(
λ x2 .
wss
(
cv
x1
)
(
cv
x2
)
)
(
λ x2 .
cfv
(
cuni
(
cv
x1
)
)
csiga
)
)
)
)
⟶
wceq
cbrsiga
(
cfv
(
cfv
(
crn
cioo
)
ctg
)
csigagen
)
⟶
x0
)
⟶
x0
type
prop
theory
SetMM
name
df_lmat__df_cref__df_ldlf__df_pcmp__df_metid__df_pstm__df_hcmp__df_qqh__df_rrh__df_rrext__df_xrh__df_mntop__df_ind__df_esum__df_ofc__df_siga__df_sigagen__df_brsiga
proof
PUV1k..
Megalodon
-
proofgold address
TMJff..
creator
36224
PrCmT..
/
ab70f..
owner
36224
PrCmT..
/
ab70f..
term root
5461c..