YES Problem: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) Proof: DP Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) f#(x) -> g#(x) TRS: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) Matrix Interpretation Processor: dim=4 interpretation: [g#](x0) = [0 0 1 0]x0, [f#](x0) = [1 1 1 1]x0 + [1], [0] [0] [g](x0) = [0] [0], [0] [0] [b] = [1] [0], [1 0 0 0] [1] [0 0 0 0] [0] [f](x0) = [0 0 0 0]x0 + [0] [0 0 0 0] [0], [0] [1] [a] = [0] [1] orientation: f#(a()) = 3 >= 2 = f#(b()) g#(b()) = 1 >= 0 = g#(a()) f#(x) = [1 1 1 1]x + [1] >= [0 0 1 0]x = g#(x) [1] [1] [0] [0] f(a()) = [0] >= [0] = f(b()) [0] [0] [0] [0] [0] [0] g(b()) = [0] >= [0] = g(a()) [0] [0] [1 0 0 0] [1] [0] [0 0 0 0] [0] [0] f(x) = [0 0 0 0]x + [0] >= [0] = g(x) [0 0 0 0] [0] [0] problem: DPs: TRS: f(a()) -> f(b()) g(b()) -> g(a()) f(x) -> g(x) Qed