THM	nat_add	n,m:. n + m
THM	nat_mul	n,m:. n * m
THM	zero_length_imp_nil	T:. l:T List. ||l|| = 0 l = []
THM	rem_quo_unique	n:. r1,r2:n. q1,q2:. r1 + q1 * n = r2 + q2 * n r1 = r2 q1 = q2
THM	div_lt_lbound	a:. n:. k:. a < n * k a n < k
DISP	en_df	en(<l:l:*>;<n:n:*>)== en(<l>) en(<l:l:*>)== en(<l>)
ML	en_ml	en(l)==r if null(l) then 0 else hd(l) + en(tl(l)) * n fi
THM	en_wf	n:. l:n List. en(l)
THM	en_inj	n:. m:. l1,l2:n List. ||l1|| = m ||l2|| = m en(l1) = en(l2) l1 = l2
DISP	exp_df	(<base:base:*><power:power:*>)== (<base><power>)
ML	exp_ml	(basepower) ==r if (power = 0) then 1 else base * (basepower - 1) fi
THM	exp_wf	n,k:. (nk)
THM	exp_functionality	n1,n2,k1,k2:. n1 = n2 k1 = k2 (n1k1) = (n2k2)
THM	comb_for_exp_wf	(n,k,z.(nk)) n: k: True
THM	exp_wf2	n,k:. (nk)
THM	comb_for_exp_wf2	(n,k,z.(nk)) n: k: True
THM	exp_zero	m:. (0m) = 0
THM	exp_non_zero	m:. n:. 0 < (mn)
THM	exp_base	n:. (n0) = 1
THM	exp_step	n,k:. 0 < k (nk) = n * (nk - 1)
THM	fun_enumer	n,m:. f:(m n) (nm). Bij(m n;(nm);f)
THM	fun_preserves_fin	S,T:. Fin(S) Fin(T) Fin(S T)
THM	en_ubound	n:. l:n List. en(l) < (n||l||)
THM	en_bound	n:. l:n List. en(l) (n||l||)
THM	en_surj	n:. m:. k:(nm). l:n List. ||l|| = m en(l) = k
DISP	geom_series_df	(<q:q:*><n:n:*>)== (<q><n>)
ML	geom_series_ml	(qn)==r if (n = 0) then 0 else (qn - 1) + (qn - 1) fi
THM	geom_series_wf	q,n:. (qn)
THM	geom_series_step	q,n:. (qn + 1) = (qn) + (qn)
THM	comb_for_geom_series_wf	(q,n,z.(qn)) q: n: True
THM	geom_ndecrease	q,n,i:. (qn) (qn + i)
THM	geom_speed_lbound	q,n:. i:. (qn) + (qn) (qn + i)
THM	geom_n_unique	q:. n:. i:. r1:(qn). r2:(qn + i). (qn) + r1 = (qn + i) + r2 False
THM	geom_unique	q:. n1,n2:. r1:(qn1). r2:(qn2). (qn1) + r1 = (qn2) + r2 n1 = n2 r1 = r2
THM	geom_series_limit	q:. a:. n:. (qn) a < (qn + 1)
DISP	enum_df	enum(<l:l:*>;<q:q:*>)== enum(<l>) enum(<l:l:*>)== enum(<l>)
ABS	enum	enum(l) == (q||l||) + en(l)
THM	enum_wf	q:. l:q List. enum(l)
THM	enum_inj	q:. l1,l2:q List. enum(l1) = enum(l2) l1 = l2
THM	enum_surj	q:. a:. l:q List. enum(l) = a
THM	list_1_1_nat	q:. 1-1-Corresp(q List;)

the other theories