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()) TDG Processor: DPs: f#(a()) -> f#(b()) g#(b()) -> g#(a()) TRS: f(a()) -> f(b()) g(b()) -> g(a()) graph: g#(b()) -> g#(a()) -> g#(b()) -> g#(a()) f#(a()) -> f#(b()) -> f#(a()) -> f#(b()) SCC Processor: #sccs: 2 #rules: 2 #arcs: 2/4 DPs: f#(a()) -> f#(b()) TRS: f(a()) -> f(b()) g(b()) -> g(a()) EDG Processor: DPs: f#(a()) -> f#(b()) TRS: f(a()) -> f(b()) g(b()) -> g(a()) graph: Qed DPs: g#(b()) -> g#(a()) TRS: f(a()) -> f(b()) g(b()) -> g(a()) EDG Processor: DPs: g#(b()) -> g#(a()) TRS: f(a()) -> f(b()) g(b()) -> g(a()) graph: Qed