Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 x2 .
∀ x3 :
ι →
ι →
ι → ο
.
(
∀ x4 .
x3
c4def..
x4
x4
)
⟶
(
∀ x4 x5 x6 x7 x8 .
x3
x4
x6
x7
⟶
x3
x5
x7
x8
⟶
x3
(
6b90c..
x4
x5
)
x6
x8
)
⟶
(
∀ x4 .
x3
c9248..
x4
236c6..
)
⟶
(
∀ x4 x5 x6 .
x3
x4
x5
x6
⟶
x3
(
a6e19..
x4
)
x5
(
0b8ef..
x6
)
)
⟶
(
∀ x4 x5 x6 .
x3
x4
x5
x6
⟶
x3
(
2fe34..
x4
)
x5
(
6c5f4..
x6
)
)
⟶
(
∀ x4 x5 x6 x7 x8 .
e05e6..
x5
⟶
x3
x4
(
cfc98..
x6
x7
)
x8
⟶
x3
(
3e00e..
x4
x5
)
(
cfc98..
(
0b8ef..
x6
)
x7
)
x8
)
⟶
(
∀ x4 x5 x6 x7 x8 .
e05e6..
x4
⟶
x3
x5
(
cfc98..
x6
x7
)
x8
⟶
x3
(
3e00e..
x4
x5
)
(
cfc98..
(
6c5f4..
x6
)
x7
)
x8
)
⟶
(
∀ x4 x5 x6 x7 x8 .
x3
x4
x6
x7
⟶
x3
x5
x6
x8
⟶
x3
(
f9341..
x4
x5
)
x6
(
cfc98..
x7
x8
)
)
⟶
(
∀ x4 x5 x6 x7 .
x3
x4
x5
x7
⟶
x3
(
1fa6d..
x4
)
(
cfc98..
x5
x6
)
x7
)
⟶
(
∀ x4 x5 x6 x7 .
x3
x4
x6
x7
⟶
x3
(
3a365..
x4
)
(
cfc98..
x5
x6
)
x7
)
⟶
x3
x0
x1
x2
as obj
d7d78..
as prop
-
theory
HOAS
stx
8d75a..
address
TMLYb..