(3steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ndiff
bound
b
,
a
:
.
b
(
b
--
a
)+
a
By:
Def of
b
--
a
Generated subgoal:
1
1.
b
:
2.
a
:
b
imax(
b
-
a
;0)+
a
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
b,a:
. b
(b -- a)+a b,a:. b(b -- a)+a
bimax(b-a;0)+a
