YES Problem: f(0()) -> cons(0(),n__f(s(0()))) f(s(0())) -> f(p(s(0()))) p(s(X)) -> X 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(X)) -> X 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(X)) -> X 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())) CDG 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(X)) -> X f(X) -> n__f(X) activate(n__f(X)) -> f(X) activate(X) -> X graph: Qed