Search for blocks/addresses/...
Proofgold Term Root Disambiguation
∀ x0 : ο .
(
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wb
(
wrmo
x1
x2
)
(
wmo
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
wceq
(
crab
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
(
x2
x3
)
)
(
x1
x3
)
)
)
)
⟶
wceq
cvv
(
cab
(
λ x1 .
wceq
(
cv
x1
)
(
cv
x1
)
)
)
⟶
(
∀ x1 : ο .
∀ x2 x3 .
wb
(
wcdeq
x1
x2
x3
)
(
wceq
(
cv
x2
)
(
cv
x3
)
⟶
x1
)
)
⟶
(
∀ x1 :
ι → ο
.
∀ x2 :
ι →
ι → ο
.
∀ x3 .
wb
(
wsbc
x1
(
x2
x3
)
)
(
wcel
(
x2
x3
)
(
cab
x1
)
)
)
⟶
(
∀ x1 x2 :
ι →
ι → ο
.
∀ x3 .
wceq
(
csb
(
x1
x3
)
x2
)
(
cab
(
λ x4 .
wsbc
(
λ x5 .
wcel
(
cv
x4
)
(
x2
x5
)
)
(
x1
x3
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cdif
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
x1
)
(
wn
(
wcel
(
cv
x3
)
x2
)
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cun
x1
x2
)
(
cab
(
λ x3 .
wo
(
wcel
(
cv
x3
)
x1
)
(
wcel
(
cv
x3
)
x2
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cin
x1
x2
)
(
cab
(
λ x3 .
wa
(
wcel
(
cv
x3
)
x1
)
(
wcel
(
cv
x3
)
x2
)
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wss
x1
x2
)
(
wceq
(
cin
x1
x2
)
x1
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wb
(
wpss
x1
x2
)
(
wa
(
wss
x1
x2
)
(
wne
x1
x2
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
csymdif
x1
x2
)
(
cun
(
cdif
x1
x2
)
(
cdif
x2
x1
)
)
)
⟶
wceq
c0
(
cdif
cvv
cvv
)
⟶
(
∀ x1 : ο .
∀ x2 x3 :
ι → ο
.
wceq
(
cif
x1
x2
x3
)
(
cab
(
λ x4 .
wo
(
wa
(
wcel
(
cv
x4
)
x2
)
x1
)
(
wa
(
wcel
(
cv
x4
)
x3
)
(
wn
x1
)
)
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
cpw
x1
)
(
cab
(
λ x2 .
wss
(
cv
x2
)
x1
)
)
)
⟶
(
∀ x1 :
ι → ο
.
wceq
(
csn
x1
)
(
cab
(
λ x2 .
wceq
(
cv
x2
)
x1
)
)
)
⟶
(
∀ x1 x2 :
ι → ο
.
wceq
(
cpr
x1
x2
)
(
cun
(
csn
x1
)
(
csn
x2
)
)
)
⟶
(
∀ x1 x2 x3 :
ι → ο
.
wceq
(
ctp
x1
x2
x3
)
(
cun
(
cpr
x1
x2
)
(
csn
x3
)
)
)
⟶
x0
)
⟶
x0
as obj
-
as prop
eed9e..
theory
SetMM
stx
ebbdd..
address
TMMM8..