MAYBE Problem: f(X) -> g(n__h(f(X))) h(X) -> n__h(X) activate(n__h(X)) -> h(X) activate(X) -> X Proof: DP Processor: DPs: f#(X) -> f#(X) activate#(n__h(X)) -> h#(X) TRS: f(X) -> g(n__h(f(X))) h(X) -> n__h(X) activate(n__h(X)) -> h(X) activate(X) -> X ADG Processor: DPs: f#(X) -> f#(X) activate#(n__h(X)) -> h#(X) TRS: f(X) -> g(n__h(f(X))) h(X) -> n__h(X) activate(n__h(X)) -> h(X) activate(X) -> X graph: f#(X) -> f#(X) -> f#(X) -> f#(X) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/4 DPs: f#(X) -> f#(X) TRS: f(X) -> g(n__h(f(X))) h(X) -> n__h(X) activate(n__h(X)) -> h(X) activate(X) -> X Open