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 Usable Rule Processor: DPs: f#(X) -> f#(X) activate#(n__h(X)) -> h#(X) TRS: ADG Processor: DPs: f#(X) -> f#(X) activate#(n__h(X)) -> h#(X) TRS: graph: f#(X) -> f#(X) -> f#(X) -> f#(X) Restore Modifier: 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 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