Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
wceq
cocaN
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
cpw
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cltrn
)
)
)
(
λ x3 .
cfv
(
co
(
co
(
cfv
(
cfv
(
cint
(
crab
(
λ x4 .
wss
(
cv
x3
)
(
cv
x4
)
)
(
λ x4 .
crn
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdia
)
)
)
)
)
(
ccnv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdia
)
)
)
)
(
cfv
(
cv
x1
)
coc
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coc
)
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cmee
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdia
)
)
)
)
)
)
⟶
wceq
cdjaN
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt2
(
λ x3 x4 .
cpw
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cltrn
)
)
)
(
λ x3 x4 .
cpw
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cltrn
)
)
)
(
λ x3 x4 .
cfv
(
cin
(
cfv
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cocaN
)
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cocaN
)
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cocaN
)
)
)
)
)
)
⟶
wceq
cdib
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
cdm
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdia
)
)
)
(
λ x3 .
cxp
(
cfv
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdia
)
)
)
(
csn
(
cmpt
(
λ x4 .
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cltrn
)
)
(
λ x4 .
cres
cid
(
cfv
(
cv
x1
)
cbs
)
)
)
)
)
)
)
)
⟶
wceq
cdic
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
crab
(
λ x4 .
wn
(
wbr
(
cv
x4
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cple
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
catm
)
)
(
λ x3 .
copab
(
λ x4 x5 .
wa
(
wceq
(
cv
x4
)
(
cfv
(
crio
(
λ x6 .
wceq
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coc
)
)
(
cv
x6
)
)
(
cv
x3
)
)
(
λ x6 .
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cltrn
)
)
)
(
cv
x5
)
)
)
(
wcel
(
cv
x5
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
ctendo
)
)
)
)
)
)
)
)
⟶
wceq
cdih
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
cfv
(
cv
x1
)
cbs
)
(
λ x3 .
cif
(
wbr
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cple
)
)
(
cfv
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdib
)
)
)
(
crio
(
λ x4 .
wral
(
λ x5 .
wa
(
wn
(
wbr
(
cv
x5
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cple
)
)
)
(
wceq
(
co
(
cv
x5
)
(
co
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cmee
)
)
(
cfv
(
cv
x1
)
cjn
)
)
(
cv
x3
)
)
⟶
wceq
(
cv
x4
)
(
co
(
cfv
(
cv
x5
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdic
)
)
)
(
cfv
(
co
(
cv
x3
)
(
cv
x2
)
(
cfv
(
cv
x1
)
cmee
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdib
)
)
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clsm
)
)
)
(
λ x5 .
cfv
(
cv
x1
)
catm
)
)
(
λ x4 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clss
)
)
)
)
)
)
⟶
wceq
coch
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
cpw
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cbs
)
)
(
λ x3 .
cfv
(
cfv
(
cfv
(
crab
(
λ x4 .
wss
(
cv
x3
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdih
)
)
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
(
cfv
(
cv
x1
)
cglb
)
)
(
cfv
(
cv
x1
)
coc
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdih
)
)
)
)
)
)
⟶
wceq
cdjh
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt2
(
λ x3 x4 .
cpw
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cbs
)
)
(
λ x3 x4 .
cpw
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cbs
)
)
(
λ x3 x4 .
cfv
(
cin
(
cfv
(
cv
x3
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
)
)
)
⟶
wceq
clpoN
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
w3a
(
wceq
(
cfv
(
cfv
(
cv
x1
)
cbs
)
(
cv
x2
)
)
(
csn
(
cfv
(
cv
x1
)
c0g
)
)
)
(
∀ x3 x4 .
w3a
(
wss
(
cv
x3
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wss
(
cv
x4
)
(
cfv
(
cv
x1
)
cbs
)
)
(
wss
(
cv
x3
)
(
cv
x4
)
)
⟶
wss
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
)
(
wral
(
λ x3 .
wa
(
wcel
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
clsh
)
)
(
wceq
(
cfv
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cv
x2
)
)
(
cv
x3
)
)
)
(
λ x3 .
cfv
(
cv
x1
)
clsa
)
)
)
(
λ x2 .
co
(
cfv
(
cv
x1
)
clss
)
(
cpw
(
cfv
(
cv
x1
)
cbs
)
)
cmap
)
)
)
⟶
wceq
clcd
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
co
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cld
)
(
crab
(
λ x3 .
wceq
(
cfv
(
cfv
(
cfv
(
cv
x3
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clk
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
(
cfv
(
cv
x3
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clk
)
)
)
(
λ x3 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clfn
)
)
cress
)
)
)
⟶
wceq
cmpd
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clss
)
(
λ x3 .
crab
(
λ x4 .
wa
(
wceq
(
cfv
(
cfv
(
cfv
(
cv
x4
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clk
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
(
cfv
(
cv
x4
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clk
)
)
)
(
wss
(
cfv
(
cfv
(
cv
x4
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clk
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
(
cv
x3
)
)
)
(
λ x4 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
clfn
)
)
)
)
)
⟶
wceq
chvm
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cmpt
(
λ x3 .
cdif
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cbs
)
(
csn
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
c0g
)
)
)
(
λ x3 .
cmpt
(
λ x4 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cbs
)
(
λ x4 .
crio
(
λ x5 .
wrex
(
λ x6 .
wceq
(
cv
x4
)
(
co
(
cv
x6
)
(
co
(
cv
x5
)
(
cv
x3
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cvsca
)
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
cplusg
)
)
)
(
λ x6 .
cfv
(
csn
(
cv
x3
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
coch
)
)
)
)
(
λ x5 .
cfv
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
csca
)
cbs
)
)
)
)
)
)
⟶
wceq
chdma1
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cab
(
λ x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wsbc
(
λ x6 .
wsbc
(
λ x7 .
wsbc
(
λ x8 .
wsbc
(
λ x9 .
wsbc
(
λ x10 .
wcel
(
cv
x3
)
(
cmpt
(
λ x11 .
cxp
(
cxp
(
cv
x5
)
(
cv
x8
)
)
(
cv
x5
)
)
(
λ x11 .
cif
(
wceq
(
cfv
(
cv
x11
)
c2nd
)
(
cfv
(
cv
x4
)
c0g
)
)
(
cfv
(
cv
x7
)
c0g
)
(
crio
(
λ x12 .
wa
(
wceq
(
cfv
(
cfv
(
csn
(
cfv
(
cv
x11
)
c2nd
)
)
(
cv
x6
)
)
(
cv
x10
)
)
(
cfv
(
csn
(
cv
x12
)
)
(
cv
x9
)
)
)
(
wceq
(
cfv
(
cfv
(
csn
(
co
(
cfv
(
cfv
(
cv
x11
)
c1st
)
c1st
)
(
cfv
(
cv
x11
)
c2nd
)
(
cfv
(
cv
x4
)
csg
)
)
)
(
cv
x6
)
)
(
cv
x10
)
)
(
cfv
(
csn
(
co
(
cfv
(
cfv
(
cv
x11
)
c1st
)
c2nd
)
(
cv
x12
)
(
cfv
(
cv
x7
)
csg
)
)
)
(
cv
x9
)
)
)
)
(
λ x12 .
cv
x8
)
)
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cmpd
)
)
)
(
cfv
(
cv
x7
)
clspn
)
)
(
cfv
(
cv
x7
)
cbs
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
clcd
)
)
)
(
cfv
(
cv
x4
)
clspn
)
)
(
cfv
(
cv
x4
)
cbs
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
)
)
)
)
⟶
wceq
chdma
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cab
(
λ x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wsbc
(
λ x6 .
wsbc
(
λ x7 .
wcel
(
cv
x3
)
(
cmpt
(
λ x8 .
cv
x6
)
(
λ x8 .
crio
(
λ x9 .
wral
(
λ x10 .
wn
(
wcel
(
cv
x10
)
(
cun
(
cfv
(
csn
(
cv
x4
)
)
(
cfv
(
cv
x5
)
clspn
)
)
(
cfv
(
csn
(
cv
x8
)
)
(
cfv
(
cv
x5
)
clspn
)
)
)
)
⟶
wceq
(
cv
x9
)
(
cfv
(
cotp
(
cv
x10
)
(
cfv
(
cotp
(
cv
x4
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
chvm
)
)
)
(
cv
x10
)
)
(
cv
x7
)
)
(
cv
x8
)
)
(
cv
x7
)
)
)
(
λ x10 .
cv
x6
)
)
(
λ x9 .
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
clcd
)
)
cbs
)
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
chdma1
)
)
)
(
cfv
(
cv
x5
)
cbs
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
)
(
cop
(
cres
cid
(
cfv
(
cv
x1
)
cbs
)
)
(
cres
cid
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cltrn
)
)
)
)
)
)
)
)
⟶
wceq
chg
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
cab
(
λ x3 .
wsbc
(
λ x4 .
wsbc
(
λ x5 .
wsbc
(
λ x6 .
wcel
(
cv
x3
)
(
cmpt
(
λ x7 .
cv
x5
)
(
λ x7 .
crio
(
λ x8 .
wral
(
λ x9 .
wceq
(
cfv
(
co
(
cv
x7
)
(
cv
x9
)
(
cfv
(
cv
x4
)
cvsca
)
)
(
cv
x6
)
)
(
co
(
cv
x8
)
(
cfv
(
cv
x9
)
(
cv
x6
)
)
(
cfv
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
clcd
)
)
cvsca
)
)
)
(
λ x9 .
cfv
(
cv
x4
)
cbs
)
)
(
λ x8 .
cv
x5
)
)
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
chdma
)
)
)
(
cfv
(
cfv
(
cv
x4
)
csca
)
cbs
)
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
)
)
)
)
⟶
wceq
chlh
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cmpt
(
λ x2 .
cfv
(
cv
x1
)
clh
)
(
λ x2 .
csb
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cdvh
)
)
(
λ x3 .
csb
(
cfv
(
cv
x3
)
cbs
)
(
λ x4 .
cun
(
ctp
(
cop
(
cfv
cnx
cbs
)
(
cv
x4
)
)
(
cop
(
cfv
cnx
cplusg
)
(
cfv
(
cv
x3
)
cplusg
)
)
(
cop
(
cfv
cnx
csca
)
(
co
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
cedring
)
)
(
cop
(
cfv
cnx
cstv
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
chg
)
)
)
csts
)
)
)
(
cpr
(
cop
(
cfv
cnx
cvsca
)
(
cfv
(
cv
x3
)
cvsca
)
)
(
cop
(
cfv
cnx
cip
)
(
cmpt2
(
λ x5 x6 .
cv
x4
)
(
λ x5 x6 .
cv
x4
)
(
λ x5 x6 .
cfv
(
cv
x5
)
(
cfv
(
cv
x6
)
(
cfv
(
cv
x2
)
(
cfv
(
cv
x1
)
chdma
)
)
)
)
)
)
)
)
)
)
)
)
⟶
wceq
cnacs
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wrex
(
λ x4 .
wceq
(
cv
x3
)
(
cfv
(
cv
x4
)
(
cfv
(
cv
x2
)
cmrc
)
)
)
(
λ x4 .
cin
(
cpw
(
cv
x1
)
)
cfn
)
)
(
λ x3 .
cv
x2
)
)
(
λ x2 .
cfv
(
cv
x1
)
cacs
)
)
)
⟶
wceq
cmzpcl
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wa
(
wa
(
wral
(
λ x3 .
wcel
(
cxp
(
co
cz
(
cv
x1
)
cmap
)
(
csn
(
cv
x3
)
)
)
(
cv
x2
)
)
(
λ x3 .
cz
)
)
(
wral
(
λ x3 .
wcel
(
cmpt
(
λ x4 .
co
cz
(
cv
x1
)
cmap
)
(
λ x4 .
cfv
(
cv
x3
)
(
cv
x4
)
)
)
(
cv
x2
)
)
(
λ x3 .
cv
x1
)
)
)
(
wral
(
λ x3 .
wral
(
λ x4 .
wa
(
wcel
(
co
(
cv
x3
)
(
cv
x4
)
(
cof
caddc
)
)
(
cv
x2
)
)
(
wcel
(
co
(
cv
x3
)
(
cv
x4
)
(
cof
cmul
)
)
(
cv
x2
)
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
)
(
λ x2 .
cpw
(
co
cz
(
co
cz
(
cv
x1
)
cmap
)
cmap
)
)
)
)
⟶
wceq
cmzp
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cint
(
cfv
(
cv
x1
)
cmzpcl
)
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
659e8..
theory
SetMM
stx
ebbdd..
address
TMZVQ..