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() TDG 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: f#(s(x)) -> f#(g(x,x)) -> f#(s(x)) -> f#(g(x,x)) f#(s(x)) -> f#(g(x,x)) -> f#(s(x)) -> g#(x,x) EDG 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