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