PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
reverse
1
2
1
1
2
3
1.
T:
Type
2.
l:
T*
3.
u:
T
4.
v:
T*
5.
||v|| > 0
hd(rev(v)) = v[(||v||-1)]
6.
||v|| = 0
||v||+1 > 0
hd([u]) = u
By:
Reduce 0
Generated subgoals:
None
About:
hd(rev(v)) = v[(||v||-1)]
||v||+1 > 0 hd([u]) = u
