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:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 1
   inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -4|[]-> 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
   Qed (ToyamaOyamaguchi95Cor22)