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