YES Problem: f(s(x),y) -> f(x,g(x,y)) f(0(),y) -> y g(x,y) -> y Proof: DP Processor: DPs: f#(s(x),y) -> g#(x,y) f#(s(x),y) -> f#(x,g(x,y)) TRS: f(s(x),y) -> f(x,g(x,y)) f(0(),y) -> y g(x,y) -> y LPO Processor: argument filtering: pi(s) = [0] pi(f) = 1 pi(g) = 1 pi(0) = [] pi(f#) = 0 pi(g#) = [] precedence: s > g# ~ f# ~ 0 ~ g ~ f problem: DPs: TRS: f(s(x),y) -> f(x,g(x,y)) f(0(),y) -> y g(x,y) -> y Qed