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 (star):
  
  strict:
   d(0)(:(0)(x)) -> :(0)(x)
   d(0)(:(0)(x)) -> :(1)(:(0)(x))
  weak:
   d(0)(:(1)(y)) -> :(1)(:(1)(d(0)(y)))
   tl(0)(:(1)(y)) -> y
   hd(0)(:(0)(x)) -> x
   inc(0)(:(0)(x)) -> :(0)(s(0)(x))
   inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
  critical peaks: 1
  inc(tl(:(0(),inc(nats())))) <-0|0,0[]- inc(tl(nats())) -2|[]-> tl(inc(nats()))
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [s(0)](x0) = x0,
    
    [inc(0)](x0) = x0 + 1,
    
    [hd(0)](x0) = x0 + 1,
    
    [tl(0)](x0) = 2x0 + 1,
    
    [:(1)](x0) = x0,
    
    [:(0)](x0) = 2x0,
    
    [d(0)](x0) = x0
   orientation:
    d(0)(:(0)(x)) = 2x >= 2x = :(0)(x)
    
    d(0)(:(0)(x)) = 2x >= 2x = :(1)(:(0)(x))
    
    d(0)(:(1)(y)) = y >= y = :(1)(:(1)(d(0)(y)))
    
    tl(0)(:(1)(y)) = 2y + 1 >= y = y
    
    hd(0)(:(0)(x)) = 2x + 1 >= x = x
    
    inc(0)(:(0)(x)) = 2x + 1 >= 2x = :(0)(s(0)(x))
    
    inc(0)(:(1)(y)) = y + 1 >= y + 1 = :(1)(inc(0)(y))
   problem:
    
    strict:
     d(0)(:(0)(x)) -> :(0)(x)
     d(0)(:(0)(x)) -> :(1)(:(0)(x))
    weak:
     d(0)(:(1)(y)) -> :(1)(:(1)(d(0)(y)))
     inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
   Matrix Interpretation Processor: dim=1, lab=right
    
    interpretation:
     [inc(0)](x0) = x0 + 1,
     
     [:(1)](x0) = x0,
     
     [:(0)](x0) = x0,
     
     [d(0)](x0) = 2x0 + 1
    orientation:
     d(0)(:(0)(x)) = 2x + 1 >= x = :(0)(x)
     
     d(0)(:(0)(x)) = 2x + 1 >= x = :(1)(:(0)(x))
     
     d(0)(:(1)(y)) = 2y + 1 >= 2y + 1 = :(1)(:(1)(d(0)(y)))
     
     inc(0)(:(1)(y)) = y + 1 >= y + 1 = :(1)(inc(0)(y))
    problem:
     
     strict:
      
     weak:
      d(0)(:(1)(y)) -> :(1)(:(1)(d(0)(y)))
      inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
    Matrix Interpretation Processor: dim=1, lab=right
     
     interpretation:
      [inc(0)](x0) = 2x0 + 1,
      
      [:(1)](x0) = x0 + 1,
      
      [d(0)](x0) = 2x0 + 1
     orientation:
      d(0)(:(1)(y)) = 2y + 3 >= 2y + 3 = :(1)(:(1)(d(0)(y)))
      
      inc(0)(:(1)(y)) = 2y + 3 >= 2y + 2 = :(1)(inc(0)(y))
     problem:
      
      strict:
       
      weak:
       d(0)(:(1)(y)) -> :(1)(:(1)(d(0)(y)))
     Matrix Interpretation Processor: dim=1, lab=right
      
      interpretation:
       [:(1)](x0) = x0 + 1,
       
       [d(0)](x0) = 3x0
      orientation:
       d(0)(:(1)(y)) = 3y + 3 >= 3y + 2 = :(1)(:(1)(d(0)(y)))
      problem:
       
       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))
        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:
         [d](x0) = 2x0 + 4,
         
         [hd](x0) = 2x0 + 4,
         
         [tl](x0) = 4x0,
         
         [s](x0) = 2x0,
         
         [:](x0, x1) = 4x0 + x1,
         
         [inc](x0) = 3x0,
         
         [0] = 0,
         
         [nats] = 0
        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)) = 12x + 3y >= 8x + 3y = :(s(x),inc(y))
         
         hd(:(x,y)) = 8x + 2y + 4 >= x = x
         
         tl(:(x,y)) = 16x + 4y >= y = y
         
         d(:(x,y)) = 8x + 2y + 4 >= 8x + 2y + 4 = :(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)))
        Matrix Interpretation Processor: dim=1
         
         interpretation:
          [d](x0) = 4x0,
          
          [tl](x0) = 2x0 + 1,
          
          [s](x0) = x0,
          
          [:](x0, x1) = x0 + x1,
          
          [inc](x0) = x0,
          
          [0] = 0,
          
          [nats] = 2
         orientation:
          inc(tl(nats())) = 5 >= 5 = inc(tl(:(0(),inc(nats()))))
          
          inc(tl(nats())) = 5 >= 5 = tl(inc(nats()))
          
          inc(tl(:(0(),inc(nats())))) = 5 >= 2 = inc(inc(nats()))
          
          tl(inc(nats())) = 5 >= 5 = tl(inc(:(0(),inc(nats()))))
          
          tl(inc(:(0(),inc(nats())))) = 5 >= 5 = tl(:(s(0()),inc(inc(nats()))))
          
          tl(:(s(0()),inc(inc(nats())))) = 5 >= 2 = inc(inc(nats()))
          
          nats() = 2 >= 2 = :(0(),inc(nats()))
          
          inc(:(x,y)) = x + y >= x + y = :(s(x),inc(y))
          
          tl(:(x,y)) = 2x + 2y + 1 >= y = y
          
          d(:(x,y)) = 4x + 4y >= 2x + 4y = :(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)))
         Matrix Interpretation Processor: dim=1
          
          interpretation:
           [d](x0) = 2x0 + 3,
           
           [tl](x0) = 4x0 + 2,
           
           [s](x0) = 4x0,
           
           [:](x0, x1) = x0 + x1,
           
           [inc](x0) = 4x0,
           
           [0] = 0,
           
           [nats] = 0
          orientation:
           inc(tl(nats())) = 8 >= 8 = inc(tl(:(0(),inc(nats()))))
           
           inc(tl(nats())) = 8 >= 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 + 4y >= 4x + 4y = :(s(x),inc(y))
           
           d(:(x,y)) = 2x + 2y + 3 >= 2x + 2y + 3 = :(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:
                      [3 0]     [1]
            [d](x0) = [0 0]x0 + [3],
            
                       [2 2]     [0]
            [tl](x0) = [0 0]x0 + [1],
            
                      [2 0]  
            [s](x0) = [0 0]x0,
            
                          [1 0]     [1 0]  
            [:](x0, x1) = [0 0]x0 + [0 0]x1,
            
                        [2 0]     [0]
            [inc](x0) = [0 0]x0 + [1],
            
                  [0]
            [0] = [0],
            
                     [0]
            [nats] = [0]
           orientation:
                              [0]    [0]                              
            inc(tl(nats())) = [1] >= [1] = inc(tl(:(0(),inc(nats()))))
            
                              [2]    [2]                              
            tl(inc(nats())) = [1] >= [1] = tl(inc(:(0(),inc(nats()))))
            
                                          [2]    [0]                                 
            tl(inc(:(0(),inc(nats())))) = [1] >= [1] = tl(:(s(0()),inc(inc(nats()))))
            
                     [0]    [0]                     
            nats() = [0] >= [0] = :(0(),inc(nats()))
            
                          [2 0]    [2 0]    [0]    [2 0]    [2 0]                  
            inc(:(x,y)) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y = :(s(x),inc(y))
            
                        [3 0]    [3 0]    [1]    [2 0]    [3 0]    [1]                 
            d(:(x,y)) = [0 0]x + [0 0]y + [3] >= [0 0]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=3
            
            interpretation:
                       [1 0 1]  
             [d](x0) = [1 0 1]x0
                       [1 0 1]  ,
             
                        [1 1 0]  
             [tl](x0) = [0 0 0]x0
                        [0 0 0]  ,
             
                       [1 0 0]  
             [s](x0) = [0 0 0]x0
                       [0 0 0]  ,
             
                           [1 0 0]     [1 0 0]  
             [:](x0, x1) = [0 0 0]x0 + [1 0 0]x1
                           [1 0 0]     [0 0 1]  ,
             
                         [1 0 0]     [0]
             [inc](x0) = [1 0 1]x0 + [1]
                         [0 0 1]     [0],
             
                   [0]
             [0] = [0]
                   [0],
             
                      [0]
             [nats] = [1]
                      [1]
            orientation:
                               [1]    [0]                              
             inc(tl(nats())) = [2] >= [1] = inc(tl(:(0(),inc(nats()))))
                               [0]    [0]                              
             
                               [2]    [2]                              
             tl(inc(nats())) = [0] >= [0] = tl(inc(:(0(),inc(nats()))))
                               [0]    [0]                              
             
                      [0]    [0]                     
             nats() = [1] >= [0] = :(0(),inc(nats()))
                      [1]    [1]                     
             
                           [1 0 0]    [1 0 0]    [0]    [1 0 0]    [1 0 0]                  
             inc(:(x,y)) = [2 0 0]x + [1 0 1]y + [1] >= [0 0 0]x + [1 0 0]y = :(s(x),inc(y))
                           [1 0 0]    [0 0 1]    [0]    [1 0 0]    [0 0 1]                  
             
                         [2 0 0]    [1 0 1]     [2 0 0]    [1 0 1]                  
             d(:(x,y)) = [2 0 0]x + [1 0 1]y >= [1 0 0]x + [1 0 1]y = :(x,:(x,d(y)))
                         [2 0 0]    [1 0 1]     [2 0 0]    [1 0 1]                  
            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:
                        [2 0]     [1]
              [d](x0) = [2 0]x0 + [3],
              
                         [1 1]     [0]
              [tl](x0) = [0 0]x0 + [1],
              
                        [1 0]  
              [s](x0) = [0 0]x0,
              
                            [1 1]     [1 0]  
              [:](x0, x1) = [0 0]x0 + [0 0]x1,
              
                          [2 0]  
              [inc](x0) = [0 2]x0,
              
                    [0]
              [0] = [0],
              
                       [0]
              [nats] = [1]
             orientation:
                                [2]    [0]                              
              tl(inc(nats())) = [1] >= [1] = tl(inc(:(0(),inc(nats()))))
              
                       [0]    [0]                     
              nats() = [1] >= [0] = :(0(),inc(nats()))
              
                            [2 2]    [2 0]     [1 0]    [2 0]                  
              inc(:(x,y)) = [0 0]x + [0 0]y >= [0 0]x + [0 0]y = :(s(x),inc(y))
              
                          [2 2]    [2 0]    [1]    [2 2]    [2 0]    [1]                 
              d(:(x,y)) = [2 2]x + [2 0]y + [3] >= [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())): 1
                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[1,1,1,0,0,1]- inc(tl(nats())) -2|
                                                                   [1,0,0,0,0,0]-> 
                                                                   tl(inc(nats()))
                joins:
                 inc(tl(:(0(),inc(nats())))) -4|0[1,1,1,0,0,0]-> inc(inc(nats()))
                 tl(inc(nats())) -0|0,0[0,1,1,0,0,1]-> tl(inc(:(0(),inc(nats())))) -1|
                                                       0[0,0,0,0,0,0]-> 
                  tl(:(s(0()),inc(inc(nats())))) -4|[0,0,0,0,0,0]-> inc(inc(nats()))
                Qed