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