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) KBO Processor: argument filtering: pi(f) = [] pi(a) = [] pi(g) = [0] pi(f#) = 0 weight function: w0 = 1 w(f#) = w(g) = w(a) = w(f) = 1 precedence: f# ~ g ~ f > a problem: DPs: TRS: f(x,x) -> a() f(g(x),y) -> f(x,y) Qed