(VAR x xs y ys z zs w ws) (RULES r(xs,ys,zs,nil) -> xs r(xs,nil,zs,cons(w,ws)) -> r(xs,xs,cons(succ(zero),zs), ws) r(xs,cons(y,ys),nil,cons(w,ws)) -> r(xs,xs,cons(succ(zero),nil), ws) r(xs,cons(y,ys),cons(z,zs),cons(w,ws)) -> r(ys, cons(y,ys), zs, cons(succ(zero),cons(w,ws))) ) (COMMENT from C. S. Lee. Program Termination Analysis in Polynomial Time. In Proc. 1st GPCE, LNCS 2487, pages 218-235, 2002. )