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