nfa
1
Sections
AutomataTheory
Doc
Def
map(f;as) == Case of as; nil
nil ; a.as'
f(a).map(f;as') (recursive)
Thm*
l:A*, f:(A
B). ||l|| > 0
hd(map(f;l)) = f(hd(l)) hd_map
In prior sections:
list
1
l:A*, f:(A
B). ||l|| > 0 
hd(map(f;l)) = f(hd(l)) hd_map
nil ; a.as' f(a).map(f;as') (recursive)
l:A*, f:(AB). ||l|| > 0 hd(map(f;l)) = f(hd(l)) hd_map