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