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