Def (x:T. b(x))(x) == b(x)

is mentioned by

Thm* all(n:hnum. implies(lt(0,n),all(k:hnum. le(div(k,n),k))))	[hdiv_less_eq]
Thm* all(k:hnum. equal(mod(k,suc(0)),0))	[hmod_one]
Thm* all Thm* (k:hnum. all Thm* (k:hnum. (n:hnum. implies Thm* (k:hnum. (n:hnum. (lt(0,n) Thm* (k:hnum. (n:hnum. ,exists Thm* (k:hnum. (n:hnum. ,(r:hnum. exists Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. and Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. (equal(k,add(mult(q,n),r)) Thm* (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. ,lt(r,n)))))))	[hda]
Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (and Thm* (P:hnum  hbool. ((P(0) Thm* (P:hnum  hbool. (,all Thm* (P:hnum  hbool. (,(n:hnum. implies Thm* (P:hnum  hbool. (,(n:hnum. (all(m:hnum. implies(lt(m,n),P(m))) Thm* (P:hnum  hbool. (,(n:hnum. ,P(n)))) Thm* (P:hnum  hbool. ,all(n:hnum. P(n))))	[hgen_induction]
Thm* all Thm* (P:hnum  hbool. implies Thm* (P:hnum  hbool. (exists(n:hnum. P(n)) Thm* (P:hnum  hbool. ,exists Thm* (P:hnum  hbool. ,(n:hnum. and Thm* (P:hnum  hbool. ,(n:hnum. (P(n) Thm* (P:hnum  hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))	[hwop]
Thm* all(n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m))))))	[hless_or_eq_add]
Thm* all(n:hnum. all(m:hnum. equal(le(suc(n),suc(m)),le(n,m))))	[hless_eq_mono]
Thm* all(n:hnum. le(0,n))	[hzero_less_eq]
Thm* all(m:hnum. all(n:hnum. lt(m,add(m,suc(n)))))	[hless_add_suc]
Thm* all(n:hnum. all(m:hnum. implies(and(le(n,m),le(m,n)),equal(n,m))))	[hless_equal_antisym]
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 Thm* (p:hnum. all Thm* (p:hnum. (q:hnum. all Thm* (p:hnum. (q:hnum. (n:hnum. equal Thm* (p:hnum. (q:hnum. (n:hnum. (exp(n,add(p,q)) Thm* (p:hnum. (q:hnum. (n:hnum. ,mult(exp(n,p),exp(n,q))))))	[hexp_add]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies Thm* (m:hnum. (n:hnum. (lt(n,m) Thm* (m:hnum. (n:hnum. ,exists(p:hnum. equal(m,add(n,add(p,1)))))))	[hless_add_1]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(p,sub(m,n)) Thm* (m:hnum. (n:hnum. (p:hnum. ,sub(mult(p,m),mult(p,n))))))	[hleft_sub_distrib]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(sub(m,n),p) Thm* (m:hnum. (n:hnum. (p:hnum. ,sub(mult(m,p),mult(n,p))))))	[hright_sub_distrib]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. implies(le(m,n),le(mult(m,p),mult(n,p))))))	[hless_mono_mult]
Thm* all(m:hnum. all(n:hnum. implies(lt(m,n),le(m,n))))	[hless_imp_less_or_eq]
Thm* all(m:hnum. le(m,m))	[hless_eq_refl]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. implies Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. (and(le(m,p),le(n,q)) Thm* (m:hnum. (n:hnum. (p:hnum. (q:hnum. ,le(add(m,n),add(p,q)))))))	[hless_eq_less_eq_mono]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all(p:hnum. implies(and(le(m,n),le(n,p)),le(m,p)))))	[hless_eq_trans]
Thm* all Thm* (m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,p),add(n,p)),le(m,n)))))	[hless_eq_mono_add_eq]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal(equal(add(m,p),add(n,p)),equal(m,n)))))	[heq_mono_add_eq]
Thm* all Thm* (m:hnum. all(n:hnum. all(p:hnum. equal(lt(add(m,p),add(n,p)),lt(m,n)))))	[hless_mono_add_eq]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all(p:hnum. implies(lt(add(m,p),add(n,p)),lt(m,n)))))	[hless_mono_add_inv]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all(p:hnum. implies(lt(m,n),lt(add(m,p),add(n,p))))))	[hless_mono_add]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. implies Thm* (m:hnum. (n:hnum. (p:hnum. (le(n,p) Thm* (m:hnum. (n:hnum. (p:hnum. ,equal Thm* (m:hnum. (n:hnum. (p:hnum. ,(equal(add(m,n),p) Thm* (m:hnum. (n:hnum. (p:hnum. ,,equal(m,sub(p,n)))))))	[hadd_eq_sub]
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. (and(lt(0,m),lt(0,n)) Thm* (m:hnum. (n:hnum. ,equal(equal(pre(m),pre(n)),equal(m,n)))))	[hinv_pre_eq]
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(m:hnum. all(n:hnum. equal(equal(add(m,n),m),equal(n,0))))	[hadd_inv_0_eq]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. equal(equal(add(m,n),0),and(equal(m,0),equal(n,0)))))	[hadd_eq_0]
Thm* all(m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))	[hpre_sub]
Thm* all(m:hnum. all(n:hnum. implies(le(n,m),equal(add(sub(m,n),n),m))))	[hsub_add]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal(mult(m,mult(n,p)),mult(mult(m,n),p)))))	[hmult_assoc]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(p,add(m,n)) Thm* (m:hnum. (n:hnum. (p:hnum. ,add(mult(p,m),mult(p,n))))))	[hleft_add_distrib]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all Thm* (m:hnum. (n:hnum. (p:hnum. equal Thm* (m:hnum. (n:hnum. (p:hnum. (mult(add(m,n),p) Thm* (m:hnum. (n:hnum. (p:hnum. ,add(mult(m,p),mult(n,p))))))	[hright_add_distrib]
Thm* all(m:hnum. all(n:hnum. equal(mult(m,n),mult(n,m))))	[hmult_sym]
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. equal(mult(m,1),m))	[hmult_right_1]
Thm* all(m:hnum. equal(mult(1,m),m))	[hmult_left_1]
Thm* all(m:hnum. all(n:hnum. equal(mult(m,suc(n)),add(m,mult(m,n)))))	[hmult_suc]
Thm* all(m:hnum. equal(mult(m,0),0))	[hmult_0]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all(p:hnum. equal(add(m,add(n,p)),add(add(m,n),p)))))	[hadd_assoc]
Thm* all(m:hnum. all(n:hnum. equal(equal(sub(m,n),0),le(m,n))))	[hsub_eq_0]
Thm* all(m:hnum. all(n:hnum. equal(not(lt(m,n)),le(n,m))))	[hnot_less]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),le(n,m)))))	[hless_eq_antisym]
Thm* all(m:hnum. all(n:hnum. implies(not(equal(n,0)),lt(m,add(m,n)))))	[hless_add_nonzero]
Thm* all(m:hnum. le(m,suc(m)))	[hless_eq_suc_refl]
Thm* all(m:hnum. all(n:hnum. le(m,add(m,n))))	[hless_eq_add]
Thm* all(m:hnum. all(n:hnum. implies(equal(add(m,n),m),equal(n,0))))	[hadd_inv_0]
Thm* all(m:hnum. all(n:hnum. or(lt(m,n),le(n,m))))	[hless_cases]
Thm* all Thm* (m:hnum. all(n:hnum. implies(and(not(lt(m,n)),not(equal(m,n))),lt(n,m))))	[hless_cases_imp]
Thm* all(m:hnum. or(equal(0,m),lt(0,m)))	[hless_0_cases]
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* 'a:S.  Thm* all Thm* (f:'a  hbool. all Thm* (f:'a  hbool. (x1:'a. all Thm* (f:'a  hbool. (x1:'a. (x2:'a. implies Thm* (f:'a  hbool. (x1:'a. (x2:'a. (and(f(x1),not(f(x2))) Thm* (f:'a  hbool. (x1:'a. (x2:'a. ,not(equal(x1,x2))))))	[hfun_eq_lemma]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,suc(m))))))	[hless_less_suc]
Thm* all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,m)))))	[hless_antisym]
Thm* all(m:hnum. equal(suc(m),add(m,1)))	[hadd1]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. all(p:hnum. implies(and(lt(m,n),lt(n,p)),lt(m,p)))))	[hless_trans]
Thm* all(m:hnum. and(equal(sub(0,m),0),equal(sub(m,0),m)))	[hsub_0]
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. implies(lt(n,m),exists(p:hnum. equal(add(p,n),m)))))	[hless_add]
Thm* all(m:hnum. equal(pre(m),sub(m,1)))	[hpre_sub1]
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(m:hnum. all(n:hnum. equal(add(m,n),add(n,m))))	[hadd_sym]
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(m:hnum. equal(add(m,0),m))	[hadd_0]
Thm* all(n:hnum. not(equal(0,suc(n))))	[hsuc_not]
Thm* all Thm* (n:hnum. implies Thm* (n:hnum. (lt(0,n) Thm* (n:hnum. ,all Thm* (n:hnum. ,(k:hnum. and Thm* (n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n))) Thm* (n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))	[hdivision]
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* all(m:hnum. all(n:hnum. equal(ge(m,n),or(gt(m,n),equal(m,n)))))	[hgreater_or_eq]
Thm* all(m:hnum. all(n:hnum. equal(le(m,n),or(lt(m,n),equal(m,n)))))	[hless_or_eq]
Thm* all(m:hnum. all(n:hnum. equal(gt(m,n),lt(n,m))))	[hgreater_def]
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 hol bool hol num hol prim rec hol min hol arithmetic 1

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