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