YES

Problem:
 f(x,x) -> a()
 f(g(x),y) -> f(x,y)

Proof:
 DP Processor:
  DPs:
   f#(g(x),y) -> f#(x,y)
  TRS:
   f(x,x) -> a()
   f(g(x),y) -> f(x,y)
  Usable Rule Processor:
   DPs:
    f#(g(x),y) -> f#(x,y)
   TRS:
    
   KBO Processor:
    argument filtering:
     pi(g) = [0]
     pi(f#) = [0,1]
    usable rules:
     
    weight function:
     w0 = 1
     w(f#) = 1
     w(g) = 0
    precedence:
     f# ~ g
    problem:
     DPs:
      
     TRS:
      
    Qed