(2steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ndiff
inv
a
:
,
b
:
. ((
a
+
b
) --
b
) =
a
By:
Auto THEN Def of <a> -- <b>
Generated subgoal:
1
1.
a
:
2.
b
:
imax(
a
+
b
-
b
;0) =
a
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
int
2
Sections
StandardLIB
Doc
a:
, b:
. ((a+b) -- b) = a a:, b:. ((a+b) -- b) = a
imax(a+b-b;0) = a
