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) = 2x0,
    
    [inc(0)](x0) = 2x0,
    
    [hd(0)](x0) = 2x0 + 2,
    
    [tl(0)](x0) = 2x0 + 2,
    
    [:(1)](x0) = x0,
    
    [:(0)](x0) = x0,
    
    [d(0)](x0) = x0
   orientation:
    d(0)(:(0)(x)) = x >= x = :(0)(x)
    
    d(0)(:(0)(x)) = x >= x = :(1)(:(0)(x))
    
    d(0)(:(1)(y)) = y >= y = :(1)(:(1)(d(0)(y)))
    
    tl(0)(:(1)(y)) = 2y + 2 >= y = y
    
    hd(0)(:(0)(x)) = 2x + 2 >= x = x
    
    inc(0)(:(0)(x)) = 2x >= 2x = :(0)(s(0)(x))
    
    inc(0)(:(1)(y)) = 2y >= 2y = :(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)(:(0)(x)) -> :(0)(s(0)(x))
     inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
   Matrix Interpretation Processor: dim=1, lab=right
    
    interpretation:
     [s(0)](x0) = x0,
     
     [inc(0)](x0) = 2x0 + 1,
     
     [:(1)](x0) = x0,
     
     [:(0)](x0) = x0,
     
     [d(0)](x0) = x0
    orientation:
     d(0)(:(0)(x)) = x >= x = :(0)(x)
     
     d(0)(:(0)(x)) = x >= x = :(1)(:(0)(x))
     
     d(0)(:(1)(y)) = y >= y = :(1)(:(1)(d(0)(y)))
     
     inc(0)(:(0)(x)) = 2x + 1 >= x = :(0)(s(0)(x))
     
     inc(0)(:(1)(y)) = 2y + 1 >= 2y + 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) = 2x0 + 1,
      
      [:(1)](x0) = x0,
      
      [:(0)](x0) = x0,
      
      [d(0)](x0) = 2x0 + 2
     orientation:
      d(0)(:(0)(x)) = 2x + 2 >= x = :(0)(x)
      
      d(0)(:(0)(x)) = 2x + 2 >= x = :(1)(:(0)(x))
      
      d(0)(:(1)(y)) = 2y + 2 >= 2y + 2 = :(1)(:(1)(d(0)(y)))
      
      inc(0)(:(1)(y)) = 2y + 1 >= 2y + 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,
          
          [hd](x0) = 4x0 + 1,
          
          [tl](x0) = x0,
          
          [s](x0) = x0,
          
          [:](x0, x1) = x0 + x1,
          
          [inc](x0) = x0,
          
          [0] = 0,
          
          [nats] = 4
         orientation:
          inc(tl(nats())) = 4 >= 4 = inc(tl(:(0(),inc(nats()))))
          
          inc(tl(nats())) = 4 >= 4 = tl(inc(nats()))
          
          inc(tl(:(0(),inc(nats())))) = 4 >= 4 = inc(inc(nats()))
          
          tl(inc(nats())) = 4 >= 4 = tl(inc(:(0(),inc(nats()))))
          
          tl(inc(:(0(),inc(nats())))) = 4 >= 4 = tl(:(s(0()),inc(inc(nats()))))
          
          tl(:(s(0()),inc(inc(nats())))) = 4 >= 4 = inc(inc(nats()))
          
          nats() = 4 >= 4 = :(0(),inc(nats()))
          
          inc(:(x,y)) = x + y >= x + y = :(s(x),inc(y))
          
          hd(:(x,y)) = 4x + 4y + 1 >= 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:
           [d](x0) = 2x0,
           
           [tl](x0) = 2x0 + 1,
           
           [s](x0) = x0,
           
           [:](x0, x1) = 2x0 + x1,
           
           [inc](x0) = x0,
           
           [0] = 0,
           
           [nats] = 0
          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)) = 2x + y >= 2x + y = :(s(x),inc(y))
           
           tl(:(x,y)) = 4x + 2y + 1 >= y = y
           
           d(:(x,y)) = 4x + 2y >= 4x + 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:
            [d](x0) = 2x0,
            
            [tl](x0) = x0 + 3x0x0 + 1,
            
            [s](x0) = x0,
            
            [:](x0, x1) = 2x0 + x1,
            
            [inc](x0) = 2x0,
            
            [0] = 0,
            
            [nats] = 0
           orientation:
            inc(tl(nats())) = 2 >= 2 = inc(tl(:(0(),inc(nats()))))
            
            inc(tl(nats())) = 2 >= 1 = tl(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()))))
            
            nats() = 0 >= 0 = :(0(),inc(nats()))
            
            inc(:(x,y)) = 4x + 2y >= 2x + 2y = :(s(x),inc(y))
            
            d(:(x,y)) = 4x + 2y >= 4x + 2y = :(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:
                       [2 0]     [3]
             [d](x0) = [2 0]x0 + [3],
             
                        [1 2]     [0]
             [tl](x0) = [0 0]x0 + [2],
             
                       [2 0]     [0]
             [s](x0) = [0 0]x0 + [3],
             
                           [1 0]     [1 0]  
             [:](x0, x1) = [0 0]x0 + [1 0]x1,
             
                         [2 0]     [0]
             [inc](x0) = [2 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())) = [2] >= [2] = tl(inc(:(0(),inc(nats()))))
             
                                           [2]    [0]                                 
             tl(inc(:(0(),inc(nats())))) = [2] >= [2] = 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)) = [2 0]x + [2 0]y + [1] >= [0 0]x + [2 0]y = :(s(x),inc(y))
             
                         [2 0]    [2 0]    [3]    [2 0]    [2 0]    [3]                 
             d(:(x,y)) = [2 0]x + [2 0]y + [3] >= [1 0]x + [2 0]y + [3] = :(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:
                        [2 0]     [1]
              [d](x0) = [2 0]x0 + [2],
              
                         [1 1]  
              [tl](x0) = [0 0]x0,
              
                        [1 0]  
              [s](x0) = [0 0]x0,
              
                            [1 0]     [1 0]  
              [:](x0, x1) = [0 0]x0 + [1 0]x1,
              
                          [2 0]  
              [inc](x0) = [2 0]x0,
              
                    [0]
              [0] = [0],
              
                       [0]
              [nats] = [1]
             orientation:
                                [2]    [0]                              
              inc(tl(nats())) = [2] >= [0] = inc(tl(:(0(),inc(nats()))))
              
                                [0]    [0]                              
              tl(inc(nats())) = [0] >= [0] = tl(inc(:(0(),inc(nats()))))
              
                       [0]    [0]                     
              nats() = [1] >= [0] = :(0(),inc(nats()))
              
                            [2 0]    [2 0]     [1 0]    [2 0]                  
              inc(:(x,y)) = [2 0]x + [2 0]y >= [0 0]x + [2 0]y = :(s(x),inc(y))
              
                          [2 0]    [2 0]    [1]    [2 0]    [2 0]    [1]                 
              d(:(x,y)) = [2 0]x + [2 0]y + [2] >= [1 0]x + [2 0]y + [1] = :(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=3
              
              interpretation:
                         [1 0 1]  
               [d](x0) = [0 0 0]x0
                         [1 0 1]  ,
               
                          [1 1 0]  
               [tl](x0) = [1 1 0]x0
                          [0 0 0]  ,
               
                         [1 0 0]  
               [s](x0) = [0 0 0]x0
                         [0 0 0]  ,
               
                             [1 1 0]     [1 0 0]  
               [:](x0, x1) = [0 0 0]x0 + [0 0 0]x1
                             [1 1 0]     [0 0 1]  ,
               
                           [1 0 0]  
               [inc](x0) = [0 1 1]x0
                           [0 0 1]  ,
               
                     [0]
               [0] = [0]
                     [0],
               
                        [1]
               [nats] = [1]
                        [1]
              orientation:
                                 [3]    [2]                              
               tl(inc(nats())) = [3] >= [2] = tl(inc(:(0(),inc(nats()))))
                                 [0]    [0]                              
               
                        [1]    [1]                     
               nats() = [1] >= [0] = :(0(),inc(nats()))
                        [1]    [1]                     
               
                             [1 1 0]    [1 0 0]     [1 0 0]    [1 0 0]                  
               inc(:(x,y)) = [1 1 0]x + [0 0 1]y >= [0 0 0]x + [0 0 0]y = :(s(x),inc(y))
                             [1 1 0]    [0 0 1]     [1 0 0]    [0 0 1]                  
               
                           [2 2 0]    [1 0 1]     [2 2 0]    [1 0 1]                  
               d(:(x,y)) = [0 0 0]x + [0 0 0]y >= [0 0 0]x + [0 0 0]y = :(x,:(x,d(y)))
                           [2 2 0]    [1 0 1]     [2 2 0]    [1 0 1]                  
              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,0,1,1,0,0,1]- 
                  inc(tl(nats())) -2|[1,0,0,0,0,0,0]-> tl(inc(nats()))
                 joins:
                  inc(tl(:(0(),inc(nats())))) -4|0[1,0,1,1,0,0,0]-> inc(inc(nats()))
                  tl(inc(nats())) -0|0,0[0,0,1,1,0,0,1]-> tl(inc(:(0(),inc(nats())))) -1|
                                                          0[0,0,0,0,0,0,0]-> 
                   tl(:(s(0()),inc(inc(nats())))) -4|[0,0,0,0,0,0,0]-> 
                   inc(inc(nats()))
                 Qed