YES Problem: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Proof: DP Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) g(c(x)) -> x g(d(x)) -> x g(c(h(0()))) -> g(d(1())) g(c(1())) -> g(d(h(0()))) g(h(x)) -> g(x) Usable Rule Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(h(0()))) -> g#(d(1())) g#(c(1())) -> g#(d(h(0()))) g#(h(x)) -> g#(x) TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) Arctic Interpretation Processor: dimension: 1 usable rules: interpretation: [g#](x0) = x0 + 0, [f#](x0) = x0 + 2, [1] = 0, [h](x0) = 1x0 + 2, [0] = 0, [d](x0) = 0, [c](x0) = 1, [f](x0) = x0 + 3 orientation: f#(f(x)) = x + 3 >= 2 = f#(c(f(x))) f#(f(x)) = x + 3 >= 2 = f#(d(f(x))) g#(c(h(0()))) = 1 >= 0 = g#(d(1())) g#(c(1())) = 1 >= 0 = g#(d(h(0()))) g#(h(x)) = 1x + 2 >= x + 0 = g#(x) f(f(x)) = x + 3 >= 3 = f(c(f(x))) f(f(x)) = x + 3 >= 3 = f(d(f(x))) problem: DPs: TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) Qed