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: Restore Modifier: 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()) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 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: dimension: 1 interpretation: [f#](x0, x1) = x0, [d] = 0, [c] = 1, [f](x0, x1) = 0, [b] = 0, [a] = 0 orientation: f#(a(),b()) = 0 >= 0 = f#(a(),c()) f#(c(),d()) = 1 >= 0 = f#(b(),d()) f(a(),b()) = 0 >= 0 = f(a(),c()) f(c(),d()) = 0 >= 0 = f(b(),d()) problem: DPs: f#(a(),b()) -> f#(a(),c()) TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x1, [d] = 0, [c] = 0, [f](x0, x1) = 0, [b] = 1, [a] = 0 orientation: f#(a(),b()) = 1 >= 0 = f#(a(),c()) f(a(),b()) = 0 >= 0 = f(a(),c()) f(c(),d()) = 0 >= 0 = f(b(),d()) problem: DPs: TRS: f(a(),b()) -> f(a(),c()) f(c(),d()) -> f(b(),d()) Qed