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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 1
   inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -2|[]-> tl(inc(nats()))
  Redundant Rules Transformation:
   nats() -> :(0(),inc(nats()))
   inc(:(x,y)) -> :(s(x),inc(y))
   hd(:(x,y)) -> x
   tl(:(x,y)) -> y
   d(:(x,y)) -> :(x,:(x,d(y)))
   Church Rosser Transformation Processor (no redundant rules):
    strict:
     d(:(x,y)) -> :(x,:(x,d(y)))
     tl(:(x,y)) -> y
     hd(:(x,y)) -> x
     inc(:(x,y)) -> :(s(x),inc(y))
     nats() -> :(0(),inc(nats()))
    weak:
     
    critical peaks: 0
    Closedness Processor (*feeble*):
     
     Qed