Thm* l:T*. ||l|| > 0 hd(rev(l)) = l[(||l||-1)] hd_reverse

Thm* l,m:T*. ||l|| = 0 ||m|| > 0 tl((l @ m)) = tl(m) tl_append_back

Thm* l,m:T*. ||l|| > 0 tl((l @ m)) = (tl(l) @ m) tl_append_front

Thm* l:A*, f:(AB). ||l|| > 0 hd(map(f;l)) = f(hd(l)) hd_map

Thm* l,m:T*. ||l|| = 0 ||m|| > 0 hd((l @ m)) = hd(m) hd_append_back

Thm* l,m:T*. ||l|| > 0 hd((l @ m)) = hd(l) hd_append_front

Thm* l:T*. ||l|| > 0 hd(l) = l[0] hd_select

Thm* l:T*. ||rev(l)|| = ||l|| length_reverse

In prior sections: list 1 finite sets list 3 autom action sets det automata exponent