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