Thm* Fin(S) & Fin(T) Fin(ST) fun_preserves_fin

Thm* R:(Alph*Alph*Prop), n:, L:(Alph*), m:. (x:Alph*. R(x,x)) & (x,y:Alph*. R(x,y) R(y,x)) & (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)) & (w:(nAlph*). l:Alph*. i:n. R(l,w(i))) & (v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))) & Fin(Alph) (x,y:Alph*. Dec(l:Alph*. L(l @ x) = L(l @ y))) auto2_lemma_8

Thm* R:(Alph*Alph*Prop), n:, L:(Alph*), m:. (x:Alph*. R(x,x)) & (x,y:Alph*. R(x,y) R(y,x)) & (x,y,z:Alph*. R(x,y) & R(y,z) R(x,z)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)) & (w:(nAlph*). l:Alph*. i:n. R(l,w(i))) & (v:(mAlph*). l:Alph*. L(l) (i:m. R(l,v(i)))) & Fin(Alph) (x,y:Alph*. Dec(l:Alph*. L(l @ x) = L(l @ y))) auto2_lemma_7

Thm* R:(TProp). Fin(T) & (t:T. Dec(R(t))) Dec(t:T. R(t)) auto2_lemma_6

Thm* n:. Fin(Alph) Fin({l:(Alph*)| ||l|| = n }) auto2_lemma_5

In prior sections: finite sets list 3 autom