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