||u.v|| > 0 
hd(rev(u.v)) = v[(||u.v||-1-1)] hd(rev(v)) = v[(||v||-1)]
||v|| = 0 ||u.v|| > 0 hd(rev(u.v)) = (u.v)[(||u.v||-1)]
a:T, as:T*, i:
. 0 < i i
||as|| (a.as)[i] = as[(i-1)])
0| 1 | ||u.v|| > 0 hd(rev(u.v)) = v[(||u.v||-1-1)] |
About:
 |  |  |  |  |
 |  |  |  |  |