PrintForm
Definitions
nfa
1
Sections
AutomataTheory
Doc
At:
hd
reverse
1
2
2
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) @ [u])) = v[(||v||+1-1-1)]
By:
RWH (LemmaC
Thm*
l,m:T*. ||l|| > 0
hd((l @ m)) = hd(l)) 0
Generated subgoal:
1
||v||+1 > 0
hd(rev(v)) = v[(||v||+1-1-1)]
About:
||v||+1 > 0 
hd(rev(v)) = v[(||v||+1-1-1)] hd(rev(v)) = v[(||v||-1)]
||v|| = 0 ||v||+1 > 0 hd((rev(v) @ [u])) = v[(||v||+1-1-1)]
l,m:T*. ||l|| > 0 hd((l @ m)) = hd(l))
0 ||v||+1 > 0 hd(rev(v)) = v[(||v||+1-1-1)]
