||nil|| = 0 
hd((nil @ m)) = hd(m)5. u: T
6. v: T*
7. ||v|| = 0
hd((v @ m)) = hd(m) ||u.v|| = 0 hd(((u.v) @ m)) = hd(m) hd((l @ m)) = hd(m)| 1 | 4. ||m|| > 0 ||nil|| = 0 hd((nil @ m)) = hd(m) |
| 2 | 4. ||m|| > 0 5. u: T 6. v: T* 7. ||v|| = 0 hd((v @ m)) = hd(m) ||u.v|| = 0 hd(((u.v) @ m)) = hd(m) |
About:
 |  |  |  |  |  |  |  |