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)) ADG 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))) Restore Modifier: 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)) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: g#(g(x)) -> g#(h(g(x))) TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) Matrix Interpretation Processor: dimension: 1 interpretation: [g#](x0) = x0, [f](x0, x1) = 0, [h](x0) = 0, [g](x0) = 1 orientation: g#(g(x)) = 1 >= 0 = g#(h(g(x))) g(h(g(x))) = 1 >= 1 = g(x) g(g(x)) = 1 >= 1 = g(h(g(x))) h(h(x)) = 0 >= 0 = h(f(h(x),x)) problem: DPs: TRS: g(h(g(x))) -> g(x) g(g(x)) -> g(h(g(x))) h(h(x)) -> h(f(h(x),x)) Qed