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