YES ---- CR(R) ---- Hot decreasingness. R: nats() -> :(0(),inc(nats())) inc(:(x,y)) -> :(s(x),inc(y)) inc(tl(nats())) -> tl(inc(nats())) hd(:(x,y)) -> x tl(:(x,y)) -> y d(:(x,y)) -> :(x,:(x,d(y))) C: Label: [nats() -> :(0(),inc(nats()))] = 0 [inc(:(x,y)) -> :(s(x),inc(y))] = 0 [inc(tl(nats())) -> tl(inc(nats()))] = 1 [hd(:(x,y)) -> x] = 0 [tl(:(x,y)) -> y] = 0 [d(:(x,y)) -> :(x,:(x,d(y)))] = 0