DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
2
Thm*
a
,
b
:
. {
a
..
b
} ~
(
b
-
a
)
[nsub_intseg_rw]
cites the following:
1
Thm*
c
,
a
:
,
b
:
.
c
=
b
-
a
({
a
..
b
} ~
c
)
[nsub_intseg]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath
Sections
DiscrMathExt
Doc
a,b:
. {a..b
} ~ 
(b-a)c,a:, b:. c = b-a 
({a..b} ~ c)a,b:. {a..b} ~ (b-a)c,a:, b:. c = b-a ({a..b} ~ c)