THM	not_dec_is_dec	A:. P:A . (x:A. P x (P x)) ((x:A. (P x)) (x:A. (P x))) (x:A. P x) (x:A. P x)
THM	rect_enumer	n,m:. f:(n m) (n * m). Bij(n m;(n * m);f)
DISP	finite_df	Fin(<s:s:*>)== Fin(<s>)
ABS	finite	Fin(s) == n:. f:n s. Bij(n;s;f)
THM	finite_wf	T:. Fin(T)
THM	comb_for_finite_wf	(T,z.Fin(T)) T: True
THM	nsub_is_finite	n:. Fin(n)
THM	bool_is_finite	Fin()
THM	one2one_preserves_fin	T,U:. 1-1-Corresp(T;U) Fin(T) Fin(U)
THM	fin_iff_1_1_nsub	T:. Fin(T) (m:. 1-1-Corresp(m;T))
THM	div_bounds_2	n:. x:(n * n). x n < n
THM	prod_fin_is_fin	T:. t:T. Fin(T) Fin(T T)
THM	fin_dec_fin	n:. T:. B:T . 1-1-Corresp(n;T) (t:T. Dec(B t)) (m:. 1-1-Corresp(m;{t:T| B t} ))
THM	finite_decidable_subset	T:. B:T . Fin(T) (t:T. Dec(B t)) Fin({t:T| B t} )
THM	one_one_preser_fin	T,S:. Fin(T) 1-1-Corresp(T;S) Fin(S)
THM	set_function	S,T:. R:S T . (s:S. Dec(t:T. R s t)) (f:{s:S| t:T. R s t} T. s:{s:S| t:T. R s t} . R s (f s))
THM	inv_of_fin_is_fin	T,S:. f:T S. Fin(S) (s:S. Dec(t:T. f t = s)) Fin(x,y:T//(f x = f y))
THM	fin_is_decid	T:. Fin(T) (x,y:T. Dec(x = y))
THM	fin_dist_func	St:. Fin(St) (eq:St St . x,y:St. (eq x y) x = y)
THM	decid_is_comp	T:. f:T . (t:T. Dec(f t)) (g:T . t:T. f t (g t))
THM	auto2_list_ind	Alph:. P:Alph List . (n: (l:Alph List. ||l|| < n P l) (l:Alph List. ||l|| = n P l)) (l:Alph List. P l)
THM	one_one_sym	T,S:. 1-1-Corresp(T;S) 1-1-Corresp(S;T)
THM	auto2_lemma_0	T:. P:T . (x:T. Dec(P x)) Dec(x:T. (P x)) Dec(x:T. P x)
THM	auto2_lemma_1	T:. P,Q:T . (t:T. P t Q t) 1-1-Corresp({t:T| P t} ;{t:T| Q t} )
THM	auto2_lemma_3	Alph:. R:Alph List Alph List . n:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (a,b,c:Alph List. ||a|| n * n (a':Alph List ||a'|| < ||a|| R (a @ b) (a' @ b) R (a @ c) (a' @ c)))
THM	auto2_lemma_4	Alph:. R:Alph List Alph List . n:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (a,b,c:Alph List. a':Alph List ||a'|| < n * n R (a @ b) (a' @ b) R (a @ c) (a' @ c))
THM	auto2_lemma_5	Alph:. n:. Fin(Alph) Fin({l:Alph List| ||l|| = n} )
THM	auto2_lemma_6	T:. R:T . Fin(T) (t:T. Dec(R t)) Dec(t:T. R t)
THM	auto2_lemma_7	Alph:. R:Alph List Alph List . n:. L:Alph List . m:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (v:m Alph List. l:Alph List. (L l) (i:m. R l (v i))) Fin(Alph) (x,y:Alph List. Dec(l:Alph List. L (l @ x) = L (l @ y)))
THM	auto2_lemma_8	Alph:. R:Alph List Alph List . n:. L:Alph List . m:. (x:Alph List. R x x) (x,y:Alph List. R x y R y x) (x,y,z:Alph List. R x y R y z R x z) (x,y,z:Alph List. R x y R (z @ x) (z @ y)) (w:n Alph List. l:Alph List. i:n. R l (w i)) (v:m Alph List. l:Alph List. (L l) (i:m. R l (v i))) Fin(Alph) (x,y:Alph List. Dec(l:Alph List. L (l @ x) = L (l @ y)))
COM	phole_descr	Pigeon-hole principle
THM	phole_aux	n:{1...}. f:(n + 1) n. i:(n + 1). j:i. f i = f j
THM	phole_lemma	n:{1...}. m:{n + 1...}. f:m n. i,j:m. i < j f i = f j
DISP	card_df	#(<t:t:*>)=<n:n:*> == #(<t>)=<n>
ABS	card	#(t)=n == 1-1-Corresp(t;n)
THM	card_wf	t:. n:. #(t)=n

the other theories