YES Problem: f(0()) -> cons(0(),n__f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X Proof: DP Processor: DPs: f#(s(0())) -> p#(s(0())) f#(s(0())) -> f#(p(s(0()))) activate#(n__f(X)) -> f#(X) TRS: f(0()) -> cons(0(),n__f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X TDG Processor: DPs: f#(s(0())) -> p#(s(0())) f#(s(0())) -> f#(p(s(0()))) activate#(n__f(X)) -> f#(X) TRS: f(0()) -> cons(0(),n__f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X graph: activate#(n__f(X)) -> f#(X) -> f#(s(0())) -> f#(p(s(0()))) activate#(n__f(X)) -> f#(X) -> f#(s(0())) -> p#(s(0())) f#(s(0())) -> f#(p(s(0()))) -> f#(s(0())) -> f#(p(s(0()))) f#(s(0())) -> f#(p(s(0()))) -> f#(s(0())) -> p#(s(0())) SCC Processor: #sccs: 1 #rules: 1 #arcs: 4/9 DPs: f#(s(0())) -> f#(p(s(0()))) TRS: f(0()) -> cons(0(),n__f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X CDG Processor: DPs: f#(s(0())) -> f#(p(s(0()))) TRS: f(0()) -> cons(0(),n__f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(0())) -> 0() f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X graph: Qed