MAYBE Problem: f(x) -> f(g(x)) Proof: DP Processor: DPs: f#(x) -> f#(g(x)) TRS: f(x) -> f(g(x)) Usable Rule Processor: DPs: f#(x) -> f#(g(x)) TRS: Open