YES Problem: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) Proof: DP Processor: DPs: g#(g(x)) -> h#(g(x)) g#(g(x)) -> g#(h(g(x))) h#(h(x)) -> h#(f(h(x),x)) TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) TDG Processor: DPs: g#(g(x)) -> h#(g(x)) g#(g(x)) -> g#(h(g(x))) h#(h(x)) -> h#(f(h(x),x)) TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) graph: h#(h(x)) -> h#(f(h(x),x)) -> h#(h(x)) -> h#(f(h(x),x)) g#(g(x)) -> h#(g(x)) -> h#(h(x)) -> h#(f(h(x),x)) g#(g(x)) -> g#(h(g(x))) -> g#(g(x)) -> g#(h(g(x))) g#(g(x)) -> g#(h(g(x))) -> g#(g(x)) -> h#(g(x)) EDG Processor: DPs: g#(g(x)) -> h#(g(x)) g#(g(x)) -> g#(h(g(x))) h#(h(x)) -> h#(f(h(x),x)) TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) graph: g#(g(x)) -> h#(g(x)) -> h#(h(x)) -> h#(f(h(x),x)) g#(g(x)) -> g#(h(g(x))) -> g#(g(x)) -> h#(g(x)) g#(g(x)) -> g#(h(g(x))) -> g#(g(x)) -> g#(h(g(x))) CDG Processor: DPs: g#(g(x)) -> h#(g(x)) g#(g(x)) -> g#(h(g(x))) h#(h(x)) -> h#(f(h(x),x)) TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) graph: Qed