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