(3steps total)
PrintForm
Definitions
hol
arithmetic
1
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nnsub
nuprl
m
,
n
:
.
m
n
nnsub(
n
;
m
) =
n
-
m
By:
Unab [`nnsub`] THEN Simp THEN StrongAuto
Generated subgoal:
1
1.
m
:
2.
n
:
3.
m
n
if
n
<
m
then 0 else
n
-
m
fi =
n
-
m
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(3steps total)
PrintForm
Definitions
hol
arithmetic
1
Sections
HOLlib
Doc
m,n:
. m
n 
nnsub(n;m) = n-m m,n:. mn nnsub(n;m) = n-m
n
if n<
m then 0 else n-m fi = n-m 
