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 (star):
  
  strict:
   
  weak:
   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())) -4|[]-> tl(inc(nats()))
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [s(0)](x0) = 2x0,
    
    [inc(0)](x0) = 3x0 + 1,
    
    [:(0)](x0) = x0,
    
    [hd(0)](x0) = 2x0,
    
    [:(1)](x0) = x0,
    
    [tl(0)](x0) = 3x0
   orientation:
    tl(0)(:(1)(y)) = 3y >= y = y
    
    hd(0)(:(0)(x)) = 2x >= x = x
    
    inc(0)(:(0)(x)) = 3x + 1 >= 2x = :(0)(s(0)(x))
    
    inc(0)(:(1)(y)) = 3y + 1 >= 3y + 1 = :(1)(inc(0)(y))
   problem:
    
    strict:
     
    weak:
     tl(0)(:(1)(y)) -> y
     hd(0)(:(0)(x)) -> x
     inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
   Matrix Interpretation Processor: dim=1, lab=right
    
    interpretation:
     [inc(0)](x0) = 2x0 + 2,
     
     [:(0)](x0) = 2x0,
     
     [hd(0)](x0) = x0 + 2,
     
     [:(1)](x0) = x0,
     
     [tl(0)](x0) = 2x0
    orientation:
     tl(0)(:(1)(y)) = 2y >= y = y
     
     hd(0)(:(0)(x)) = 2x + 2 >= x = x
     
     inc(0)(:(1)(y)) = 2y + 2 >= 2y + 2 = :(1)(inc(0)(y))
    problem:
     
     strict:
      
     weak:
      tl(0)(:(1)(y)) -> y
      inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
    Matrix Interpretation Processor: dim=1, lab=right
     
     interpretation:
      [inc(0)](x0) = 2x0,
      
      [:(1)](x0) = x0,
      
      [tl(0)](x0) = x0 + 1
     orientation:
      tl(0)(:(1)(y)) = y + 1 >= y = y
      
      inc(0)(:(1)(y)) = 2y >= 2y = :(1)(inc(0)(y))
     problem:
      
      strict:
       
      weak:
       inc(0)(:(1)(y)) -> :(1)(inc(0)(y))
     Matrix Interpretation Processor: dim=2, lab=right
      
      interpretation:
                      [1 1]  
       [inc(0)](x0) = [1 0]x0,
       
                    [2 1]     [1]
       [:(1)](x0) = [1 1]x0 + [1]
      orientation:
                         [3 2]    [2]    [3 2]    [1]                  
       inc(0)(:(1)(y)) = [2 1]y + [1] >= [2 1]y + [1] = :(1)(inc(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))
        hd(:(x,y)) -> x
        tl(:(x,y)) -> y
        inc(tl(nats())) -> tl(inc(nats()))
       Matrix Interpretation Processor: dim=1
        
        interpretation:
         [tl](x0) = 4x0,
         
         [hd](x0) = 4x0 + 2,
         
         [s](x0) = x0,
         
         [:](x0, x1) = 2x0 + 2x1,
         
         [inc](x0) = 4x0,
         
         [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)) = 8x + 8y >= 2x + 8y = :(s(x),inc(y))
         
         hd(:(x,y)) = 8x + 8y + 2 >= x = x
         
         tl(:(x,y)) = 8x + 8y >= 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:
          [tl](x0) = x0 + 1,
          
          [s](x0) = 2x0,
          
          [:](x0, x1) = x0 + 4x1,
          
          [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()))
          
          inc(tl(:(0(),inc(nats())))) = 2 >= 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 + 8y >= 2x + 8y = :(s(x),inc(y))
          
          tl(:(x,y)) = x + 4y + 1 >= 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:
            s1(15) -> 51*
            s1(7) -> 15*
            s1(51) -> 15*
            inc0(7) -> 7*
            tl0(7) -> 7*
            nats0() -> 7*
            :0(7,7) -> 7*
            00() -> 7*
            s0(7) -> 7*
            inc1(50) -> 14*
            inc1(17) -> 14,7
            inc1(7) -> 14*
            inc1(14) -> 50*
            inc1(16) -> 46*
            inc1(13) -> 14*
            tl1(46) -> 7*
            tl1(16) -> 17*
            :1(51,50) -> 50,7,14,46
            :1(15,14) -> 50,14,13,7,16
            01() -> 15*
            nats1() -> 13*
          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:
             s1(15) -> 33*
             s1(7) -> 15*
             s1(33) -> 15*
             inc0(7) -> 7*
             tl0(7) -> 7*
             nats0() -> 7*
             :0(7,7) -> 7*
             00() -> 7*
             s0(7) -> 7*
             inc1(32) -> 14*
             inc1(7) -> 14*
             inc1(14) -> 32*
             inc1(16) -> 17*
             inc1(13) -> 14*
             tl1(17) -> 7*
             :1(33,32) -> 32,7,14,17
             :1(15,14) -> 32,14,13,7,16
             01() -> 15*
             nats1() -> 13*
           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:
              s1(17) -> 18*
              s1(7) -> 17*
              s1(18) -> 17*
              inc0(7) -> 7*
              tl0(7) -> 7*
              nats0() -> 7*
              :0(7,7) -> 7*
              00() -> 7*
              s0(7) -> 7*
              inc1(15) -> 16*
              inc1(7) -> 15*
              inc1(14) -> 15*
              inc1(16) -> 15*
              tl1(19) -> 7*
              :1(17,15) -> 16,15,14,7
              :1(18,16) -> 16,15,7,19
              01() -> 17*
              nats1() -> 14*
            problem:
             
             strict:
              
             weak:
              nats() -> :(0(),inc(nats()))
              inc(:(x,y)) -> :(s(x),inc(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
               hd(:(x,y)) -> x: 0
               tl(:(x,y)) -> y: 0
               inc(tl(nats())) -> tl(inc(nats())): 0
              Decreasing Processor:
               The following diagrams are decreasing:
               peak:
                inc(tl(:(0(),inc(nats())))) <-0|0,0[1,1,2,0,0,1]- inc(tl(nats())) -4|
                                                                  [1,0,0,0,0,0]-> 
                                                                  tl(inc(nats()))
               joins:
                inc(tl(:(0(),inc(nats())))) -3|0[1,1,2,0,0,0]-> inc(inc(nats()))
                tl(inc(nats())) -0|0,0[0,3,4,0,0,1]-> tl(inc(:(0(),inc(nats())))) -1|
                                                      0[0,0,0,0,0,0]-> 
                 tl(:(s(0()),inc(inc(nats())))) -3|[0,0,0,0,0,0]-> inc(inc(nats()))
               Qed