YES

Problem:
 g(0(),f(x,x)) -> x
 g(x,s(y)) -> g(f(x,y),0())
 g(s(x),y) -> g(f(x,y),0())
 g(f(x,y),0()) -> f(g(x,0()),g(y,0()))

Proof:
 DP Processor:
  DPs:
   g#(x,s(y)) -> g#(f(x,y),0())
   g#(s(x),y) -> g#(f(x,y),0())
   g#(f(x,y),0()) -> g#(y,0())
   g#(f(x,y),0()) -> g#(x,0())
  TRS:
   g(0(),f(x,x)) -> x
   g(x,s(y)) -> g(f(x,y),0())
   g(s(x),y) -> g(f(x,y),0())
   g(f(x,y),0()) -> f(g(x,0()),g(y,0()))
  Usable Rule Processor:
   DPs:
    g#(x,s(y)) -> g#(f(x,y),0())
    g#(s(x),y) -> g#(f(x,y),0())
    g#(f(x,y),0()) -> g#(y,0())
    g#(f(x,y),0()) -> g#(x,0())
   TRS:
    
   Matrix Interpretation Processor: dim=4
    
    usable rules:
     
    interpretation:
     [g#](x0, x1) = [0 1 1 1]x0 + [0 1 1 1]x1 + [1],
     
               [0 0 0 0]     [0]
               [0 0 0 0]     [0]
     [s](x0) = [0 0 0 1]x0 + [1]
               [0 1 1 0]     [1],
     
                   [0 0 0 0]     [0 0 0 0]     [0]
                   [0 0 1 0]     [0 1 0 1]     [0]
     [f](x0, x1) = [0 1 0 1]x0 + [0 0 1 0]x1 + [1]
                   [0 0 0 0]     [0 0 0 0]     [0],
     
           [0]
           [0]
     [0] = [0]
           [0]
    orientation:
     g#(x,s(y)) = [0 1 1 1]x + [0 1 1 1]y + [3] >= [0 1 1 1]x + [0 1 1 1]y + [2] = g#(f(x,y),0())
     
     g#(s(x),y) = [0 1 1 1]x + [0 1 1 1]y + [3] >= [0 1 1 1]x + [0 1 1 1]y + [2] = g#(f(x,y),0())
     
     g#(f(x,y),0()) = [0 1 1 1]x + [0 1 1 1]y + [2] >= [0 1 1 1]y + [1] = g#(y,0())
     
     g#(f(x,y),0()) = [0 1 1 1]x + [0 1 1 1]y + [2] >= [0 1 1 1]x + [1] = g#(x,0())
    problem:
     DPs:
      
     TRS:
      
    Qed