Search for blocks/addresses/...
Proofgold Proof
pf
The subproof is completed by applying Sep_Subq with
real
,
λ x0 .
∃ x1 .
and
(
x1
∈
int
)
(
∃ x2 .
and
(
x2
∈
setminus
omega
(
Sing
0
)
)
(
x0
=
div_SNo
x1
x2
)
)
.
■