Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
wf
(
cxp
chil
chil
)
chil
cva
⟶
(
∀ x1 x2 :
ι → ο
.
wa
(
wcel
x1
chil
)
(
wcel
x2
chil
)
⟶
wceq
(
co
x1
x2
cva
)
(
co
x2
x1
cva
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
w3a
(
wcel
x1
chil
)
(
wcel
x2
chil
)
(
wcel
x3
chil
)
⟶
wceq
(
co
(
co
x1
x2
cva
)
x3
cva
)
(
co
x1
(
co
x2
x3
cva
)
cva
)
)
⟶
wcel
c0v
chil
⟶
(
∀ x1 :
ι → ο
.
wcel
x1
chil
⟶
wceq
(
co
x1
c0v
cva
)
x1
)
⟶
wf
(
cxp
cc
chil
)
chil
csm
⟶
(
∀ x1 :
ι → ο
.
wcel
x1
chil
⟶
wceq
(
co
c1
x1
csm
)
x1
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
w3a
(
wcel
x1
cc
)
(
wcel
x2
cc
)
(
wcel
x3
chil
)
⟶
wceq
(
co
(
co
x1
x2
cmul
)
x3
csm
)
(
co
x1
(
co
x2
x3
csm
)
csm
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
w3a
(
wcel
x1
cc
)
(
wcel
x2
chil
)
(
wcel
x3
chil
)
⟶
wceq
(
co
x1
(
co
x2
x3
cva
)
csm
)
(
co
(
co
x1
x2
csm
)
(
co
x1
x3
csm
)
cva
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
w3a
(
wcel
x1
cc
)
(
wcel
x2
cc
)
(
wcel
x3
chil
)
⟶
wceq
(
co
(
co
x1
x2
caddc
)
x3
csm
)
(
co
(
co
x1
x3
csm
)
(
co
x2
x3
csm
)
cva
)
)
⟶
(
∀ x1 :
ι → ο
.
wcel
x1
chil
⟶
wceq
(
co
cc0
x1
csm
)
c0v
)
⟶
wf
(
cxp
chil
chil
)
cc
csp
⟶
(
∀ x1 x2 :
ι → ο
.
wa
(
wcel
x1
chil
)
(
wcel
x2
chil
)
⟶
wceq
(
co
x1
x2
csp
)
(
cfv
(
co
x2
x1
csp
)
ccj
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
w3a
(
wcel
x1
chil
)
(
wcel
x2
chil
)
(
wcel
x3
chil
)
⟶
wceq
(
co
(
co
x1
x2
cva
)
x3
csp
)
(
co
(
co
x1
x3
csp
)
(
co
x2
x3
csp
)
caddc
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
w3a
(
wcel
x1
cc
)
(
wcel
x2
chil
)
(
wcel
x3
chil
)
⟶
wceq
(
co
(
co
x1
x2
csm
)
x3
csp
)
(
co
x1
(
co
x2
x3
csp
)
cmul
)
)
⟶
(
∀ x1 :
ι → ο
.
wa
(
wcel
x1
chil
)
(
wne
x1
c0v
)
⟶
wbr
cc0
(
co
x1
x1
csp
)
clt
)
⟶
(
∀ x1 :
ι → ο
.
wcel
x1
ccau
⟶
wrex
(
λ x2 .
wbr
x1
(
cv
x2
)
chli
)
(
λ x2 .
chil
)
)
⟶
wceq
csh
(
crab
(
λ x1 .
w3a
(
wcel
c0v
(
cv
x1
)
)
(
wss
(
cima
cva
(
cxp
(
cv
x1
)
(
cv
x1
)
)
)
(
cv
x1
)
)
(
wss
(
cima
csm
(
cxp
cc
(
cv
x1
)
)
)
(
cv
x1
)
)
)
(
λ x1 .
cpw
chil
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
c7505..
theory
SetMM
stx
ebbdd..
address
TMbHK..