lslr(x,v) * lsr(v,y) |- lslr(x,y)