YES TRS: a__nats() -> cons(0(),incr(nats())) a__pairs() -> cons(0(),incr(odds())) a__odds() -> a__incr(a__pairs()) a__incr(cons(X,XS)) -> cons(s(mark(X)),incr(XS)) a__head(cons(X,XS)) -> mark(X) a__tail(cons(X,XS)) -> mark(XS) mark(nats()) -> a__nats() mark(pairs()) -> a__pairs() mark(odds()) -> a__odds() mark(incr(X)) -> a__incr(mark(X)) mark(head(X)) -> a__head(mark(X)) mark(tail(X)) -> a__tail(mark(X)) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(nil()) -> nil() mark(cons(X1,X2)) -> cons(mark(X1),X2) a__nats() -> nats() a__pairs() -> pairs() a__odds() -> odds() a__incr(X) -> incr(X) a__head(X) -> head(X) a__tail(X) -> tail(X) max/plus interpretations on N: a__nats_A = 33 a__nats#_A = 42 cons_A(x1,x2) = max{12, 20 + x1, -19 + x2} cons#_A(x1,x2) = max{1, 41, -1} 0_A = 5 0#_A = 36 incr_A(x1) = max{52, 12 + x1} incr#_A(x1) = max{21, 41} nats_A = 28 nats#_A = 0 a__pairs_A = 40 a__pairs#_A = 42 odds_A = 47 odds#_A = 0 a__odds_A = 52 a__odds#_A = 62 a__incr_A(x1) = max{52, 12 + x1} a__incr#_A(x1) = max{41, 21 + x1} s_A(x1) = max{5, 7 + x1} s#_A(x1) = max{0, 31} mark_A(x1) = max{4, 5 + x1} mark#_A(x1) = max{32, 30 + x1} a__head_A(x1) = max{3, x1} a__head#_A(x1) = max{22, 24 + x1} a__tail_A(x1) = max{34, 28 + x1} a__tail#_A(x1) = max{59, 52 + x1} pairs_A = 35 pairs#_A = 0 head_A(x1) = max{3, x1} head#_A(x1) = max{21, 23 + x1} tail_A(x1) = max{30, 28 + x1} tail#_A(x1) = max{53, 0} nil_A = 0 nil#_A = 31 precedence: a__tail > mark > a__pairs = a__head = tail = nil > 0 = a__odds = pairs = head > a__nats = odds = a__incr > cons = incr = nats > s