Problem:
 -(0(),0()) -> 0()
 -(s(x),0()) -> s(x)
 -(x,s(y)) -> -(d(x),y)
 d(s(x)) -> x
 -(s(x),s(y)) -> -(x,y)
 -(d(x),y) -> -(x,s(y))

Proof:
 Church Rosser Transformation Processor (star):
  
  strict:
   
  weak:
   -(0)(d(0)(x)) -> -(0)(x)
   -(1)(y) -> -(1)(s(0)(y))
   -(0)(s(0)(x)) -> -(0)(x)
   -(1)(s(0)(y)) -> -(1)(y)
   d(0)(s(0)(x)) -> x
   -(0)(x) -> -(0)(d(0)(x))
   -(0)(s(0)(x)) -> s(0)(x)
  critical peaks: 5
  -(d(s(x)),y) <-2|[]- -(s(x),s(y)) -4|[]-> -(x,y)
  -(d(d(x)),x125) <-2|[]- -(d(x),s(x125)) -5|[]-> -(x,s(s(x125)))
  -(x126,y) <-3|0[]- -(d(s(x126)),y) -5|[]-> -(s(x126),s(y))
  -(x127,y) <-4|[]- -(s(x127),s(y)) -2|[]-> -(d(s(x127)),y)
  -(x129,s(s(y))) <-5|[]- -(d(x129),s(y)) -2|[]-> -(d(d(x129)),y)
  Matrix Interpretation Processor: dim=1, lab=right
   
   interpretation:
    [s(0)](x0) = x0,
    
    [-(1)](x0) = 2x0 + 2,
    
    [d(0)](x0) = x0,
    
    [-(0)](x0) = x0 + 2
   orientation:
    -(0)(d(0)(x)) = x + 2 >= x + 2 = -(0)(x)
    
    -(1)(y) = 2y + 2 >= 2y + 2 = -(1)(s(0)(y))
    
    -(0)(s(0)(x)) = x + 2 >= x + 2 = -(0)(x)
    
    -(1)(s(0)(y)) = 2y + 2 >= 2y + 2 = -(1)(y)
    
    d(0)(s(0)(x)) = x >= x = x
    
    -(0)(x) = x + 2 >= x + 2 = -(0)(d(0)(x))
    
    -(0)(s(0)(x)) = x + 2 >= x = s(0)(x)
   problem:
    
    strict:
     
    weak:
     -(0)(d(0)(x)) -> -(0)(x)
     -(1)(y) -> -(1)(s(0)(y))
     -(0)(s(0)(x)) -> -(0)(x)
     -(1)(s(0)(y)) -> -(1)(y)
     d(0)(s(0)(x)) -> x
     -(0)(x) -> -(0)(d(0)(x))
   Matrix Interpretation Processor: dim=2, lab=right
    
    interpretation:
                  [1 0]     [0]
     [s(0)](x0) = [1 1]x0 + [1],
     
                  [1 0]  
     [-(1)](x0) = [2 0]x0,
     
                    
     [d(0)](x0) = x0,
     
                  [1 2]  
     [-(0)](x0) = [0 1]x0
    orientation:
                     [1 2]     [1 2]           
     -(0)(d(0)(x)) = [0 1]x >= [0 1]x = -(0)(x)
     
               [1 0]     [1 0]                 
     -(1)(y) = [2 0]y >= [2 0]y = -(1)(s(0)(y))
     
                     [3 2]    [2]    [1 2]           
     -(0)(s(0)(x)) = [1 1]x + [1] >= [0 1]x = -(0)(x)
     
                     [1 0]     [1 0]           
     -(1)(s(0)(y)) = [2 0]y >= [2 0]y = -(1)(y)
     
                     [1 0]    [0]         
     d(0)(s(0)(x)) = [1 1]x + [1] >= x = x
     
               [1 2]     [1 2]                 
     -(0)(x) = [0 1]x >= [0 1]x = -(0)(d(0)(x))
    problem:
     
     strict:
      
     weak:
      -(0)(d(0)(x)) -> -(0)(x)
      -(1)(y) -> -(1)(s(0)(y))
      -(1)(s(0)(y)) -> -(1)(y)
      d(0)(s(0)(x)) -> x
      -(0)(x) -> -(0)(d(0)(x))
    Shift Processor lab=left (dd):
     
     strict:
      -(s(x),s(y)) -> -(d(s(x)),y)
      -(s(x),s(y)) -> -(x,y)
      -(d(s(x)),y) -> -(x,y)
      -(d(x),s(x125)) -> -(d(d(x)),x125)
      -(d(x),s(x125)) -> -(x,s(s(x125)))
      -(d(d(x)),x125) -> -(d(x),s(x125))
      -(x,s(s(x125))) -> -(d(x),s(x125))
      -(d(s(x126)),y) -> -(x126,y)
      -(d(s(x126)),y) -> -(s(x126),s(y))
      -(s(x126),s(y)) -> -(x126,y)
      -(s(x127),s(y)) -> -(x127,y)
      -(s(x127),s(y)) -> -(d(s(x127)),y)
      -(d(s(x127)),y) -> -(x127,y)
      -(d(x129),s(y)) -> -(x129,s(s(y)))
      -(d(x129),s(y)) -> -(d(d(x129)),y)
      -(x129,s(s(y))) -> -(d(x129),s(y))
      -(d(d(x129)),y) -> -(d(x129),s(y))
     weak:
      -(0(),0()) -> 0()
      -(s(x),0()) -> s(x)
      -(x,s(y)) -> -(d(x),y)
      d(s(x)) -> x
      -(s(x),s(y)) -> -(x,y)
      -(d(x),y) -> -(x,s(y))
     Matrix Interpretation Processor: dim=1
      
      interpretation:
       [d](x0) = x0,
       
       [s](x0) = x0,
       
       [-](x0, x1) = x0 + 2x1 + 3,
       
       [0] = 1
      orientation:
       -(s(x),s(y)) = x + 2y + 3 >= x + 2y + 3 = -(d(s(x)),y)
       
       -(s(x),s(y)) = x + 2y + 3 >= x + 2y + 3 = -(x,y)
       
       -(d(s(x)),y) = x + 2y + 3 >= x + 2y + 3 = -(x,y)
       
       -(d(x),s(x125)) = x + 2x125 + 3 >= x + 2x125 + 3 = -(d(d(x)),x125)
       
       -(d(x),s(x125)) = x + 2x125 + 3 >= x + 2x125 + 3 = -(x,s(s(x125)))
       
       -(d(d(x)),x125) = x + 2x125 + 3 >= x + 2x125 + 3 = -(d(x),s(x125))
       
       -(x,s(s(x125))) = x + 2x125 + 3 >= x + 2x125 + 3 = -(d(x),s(x125))
       
       -(d(s(x126)),y) = x126 + 2y + 3 >= x126 + 2y + 3 = -(x126,y)
       
       -(d(s(x126)),y) = x126 + 2y + 3 >= x126 + 2y + 3 = -(s(x126),s(y))
       
       -(s(x126),s(y)) = x126 + 2y + 3 >= x126 + 2y + 3 = -(x126,y)
       
       -(s(x127),s(y)) = x127 + 2y + 3 >= x127 + 2y + 3 = -(x127,y)
       
       -(s(x127),s(y)) = x127 + 2y + 3 >= x127 + 2y + 3 = -(d(s(x127)),y)
       
       -(d(s(x127)),y) = x127 + 2y + 3 >= x127 + 2y + 3 = -(x127,y)
       
       -(d(x129),s(y)) = x129 + 2y + 3 >= x129 + 2y + 3 = -(x129,s(s(y)))
       
       -(d(x129),s(y)) = x129 + 2y + 3 >= x129 + 2y + 3 = -(d(d(x129)),y)
       
       -(x129,s(s(y))) = x129 + 2y + 3 >= x129 + 2y + 3 = -(d(x129),s(y))
       
       -(d(d(x129)),y) = x129 + 2y + 3 >= x129 + 2y + 3 = -(d(x129),s(y))
       
       -(0(),0()) = 6 >= 1 = 0()
       
       -(s(x),0()) = x + 5 >= x = s(x)
       
       -(x,s(y)) = x + 2y + 3 >= x + 2y + 3 = -(d(x),y)
       
       d(s(x)) = x >= x = x
       
       -(d(x),y) = x + 2y + 3 >= x + 2y + 3 = -(x,s(y))
      problem:
       
       strict:
        -(s(x),s(y)) -> -(d(s(x)),y)
        -(s(x),s(y)) -> -(x,y)
        -(d(s(x)),y) -> -(x,y)
        -(d(x),s(x125)) -> -(d(d(x)),x125)
        -(d(x),s(x125)) -> -(x,s(s(x125)))
        -(d(d(x)),x125) -> -(d(x),s(x125))
        -(x,s(s(x125))) -> -(d(x),s(x125))
        -(d(s(x126)),y) -> -(x126,y)
        -(d(s(x126)),y) -> -(s(x126),s(y))
        -(s(x126),s(y)) -> -(x126,y)
        -(s(x127),s(y)) -> -(x127,y)
        -(s(x127),s(y)) -> -(d(s(x127)),y)
        -(d(s(x127)),y) -> -(x127,y)
        -(d(x129),s(y)) -> -(x129,s(s(y)))
        -(d(x129),s(y)) -> -(d(d(x129)),y)
        -(x129,s(s(y))) -> -(d(x129),s(y))
        -(d(d(x129)),y) -> -(d(x129),s(y))
       weak:
        -(x,s(y)) -> -(d(x),y)
        d(s(x)) -> x
        -(s(x),s(y)) -> -(x,y)
        -(d(x),y) -> -(x,s(y))
      Matrix Interpretation Processor: dim=1
       
       interpretation:
        [d](x0) = x0 + 1,
        
        [s](x0) = x0 + 1,
        
        [-](x0, x1) = x0 + x1
       orientation:
        -(s(x),s(y)) = x + y + 2 >= x + y + 2 = -(d(s(x)),y)
        
        -(s(x),s(y)) = x + y + 2 >= x + y = -(x,y)
        
        -(d(s(x)),y) = x + y + 2 >= x + y = -(x,y)
        
        -(d(x),s(x125)) = x + x125 + 2 >= x + x125 + 2 = -(d(d(x)),x125)
        
        -(d(x),s(x125)) = x + x125 + 2 >= x + x125 + 2 = -(x,s(s(x125)))
        
        -(d(d(x)),x125) = x + x125 + 2 >= x + x125 + 2 = -(d(x),s(x125))
        
        -(x,s(s(x125))) = x + x125 + 2 >= x + x125 + 2 = -(d(x),s(x125))
        
        -(d(s(x126)),y) = x126 + y + 2 >= x126 + y = -(x126,y)
        
        -(d(s(x126)),y) = x126 + y + 2 >= x126 + y + 2 = -(s(x126),s(y))
        
        -(s(x126),s(y)) = x126 + y + 2 >= x126 + y = -(x126,y)
        
        -(s(x127),s(y)) = x127 + y + 2 >= x127 + y = -(x127,y)
        
        -(s(x127),s(y)) = x127 + y + 2 >= x127 + y + 2 = -(d(s(x127)),y)
        
        -(d(s(x127)),y) = x127 + y + 2 >= x127 + y = -(x127,y)
        
        -(d(x129),s(y)) = x129 + y + 2 >= x129 + y + 2 = -(x129,s(s(y)))
        
        -(d(x129),s(y)) = x129 + y + 2 >= x129 + y + 2 = -(d(d(x129)),y)
        
        -(x129,s(s(y))) = x129 + y + 2 >= x129 + y + 2 = -(d(x129),s(y))
        
        -(d(d(x129)),y) = x129 + y + 2 >= x129 + y + 2 = -(d(x129),s(y))
        
        -(x,s(y)) = x + y + 1 >= x + y + 1 = -(d(x),y)
        
        d(s(x)) = x + 2 >= x = x
        
        -(d(x),y) = x + y + 1 >= x + y + 1 = -(x,s(y))
       problem:
        
        strict:
         -(s(x),s(y)) -> -(d(s(x)),y)
         -(d(x),s(x125)) -> -(d(d(x)),x125)
         -(d(x),s(x125)) -> -(x,s(s(x125)))
         -(d(d(x)),x125) -> -(d(x),s(x125))
         -(x,s(s(x125))) -> -(d(x),s(x125))
         -(d(s(x126)),y) -> -(s(x126),s(y))
         -(s(x127),s(y)) -> -(d(s(x127)),y)
         -(d(x129),s(y)) -> -(x129,s(s(y)))
         -(d(x129),s(y)) -> -(d(d(x129)),y)
         -(x129,s(s(y))) -> -(d(x129),s(y))
         -(d(d(x129)),y) -> -(d(x129),s(y))
        weak:
         -(x,s(y)) -> -(d(x),y)
         -(d(x),y) -> -(x,s(y))
       Shift Processor (ldh) lab=left (force):
        
        strict:
         
        weak:
         
        Rule Labeling Processor:
         
         strict:
          
         weak:
          
         rule labeling (left):
          -(0(),0()) -> 0(): 0
          -(s(x),0()) -> s(x): 0
          -(x,s(y)) -> -(d(x),y): 0
          d(s(x)) -> x: 0
          -(s(x),s(y)) -> -(x,y): 1
          -(d(x),y) -> -(x,s(y)): 2
         Decreasing Processor:
          The following diagrams are decreasing:
          peak:
           -(d(s(x)),y) <-2|[0,1,0,0]- -(s(x),s(y)) -4|[1,1,0,0]-> -(x,y)
          joins:
           -(d(s(x)),y) -3|0[0,1,2,0]-> -(x,y)
           
          peak:
           -(d(d(x)),x125) <-2|[0,1,0,0]- -(d(x),s(x125)) -5|[2,1,0,0]-> -(x,s(s(x125)))
          joins:
           -(d(d(x)),x125) -5|[2,1,0,0]-> -(d(x),s(x125))
           -(x,s(s(x125))) -2|[0,1,0,0]-> -(d(x),s(x125))
          peak:
           -(x126,y) <-3|0[0,1,2,0]- -(d(s(x126)),y) -5|[2,1,0,0]-> -(s(x126),s(y))
          joins:
           
           -(s(x126),s(y)) -4|[1,1,0,0]-> -(x126,y)
          peak:
           -(x127,y) <-4|[1,1,0,0]- -(s(x127),s(y)) -2|[0,1,0,0]-> -(d(s(x127)),y)
          joins:
           
           -(d(s(x127)),y) -3|0[0,1,2,0]-> -(x127,y)
          peak:
           -(x129,s(s(y))) <-5|[2,1,0,0]- -(d(x129),s(y)) -2|[0,1,0,0]-> -(d(d(x129)),y)
          joins:
           -(x129,s(s(y))) -2|[0,1,0,0]-> -(d(x129),s(y))
           -(d(d(x129)),y) -5|[2,1,0,0]-> -(d(x129),s(y))
          Qed