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