THM	phole_aux	n:{1...}. f:(n + 1) n. i:(n + 1). j:{(i + 1)..(n + 1)}. 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
THM	one_one_sym	T,S:. 1-1-Corresp(T;S) 1-1-Corresp(S;T)
DISP	action_set_df	ActionSet{<i:le>}(<T:T:*>)== ActionSet{<i>}(<T>) ActionSet(<T:T:*>)== ActionSet(<T>)
ABS	action_set	ActionSet(T) == car: (T car car)
THM	action_set_wf	T:. ActionSet(T) '
DISP	aset_car_df	<a:aset:E>.car== <a>.car
ABS	aset_car	a.car == a.1
THM	aset_car_wf	T:. a:ActionSet(T). a.car
DISP	aset_act_df	<a:aset:E>.act== <a>.act
ABS	aset_act	a.act == a.2
THM	aset_act_wf	T:. a:ActionSet(T). a.act T a.car a.car
ML	create_action_set	Class Declaration for: s ActionSet(T) Long Name: action_set Short Name: aset Parameters: T : Fields: ([example]) car : ([example]) act : T car car Universe: '
THM	ex1_of_aset	<, x,y.0> ActionSet{1}()
THM	ex2_of_aset	<, x,y.x + y> ActionSet{1}()
THM	ex3_of_aset	T,S:. a:T S S. <S, a> ActionSet(T)
THM	ex4_of_aset	<, x,y.x * y> ActionSet{1}()
THM	ex5_of_aset	< List, z,l.(z::l)> ActionSet{1}()
THM	ex6_of_aset	< List, u,l.rev(l)> ActionSet{1}(Unit)
THM	nat_is_int	n:. n
DISP	factorial_df	(<n:n:*>)! == (<n>)!
ML	factorial_ml	(n)! ==r if (n = 0) then 1 else n * (n - 1)! fi
THM	factorial_wf	n:. (n)!
THM	ex1_of_factorial	(0)! = 1
ABS	multi_action	multi_action(l; s; ASet) == Y (multi_action,l,s,ASet. if null(l) then s else ASet.act hd(rev(l)) (multi_action ASet.act rev(tl(rev(l))) s) fi ) l s ASet
DISP	maction_df	(<S:ActionSet:*>:<L:list:*><s:init:*>)== (<S>:<L><s>)
ML	maction_ml	(S:Ls)==r if null(L) then s else S.act hd(L) (S:tl(L)s) fi
THM	maction_wf	Alph:. S:ActionSet(Alph). L:Alph List. s:S.car. (S:Ls) S.car
THM	comb_for_maction_wf	(Alph,S,L,s,z.(S:Ls)) Alph: S:ActionSet(Alph) L:Alph List s:S.car True S.car
THM	maction_lemma	Alph:. S:ActionSet(Alph). s:S.car. L1,L2,L:Alph List. (S:L1s) = (S:L2s) (S:L @ L1s) = (S:L @ L2s)
DISP	lpower_df	(<L:L:*><n:n:*>)== (<L><n>)
ML	lpower_ml	(Ln)==r if (n = 0) then [] else (Ln - 1) @ L fi
THM	lpower_wf	Alph:. L:Alph List. n:. (Ln) Alph List
THM	lpower_alt	Alph:. L:Alph List. n:. (Ln) = if (n = 0) then [] else L @ (Ln - 1) fi
THM	pump_theorem	Alph:. S:ActionSet(Alph). N:. s:S.car. #(S.car)=N (A:Alph List N < ||A|| (a,b,c:Alph List (0 < ||b|| A = (a @ b) @ c) (k:. (S:(a @ (bk)) @ cs) = (S:As))))
THM	pump_thm_cor	n:. Alph:. S:ActionSet(Alph). s,f:S.car. #(S.car)=n (l:Alph List. (S:ls) = f) (l:Alph List. ||l|| n (S:ls) = f)
DISP	n0n1_df	n0n1(<n:n:*>)== n0n1(<n>)
ABS	n0n1	n0n1(n) == (0::[]n) @ (1::[]n)
THM	n0n1_wf	n:. n0n1(n) List
THM	comb_for_n0n1_wf	(n,z.n0n1(n)) n: True List
DISP	el_counter_df	||<e:e:*>:<L:L:*>||== ||<e>:<L>||
ML	el_counter_ml	||e:L|| ==r if null(L) then 0 if (e = hd(L)) then 1 + ||e:tl(L)|| else ||e:tl(L)|| fi
THM	el_counter_wf	n:. L: List. ||n:L||
THM	comb_for_el_counter_wf	(n,L,z.||n:L||) n: L: List True
THM	counter_of_nil	e:. ||e:[]|| = 0
THM	counter_append	e:. L,M: List. ||e:L @ M|| = ||e:L|| + ||e:M||
THM	counter_lpower	e:. L: List. n:. ||e:(Ln)|| = n * ||e:L||
THM	n0n1_irregular	S:ActionSet(). s,q:S.car. (n:. #(S.car)=n ) (k:. (S:n0n1(k)s) = q) (L: List. (S:Ls) = q (k:. (L = n0n1(k))))

the other theories