Search for blocks/addresses/...
Proofgold Term Root Disambiguation
λ x0 x1 x2 x3 .
and
(
and
(
subfield
x0
x1
)
(
x3
∈
setexp
(
field0
x0
)
(
ordsucc
x2
)
)
)
(
∃ x4 .
and
(
x4
∈
setminus
(
field0
x0
)
(
Sing
(
field3
x0
)
)
)
(
and
(
ap
x3
x2
=
x4
)
(
∃ x6 .
and
(
x6
∈
setexp
(
setexp
(
field0
x1
)
2
)
x2
)
(
and
(
∀ x8 .
x8
∈
x2
⟶
ap
(
ap
x6
x8
)
1
=
field4
x0
)
(
∀ x8 .
x8
∈
field0
x1
⟶
CRing_with_id_eval_poly
x1
(
ordsucc
x2
)
x3
x8
=
nat_primrec
x4
(
λ x10 x11 .
field2b
x1
x11
(
CRing_with_id_eval_poly
x1
2
(
ap
x6
x10
)
x8
)
)
x2
)
)
)
)
)
as obj
ca601..
as prop
-
theory
HotG
stx
6b5ba..
address
TMS2k..