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()) Usable Rule Processor: DPs: f#(a(),b()) -> f#(a(),c()) f#(c(),d()) -> f#(b(),d()) TRS: Matrix Interpretation Processor: dim=4 usable rules: interpretation: [f#](x0, x1) = [1 1 0 1]x0 + [0 0 1 1]x1, [0] [0] [d] = [1] [0], [1] [1] [c] = [0] [0], [0] [0] [b] = [0] [1], [0] [0] [a] = [0] [0] orientation: f#(a(),b()) = 1 >= 0 = f#(a(),c()) f#(c(),d()) = 3 >= 2 = f#(b(),d()) problem: DPs: TRS: Qed