YES Problem: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X Proof: DP Processor: DPs: g#(s(X)) -> g#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) activate#(n__g(X)) -> activate#(X) activate#(n__g(X)) -> g#(activate(X)) TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X TDG Processor: DPs: g#(s(X)) -> g#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) activate#(n__f(X)) -> activate#(X) activate#(n__f(X)) -> f#(activate(X)) activate#(n__g(X)) -> activate#(X) activate#(n__g(X)) -> g#(activate(X)) TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X graph: activate#(n__f(X)) -> activate#(X) -> activate#(n__g(X)) -> g#(activate(X)) activate#(n__f(X)) -> activate#(X) -> activate#(n__g(X)) -> activate#(X) activate#(n__f(X)) -> activate#(X) -> activate#(n__f(X)) -> f#(activate(X)) activate#(n__f(X)) -> activate#(X) -> activate#(n__f(X)) -> activate#(X) 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(X)) -> f#(activate(X)) activate#(n__g(X)) -> activate#(X) -> activate#(n__f(X)) -> activate#(X) activate#(n__g(X)) -> g#(activate(X)) -> g#(s(X)) -> g#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__g(X)) -> g#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__g(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__f(X)) -> f#(activate(X)) sel#(s(X),cons(Y,Z)) -> activate#(Z) -> activate#(n__f(X)) -> activate#(X) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) -> sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) -> sel#(s(X),cons(Y,Z)) -> activate#(Z) g#(s(X)) -> g#(X) -> g#(s(X)) -> g#(X) SCC Processor: #sccs: 3 #rules: 4 #arcs: 16/49 DPs: sel#(s(X),cons(Y,Z)) -> sel#(X,activate(Z)) TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X LPO Processor: argument filtering: pi(f) = [0] pi(n__g) = [0] pi(n__f) = [0] pi(cons) = [0,1] pi(0) = [] pi(g) = [0] pi(s) = [0] pi(sel) = [0,1] pi(activate) = [0] pi(sel#) = [0] precedence: sel > activate > f > g > sel# ~ s ~ 0 ~ cons ~ n__f ~ n__g problem: DPs: TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X Qed DPs: activate#(n__f(X)) -> activate#(X) activate#(n__g(X)) -> activate#(X) TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X LPO Processor: argument filtering: pi(f) = [0] pi(n__g) = [0] pi(n__f) = [0] pi(cons) = [0,1] pi(0) = [] pi(g) = [0] pi(s) = [0] pi(sel) = [0,1] pi(activate) = [0] pi(activate#) = 0 precedence: sel > activate > g ~ f > activate# ~ s ~ 0 ~ cons ~ n__f ~ n__g problem: DPs: TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X Qed DPs: g#(s(X)) -> g#(X) TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X LPO Processor: argument filtering: pi(f) = [0] pi(n__g) = [0] pi(n__f) = [0] pi(cons) = [0,1] pi(0) = [] pi(g) = [0] pi(s) = [0] pi(sel) = [0,1] pi(activate) = [0] pi(g#) = [0] precedence: sel > activate > g ~ f > s > g# ~ 0 ~ cons ~ n__f ~ n__g problem: DPs: TRS: f(X) -> cons(X,n__f(n__g(X))) g(0()) -> s(0()) g(s(X)) -> s(s(g(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) f(X) -> n__f(X) g(X) -> n__g(X) activate(n__f(X)) -> f(activate(X)) activate(n__g(X)) -> g(activate(X)) activate(X) -> X Qed