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(activate(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)) -> activate#(X) activate#(n__g(X)) -> g#(activate(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(activate(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)) -> activate#(X) activate#(n__g(X)) -> g#(activate(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(activate(X)) activate(X) -> X graph: 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) f#(X,n__g(X),Y) -> activate#(Y) -> activate#(n__g(X)) -> g#(activate(X)) f#(X,n__g(X),Y) -> activate#(Y) -> activate#(n__g(X)) -> activate#(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: 2 #rules: 2 #arcs: 6/16 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(activate(X)) activate(X) -> X Open DPs: activate#(n__g(X)) -> activate#(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(activate(X)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(activate#) = 0 problem: DPs: 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(activate(X)) activate(X) -> X Qed