MAYBE Problem: f(a()) -> f(a()) a() -> b() Proof: DP Processor: DPs: f#(a()) -> f#(a()) TRS: f(a()) -> f(a()) a() -> b() Usable Rule Processor: DPs: f#(a()) -> f#(a()) TRS: a() -> b() Restore Modifier: DPs: f#(a()) -> f#(a()) TRS: f(a()) -> f(a()) a() -> b() SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: f#(a()) -> f#(a()) TRS: f(a()) -> f(a()) a() -> b() Open