YES

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 (redex):
  strict:
   
  weak:
   inc(tl(nats())) -> tl(inc(nats()))
   tl(:(x,y)) -> y
   hd(:(x,y)) -> x
   inc(:(x,y)) -> :(s(x),inc(y))
   nats() -> :(0(),inc(nats()))
  critical peaks: 1
   inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -4|[]-> tl(inc(nats()))
  Shift Processor (no label):
   strict:
    
   weak:
    
   Shift Processor lab=left (dd):
    strict:
     inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
     inc(tl(nats())) -> tl(inc(nats()))
     inc(tl(:(0(),inc(nats())))) -> inc(inc(nats()))
     tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
     tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
     tl(:(s(0()),inc(inc(nats())))) -> inc(inc(nats()))
    weak:
     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()))
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [s](x0) = 2x0,
      
      [0] = 0,
      
      [:](x0, x1) = x0 + 4x1,
      
      [hd](x0) = x0 + 5,
      
      [nats] = 0,
      
      [tl](x0) = x0,
      
      [inc](x0) = 2x0
     orientation:
      inc(tl(nats())) = 0 >= 0 = inc(tl(:(0(),inc(nats()))))
      
      inc(tl(nats())) = 0 >= 0 = tl(inc(nats()))
      
      inc(tl(:(0(),inc(nats())))) = 0 >= 0 = inc(inc(nats()))
      
      tl(inc(nats())) = 0 >= 0 = tl(inc(:(0(),inc(nats()))))
      
      tl(inc(:(0(),inc(nats())))) = 0 >= 0 = tl(:(s(0()),inc(inc(nats()))))
      
      tl(:(s(0()),inc(inc(nats())))) = 0 >= 0 = inc(inc(nats()))
      
      nats() = 0 >= 0 = :(0(),inc(nats()))
      
      inc(:(x,y)) = 2x + 8y >= 2x + 8y = :(s(x),inc(y))
      
      hd(:(x,y)) = x + 4y + 5 >= x = x
      
      tl(:(x,y)) = x + 4y >= y = y
     problem:
      strict:
       inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
       inc(tl(nats())) -> tl(inc(nats()))
       inc(tl(:(0(),inc(nats())))) -> inc(inc(nats()))
       tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
       tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
       tl(:(s(0()),inc(inc(nats())))) -> inc(inc(nats()))
      weak:
       nats() -> :(0(),inc(nats()))
       inc(:(x,y)) -> :(s(x),inc(y))
       tl(:(x,y)) -> y
       inc(tl(nats())) -> tl(inc(nats()))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [s](x0) = 2x0,
       
       [0] = 0,
       
       [:](x0, x1) = x0 + 2x1,
       
       [nats] = 0,
       
       [tl](x0) = 4x0 + 2,
       
       [inc](x0) = 4x0
      orientation:
       inc(tl(nats())) = 8 >= 8 = inc(tl(:(0(),inc(nats()))))
       
       inc(tl(nats())) = 8 >= 2 = tl(inc(nats()))
       
       inc(tl(:(0(),inc(nats())))) = 8 >= 0 = inc(inc(nats()))
       
       tl(inc(nats())) = 2 >= 2 = tl(inc(:(0(),inc(nats()))))
       
       tl(inc(:(0(),inc(nats())))) = 2 >= 2 = tl(:(s(0()),inc(inc(nats()))))
       
       tl(:(s(0()),inc(inc(nats())))) = 2 >= 0 = inc(inc(nats()))
       
       nats() = 0 >= 0 = :(0(),inc(nats()))
       
       inc(:(x,y)) = 4x + 8y >= 2x + 8y = :(s(x),inc(y))
       
       tl(:(x,y)) = 4x + 8y + 2 >= y = y
      problem:
       strict:
        inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
        tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
        tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
       weak:
        nats() -> :(0(),inc(nats()))
        inc(:(x,y)) -> :(s(x),inc(y))
      Bounds Processor:
       bound: 1
       enrichment: match-rt
       automaton:
        final states: {7}
        transitions:
         tl1(46) -> 7*
         tl1(16) -> 17*
         01() -> 15*
         tl0(7) -> 7*
         inc0(7) -> 7*
         inc1(17) -> 14,7
         inc1(13) -> 14*
         inc1(14) -> 50*
         inc1(50) -> 14*
         inc1(7) -> 14*
         inc1(16) -> 46*
         s0(7) -> 7*
         nats0() -> 7*
         00() -> 7*
         :0(7,7) -> 7*
         nats1() -> 13*
         s1(7) -> 15*
         s1(15) -> 51*
         s1(51) -> 15*
         :1(51,50) -> 50,14,7,46
         :1(15,14) -> 50,14,13,7,16
       problem:
        strict:
         tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
         tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
        weak:
         nats() -> :(0(),inc(nats()))
         inc(:(x,y)) -> :(s(x),inc(y))
       Bounds Processor:
        bound: 1
        enrichment: match-rt
        automaton:
         final states: {7}
         transitions:
          tl1(17) -> 7*
          01() -> 15*
          tl0(7) -> 7*
          inc0(7) -> 7*
          inc1(13) -> 14*
          inc1(14) -> 32*
          inc1(32) -> 14*
          inc1(7) -> 14*
          inc1(16) -> 17*
          s0(7) -> 7*
          nats0() -> 7*
          00() -> 7*
          :0(7,7) -> 7*
          nats1() -> 13*
          s1(7) -> 15*
          s1(33) -> 15*
          s1(15) -> 33*
          :1(15,14) -> 32,14,13,7,16
          :1(33,32) -> 32,14,7,17
        problem:
         strict:
          tl(inc(:(0(),inc(nats())))) -> tl(:(s(0()),inc(inc(nats()))))
         weak:
          nats() -> :(0(),inc(nats()))
          inc(:(x,y)) -> :(s(x),inc(y))
        Bounds Processor:
         bound: 1
         enrichment: match-rt
         automaton:
          final states: {7}
          transitions:
           tl1(19) -> 7*
           01() -> 17*
           tl0(7) -> 7*
           inc0(7) -> 7*
           inc1(15) -> 16*
           inc1(14) -> 15*
           inc1(7) -> 15*
           inc1(16) -> 15*
           s0(7) -> 7*
           nats0() -> 7*
           00() -> 7*
           :0(7,7) -> 7*
           nats1() -> 14*
           s1(7) -> 17*
           s1(18) -> 17*
           s1(17) -> 18*
           :1(17,15) -> 16,15,14,7
           :1(18,16) -> 16,15,7,19
         problem:
          strict:
           
          weak:
           nats() -> :(0(),inc(nats()))
           inc(:(x,y)) -> :(s(x),inc(y))
         Shift Processor (ldh) lab=left (force):
          strict:
           
          weak:
           
          Decreasing Processor:
           The following diagrams are decreasing:
           peak:
            inc(tl(:(0(),inc(nats())))) <-0|0,0[==1]- inc(tl(nats())) -4|[==1]-> tl(inc(nats()))
           joins (1):
            inc(tl(:(0(),inc(nats())))) -3|0[>>0]-> inc(inc(nats()))
            tl(inc(nats())) -0|0,0[>>0]-> tl(inc(:(0(),inc(nats())))) -1|0[>>0]-> 
             tl(:(s(0()),inc(inc(nats())))) -3|[>>0]-> inc(inc(nats()))
           Qed