Def suc == n:. n+1

is mentioned by

Thm* all(k:hnum. equal(mod(k,suc(0)),0))	[hmod_one]
Thm* all(n:hnum. all(m:hnum. equal(le(suc(n),suc(m)),le(n,m))))	[hless_eq_mono]
Thm* all(m:hnum. all(n:hnum. lt(m,add(m,suc(n)))))	[hless_add_suc]
Thm* all Thm* (p:hnum. all Thm* (p:hnum. (q:hnum. all Thm* (p:hnum. (q:hnum. (n:hnum. all Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. equal Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. (equal Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. ((mult(n,exp(suc(q),p)) Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. (,mult(m,exp(suc(q),p))) Thm* (p:hnum. (q:hnum. (n:hnum. (m:hnum. ,equal(n,m))))))	[hmult_exp_mono]
Thm* all Thm* (p:hnum. all Thm* (p:hnum. (m:hnum. all Thm* (p:hnum. (m:hnum. (n:hnum. equal Thm* (p:hnum. (m:hnum. (n:hnum. (equal(mult(n,suc(p)),mult(m,suc(p))) Thm* (p:hnum. (m:hnum. (n:hnum. ,equal(n,m)))))	[hmult_suc_eq]
Thm* all(n:hnum. all(m:hnum. not(equal(suc(add(n,n)),add(m,m)))))	[hnot_odd_eq_even]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),not(lt(n,suc(m))))))	[hless_suc_not]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (lt(0,n) Thm* (m:hnum. (n:hnum. ,equal(equal(m,pre(n)),equal(suc(m),n)))))	[hpre_suc_eq]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. and Thm* (m:hnum. (n:hnum. (equal(mult(0,m),0) Thm* (m:hnum. (n:hnum. ,and Thm* (m:hnum. (n:hnum. ,(equal(mult(m,0),0) Thm* (m:hnum. (n:hnum. ,,and Thm* (m:hnum. (n:hnum. ,,(equal(mult(1,m),m) Thm* (m:hnum. (n:hnum. ,,,and Thm* (m:hnum. (n:hnum. ,,,(equal(mult(m,1),m) Thm* (m:hnum. (n:hnum. ,,,,and Thm* (m:hnum. (n:hnum. ,,,,(equal(mult(suc(m),n),add(mult(m,n),n)) Thm* (m:hnum. (n:hnum. ,,,,,equal(mult(m,suc(n)),add(m,mult(m,n))))))))))	[hmult_clauses]
Thm* all(m:hnum. all(n:hnum. equal(mult(m,suc(n)),add(m,mult(m,n)))))	[hmult_suc]
Thm* all(m:hnum. le(m,suc(m)))	[hless_eq_suc_refl]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (and(lt(m,n),not(equal(n,suc(m)))) Thm* (m:hnum. (n:hnum. ,lt(suc(m),n))))	[hless_not_suc]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (and(lt(m,n),not(equal(suc(m),n))) Thm* (m:hnum. (n:hnum. ,lt(suc(m),n))))	[hless_suc_eq_cor]
Thm* all(m:hnum. all(n:hnum. equal(lt(m,n),le(suc(m),n))))	[hless_eq]
Thm* all(m:hnum. all(n:hnum. implies(le(suc(m),n),lt(m,n))))	[hor_less]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),le(suc(m),n))))	[hless_or]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,suc(m))))))	[hless_less_suc]
Thm* all(m:hnum. equal(suc(m),add(m,1)))	[hadd1]
Thm* all(m:hnum. equal(sub(suc(m),1),m))	[hsuc_sub1]
Thm* all(m:hnum. all(n:hnum. equal(lt(suc(m),suc(n)),lt(m,n))))	[hless_mono_eq]
Thm* all(m:hnum. all(n:hnum. implies(lt(suc(m),suc(n)),lt(m,n))))	[hless_mono_rev]
Thm* all(m:hnum. or(equal(m,0),exists(n:hnum. equal(m,suc(n)))))	[hnum_cases]
Thm* all Thm* (n:hnum. all Thm* (n:hnum. (m:hnum. and Thm* (n:hnum. (m:hnum. (equal(add(0,m),m) Thm* (n:hnum. (m:hnum. ,and Thm* (n:hnum. (m:hnum. ,(equal(add(m,0),m) Thm* (n:hnum. (m:hnum. ,,and Thm* (n:hnum. (m:hnum. ,,(equal(add(suc(m),n),suc(add(m,n))) Thm* (n:hnum. (m:hnum. ,,,equal(add(m,suc(n)),suc(add(m,n))))))))	[hadd_clauses]
Thm* all(m:hnum. all(n:hnum. equal(suc(add(m,n)),add(m,suc(n)))))	[hadd_suc]
Thm* all(n:hnum. not(equal(0,suc(n))))	[hsuc_not]
Thm* and(equal(odd(0),f),all(n:hnum. equal(odd(suc(n)),not(odd(n)))))	[hodd_wd]
Thm* and(equal(even(0),t),all(n:hnum. equal(even(suc(n)),not(even(n)))))	[heven_wd]
Thm* and Thm* (equal(fact(0),1) Thm* ,all(n:hnum. equal(fact(suc(n)),mult(suc(n),fact(n)))))	[hfact_wd]
Thm* and Thm* (all(m:hnum. equal(exp(m,0),1)) Thm* ,all(m:hnum. all(n:hnum. equal(exp(m,suc(n)),mult(m,exp(m,n))))))	[hexp_wd]
Thm* and Thm* (all(n:hnum. equal(mult(0,n),0)) Thm* ,all(m:hnum. all(n:hnum. equal(mult(suc(m),n),add(mult(m,n),n)))))	[hmult_wd]
Thm* and Thm* (all(m:hnum. equal(sub(0,m),0)) Thm* ,all Thm* ,(m:hnum. all Thm* ,(m:hnum. (n:hnum. equal(sub(suc(m),n),cond(lt(m,n),0,suc(sub(m,n)))))))	[hsub_wd]
Thm* and Thm* (all(n:hnum. equal(add(0,n),n)) Thm* ,all(m:hnum. all(n:hnum. equal(add(suc(m),n),suc(add(m,n))))))	[hadd_wd]

In prior sections: hol num hol prim rec

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