hol
arithmetic
4
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
m
:
. nnsub(0;
m
) = 0 & nnsub(
m
;0) =
m
[sub_0]
cites the following:
Thm*
all(
m
:hnum. and(equal(sub(0,
m
),0),equal(sub(
m
,0),
m
)))
[hsub_0]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
arithmetic
4
Sections
HOLlib
Doc
m:
. nnsub(0;m) = 0 & nnsub(m;0) = m
m:hnum. and(equal(sub(0,m),0),equal(sub(m,0),m)))m:. nnsub(0;m) = 0 & nnsub(m;0) = mm:hnum. and(equal(sub(0,m),0),equal(sub(m,0),m)))