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