Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ 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
as obj
-
as prop
4b79d..
theory
SetMM
stx
ebbdd..
address
TMdGt..