PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
map
1
1.
A:
Type
2.
B:
Type
3.
l:
A*
4.
f:
A
B
5.
||l|| > 0
hd(map(f;l)) = f(hd(l))
By:
RWH (LemmaC
Thm*
l:T*. ||l|| > 0
hd(l) = l[0]) 0
Generated subgoal:
1
map(f;l)[0] = f(l[0])
About:
map(f;l)[0] = f(l[0])
B hd(map(f;l)) = f(hd(l))
l:T*. ||l|| > 0 
hd(l) = l[0])
0 map(f;l)[0] = f(l[0])
