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 KBO Processor: argument filtering: pi(n__g) = [0] pi(f) = [] pi(activate) = [0] pi(b) = [] pi(g) = [0] pi(c) = [] pi(activate#) = 0 weight function: w0 = 1 w(activate#) = w(c) = w(g) = w(b) = w(activate) = w(f) = w(n__g) = 1 precedence: activate# ~ b ~ activate ~ f > g > c ~ n__g 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