YES Problem: first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(s(X))) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Proof: DP Processor: DPs: first#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__first(X1,X2)) -> first#(X1,X2) activate#(n__from(X)) -> from#(X) TRS: first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(s(X))) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X KBO Processor: argument filtering: pi(0) = [] pi(first) = [0,1] pi(nil) = [] pi(s) = [0] pi(cons) = 1 pi(activate) = [0] pi(n__first) = [0,1] pi(from) = [] pi(n__from) = [] pi(first#) = [1] pi(activate#) = 0 pi(from#) = [] weight function: w0 = 1 w(from#) = w(n__from) = w(from) = w(activate) = w(s) = w(nil) = w( first) = w(0) = 1 w(activate#) = w(first#) = w(n__first) = w(cons) = 0 precedence: first# ~ s ~ nil ~ 0 > from > n__from > activate > from# ~ activate# ~ n__first ~ cons ~ first problem: DPs: TRS: first(0(),X) -> nil() first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z))) from(X) -> cons(X,n__from(s(X))) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) activate(n__first(X1,X2)) -> first(X1,X2) activate(n__from(X)) -> from(X) activate(X) -> X Qed