hol
prim
rec
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
pre(0) = 0 & (
m
:
. pre(
m
+1) =
m
)
[pre_suc]
cites the following:
Thm*
and(equal(pre(0),0),all(
m
:hnum. equal(pre(suc(
m
)),
m
)))
[hpre_suc]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol
prim
rec
Sections
HOLlib
Doc
m:
. pre(m+1) = m)
m:hnum. equal(pre(suc(m)),m)))m:. pre(m+1) = m)m:hnum. equal(pre(suc(m)),m)))