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(n__s(X))) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Proof: DP Processor: DPs: first#(s(X),cons(Y,Z)) -> activate#(Z) activate#(n__first(X1,X2)) -> activate#(X2) activate#(n__first(X1,X2)) -> activate#(X1) activate#(n__first(X1,X2)) -> first#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(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(n__s(X))) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Matrix Interpretation Processor: dim=1 interpretation: [s#](x0) = 0, [from#](x0) = 3/2, [activate#](x0) = x0, [first#](x0, x1) = 2x1, [n__from](x0) = 2x0 + 2, [n__s](x0) = 2x0 + 1/2, [from](x0) = 2x0 + 2, [n__first](x0, x1) = x0 + 2x1 + 2, [activate](x0) = x0, [cons](x0, x1) = 1/2x1 + 1/2, [s](x0) = 2x0 + 1/2, [nil] = 0, [first](x0, x1) = x0 + 2x1 + 2, [0] = 5/2 orientation: first#(s(X),cons(Y,Z)) = Z + 1 >= Z = activate#(Z) activate#(n__first(X1,X2)) = X1 + 2X2 + 2 >= X2 = activate#(X2) activate#(n__first(X1,X2)) = X1 + 2X2 + 2 >= X1 = activate#(X1) activate#(n__first(X1,X2)) = X1 + 2X2 + 2 >= 2X2 = first#(activate(X1),activate(X2)) activate#(n__from(X)) = 2X + 2 >= X = activate#(X) activate#(n__from(X)) = 2X + 2 >= 3/2 = from#(activate(X)) activate#(n__s(X)) = 2X + 1/2 >= X = activate#(X) activate#(n__s(X)) = 2X + 1/2 >= 0 = s#(activate(X)) first(0(),X) = 2X + 9/2 >= 0 = nil() first(s(X),cons(Y,Z)) = 2X + Z + 7/2 >= 1/2X + Z + 3/2 = cons(Y,n__first(X,activate(Z))) from(X) = 2X + 2 >= 2X + 2 = cons(X,n__from(n__s(X))) first(X1,X2) = X1 + 2X2 + 2 >= X1 + 2X2 + 2 = n__first(X1,X2) from(X) = 2X + 2 >= 2X + 2 = n__from(X) s(X) = 2X + 1/2 >= 2X + 1/2 = n__s(X) activate(n__first(X1,X2)) = X1 + 2X2 + 2 >= X1 + 2X2 + 2 = first(activate(X1),activate(X2)) activate(n__from(X)) = 2X + 2 >= 2X + 2 = from(activate(X)) activate(n__s(X)) = 2X + 1/2 >= 2X + 1/2 = s(activate(X)) activate(X) = X >= X = X 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(n__s(X))) first(X1,X2) -> n__first(X1,X2) from(X) -> n__from(X) s(X) -> n__s(X) activate(n__first(X1,X2)) -> first(activate(X1),activate(X2)) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(X) -> X Qed