YES

Problem:
 minus(x,0()) -> x
 minus(s(x),s(y)) -> minus(x,y)
 quot(0(),s(y)) -> 0()
 quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
 plus(0(),y) -> y
 plus(s(x),y) -> s(plus(x,y))
 plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))

Proof:
 DP Processor:
  DPs:
   minus#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> minus#(x,y)
   quot#(s(x),s(y)) -> quot#(minus(x,y),s(y))
   plus#(s(x),y) -> plus#(x,y)
   plus#(minus(x,s(0())),minus(y,s(s(z)))) -> plus#(minus(y,s(s(z))),minus(x,s(0())))
  TRS:
   minus(x,0()) -> x
   minus(s(x),s(y)) -> minus(x,y)
   quot(0(),s(y)) -> 0()
   quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
   plus(0(),y) -> y
   plus(s(x),y) -> s(plus(x,y))
   plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
  Matrix Interpretation Processor: dim=3
   
   interpretation:
    [plus#](x0, x1) = [0 1 0]x0 + [1 0 0]x1,
    
    [quot#](x0, x1) = [0 0 1]x0,
    
    [minus#](x0, x1) = [0 0 1]x0,
    
                     [0 1 0]       
    [plus](x0, x1) = [0 1 0]x0 + x1
                     [0 0 1]       ,
    
                     [0 0 0]     [0 0 0]     [1]
    [quot](x0, x1) = [0 0 1]x0 + [0 1 0]x1 + [0]
                     [0 0 1]     [1 0 0]     [0],
    
                   [0]
    [s](x0) = x0 + [1]
                   [1],
    
                      [1 1 0]     [1 1 0]  
    [minus](x0, x1) = [1 1 0]x0 + [1 0 0]x1
                      [0 0 1]     [0 0 0]  ,
    
          [1]
    [0] = [0]
          [1]
   orientation:
    minus#(s(x),s(y)) = [0 0 1]x + [1] >= [0 0 1]x = minus#(x,y)
    
    quot#(s(x),s(y)) = [0 0 1]x + [1] >= [0 0 1]x = minus#(x,y)
    
    quot#(s(x),s(y)) = [0 0 1]x + [1] >= [0 0 1]x = quot#(minus(x,y),s(y))
    
    plus#(s(x),y) = [0 1 0]x + [1 0 0]y + [1] >= [0 1 0]x + [1 0 0]y = plus#(x,y)
    
    plus#(minus(x,s(0())),minus(y,s(s(z)))) = [1 1 0]x + [1 1 0]y + [1 1 0]z + [3] >= [1 1 0]x + [1 1 0]y + [1 0 0]z + [2] = plus#(minus(y,s(s(z))),minus(x,s(0())))
    
                   [1 1 0]    [1]         
    minus(x,0()) = [1 1 0]x + [1] >= x = x
                   [0 0 1]    [0]         
    
                       [1 1 0]    [1 1 0]    [2]    [1 1 0]    [1 1 0]              
    minus(s(x),s(y)) = [1 1 0]x + [1 0 0]y + [1] >= [1 1 0]x + [1 0 0]y = minus(x,y)
                       [0 0 1]    [0 0 0]    [1]    [0 0 1]    [0 0 0]              
    
                     [0 0 0]    [1]    [1]      
    quot(0(),s(y)) = [0 1 0]y + [2] >= [0] = 0()
                     [1 0 0]    [1]    [1]      
    
                      [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [1]                           
    quot(s(x),s(y)) = [0 0 1]x + [0 1 0]y + [2] >= [0 0 1]x + [0 1 0]y + [2] = s(quot(minus(x,y),s(y)))
                      [0 0 1]    [1 0 0]    [1]    [0 0 1]    [1 0 0]    [1]                           
    
                      [0]         
    plus(0(),y) = y + [0] >= y = y
                      [1]         
    
                   [0 1 0]        [1]    [0 1 0]        [0]               
    plus(s(x),y) = [0 1 0]x + y + [1] >= [0 1 0]x + y + [1] = s(plus(x,y))
                   [0 0 1]        [1]    [0 0 1]        [1]               
    
                                             [1 1 0]    [1 1 0]    [1 1 0]    [3]    [1 1 0]    [1 1 0]    [1 0 0]    [2]                                         
    plus(minus(x,s(0())),minus(y,s(s(z)))) = [1 1 0]x + [1 1 0]y + [1 0 0]z + [1] >= [1 1 0]x + [1 1 0]y + [1 0 0]z + [1] = plus(minus(y,s(s(z))),minus(x,s(0())))
                                             [0 0 1]    [0 0 1]    [0 0 0]    [0]    [0 0 1]    [0 0 1]    [0 0 0]    [0]                                         
   problem:
    DPs:
     
    TRS:
     minus(x,0()) -> x
     minus(s(x),s(y)) -> minus(x,y)
     quot(0(),s(y)) -> 0()
     quot(s(x),s(y)) -> s(quot(minus(x,y),s(y)))
     plus(0(),y) -> y
     plus(s(x),y) -> s(plus(x,y))
     plus(minus(x,s(0())),minus(y,s(s(z)))) -> plus(minus(y,s(s(z))),minus(x,s(0())))
   Qed