PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
append
front
1
1.
T:
Type
2.
l:
T*
3.
m:
T*
4.
||l|| > 0
hd((l @ m)) = hd(l)
By:
RWH (LemmaC
Thm*
l:T*. ||l|| > 0
hd(l) = l[0]) 0
Generated subgoal:
1
(l @ m)[0] = l[0]
About:
(l @ m)[0] = l[0] hd((l @ m)) = hd(l)
l:T*. ||l|| > 0 
hd(l) = l[0])
0 (l @ m)[0] = l[0]
