Selected Objects

THM	nat_add	n,m:. n+m
THM	nat_mul	n,m:. nm
THM	zero_length_imp_nil	l:T*. ||l|| = 0 l = nil
THM	rem_quo_unique	n:, r1,r2:n, q1,q2:. r1+q1n = r2+q2n r1 = r2 & q1 = q2
THM	div_lt_lbound	a:, n:, k:. a < nk (a n) < k
def	en	(rec) en(l) == if null(l) 0 else hd(l)+en(tl(l))n fi
THM	en_inj	n:, m:, l1,l2:n*. ||l1|| = m & ||l2|| = m en(l1) = en(l2) l1 = l2
def	exp	(rec) (basepower) == if power=0 1 else base(basepower-1) fi
THM	exp_functionality	n1,n2,k1,k2:. n1 = n2 k1 = k2 (n1k1) = (n2k2)
THM	exp_zero	m:. (0m) = 0
THM	exp_non_zero	m:, n:. 0 < (mn)
THM	exp_base	n:. (n0) = 1
THM	exp_step	n,k:. 0 < k (nk) = n(nk-1)
THM	fun_enumer	n,m:. f:((mn)(nm)). Bij(mn; (nm); f)
THM	auto2_lemma_0	P:(TProp). (x:T. Dec(P(x))) & Dec(x:T. P(x)) Dec(x:T. P(x))
THM	auto2_lemma_1	P,Q:(TProp). (t:T. P(t) Q(t)) ({t:T| P(t) } ~ {t:T| Q(t) })
THM	auto2_lemma_3	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)))
THM	auto2_lemma_4	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))
THM	auto2_lemma_5	n:. Fin(Alph) Fin({l:(Alph*)| ||l|| = n })
THM	auto2_lemma_6	R:(TProp). Fin(T) & (t:T. Dec(R(t))) Dec(t:T. R(t))
THM	auto2_lemma_7	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)))
THM	auto2_lemma_8	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)))
THM	fun_preserves_fin	Fin(S) & Fin(T) Fin(ST)
THM	en_ubound	n:, l:n*. en(l) < (n||l||)
THM	en_bound	n:, l:n*. en(l) (n||l||)
THM	en_surj	n:, m:, k:(nm). l:n*. ||l|| = m & en(l) = k
def	geom_series	(rec) (qn) == if n=0 0 else (qn-1)+(qn-1) fi
THM	geom_series_step	q,n:. (qn+1) = (qn)+(qn)
THM	geom_ndecrease	q,n,i:. (qn)(qn+i)
THM	geom_speed_lbound	q,n:, i:. (qn)+(qn)(qn+i)
THM	geom_n_unique	q:, n:, i:, r1:(qn), r2:(qn+i). (qn)+r1 = (qn+i)+r2 False
THM	geom_unique	q:, n1,n2:, r1:(qn1), r2:(qn2). (qn1)+r1 = (qn2)+r2 n1 = n2 & r1 = r2
THM	geom_series_limit	q:, a:. n:. (qn) a < (qn+1)
def	enum	enum(l) == (q||l||)+en(l)
THM	enum_inj	q:, l1,l2:q*. enum(l1) = enum(l2) l1 = l2
THM	enum_surj	q:, a:. l:q*. enum(l) = a
THM	list_1_1_nat	q:. (q*) ~