Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
wceq
csx
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cfv
(
crn
(
cmpt2
(
λ x3 x4 .
cv
x1
)
(
λ x3 x4 .
cv
x2
)
(
λ x3 x4 .
cxp
(
cv
x3
)
(
cv
x4
)
)
)
)
csigagen
)
)
⟶
wceq
cmeas
(
cmpt
(
λ x1 .
cuni
(
crn
csiga
)
)
(
λ x1 .
cab
(
λ x2 .
w3a
(
wf
(
cv
x1
)
(
co
cc0
cpnf
cicc
)
(
cv
x2
)
)
(
wceq
(
cfv
c0
(
cv
x2
)
)
cc0
)
(
wral
(
λ x3 .
wa
(
wbr
(
cv
x3
)
com
cdom
)
(
wdisj
(
λ x4 .
cv
x3
)
cv
)
⟶
wceq
(
cfv
(
cuni
(
cv
x3
)
)
(
cv
x2
)
)
(
cesum
(
λ x4 .
cv
x3
)
(
λ x4 .
cfv
(
cv
x4
)
(
cv
x2
)
)
)
)
(
λ x3 .
cpw
(
cv
x1
)
)
)
)
)
)
⟶
wceq
cdde
(
cmpt
(
λ x1 .
cpw
cr
)
(
λ x1 .
cif
(
wcel
cc0
(
cv
x1
)
)
c1
cc0
)
)
⟶
wceq
cae
(
copab
(
λ x1 x2 .
wceq
(
cfv
(
cdif
(
cuni
(
cdm
(
cv
x2
)
)
)
(
cv
x1
)
)
(
cv
x2
)
)
cc0
)
)
⟶
wceq
cfae
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cuni
(
crn
cmeas
)
)
(
λ x1 x2 .
copab
(
λ x3 x4 .
wa
(
wa
(
wcel
(
cv
x3
)
(
co
(
cdm
(
cv
x1
)
)
(
cuni
(
cdm
(
cv
x2
)
)
)
cmap
)
)
(
wcel
(
cv
x4
)
(
co
(
cdm
(
cv
x1
)
)
(
cuni
(
cdm
(
cv
x2
)
)
)
cmap
)
)
)
(
wbr
(
crab
(
λ x5 .
wbr
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cfv
(
cv
x5
)
(
cv
x4
)
)
(
cv
x1
)
)
(
λ x5 .
cuni
(
cdm
(
cv
x2
)
)
)
)
(
cv
x2
)
cae
)
)
)
)
⟶
wceq
cmbfm
(
cmpt2
(
λ x1 x2 .
cuni
(
crn
csiga
)
)
(
λ x1 x2 .
cuni
(
crn
csiga
)
)
(
λ 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
)
)
)
⟶
wceq
coms
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cuni
(
cdm
(
cv
x1
)
)
)
)
(
λ x2 .
cinf
(
crn
(
cmpt
(
λ x3 .
crab
(
λ x4 .
wa
(
wss
(
cv
x2
)
(
cuni
(
cv
x4
)
)
)
(
wbr
(
cv
x4
)
com
cdom
)
)
(
λ x4 .
cpw
(
cdm
(
cv
x1
)
)
)
)
(
λ x3 .
cesum
(
λ x4 .
cv
x3
)
(
λ x4 .
cfv
(
cv
x4
)
(
cv
x1
)
)
)
)
)
(
co
cc0
cpnf
cicc
)
clt
)
)
)
⟶
wceq
ccarsg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wceq
(
co
(
cfv
(
cin
(
cv
x3
)
(
cv
x2
)
)
(
cv
x1
)
)
(
cfv
(
cdif
(
cv
x3
)
(
cv
x2
)
)
(
cv
x1
)
)
cxad
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
)
(
λ x3 .
cpw
(
cuni
(
cdm
(
cv
x1
)
)
)
)
)
(
λ x2 .
cpw
(
cuni
(
cdm
(
cv
x1
)
)
)
)
)
)
⟶
wceq
csitg
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cuni
(
crn
cmeas
)
)
(
λ x1 x2 .
cmpt
(
λ x3 .
crab
(
λ x4 .
wa
(
wcel
(
crn
(
cv
x4
)
)
cfn
)
(
wral
(
λ x5 .
wcel
(
cfv
(
cima
(
ccnv
(
cv
x4
)
)
(
csn
(
cv
x5
)
)
)
(
cv
x2
)
)
(
co
cc0
cpnf
cico
)
)
(
λ x5 .
cdif
(
crn
(
cv
x4
)
)
(
csn
(
cfv
(
cv
x1
)
c0g
)
)
)
)
)
(
λ x4 .
co
(
cdm
(
cv
x2
)
)
(
cfv
(
cfv
(
cv
x1
)
ctopn
)
csigagen
)
cmbfm
)
)
(
λ x3 .
co
(
cv
x1
)
(
cmpt
(
λ x4 .
cdif
(
crn
(
cv
x3
)
)
(
csn
(
cfv
(
cv
x1
)
c0g
)
)
)
(
λ x4 .
co
(
cfv
(
cfv
(
cima
(
ccnv
(
cv
x3
)
)
(
csn
(
cv
x4
)
)
)
(
cv
x2
)
)
(
cfv
(
cfv
(
cv
x1
)
csca
)
crrh
)
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cvsca
)
)
)
cgsu
)
)
)
⟶
wceq
csitm
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cuni
(
crn
cmeas
)
)
(
λ x1 x2 .
cmpt2
(
λ x3 x4 .
cdm
(
co
(
cv
x1
)
(
cv
x2
)
csitg
)
)
(
λ x3 x4 .
cdm
(
co
(
cv
x1
)
(
cv
x2
)
csitg
)
)
(
λ x3 x4 .
cfv
(
co
(
cv
x3
)
(
cv
x4
)
(
cof
(
cfv
(
cv
x1
)
cds
)
)
)
(
co
(
co
cxrs
(
co
cc0
cpnf
cicc
)
cress
)
(
cv
x2
)
csitg
)
)
)
)
⟶
wceq
citgm
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cuni
(
crn
cmeas
)
)
(
λ x1 x2 .
cfv
(
co
(
cv
x1
)
(
cv
x2
)
csitg
)
(
co
(
cfv
(
co
(
cv
x1
)
(
cv
x2
)
csitm
)
cmetu
)
(
cfv
(
cv
x1
)
cuss
)
ccnext
)
)
)
⟶
wceq
csseq
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cun
(
cv
x1
)
(
ccom
clsw
(
cseq
(
cmpt2
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
cvv
)
(
λ x3 x4 .
co
(
cv
x3
)
(
cs1
(
cfv
(
cv
x3
)
(
cv
x2
)
)
)
cconcat
)
)
(
cxp
cn0
(
csn
(
co
(
cv
x1
)
(
cs1
(
cfv
(
cv
x1
)
(
cv
x2
)
)
)
cconcat
)
)
)
(
cfv
(
cv
x1
)
chash
)
)
)
)
)
⟶
wceq
cfib
(
co
(
cs2
cc0
c1
)
(
cmpt
(
λ x1 .
cin
(
cword
cn0
)
(
cima
(
ccnv
chash
)
(
cfv
c2
cuz
)
)
)
(
λ x1 .
co
(
cfv
(
co
(
cfv
(
cv
x1
)
chash
)
c2
cmin
)
(
cv
x1
)
)
(
cfv
(
co
(
cfv
(
cv
x1
)
chash
)
c1
cmin
)
(
cv
x1
)
)
caddc
)
)
csseq
)
⟶
wceq
cprb
(
crab
(
λ x1 .
wceq
(
cfv
(
cuni
(
cdm
(
cv
x1
)
)
)
(
cv
x1
)
)
c1
)
(
λ x1 .
cuni
(
crn
cmeas
)
)
)
⟶
wceq
ccprob
(
cmpt
(
λ x1 .
cprb
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cdm
(
cv
x1
)
)
(
λ x2 x3 .
cdm
(
cv
x1
)
)
(
λ x2 x3 .
co
(
cfv
(
cin
(
cv
x2
)
(
cv
x3
)
)
(
cv
x1
)
)
(
cfv
(
cv
x3
)
(
cv
x1
)
)
cdiv
)
)
)
⟶
wceq
crrv
(
cmpt
(
λ x1 .
cprb
)
(
λ x1 .
co
(
cdm
(
cv
x1
)
)
cbrsiga
cmbfm
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
corvc
x1
)
(
cmpt2
(
λ x2 x3 .
cab
(
λ x4 .
wfun
(
cv
x4
)
)
)
(
λ x2 x3 .
cvv
)
(
λ x2 x3 .
cima
(
ccnv
(
cv
x2
)
)
(
cab
(
λ x4 .
wbr
(
cv
x4
)
(
cv
x3
)
x1
)
)
)
)
)
⟶
wceq
crepr
(
cmpt
(
λ x1 .
cn0
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cpw
cn
)
(
λ x2 x3 .
cz
)
(
λ x2 x3 .
crab
(
λ x4 .
wceq
(
csu
(
co
cc0
(
cv
x1
)
cfzo
)
(
λ x5 .
cfv
(
cv
x5
)
(
cv
x4
)
)
)
(
cv
x3
)
)
(
λ x4 .
co
(
cv
x2
)
(
co
cc0
(
cv
x1
)
cfzo
)
cmap
)
)
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
148ed..
theory
SetMM
stx
ebbdd..
address
TMPK9..