Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
wceq
crag
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wa
(
wceq
(
cfv
(
cv
x2
)
chash
)
c3
)
(
wceq
(
co
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cds
)
)
(
co
(
cfv
cc0
(
cv
x2
)
)
(
cfv
(
cfv
c2
(
cv
x2
)
)
(
cfv
(
cfv
c1
(
cv
x2
)
)
(
cfv
(
cv
x1
)
cmir
)
)
)
(
cfv
(
cv
x1
)
cds
)
)
)
)
(
λ x2 .
cword
(
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
cperpg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
crn
(
cfv
(
cv
x1
)
clng
)
)
)
(
wcel
(
cv
x3
)
(
crn
(
cfv
(
cv
x1
)
clng
)
)
)
)
(
wrex
(
λ x4 .
wral
(
λ x5 .
wral
(
λ x6 .
wcel
(
cs3
(
cv
x5
)
(
cv
x4
)
(
cv
x6
)
)
(
cfv
(
cv
x1
)
crag
)
)
(
λ x6 .
cv
x3
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cin
(
cv
x2
)
(
cv
x3
)
)
)
)
)
)
⟶
wceq
chpg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
crn
(
cfv
(
cv
x1
)
clng
)
)
(
λ x2 .
copab
(
λ x3 x4 .
wsbc
(
λ x5 .
wsbc
(
λ x6 .
wrex
(
λ x7 .
wa
(
wa
(
wa
(
wcel
(
cv
x3
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
(
wcel
(
cv
x7
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
)
(
wrex
(
λ x8 .
wcel
(
cv
x8
)
(
co
(
cv
x3
)
(
cv
x7
)
(
cv
x6
)
)
)
(
λ x8 .
cv
x2
)
)
)
(
wa
(
wa
(
wcel
(
cv
x4
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
(
wcel
(
cv
x7
)
(
cdif
(
cv
x5
)
(
cv
x2
)
)
)
)
(
wrex
(
λ x8 .
wcel
(
cv
x8
)
(
co
(
cv
x4
)
(
cv
x7
)
(
cv
x6
)
)
)
(
λ x8 .
cv
x2
)
)
)
)
(
λ x7 .
cv
x5
)
)
(
cfv
(
cv
x1
)
citv
)
)
(
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
cmid
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
crio
(
λ x4 .
wceq
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x1
)
cmir
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
clmi
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
crn
(
cfv
(
cv
x1
)
clng
)
)
(
λ x2 .
cmpt
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 .
crio
(
λ x4 .
wa
(
wcel
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cmid
)
)
(
cv
x2
)
)
(
wo
(
wbr
(
cv
x2
)
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
clng
)
)
(
cfv
(
cv
x1
)
cperpg
)
)
(
wceq
(
cv
x3
)
(
cv
x4
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
ccgra
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wa
(
wa
(
wcel
(
cv
x2
)
(
co
(
cv
x4
)
(
co
cc0
c3
cfzo
)
cmap
)
)
(
wcel
(
cv
x3
)
(
co
(
cv
x4
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wrex
(
λ x6 .
wrex
(
λ x7 .
w3a
(
wbr
(
cv
x2
)
(
cs3
(
cv
x6
)
(
cfv
c1
(
cv
x3
)
)
(
cv
x7
)
)
(
cfv
(
cv
x1
)
ccgrg
)
)
(
wbr
(
cv
x6
)
(
cfv
cc0
(
cv
x3
)
)
(
cfv
(
cfv
c1
(
cv
x3
)
)
(
cv
x5
)
)
)
(
wbr
(
cv
x7
)
(
cfv
c2
(
cv
x3
)
)
(
cfv
(
cfv
c1
(
cv
x3
)
)
(
cv
x5
)
)
)
)
(
λ x7 .
cv
x4
)
)
(
λ x6 .
cv
x4
)
)
)
(
cfv
(
cv
x1
)
chlg
)
)
(
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
cinag
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wcel
(
cv
x3
)
(
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wa
(
w3a
(
wne
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
)
(
wne
(
cfv
c2
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
)
(
wne
(
cv
x2
)
(
cfv
c1
(
cv
x3
)
)
)
)
(
wrex
(
λ x4 .
wa
(
wcel
(
cv
x4
)
(
co
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c2
(
cv
x3
)
)
(
cfv
(
cv
x1
)
citv
)
)
)
(
wo
(
wceq
(
cv
x4
)
(
cfv
c1
(
cv
x3
)
)
)
(
wbr
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cfv
c1
(
cv
x3
)
)
(
cfv
(
cv
x1
)
chlg
)
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
)
⟶
wceq
cleag
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
wa
(
wa
(
wcel
(
cv
x2
)
(
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
(
wcel
(
cv
x3
)
(
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
(
wrex
(
λ x4 .
wa
(
wbr
(
cv
x4
)
(
cs3
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
(
cfv
c2
(
cv
x3
)
)
)
(
cfv
(
cv
x1
)
cinag
)
)
(
wbr
(
cs3
(
cfv
cc0
(
cv
x2
)
)
(
cfv
c1
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
)
(
cs3
(
cfv
cc0
(
cv
x3
)
)
(
cfv
c1
(
cv
x3
)
)
(
cv
x4
)
)
(
cfv
(
cv
x1
)
ccgra
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
)
)
⟶
wceq
ceqlg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cv
x2
)
(
cs3
(
cfv
c1
(
cv
x2
)
)
(
cfv
c2
(
cv
x2
)
)
(
cfv
cc0
(
cv
x2
)
)
)
(
cfv
(
cv
x1
)
ccgrg
)
)
(
λ x2 .
co
(
cfv
(
cv
x1
)
cbs
)
(
co
cc0
c3
cfzo
)
cmap
)
)
)
⟶
wceq
cttg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
csb
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x2 x3 .
crab
(
λ x4 .
wrex
(
λ x5 .
wceq
(
co
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cv
x1
)
csg
)
)
(
co
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
csg
)
)
(
cfv
(
cv
x1
)
cvsca
)
)
)
(
λ x5 .
co
cc0
c1
cicc
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
)
(
λ x2 .
co
(
co
(
cv
x1
)
(
cop
(
cfv
cnx
citv
)
(
cv
x2
)
)
csts
)
(
cop
(
cfv
cnx
clng
)
(
cmpt2
(
λ x3 x4 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 x4 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 x4 .
crab
(
λ x5 .
w3o
(
wcel
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x2
)
)
)
(
wcel
(
cv
x3
)
(
co
(
cv
x5
)
(
cv
x4
)
(
cv
x2
)
)
)
(
wcel
(
cv
x4
)
(
co
(
cv
x3
)
(
cv
x5
)
(
cv
x2
)
)
)
)
(
λ x5 .
cfv
(
cv
x1
)
cbs
)
)
)
)
csts
)
)
)
⟶
wceq
cee
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
co
cr
(
co
c1
(
cv
x1
)
cfz
)
cmap
)
)
⟶
wceq
cbtwn
(
ccnv
(
coprab
(
λ x1 x2 x3 .
wrex
(
λ x4 .
wa
(
w3a
(
wcel
(
cv
x1
)
(
cfv
(
cv
x4
)
cee
)
)
(
wcel
(
cv
x2
)
(
cfv
(
cv
x4
)
cee
)
)
(
wcel
(
cv
x3
)
(
cfv
(
cv
x4
)
cee
)
)
)
(
wrex
(
λ x5 .
wral
(
λ x6 .
wceq
(
cfv
(
cv
x6
)
(
cv
x3
)
)
(
co
(
co
(
co
c1
(
cv
x5
)
cmin
)
(
cfv
(
cv
x6
)
(
cv
x1
)
)
cmul
)
(
co
(
cv
x5
)
(
cfv
(
cv
x6
)
(
cv
x2
)
)
cmul
)
caddc
)
)
(
λ x6 .
co
c1
(
cv
x4
)
cfz
)
)
(
λ x5 .
co
cc0
c1
cicc
)
)
)
(
λ x4 .
cn
)
)
)
)
⟶
wceq
ccgr
(
copab
(
λ x1 x2 .
wrex
(
λ x3 .
wa
(
wa
(
wcel
(
cv
x1
)
(
cxp
(
cfv
(
cv
x3
)
cee
)
(
cfv
(
cv
x3
)
cee
)
)
)
(
wcel
(
cv
x2
)
(
cxp
(
cfv
(
cv
x3
)
cee
)
(
cfv
(
cv
x3
)
cee
)
)
)
)
(
wceq
(
csu
(
co
c1
(
cv
x3
)
cfz
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cfv
(
cv
x1
)
c1st
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x1
)
c2nd
)
)
cmin
)
c2
cexp
)
)
(
csu
(
co
c1
(
cv
x3
)
cfz
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
c1st
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
c2nd
)
)
cmin
)
c2
cexp
)
)
)
)
(
λ x3 .
cn
)
)
)
⟶
wceq
ceeng
(
cmpt
(
λ x1 .
cn
)
(
λ x1 .
cun
(
cpr
(
cop
(
cfv
cnx
cbs
)
(
cfv
(
cv
x1
)
cee
)
)
(
cop
(
cfv
cnx
cds
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
csu
(
co
c1
(
cv
x1
)
cfz
)
(
λ x4 .
co
(
co
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x4
)
(
cv
x3
)
)
cmin
)
c2
cexp
)
)
)
)
)
(
cpr
(
cop
(
cfv
cnx
citv
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
crab
(
λ x4 .
wbr
(
cv
x4
)
(
cop
(
cv
x2
)
(
cv
x3
)
)
cbtwn
)
(
λ x4 .
cfv
(
cv
x1
)
cee
)
)
)
)
(
cop
(
cfv
cnx
clng
)
(
cmpt2
(
λ x2 x3 .
cfv
(
cv
x1
)
cee
)
(
λ x2 x3 .
cdif
(
cfv
(
cv
x1
)
cee
)
(
csn
(
cv
x2
)
)
)
(
λ x2 x3 .
crab
(
λ x4 .
w3o
(
wbr
(
cv
x4
)
(
cop
(
cv
x2
)
(
cv
x3
)
)
cbtwn
)
(
wbr
(
cv
x2
)
(
cop
(
cv
x4
)
(
cv
x3
)
)
cbtwn
)
(
wbr
(
cv
x3
)
(
cop
(
cv
x2
)
(
cv
x4
)
)
cbtwn
)
)
(
λ x4 .
cfv
(
cv
x1
)
cee
)
)
)
)
)
)
)
⟶
wceq
cedgf
(
cslot
(
cdc
c1
c8
)
)
⟶
wceq
cvtx
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
(
cxp
cvv
cvv
)
)
(
cfv
(
cv
x1
)
c1st
)
(
cfv
(
cv
x1
)
cbs
)
)
)
⟶
wceq
ciedg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cif
(
wcel
(
cv
x1
)
(
cxp
cvv
cvv
)
)
(
cfv
(
cv
x1
)
c2nd
)
(
cfv
(
cv
x1
)
cedgf
)
)
)
⟶
wceq
cedg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crn
(
cfv
(
cv
x1
)
ciedg
)
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
6aa37..
theory
SetMM
stx
ebbdd..
address
TMY6x..