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()) EDG 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()) graph: Qed