Thm* q:. (q*) ~ list_1_1_nat

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

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

Thm* q:, a:. n:. (qn) a < (qn+1) geom_series_limit

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* q,n:, i:. (qn)+(qn)(qn+i) geom_speed_lbound

Thm* q,n,i:. (qn)(qn+i) geom_ndecrease

Thm* q,n:. (qn+1) = (qn)+(qn) geom_series_step

Thm* q,n:. (qn) geom_series_wf

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* n:. Fin(Alph) Fin({l:(Alph*)| ||l|| = n }) auto2_lemma_5

Thm* n,m:. f:((mn)(nm)). Bij(mn; (nm); f) fun_enumer

Thm* n,k:. 0 < k (nk) = n(nk-1) exp_step

Thm* n:. (n0) = 1 exp_base

Thm* m:, n:. 0 < (mn) exp_non_zero

Thm* n,k:. (nk) exp_wf2

Thm* n1,n2,k1,k2:. n1 = n2 k1 = k2 (n1k1) = (n2k2) exp_functionality

Thm* n,k:. (nk) exp_wf

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* a:, n:, k:. a < nk (a n) < k div_lt_lbound

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

Thm* n,m:. nm nat_mul

Thm* n,m:. n+m nat_add

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