Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
wceq
cops
(
crab
(
λ x1 .
wa
(
wa
(
wcel
(
cfv
(
cv
x1
)
cbs
)
(
cdm
(
cfv
(
cv
x1
)
club
)
)
)
(
wcel
(
cfv
(
cv
x1
)
cbs
)
(
cdm
(
cfv
(
cv
x1
)
cglb
)
)
)
)
(
wex
(
λ x2 .
wa
(
wceq
(
cv
x2
)
(
cfv
(
cv
x1
)
coc
)
)
(
wral
(
λ x3 .
wral
(
λ x4 .
w3a
(
w3a
(
wcel
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wceq
(
cfv
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cv
x2
)
)
(
cv
x3
)
)
(
wbr
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cple
)
⟶
wbr
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cple
)
)
)
(
wceq
(
co
(
cv
x3
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cp1
)
)
(
wceq
(
co
(
cv
x3
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cmee
)
)
(
cfv
(
cv
x1
)
cp0
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
(
λ x1 .
cpo
)
)
⟶
wceq
ccmtN
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
w3a
(
wcel
(
cv
x2
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wcel
(
cv
x3
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wceq
(
cv
x2
)
(
co
(
co
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cmee
)
)
(
co
(
cv
x2
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x1
)
coc
)
)
(
cfv
(
cv
x1
)
cmee
)
)
(
cfv
(
cv
x1
)
cjn
)
)
)
)
)
)
⟶
wceq
col
(
cin
clat
cops
)
⟶
wceq
coml
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wbr
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cple
)
⟶
wceq
(
cv
x3
)
(
co
(
cv
x2
)
(
co
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coc
)
)
(
cfv
(
cv
x1
)
cmee
)
)
(
cfv
(
cv
x1
)
cjn
)
)
)
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x1 .
col
)
)
⟶
wceq
ccvr
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
w3a
(
wa
(
wcel
(
cv
x2
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wcel
(
cv
x3
)
(
cfv
(
cv
x1
)
cbs
)
)
)
(
wbr
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cplt
)
)
(
wn
(
wrex
(
λ x4 .
wa
(
wbr
(
cv
x2
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cplt
)
)
(
wbr
(
cv
x4
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cplt
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
)
⟶
wceq
catm
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cfv
(
cv
x1
)
cp0
)
(
cv
x2
)
(
cfv
(
cv
x1
)
ccvr
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
cal
(
crab
(
λ x1 .
wa
(
wcel
(
cfv
(
cv
x1
)
cbs
)
(
cdm
(
cfv
(
cv
x1
)
cglb
)
)
)
(
wral
(
λ x2 .
wne
(
cv
x2
)
(
cfv
(
cv
x1
)
cp0
)
⟶
wrex
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cple
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
(
λ x1 .
clat
)
)
⟶
wceq
clc
(
crab
(
λ x1 .
wral
(
λ x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wa
(
wn
(
wbr
(
cv
x2
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cple
)
)
)
(
wbr
(
cv
x2
)
(
co
(
cv
x4
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cple
)
)
⟶
wbr
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cple
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
(
λ x2 .
cfv
(
cv
x1
)
catm
)
)
(
λ x1 .
cal
)
)
⟶
wceq
chlt
(
crab
(
λ x1 .
wa
(
wral
(
λ x2 .
wral
(
λ x3 .
wne
(
cv
x2
)
(
cv
x3
)
⟶
wrex
(
λ x4 .
w3a
(
wne
(
cv
x4
)
(
cv
x2
)
)
(
wne
(
cv
x4
)
(
cv
x3
)
)
(
wbr
(
cv
x4
)
(
co
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cple
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
catm
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
(
λ x2 .
cfv
(
cv
x1
)
catm
)
)
(
wrex
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wa
(
wa
(
wbr
(
cfv
(
cv
x1
)
cp0
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cplt
)
)
(
wbr
(
cv
x2
)
(
cv
x3
)
(
cfv
(
cv
x1
)
cplt
)
)
)
(
wa
(
wbr
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cplt
)
)
(
wbr
(
cv
x4
)
(
cfv
(
cv
x1
)
cp1
)
(
cfv
(
cv
x1
)
cplt
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
(
λ x1 .
cin
(
cin
coml
ccla
)
clc
)
)
⟶
wceq
clln
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wrex
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
ccvr
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
clpl
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wrex
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
ccvr
)
)
(
λ x3 .
cfv
(
cv
x1
)
clln
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
clvol
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wrex
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
ccvr
)
)
(
λ x3 .
cfv
(
cv
x1
)
clpl
)
)
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
clines
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wa
(
wne
(
cv
x3
)
(
cv
x4
)
)
(
wceq
(
cv
x2
)
(
crab
(
λ x5 .
wbr
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cple
)
)
(
λ x5 .
cfv
(
cv
x1
)
catm
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
catm
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
)
)
⟶
wceq
cpointsN
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cab
(
λ x2 .
wrex
(
λ x3 .
wceq
(
cv
x2
)
(
csn
(
cv
x3
)
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
)
)
⟶
wceq
cpsubsp
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cab
(
λ x2 .
wa
(
wss
(
cv
x2
)
(
cfv
(
cv
x1
)
catm
)
)
(
wral
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wbr
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cple
)
⟶
wcel
(
cv
x5
)
(
cv
x2
)
)
(
λ x5 .
cfv
(
cv
x1
)
catm
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
)
)
)
⟶
wceq
cpmap
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 .
crab
(
λ x3 .
wbr
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cple
)
)
(
λ x3 .
cfv
(
cv
x1
)
catm
)
)
)
)
⟶
wceq
cpadd
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cpw
(
cfv
(
cv
x1
)
catm
)
)
(
λ x2 x3 .
cpw
(
cfv
(
cv
x1
)
catm
)
)
(
λ x2 x3 .
cun
(
cun
(
cv
x2
)
(
cv
x3
)
)
(
crab
(
λ x4 .
wrex
(
λ x5 .
wrex
(
λ x6 .
wbr
(
cv
x4
)
(
co
(
cv
x5
)
(
cv
x6
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cfv
(
cv
x1
)
cple
)
)
(
λ x6 .
cv
x3
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cfv
(
cv
x1
)
catm
)
)
)
)
)
⟶
wceq
cpclN
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cpw
(
cfv
(
cv
x1
)
catm
)
)
(
λ x2 .
cint
(
crab
(
λ x3 .
wss
(
cv
x2
)
(
cv
x3
)
)
(
λ x3 .
cfv
(
cv
x1
)
cpsubsp
)
)
)
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
2cafa..
theory
SetMM
stx
ebbdd..
address
TMXpq..