hol
arithmetic
3
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
m
:
. nnsub(
m
+1;1) =
m
[suc_sub1]
cites the following:
Thm* all(
m
:hnum. equal(sub(suc(
m
),1),
m
))
[hsuc_sub1]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
3
Sections
HOLlib
Doc
m:
. nnsub(m+1;1) = m
m:hnum. equal(sub(suc(m),1),m))m:. nnsub(m+1;1) = mm:hnum. equal(sub(suc(m),1),m))