Thm* n:, m:, k:(nm). l:n*. ||l|| = m & en(l) = k en_surj

Thm* n:, l:n*. en(l) (n||l||) en_bound

Thm* n:, l:n*. en(l) < (n||l||) en_ubound

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

Thm* R:(Alph*Alph*Prop), n:. (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))) (a,b,c:Alph*. a':Alph*. ||a'|| < nn & R((a @ b),a' @ b) & R((a @ c),a' @ c)) auto2_lemma_4

Thm* R:(Alph*Alph*Prop), n:. (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))) (a,b,c:Alph*. ||a||nn (a':Alph*. ||a'|| < ||a|| & R((a @ b),a' @ b) & R((a @ c),a' @ c))) auto2_lemma_3

Thm* n:, m:, l1,l2:n*. ||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2 en_inj

Thm* l:T*. ||l|| = 0 l = nil zero_length_imp_nil

In prior sections: list 1 finite sets list 3 autom