YES

Problem:
 minus(minus(x)) -> x
 minus(+(x,y)) -> *(minus(minus(minus(x))),minus(minus(minus(y))))
 minus(*(x,y)) -> +(minus(minus(minus(x))),minus(minus(minus(y))))
 f(minus(x)) -> minus(minus(minus(f(x))))

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