YES Problem: f(a()) -> f(b()) g(b()) -> g(a()) Proof: DP Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) TRS: f(a()) -> f(b()) g(b()) -> g(a()) Usable Rule Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) TRS: CDG Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) TRS: graph: Qed