Def ||as|| == Case of as; nil 
0 ; a.as' ||as'||+1 (recursive)
Thm* 
S:ActionSet(Alph), si:S.car, nn:
, f:(nn
Alph), g:(Alphnn).
Fin(S.car) 
InvFuns(nn; Alph; f; g)
(n:.
RL:{y:{x:(S.car*)| 0 < ||x|| & ||x||
n+1 }| y[(||y||-1)] = si }.
(s:S.car. (w:Alph*. (S:w
si) = s) 
mem_f(S.car;s;RL))
||RL|| = n+1
& (i:||RL||, j:i. 
RL[i] = RL[j])
& (s:S.car. mem_f(S.car;s;RL) (w:Alph*. (S:wsi) = s))
& (k:.
knn
(RLa:S.car*.
(i:{1..||RL||
}, a:Alph.
mem_f(S.car;S.act(a,RL[i]);RL) mem_f(S.car;S.act(a,RL[i]);RLa))
& (a:Alph.
g(a) < k
mem_f(S.car;S.act(a,hd(RL));RL) mem_f(S.car;S.act(a,hd(RL));RLa))
& (s:S.car. mem_f(S.car;s;RLa) (w:Alph*. (S:wsi) = s)))))
reach_lemma
In prior sections: list 1 finite sets list 3 autom action sets