Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
wceq
cgbow
(
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wceq
(
cv
x1
)
(
co
(
co
(
cv
x2
)
(
cv
x3
)
caddc
)
(
cv
x4
)
caddc
)
)
(
λ x4 .
cprime
)
)
(
λ x3 .
cprime
)
)
(
λ x2 .
cprime
)
)
(
λ x1 .
codd
)
)
⟶
wceq
cgbo
(
crab
(
λ x1 .
wrex
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wa
(
w3a
(
wcel
(
cv
x2
)
codd
)
(
wcel
(
cv
x3
)
codd
)
(
wcel
(
cv
x4
)
codd
)
)
(
wceq
(
cv
x1
)
(
co
(
co
(
cv
x2
)
(
cv
x3
)
caddc
)
(
cv
x4
)
caddc
)
)
)
(
λ x4 .
cprime
)
)
(
λ x3 .
cprime
)
)
(
λ x2 .
cprime
)
)
(
λ x1 .
codd
)
)
⟶
(
∀ x1 :
ι → ο
.
w3a
(
wcel
x1
ceven
)
(
wbr
c4
x1
clt
)
(
wbr
x1
(
co
c4
(
co
(
cdc
c1
cc0
)
(
cdc
c1
c8
)
cexp
)
cmul
)
cle
)
⟶
wcel
x1
cgbe
)
⟶
(
∀ x1 :
ι →
ι →
ι →
ι →
ι →
ι → ο
.
∀ x2 :
ι →
ι → ο
.
(
∀ x3 .
wceq
(
x2
x3
)
(
crab
(
λ x4 .
wn
(
wbr
c2
(
cv
x4
)
cdvds
)
)
(
λ x4 .
cz
)
)
)
⟶
(
∀ x3 x4 x5 x6 x7 .
wceq
(
x1
x3
x4
x5
x6
x7
)
(
crab
(
λ x8 .
wrex
(
λ x9 .
wrex
(
λ x10 .
wrex
(
λ x11 .
wa
(
w3a
(
wcel
(
cv
x9
)
(
x2
x4
)
)
(
wcel
(
cv
x10
)
(
x2
x4
)
)
(
wcel
(
cv
x11
)
(
x2
x4
)
)
)
(
wceq
(
cv
x8
)
(
co
(
co
(
cv
x9
)
(
cv
x10
)
caddc
)
(
cv
x11
)
caddc
)
)
)
(
λ x11 .
cprime
)
)
(
λ x10 .
cprime
)
)
(
λ x9 .
cprime
)
)
(
λ x8 .
x2
x4
)
)
)
⟶
∀ x3 x4 x5 x6 .
wrex
(
λ x7 .
wa
(
wbr
(
cv
x7
)
(
co
(
cdc
c1
cc0
)
(
cdc
c2
c7
)
cexp
)
cle
)
(
wral
(
λ x8 .
wbr
(
cv
x7
)
(
cv
x8
)
clt
⟶
wcel
(
cv
x8
)
(
x1
x3
x8
x4
x5
x6
)
)
x2
)
)
(
λ x7 .
cn
)
)
⟶
wrex
(
λ x1 .
wrex
(
λ x2 .
wa
(
w3a
(
wceq
(
cfv
cc0
(
cv
x2
)
)
c7
)
(
wceq
(
cfv
c1
(
cv
x2
)
)
(
cdc
c1
c3
)
)
(
wceq
(
cfv
(
cv
x1
)
(
cv
x2
)
)
(
co
(
cdc
c8
c9
)
(
co
(
cdc
c1
cc0
)
(
cdc
c2
c9
)
cexp
)
cmul
)
)
)
(
wral
(
λ x3 .
w3a
(
wcel
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cdif
cprime
(
csn
c2
)
)
)
(
wbr
(
co
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
(
co
(
co
c4
(
co
(
cdc
c1
cc0
)
(
cdc
c1
c8
)
cexp
)
cmul
)
c4
cmin
)
clt
)
(
wbr
c4
(
co
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
clt
)
)
(
λ x3 .
co
cc0
(
cv
x1
)
cfzo
)
)
)
(
λ x2 .
cfv
(
cv
x1
)
ciccp
)
)
(
λ x1 .
cfv
c3
cuz
)
⟶
(
∀ x1 :
ι → ο
.
w3a
(
wcel
x1
ceven
)
(
wbr
c4
x1
clt
)
(
wbr
x1
(
co
c4
(
co
c10
(
cdc
c1
c8
)
cexp
)
cmul
)
cle
)
⟶
wcel
x1
cgbe
)
⟶
wrex
(
λ x1 .
wrex
(
λ x2 .
wa
(
w3a
(
wceq
(
cfv
cc0
(
cv
x2
)
)
c7
)
(
wceq
(
cfv
c1
(
cv
x2
)
)
(
cdc
c1
c3
)
)
(
wceq
(
cfv
(
cv
x1
)
(
cv
x2
)
)
(
co
(
cdc
c8
c9
)
(
co
c10
(
cdc
c2
c9
)
cexp
)
cmul
)
)
)
(
wral
(
λ x3 .
w3a
(
wcel
(
cfv
(
cv
x3
)
(
cv
x2
)
)
(
cdif
cprime
(
csn
c2
)
)
)
(
wbr
(
co
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
(
co
(
co
c4
(
co
c10
(
cdc
c1
c8
)
cexp
)
cmul
)
c4
cmin
)
clt
)
(
wbr
c4
(
co
(
cfv
(
co
(
cv
x3
)
c1
caddc
)
(
cv
x2
)
)
(
cfv
(
cv
x3
)
(
cv
x2
)
)
cmin
)
clt
)
)
(
λ x3 .
co
cc0
(
cv
x1
)
cfzo
)
)
)
(
λ x2 .
cfv
(
cv
x1
)
ciccp
)
)
(
λ x1 .
cfv
c3
cuz
)
⟶
wrex
(
λ x1 .
wa
(
wbr
(
cv
x1
)
(
co
c10
(
cdc
c2
c7
)
cexp
)
cle
)
(
wral
(
λ x2 .
wbr
(
cv
x1
)
(
cv
x2
)
clt
⟶
wcel
(
cv
x2
)
cgbo
)
(
λ x2 .
codd
)
)
)
(
λ x1 .
cn
)
⟶
wceq
cupwlks
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
copab
(
λ x2 x3 .
w3a
(
wcel
(
cv
x2
)
(
cword
(
cdm
(
cfv
(
cv
x1
)
ciedg
)
)
)
)
(
wf
(
co
cc0
(
cfv
(
cv
x2
)
chash
)
cfz
)
(
cfv
(
cv
x1
)
cvtx
)
(
cv
x3
)
)
(
wral
(
λ x4 .
wceq
(
cfv
(
cfv
(
cv
x4
)
(
cv
x2
)
)
(
cfv
(
cv
x1
)
ciedg
)
)
(
cpr
(
cfv
(
cv
x4
)
(
cv
x3
)
)
(
cfv
(
co
(
cv
x4
)
c1
caddc
)
(
cv
x3
)
)
)
)
(
λ x4 .
co
cc0
(
cfv
(
cv
x2
)
chash
)
cfzo
)
)
)
)
)
⟶
wceq
cspr
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
cab
(
λ x2 .
wrex
(
λ x3 .
wrex
(
λ x4 .
wceq
(
cv
x2
)
(
cpr
(
cv
x3
)
(
cv
x4
)
)
)
(
λ x4 .
cv
x1
)
)
(
λ x3 .
cv
x1
)
)
)
)
⟶
wceq
cmgmhm
(
cmpt2
(
λ x1 x2 .
cmgm
)
(
λ x1 x2 .
cmgm
)
(
λ x1 x2 .
crab
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wceq
(
cfv
(
co
(
cv
x4
)
(
cv
x5
)
(
cfv
(
cv
x1
)
cplusg
)
)
(
cv
x3
)
)
(
co
(
cfv
(
cv
x4
)
(
cv
x3
)
)
(
cfv
(
cv
x5
)
(
cv
x3
)
)
(
cfv
(
cv
x2
)
cplusg
)
)
)
(
λ x5 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x4 .
cfv
(
cv
x1
)
cbs
)
)
(
λ x3 .
co
(
cfv
(
cv
x2
)
cbs
)
(
cfv
(
cv
x1
)
cbs
)
cmap
)
)
)
⟶
wceq
csubmgm
(
cmpt
(
λ x1 .
cmgm
)
(
λ x1 .
crab
(
λ x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wcel
(
co
(
cv
x3
)
(
cv
x4
)
(
cfv
(
cv
x1
)
cplusg
)
)
(
cv
x2
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
(
λ x2 .
cpw
(
cfv
(
cv
x1
)
cbs
)
)
)
)
⟶
wceq
ccllaw
(
copab
(
λ x1 x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wcel
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x1
)
)
(
cv
x2
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
)
⟶
wceq
ccomlaw
(
copab
(
λ x1 x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wceq
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x1
)
)
(
co
(
cv
x4
)
(
cv
x3
)
(
cv
x1
)
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
)
⟶
wceq
casslaw
(
copab
(
λ x1 x2 .
wral
(
λ x3 .
wral
(
λ x4 .
wral
(
λ x5 .
wceq
(
co
(
co
(
cv
x3
)
(
cv
x4
)
(
cv
x1
)
)
(
cv
x5
)
(
cv
x1
)
)
(
co
(
cv
x3
)
(
co
(
cv
x4
)
(
cv
x5
)
(
cv
x1
)
)
(
cv
x1
)
)
)
(
λ x5 .
cv
x2
)
)
(
λ x4 .
cv
x2
)
)
(
λ x3 .
cv
x2
)
)
)
⟶
wceq
cintop
(
cmpt2
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
cvv
)
(
λ x1 x2 .
co
(
cv
x2
)
(
cxp
(
cv
x1
)
(
cv
x1
)
)
cmap
)
)
⟶
wceq
cclintop
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
co
(
cv
x1
)
(
cv
x1
)
cintop
)
)
⟶
wceq
cassintop
(
cmpt
(
λ x1 .
cvv
)
(
λ x1 .
crab
(
λ x2 .
wbr
(
cv
x2
)
(
cv
x1
)
casslaw
)
(
λ x2 .
cfv
(
cv
x1
)
cclintop
)
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
28efb..
theory
SetMM
stx
ebbdd..
address
TMKk2..