Thm* q:. (q*) ~ list_1_1_nat

Thm* q:, a:. l:q*. enum(l) = a enum_surj

Thm* q:, l1,l2:q*. enum(l1) = enum(l2) l1 = l2 enum_inj

Thm* q:, l:q*. enum(l) enum_wf

Thm* q:, n1,n2:, r1:(qn1), r2:(qn2). (qn1)+r1 = (qn2)+r2 n1 = n2 & r1 = r2 geom_unique

Thm* q:, n:, i:, r1:(qn), r2:(qn+i). (qn)+r1 = (qn+i)+r2 False geom_n_unique

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* 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:(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:. f:((mn)(nm)). Bij(mn; (nm); f) fun_enumer

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

Thm* n:, l:n*. en(l) en_wf

Thm* n:, r1,r2:n, q1,q2:. r1+q1n = r2+q2n r1 = r2 & q1 = q2 rem_quo_unique

In prior sections: int 1 bool 1 int 2 list 1 finite sets list 3 autom