MAYBE Problem: f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(b()) -> c() b() -> c() g(X) -> n__g(X) activate(n__g(X)) -> g(X) activate(X) -> X Proof: DP Processor: DPs: f#(X,n__g(X),Y) -> activate#(Y) f#(X,n__g(X),Y) -> f#(activate(Y),activate(Y),activate(Y)) activate#(n__g(X)) -> g#(X) TRS: f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(b()) -> c() b() -> c() g(X) -> n__g(X) activate(n__g(X)) -> g(X) activate(X) -> X TDG Processor: DPs: f#(X,n__g(X),Y) -> activate#(Y) f#(X,n__g(X),Y) -> f#(activate(Y),activate(Y),activate(Y)) activate#(n__g(X)) -> g#(X) TRS: f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(b()) -> c() b() -> c() g(X) -> n__g(X) activate(n__g(X)) -> g(X) activate(X) -> X graph: f#(X,n__g(X),Y) -> activate#(Y) -> activate#(n__g(X)) -> g#(X) f#(X,n__g(X),Y) -> f#(activate(Y),activate(Y),activate(Y)) -> f#(X,n__g(X),Y) -> f#(activate(Y),activate(Y),activate(Y)) f#(X,n__g(X),Y) -> f#(activate(Y),activate(Y),activate(Y)) -> f#(X,n__g(X),Y) -> activate#(Y) SCC Processor: #sccs: 1 #rules: 1 #arcs: 3/9 DPs: f#(X,n__g(X),Y) -> f#(activate(Y),activate(Y),activate(Y)) TRS: f(X,n__g(X),Y) -> f(activate(Y),activate(Y),activate(Y)) g(b()) -> c() b() -> c() g(X) -> n__g(X) activate(n__g(X)) -> g(X) activate(X) -> X Open