NO

Problem:
 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()))

Proof:
 Containment Processor: loop length: 1
                        terms:
                         nats()
                        context: :(0(),inc([]))
                        substitution:
                         
  Qed