e:
, L:*, n:
. ||e:(L
n)|| = n
||e:L|| 
counter_lpower
n) == if n=
0
nil else (Ln-1) @ L fi (recursive)
Thm* e:, L:*, n:. ||e:(Ln)|| = n||e:L|| counter_lpower
Thm* S:ActionSet(Alph), N:
, s:S.car.
#(S.car)=N 
(A:Alph*.
N < ||A||
(
a,b,c:Alph*.
0 < ||b|| & A = ((a @ b) @ c) & (k:. (S:(a @ (bk)) @ c
s) = (S:As))))
pump_theorem
Thm* L:Alph*, n:. (Ln) = if n=0 nil else L @ (Ln-1) fi lpower_alt