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