PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: hd reverse 1 2 2 1 1 1
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(rev(v)) = v[(||v||+1-1-1)]
By: Analyze 5
Generated subgoal:

15. ||v|| = 0
6. hd(rev(v)) = v[(||v||-1)]
||v||+1 > 0 hd(rev(v)) = v[(||v||+1-1-1)]

About:
impliesaddnatural_numberequalsubtractuniverselistint