Search for blocks/addresses/...
Proofgold Term Root Disambiguation
(
∃ x0 .
and
(
Subq
x0
(
binrep
(
Power
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
)
(
∃ x2 .
and
(
∀ x4 .
not
(
exactly3
x0
)
⟶
∃ x5 .
and
(
Subq
x5
x2
)
(
∃ x7 .
and
(
ordinal
x0
)
(
and
(
and
(
and
(
not
(
Subq
x5
x7
)
)
(
nat_p
0
)
)
(
atleast3
x4
)
)
(
and
(
not
(
atleast3
x5
)
)
(
and
(
exactly4
(
setprod
x5
x5
)
)
(
and
(
TransSet
x7
⟶
(
and
(
and
(
SNoLe
x5
x0
)
(
atleast4
(
binrep
(
binrep
(
binrep
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
(
Power
(
Power
0
)
)
)
(
Power
0
)
)
0
)
⟶
exactly1of3
(
not
(
atleast2
(
Power
(
binrep
(
Power
(
Power
0
)
)
0
)
)
)
)
(
SNo
x5
)
(
SNoLe
x7
x5
)
)
)
(
not
(
exactly5
0
)
)
⟶
not
(
atleast2
x7
)
)
⟶
nat_p
x7
)
(
not
(
nat_p
x2
)
)
)
)
)
)
)
)
(
∃ x4 .
and
(
In
x4
0
)
(
∀ x6 .
In
x6
x4
⟶
∃ x7 .
atleast2
x7
)
)
)
)
⟶
∀ x0 : ο .
x0
as obj
-
as prop
60b3a..
theory
HF
stx
d00af..
address
TMYoY..