list 3 autom Sections AutomataTheory Doc

Def Fin(s) == n:, f:(ns). Bij(n; s; f)

Thm* L,La:T*. Fin(T) (La':T*. (t:T. mem_f(T;t;La) mem_f(T;t;L) mem_f(T;t;La')) & (t:T. mem_f(T;t;La') mem_f(T;t;La)) & (||La'||1 mem_f(T;hd(La');L))) shorten_list

Thm* s:S, l:S*. Fin(S) Dec(mem_f(S;s;l)) mem_f_dec

In prior sections: finite sets