YES TRS: active(from(X)) -> mark(cons(X,from(s(X)))) active(length(nil())) -> mark(0()) active(length(cons(X,Y))) -> mark(s(length1(Y))) active(length1(X)) -> mark(length(X)) mark(from(X)) -> active(from(mark(X))) mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) mark(s(X)) -> active(s(mark(X))) mark(length(X)) -> active(length(X)) mark(nil()) -> active(nil()) mark(0()) -> active(0()) mark(length1(X)) -> active(length1(X)) from(mark(X)) -> from(X) from(active(X)) -> from(X) cons(mark(X1),X2) -> cons(X1,X2) cons(X1,mark(X2)) -> cons(X1,X2) cons(active(X1),X2) -> cons(X1,X2) cons(X1,active(X2)) -> cons(X1,X2) s(mark(X)) -> s(X) s(active(X)) -> s(X) length(mark(X)) -> length(X) length(active(X)) -> length(X) length1(mark(X)) -> length1(X) length1(active(X)) -> length1(X) max/plus interpretations on N: active_A(x1) = max{61, x1} active#_A(x1) = max{14, -51 + x1} from_A(x1) = max{52, 83 + x1} from#_A(x1) = max{0, 4} mark_A(x1) = max{24, 54 + x1} mark#_A(x1) = max{16, 5 + x1} cons_A(x1,x2) = max{25, 26 + x1, -1} cons#_A(x1,x2) = max{21, -39 + x1, -2} s_A(x1) = max{7, x1} s#_A(x1) = max{15, 11} length_A(x1) = max{7, 6} length#_A(x1) = max{18, 19} nil_A = 8 nil#_A = 15 0_A = 7 0#_A = 13 length1_A(x1) = max{6, 7} length1#_A(x1) = max{17, 20} precedence: active > cons > length1 > mark > length = nil > s = 0 > from