hol arithmetic 1 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  == {i:| 0i }

is mentioned by

Thm* m,n:. ndiv(m;n [ndiv_wf]
Thm* m,n:. nmod(m;n [nmod_wf]
Thm* n:n>0  odd(n) = odd(n-1)[odd_pos]
Thm* n:. odd(n [odd_wf]
Thm* n:n>0  even(n) = even(n-1)[even_pos]
Thm* n:. even(n [even_wf]
Thm* n:n>0  fact(n) = nfact(n-1)[fact_pos]
Thm* fact(0) = 1[fact_zero]
Thm* n:. fact(n [fact_wf]
Thm* m,n:n>0  exp(m;n) = mexp(m;n-1)[exp_pos]
Thm* m:. exp(m;0) = 1[exp_zero]
Thm* m,n:. exp(m;n [exp_wf]
Thm* m,n:mn  [multiply_wf_nat]
Thm* m,n:. nnsub(m;n [nnsub_wf]
Thm* m,n:mn  nnsub(n;m) = n-m[nnsub_nuprl]
Thm* m,n:m+n  [add_wf_nat]
Def div == m:n:. ndiv(m;n)[hdiv]
Def mod == m:n:. nmod(m;n)[hmod]
Def odd == n:. odd(n)[hodd]
Def even == n:. even(n)[heven]
Def fact == n:. fact(n)[hfact]
Def ge == m:n:nm[hge]
Def le == m:n:mn[hle]
Def gt == m:n:n<m[hgt]
Def exp == m:n:. exp(m;n)[hexp]
Def mult == m:n:mn[hmult]
Def sub == m:n:. nnsub(m;n)[hsub]
Def add == m:n:m+n[hadd]

In prior sections: int 1 bool 1 hol min

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

hol arithmetic 1 Sections HOLlib Doc