YES

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()))
  Shift Processor lab=left (dd) (force):
   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))
    inc(tl(nats())) -> tl(inc(nats()))
    hd(:(x,y)) -> x
    tl(:(x,y)) -> y
    d(:(x,y)) -> :(x,:(x,d(y)))
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [s](x0) = x0,
     
     [0] = 0,
     
     [:](x0, x1) = x0 + x1,
     
     [tl](x0) = x0,
     
     [nats] = 0,
     
     [d](x0) = 2x0,
     
     [hd](x0) = 6x0 + 2,
     
     [inc](x0) = x0
    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)) = x + y >= x + y = :(s(x),inc(y))
     
     hd(:(x,y)) = 6x + 6y + 2 >= x = x
     
     tl(:(x,y)) = x + y >= y = y
     
     d(:(x,y)) = 2x + 2y >= 2x + 2y = :(x,:(x,d(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))
      inc(tl(nats())) -> tl(inc(nats()))
      tl(:(x,y)) -> y
      d(:(x,y)) -> :(x,:(x,d(y)))
    Polynomial Interpretation Processor:
     dimension: 1
     interpretation:
      [s](x0) = x0,
      
      [0] = 0,
      
      [:](x0, x1) = x0 + x1,
      
      [tl](x0) = 2x0 + 2x0x0 + 1,
      
      [nats] = 0,
      
      [d](x0) = 2x0,
      
      [inc](x0) = x0
     orientation:
      inc(tl(nats())) = 1 >= 1 = inc(tl(:(0(),inc(nats()))))
      
      inc(tl(nats())) = 1 >= 1 = tl(inc(nats()))
      
      inc(tl(:(0(),inc(nats())))) = 1 >= 0 = inc(inc(nats()))
      
      tl(inc(nats())) = 1 >= 1 = tl(inc(:(0(),inc(nats()))))
      
      tl(inc(:(0(),inc(nats())))) = 1 >= 1 = tl(:(s(0()),inc(inc(nats()))))
      
      tl(:(s(0()),inc(inc(nats())))) = 1 >= 0 = inc(inc(nats()))
      
      nats() = 0 >= 0 = :(0(),inc(nats()))
      
      inc(:(x,y)) = x + y >= x + y = :(s(x),inc(y))
      
      tl(:(x,y)) = 2x + 2x*x + 4x*y + 2y + 2y*y + 1 >= y = y
      
      d(:(x,y)) = 2x + 2y >= 2x + 2y = :(x,:(x,d(y)))
     problem:
      strict:
       inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
       inc(tl(nats())) -> tl(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))
       inc(tl(nats())) -> tl(inc(nats()))
       d(:(x,y)) -> :(x,:(x,d(y)))
     Polynomial Interpretation Processor:
      dimension: 1
      interpretation:
       [s](x0) = x0,
       
       [0] = 0,
       
       [:](x0, x1) = 2x0 + x1,
       
       [tl](x0) = 2x0 + 2x0x0 + 2,
       
       [nats] = 0,
       
       [d](x0) = 2x0 + 1,
       
       [inc](x0) = 2x0
      orientation:
       inc(tl(nats())) = 4 >= 4 = inc(tl(:(0(),inc(nats()))))
       
       inc(tl(nats())) = 4 >= 2 = tl(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()))))
       
       nats() = 0 >= 0 = :(0(),inc(nats()))
       
       inc(:(x,y)) = 4x + 2y >= 2x + 2y = :(s(x),inc(y))
       
       d(:(x,y)) = 4x + 2y + 1 >= 4x + 2y + 1 = :(x,:(x,d(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))
        d(:(x,y)) -> :(x,:(x,d(y)))
      Matrix Interpretation Processor: dim=2
       
       interpretation:
                  [1 0]  
        [s](x0) = [0 0]x0,
        
              [0]
        [0] = [1],
        
                           [1 0]  
        [:](x0, x1) = x0 + [0 0]x1,
        
                   [1 1]     [0]
        [tl](x0) = [0 0]x0 + [3],
        
                 [0]
        [nats] = [1],
        
                  [2 0]     [3]
        [d](x0) = [0 2]x0 + [0],
        
                    [2 0]     [0]
        [inc](x0) = [1 0]x0 + [2]
       orientation:
                          [2]    [2]                              
        inc(tl(nats())) = [3] >= [3] = inc(tl(:(0(),inc(nats()))))
        
                          [2]    [2]                              
        tl(inc(nats())) = [3] >= [3] = tl(inc(:(0(),inc(nats()))))
        
                                      [2]    [0]                                 
        tl(inc(:(0(),inc(nats())))) = [3] >= [3] = tl(:(s(0()),inc(inc(nats()))))
        
                 [0]    [0]                     
        nats() = [1] >= [1] = :(0(),inc(nats()))
        
                      [2 0]    [2 0]    [0]    [1 0]    [2 0]                  
        inc(:(x,y)) = [1 0]x + [1 0]y + [2] >= [0 0]x + [0 0]y = :(s(x),inc(y))
        
                    [2 0]    [2 0]    [3]    [2 0]    [2 0]    [3]                 
        d(:(x,y)) = [0 2]x + [0 0]y + [0] >= [0 1]x + [0 0]y + [0] = :(x,:(x,d(y)))
       problem:
        strict:
         inc(tl(nats())) -> inc(tl(:(0(),inc(nats()))))
         tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
        weak:
         nats() -> :(0(),inc(nats()))
         inc(:(x,y)) -> :(s(x),inc(y))
         d(:(x,y)) -> :(x,:(x,d(y)))
       Matrix Interpretation Processor: dim=2
        
        interpretation:
                   [1 0]  
         [s](x0) = [0 0]x0,
         
               [0]
         [0] = [0],
         
                       [1 0]     [1 0]  
         [:](x0, x1) = [0 0]x0 + [1 0]x1,
         
                    [2 1]  
         [tl](x0) = [0 1]x0,
         
                  [0]
         [nats] = [1],
         
                   [2 0]  
         [d](x0) = [1 2]x0,
         
                     [1 0]     [0]
         [inc](x0) = [1 0]x0 + [2]
        orientation:
                           [1]    [0]                              
         inc(tl(nats())) = [3] >= [2] = inc(tl(:(0(),inc(nats()))))
         
                           [2]    [2]                              
         tl(inc(nats())) = [2] >= [2] = tl(inc(:(0(),inc(nats()))))
         
                  [0]    [0]                     
         nats() = [1] >= [0] = :(0(),inc(nats()))
         
                       [1 0]    [1 0]    [0]    [1 0]    [1 0]                  
         inc(:(x,y)) = [1 0]x + [1 0]y + [2] >= [0 0]x + [1 0]y = :(s(x),inc(y))
         
                     [2 0]    [2 0]     [2 0]    [2 0]                  
         d(:(x,y)) = [1 0]x + [3 0]y >= [1 0]x + [2 0]y = :(x,:(x,d(y)))
        problem:
         strict:
          tl(inc(nats())) -> tl(inc(:(0(),inc(nats()))))
         weak:
          nats() -> :(0(),inc(nats()))
          inc(:(x,y)) -> :(s(x),inc(y))
          d(:(x,y)) -> :(x,:(x,d(y)))
        Matrix Interpretation Processor: dim=2
         
         interpretation:
                    [1 0]  
          [s](x0) = [0 0]x0,
          
                [0]
          [0] = [0],
          
                        [1 0]     [1 0]  
          [:](x0, x1) = [0 0]x0 + [0 0]x1,
          
                     [1 1]     [0]
          [tl](x0) = [0 0]x0 + [2],
          
                   [2]
          [nats] = [1],
          
                    [2 0]     [2]
          [d](x0) = [0 0]x0 + [0],
          
                        
          [inc](x0) = x0
         orientation:
                            [3]    [2]                              
          tl(inc(nats())) = [2] >= [2] = tl(inc(:(0(),inc(nats()))))
          
                   [2]    [2]                     
          nats() = [1] >= [0] = :(0(),inc(nats()))
          
                        [1 0]    [1 0]     [1 0]    [1 0]                  
          inc(:(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = :(s(x),inc(y))
          
                      [2 0]    [2 0]    [2]    [2 0]    [2 0]    [2]                 
          d(:(x,y)) = [0 0]x + [0 0]y + [0] >= [0 0]x + [0 0]y + [0] = :(x,:(x,d(y)))
         problem:
          strict:
           
          weak:
           nats() -> :(0(),inc(nats()))
           inc(:(x,y)) -> :(s(x),inc(y))
           d(:(x,y)) -> :(x,:(x,d(y)))
         Shift Processor (ldh) lab=left (force):
          strict:
           
          weak:
           
          Rule Labeling Processor:
           strict:
            
           weak:
            
           rule labeling (right):
            nats() -> :(0(),inc(nats())): 0
            inc(:(x,y)) -> :(s(x),inc(y)): 0
            inc(tl(nats())) -> tl(inc(nats())): 0
            hd(:(x,y)) -> x: 0
            tl(:(x,y)) -> y: 0
            d(:(x,y)) -> :(x,:(x,d(y))): 0
           Rule Labeling Processor:
            strict:
             
            weak:
             
            rule labeling (left):
             nats() -> :(0(),inc(nats())): 0
             inc(:(x,y)) -> :(s(x),inc(y)): 0
             inc(tl(nats())) -> tl(inc(nats())): 0
             hd(:(x,y)) -> x: 0
             tl(:(x,y)) -> y: 0
             d(:(x,y)) -> :(x,:(x,d(y))): 0
            Decreasing Processor:
             The following diagrams are decreasing:
             peak:
              inc(tl(:(0(),inc(nats())))) <-0|0,0[==0,==1,==0]- inc(tl(nats())) -2|
                                                                [==0,==1,==0]-> 
                                                                tl(inc(nats()))
             joins (1):
              inc(tl(:(0(),inc(nats())))) -4|0[==0,>>0,==0]-> inc(inc(nats()))
              tl(inc(nats())) -0|0,0[==0,>>0,==0]-> tl(inc(:(0(),inc(nats())))) -1|
                                                    0[==0,>>0,==0]-> 
               tl(:(s(0()),inc(inc(nats())))) -4|[==0,>>0,==0]-> inc(inc(nats()))
             Qed