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