YES Problem: f(f(x)) -> f(x) g(0()) -> g(f(0())) Proof: DP Processor: DPs: g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: f(f(x)) -> f(x) g(0()) -> g(f(0())) Usable Rule Processor: DPs: g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: TDG Processor: DPs: g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: graph: g#(0()) -> g#(f(0())) -> g#(0()) -> g#(f(0())) g#(0()) -> g#(f(0())) -> g#(0()) -> f#(0()) EDG Processor: DPs: g#(0()) -> f#(0()) g#(0()) -> g#(f(0())) TRS: graph: Qed