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