YES Problem: f(s(x)) -> f(g(x,x)) g(0(),1()) -> s(0()) 0() -> 1() Proof: DP Processor: DPs: f#(s(x)) -> g#(x,x) f#(s(x)) -> f#(g(x,x)) TRS: f(s(x)) -> f(g(x,x)) g(0(),1()) -> s(0()) 0() -> 1() CDG Processor: DPs: f#(s(x)) -> g#(x,x) f#(s(x)) -> f#(g(x,x)) TRS: f(s(x)) -> f(g(x,x)) g(0(),1()) -> s(0()) 0() -> 1() graph: Qed