A transformation strategy for verifying logic programs on infinite lists