Nuprl - hol_arithmetic

Origin Definitions Sections HOLlib Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
hol_arithmetic_2Nuprl Section: hol_arithmetic_2

Selected Objects
THM hadd_wd and
(all(n:hnum. equal(add(0,n),n))
,all(m:hnum. all(n:hnum. equal(add(suc(m),n),suc(add(m,n))))))

THM hsub_wd and
(all(m:hnum. equal(sub(0,m),0))
,all(m:hnum. all(n:hnum. equal(sub(suc(m),n),cond(lt(m,n),0,suc(sub(m,n)))))))

THM hmult_wd and
(all(n:hnum. equal(mult(0,n),0))
,all(m:hnum. all(n:hnum. equal(mult(suc(m),n),add(mult(m,n),n)))))

THM hexp_wd and
(all(m:hnum. equal(exp(m,0),1))
,all(m:hnum. all(n:hnum. equal(exp(m,suc(n)),mult(m,exp(m,n))))))

THM hgreater_def all(m:hnum. all(n:hnum. equal(gt(m,n),lt(n,m))))

THM hless_or_eq all(m:hnum. all(n:hnum. equal(le(m,n),or(lt(m,n),equal(m,n)))))

THM hgreater_or_eq all(m:hnum. all(n:hnum. equal(ge(m,n),or(gt(m,n),equal(m,n)))))

THM hfact_wd and(equal(fact(0),1),all(n:hnum. equal(fact(suc(n)),mult(suc(n),fact(n)))))

THM heven_wd and(equal(even(0),t),all(n:hnum. equal(even(suc(n)),not(even(n)))))

THM hodd_wd and(equal(odd(0),f),all(n:hnum. equal(odd(suc(n)),not(odd(n)))))

THM hdivision all
(n:hnum. implies
(n:hnum. (lt(0,n)
(n:hnum. ,all
(n:hnum. ,(k:hnum. and
(n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n)))
(n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))

THM hsuc_not all(n:hnum. not(equal(0,suc(n))))

THM hadd_0 all(m:hnum. equal(add(m,0),m))

THM hadd_suc all(m:hnum. all(n:hnum. equal(suc(add(m,n)),add(m,suc(n)))))

THM hadd_clauses all
(n:hnum. all
(n:hnum. (m:hnum. and
(n:hnum. (m:hnum. (equal(add(0,m),m)
(n:hnum. (m:hnum. ,and
(n:hnum. (m:hnum. ,(equal(add(m,0),m)
(n:hnum. (m:hnum. ,,and
(n:hnum. (m:hnum. ,,(equal(add(suc(m),n),suc(add(m,n)))
(n:hnum. (m:hnum. ,,,equal(add(m,suc(n)),suc(add(m,n))))))))

THM hadd_sym all(m:hnum. all(n:hnum. equal(add(m,n),add(n,m))))

THM hnum_cases all(m:hnum. or(equal(m,0),exists(n:hnum. equal(m,suc(n)))))

THM hless_mono_rev all(m:hnum. all(n:hnum. implies(lt(suc(m),suc(n)),lt(m,n))))

THM hless_mono_eq all(m:hnum. all(n:hnum. equal(lt(suc(m),suc(n)),lt(m,n))))

THM hsuc_sub1 all(m:hnum. equal(sub(suc(m),1),m))

THM hpre_sub1 all(m:hnum. equal(pre(m),sub(m,1)))

THM hless_add all(m:hnum. all(n:hnum. implies(lt(n,m),exists(p:hnum. equal(add(p,n),m)))))

THM hsub_0 all(m:hnum. and(equal(sub(0,m),0),equal(sub(m,0),m)))

THM hless_trans all(m:hnum. all(n:hnum. all(p:hnum. implies(and(lt(m,n),lt(n,p)),lt(m,p)))))

THM hadd1 all(m:hnum. equal(suc(m),add(m,1)))

THM hless_antisym all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,m)))))

THM hless_less_suc all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,suc(m))))))

THM hfun_eq_lemma 'a:S.
all
(f:'a  hbool. all
(f:'a  hbool. (x1:'a. all
(f:'a  hbool. (x1:'a. (x2:'a. implies
(f:'a  hbool. (x1:'a. (x2:'a. (and(f(x1),not(f(x2)))
(f:'a  hbool. (x1:'a. (x2:'a. ,not(equal(x1,x2))))))

THM hless_or all(m:hnum. all(n:hnum. implies(lt(m,n),le(suc(m),n))))

THM hor_less all(m:hnum. all(n:hnum. implies(le(suc(m),n),lt(m,n))))

THM hless_eq all(m:hnum. all(n:hnum. equal(lt(m,n),le(suc(m),n))))

THM hless_suc_eq_cor all
(m:hnum. all(n:hnum. implies(and(lt(m,n),not(equal(suc(m),n))),lt(suc(m),n))))

THM hless_not_suc all
(m:hnum. all(n:hnum. implies(and(lt(m,n),not(equal(n,suc(m)))),lt(suc(m),n))))

THM hless_0_cases all(m:hnum. or(equal(0,m),lt(0,m)))

THM hless_cases_imp all(m:hnum. all(n:hnum. implies(and(not(lt(m,n)),not(equal(m,n))),lt(n,m))))

THM hless_cases all(m:hnum. all(n:hnum. or(lt(m,n),le(n,m))))

THM hadd_inv_0 all(m:hnum. all(n:hnum. implies(equal(add(m,n),m),equal(n,0))))

THM hless_eq_add all(m:hnum. all(n:hnum. le(m,add(m,n))))

THM hless_eq_suc_refl all(m:hnum. le(m,suc(m)))

THM hless_add_nonzero all(m:hnum. all(n:hnum. implies(not(equal(n,0)),lt(m,add(m,n)))))

THM hless_eq_antisym all(m:hnum. all(n:hnum. not(and(lt(m,n),le(n,m)))))

THM hnot_less all(m:hnum. all(n:hnum. equal(not(lt(m,n)),le(n,m))))

THM hsub_eq_0 all(m:hnum. all(n:hnum. equal(equal(sub(m,n),0),le(m,n))))

THM hadd_assoc all(m:hnum. all(n:hnum. all(p:hnum. equal(add(m,add(n,p)),add(add(m,n),p)))))

THM hmult_0 all(m:hnum. equal(mult(m,0),0))

THM hmult_suc all(m:hnum. all(n:hnum. equal(mult(m,suc(n)),add(m,mult(m,n)))))

THM hmult_left_1 all(m:hnum. equal(mult(1,m),m))

THM hmult_right_1 all(m:hnum. equal(mult(m,1),m))

THM hmult_clauses all
(m:hnum. all
(m:hnum. (n:hnum. and
(m:hnum. (n:hnum. (equal(mult(0,m),0)
(m:hnum. (n:hnum. ,and
(m:hnum. (n:hnum. ,(equal(mult(m,0),0)
(m:hnum. (n:hnum. ,,and
(m:hnum. (n:hnum. ,,(equal(mult(1,m),m)
(m:hnum. (n:hnum. ,,,and
(m:hnum. (n:hnum. ,,,(equal(mult(m,1),m)
(m:hnum. (n:hnum. ,,,,and
(m:hnum. (n:hnum. ,,,,(equal(mult(suc(m),n),add(mult(m,n),n))
(m:hnum. (n:hnum. ,,,,,equal(mult(m,suc(n)),add(m,mult(m,n))))))))))

THM hmult_sym all(m:hnum. all(n:hnum. equal(mult(m,n),mult(n,m))))

THM hright_add_distrib all
(m:hnum. all
(m:hnum. (n:hnum. all
(m:hnum. (n:hnum. (p:hnum. equal
(m:hnum. (n:hnum. (p:hnum. (mult(add(m,n),p)
(m:hnum. (n:hnum. (p:hnum. ,add(mult(m,p),mult(n,p))))))

THM hleft_add_distrib all
(m:hnum. all
(m:hnum. (n:hnum. all
(m:hnum. (n:hnum. (p:hnum. equal
(m:hnum. (n:hnum. (p:hnum. (mult(p,add(m,n))
(m:hnum. (n:hnum. (p:hnum. ,add(mult(p,m),mult(p,n))))))

THM hmult_assoc all
(m:hnum. all
(m:hnum. (n:hnum. all(p:hnum. equal(mult(m,mult(n,p)),mult(mult(m,n),p)))))

THM hsub_add all(m:hnum. all(n:hnum. implies(le(n,m),equal(add(sub(m,n),n),m))))

THM hpre_sub all(m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))

THM hadd_eq_0 all(m:hnum. all(n:hnum. equal(equal(add(m,n),0),and(equal(m,0),equal(n,0)))))

THM hadd_inv_0_eq all(m:hnum. all(n:hnum. equal(equal(add(m,n),m),equal(n,0))))

THM hpre_suc_eq all
(m:hnum. all(n:hnum. implies(lt(0,n),equal(equal(m,pre(n)),equal(suc(m),n)))))

THM hinv_pre_eq all
(m:hnum. all
(m:hnum. (n:hnum. implies
(m:hnum. (n:hnum. (and(lt(0,m),lt(0,n))
(m:hnum. (n:hnum. ,equal(equal(pre(m),pre(n)),equal(m,n)))))

THM hless_suc_not all(m:hnum. all(n:hnum. implies(lt(m,n),not(lt(n,suc(m))))))

THM hadd_eq_sub all
(m:hnum. all
(m:hnum. (n:hnum. all
(m:hnum. (n:hnum. (p:hnum. implies
(m:hnum. (n:hnum. (p:hnum. (le(n,p)
(m:hnum. (n:hnum. (p:hnum. ,equal(equal(add(m,n),p),equal(m,sub(p,n)))))))

THM hless_mono_add all(m:hnum. all(n:hnum. all(p:hnum. implies(lt(m,n),lt(add(m,p),add(n,p))))))

THM hless_mono_add_inv all(m:hnum. all(n:hnum. all(p:hnum. implies(lt(add(m,p),add(n,p)),lt(m,n)))))

THM hless_mono_add_eq all(m:hnum. all(n:hnum. all(p:hnum. equal(lt(add(m,p),add(n,p)),lt(m,n)))))

THM heq_mono_add_eq all
(m:hnum. all
(m:hnum. (n:hnum. all(p:hnum. equal(equal(add(m,p),add(n,p)),equal(m,n)))))

THM hless_eq_mono_add_eq all(m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,p),add(n,p)),le(m,n)))))

THM hless_eq_trans all(m:hnum. all(n:hnum. all(p:hnum. implies(and(le(m,n),le(n,p)),le(m,p)))))

THM hless_eq_less_eq_mono all
(m:hnum. all
(m:hnum. (n:hnum. all
(m:hnum. (n:hnum. (p:hnum. all
(m:hnum. (n:hnum. (p:hnum. (q:hnum. implies
(m:hnum. (n:hnum. (p:hnum. (q:hnum. (and(le(m,p),le(n,q))
(m:hnum. (n:hnum. (p:hnum. (q:hnum. ,le(add(m,n),add(p,q)))))))

THM hless_eq_refl all(m:hnum. le(m,m))

THM hless_imp_less_or_eq all(m:hnum. all(n:hnum. implies(lt(m,n),le(m,n))))

THM hless_mono_mult all
(m:hnum. all(n:hnum. all(p:hnum. implies(le(m,n),le(mult(m,p),mult(n,p))))))

THM hright_sub_distrib all
(m:hnum. all
(m:hnum. (n:hnum. all
(m:hnum. (n:hnum. (p:hnum. equal
(m:hnum. (n:hnum. (p:hnum. (mult(sub(m,n),p)
(m:hnum. (n:hnum. (p:hnum. ,sub(mult(m,p),mult(n,p))))))

THM hleft_sub_distrib all
(m:hnum. all
(m:hnum. (n:hnum. all
(m:hnum. (n:hnum. (p:hnum. equal
(m:hnum. (n:hnum. (p:hnum. (mult(p,sub(m,n))
(m:hnum. (n:hnum. (p:hnum. ,sub(mult(p,m),mult(p,n))))))

THM hless_add_1 all
(m:hnum. all
(m:hnum. (n:hnum. implies(lt(n,m),exists(p:hnum. equal(m,add(n,add(p,1)))))))

THM hexp_add all
(p:hnum. all
(p:hnum. (q:hnum. all
(p:hnum. (q:hnum. (n:hnum. equal(exp(n,add(p,q)),mult(exp(n,p),exp(n,q))))))

THM hnot_odd_eq_even all(n:hnum. all(m:hnum. not(equal(suc(add(n,n)),add(m,m)))))

THM hmult_suc_eq all
(p:hnum. all
(p:hnum. (m:hnum. all
(p:hnum. (m:hnum. (n:hnum. equal
(p:hnum. (m:hnum. (n:hnum. (equal(mult(n,suc(p)),mult(m,suc(p)))
(p:hnum. (m:hnum. (n:hnum. ,equal(n,m)))))

THM hmult_exp_mono all
(p:hnum. all
(p:hnum. (q:hnum. all
(p:hnum. (q:hnum. (n:hnum. all
(p:hnum. (q:hnum. (n:hnum. (m:hnum. equal
(p:hnum. (q:hnum. (n:hnum. (m:hnum. (equal
(p:hnum. (q:hnum. (n:hnum. (m:hnum. ((mult(n,exp(suc(q),p))
(p:hnum. (q:hnum. (n:hnum. (m:hnum. (,mult(m,exp(suc(q),p)))
(p:hnum. (q:hnum. (n:hnum. (m:hnum. ,equal(n,m))))))

THM hless_equal_antisym all(n:hnum. all(m:hnum. implies(and(le(n,m),le(m,n)),equal(n,m))))

THM hless_add_suc all(m:hnum. all(n:hnum. lt(m,add(m,suc(n)))))

THM hzero_less_eq all(n:hnum. le(0,n))

THM hless_eq_mono all(n:hnum. all(m:hnum. equal(le(suc(n),suc(m)),le(n,m))))

THM hless_or_eq_add all(n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m))))))

THM hwop all
(P:hnum  hbool. implies
(P:hnum  hbool. (exists(n:hnum. P(n))
(P:hnum  hbool. ,exists
(P:hnum  hbool. ,(n:hnum. and
(P:hnum  hbool. ,(n:hnum. (P(n)
(P:hnum  hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))

THM hgen_induction all
(P:hnum  hbool. implies
(P:hnum  hbool. (and
(P:hnum  hbool. ((P(0)
(P:hnum  hbool. (,all
(P:hnum  hbool. (,(n:hnum. implies
(P:hnum  hbool. (,(n:hnum. (all(m:hnum. implies(lt(m,n),P(m)))
(P:hnum  hbool. (,(n:hnum. ,P(n))))
(P:hnum  hbool. ,all(n:hnum. P(n))))

THM hda all
(k:hnum. all
(k:hnum. (n:hnum. implies
(k:hnum. (n:hnum. (lt(0,n)
(k:hnum. (n:hnum. ,exists
(k:hnum. (n:hnum. ,(r:hnum. exists
(k:hnum. (n:hnum. ,(r:hnum. (q:hnum. and
(k:hnum. (n:hnum. ,(r:hnum. (q:hnum. (equal(k,add(mult(q,n),r))
(k:hnum. (n:hnum. ,(r:hnum. (q:hnum. ,lt(r,n)))))))

THM hmod_one all(k:hnum. equal(mod(k,suc(0)),0))

THM hdiv_less_eq all(n:hnum. implies(lt(0,n),all(k:hnum. le(div(k,n),k))))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Selected Objects
THM	hadd_wd	and (all(n:hnum. equal(add(0,n),n)) ,all(m:hnum. all(n:hnum. equal(add(suc(m),n),suc(add(m,n))))))
THM	hsub_wd	and (all(m:hnum. equal(sub(0,m),0)) ,all(m:hnum. all(n:hnum. equal(sub(suc(m),n),cond(lt(m,n),0,suc(sub(m,n)))))))
THM	hmult_wd	and (all(n:hnum. equal(mult(0,n),0)) ,all(m:hnum. all(n:hnum. equal(mult(suc(m),n),add(mult(m,n),n)))))
THM	hexp_wd	and (all(m:hnum. equal(exp(m,0),1)) ,all(m:hnum. all(n:hnum. equal(exp(m,suc(n)),mult(m,exp(m,n))))))
THM	hgreater_def	all(m:hnum. all(n:hnum. equal(gt(m,n),lt(n,m))))
THM	hless_or_eq	all(m:hnum. all(n:hnum. equal(le(m,n),or(lt(m,n),equal(m,n)))))
THM	hgreater_or_eq	all(m:hnum. all(n:hnum. equal(ge(m,n),or(gt(m,n),equal(m,n)))))
THM	hfact_wd	and(equal(fact(0),1),all(n:hnum. equal(fact(suc(n)),mult(suc(n),fact(n)))))
THM	heven_wd	and(equal(even(0),t),all(n:hnum. equal(even(suc(n)),not(even(n)))))
THM	hodd_wd	and(equal(odd(0),f),all(n:hnum. equal(odd(suc(n)),not(odd(n)))))
THM	hdivision	all (n:hnum. implies (n:hnum. (lt(0,n) (n:hnum. ,all (n:hnum. ,(k:hnum. and (n:hnum. ,(k:hnum. (equal(k,add(mult(div(k,n),n),mod(k,n))) (n:hnum. ,(k:hnum. ,lt(mod(k,n),n)))))
THM	hsuc_not	all(n:hnum. not(equal(0,suc(n))))
THM	hadd_0	all(m:hnum. equal(add(m,0),m))
THM	hadd_suc	all(m:hnum. all(n:hnum. equal(suc(add(m,n)),add(m,suc(n)))))
THM	hadd_clauses	all (n:hnum. all (n:hnum. (m:hnum. and (n:hnum. (m:hnum. (equal(add(0,m),m) (n:hnum. (m:hnum. ,and (n:hnum. (m:hnum. ,(equal(add(m,0),m) (n:hnum. (m:hnum. ,,and (n:hnum. (m:hnum. ,,(equal(add(suc(m),n),suc(add(m,n))) (n:hnum. (m:hnum. ,,,equal(add(m,suc(n)),suc(add(m,n))))))))
THM	hadd_sym	all(m:hnum. all(n:hnum. equal(add(m,n),add(n,m))))
THM	hnum_cases	all(m:hnum. or(equal(m,0),exists(n:hnum. equal(m,suc(n)))))
THM	hless_mono_rev	all(m:hnum. all(n:hnum. implies(lt(suc(m),suc(n)),lt(m,n))))
THM	hless_mono_eq	all(m:hnum. all(n:hnum. equal(lt(suc(m),suc(n)),lt(m,n))))
THM	hsuc_sub1	all(m:hnum. equal(sub(suc(m),1),m))
THM	hpre_sub1	all(m:hnum. equal(pre(m),sub(m,1)))
THM	hless_add	all(m:hnum. all(n:hnum. implies(lt(n,m),exists(p:hnum. equal(add(p,n),m)))))
THM	hsub_0	all(m:hnum. and(equal(sub(0,m),0),equal(sub(m,0),m)))
THM	hless_trans	all(m:hnum. all(n:hnum. all(p:hnum. implies(and(lt(m,n),lt(n,p)),lt(m,p)))))
THM	hadd1	all(m:hnum. equal(suc(m),add(m,1)))
THM	hless_antisym	all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,m)))))
THM	hless_less_suc	all(m:hnum. all(n:hnum. not(and(lt(m,n),lt(n,suc(m))))))
THM	hfun_eq_lemma	'a:S. all (f:'a hbool. all (f:'a hbool. (x1:'a. all (f:'a hbool. (x1:'a. (x2:'a. implies (f:'a hbool. (x1:'a. (x2:'a. (and(f(x1),not(f(x2))) (f:'a hbool. (x1:'a. (x2:'a. ,not(equal(x1,x2))))))
THM	hless_or	all(m:hnum. all(n:hnum. implies(lt(m,n),le(suc(m),n))))
THM	hor_less	all(m:hnum. all(n:hnum. implies(le(suc(m),n),lt(m,n))))
THM	hless_eq	all(m:hnum. all(n:hnum. equal(lt(m,n),le(suc(m),n))))
THM	hless_suc_eq_cor	all (m:hnum. all(n:hnum. implies(and(lt(m,n),not(equal(suc(m),n))),lt(suc(m),n))))
THM	hless_not_suc	all (m:hnum. all(n:hnum. implies(and(lt(m,n),not(equal(n,suc(m)))),lt(suc(m),n))))
THM	hless_0_cases	all(m:hnum. or(equal(0,m),lt(0,m)))
THM	hless_cases_imp	all(m:hnum. all(n:hnum. implies(and(not(lt(m,n)),not(equal(m,n))),lt(n,m))))
THM	hless_cases	all(m:hnum. all(n:hnum. or(lt(m,n),le(n,m))))
THM	hadd_inv_0	all(m:hnum. all(n:hnum. implies(equal(add(m,n),m),equal(n,0))))
THM	hless_eq_add	all(m:hnum. all(n:hnum. le(m,add(m,n))))
THM	hless_eq_suc_refl	all(m:hnum. le(m,suc(m)))
THM	hless_add_nonzero	all(m:hnum. all(n:hnum. implies(not(equal(n,0)),lt(m,add(m,n)))))
THM	hless_eq_antisym	all(m:hnum. all(n:hnum. not(and(lt(m,n),le(n,m)))))
THM	hnot_less	all(m:hnum. all(n:hnum. equal(not(lt(m,n)),le(n,m))))
THM	hsub_eq_0	all(m:hnum. all(n:hnum. equal(equal(sub(m,n),0),le(m,n))))
THM	hadd_assoc	all(m:hnum. all(n:hnum. all(p:hnum. equal(add(m,add(n,p)),add(add(m,n),p)))))
THM	hmult_0	all(m:hnum. equal(mult(m,0),0))
THM	hmult_suc	all(m:hnum. all(n:hnum. equal(mult(m,suc(n)),add(m,mult(m,n)))))
THM	hmult_left_1	all(m:hnum. equal(mult(1,m),m))
THM	hmult_right_1	all(m:hnum. equal(mult(m,1),m))
THM	hmult_clauses	all (m:hnum. all (m:hnum. (n:hnum. and (m:hnum. (n:hnum. (equal(mult(0,m),0) (m:hnum. (n:hnum. ,and (m:hnum. (n:hnum. ,(equal(mult(m,0),0) (m:hnum. (n:hnum. ,,and (m:hnum. (n:hnum. ,,(equal(mult(1,m),m) (m:hnum. (n:hnum. ,,,and (m:hnum. (n:hnum. ,,,(equal(mult(m,1),m) (m:hnum. (n:hnum. ,,,,and (m:hnum. (n:hnum. ,,,,(equal(mult(suc(m),n),add(mult(m,n),n)) (m:hnum. (n:hnum. ,,,,,equal(mult(m,suc(n)),add(m,mult(m,n))))))))))
THM	hmult_sym	all(m:hnum. all(n:hnum. equal(mult(m,n),mult(n,m))))
THM	hright_add_distrib	all (m:hnum. all (m:hnum. (n:hnum. all (m:hnum. (n:hnum. (p:hnum. equal (m:hnum. (n:hnum. (p:hnum. (mult(add(m,n),p) (m:hnum. (n:hnum. (p:hnum. ,add(mult(m,p),mult(n,p))))))
THM	hleft_add_distrib	all (m:hnum. all (m:hnum. (n:hnum. all (m:hnum. (n:hnum. (p:hnum. equal (m:hnum. (n:hnum. (p:hnum. (mult(p,add(m,n)) (m:hnum. (n:hnum. (p:hnum. ,add(mult(p,m),mult(p,n))))))
THM	hmult_assoc	all (m:hnum. all (m:hnum. (n:hnum. all(p:hnum. equal(mult(m,mult(n,p)),mult(mult(m,n),p)))))
THM	hsub_add	all(m:hnum. all(n:hnum. implies(le(n,m),equal(add(sub(m,n),n),m))))
THM	hpre_sub	all(m:hnum. all(n:hnum. equal(pre(sub(m,n)),sub(pre(m),n))))
THM	hadd_eq_0	all(m:hnum. all(n:hnum. equal(equal(add(m,n),0),and(equal(m,0),equal(n,0)))))
THM	hadd_inv_0_eq	all(m:hnum. all(n:hnum. equal(equal(add(m,n),m),equal(n,0))))
THM	hpre_suc_eq	all (m:hnum. all(n:hnum. implies(lt(0,n),equal(equal(m,pre(n)),equal(suc(m),n)))))
THM	hinv_pre_eq	all (m:hnum. all (m:hnum. (n:hnum. implies (m:hnum. (n:hnum. (and(lt(0,m),lt(0,n)) (m:hnum. (n:hnum. ,equal(equal(pre(m),pre(n)),equal(m,n)))))
THM	hless_suc_not	all(m:hnum. all(n:hnum. implies(lt(m,n),not(lt(n,suc(m))))))
THM	hadd_eq_sub	all (m:hnum. all (m:hnum. (n:hnum. all (m:hnum. (n:hnum. (p:hnum. implies (m:hnum. (n:hnum. (p:hnum. (le(n,p) (m:hnum. (n:hnum. (p:hnum. ,equal(equal(add(m,n),p),equal(m,sub(p,n)))))))
THM	hless_mono_add	all(m:hnum. all(n:hnum. all(p:hnum. implies(lt(m,n),lt(add(m,p),add(n,p))))))
THM	hless_mono_add_inv	all(m:hnum. all(n:hnum. all(p:hnum. implies(lt(add(m,p),add(n,p)),lt(m,n)))))
THM	hless_mono_add_eq	all(m:hnum. all(n:hnum. all(p:hnum. equal(lt(add(m,p),add(n,p)),lt(m,n)))))
THM	heq_mono_add_eq	all (m:hnum. all (m:hnum. (n:hnum. all(p:hnum. equal(equal(add(m,p),add(n,p)),equal(m,n)))))
THM	hless_eq_mono_add_eq	all(m:hnum. all(n:hnum. all(p:hnum. equal(le(add(m,p),add(n,p)),le(m,n)))))
THM	hless_eq_trans	all(m:hnum. all(n:hnum. all(p:hnum. implies(and(le(m,n),le(n,p)),le(m,p)))))
THM	hless_eq_less_eq_mono	all (m:hnum. all (m:hnum. (n:hnum. all (m:hnum. (n:hnum. (p:hnum. all (m:hnum. (n:hnum. (p:hnum. (q:hnum. implies (m:hnum. (n:hnum. (p:hnum. (q:hnum. (and(le(m,p),le(n,q)) (m:hnum. (n:hnum. (p:hnum. (q:hnum. ,le(add(m,n),add(p,q)))))))
THM	hless_eq_refl	all(m:hnum. le(m,m))
THM	hless_imp_less_or_eq	all(m:hnum. all(n:hnum. implies(lt(m,n),le(m,n))))
THM	hless_mono_mult	all (m:hnum. all(n:hnum. all(p:hnum. implies(le(m,n),le(mult(m,p),mult(n,p))))))
THM	hright_sub_distrib	all (m:hnum. all (m:hnum. (n:hnum. all (m:hnum. (n:hnum. (p:hnum. equal (m:hnum. (n:hnum. (p:hnum. (mult(sub(m,n),p) (m:hnum. (n:hnum. (p:hnum. ,sub(mult(m,p),mult(n,p))))))
THM	hleft_sub_distrib	all (m:hnum. all (m:hnum. (n:hnum. all (m:hnum. (n:hnum. (p:hnum. equal (m:hnum. (n:hnum. (p:hnum. (mult(p,sub(m,n)) (m:hnum. (n:hnum. (p:hnum. ,sub(mult(p,m),mult(p,n))))))
THM	hless_add_1	all (m:hnum. all (m:hnum. (n:hnum. implies(lt(n,m),exists(p:hnum. equal(m,add(n,add(p,1)))))))
THM	hexp_add	all (p:hnum. all (p:hnum. (q:hnum. all (p:hnum. (q:hnum. (n:hnum. equal(exp(n,add(p,q)),mult(exp(n,p),exp(n,q))))))
THM	hnot_odd_eq_even	all(n:hnum. all(m:hnum. not(equal(suc(add(n,n)),add(m,m)))))
THM	hmult_suc_eq	all (p:hnum. all (p:hnum. (m:hnum. all (p:hnum. (m:hnum. (n:hnum. equal (p:hnum. (m:hnum. (n:hnum. (equal(mult(n,suc(p)),mult(m,suc(p))) (p:hnum. (m:hnum. (n:hnum. ,equal(n,m)))))
THM	hmult_exp_mono	all (p:hnum. all (p:hnum. (q:hnum. all (p:hnum. (q:hnum. (n:hnum. all (p:hnum. (q:hnum. (n:hnum. (m:hnum. equal (p:hnum. (q:hnum. (n:hnum. (m:hnum. (equal (p:hnum. (q:hnum. (n:hnum. (m:hnum. ((mult(n,exp(suc(q),p)) (p:hnum. (q:hnum. (n:hnum. (m:hnum. (,mult(m,exp(suc(q),p))) (p:hnum. (q:hnum. (n:hnum. (m:hnum. ,equal(n,m))))))
THM	hless_equal_antisym	all(n:hnum. all(m:hnum. implies(and(le(n,m),le(m,n)),equal(n,m))))
THM	hless_add_suc	all(m:hnum. all(n:hnum. lt(m,add(m,suc(n)))))
THM	hzero_less_eq	all(n:hnum. le(0,n))
THM	hless_eq_mono	all(n:hnum. all(m:hnum. equal(le(suc(n),suc(m)),le(n,m))))
THM	hless_or_eq_add	all(n:hnum. all(m:hnum. or(lt(n,m),exists(p:hnum. equal(n,add(p,m))))))
THM	hwop	all (P:hnum hbool. implies (P:hnum hbool. (exists(n:hnum. P(n)) (P:hnum hbool. ,exists (P:hnum hbool. ,(n:hnum. and (P:hnum hbool. ,(n:hnum. (P(n) (P:hnum hbool. ,(n:hnum. ,all(m:hnum. implies(lt(m,n),not(P(m))))))))
THM	hgen_induction	all (P:hnum hbool. implies (P:hnum hbool. (and (P:hnum hbool. ((P(0) (P:hnum hbool. (,all (P:hnum hbool. (,(n:hnum. implies (P:hnum hbool. (,(n:hnum. (all(m:hnum. implies(lt(m,n),P(m))) (P:hnum hbool. (,(n:hnum. ,P(n)))) (P:hnum hbool. ,all(n:hnum. P(n))))
THM	hda	all (k:hnum. all (k:hnum. (n:hnum. implies (k:hnum. (n:hnum. (lt(0,n) (k:hnum. (n:hnum. ,exists (k:hnum. (n:hnum. ,(r:hnum. exists (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. and (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. (equal(k,add(mult(q,n),r)) (k:hnum. (n:hnum. ,(r:hnum. (q:hnum. ,lt(r,n)))))))
THM	hmod_one	all(k:hnum. equal(mod(k,suc(0)),0))
THM	hdiv_less_eq	all(n:hnum. implies(lt(0,n),all(k:hnum. le(div(k,n),k))))

Origin Definitions Sections HOLlib Doc