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(0())) -> g(d(1())) g(c(1())) -> g(d(0())) Proof: DP Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(0())) -> g#(d(1())) g#(c(1())) -> g#(d(0())) 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(0())) -> g(d(1())) g(c(1())) -> g(d(0())) Usable Rule Processor: DPs: f#(f(x)) -> f#(c(f(x))) f#(f(x)) -> f#(d(f(x))) g#(c(0())) -> g#(d(1())) g#(c(1())) -> g#(d(0())) 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 + 0, [1] = 3, [0] = 1, [d](x0) = 0, [c](x0) = 1, [f](x0) = 3x0 + 3 orientation: f#(f(x)) = 3x + 3 >= 1 = f#(c(f(x))) f#(f(x)) = 3x + 3 >= 0 = f#(d(f(x))) g#(c(0())) = 1 >= 0 = g#(d(1())) g#(c(1())) = 1 >= 0 = g#(d(0())) f(f(x)) = 6x + 6 >= 4 = f(c(f(x))) f(f(x)) = 6x + 6 >= 3 = f(d(f(x))) problem: DPs: TRS: f(f(x)) -> f(c(f(x))) f(f(x)) -> f(d(f(x))) Qed