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