YES

2 decompositions
 #1 -----------
   3: hd(:(x1,x2)) -> x1

 #2 -----------
   1: nats() -> :(0(),inc(nats()))
   2: inc(:(x1,x2)) -> :(s(x1),inc(x2))
   4: tl(:(x1,x2)) -> x2
   5: inc(tl(nats())) -> tl(inc(nats()))

@Jouannaud and Kirchner's criterion
--- R
   3: hd(:(x1,x2)) -> x1

--- S
   3: hd(:(x1,x2)) -> x1


@Rule Labeling
--- R
   1: nats() -> :(0(),inc(nats()))
   2: inc(:(x1,x2)) -> :(s(x1),inc(x2))
   4: tl(:(x1,x2)) -> x2
   5: inc(tl(nats())) -> tl(inc(nats()))

--- S
   1: nats() -> :(0(),inc(nats()))
   2: inc(:(x1,x2)) -> :(s(x1),inc(x2))
   4: tl(:(x1,x2)) -> x2
   5: inc(tl(nats())) -> tl(inc(nats()))